Systems and methods for concurrency analysis

1. A method having a processor to check properties of bounded concurrent programs, comprising:

encoding concurrent control flow graph (CFG) and property for programming threads as a first-order formula F 1 ;

initializing an interference abstraction (IA) by de-coupling one or more reads from the writes that may interfere with the read from a set of rules including: not coupling a read with any write; forcing a read to be coupled with a limited number of writes; coupling a read with a write but ignore data flow and ordering constraints; or allowing an interfering write to execute between a coupled read and write, wherein the IA corresponds to a violation of one or more of the rules and obtained by instantiating sequential consistency (SC) axioms;

encoding the IA as a first-order formula F 2 ;

checking a conjunction of F 1 and F 2 (F 1 ^F 2 );

if the conjunction is satisfiable, checking if an interference relation (IR) is spurious, and iteratively refining the IA; and

if the conjunction is unsatisfiable, checking if the proof is spurious, and iteratively refining the IA.

2. The method of claim 1 , wherein the property comprises one or more bugs.

3. The method of claim 1 , comprising obtaining IAs syntactically from axioms of sequential consistency by reducing the moves of the existential and universal players.

4. The method of claim 3 , comprising performing biased initialization of the IA.

5. The method of claim 1 , comprising checking the property using IA with iterative refinement.

6. The method of claim 1 , comprising checking if (F 1 ^F 2 ) is satisfiable or has a proof.

7. The method of claim 1 , comprising checking if the satisfying interference relation (IR) is spurious.

8. The method of claim 1 , comprising checking a spurious IR by layered instantiation of SC axioms.

9. The method of claim 1 , comprising checking if an infeasibility proof is spurious.

10. The method of claim 1 , comprising performing interference pruning for focusing of iterative refinement.

11. The method of claim 1 , comprising using lock lemmas for focusing of iterative refinement.

12. The method of claim 1 , comprising:

picking an initial abstract game configuration C=(R 0 , W 0 , F 0 , PO 0 );

solving for a winning strategy for both players E and A in G=(Π, C);

checking if σ is winning for E in an original game Ĝ and if so output σ and terminate and otherwise, augment the moves of A in C; and

checking if σ is winning for A in the original game Ĝ and if so output σ and terminate and otherwise, augment the moves of E in C.

13. A system having a processor to check properties of bounded concurrent programs, comprising:

means for encoding concurrent control flow graph (CFG) and property for programming threads as a first-order formula F 1 ;

means for initializing an interference abstraction (IA) by de-coupling one or more reads from the writes that may interfere with the read from a set of rules including: not coupling a read with any write; forcing a read to be coupled with a limited number of writes; coupling a read with a write but ignore data flow and ordering constraints; or allowing an interfering write to execute between a coupled read and write, wherein the IA corresponds to a violation of one or more of the rules and obtained by instantiating sequential consistency (SC) axioms;

means for encoding the IA as a first-order formula F 2 ;

means for checking a conjunction of F 1 and F 2 (F 1 ^F 2 );

means for checking if an interference relation (IR) is spurious, and iteratively refining the IA if the conjunction is satisfiable; and

means for checking if the proof is spurious, and iteratively refining the IA if the conjunction is unsatisfiable.

14. The system of claim 13 , wherein the property comprises one or more bugs.

15. The system of claim 13 , comprising means for obtaining IAs syntactically from axioms of sequential consistency by reducing the moves of the existential and universal players.

16. The system of claim 15 , comprising means for performing biased initialization of the IA.

17. The system of claim 13 , comprising means for checking the property using IA with iterative refinement.

18. The system of claim 13 , comprising means for checking if (F 1 ^F 2 ) is satisfiable or has a proof.

19. The system of claim 13 , comprising means for checking if the satisfying interference relation (IR) is spurious.

20. The system of claim 13 , comprising means for checking a spurious IR by layered instantiation of SC axioms; means for checking if an infeasibility proof is spurious; means for performing interference pruning for focusing of iterative refinement and means for using lock lemmas for focusing of iterative refinement.