Iterative Context Bounding for Systematic Testing of Multithreaded Programs

Multithreaded programs are difficult to get right because of unexpected interaction between concurrently executing threads. Traditional testing methods are inadequate for catching subtle concurrency errors which manifest themselves late in the development cycle and post-deployment. Model checking or systematic exploration of program behavior is a promising alternative to traditional testing methods. However, it is difficult to perform systematic search on large programs as the number of possible program behaviors grows explosively with the program size. Confronted with this state-explosion problem, traditional model checkers perform iterative depth-bounded search. Although effective for message-passing software, iterative depth-bounding is inadequate for multithreaded software. This paper proposes iterative context-bounding, a new search algorithm that systematically explores the executions of a multithreaded program in an order that prioritizes executions with fewer context switches. We distinguish between two kinds of context switches, preempting and nonpreempting, and show that bounding the number of preempting context switches to a small number significantly alleviates the state space explosion, without limiting the depth of the execution. We show both theoretically and empirically that context-bounded search is an effective method for exploring the behaviors of multithreaded programs. We have implemented our algorithm in two model checkers and applied it to a number of real-world multithreaded programs. The iterative context-bounding algorithm uncovered 7 previously unknown bugs in our benchmarks. Each of these bugs was exposed by an execution with at most two context switches. Our initial experience with the technique is very encouraging and demonstrates that iterative contextbounding is a significant improvement on existing techniques for testing multithreaded programs