SYMAC: Symbolic Execution Augmented with Concurrent Coverage Criteria

Symbolic execution [1] is an effective technique that is commonly used to analyse sequential [2, 3] and concurrent programs. However, when baseline symbolic algorithm is applied to system testing of multithreaded programs [4, 5, 6], the performance is limited by the space explosion problem [7, 8] of thread interleavings. Such a space explosion problem is raised by trying to explore all impossible interleavings that are intra-thread and inter-thread; this is due to the exponentially increment of the number of all possible thread interleavings which is influenced by the increase of the sum of threads. Many techniques have been proposed to address this problem, including the hybrid execution [9, 10, 20], the use of function summaries [11], the dependence analysis [12], partial order reduction [13, 14, 15, 21], and lazy annotation [16]. We present a framework named SYMAC that combined the symbolic algorithm with the hierarchical coverage criteria to reduce the space of thread interleavings. We give a new definition of Hierarchical Coverage Criteria based on History-aware Predecessor Set that is called HaPSet and can be generated from concurrent programs, and implemented an improved Symbolic algorithm based on the HaPSet. 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 the newly method and conducted a series of experiments. Our experiment results show that the new method is crucial in finding satisfactory trade-offs between the cost and performance in concurrent program testing.