SYSTEM AND METHOD FOR DEBUGGING MEMORY CONSISTENCY MODELS

摘要

A system and method for analyzing a test program (P) with respect to a memory model (M) includes preprocessing a test program into an intermediate form and translating (204) the intermediate form of the test program into a relational logic representation. The relational logic representation is combined (206) with a memory model to produce a legality formula. A set of bounds are computed (208) on a space to be searched for the memory model or on a core of the legality formula. A relational satisfiability problem is solved (212), which is defined by the legality formula and the set of bounds to determine a legal trace of the test program or debug the memory model.