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

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

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

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.