Methods and systems for reducing verification conditions for concurrent programs using mutually atomic transactions

Abstract

Methods and systems for generating verification conditions and verifying the correctness of a concurrent system of program threads are described. The methods and systems determine and employ mutually atomic transactions to reduce verification problem sizes and state space for concurrent systems. The embodiments provide both an adequate and an optimal set of token-passing constraints for a bounded unrolling of threads.

What is claimed is: 
     
       1. A computer-implemented method for verifying the correctness of a concurrent system of program threads comprising:
 identifying, for each pair of the program threads, a set of pair-wise, conflicting program thread locations at which access of shared memory resources by the corresponding pair of program threads is conflicting; 
 determining, for each pair of the program threads, a set of mutually atomic transactions (MATs), wherein, between threads in said pair, only the last thread program locations in said transactions are conflicting; 
 constructing, with respect to each pair of program threads, token passing constraints between conflicting program thread locations and initial thread locations in corresponding MATs to permit context switching between threads in a respective pair of program threads; 
 adding, for each pair of program threads, additional token passing constraints between conflicting program thread locations and chosen program thread locations which lie within corresponding MATs, wherein said chosen program thread locations are conflicting with thread locations of one or more threads other than threads in said pair, and for which token passing constraints are generated at the constructing step to permit additional context switching between the threads in the respective pair of program threads; and 
 verifying the correctness of the concurrent system of program threads by employing verification conditions that are generated based on the constructed token passing constraints. 
 
     
     
       2. The computer-implemented method of  claim 1 , wherein the token passing constraints are the only token passing constraints employed to verify the concurrent system if the system is a two-threaded system. 
     
     
       3. The computer-implemented method of  claim 1 , wherein the token passing constraints are the only token passing constraints employed to verify the concurrent system if the system has more than two threads. 
     
     
       4. The computer-implemented method of  claim 1 , further comprising:
 deriving happens-before relations for program thread locations from fork-join constraints. 
 
     
     
       5. The computer-implemented method of  claim 4 , further comprising:
 identifying pair-wise, conflicting thread locations that are simultaneously unreachable by employing the happens-before relations to reduce the sizes of sets of pair-wise, conflicting thread locations. 
 
     
     
       6. The computer-implemented method of  claim 1 , further comprising:
 generating linear constraints on clock vector variables to bound context-switches between threads. 
 
     
     
       7. The computer-implemented method of  claim 1 , wherein the pair-wise, conflicting program thread locations and the token passing constraints are incrementally identified and constructed, respectively, with increasing depth bound. 
     
     
       8. A non-transitory computer readable storage medium comprising a computer readable program embodying a program of instructions for generating verification conditions for a concurrent system of program threads, the instructions executable by a computer, wherein the computer readable program when executed on a computer causes the computer to:
 identify, for each pair of the program threads, a set of pair-wise, conflicting program thread locations at which access of shared memory resources by the corresponding pair of program threads is conflicting; 
 determine, for each pair of the program threads, a set of mutually atomic transactions (MATs), wherein, between threads in said pair, only the last thread program locations in said transactions are conflicting; 
 construct, with respect to each pair of program threads, token passing constraints between conflicting program thread locations and initial thread locations in corresponding MATs to permit context switching between threads in a respective pair of program threads; 
 add, for each pair of program threads, additional token passing constraints between conflicting program thread locations and chosen program thread locations which lie within corresponding MATs, wherein said chosen program thread locations are conflicting with thread locations of one or more threads other than threads in said pair, and for which token passing constraints are generated at the construct step to permit additional context switching between the threads in the respective pair of program threads; and 
 generate verification conditions based on the token passing constraints for the concurrent system. 
 
     
     
       9. A verification system for generating verification conditions to permit verification of a concurrent system of program threads, said verification system being implemented on a processor and a program storage device and said verification system comprising:
 a conflicts identifier module configured to identify, for each pair of the program threads, a set of pair-wise, conflicting program thread locations at which access of shared memory resources by the corresponding pair of program threads is conflicting; 
 a mutually atomic transactions (MAT) analyzer configured to determine a set of MATs for each pair of program threads; and 
 a token passing constraint generator configured to construct, with respect to each pair of program threads, first token passing constraints between conflicting program thread locations and initial thread locations in corresponding MATs to permit context switching between threads in a respective pair of program threads, wherein said token passing constraint generator is further configured to generate verification conditions for the concurrent system, and 
 wherein the token passing constraint generator is further configured to add, for each pair of program threads, additional token passing constraints between conflicting program thread locations and chosen program thread locations which lie within corresponding MATs, wherein said chosen program thread locations are conflicting with thread locations of one or more threads other than threads in said pair, and for which the first token passing constraints were constructed to permit additional context switching between the threads in the respective pair of program threads. 
 
     
     
       10. The verification system of  claim 9 , further comprising:
 a solver configured to verify the correctness of the concurrent system of program threads by employing verification conditions that are generated based on the constructed token passing constraints. 
 
     
     
       11. The verification system of  claim 9 , wherein the token passing constraints are the only token passing constraints generated by the verification system if the concurrent system is a two-threaded system. 
     
     
       12. The verification system of  claim 9 , wherein the token passing constraints are the only token passing constraints generated by the verification system if the concurrent system has more than two threads. 
     
     
       13. The verification system of  claim 9 , wherein the conflicts identifier module is further configured to derive happens-before relations for program thread locations from fork-join constraints. 
     
     
       14. The verification system of  claim 13 , wherein the conflicts identifier module is further configured to identify pair-wise, conflicting thread locations that are simultaneously unreachable by employing the happens-before relations to reduce the sizes of sets of pair-wise, conflicting thread locations. 
     
     
       15. The verification system of  claim 9 , further comprising:
 a context-switch bounding module configured to generate linear constraints on clock vector variables to bound context-switches between threads. 
 
     
     
       16. The verification system of  claim 9 , wherein the conflicts identifier module is further configured to incrementally identify the pair-wise, conflicting program thread locations with increasing depth bound. 
     
     
       17. The verification system of  claim 9 , wherein the token passing constraints generator is further configured to incrementally construct the token passing constraints with increasing depth bound.