Universal causality graphs for bug detection in concurrent programs

1. A method for predictive analysis, comprising:

generating an execution trace on an instrumented version of source code for a multithreaded computer program stored on computer readable storage media;

statically generating interleavings which lead to a violation in the program by performing a static predictive analysis using a Universal Causality Graph (UCG) to generate alternative interleavings that lead to an error, the UCG being a unified happens-before model for the concurrent program and a property being analyzed;

symbolically checking the interleavings to determine errors in the program; and

decomposing lengths of computations of the UCG into smaller segments, which are lock-free and there does not exist a wait/notify seed edge, a fork join seed edge or a property seed edge with endpoints along the segments,

wherein the UCG is configured to capture, as happens-before constraints, a set of all interleavings that are possible under scheduling constraints imposed by synchronization primitives that lead to violations of the property, and

wherein the Universal Causality Graph incorporates happens-before constraints arising from the concurrent program and a correctness property.

2. The method as recited in claim 1 , wherein the static predictive analysis using a Universal Causality Graph (UCG) is performed to isolate locations that violate the correctness property being checked.

3. The method as recited in claim 1 , wherein decomposing the UCG increases scalability of the predictive analysis.

4. The method as recited in claim 1 , wherein the UCG handles all standard synchronization primitives in threads.

5. A non-transitory computer readable storage medium comprising a computer readable program for predictive analysis, wherein the computer readable program when executed on a computer causes the computer to perform the steps of:

generating an execution trace on an instrumented version of source code for a multithreaded computer program;

statically generating interleavings which lead to a violation in the program by performing a static predictive analysis using a Universal Causality Graph (UCG) to generate alternative interleavings that lead to an error, the UCG being a unified happens-before model for the concurrent program and a property being analyzed;

symbolically checking the interleavings to determine errors in the program; and

decomposing lengths of computations of the UCG into smaller segments, which are lock-free and there does not exist a wait/notify seed edge, a fork join seed edge or a property seed edge with endpoints along the segments,

wherein the UCG is configured to capture, as happens-before constraints, a set of all interleavings that are possible under scheduling constraints imposed by synchronization primitives that lead to violations of the property, and

wherein the Universal Causality Graph incorporates happens-before constraints arising from the concurrent program and a correctness property.

6. The non-transitory computer readable storage medium as recited in claim 5 , wherein a static predictive analysis using a Universal Causality Graph (UCG) is performed to isolate locations that violate the correctness property being checked.

7. The non-transitory computer readable storage medium as recited in claim 5 , wherein decomposing the UCG increases scalability of the predictive analysis.

8. The non-transitory computer readable storage medium as recited in claim 5 , wherein the UCG handles all standard synchronization primitives in threads.

9. A system for predictive analysis, comprising:

a source code instrumentation module stored on non-transitory computer readable storage media and configured to generate an instrumented version of source code for a multithreaded computer program;

a predictive analysis module configured to statically generate interleavings which lead to a violation in an execution trace of the program by performing a static predictive analysis using a Universal Causality Graph (UCG) to generate alternative interleavings that lead to an error, the UCG being a unified happens-before model for the program and a property being analyzed; and

a symbolic checker to check the interleavings to determine errors in the program,

wherein lengths of computations of the UCG are decomposable into smaller segments, which are lock-free and do not have a wait/notify seed edge, a fork join seed edge or a property seed edge with endpoints along the segments,

wherein the UCG is configured to capture, as happens-before constraints, a set of all interleavings that are possible under scheduling constraints imposed by synchronization primitives that lead to violations of the property, and

wherein the Universal Causality Graph incorporates happens-before constraints arising from the concurrent program and a correctness property.

10. The system as recited in claim 9 , wherein the decomposable segments increase scalability of the predictive analysis.

11. The system as recited in claim 9 , wherein the UCG handles all standard synchronization primitives.