SYSTEM AND METHOD FOR DEBUGGING MEMORY CONSISTENCY MODELS

摘要

A system and method for analyzing a test program with respect to a memory model includes preprocessing a test program into an intermediate form and translating the intermediate form of the test program into a relational logic representation. The relational logic representation is combined with a memory model to produce a legality formula. A set of bounds are computed on a space to be searched for the memory model or on a core of the legality formula. A relational satisfiability problem is solved, 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.