Patent ID: 8595708
Filing Date: 2013-11-26
Classification: G06F

Abstract:
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 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 checking a conjunction of F 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.