A graph model for investigating memory consistency

The complexity of a multiprocessor memory system grows with the endeavors people make to improve the performance. The pseudo and real execution graphs introduced here can formally describe the complex event ordering behavior of the multiprocessor memory system and to verify the correctness of a parallel program under a consistency model. A pseudo execution graph represents the programmer´s abstraction of an execution in which memory accesses are simple, atomic operations. A loop in the pseudo execution graph indicates an incorrect execution. A real execution graph represents the hardware designer´s abstraction of an execution in which each memory access is a causal sequence of events. A loop in the real execution graph indicates that this execution is impossible to occur. A program is correct if all loops in the pseudo execution graphs cause loops in the corresponding real execution graphs