Store Atomicity: Giving Meaning to Loads and Stores in Shared Memory Systems

Arvind & Jan-Willem Maessen (SUN)

Abstract

We suggest that popular memory models, such as SC, Sun's TSO and RMO, and PowerPC's WO, should be thought of in terms of two orthogonal components: Purely local reordering of instructions plus Store Atomicity. We capture local ordering in an execution graph. Store Atomicity imposes additional dependency edges between memory operations to a given location in different threads (for example, every load depends upon the store which provides its value). This separation resolves the mystery of why cache consistency protocols for most memory models are so similar: all they do is enforce Store Atomicity.

Unlike SC, for weak memory models no adequate procedures exist for enumerating the legal behaviors of programs. This invariably leads to misunderstandings about which behaviors are permitted by the specification. We give a procedure for generating all legal behaviors of a program under a weak memory model similar to RMO or WO.

The rules for Store Atomicity attempt to impose minimal constraints among operations on different processors. Actual implementations employ simple mechanisms, but are significantly more conservative than required. This research will provide a definitional framework which will permit us and others to exploit the gap between current implementations and the less restrictive requirements of store atomicity.

Approach

1.  We define store atomicity as a property of execution graphs. Store Atomicity is not derived directly from any particular memory model. It relies on three kinds of dependencies:

A. Ordering dependencies imposed by the thread-local reordering semantics.

B. A dependency to each Load from the Store which provides its value.

C.  Additional dependencies between threads required to guarantee Store Atomicity.  Though the rules for drawing these edges are the  same in all memory models, the actual edges drawn depend on (A) and (B).

2. We know of no adequate procedure for enumerating behaviors of a program under a weak memory model (including the new JMM). Consider the following strawman for enumerating behaviors:

a) Execute program under SC, ignoring all fences.

b) Reorder instructions statically as permitted by the memory model.

c) Repeat from (a) as often as necessary.

This will not generate all legal behaviors because address aliasing and control dependencies are revealed dynamically as a program executes. Address and control speculation further complicate matters.

Instead we provide an algorithm for generating the execution graph of a multithreaded shared memory program where the execution dynamically renames registers, and data dependence and control edges are drawn after each operation. Our procedure also permits speculation where the generated graph may have to be rejected later when an inconsistency is revealed. Each execution graph corresponds to a legal execution of the program.

We believe we have presented the first adequate procedure for enumeration.

Research Support

Partial funding for this work has been provided by the IBM agreement number W0133890 as a part of DARPA's PERCS Projects.