System and method for monotonic partial order reduction
View Patent ↗A system and method for analyzing concurrent programs that guarantees optimality in the number of thread inter-leavings to be explored. Optimality is ensured by globally constraining the inter-leavings of the local operations of its threads so that only quasi-monotonic sequences of threads operations are explored. For efficiency, a SAT/SMT solver is used to explore the quasi-monotonic computations of the given concurrent program. Constraints are added dynamically during exploration of the concurrent program via a SAT/SMT solver to ensure quasi-montonicity for model checking.
1. A method for fixing errors in concurrent programs stored on a memory device, comprising:
inputting a concurrent program with at least two threads; and
efficiently exploring the state space of the concurrent program by analyzing only those inter-leavings of threads comprising the concurrent program that form quasi-monotonic sequences of thread operations;
generating witness traces for errors in the concurrent program detected through the state space search;
modifying the source code of the concurrent program to fix the errors based on the witness traces.
2. The method as recited in claim 1 , wherein exploring only quasi-monotonic sequences of thread operations includes forcing independent transitions accessing different shared variables to execute in increasing order of their thread identifiers unless dependencies between transitions resulting from accesses to the same shared variable force an out-of-order-execution in that transitions with higher thread identifiers are executed before transitions with lower thread identifiers.
3. The method as recited in claim 1 , wherein a SAT/SMT solver is employed to explore the quasi-monotonic computations of the concurrent program.
4. The method as recited in claim 3 , wherein constraints are added dynamically during exploration of the concurrent program via a SAT/SMT solver by using extra variables to track dependency chains in threads that are used to ensure quasi-monotonicity of thread sequences.
5. The method as recited in claim 1 , wherein the method is applicable to at least one of explicit-state and symbolic searching using a satisfiability solver.
6. The method as recited in claim 1 , wherein globally constraining transitions includes constraining a set of interleavings such that no two explored interleavings are equivalent or redundant.