Research Of Concurrent Program Testing Framework Based On Symbolic Execution

Symbolic execution is an effective technique that is commonly used to analyze sequential and concurrent programs.However,when applied to system testing of multithreaded programs,the performance is limited by the space explosion problem.Such a space explosion problem is raised by trying to cover all feasible thread interleavings;this is because that the number of thread interleavings is exponentially increased with the increase of the sum of threads.Thus,it is meaningful to find a tradeoff between effectiveness and accuracy through improving the baseline symbolic execution algorithm.We present a framework named SYMAC that denotes the symbolic executionalgorithm augmented with the concurrent coverage criteria to reduce the space of thread interleavings.We propose a definition of Hierarchical Coverage Criteria based on Access-conflict Predecessor Set that is called AcPSet and can be generated from concurrent programs through static analysis tool,and implemented an improved concurrent symbolic execution algorithm based on the AcPSet.We combined the improved Symbolic algorithm with an assertion guided pruning framework that prunes the interleavings which is guaranteed not to raise error by summarizing the reason why previous interleaving cannot leading to an error.We also use precise slicing of concurrent programs to further mitigate the influence of state space explosion.We have implemented our method and empirically evaluated on a large set of multithreaded C/C++ programs.Our experiment results show that the new method is crucial in finding satisfactory tradeoffs between the cost and performance in concurrent program testing.