A system and method for verifying a memory consistency model for a shared memory
multiprocessor computer systems generates random instructions to run on the processors,
saves the results of the running of the instructions, and analyzes the results
to detect a memory subsystem error if the results fall outside of the space of
possible outcomes consistent with the memory consistency model. A precedence relationship
of the results is determined by uniquely identifying results of a store location
with each result distinct to allow association of a read result value to the instruction
that created the read result value. A precedence graph with static, direct and
derived edges identifies errors when a cycle is detected that indicates results
that are inconsistent with memory consistency model rules.
