钱俊彦，贾书贵，蔡国永，赵岭忠

（1.桂林电子科技大学计算机科学与工程学院，广西 桂林 541004）；2.并行与分布处理国家重点实验室，湖南 长沙 410073）

1 引言

无论从理论，还是实践角度来看，并发程序验证都是极具挑战性的问题。随着多核技术日益发展，通过引入Fork／Join并行性，并发程序将任务分解为更细粒度的子任务并行执行，从而充分利用多核处理器提供的计算性能［1］。但是，多个线程之间的交错执行可能会产生隐匿的错误和漏洞，故保证并发程序的正确性具有十分重要的意义［2］。近些年提出的上下文定界方法是一种适合并发程序的分析技术，其思想是仅考虑有限次上下文切换（控制权从一个线程切换到另一个线程）之内程序执行的计算。由于在有限次上下文切换之内可发现许多并发相关的错误，上下文定界思想有助于程序分析。在程序中存在递归和过程调用的情况下，虽然被搜索的状态空间是无界的，但上下文定界可达问题是可判定的［3］。

针对Fork／Join并行性的并发程序进行可达性分析，主要基于以下考虑：Fork／Join 并行性涉及到动态线程创建，而动态线程创建对于构建操作系统的组件是非常重要的［4］。例如：（1）文件系统、设备驱动、无封装数据结构等软件模块的无界并发执行；（2）异步行为的生成：例如创建一个线程、回调函数等；（3）实现应用软件的并行化执行，充分利用多核体系结构的强大性能。

2 下推系统

3 并发下推系统

3.1 定界可达问题

3.2 k－定界可达算法

Qadeer提出的上下文定界模型检验算法假设全局状态集合G 是有限的。……