Patent ID: 8448145
Filing Date: 2013-05-21
Classification: G06F

Abstract:
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.