A Unified Formalization of Four Shared-Memory Models.
The authors present a data-race-free-1, shared-memory model that unifies four earliermodels: weak ordering, release consistency (with sequentially consistent specialoperations), the VAX memory model, and data-race-free-0. Data-race-free-1 unifies themodels of weak ordering, release consistency, the VAX, and data-race-free-0 byformalizing the intuition that if programs synchronize explicitly and correctly, thensequential consistency can be guaranteed with high performance in a manner that retainsthe advantages of each of the four models. Data-race-free-1 expresses the programmer'sinterface more explicitly and formally than weak ordering and the VAX, and allows animplementation not allowed by weak ordering, release consistency, or data-race-free-0.The implementation proposal for data-race-free-1 differs from earlier implementations bypermitting the execution of all synchronization operations of a processor even whileprevious data operations of the processor are in progress. To ensure sequentialconsistency, two sychronizing processors exchange information to delay later operationsof the second processor that conflict with an incomplete data operation of the firstprocessor.
Introduction
A memory model for a shared-memory multiprocessor system is a formal specification of how memory
operations in a program will appear to execute to the programmer. In particular, a memory model specifies the
values that may be returned by read operations executed on a shared-memory system. This paper presents a new
memory model, data-race-free-1, that unifies four earlier models. 1 Although the four models are very similar, each
model has different advantages and disadvantages for programmers and system designers.
unifies the four models by retaining all the advantages of the four models.
Most uniprocessors provide a simple memory model that ensures that memory operations will appear to
execute one at a time, in the order specified by the program (program order). Thus, a read returns the value from
the last write (in program order) to the same location. To improve performance, however, uniprocessors often
allow memory operations to overlap other memory operations and to be issued and executed out of program order.
Uniprocessors use interlock logic to maintain the programmer's model of memory (that memory operations
appear to execute one at a time, in program order). This model of uniprocessor memory, therefore, has the
advantage of simplicity and yet allows for high performance optimizations.
The most commonly (and often implicitly) assumed memory model for shared-memory multiprocessor systems
is sequential consistency, formalized by Lamport [21] as follows.
Definition 1.1: [A multiprocessor system is sequentially consistent if and only if] the result of any
execution is the same as if the operations of all the processors were executed in some sequential
order, and the operations of each individual processor appear in this sequence in the order specified
by its program.
In other words, a sequentially consistent multiprocessor appears like a multiprogrammed uniprocessor [24].
Although sequential consistency retains the simplicity of the uniprocessor memory model, it limits performance
by preventing the use of several optimizations. Figure 1 shows that in multiprocessor systems, both with
and without caches, common uniprocessor hardware optimizations, such as write buffers, overlapped memory
operations, out-of-order memory operations, and lockup-free caches [20], can violate sequential consistency.
These optimizations significantly improve performance and will become increasingly important in the future as
processor cycle times decrease and memory latencies increase [13]. Gharachorloo et al. have described
1. An earlier version of this work appears in the Proceedings of the 17th Annual International Symposium on Computer
Architecture, June 1990 [1]. The data-race-free-1 memory model developed in this paper extends the data-race-free-0
model of [1] by distinguishing unpaired synchronization operations from paired release and acquire synchronization opera-
tions. The definition of data-race-free-1 in Section 2 uses the notions of how different operations are distinguished, when
the distinction is correct, the synchronization-order-1 and happens-before-1 relations, and data races. These notions are extensions
of similar concepts developed for data-race-free-0. Also, in parallel with our work on this paper, we published a
technique for detecting data races on a data-race-free-1 system [2]. Consequently, [2] reviews data races and the data-race-
memory model, and contains the definitions (in slightly different form) of Section 2. This material is used in Section
2 with the permission of the ACM.
mechanisms that allow these optimizations to be used with the sequential consistency model, but the mechanisms
require hardware support for prefetching and rollback [12].
Initially

Figure

1. A violation of sequential consistency. 2
and Y are shared variables and r1 and r2 are local registers. The execution depicted above violates sequential
consistency since no total order of memory operations consistent with program order lets both P 1 and P 2 return 0
for their reads on Y and X. Note that neither processor has data dependencies among its instructions; therefore,
simple interlock logic will not preclude either processor from issuing its second instruction before the first.
Shared-bus systems without caches - The execution is possible if processors issue memory operations out of order
or allow reads to pass writes in write buffers.
Systems with general interconnection networks without caches - The execution is possible even if processors
issue memory operations in program order, if the operations reach memory modules in a different order [21].
Shared-bus systems with caches - Even with a cache coherence protocol [6], the execution is possible if processors
issue memory operations out-of-order or allow reads to pass writes in write buffers.
Systems with general interconnection networks and caches - The execution is possible even if memory operations
are issued and reach memory modules in program order, if they do not complete in program order. Such a situation
can arise if both processors initially have X and Y in their caches, and a processor issues its read before its
write propagates to the cache of the other processor.
Alternate memory models have been proposed to improve the performance of shared-memory systems. To
be useful, the new models should satisfy the following properties: (1) the model should be simple for programmers
to use, and (2) the model should allow high performance. The central assumption of this work is that most
programmers prefer to reason with the sequential consistency model since it is a natural extension of the well-understood
uniprocessor model. Therefore, one way in which a memory model can satisfy the first property is to
appear sequentially consistent to most programs and to formally characterize this group of programs. A memory
model can satisfy the second property by allowing all high performance optimizations that guarantee sequential
consistency for this group of programs.
One group of programs for which it is possible to guarantee sequential consistency and still use many
optimizations is programs that explicitly distinguish between synchronization memory operations (operations used
to order other operations) and data memory operations (operations used to read and write data). This dichotomy
2.

Figure

1 is a modified version of Figure 1 in [1] and is presented with the permission of the IEEE.
between memory operations is the motivation behind the four models of weak ordering [9], release consistency
with sequentially consistent special operations (henceforth called release consistency) [11], the VAX [8], and
data-race-free-0 (originally called ordering with respect to data-race-free-0) [1].
Although the four memory models are very similar, small differences in their formalization lead to differences
in the way they satisfy the above two properties. Weak ordering [9] and release consistency [11] restrict
hardware to actually execute specific memory operations in program order. For programmers, the authors of
ordering later stated that mutual exclusion should be ensured for each access to a shared variable by using
constructs such as critical sections, which are implemented with hardware-recognizable synchronization operations
[10, 26]. The authors of release consistency formalize a group of programs called properly labeled pro-
grams, for which release consistency ensures sequential consistency. A properly labeled program distinguishes its
memory operations depending on their use. For example, it distinguishes synchronization operations from ordinary
data operations. The VAX and data-race-free-0 models differ from weak ordering and release consistency
by avoiding explicit restrictions on the actual order of execution of specific memory operations. In the VAX
architecture handbook [8], the data sharing and synchronization section states the following. "Accesses to explicitly
shared data that may be written must be synchronized. Before accessing shared writable data, the programmer
must acquire control of the data structure. Seven instructions are provided to permit interlocked access to a
control variable." Data-race-free-0 [1] states that sequential consistency will be provided to data-race-free pro-
grams. A data-race-free program (discussed formally in Sections 2 and distinguishes between synchronization
operations and data operations and ensures that conflicting data operations do not race (i.e., cannot execute con-
currently). For programs that contain data races, data-race-free-0 does not guarantee the behavior of the
hardware.
The different formalizations of the four models result in some models satisfying the simplicity or the high-performance
property better than other models; however, no model satisfies both properties better than all other
models. For example, the VAX imposes the least restrictions on hardware, but its specification is less explicit and
formal than the other models. Consider the statement, "before accessing shared writable data, the programmer
must acquire control of the data structure." Does this allow concurrent readers? Further, how will hardware
behave if programs satisfy the specified conditions? Although it may be possible to answer these questions from
the VAX handbook, a more explicit and formal interface would allow a straightforward and unambiguous resolution
of such questions. Release consistency, on the other hand, provides a formal and explicit interface. However,
as Section 4 will show, the hardware requirements of release consistency are more restrictive than necessary.
This paper defines a new model, data-race-free-1, which unifies the weak ordering, release consistency,
VAX, and data-race-free-0 models in a manner that retains the advantages of each of the models for both the
programmer and the hardware designer. The following summarizes how data-race-free-1 unifies the four models
and how it overcomes specific disadvantages of specific models.
For a programmer, data-race-free-1 unifies the four models by explicitly addressing two questions: (a)
when is a program correctly synchronized? and (b) how does hardware behave for correctly synchronized pro-
answers these questions formally, but the intuition behind the answers is simple: (a) a
program is correctly synchronized if none of its sequentially consistent executions have a data race (i.e.,
conflicting data operations do not execute concurrently), and (b) for programs that are correctly synchronized, the
hardware behaves as if it were sequentially consistent. This viewpoint is practically the same as that provided by
release consistency and data-race-free-0. However, it is more explicit and formal than weak ordering and the
VAX (e.g., it allows concurrent readers because they do not form a data race).
For a hardware designer, data-race-free-1 unifies the four models because (as will be shown in Section
implementing any of the models is sufficient to implement data-race-free-1. Furthermore, data-race-free-1 is less
restrictive than either weak ordering, release consistency, or data-race-free-0 for hardware designers since there
exists an implementation of data-race-free-1 that is not allowed by weak ordering, release consistency, or data-
race-free-0. The new implementation (described in Section 4) differs from implementations of weak ordering and
release consistency by allowing synchronization operations to execute even while previous data operations of the
synchronizing processors are incomplete. To achieve sequential consistency, processors exchange information at
the time of synchronization that ensures that a later operation that may conflict with an incomplete data operation
is delayed until the data operation completes. The new implementation differs from implementations of data-
race-free-0 by distinguishing between different types of synchronization operations.
The rest of the paper is organized as follows. Section 2 defines data-race-free-1. Sections 3 and 4 compare
data-race-free-1 with the weak ordering, release consistency, VAX, and data-race-free-0 models from the
viewpoint of a programmer and hardware designer respectively. Section 5 relates data-race-free-1 to other
models. Section 6 concludes the paper.
2. The Data-Race-Free-1 Memory Model
Section 2.1 first clarifies common terminology that will be used throughout the paper and then informally
motivates the data-race-free-1 memory model. Section 2.2 gives the formal definition of data-race-free-1. Data-
race-free-1 is an extension of our earlier model data-race-free-0 [1].
2.1. Terminology and Motivation for
The rest of the paper assumes the following terminology. The terms system, program, and operations (as in
definition 1.1 of sequential consistency) can be used at several levels. This paper discusses memory models at the
lowest level, where the system is the machine hardware, a program is a set of machine-level instructions, and an
operation is a memory operation that either reads a memory location (a read operation) or modifies a memory
location (a write operation) as part of the machine instructions of the program. The program order for an execution
is a partial order on the memory operations of the execution imposed by the program text [27]. The result of
an execution refers to the values returned by the read operations in the execution. A sequentially consistent execution
is an execution that could occur on sequentially consistent hardware. Two memory operations conflict if at
least one of them is a write and they access the same location [27].
The motivation for data-race-free-1, which is similar to that for weak ordering, release consistency, the
VAX model and data-race-free-0, is based on the following observations made in [1]. 3 Assuming processors
maintain uniprocessor data and control dependencies, sequential consistency can be violated only when two or
more processors interact through memory operations on common locations. These interactions can be classified
as data memory operations and synchronization memory operations. Data operations are usually more frequent
and involve reading and writing of data. Synchronization operations are usually less frequent and are used to
order conflicting data operations from different processors. For example, in the implementation of a critical section
using semaphores, the test of the semaphore and the unset or clear of the semaphore are synchronization
operations, while the reads and writes in the critical section are data operations.
Additionally, synchronization operations can be characterized as paired acquire and release synchronization
operations or as unpaired synchronization operations as follows. (The characterization is similar to that used for
properly labeled programs for release consistency [11]; Section 3 discusses the differences.) In an execution, consider
a write and a read synchronization operation to the same location, where the read returns the value of the
write, and the value is used by the reading processor to conclude the completion of all memory operations of the
writing processor that were before the write in the program. In such an interaction, the write synchronization
operation is called a release, the read synchronization operation is called an acquire, and the release and acquire
are said to be paired with each other. A synchronization operation is unpaired if it is not paired with any other
synchronization operation in the execution. For example, consider an implementation of a critical section using
semaphores, where the semaphore is tested with a test&set instruction and is cleared with an unset instruction.
The write due to an unset is paired with the test that returns the unset value; the unset write is a release operation
3. The observations are paraphrased from [1] with the permission of the IEEE.
and the test read is an acquire operation because the unset value returned by the test is used to conclude the completion
of the memory operations of the previous invocation of the critical section. The write due to a set of a
test&set and a read due to the test of a test&set that returns the set value are unpaired operations; such a read is
not an acquire and the write is not a release because the set value does not communicate the completion of any
previous memory operations.
As will be illustrated by Section 4, it is possible to ensure sequential consistency by placing most hardware
restrictions only on the synchronization operations. Further, of the synchronization operations, the paired operations
require more restrictions. Thus, if hardware could distinguish the type of an operation, it could complete
data operations faster than all the other operations, and unpaired synchronization operations faster than the paired
synchronization operations, without violating sequential consistency. A data-race-free-1 system gives programmers
the option of distinguishing the above types of operations to enable higher performance.
2.2. Definition of Data-Race-Free-1
Section 2.1 informally characterized memory operations based on the function they perform, and indicated
that by distinguishing memory operations based on this characterization, higher performance can be obtained
without violating sequential consistency. This section first discusses how the memory operations can be distinguished
based on their characterization on a data-race-free-1 system, and then gives the formal criterion for
when the operations are distinguished correctly for data-race-free-1. The section concludes with the definition of
the data-race-free-1 memory model.
does not impose any restrictions on how different memory operations may be dis-
tinguished. One option for distinguishing data operations from synchronization operations is for hardware to provide
different instructions that may be used for each type of operation. For example, only special instructions
such as Test&Set and Unset may be used to generate synchronization operations. Alternatively, only operations
to certain memory-mapped locations may be distinguished as synchronization operations. One way of distinguishing
between paired and unpaired synchronization operations is for hardware to provide special instructions
for synchronization operations and a static pairable relation on those instructions; a write and a read in an execution
are distinguished by the hardware as paired release and acquire if they are generated by instructions related
by the pairable relation, and if the read returns the value of the write. Figure 2 gives examples of different instructions
and the pairable relation, and illustrates their use.
The following discusses when a programmer distinguishes operations correctly for data-race-free-1. If the
operations are distinguished exactly according to their function outlined in Section 2.1, then the distinction is
indeed correct. However, data-race-free-1 does not require a programmer to distinguish operations to match their
SyncRead,flag
(a)
Test&Set,s
(b)
Fetch&Inc,count
Fetch&Inc,count
SyncWrite,flag
Fetch of
Inc of
SyncWrite
Unset,s
Test&Set,s
Unset,s
Test of
Test&Set
Set of
Test&Set
Unset -
while (Test&Set,s) {;}
Unset,s
data ops in critical section
data ops before barrier
/* code for barrier */
if (Fetch&Inc,count == N) {
data ops after barrier
Test&Set,s
/* code for critical setion */
Sync-
Read
acquire
acquire
release
release
SyncRead,flag
local_flag
while(SyncRead,flag != local_flag) {;}
else

Figure

2. Synchronization instructions and the pairable relation for different systems.
Figures 2a and 2b represent two systems with different sets of instructions that can be used for synchronization
operations. For each system, the figure shows the different synchronization operations and the pairable relation,
along with programs and executions that use these operations. The table in each figure lists the read synchronization
operations (potential acquires) horizontally, and the write synchronization operations (potential releases) verti-
cally. A '-' indicates that the synchronization operations of the corresponding row and column are pairable; they
will be paired in an execution if the read returns the value written by the write in that execution. The executions
occur on sequentially consistent hardware and their operations execute in the order shown. op,x denotes an operation
op on location x. DataRead and DataWrite denote data operations. The Test&Set and Fetch&Inc [17] instructions
are defined to be atomic instructions. Their read and write operations are represented together as Test&Set,x
or Fetch&Inc,x. Paired operations are connected with arrows.
Figure 2a shows a system with the Test&Set and Unset instructions, which are useful to implement a critical sec-
tion. A Test&Set atomically reads a memory location and updates it to the value 1. An Unset updates a memory
location to the value 0. A write due to an Unset and a read due to a Test&Set are pairable. The figure shows code
for a critical section and its execution involving two processors.
Figure 2b shows a system with the Fetch&Inc [17], SyncWrite and SyncRead instructions, which are useful to implement
a barrier. Fetch&Inc atomically reads and increments a memory location, SyncWrite is a synchronization
write that updates a memory location to the specified value, and SyncRead is a synchronization read of a memory
location. A write due to a Fetch&Inc is pairable with a read due to another Fetch&Inc and a write due to a
SyncWrite is pairable with a read due to a SyncRead. Also shown is code where N processors synchronize on a
barrier [23], and its execution for 2. The variable local_flag is implemented in a local register of the processor
and operations on it are not shown in the execution.
function exactly. In the absence of precise knowledge regarding the function of an operation, a programmer can
conservatively distinguish an operation as a synchronization operation even if the operation actually performs the
function of a data operation. Sequential consistency will still be guaranteed although the full performance potential
of the system may not be exploited. Henceforth, the characterization of an operation will be the one distinguished
by the programmer (which may be different from that based on the actual function the operation per-
forms). For example, an operation that is actually a data operation, but for which the programmer uses a synchronization
instruction, will be referred to as a synchronization operation.
Intuitively, operations are distinguished correctly for data-race-free-1 if sufficient synchronization operations
are distinguished as releases and acquires. The criteria for sufficiency is that if an operation is distinguished
as data, then it should not be involved in a race; i.e, the program should be data-race-free. The notion of a data
race is formalized by defining a happens-before-1 relation for every execution of a program as follows.
The happens-before-1 relation for an execution is a partial order on the memory operations of the execution.
Informally, happens-before-1 orders two operations initiated by different processors only if paired release and
acquire operations execute between them. Definition 2.2 formalizes this intuition by using the program order and
the synchronization-order-1 relations (Definition 2.1).
Definition 2.1: In an execution, memory operation S 1 is ordered before memory operation S 2 by the
relation if and only if S 1 is a release operation, S 2 is an acquire operation
are paired with each other.
Definition 2.2: The happens-before-1 relation for an execution is the irreflexive transitive closure of
the program order and synchronization-order-1 relations for the execution.
The definitions of a data race, a data-race-free program and the data-race-free-1 model follow.
Definition 2.3: A data race in an execution is a pair of conflicting operations, at least one of which is
data, that is not ordered by the happens-before-1 relation defined for the execution. An execution is
data-race-free if and only if it does not have any data races. A program is data-race-free if and only
if all its sequentially consistent executions are data-race-free.
Definition 2.4: Hardware obeys the data -race -free -1 memory model if and only if the result of
every execution of a data-race-free program on the hardware can be obtained by an execution of the
program on sequentially consistent hardware.
Figures 3a and 3b illustrate executions that respectively exhibit and do not exhibit data races. The execution
in Figure 3a is an implementation of the critical section code in Figure 2a, except that the programmer used a data
operation instead of the Unset synchronization operation for P 0 's write on s. Therefore, happens-before-1
does not order P 0 's write on x and P 1 's read on x. Since the write and read on x conflict and are both data opera-
tions, they form a data race. For similar reasons, P 0 's data write on s forms a data race with P 1 's test, set and
data write on s. Figure 3b shows an execution of the barrier code of Figure 2b. The execution is data-race-free
because happens-before-1 orders all conflicting pairs of operations, where at least one of the pair is data.
Note that the execution of Figure 3b does not use critical sections and therefore data-race-free-1 does not
require that all sharing be done through critical sections. Also note that in programs based on asynchronous algorithms
some operations access data, but are not ordered by synchronization. For such programs to be data-
race-free, these operations also need to be distinguished as synchronization operations.
SyncRead,flag
(a)
Test&Set,s
(b)
Fetch&Inc,count
Fetch&Inc,count
SyncWrite,flag
Test&Set,s
SyncRead,flag
po
po
po
po
po
po
po
po
po
so1
so1
po
po
po

Figure

3. Executions that (a) exhibit and (b) do not exhibit data races.
As discussed in Section 2.1, the definition of data-race-free-1 assumes a program that uses machine instructions
and hardware-defined synchronization primitives. However, programmers using high-level parallel programming
languages can use data-race-free-1 by extending the definition of data-race-free to high-level programs
(as discussed for data-race-free-0 in [1]). The extension is straightforward, but requires high-level parallel
languages to provide special constructs for synchronization, e.g., semaphores, monitors, fork-joins, and task ren-
dezvous. Data-race-free-1 does not place any restrictions on the high-level synchronization mechanisms. It is the
responsibility of the compiler to ensure that a program that is data-race-free at the high-level compiles into one
that is data-race-free at the machine-level, ensuring sequential consistency to the programmer.
3. vs. Weak Ordering, Release Consistency, the VAX Model, and Data-Race-Free-0 for
Programmers
This section compares the data-race-free-1 memory model to weak ordering, release consistency, the VAX,
and data-race-free-0 from a programmer's viewpoint. As stated earlier, the central assumption of this work is that
most programmers prefer to reason with sequential consistency. For such programmers, data-race-free-1 provides
a simple model: if the program is data-race-free, then hardware will appear sequentially consistent.
Both weak ordering and the VAX memory model state that programs have to obey certain conditions for
hardware to be well-behaved. However, sometimes further interpretation may be needed to deduce whether a program
obeys the required conditions (as in the concurrent readers case of Section 1), and how the hardware will
behave for programs that obey the required conditions. Data-race-free-1 expresses both these aspects more explicitly
and formally than weak ordering and the VAX: data-race-free-1 states that a program should be data-race-
free, and hardware appears sequentially consistent to programs that are data-race-free.
and release consistency provide a formal interface for programmers. Data-race-free-1 provides
a similar interface with a few minor differences. The programs for which data-race-free-0 ensures sequential
consistency are also called data-race-free programs [1]. The difference is that data-race-free-0 does not distinguish
between different synchronization operations; it effectively pairs all conflicting synchronization operations
depending on the order in which they execute. This distinction does not significantly affect programmers, but can
be exploited by hardware designers.
The programs for which release consistency ensures sequential consistency are called properly labeled programs
[11]. All data-race-free programs are properly labeled, but there are some properly labeled programs that
are not data-race-free (as defined by Definition 2.4) [15]. The difference is minor and arises because properly
labeled programs have a less explicit notion of pairing. They allow conflicting data operations to be ordered by
operations (nsyncs) that correspond to the nonpairable synchronization operations of data-race-free-1. Although a
memory model that allows all hardware that guarantees sequential consistency to properly labeled programs has
not been formally described, such a model would be similar to data-race-free-1 because of the similarity between
data-race-free and properly labeled programs.
A potential disadvantage of data-race-free-1 relative to weak ordering and release consistency is for programmers
of asynchronous algorithms that do not rely on sequential consistency for correctness [7]. Weak ordering
and release consistency provide such programmers the option of reasoning with their explicit hardware conditions
and writing programs that are not data-race-free, but work correctly and possibly faster. Data-race-free-1 is
based on the assumption that programmers prefer to reason with sequential consistency. Therefore, it does not restrict
the behavior of hardware for a program that is not data-race-free. Nevertheless, for maximum performance,
programmers of asynchronous algorithms could deal directly with specific implementations of data-race-free-1.
This would entail some risk of portability across other data-race-free-1 implementations, but would enable future
faster implementations for the other, more common programs.
To summarize, for programmers, data-race-free-1 is similar to release consistency and data-race-free-0, but
provides a more explicit and formal interface than weak ordering and the VAX model. Previous work discusses
how the requirement of data-race-free programs for all the above models is not very restrictive for programmers
[1, 11], and how data races [2] or violations of sequential consistency due to data races [14] may be dynamically
detected with these models.
4. vs. Weak Ordering, Release Consistency, the VAX Model, and Data-Race-Free-0 for
Hardware Designers
This section compares data-race-free-1 to weak ordering, release consistency, the VAX model, and data-
race-free-0 from a hardware designer's viewpoint. It first shows that data-race-free-1 unifies the four models for a
hardware designer because any implementation of weak ordering, release consistency, the VAX model, or data-
race-free-0 obeys data-race-free-1 (Section 4.1). It then shows that data-race-free-1 is less restrictive than weak
release consistency, and data-race-free-0 for a hardware designer because data-race-free-1 allows an
implementation not allowed by weak ordering, release consistency, or data-race-free-0 (Section 4.2).
4.1. Unifies Weak Ordering, Release Consistency, the VAX Model, and Data-Race-
Free-0 for Hardware Designers
For a hardware designer, data-race-free-1 unifies release consistency, data-race-free-0, weak ordering, and
the VAX model because any implementation of any of the four models obeys data-race-free-1. Specifically,
all implementations of release consistency obey data-race-free-1 because, as discussed in Section 3, all
implementations of release consistency ensure sequential consistency to all data-race-free programs;
all implementations of data-race-free-0 obey data-race-free-1 because, again as discussed in Section 3, all
implementations of data-race-free-0 ensure sequential consistency to all data-race-free programs;
all implementations of weak ordering obey data-race-free-1 because our earlier work shows that all implementations
of weak ordering obey data-race-free-0 [1], and from the above argument, all implementations of
data-race-free-0 obey data-race-free-1;
# data-race-free-1 formalizes the VAX model; therefore, all implementations of the VAX model obey data-
race-free-1.
4.2. Data-Race-Free-1 is Less Restrictive than Weak Ordering, Release Consistency, or Data-Race-Free-0
for Hardware Designers
is less restrictive for a hardware designer to implement than either weak ordering, release
consistency, or data-race-free-0 because data-race-free-1 allows an implementation that is not allowed by weak
release consistency, or data-race-free-0. Figure 4 motivates such an implementation. The figure shows
part of an execution in which two processors execute the critical section code of Figure 2a. Processors P 0 and P 1
Test&Set s until they succeed, execute data operations (including one on location x), and finally Unset s. The critical
section code is data-race-free; therefore, its executions on a data-race-free-1 implementation should appear
sequentially consistent. In the execution of Figure 4, P 0 's Test&Set succeeds first. Therefore, P 1 's Test&Set
succeeds only when it returns the value written by P 0 's Unset. Thus, to appear sequentially consistent, P 1 's data
read of x should return the value written by P 0 's data write of x. Figure 4 shows how implementations of weak
release consistency, and data-race-free-1 can achieve this.
Unset,s
. Test&Set,s
WO stalls P0 until DataWrite completes
WO, RC stall P1 for Unset and (therefore for) DataWrite
DRF1 delays DataRead until DataWrite completes
Test&Set,s
RC delays Unset until DataWrite completes
DRF1 stalls P1 only for Unset
po
po
po
po
po
po
po
so1
need never stall P0 nor delay its operations
Test&Set,s
po
Unset,s
po
po
po
release consistency,

Figure

4. Implementations of memory models.
Both weak ordering and release consistency require P 0 to delay the execution of its Unset until P 0 's data
completes (i.e., is seen by all processors). However, this delay is not necessary to maintain sequential consistency
(as also observed by Zucker [28]), and it is not imposed by the implementation proposal for data-race-
described next. Instead, the implementation maintains sequential consistency by requiring that P 0 's data
write on x completes before P 1 executes its data read on x. It achieves this by ensuring that (i) when P 1 executes
its Test&Set, P 0 notifies P 1 about its incomplete write on x, and (ii) P 1 delays its read on x until P 0 's write on x
completes.
With the new optimization, P 0 can execute its Unset earlier and P 1 's Test&Set can succeed earlier than
with weak ordering or release consistency. Thus, P 1 's reads and writes following its Test&Set (by program order)
that do not conflict with previous operations of P 0 will also complete earlier. Operations such as the data read on
x that conflict with previous operations of P 0 may be delayed until P 0 's corresponding operation completes.
Nevertheless, such operations can also complete earlier than with weak ordering and release consistency. For
example, if P 1 's read on x occurs late enough in the program, P 0 's write may already be complete before P 1
examines the read; therefore, the read can proceed without any delay. Recently, an implementation of release
consistency has been proposed that uses a rollback mechanism to let a processor conditionally execute its reads
following its acquire (such as P 1 's Test&Set) before the acquire completes [12]; our optimization will benefit
such implementations also because it allows the writes following the acquire to be issued and completed earlier,
and lets the reads following the acquire to be committed earlier.
The data-race-free-1 implementation differs from data-race-free-0 implementations because data-race-free-
distinguishes between the Unset and Test&Set synchronization operations and can take different actions for
data-race-free-0 does not make such distinctions.
Section 4.2.1 describes a sufficient condition for implementing data-race-free-1 based on the above motiva-
tion. Section 4.2.2 gives a detailed implementation proposal based on these conditions.
4.2.1. Sufficient Conditions for
Hardware obeys the data-race-free-1 memory model if the result of any execution of a data-race-free program
on the hardware can be obtained by a sequentially consistent execution of the program. The result of an
execution is the set of values its read operations return (Section 2.1). The value returned by a read is the value
from the write (to the same location) that was seen last by the reading processor. Thus, the value returned by a
read depends on the order in which the reading processor sees its read with respect to writes to the same location;
i.e., the order in which a processor sees conflicting operations. Thus, hardware is data-race-free-1 if it obeys the
following conditions.
Conditions: Hardware is data-race-free-1 if for every execution, E, of a data-
race-free program on the hardware, (i) the operations of execution E are the same as those of some
sequentially consistent execution of the program, and (ii) the order in which two conflicting operations
are seen by a processor in execution E is the same as in that sequentially consistent execution.
processor sees a write when a read executed by the processor to the same location as the write will return the
value of that or a subsequent write. A processor sees a read when the read returns its value. These notions are
similar to those of "performed with respect to a processor" and "performed" [9].)
The following gives three requirements (data, synchronization, and control) that are together sufficient for
hardware to satisfy the data-race-free-1 conditions, and therefore to obey data-race-free-1.
The data requirement pertains to all pairs of conflicting operations of a data-race-free program, where at
least one of the operations is a data operation. In an execution on sequentially consistent hardware, such a pair of
operations is ordered by the happens-before-1 relation of the execution, and is seen by all processors in that
order. The data requirement for an execution on data-race-free-1 hardware is that all such pairs
of operations continue to be seen by all processors in the happens-before-1 order of the execution. This requirement
ensures that in Figure 4, P 1 sees P 0 's write of x before the read of x. Based on the discussion of Figure 4,
the data requirement conditions below meet the data requirement for a pair of conflicting operations from different
processors. For conflicting operations from the same processor, it is sufficient to maintain intra-processor data
dependencies. The conditions below assume these are maintained.
In the rest of this section, preceding and following refer to the ordering by program order. An operation,
either synchronization or data, completes (or performs [9]) when it is seen (as defined above) by all processors.
Data Requirement Conditions: Let Rel and Acq be release and acquire operations issued by processors
P rel and P acq respectively. Let Rel and Acq be paired with each other.
Pre-Release Condition - When P rel issues Rel, it remembers the operations preceding Rel that are
incomplete.
Release-Acquire Condition - (i) Before Acq completes, P rel transfers to P acq the addresses and identity
of all its remembered operations. (ii) Before Acq completes, Rel completes and all operations
transferred to P rel (on P rel 's acquires preceding Rel) complete.
Post-Acquire Condition - Let Acq precede Y (by program order) and let the operation X be transferred
to P acq on Acq. (i) Before Y is issued, Acq completes. (ii) If X and Y conflict, then before Y is issued,
completes.
The data requirement conditions can be proved correct by showing that they ensure that if X and Y are
conflicting operations from different processors and happens-before-1 orders X before Y, then X completes before
any processor sees Y. This implies that all processors see X before Y, meeting the data requirement. For the execution
in Figure 4, the pre-release condition ensures that when P 0 executes its Unset, it remembers that
is incomplete. The release-acquire condition ensures that when P 1 executes its successful Test&Set,
transfers the address of x to P 1 . The post-acquire condition ensures that P 1 detects that it has to delay
completes and enforces the delay. Thus, DataRead,x returns the value written by
Besides the data requirement, the data-race-free-1 conditions also require that the order in which two
conflicting synchronization operations are seen by a processor is as on sequentially consistent hardware. This is
the synchronization requirement. The data and synchronization requirements would suffice to satisfy the data-
conditions if they also guaranteed that for any execution, E, on hardware that obeyed these
requirements, there is some sequentially consistent execution with the same operations, the same happens-before-
1, and the same order of execution of conflicting synchronization operations as E. In the absence of control flow
operations (such as branches), the above is automatically ensured. In the presence of control flow operations, how-
ever, an extra requirement, called the control requirement, is needed to ensure the above [3].
Weak ordering, release consistency, and all proposed implementations of data-race-free-0 satisfy the synchronization
requirement explicitly and the control requirement implicitly (by requiring "uniprocessor control
dependencies" to be maintained). Since the key difference between implementations of the earlier models and
the new implementation of data-race-free-1 is in the data requirement, the following describes an implementation
proposal only for the data requirement conditions. In [3], we formalize the above three requirements and give
explicit conditions for the synchronization and control requirements. A conservative way to satisfy the synchronization
requirement is for a processor to also stall the issue of a synchronization operation until the completion of
preceding synchronization operations and the write operations whose values are returned by preceding synchronization
read operations. A conservative way to satisfy the control requirement is for a processor to also block on a
read that controls program flow until the read completes.
Note that further optimizations on the data requirement conditions and on the implementation of the following
section are possible [3]. For example, for the release-acquire condition, the acquire can complete even while
operations transferred to the releasing processor are incomplete, as long as the releasing processor transfers the
identity of those incomplete operations to the acquiring processor. For the post-acquire condition, it is not necessary
to delay an operation (Y) following an acquire until a conflicting operation (X) transferred to the acquiring
processor completes. Instead, it is sufficient to delay Y only until X is seen by the acquiring processor, as long as a
mechanism (such as a cache-coherence protocol) ensures that all writes to the same location are seen in the same
order by all processors. Thus, the releasing processor can also transfer the values to be written by its incomplete
writes. Then reads following an acquire can use the transferred values and need not be delayed.
4.2.2. An Implementation Proposal for Data-Race-Free-1 that does not obey Weak Ordering, Release Con-
sistency, or Data-Race-Free-0
This section describes an implementation proposal for the data requirement conditions. The proposal
assumes an arbitrarily large shared-memory system in which every processor has an independent cache and processors
are connected to memory through an arbitrary interconnection network. The proposal also assumes a
directory-based, writeback, invalidation, ownership, hardware cache-coherence protocol, similar in most respects
to those discussed by Agarwal et al. [4]. One significant feature of the protocol is that invalidations sent on a
write to a line in read-only or shared state are acknowledged by the invalidated processors.
The cache-coherence protocol ensures that (a) all operations are eventually seen by all processors, (b) writes
to the same location are seen in the same order by all processors, and (c) a processor can detect when an operation
it issues is complete. For (c), most operations complete when the issuing processor receives the requested line in
its cache. However, a write (data or synchronization) to a line in read-only or shared state completes when all
invalidated processors send their acknowledgements. (Either the writing processor may directly receive the ack-
nowledgements, or the directory may collect them and then forward a single message to the writing processor to
indicate the completion of the write.)
The implementation proposal involves adding the following four features to a uniprocessor-based processor
logic and the base cache-coherence logic mentioned above. (Tables 1 and 2 summarize these features.)
# Addition of three buffers per processor - incomplete, reserve, and special (Table 1),
# Modification of issue logic to delay the issue of or stall on certain operations (Table 2(a)),
# Modification of cache-coherence logic to allow a processor to retain ownership of a line in the processor's
reserve buffer and to specially handle paired acquires to such a line (Table 2(b)),
# a new processor-to-processor message called "empty special buffer" (Table 2(c)).
The discussion below explains how the above features can be used to implement the pre-release, release-
acquire, and post-acquire parts of the data requirement conditions. (Recall that "preceding" and "following"
refer to the ordering by program order.)
For the pre-release condition, a processor must remember which operations preceding its releases are
incomplete. For this, a processor uses its incomplete buffer to store the address of all its incomplete data opera-
tions. A release is not issued until all preceding synchronization operations complete (to prevent deadlock) and all
preceding data operations are issued. Thus, the incomplete buffer remembers all the operations required by the
pre-release condition. (To distinguish between operations preceding and following a release, entries in the incomplete
buffer may be tagged or multiple incomplete buffers may be used.)
For the release-acquire condition, an acquire cannot complete until the following have occurred regarding
the release paired with the acquire: (a) release is complete, (b) all operations received by the releasing processor
on its acquires preceding the release are complete, and (c) the releasing processor transfers to the new acquiring
processor the addresses of all incomplete operations preceding the release. For this purpose, every processor uses
a reserve buffer to store the processor's releases for which the above conditions do not hold. On a release (which
is a write operation), the releasing processor procures ownership of the released line. The processor does not give
up its ownership while the address of the line is in its reserve buffer. Consequently, the cache-coherence protocol
forwards subsequent requests to the line, including acquires that will be paired with the release, to the releasing
Buffer Contents Purpose
Incomplete Incomplete data operations
(of this processor)
Used to remember incomplete operations (of
this processor) preceding a release (of this pro-
cessor).
Reserve Releases (of this processor)
for which there are incomplete
operations
Used to remember releases (of this processor)
that may cause future paired acquires (of other
processors) to need special attention.
Special Incomplete operations (of
another processor) received
on an acquire (by this processor

Used to identify if an operation (of this proces-
requires special action due to early completion
of acquire (of this processor).
(a) Contents and purpose of buffers
Buffer Insertions Deletions
Event Entry Inserted Event Entry Deleted
Incomplete Data miss Address of data
operation
Data miss complete

Address of data
operation
Reserve Release issued Address of release
operation
Release com-
pletes, operations
preceding release
complete (i.e.,
deleted from incomplete
buffer),
and special buffer
empties
Address of release
operation
Special Acquire completes Addresses received
on acquire
"Empty special
buffer" message
arrives
All entries
(b) Insertion and deletion actions for buffers

Table

1. Key buffers for aggressive implementation of data-race-free-1.
processor. The releasing processor can now stall the acquires paired with the release until conditions (a), (b), and
(c) above are met.

Table

2(b) gives the details of how the base cache-coherence logic can be modified to allow a releasing processor
to retain ownership of the released line in its reserve buffer, and to service acquires paired with the release
only when (a), (b), and (c) above are met. To retain ownership of a released line, the releasing processor stalls
release operations from other processors to the same line and performs a remote service for other external requests
to the same line. The remote service mechanism allows the releasing processor to service the requests of other
Address in
Operation Special Buffer? Action
Process as usual.
Data or unpaired
synchronization
Release No Issue after all previous operations are issued and
all previous synchronization operations complete.
Acquire No Issue after special buffer empties and stall until
acquire completes.
Any Yes Stall or delay issue of only this operation until
special buffer empties.
(a) Modification to issue logic
Address in
Request
Reserve Buffer?
Action
Requests by this processor
Any No Process as usual.
Process as usual.
Any read or write
Cache line replace-
ment
Stall processor until address is deleted from
reserve buffer.
Requests from other processors forwarded to this processor
Any Process as usual.
Release Stall request until address is deleted from reserve
buffer.
Acquire Stall request until special buffer empties and
paired release (in reserve buffer) completes, send
to acquiring processor the released line and entries
of incomplete buffer tagged as preceding the
release, request acquiring processor to not cache
the line, inform directory that this processor is retaining
ownership.
Data or unpaired
synchronization
If read request, send line to other processor; if
write request, update line in this processor's
cache and send acknowledgement to other pro-
request other processor to not cache the
line; inform directory that this processor is retaining
ownership.
(b) Modification to cache-coherence logic at processor
Event Message
All incomplete buffer entries
corresponding to a release deleted
Send "empty special buffer" message
to processors that executed acquires
paired with release.
(c) New processor-to-processor message

Table

2. Aggressive implementation of data-race-free-1.
processors without allowing those processors to cache the line. The mechanisms of stalling operations for an
external release and remote service for other external operations are both necessary. This is because stalling data
operations can lead to deadlock and servicing external release operations remotely would not let the new releasing
processors procure ownership of the line as required for the release-acquire condition. Meeting conditions (a),
(b), and (c) above requires the processor to wait for its release to complete and its special buffer to empty, and to
transfer contents of its incomplete buffer to the acquiring processor.
For the post-acquire condition, a processor must (a) stall on an acquire until it completes, and (b) delay a
following operation until the completion of any conflicting operation transferred to it on the acquire. For this pur-
pose, a processor uses a special buffer to save all the information transferred to it on an acquire. If a following
operation conflicts with an operation stored in the special buffer, the processor can either (a) stall or (b) delay only
this operation, until it receives an "empty special buffer" message from the releasing processor. The releasing
processor sends the "empty special buffer" message when it deletes the address of the release paired with the
acquire from its reserve buffer. For simplicity, an acquiring processor can also stall on the acquire until its special
buffer empties to avoid the complexity of having to delay an operation for incomplete operations of multiple processors

This completes the implementation proposal for the data requirement conditions, assuming a process runs
uninterrupted on the same processor. To handle context switches correctly, a processor must stall before switching
until the various buffers mentioned above empty. Overflow of the above buffers can also be handled by making
a processor stall until an entry is deleted from the relevant buffer.
The above proposal never leads to deadlock or livelock as long as the underlying cache-coherence protocol
is implemented correctly, and messages are not lost in the network (or a time-out that initiates a system clean-up is
generated on a lost message). Specifically, the above proposal never stalls a memory operation indefinitely since
(i) the proposal never delays the completion of issued data operations, and (ii) the proposal delays an operation
only if certain issued data operations are incomplete. Thus, the above proposal does not lead to deadlock or
livelock.
5. vs. Other Models
Previous sections have shown how the data-race-free-1 memory model unifies weak ordering, release con-
sistency, the VAX model, and data-race-free-0. This section first summarizes other memory models proposed in
the literature, and then examines how data-race-free-1 relates to them.
The IBM 370 memory model [19] guarantees that except for a write followed by a read to a different loca-
tion, operations of a single processor will appear to execute in program order, and writes will appear to execute
atomically. The 370 also provides serialization operations. Before executing a serialization operation, a processor
completes all operations that are before the serialization operation according to program order. Before executing
any nonserialization operation, a processor completes all serialization operations that are before that nonserializa-
tion operation according to program order. The processor consistency [11, 16], PRAM [22] and total store ordering
[25] models ensure that writes of a given processor appear to execute in the same order to all other processors.
The models mainly differ in whether a write appears to become visible to all other processors simultaneously or at
different times. The partial store ordering model [25] is similar to total store ordering except that it orders writes
by a processor only if they are separated by a store barrier operation. The model known as release consistency
with processor-consistent special operations [11] is similar to release consistency with sequentially consistent special
operations except that it requires special operations (syncs and nsyncs) to be processor-consistent. The
concurrent-consistency model [26] ensures sequential consistency to all programs except those "which explicitly
test for sequential consistency or take access timings into consideration." The slow memory model [18] requires
that a read return the value of some previous conflicting write. After a value written by (say) processor P i is read,
the values of earlier conflicting writes by P i cannot be returned. The causal memory model [5, 18] ensures that
any write that causally precedes a read is observed by the read. Causal precedence is a transitive relation established
by program order or due to a read that returns the value of a write.
is based on the assumption that most programmers prefer to reason with sequential con-
sistency. Concurrent consistency is the only model above that explicitly states when programmers can expect
sequential consistency; however, the conditions that give sequential consistency seem ambiguous and are difficult
to relate directly to data-race-free-1. The 370 model does not explicitly state when programmers can expect
sequential consistency; however, the previous sections on data-race-free-1 can be used to determine a sufficient
condition as follows. The serialization operations are analogous to the synchronization operations of weak order-
ing; therefore, the 370 appears sequentially consistent to data-race-free programs where serialization operations
that access memory are interpreted as synchronization operations and every write serialization operation is pair-
able with every read serialization operation.
For the remaining models, it is difficult to determine exactly when programmers can expect sequential con-
sistency. If the assumption that programmers prefer to reason with sequential consistency is true, then as stated,
the above models are harder to reason with than data-race-free-1. In the future, we hope to specify the above
models using the approach of data-race-free-1; i.e., specify the models in terms of a formal set of constraints on
programs such that the hardware appears sequentially consistent to all programs that obey those constraints. We
call this approach the sequential consistency normal form. We will investigate if such specifications provide
greater insight and lead to more unifications.
6. Conclusions
Many programmers of shared-memory systems implicitly assume the model of sequential consistency for
the shared memory. Unfortunately, sequential consistency restricts the use of many high performance uniprocessor
optimizations. For higher performance, several alternate memory models have been proposed. Such models
should (1) be simple to reason with and (2) provide high performance. We believe that most programmers prefer
to reason with sequential consistency. Therefore, a way to satisfy the above properties is for a model to appear
sequentially consistent to the most common programs and to give these programs the highest performance possi-
ble. The models of weak ordering, release consistency (with sequentially consistent special operations), the VAX,
and data-race-free-0 are based on the common intuition that if programmers distinguish their data and synchronization
operations, then correct execution can be guaranteed along with high performance. However, each model
formalizes the intuition differently, and has different advantages and disadvantages with respect to the other
models.
This paper proposed a memory model, data-race-free-1, that unifies weak ordering, release consistency, the
VAX model and data-race-free-0, and retains the advantages of each of them. Hardware is data-race-free-1 if it
appears sequentially consistent to all programs that are data-race-free. Data-race-free-1 unifies the four models by
providing a programmer's view that is similar to that of the four models, and by permitting all hardware allowed
by the four models. Compared to weak ordering, data-race-free-1 provides a more formal interface for programmers
since it explicitly states when a program is correctly synchronized (data-race-free) and how hardware
behaves for correctly synchronized programs (sequentially consistent). Also, data-race-free-1 is less restrictive
than weak ordering for hardware designers since it allows an implementation that weak ordering does not allow.
Compared to release consistency, data-race-free-1 is less restrictive for hardware designers since it allows an
implementation that release consistency does not allow. Compared to the VAX model, data-race-free-1 provides
a more formal interface since it explicitly states when a program is correctly synchronized and how hardware
behaves for correctly synchronized programs. Compared to data-race-free-0, data-race-free-1 is less restrictive
for hardware designers since it allows implementations to take different actions on different types of synchronization
operations.

Acknowledgements

We are immensely grateful to Dr. Harold Stone, the editor, for his advice and patience through several revisions
of this paper. We are also grateful to the anonymous referees for many comments and suggestions that have
improved this work considerably. We thank Kourosh Gharachorloo for many insightful discussions on memory
models and comments on earlier drafts of this paper. We also thank Vikram Adve, Brian Bershad, Allan Gottlieb,
Ross Johnson, Alex Klaiber, Jim Larus, David Wood, and Richard Zucker for their valuable comments on earlier
drafts of this paper.



--R

Weak Ordering - A New Definition
Detecting Data Races on Weak Memory Systems
Sufficient Conditions for Implementing the Data-Race-Free-1 Memory Model
An Evaluation of Directory Schemes for Cache Coherence
Implementing and Programming Causal Distributed Shared Memory
Evaluation Using a Multiprocessor Simulation Model
Asynchronous Parallel Successive Overrelaxation for the Symmetric Linear Complementarity Problem

Memory Access Buffering in Multiprocessors
Memory Access Dependencies in Shared-Memory Multiprocessor
Memory Consistency and Event Ordering in Scalable Shared-Memory Multiprocessors
Two Techniques to Enhance the Performance of Memory Consistency Models
Performance Evaluation of Memory Consistency Models for Shared-Memory Multiprocessors
Detecting Violations of
Proving
Computer Sciences Technical Report
The NYU Ultracomputer - Designing an MIMD Shared Memory Parallel Computer
Weakening Consistency to Enhance Concurrency in Distributed Shared Memories


How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
PRAM: A Scalable Shared Memory
Algorithms for Scalable Synchronization on Shared-Memory Multiprocessors
Seminar at Texas Instruments Research Labs (Dallas

Access Ordering and Coherence in Shared Memory Multiprocessors
Efficient and Correct Execution of Parallel Programs that Share Memory
A Study of Weak Consistency Models
--TR
Cache coherence protocols: evaluation using a multiprocessor simulation model
Memory access buffering in multiprocessors
Efficient and correct execution of parallel programs that share memory
An evaluation of directory schemes for cache coherence
Asynchronous parallel successive overrelaxation for the symmetric linear complementarity problem
Access ordering and coherence in shared memory multiprocessors
Memory Access Dependencies in Shared-Memory Multiprocessors
Algorithms for scalable synchronization on shared-memory multiprocessors
Performance evaluation of memory consistency models for shared-memory multiprocessors
Proving sequential consistency of high-performance shared memories (extended abstract)
Detecting violations of sequential consistency
Detecting data races on weak memory systems
Weak orderingMYAMPERSANDmdash;a new definition
Memory consistency and event ordering in scalable shared-memory multiprocessors
Lockup-free instruction fetch/prefetch cache organization

--CTR
Honghui Lu , Alan L. Cox , Willy Zwaenepoel, Contention elimination by replication of sequential sections in distributed shared memory programs, ACM SIGPLAN Notices, v.36 n.7, p.53-61, July 2001
Alvaro E. Campos , Juan E. Navarro, A page-coherent, causally consistent protocol for distributed shared memory, Journal of Systems and Software, v.72 n.3, p.305-319, August 2004
A. L. Cox , S. Dwarkadas , P. Keleher , H. Lu , R. Rajamony , W. Zwaenepoel, Software versus hardware shared-memory implementation: a case study, ACM SIGARCH Computer Architecture News, v.22 n.2, p.106-117, April 1994
Leonidas I. Kontothanassis , Michael L. Scott , Ricardo Bianchini, Lazy release consistency for hardware-coherent multiprocessors, Proceedings of the 1995 ACM/IEEE conference on Supercomputing (CDROM), p.61-es, December 04-08, 1995, San Diego, California, United States
Neves , Miguel Castro , Paulo Guedes, A checkpoint protocol for an entry consistent shared memory system, Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing, p.121-129, August 14-17, 1994, Los Angeles, California, United States
Chong , Kai Hwang, Performance Analysis of Four Memory Consistency Models for Multithreaded Multiprocessors, IEEE Transactions on Parallel and Distributed Systems, v.6 n.10, p.1085-1099, October 1995
Povl T. Koch , Robert J. Fowler , Eric Jul, Message-driven relaxed consistency in a software distributed shared memory, Proceedings of the 1st USENIX conference on Operating Systems Design and Implementation, p.7-es, November 14-17, 1994, Monterey, California
Jos F. Martnez , Josep Torrellas, Speculative synchronization: applying thread-level speculation to explicitly parallel applications, ACM SIGOPS Operating Systems Review, v.36 n.5, December 2002
James R. Larus , Brad Richards , Guhan Viswanathan, LCM: memory system support for parallel language implementation, ACM SIGPLAN Notices, v.29 n.11, p.208-218, Nov. 1994
Robert Stets , Sandhya Dwarkadas , Nikolaos Hardavellas , Galen Hunt , Leonidas Kontothanassis , Srinivasan Parthasarathy , Michael Scott, Cashmere-2L: software coherent shared memory on a clustered remote-write network, ACM SIGOPS Operating Systems Review, v.31 n.5, p.170-183, Dec. 1997
Ramakrishnan Rajamony , Alan L. Cox, Performance debugging shared memory parallel programs using run-time dependence analysis, ACM SIGMETRICS Performance Evaluation Review, v.25 n.1, p.75-87, June 1997
Alex Gontmakher , Avi Mendelson , Assaf Schuster, Using fine grain multithreading for energy efficient computing, Proceedings of the 12th ACM SIGPLAN symposium on Principles and practice of parallel programming, March 14-17, 2007, San Jose, California, USA
Dejan Perkovic , Peter J. Keleher, A Protocol-Centric Approach to on-the-Fly Race Detection, IEEE Transactions on Parallel and Distributed Systems, v.11 n.10, p.1058-1072, October 2000
Leonidas Kontothanassis , Robert Stets , Galen Hunt , Umit Rencuzogullari , Gautam Altekar , Sandhya Dwarkadas , Michael L. Scott, Shared memory computing on clusters with symmetric multiprocessors and system area networks, ACM Transactions on Computer Systems (TOCS), v.23 n.3, p.301-335, August 2005
Guang R. Gao , Vivek Sarkar, Location Consistency-A New Memory Model and Cache Consistency Protocol, IEEE Transactions on Computers, v.49 n.8, p.798-813, August 2000
Fong Pong , Michel Dubois, Formal Automatic Verification of Cache Coherence in Multiprocessors with Relaxed Memory Models, IEEE Transactions on Parallel and Distributed Systems, v.11 n.9, p.989-1006, September 2000
Robert C. Steinke , Gary J. Nutt, A unified theory of shared memory consistency, Journal of the ACM (JACM), v.51 n.5, p.800-849, September 2004
Vijay S. Pai , Parthasarathy Ranganathan , Sarita V. Adve , Tracy Harton, An evaluation of memory consistency models for shared-memory systems with ILP processors, ACM SIGPLAN Notices, v.31 n.9, p.12-23, Sept. 1996
Matthew J. Zekauskas , Wayne A. Sawdon , Brian N. Bershad, Software write detection for a distributed shared memory, Proceedings of the 1st USENIX conference on Operating Systems Design and Implementation, p.8-es, November 14-17, 1994, Monterey, California
Xiaowei Shen , Arvind , Larry Rudolph, Commit-reconcile & fences (CRF): a new memory model for architects and compiler writers, ACM SIGARCH Computer Architecture News, v.27 n.2, p.150-161, May 1999
Fong Pong , Michel Dubois, Verification techniques for cache coherence protocols, ACM Computing Surveys (CSUR), v.29 n.1, p.82-126, March 1997
Allon Adir , Hagit Attiya , Gil Shurek, Information-Flow Models for Shared Memory with an Application to the PowerPC Architecture, IEEE Transactions on Parallel and Distributed Systems, v.14 n.5, p.502-515, May
Dan Grossman , Jeremy Manson , William Pugh, What do high-level memory models mean for transactions?, Proceedings of the 2006 workshop on Memory system performance and correctness, October 22-22, 2006, San Jose, California
Jeremy Manson , William Pugh , Sarita V. Adve, The Java memory model, ACM SIGPLAN Notices, v.40 n.1, p.378-391, January 2005
Jae Bum Lee , Chu Shik Jhon, Reducing coherence overhead of barrier synchronization in software DSMs, Proceedings of the 1998 ACM/IEEE conference on Supercomputing (CDROM), p.1-18, November 07-13, 1998, San Jose, CA
H. Sarojadevi , S. K. Nandy , S. Balakrishnan, On the correctness of program execution when cache coherence is maintained locally at data-sharing boundaries in distributed shared memory multiprocessors, International Journal of Parallel Programming, v.32 n.5, p.415-446, October 2004
M. Rasit Eskicioglu, A comprehensive bibliography of distributed shared memory, ACM SIGOPS Operating Systems Review, v.30 n.1, p.71-96, Jan. 1996
hazards and raceconditions;data-race-free-1;shared-memory models;weak ordering;shared memory systems;formalization;index termsmultiprocessors;data-race-free-0;sequential consistency;release consistency