Partial-Order Reduction for Context-Bounded State Exploration

Iterative context-bounding is a technique for performing prioritized search of the state-space of multithreaded programs. A context switch occurs in a concurrent execution when a thread temporarily stops and a different thread resumes. Iterative context-bounding gives priority to executions with fewer context switches during state-space search, exploring for a given context-bound c only those executions in which the number of context switches is at most c. Prior work has shown that this search algorithm is effective in finding many subtle concurrency errors in large programs. Partial-order reduction has traditionally been applied in complete state-space search and depth-bounded search for reducing the cost of state exploration; however, these techniques have not been applied to context-bounded search. As we show in our paper, it is difficult to perform partial-order reduction during a context-bounded search because of subtle interactions between the two techniques. The main contribution of our paper is an algorithm for performing partial-order reduction for context-bounded state exploration.