System and method for verification of programs using threads having bounded lock chains

1. A method for model checking of concurrent multi-threaded programs with bounded lock chains, comprising:

analyzing individual program threads in a concurrent multi-threaded program, using a model checking program stored in a memory storage device, to determine sets of reachable states and lock access patterns for bounded lock chains by:

tracking sets of states reachable from a given set of states; and

tracking lock acquisitions and releases by maintaining a bi-directional lock causality graph;

using an acceptance condition of the lock causality graph to combine analysis results from multiple threads to determine whether there is a violation of a correctness property in the concurrent multi-threaded program;

reducing a reachability problem by taking a specialized cross product that removes pairs that are not reachable; and

keeping projection automata separate to circumvent a state explosion problem and avoid construction of a global automata.

2. The method as recited in claim 1 , wherein a lock causality automaton is employed to track the sets of states reachable from the given set of states in the concurrent multi-threaded program.

3. The method as recited in claim 2 , further comprising expressing a model checking problem as a reachability problem for regular sets of configurations accepted by the lock causality automaton.

4. The method as recited in claim 2 , wherein the lock causality automaton is built for each temporal operator appearing in a given correctness formula.

5. The method as recited in claim 2 , further comprising:

computing pre*-closures for the lock causality automaton with bounded lock chains by projecting the lock causality automaton onto individual threads; and

recovering the pre*-closures of lock causality automaton by removing pairs of local states that are unreachable by encoding reachability criterion in the acceptance condition.

6. The method as recited in claim 2 , further comprising composing a lock causality automaton for each operator to form a lock causality automaton for an entire formula.

7. The method as recited in claim 6 , wherein the entire formula is satisfied by the concurrent multi-threaded program if a language accepted by the lock causality automaton is non-empty.

8. The method as recited in claim 1 , wherein a length of lock chains is employed to compute a bound on a size of the bi-directional lock causality graph, and the method further comprising enumerating all acyclic lock causality graphs of a size of the bound.

9. The method as recited in claim 8 , wherein the acyclic lock causality graphs are employed to compute a lock causality automaton that captures a set of configurations reachable from a given set of regular configurations such that the lock causality automaton accepts sets of configurations of the concurrent multi-threaded program in accordance with set conditions.

10. A system for model checking of concurrent multi-threaded programs with bounded lock chains, comprising:

a memory storage device: and

a model checking program stored in the memory storage device and executed by one or more processing cores, the model checking program being configured to analyze, using a processor, individual program threads in a concurrent multi-threaded program stored on memory storage media to determine sets of reachable states and lock access patterns for bounded lock chains, the model checking program being configured to track sets of states reachable from a given set of states and track lock acquisitions and releases by maintaining a bi-directional lock causality graph in the memory storage device; the model checking program is configured to use an acceptance condition of the lock causality graph to combine analysis results from multiple threads to determine whether there is a violation of a correctness property in the concurrent multi-threaded program, to reduce a reachability problem by taking a specialized cross product that removes pairs that are not reachable, and to keep projection automata separate to circumvent a state explosion problem and avoid construction of a global automata.

11. The system as recited in claim 10 , further comprising lock causality automaton generated to track the sets of states reachable from the given set of states in the concurrent multi-threaded program.

12. The system as recited in claim 11 , wherein the lock causality automaton is built for each temporal operator appearing in a given correctness formula.

13. The system as recited in claim 11 , further comprising:

pre*-closures computed for the lock causality automaton with bounded lock chains by projecting the lock causality automaton onto individual threads, wherein the pre*-closures of lock causality automaton are recovered by taking a cross product that does not consider all resulting pairs of local control states of the individual threads, but removes the pairs that are not reachable.

14. The system as recited in claim 11 , wherein a lock causality automata is included for each operator to form a lock causality automaton for an entire formula.

15. The system as recited in claim 14 , wherein, the entire formula is satisfied by the concurrent multi-threaded program if a language accepted by the lock causality automaton is non-empty.