Access graphs: a model for investigating memory consistency

Computer architectures supporting shared memory continue to increase in complexity as designers seek to improve memory performance. This is especially true of proposals for massively parallel systems with distributed, yet shared, memory. The need to maintain a reasonably simple memory model for programmers, in spite of enhancements like caches and access pipelining, is responsible for many of the complications. We develop a novel graph model, access graphs, for visualizing processor/memory interaction. Access graphs symbolically represent the causal relationships between load, store, and synchronization events. The focus is on two classes of access graphs: pseudo and real. A pseudo access graph describes an execution in terms of abstract events familiar to the programmer. If the pseudo access graph is acyclic, then memory consistency is preserved during the execution. A real access graph describes an execution in terms of physical events known to the hardware designer. A real access graph must be acyclic since hardware cannot violate causality. Memory consistency can be verified for a given computer system by proving that for any acyclic real access graph describing a program´s execution on that computer, an acyclic pseudo access graph can be derived describing the same execution