Memory Model = Instruction Reordering + Store Atomicity
7We present a novel framework for defining memory models in terms of two properties: thread-local Instruction Reordering axioms and Store Atomicity (SA), which describes inter-thread communication via memory. SA guarantees serializability, that is, a unique global interleaving of all operations which respects the reordering rules. It is the SA property that is enforced by cache coherence protocols. Our framework uses partially ordered execution graphs; one graph represents many instruction interleavings with identical behaviors. The major contribution of this framework is a procedure for enumerating all legal program behaviors in any memory model with Store Atomicity. We will show that address aliasing speculation introduces new program behaviors and argue that these new behaviors should be permitted by the memory model specification. We will briefly discuss non-atomic memory models and the relationship of this work with the new Java Memory Model and the semantics of Transactional memory. This is joint work with Jan Willem Maessen of SUN Microsystems and will be presented at ISCA 2006 http://csg.lcs.mit.edu/pubs/memos/Memo-493/memo-493.pdf http://csg.csail.mit.edu/pubs/publications.html