Memory Model = Instruction Reordering + Store Atomicity

May 15, 2006
Arvind | MIT, Computer Science and Artificial Intelligence Laboratory

We 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

Speaker Details

Arvind is the Johnson Professor of Computer Science and Engineering at MIT where in collaboration with Motorola his group built the Monsoon dataflow machines and its associated software in the late eighties. In 2000, Arvind started Sandburst which got sold to Broadcom in 2006. In 2003, Arvind co-founded Bluespec Inc., an EDA company to produce a set of tools for high-level synthesis. In 2001, Dr. R. S. Nikhil and Arvind published the book “Implicit parallel programming in pH”. Arvind’s current research interests are synthesis and verification of large digital systems described using Guarded Atomic Actions; and Memory Models for parallel architectures and languages.