Testing Multithreaded Programs with Contextual Unfoldings and Dynamic Symbolic Execution

Systematic testing of multithreaded programs is challenging as possible execution paths depend not only on input values but also on how threads interleave their executions. As the number of all interleavings is typically too large to explore exhaustively, ways to avoid testing irrelevant interleavings are needed. We have previously presented a testing approach that is based on dynamic symbolic execution to handle input values and on Petri net unfoldings to succinctly represent how threads can interleave their executions. In this paper we improve this approach by using contextual nets instead of ordinary nets. This way, the interleavings of threads can be represented even more succinctly which allows the local states of threads to be covered with less test executions. Furthermore, the new approach makes it possible to test programs that create threads dynamically which was a limitation of the previous approach. We have implemented our improved algorithm in a testing tool for Java programs. Experiments demonstrate that the new approach can significantly reduce the number of needed tests to cover all the reachable local states of threads while keeping additional overhead required by the algorithm small.