基于上下文定界的Fork/Join并行性的并发程序可达性分析

Context-bounded analysis of concurrent programs with Fork/Join parallelism

随着多核技术日益发展,并发程序通过引入Fork/Join并行性,将任务分解为更细粒度的子任务并行执行,从而充分利用多核处理器提供的计算性能。并发执行线程之间的交错可能产生隐匿的程序设计错误,因此有必要对此类并发程序的正确性进行分析。上下文定界分析方法是一种检测并发程序中隐匿错误的高效方法,计算线程有限次上下文切换内的可达状态,确定错误状态是否可达。针对Fork/Join并行性的并发程序的可达性分析思想如下:首先,动态并发程序被建模为可模拟线程Fork/Join操作的动态并发下推系统P;然后从P中提取模拟其k-定界执行的并发下推系统Pk。现有的上下文定界可达算法可解决提取后的并发下推系统的k-定界可达性问题。

As multicore technique has been well developed, in order to utilize the computing power provided by multicore processor, concurrent programs bring in Fork/Join parallelism to decompose a task into finegrained subtasks. But interaction among concurrent threads results in insidious programming errors, it is necessary to analyze the correctness of these concurrent programs. Contextbounded analysis is an efficient method for finding insidious errors in concurrent programs by computing reachable states in a run within a bounded number of context switches, it determines whether an error state is reachable or not. In this paper, we perform reachablility analysis for concurrent programs with Fork/Join parallelism. The main idea is as follows： dynamic concurrent programs is modeled as an abstract modeldynamic concurrent pushdown system P, the abstract model can simulate the Fork/Join operation, then a concurrent pushdown system P can be abstracted from dynamic pushdown system that simulate the kbounded execution of P, and the kreachability problems of abstracted Pk can be solved by existing contextbounded reachability algorithm.