关键词: 上下文定界；并发；可达性分析；Fork/Join并行性；动态线程创建

Abstract:

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.

Key words: contextbounded;concurrency;reachability analysis;fork/join parallelism;dynamic thread creation