Weak Memory Models: Balancing Definitional Simplicity and Implementation
Flexibility

arXiv:1707.05923v1 [] 19 Jul 2017

Sizhuo Zhang, Muralidaran Vijayaraghavan, Arvind
Computer Science and Artificial Intelligence Laboratory
Massachusetts Institute of Technology
{szzhang, vmurali, arvind}@csail.mit.edu

Abstract—The memory model for RISC-V, a newly developed
open source ISA, has not been finalized yet and thus, offers an
opportunity to evaluate existing memory models. We believe
RISC-V should not adopt the memory models of POWER or
ARM, because their axiomatic and operational definitions are
too complicated. We propose two new weak memory models:
WMM and WMM-S, which balance definitional simplicity and
implementation flexibility differently. Both allow all instruction
reorderings except overtaking of loads by a store. We show
that this restriction has little impact on performance and it
considerably simplifies operational definitions. It also rules
out the out-of-thin-air problem that plagues many definitions.
WMM is simple (it is similar to the Alpha memory model),
but it disallows behaviors arising due to shared store buffers
and shared write-through caches (which are seen in POWER
processors). WMM-S, on the other hand, is more complex and
allows these behaviors. We give the operational definitions of
both models using Instantaneous Instruction Execution (I2 E),
which has been used in the definitions of SC and TSO. We also
show how both models can be implemented using conventional
cache-coherent memory systems and out-of-order processors,
and encompasses the behaviors of most known optimizations.

commercial processors and then constructing models to fit
these observations [7]–[10], [12]–[16].
The newly designed open-source RISC-V ISA [17] offers a
unique opportunity to reverse this trend by giving a clear definition with understandable implications for implementations.
The RISC-V ISA manual only states that its memory model
is weak in the sense that it allows a variety of instruction
reorderings [18]. However, so far no detailed definition has
been provided, and the memory model is not fixed yet.
In this paper we propose two weak memory models for
RISC-V: WMM and WMM-S, which balance definitional
simplicity and implementation flexibility differently. The difference between the two models is regarding store atomicity,
which is often classified into the following three types [19]:
•
•

Keywords-weak memory model
•

I. I NTRODUCTION
A memory model for an ISA is the specification of all
legal multithreaded program behaviors. If microarchitectural
changes conform to the memory model, software remains
compatible. Leaving the meanings of corner cases to be
implementation dependent makes the task of proving the
correctness of multithreaded programs, microarchitectures
and cache protocols untenable. While strong memory models
like SC and SPARC/Intel-TSO are well understood, weak
memory models of commercial ISAs like ARM and POWER
are driven too much by microarchitectural details, and
inadequately documented by manufacturers. For example, the
memory model in the POWER ISA manual [11] is “defined”
as reorderings of events, and an event refers to performing
an instruction with respect to a processor. While reorderings
capture some properties of memory models, it does not
specify the result of each load, which is the most important
information to understand program behaviors. This forces
the researchers to formalize these weak memory models by
empirically determining the allowed/disallowed behaviors of

Single-copy atomic: a store becomes visible to all processors at the same time, e.g., in SC.
Multi-copy atomic: a store becomes visible to the issuing
processor before it is advertised simultaneously to all other
processors, e.g., in TSO and Alpha [5].
Non-atomic (or non-multi-copy-atomic): a store becomes
visible to different processors at different times, e.g., in
POWER and ARM.

Multi-copy atomic stores are caused by the store buffer
or write-through cache that is private to each processor.
Non-atomic stores arise (mostly) because of the sharing
of a store buffer or a write-through cache by multiple
processors, and such stores considerably complicate the
formal definitions [7], [8]. WMM is an Alpha-like memory
model which permits only multi-copy atomic stores and
thus, prohibits shared store buffers or shared write-through
caches in implementations. WMM-S is an ARM/POWERlike memory model which admits non-atomic stores. We will
present the implementations of both models using out-oforder (OOO) processors and cache-coherent memory systems.
In particular, WMM and WMM-S allow the OOO processors
in multicore settings to use all speculative techniques which
are valid for uniprocessors, including even the load-value
speculation [20]–[24], without additional checks or logic.
We give operational definitions of both WMM and WMMS. An operational definition specifies an abstract machine,
and the legal behaviors of a program under the memory

Operational
model
SC
TSO
RMO
Alpha
RC
ARM and
POWER
WMM
WMM-S

Simple; I2 E [1]
Simple; I2 E [2]
Doesn’t exist
Doesn’t exist
Doesn’t exist
Complex; non
I2 E [7], [8]
Simple; I2 E
Medium; I2 E

Definition
Axiomatic model

Simple [1]
Simple [3]
Simple; needs fix [4]
Medium [5]
Medium [6]
Complex [9], [10]

Single-copy atomic
Multi-copy atomic
Multi-copy atomic
Multi-copy atomic
Unclear
Non-atomic

Model properties / Implementation flexibility
Allow shared write- Instruction reorderings
through cache/shared
store buffer
No
None
No
Only St-Ld reordering
No
All four
No
All four
No
All four
Yes
All four

Simple
Doesn’t exist

Multi-copy atomic
Non-atomic

No
Yes

Store atomicity

Figure 1.

All except Ld-St reordering
All except Ld-St reordering

Ordering
of
data-dependent
loads
Yes
Yes
Yes
No
Yes
Yes
No
No

Summary of different memory models

model are those that can result by running the program
on the abstract machine. We observe a growing interest
in operational definitions: memory models of x86, ARM
and POWER have all been formalized operationally [2], [7],
[8], [15], [25], and researchers are even seeking operational
definitions for high-level languages like C++ [26]. This is
perhaps because all possible program results can be derived
from operational definitions mechanically while axiomatic
definitions require guessing the whole program execution
at the beginning. For complex programs with dependencies,
loops and conditional branches, guessing the whole execution
may become prohibitive.
Unfortunately, the operational models of ARM and
POWER are too complicated because their abstract machines
involve microarchitectural details like reorder buffers (ROBs),
partial and speculative instruction execution, instruction
replay on speculation failure, etc. The operational definitions
of WMM and WMM-S are much simpler because they are
described in terms of Instantaneous Instruction Execution
(I2 E), which is the style used in the operational definitions of
SC [1] and TSO [2], [25]. An I2 E abstract machine consists
of n atomic processors and an n-ported atomic memory.
The atomic processor executes instructions instantaneously
and in order, so it always has the up-to-date architectural
(register) state. The atomic memory executes loads and
stores instantaneously. Instruction reorderings and store
atomicity/non-atomicity are captured by including different
types of buffers between the processors and the atomic
memory, like the store buffer in the definition of TSO. In
the background, data moves between these buffers and the
memory asynchronously, e.g., to drain a value from a store
buffer to the memory.
I2 E definitions free programmers from reasoning partially
executed instructions, which is unavoidable for ARM and
POWER operational definitions. One key tradeoff to achieve
I2 E is to forbid a store to overtake a load, i.e., disallow Ld-St
reordering. Allowing such reordering requires each processor
in the abstract machine to maintain multiple unexecuted
instructions in order to see the effects of future stores, and
the abstract machine has to contain the complicated ROBlike structures. Ld-St reordering also complicates axiomatic

definitions because it creates the possibility of “out-ofthin-air” behaviors [27], which are impossible in any real
implementation and consequently must be disallowed. We
also offer evidence, based on simulation experiments, that
disallowing Ld-St reordering has no discernible impact on
performance.
For a quick comparison, we summarize the properties of
common memory models in Figure 1. SC and TSO have
simple definitions but forbid Ld-Ld and St-St reorderings,
and consequently, are not candidates for RISC-V. WMM is
similar to RMO and Alpha but neither has an operational
definition. Also WMM has a simple axiomatic definition,
while Alpha requires a complicated axiom to forbid outof-thin-air behaviors (see Section V-B), and RMO has
an incorrect axiom about data-dependency ordering (see
Section X).
ARM, POWER, and WMM-S are similar models in the
sense that they all admit non-atomic stores. While the
operational models of ARM and POWER are complicated,
WMM-S has a simpler I2 E definition and allows competitive
implementations (see Section IX-B). The axiomatic models
of ARM and POWER are also complicated: four relations in
the POWER axiomatic model [10, Section 6] are defined in
a fixed point manner, i.e., their definitions mutually depend
on each other.
Release Consistency (RC) are often mixed with the concept
of “SC for data-race-free (DRF) programs” [28]. It should be
noted that “SC for DRF” is inadequate for an ISA memory
model, which must specify behaviors of all programs. The
original RC definition [6] attempts to specify all program
behaviors, and are more complex and subtle than the “SC for
DRF” concept. We show in Section X that the RC definition
fails a litmus test for non-atomic stores and forbids shared
write-through caches in implementation.
This paper makes the following contributions:
1) WMM, the first weak memory model that is defined
in I2 E and allows Ld-Ld reordering, and its axiomatic
definition;
2) WMM-S, an extension on WMM that admits non-atomic
stores and has an I2 E definition;
3) WMM and WMM-S implementations based on OOO pro-

cessors that admit all uniprocessor speculative techniques
(such as load-value prediction) without additional checks;
4) Introduction of invalidation buffers in the I2 E definitional
framework to model Ld-Ld and other reorderings.
Paper organization: Section II presents the related work.
Section III gives litmus tests for distinguishing memory
models. Section IV introduces I2 E. Section V defines
WMM. Section VI shows the WMM implementation using
OOO processors. Section VII evaluates the performance of
WMM and the influence of forbidding Ld-St reordering.
Section VIII defines WMM-S. Section IX presents the
WMM-S implementations with non-atomic stores. Section X
shows the problems of RC and RMO. Section XI offers the
conclusion.

dependency between I2 and I3 in Figure 2a. Thus the
resulting behaviors can arise only because of different store
atomicity properties. We use FENCELL for memory models
that can reorder data-dependent loads, e.g., I5 in Figure 2b
would be the MB fence for Alpha. For other memory models
that order data-dependent loads (e.g., ARM), FENCELL could
be replaced by a data dependency (like the data dependency
between I2 and I3 in Figure 2a). The Ld-Ld fences only
stop Ld-Ld reordering; they do not affect store atomicity in
these tests.

II. R ELATED W ORK

(a) SBE: test for multi-copy atomic stores

SC [1] is the simplest model, but naive implementations of
SC suffer from poor performance. Although researchers have
proposed aggressive techniques to preserve SC [29]–[38],
they are rarely adopted in commercial processors perhaps due
to their hardware complexity. Instead the manufactures and
researchers have chosen to present weaker memory models,
e.g., TSO [2], [3], [25], [39], PSO [4], RMO [4], Alpha [5],
Processor Consistency [40], Weak Consistency [41], RC [6],
CRF [42], Instruction Reordering + Store Atomicity [43],
POWER [11] and ARM [44]. The tutorials by Adve et al.
[45] and by Maranget et al. [46] provide relationships among
some of these models.
A large amount of research has also been devoted to
specifying the memory models of high-level languages:
C++ [26], [47]–[50], Java [51]–[53], etc. We will provide
compilation schemes from C++ to WMM and WMM-S.
Recently, Lustig et al. have used Memory Ordering
Specification Tables (MOSTs) to describe memory models,
and proposed a hardware scheme to dynamically convert
programs across memory models described in MOSTs
[19]. MOST specifies the ordering strength (e.g., locally
ordered, multi-copy atomic) of two instructions from the same
processor under different conditions (e.g., data dependency,
control dependency). Our work is orthogonal in that we
propose new memory models with operational definitions.
III. M EMORY M ODEL L ITMUS T ESTS
Here we offer two sets of litmus tests to highlight
the differences between memory models regarding store
atomicity and instruction reorderings, including enforcement
of dependency-ordering. All memory locations are initialized
to 0.
A. Store Atomicity Litmus Tests
Figure 2 shows four litmus tests to distinguish between
these three types of stores. We have deliberately added
data dependencies and Ld-Ld fences (FENCELL ) to these
litmus tests to prevent instruction reordering, e.g., the data

Proc. P1
I1 : St a 1
I2 : r1 = Ld a
I3 : r2 = Ld (b+r1 −1)
SC forbids but TSO allows:

Proc. P1
I1 : St a 2

Proc. P2
I4 : St b 1
I5 : r3 = Ld b
I6 : r4 = Ld (a+r3 −1)
r1 = 1, r2 = 0, r3 = 1, r4 = 0

Proc. P2
I2 : r1 = Ld a
I3 : St b (r1 − 1)

Proc. P3
I4 : r2 = Ld b
I5 : FENCELL
I6 : r3 = Ld a
TSO, RMO and Alpha forbid, but RC, ARM
and POWER allow: r1 = 2, r2 = 1, r3 = 0
(b) WRC: test for non-atomic stores [7]
Proc. P1
I1 : St a 2

Proc. P2
Proc. P3
I2 : r1 = Ld a
I4 : r2 = Ld b
I3 : St b (r1 − 1)
I5 : St a r2
TSO, RMO, Alpha and RC forbid, but ARM and
POWER allow: r1 = 2, r2 = 1, m[a] = 2
(c) WWC: test for non-atomic stores [46], [54]
Proc. P1
I1 : St a 1

Proc. P2
I2 : r1 = Ld a
I3 : FENCELL
I4 : r2 = Ld b
TSO, RMO and Alpha forbid,
POWER allow: r1 = 1, r2 = 0,

Proc. P3
I5 : St b 1

Proc. P4
I6 : r3 = Ld b
I7 : FENCELL
I8 : r4 = Ld a
but RC, ARM and
r3 = 1, r4 = 0

(d) IRIW: test for non-atomic stores [7]
Figure 2.

Litmus tests for store atomicity

SBE: In a machine with single-copy atomic stores (e.g., an
SC machine), when both I2 and I5 have returned value 1,
stores I1 and I4 must have been globally advertised. Thus
r2 and r4 cannot both be 0. However, a machine with store
buffers (e.g., a TSO machine) allows P1 to forward the value
of I1 to I2 locally without advertising I1 to other processors,
violating the single-copy atomicity of stores.
WRC: Assuming the store buffer is private to each processor
(i.e., multi-copy atomic stores), if one observes r1 = 2 and
r2 = 1 then r3 must be 2. However, if an architecture allows
a store buffer to be shared by P1 and P2 but not P3, then P2
can see the value of I1 from the shared store buffer before
I1 has updated the memory, allowing P3 to still see the old
value of a. A write-through cache shared by P1 and P2 but
not P3 can cause this non-atomic store behavior in a similar
way, e.g., I1 updates the shared write-through cache but has
not invalidated the copy in the private cache of P3 before I6

is executed.
WWC: This litmus test is similar to WRC but replaces the
load in I6 with a store. The behavior is possible if P1 and
P2 share a write-through cache or store buffer. However, RC
forbids this behavior (see Section X).
IRIW: This behavior is possible if P1 and P2 share a writethrough cache or a store buffer and so do P3 and P4.
B. Instruction Reordering Litmus Tests
Although processors fetch and commit instructions in order,
speculative and out-of-order execution causes behaviors as if
instructions were reordered. Figure 3 shows the litmus tests
on these reordering behaviors.
Proc. P1
Proc. P2
I1 : St a 1
I3 : St b 1
I2 : r1 = Ld b I4 : r2 = Ld a
SC forbids, but TSO allows:
r1 = 0, r2 = 0

Proc. P1
Proc. P2
I1 : St a 1 I3 : r1 = Ld b
I2 : St b 1 I4 : r2 = Ld a
TSO forbids, but Alpha and
RMO allow: r1 = 1, r2 = 0

(a) SB: test for St-Ld reordering [46] (b) MP: test for Ld-Ld and St-St
reorderings [7]
Proc. P1
Proc. P2
I1 : r1 = Ld b I3 : r2 = Ld a
I2 : St a 1
I4 : St b 1
TSO forbids, but Alpha,
RMO, RC, POWER and
ARM allow: r1 = r2 = 1

Proc. P1
Proc. P2
I1 : St a 1 I4 : r1 = Ld b
I2 : FENCE I5 : if(r1 6= 0) exit
I3 : St b 1 I6 : r2 = Ld a
Alpha, RMO, RC, ARM and
POWER allow: r1 = 1, r2 = 0

(c) LB: test for Ld-St reordering [7] (d) MP+Ctrl: test
dependency ordering
Proc. P1
Proc. P2
I1 : St a 1
I4 : r1 = Ld b
I2 : FENCE I5 : St (r1 + a) 42
I3 : St b 100 I6 : r2 = Ld a
Alpha, RMO, RC, ARM
and POWER allow: r1 =
100, r2 = 0

for

Proc. P1
Proc. P2
I1 : St a 1 I4 : r1 = Ld b
I2 : FENCE I5 : r2 = Ld r1
I3 : St b a
RMO, RC, ARM and
POWER forbid, but Alpha
allows: r1 = a, r2 = 0

(e) MP+Mem: test for memory- (f) MP+Data: test
dependency ordering
dependency ordering
Figure 3.

control-

for

data-

Litmus tests for instruction reorderings

SB: A TSO machine can execute I2 and I4 while I1 and I3
are buffered in the store buffers. The resulting behavior is as
if the store and the load were reordered on each processor.
MP: In an Alpha machine, I1 and I2 may be drained from
the store buffer of P1 out of order; I3 and I4 in the ROB of
P2 may be executed out of order. This is as if P1 reordered
the two stores and P2 reordered the two loads.
LB: Some machines may enter a store into the memory before
all older instructions have been committed. This results in the
Ld-St reordering shown in Figure 3c. Since instructions are
committed in order and stores are usually not on the critical
path, the benefit of the eager execution of stores is limited.
In fact we will show by simulation that Ld-St reordering
does not improve performance (Section VII).
MP+Ctrl: This test is a variant of MP. The two stores in
P1 must update memory in order due to the fence. Although

the execution of I6 is conditional on the result of I4 , P2 can
issue I6 speculatively by predicting branch I5 to be not taken.
The execution order I6 , I1 , I2 , I3 , I4 , I5 results in r1 = 1 and
r2 = 0.
MP+Mem: This test replaces the control dependency in
MP+Ctrl with a (potential) memory dependency, i.e., the
unresolved store address of I5 may be the same as the load
address of I6 before I4 is executed, However, P2 can execute
I6 speculatively by predicting the addresses are not the same.
This results in having I6 overtake I4 and I5 .
MP+Data: This test replaces the control dependency in
MP+Ctrl with a data dependency, i.e., the load address
of I5 depends on the result of I4 . A processor with loadvalue prediction [20]–[24] may guess the result of I4 before
executing it, and issue I5 speculatively. If the guess fails to
match the real execution result of I4 , then I5 would be killed.
But, if the guess is right, then essentially the execution of
the two data-dependent loads (I4 and I5 ) has been reordered.
C. Miscellaneous Tests
All programmers expect memory models to obey perlocation SC [55], i.e., all accesses to a single address appear
to execute in a sequential order which is consistent with the
program order of each thread (Figure 4).
Proc. P1
Proc. P2
I1 : r1 = Ld a I3 : St a 1
I2 : r2 = Ld a
Models with per-location
SC forbid: r1 = 1, r2 = 0
Figure 4.

Per-location SC

Proc. P1
Proc. P2
I1 : r1 = Ld b I3 : r2 = Ld a
I2 : St a r1
I4 : St b r2
All models forbid: r1 = r2 = 42
Figure 5.

Out-of-thin-air read

Out-of-thin-air behaviors (Figure 5) are impossible in real
implementations. Sometimes such behaviors are permitted
by axiomatic models due to incomplete axiomatization.
IV. D EFINING M EMORY M ODELS IN I 2 E
Figure 6 shows the I2 E abstract machines for SC,
TSO/PSO and WMM models. All abstract machines consist
of n atomic processors and an n-ported atomic memory m.
Each processor contains a register state s, which represents
all architectural registers, including both the general purpose
registers and special purpose registers, such as PC. The
abstract machines for TSO/PSO and WMM also contain a
store buffer sb for each processor, and the one for WMM
also contains an invalidation buffer ib for each processor as
shown in the figure. In the abstract machines all buffers are
unbounded. The operations of these buffers will be explained
shortly.
The operations of the SC abstract machine are the simplest:
in one step we can select any processor to execute the
next instruction on that processor atomically. That is, if
the instruction is a non-memory instruction (e.g., ALU or
branch), it just modifies the register states of the processor; if
it is a load, it reads from the atomic memory instantaneously

Processor ݅

Processor ݅

Reg State ‫ݏ‬
Processor ݅
…

Reg State ‫ݏ‬

…

…

Reg State ‫ݏ‬

…
Store
Buffer ‫ܾݏ‬

…

Inv
Buffer ܾ݅

Store
Buffer ‫ܾݏ‬

Atomic Memory ݉

Atomic Memory ݉

Atomic Memory ݉

(a) SC

(b) TSO/PSO

(c) WMM

Figure 6.

…

I2 E abstract machines for different models

and updates the register state; and if it is a store, it updates
the atomic memory instantaneously and increments the PC.
A. TSO Model
The TSO abstract machine proposed in [2], [25] (Figure
6b) contains a store buffer sb for each processor. Just like SC,
any processor can execute an instruction atomically, and if
the instruction is a non-memory instruction, it just modifies
the local register state. A store is executed by inserting its
haddress, valuei pair into the local sb instead of writing the
data in memory. A load first looks for the load address in the
local sb and returns the value of the youngest store for that
address. If the address is not in the local sb, then the load
returns the value from the atomic memory. TSO can also
perform a background operation, which removes the oldest
store from a sb and writes it into the atomic memory. As
we discussed in Section III, store buffer allows TSO to do
St-Ld reordering, i.e., pass the SB litmus test (Figure 3a).
In order to enforce ordering in accessing the memory and
to rule out non-SC behaviors, TSO has a fence instruction,
which we refer to as Commit. When a processor executes
a Commit fence, it gets blocked unless its sb is empty.
Eventually, any sb will become empty as a consequence
of the background operations that move data from the sb to
the memory. For example, we need to insert a Commit fence
after each store in Figure 3a to forbid the non-SC behavior
in TSO.
We summarize the operations of the TSO abstract machine
in Figure 7. Each operation consists of a predicate and an
action. The operation can be performed by taking the action
only when the predicate is true. Each time we perform only
one operation (either instruction execution or sb dequeue)
atomically in the whole system (e.g., no two processors can
execute instructions simultaneously). The choice of which
operation to perform is nondeterministic.
Enabling St-St reordering: We can extend TSO to PSO by
changing the background operation to dequeue the oldest
store for any address in sb (see the PSO-DeqSb operation in
Figure 7). This extends TSO by permitting St-St reordering.
V. WMM M ODEL
WMM allows Ld-Ld reordering in addition to the reorderings allowed by PSO. Since a reordered load may read a stale

TSO-Nm (non-memory execution)
Predicate: The next instruction of a processor is a non-memory
instruction.
Action: Instruction is executed by local computation.
TSO-Ld (load execution)
Predicate: The next instruction of a processor is a load.
Action: Assume the load address is a. The load returns the value
of the youngest store for a in sb if a is present in the sb of
the processor, otherwise, the load returns m[a], i.e., the value of
address a in the atomic memory.
TSO-St (store execution)
Predicate: The next instruction of a processor is a store.
Action: Assume the store address is a and the store value is v.
The processor inserts the store ha, vi into its sb.
TSO-Com (Commit execution)
Predicate: The next instruction of a processor is a Commit and
the sb of the processor is empty.
Action: The Commit fence is executed simply as a NOP.
TSO-DeqSb (background store buffer dequeue)
Predicate: The sb of a processor is not empty.
Action: Assume the haddress, valuei pair of the oldest store in
the sb is ha, vi. Then this store is removed from sb, and the
atomic memory m[a] is updated to v.
PSO-DeqSb (background store buffer dequeue)
Predicate: The sb of a processor is not empty.
Action: Assume the value of the oldest store for some address a
in the sb is v. Then this store is removed from sb, and the atomic
memory m[a] is updated to v.
Figure 7.

Operations of the TSO/PSO abstract machine

value, we introduce a conceptual device called invalidation
buffer, ib, for each processor in the I2 E abstract machine (see
Figure 6c). ib is an unbounded buffer of haddress, valuei
pairs, each representing a stale memory value for an address
that can be observed by the processor. Multiple stale values
for an address in ib are kept ordered by their staleness.
The operations of the WMM abstract machine are similar
to those of PSO except for the background operation and
the load execution. When the background operation moves
a store from sb to the atomic memory, the original value
in the atomic memory, i.e., the stale value, enters the ib of
every other processor. A load first searches the local sb. If
the address is not found in sb, it either reads the value in
the atomic memory or any stale value for the address in the
local ib, the choice between the two being nondeterministic.
The abstract machine operations maintain the following
invariants: once a processor observes a store, it cannot observe
any staler store for that address. Therefore, (1) when a store
is executed, values for the store address in the local ib are
purged; (2) when a load is executed, values staler than
the load result are flushed from the local ib; and (3) the
background operation does not insert the stale value into
the ib of a processor if the sb of the processor contains the
address.
Just like introducing the Commit fence in TSO, to prevent
loads from reading the stale values in ib, we introduce the
Reconcile fence to clear the local ib. Figure 8 summarizes

the operations of the WMM abstract machine.
WMM-Nm (non-memory execution): Same as TSO-Nm.
WMM-Ld (load execution)
Predicate: The next instruction of a processor is a load.
Action: Assume the load address is a. If a is present in the sb
of the processor, then the load returns the value of the youngest
store for a in the local sb. Otherwise, the load is executed in
either of the following two ways (the choice is arbitrary):
1) The load returns the atomic memory value m[a], and all values
for a in the local ib are removed.
2) The load returns some value for a in the local ib, and all
values for a older than the load result are removed from the
local ib. (If there are multiple values for a in ib, the choice
of which one to read is arbitrary).
WMM-St (store execution)
Predicate: The next instruction of a processor is a store.
Action: Assume the store address is a and the store value is v.
The processor inserts the store ha, vi into its sb, and removes all
values for a from its ib.
WMM-Com (Commit execution): Same as TSO-Com.
WMM-Rec (execution of a Reconcile fence)
Predicate: The next instruction of a processor is a Reconcile.
Action: All values in the ib of the processor are removed.
WMM-DeqSb (background store buffer dequeue)
Predicate: The sb of a processor is not empty.
Action: Assume the value of the oldest store for some address
a in the sb is v. First, the stale haddress, valuei pair ha, m[a]i
is inserted to the ib of every other processor whose sb does not
contain a. Then this store is removed from sb, and m[a] is set
to v.
Figure 8.

Operations of the WMM abstract machine

A. Properties of WMM
Similar to TSO/PSO, WMM allows St-Ld and St-St
reorderings because of sb (Figures 3a and 3b). To forbid
the behavior in Figure 3a, we need to insert a Commit
followed by a Reconcile after the store in each processor.
Reconcile is needed to prevent loads from getting stale values
from ib. The I2 E definition of WMM automatically forbids
Ld-St reordering (Figure 3c) and out-of-thin-air behaviors
(Figure 5).
Ld-Ld reordering: WMM allows the behavior in Figure 3b
due to St-St reordering. Even if we insert a Commit between
the two stores in P1, the behavior is still allowed because
I4 can read the stale value 0 from ib. This is as if the two
loads in P2 were reordered. Thus, we also need a Reconcile
between the two loads in P2 to forbid this behavior in WMM.
No dependency ordering: WMM does not enforce any dependency ordering. For example, WMM allows the behaviors
of litmus tests in Figures 3d, 3e and 3f (I2 should be Commit
in case of WMM), because the last load in P2 can always
get the stale value 0 from ib in each test. Thus, it requires
Reconcile fences to enforce dependency ordering in WMM.
In particular, WMM can reorder the data-dependent loads
(i.e., I4 and I5 ) in Figure 3f.
Multi-copy atomic stores: Stores in WMM are multicopy atomic, and WMM allows the behavior in Figure 2a

even when Reconcile fences are inserted between Ld-Ld
pairs hI2 , I3 i and hI5 , I6 i. This is because a store can be
read by a load from the same processor while the store
is in sb. However, if the store is ever pushed from sb
to the atomic memory, it becomes visible to all other
processors simultaneously. Thus, WMM forbids the behaviors
in Figures 2b, 2c and 2d (FENCELL should be Reconcile in
these tests).
Per-location SC: WMM enforces per-location SC (Figure 4),
because both sb and ib enforce FIFO on same address entries.
B. Axiomatic Definition of WMM
Based on the above properties of WMM, we give a simple
axiomatic definition for WMM in Figure 9 in the style of
the axiomatic definitions of TSO and Alpha. A True entry
in the order-preserving table (Figure 9b) indicates that if
instruction X precedes instruction Y in the program order
(X <po Y ) then the order must be maintained in the global
memory order (<mo ). <mo is a total order of all the memory
and fence instructions from all processors. The notation
rf
S −→ L means a load L reads from a store S. The notation
max<mo {set of stores} means the youngest store in the
set according to <mo . The axioms are self-explanatory: the
program order must be maintained if the order-preserving
table says so, and a load must read from the youngest
store among all stores that precede the load in either the
memory order or the program order. (See Appendix A for
the equivalence proof of the axiomatic and I2 E definitions.)
These axioms also hold for Alpha with a slightly different
order-preserving table, which marks the (Ld,St) entry as
a = b. (Alpha also merges Commit and Reconcile into a
single fence). However, allowing Ld-St reordering creates
the possibility of out-of-thin-air behaviors, and Alpha uses an
additional complicated axiom to disallow such behaviors [5,
Chapter 5.6.1.7]. This axiom requires considering all possible
execution paths to determine if a store is ordered after a load
by dependency, while normal axiomatic models only examine
a single execution path at a time. Allowing Ld-St reordering
also makes it difficult to define Alpha operationally.
Axiom Inst-Order (preserved instruction ordering):
X <po Y ∧ order(X, Y ) ⇒ X <mo Y
Axiom Ld-Val (the value of a load):
rf
St a v −→ Ld a ⇒ St a v =
max<mo {St a v 0 | St a v 0 <mo Ld a ∨ St a v 0 <po Ld a}
(a) Axioms for WMM

HH Y
X H
H

Ld a
St a v
Reconcile
Commit

Ld b

St b v 0

Reconcile

Commit

a=b
False
True
False

True
a=b
True
True

True
False
True
True

True
True
True
True

(b) WMM order-preserving table, i.e. order(X, Y ) where X <po Y
Figure 9.

Axiomatic definition of WMM

C. Compiling C++11 to WMM

OOO Processor ܲ݅

…

Reorder Buffer (ROB)

C++ primitives [47] can be mapped to WMM instructions
in an efficient way as shown in Figure 10. For the purpose
of comparison, we also include a mapping to POWER [56].
C++ operations
Non-atomic Load
Load Relaxed
Load Consume
Load Acquire
Load SC
Non-atomic Store
Store Relaxed
Store Release
Store SC
Figure 10.

WMM instructions
Ld
Ld
Ld; Reconcile
Ld; Reconcile
Commit; Reconcile;
Ld; Reconcile
St
St
Commit; St
Commit; St

POWER instructions
Ld
Ld
Ld
Ld; cmp; bc; isync
sync; Ld; cmp;
bc; isync
St
St
lwsync; St
sync; St

Mapping C++ to WMM and POWER

The Commit; Reconcile sequence in WMM is the same as
a sync fence in POWER, and Commit is similar to lwsync.
The cmp; bc; isync sequence in POWER serves as a Ld-Ld
fence, so it is similar to a Reconcile fence in WMM. In case
of Store SC in C++, WMM uses a Commit while POWER
uses a sync, so WMM effectively saves one Reconcile. On
the other hand, POWER does not need any fence for Load
Consume in C++, while WMM requires a Reconcile.
Besides the C++ primitives, a common programming
paradigm is the well-synchronized program, in which all
critical sections are protected by locks. To maintain SC
behaviors for such programs in WMM, we can add a
Reconcile after acquiring the lock and a Commit before
releasing the lock.
For any program, if we insert a Commit before every store
and insert a Commit followed by a Reconcile before every
load, then the program behavior in WMM is guaranteed to
be sequentially consistent. This provides a conservative way
for inserting fences when performance is not an issue.
VI. WMM I MPLEMENTATION
WMM can be implemented using conventional OOO
multiprocessors, and even the most aggressive speculative
techniques cannot step beyond WMM. To demonstrate this,
we describe an OOO implementation of WMM, and show
simultaneously how the WMM model (i.e., the I2 E abstract
machine) captures the behaviors of the implementation. The
implementation is described abstractly to skip unrelated
details (e.g., ROB entry reuse). The implementation consists
of n OOO processors and a coherent write-back cache
hierarchy which we discuss next.

Ld resp
delay

Ld req

…

Store Buffer

Port ݅

St req

Mem Req Buffer ݉‫ܾݎ‬ሾ݅ሿ

St resp

Write‐back
Cache Hierarchy

(CCM)

Atomic Memory ݉

Figure 11.

CCM+OOO: implementation of WMM

Consider a real n-ported write-back cache hierarchy with
each port i connected to processor P i. A request issued to
port i may be from a load instruction in the ROB of P i or
a store in the store buffer of P i. In conventional coherence
protocols, all memory requests can be serialized, i.e., each
request can be considered as taking effect at some time point
within its processing period [57]. For example, consider the
non-stalling MSI directory protocol in the Primer by Sorin
et al. [58, Chapter 8.7.2]. In this protocol, a load request
takes effect immediately if it hits in the cache; otherwise, it
takes effect when it gets the data at the directory or a remote
cache with M state. A store request always takes effect at
the time of writing the cache, i.e., either when it hits in the
cache, or when it has received the directory response and all
invalidation responses in case of miss. We also remove the
requesting store from the store buffer when a store request
takes effect. Since a cache cannot process multiple requests
to the same address simultaneously, we assume requests to
the same address from the same processor are processed in
the order that the requests are issued to the cache.
CCM (Figure 11) abstracts the above cache hierarchy
by operating as follows: every new request from port i is
inserted into a memory request buffer mrb[i], which keeps
requests to the same address in order; at any time we can
remove the oldest request for an address from a mrb, let
the request access the atomic memory m, and either send
the load result to ROB (which may experience a delay)
or immediately dequeue the store buffer. m represents the
coherent memory states. Removing a request from mrb and
accessing m captures the moment when the request takes
effect.
It is easy to see that the atomic memory in CCM
corresponds to the atomic memory in the WMM model,
because they both hold the coherent memory values. We will
show shortly that how WMM captures the combination of
CCM and OOO processors. Thus any coherent protocol that
can be abstracted as CCM can be used to implement WMM.
B. Out-of-Order Processor (OOO)

A. Write-Back Cache Hierarchy (CCM)
We describe CCM as an abstraction of a conventional
write-back cache hierarchy to avoid too much details. In the
following, we explain the function of such a cache hierarchy,
abstract it to CCM, and relate CCM to the WMM model.

The major components of an OOO processor are the ROB
and the store buffer (see Figure 11). Instructions are fetched
into and committed from ROB in order; loads can be issued
(i.e., search for data forwarding and possibly request CCM)
as soon as its address is known; a store is enqueued into the

store buffer only when the store commits (i.e., entries in a
store buffer cannot be killed). To maintain the per-location
SC property of WMM, when a load L is issued, it kills
younger loads which have been issued but do not read from
stores younger than L. Next we give the correspondence
between OOO and WMM.
Store buffer: The state of the store buffer in OOO is
represented by the sb in WMM. Entry into the store buffer
when a store commits in OOO corresponds to the WMM-St
operation. In OOO, the store buffer only issues the oldest
store for some address to CCM. The store is removed from
the store buffer when the store updates the atomic memory
in CCM. This corresponds to the WMM-DeqSb operation.
ROB and eager loads: Committing an instruction from
ROB corresponds to executing it in WMM, and thus the
architectural register state in both WMM and OOO must
match at the time of commit. Early execution of a load L to
address a with a return value v in OOO can be understood by
considering where ha, vi resides in OOO when L commits.
Reading from sb or atomic memory m in the WMM-Ld
operation covers the cases that ha, vi is, respectively, in the
store buffer or the atomic memory of CCM when L commits.
Otherwise ha, vi is no longer present in CCM+OOO at the
time of load commit and must have been overwritten in the
atomic memory of CCM. This case corresponds to having
performed the WMM-DeqSb operation to insert ha, vi into
ib previously, and now using the WMM-Ld operation to read
v from ib.
Speculations: OOO can issue a load speculatively by
aggressive predictions, such as branch prediction (Figure 3d),
memory dependency prediction (Figure 3e) and even loadvalue prediction (Figure 3f). As long as all predictions related
to the load eventually turn out to be correct, the load result
got from the speculative execution can be preserved. No
further check is needed. Speculations effectively reorder
dependent instructions, e.g., load-value speculation reorders
data-dependent loads. Since WMM does not require preserving any dependency ordering, speculations will neither break
WMM nor affect the above correspondence between OOO
and WMM.
Fences: Fences never go into store buffers or CCM in the
implementation. In OOO, a Commit can commit from ROB
only when the local store buffer is empty. Reconcile plays a
different role; at the time of commit it is a NOP, but while
it is in the ROB, it stalls all younger loads (unless the load
can bypass directly from a store which is younger than the
Reconcile). The stall prevents younger loads from reading
values that would become stale when the Reconcile commits.
This corresponds to clearing ib in WMM.
Summary: For any execution in the CCM+OOO implementation, we can operate the WMM model following the
above correspondence. Each time CCM+OOO commits an
instruction I from ROB or dequeues a store S from a store
buffer to memory, the atomic memory of CCM, store buffers,

and the results of committed instructions in CCM+OOO
are exactly the same as those in the WMM model when the
WMM model executes I or dequeues S from sb, respectively.
VII. P ERFORMANCE E VALUATION OF WMM
We evaluate the performance of implementations of WMM,
Alpha, SC and TSO. All implementations use OOO cores
and coherent write-back cache hierarchy. Since Alpha allows
Ld-St reordering, the comparison of WMM and Alpha will
show whether such reordering affects performance.
A. Evaluation Methodology
We ran SPLASH-2x benchmarks [59], [60] on an 8-core
multiprocessor using the ESESC simulator [61]. We ran all
benchmarks except ocean ncp, which allocates too much
memory and breaks the original simulator. We used simmedium inputs except for cholesky, fft and radix, where we
used sim-large inputs. We ran all benchmarks to completion
without sampling.
The configuration of the 8-core multiprocessor is shown
in Figures 12 and 13 . We do not use load-value speculation
in this evaluation. The Alpha implementation can mark a
younger store as committed when instruction commit is
stalled, as long as the store can never be squashed and
the early commit will not affect single-thread correctness. A
committed store can be issued to memory or merged with
another committed store in WMM and Alpha. SC and TSO
issue loads speculatively and monitor L1 cache evictions to
kill speculative loads that violate the consistency model. We
also implement store prefetch as an optional feature for SC
and TSO; We use SC-pf and TSO-pf to denote the respective
implementations with store prefetch.
Cores
L3 cache

Memory

8 cores (@2GHz) with private L1 and L2 caches
4MB shared, MESI coherence, 64-byte cache line
8 banks, 16-way, LRU replacement, max 32 req per bank
3-cycle tag, 10-cycle data (both pipelined)
5 cycles between cache bank and core (pipelined)
120-cycle latency, max 24 requests
Figure 12.

Frontend
ROB
Function
units
Ld queue
St queue
L1 D
cache
L2 cache

Multiprocessor system configuration

fetch + decode + rename, 7-cycle pipelined latency in all
2-way superscalar, hybrid branch predictor
128 entries, 2-way issue/commit
2 ALUs, 1 FPU, 1 branch unit, 1 load unit, 1 store unit
32-entry reservation station per unit
Max 32 loads
Max 24 stores, containing speculative and committed stores
32KB private, 1 bank, 4-way, 64-byte cache line
LRU replacement, 1-cycle tag, 2-cycle data (pipelined)
Max 32 upgrade and 8 downgrade requests
128KB private, 1 bank, 8-way, 64-byte cache line
LRU replacement, 2-cycle tag, 6-cycle data (both pipelined)
Max 32 upgrade and 8 downgrade requests
Figure 13.

Core configuration

empty

pendSt

flushRep

flushInv

flushLS

exe

active

1
0.5

(Bench.)

MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC
MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC
MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC
MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC
MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC
MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC
MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC
MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC
MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC
MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC
MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC
MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC
MM
W ha f
p
Al O-p
TSO
TS -pf
SC
SC

0

barnes

cholesky

fft

Figure 14.

fmm

lu_cb

lu_ncb

ocean_cp

radix

radiosity

raytrace

volrend

water_nsq

water_sp

Normalized execution time and its breakdown at the commit slot of ROB

B. Simulation Results
A common way to study the performance of memory
models is to monitor the commit of instructions at the commit
slot of ROB (i.e., the oldest ROB entry). Here are some
reasons why an instruction may not commit in a given cycle:
• empty: The ROB is empty.
• exe: The instruction at the commit slot is still executing.
• pendSt: The load (in SC) or Commit (in TSO, Alpha and
WMM) cannot commit due to pending older stores.
• flushLS: ROB is being flushed because a load is killed
by another older load (only in WMM and Alpha) or older
store (in all models) to the same address.
• flushInv: ROB is being flushed after cache invalidation
caused by a remote store (only in SC or TSO).
• flushRep: ROB is being flushed after cache replacement
(only in SC or TSO).
Figure 14 shows the execution time (normalized to WMM)
and its breakdown at the commit slot of ROB. The total
height of each bar represents the normalized execution time,
and stacks represent different types of stall times added to
the active committing time at the commit slot.
WMM versus SC: WMM is much faster than both SC and
SC-pf for most benchmarks, because a pending older store
in the store queue can block SC from committing loads.
WMM versus TSO: WMM never does worse than TSO or
TSO-pf, and in some cases it shows up to 1.45× speedup over
TSO (in radix) and 1.18× over TSO-pf (in lu ncb). There
are two disadvantages of TSO compared to WMM. First,
load speculation in TSO is subject to L1 cache eviction, e.g.,
in benchmark ocean cp. Second, TSO requires prefetch to
reduce store miss latency, e.g., a full store queue in TSO stalls
issue to ROB and makes ROB empty in benchmark radix.
However, prefetch may sometimes degrade performance due
to interference with load execution, e.g., TSO-pf has more
commit stalls due to unfinished loads in benchmark lu ncb.
WMM versus Alpha: Figure 15 shows the average number
of cycles that a store in Alpha can commit before it reaches
the commit slot. However, the early commit (i.e., Ld-St
reordering) does not make Alpha outperform WMM (see
Figure 14), because store buffers can already hide the store
miss latency. Note that ROB is typically implemented as
a FIFO (i.e., a circular buffer) for register renaming (e.g.,

freeing physical registers in order), precise exceptions, etc.
Thus, if the early committed store is in the middle of ROB, its
ROB entry cannot be reused by a newly fetched instruction,
i.e., the effective size of the ROB will not increase. In
summary, the Ld-St reordering in Alpha does not increase
performance but complicates the definition (Section V-B).
15

Cycles

Normalized time

1.5

10
5
0

bar cho fft
nes les
ky

Figure 15.

fmm lu_ lu_ oce rad rad ray vol wa wa
cb ncb an ix
ios trac ren ter_ ter_
_cp
ity
nsq sp
e d

Average cycles to commit stores early in Alpha

VIII. WMM-S M ODEL
Unlike the multi-copy atomic stores in WMM, stores in
some processors (e.g., POWER) are non-atomic due to shared
write-through caches or shared store buffers. If multiple
processors share a store buffer or write-through cache, a
store by any of these processors may be seen by all these
processors before other processors. Although we could tag
stores with processor IDs in the store buffer, it is infeasible
to separate values stored by different processors in a cache.
In this section, we introduce a new I2 E model, WMMS, which captures the non-atomic store behaviors in a way
independent from the sharing topology. WMM-S is derived
from WMM by adding a new background operation. We will
show later in Section IX why WMM-S can be implemented
using memory systems with non-atomic stores.
A. I2 E Definition of WMM-S
The structure of the abstract machine of WMM-S is the
same as that of WMM. To model non-atomicity of stores,
i.e., to make a store by one processor readable by another
processor before the store updates the atomic memory, WMMS introduces a new background operation that copies a store
from one store buffer into another. However, we need to
ensure that all stores for an address can still be put in a total
order (i.e., the coherence order), and the order seen by any
processor is consistent with this total order (i.e., per-location
SC).

To identify all the copies of a store in various store buffers,
we assign a unique tag t when a store is executed (by being
inserted into sb), and this tag is copied when a store is
copied from one store buffer to another. When a background
operation dequeues a store from a store buffer to the memory,
all its copies must be deleted from all the store buffers which
have them. This requires that all copies of the store are the
oldest for that address in their respective store buffers.
All the stores for an address in a store buffer can be strictly
ordered as a list, where the youngest store is the one that
entered the store buffer last. We make sure that all ordered
lists (of all store buffers) can be combined transitively to
form a partial order (i.e., no cycle), which has now to be
understood in terms of the tags on stores because of the
copies. We refer to this partial order as the partial coherence
order (<co ), because it is consistent with the coherence order.
Consider the states of store buffers shown in Figure 16
(primes are copies). A, B, C and D are different stores
to the same address, and their tags are tA , tB , tC and tD ,
respectively. A0 and B 0 are copies of A and B respectively
created by the background copy operation. Ignoring C 0 , the
partial coherence order contains: tD <co tB <co tA (D is
older than B, and B is older than A0 in P2), and tC <co tB
(C is older than B 0 in P3). Note that tD and tC are not
related here.
At this point, if we copied C in P3 as C 0 into P1, we
would add a new edge tA <co tC , breaking the partial order
by introducing the cycle tA <co tC <co tB <co tA . Thus
copying of C into P1 should be forbidden in this state.
Similarly, copying a store with tag tA into P1 or P2 should
be forbidden because it would immediately create a cycle:
tA <co tA . In general, the background copy operation must
be constrained so that the partial coherence order is still
acyclic after copying.

Enqueued later (younger)
↕
Enqueued earlier (Older)

Figure 16.

P1 sb

P2 sb

P3 sb

C’:

A’:
B:
D:

B’:

A:

C:

Example states of store buffers

Figure 17 shows the background operations of the WMMS abstract machine. The operations that execute instructions
in WMM-S are the same as those in WMM, so we do not
show them again. (The store execution operation in WMM-S
needs to also insert the tag of the store into sb).
Binding background copy with load execution: If the
WMM-S-Copy operation is restricted to always happen right
before a load execution operation that reads from the newly
created copy, it is not difficult to prove that the WMMS model remains the same, i.e., legal behaviors do not
change. In the rest of the paper, we will only consider this
“restricted” version of WMM-S. In particular, all WMM-SCopy operations in the following analysis of litmus tests fall

WMM-DeqSb (background store buffer dequeue)
Predicate: There is a store S in a store buffer, and all copies of
S are the oldest store for that address in their respective store
buffers.
Action: Assume the haddress, value, tagi tuple of store S is
ha, v, ti. First, the stale haddress, valuei pair ha, m[a]i is inserted
to the ib of every processor whose sb does not contain a. Then
all copies of S are removed from their respective store buffers,
and the atomic memory m[a] is updated to v.
WMM-S-Copy (background store copy)
Predicate: There is a store S that is in the sb of some processor
i but not in the sb of some other processor j. Additionally, the
partial coherence order will still be acyclic if we insert a copy of
S into the sb of processor j.
Action: Insert a copy of S into the sb of processor j, and remove
all values for the store address of S from the ib of processor j.
Figure 17.

Background operations of WMM-S

into this pattern.

B. Properties of WMM-S
WMM-S enforces per-location SC (Figure 4), because it
prevents cycles in the order of stores to the same address. It
also allows the same instruction reorderings as WMM does
(Figure 3). We focus on the store non-atomicity of WMM-S.
Non-atomic stores and cumulative fences: Consider the
litmus tests for non-atomic stores in Figures 2b, 2c and
2d (FENCELL should be Reconcile in these tests). WMM-S
allows the behavior in Figure 2b by copying I1 into the sb of
P2 and then executing I2 , I3 , I4 , I5 , I6 sequentially. I1 will
not be dequeued from sb until I6 returns value 0. To forbid
this behavior, a Commit is required between I2 and I3 in
P2 to push I1 into memory. Similarly, WMM-S allows the
behavior in Figure 2c (i.e., we copy I1 into the sb of P2
to satisfy I2 , and I1 is dequeued after I5 has updated the
atomic memory), and we need a Commit between I2 and
I3 to forbid the behavior. In both litmus tests, the inserted
fences have a cumulative global effect in ordering I1 before
I3 and the last instruction in P3.
WMM-S also allows the behavior in Figure 2d by copying
I1 into the sb of P2 to satisfy I2 , and copying I5 into the sb
of P4 to satisfy I6 . To forbid the behavior, we need to add a
Commit right after the first load in P2 and P4 (but before the
FENCELL /Reconcile that we added to stop Ld-Ld reordering).
As we can see, Commit and Reconcile are similar to release
and acquire respectively. Cumulation is achieved by globally
advertising observed stores (Commit) and preventing later
loads from reading stale values (Reconcile).
Programming properties: WMM-S is the same as WMM
in the properties described in Section V-C, including the
compilation of C++ primitives, maintaining SC for wellsynchronized programs, and the conservative way of inserting
fences.

IX. WMM-S I MPLEMENTATIONS
Since WMM-S is strictly more relaxed than WMM, any
WMM implementation is a valid WMM-S implementation.
However, we are more interested in implementations with
non-atomic memory systems. Instead of discussing each
specific system one by one, we explain how WMM-S can be
implemented using the ARMv8 flowing model, which is a
general abstraction of non-atomic memory systems [8]. We
first describe the adapted flowing model (FM) which uses
fences in WMM-S instead of ARM, and then explain how it
obeys WMM-S.
A. The Flowing Model (FM)
FM consists of a tree of segments s[i] rooted at the
atomic memory m. For example, Figure 19 shows four OOO
processors (P1. . .P4) connected to a 4-ported FM which has
six segments (s[1 . . . 6]). Each segment is a list of memory
requests, (e.g., the list of blue nodes in s[6], whose head is
at the bottom and the tail is at the top).
OOO interacts with FM in a slightly different way than
CCM. Every memory request from a processor is appended to
the tail of the list of the segment connected to the processor
(e.g., s[1] for P1). OOO no longer contains a store buffer;
after a store is committed from ROB, it is directly sent to
FM and there is no store response. When a Commit fence
reaches the commit slot of ROB, the processor sends a
Commit request to FM, and the ROB will not commit the
Commit fence until FM sends back the response for the
Commit request.
Inside FM, there are three background operations: (1) Two
requests in the same segment can be reordered in certain
cases; (2) A load can bypass from a store in the same segment;
(3) The request at the head of the list of a segment can flow
into the parent segment (e.g., flow from s[1] into s[5]) or the
atomic memory (in case the parent of the segment, e.g., s[6],
is m). Details of these operations are shown in Figure 18.
It is easy to see that FM abstracts non-atomic memory
systems, e.g., Figure 19 abstracts a system in which P1
and P2 share a write-through cache while P3 and P4 share
another.
Two properties of FM+OOO: First, FM+OOO enforces
per-location SC because the segments in FM never reorder
requests to the same address. Second, stores for the same
address, which lie on the path from a processor to m in
the tree structure of FM, are strictly ordered based on their
distance to the tree root m; and the combination of all
such orderings will not contain any cycle. For example, in
Figure 19, stores in segments s[3] and s[6] are on the path
from P3 to m; a store in s[6] is older than any store (for the
same address) in s[3], and stores (for the same address) in
the same segment are ordered from bottom to top (bottom
is older).

FM-Reorder (reorder memory requests)
Predicate: The list of segment s[i] contains two consecutive
requests rnew and rold (rnew is above rold in s[i]); and neither
of the following is true:
1) rnew and rold are memory accesses to the same address.
2) rnew is a Commit and rold is a store.
Action: Reorder rnew and rold in the list of s[i].
FM-Bypass (store forwarding)
Predicate: The list of segment s[i] contains two consecutive
requests rnew and rold (rnew is above rold in s[i]). rnew is a
load, rold is a store, and they are for the same address.
Action: we send the load response for rnew using the store value
of rold , and remove rnew from the segment.
FM-Flow (flow request)
Predicate: A segment s[i] is not empty.
Action: Remove the request r which is the head of the list of s[i].
If the parent of s[i] in the tree structure is another segment s[j],
we append r to the tail of the list of s[j]. Otherwise, the parent
of s[i] is m, and we take the following actions according to the
type of r:
• If r is a load, we send a load response using the value in m.
• If r is a store ha, vi, we update m[a] to v.
• If r is a Commit, we send a response to the requesting processor
and the Commit fence can then be committed from ROB.
Figure 18.

Background operations of FM

B. Relating FM+OOO to WMM-S
WMM-S can capture the behaviors of any program
execution in implementation FM+OOO in almost the same
way that WMM captures the behaviors of CCM+OOO. When
a store updates the atomic memory in FM+OOO, WMMS performs a WMM-S-DeqSb operation to dequeue that
store from store buffers to memory. When an instruction
is committed from a ROB in FM+OOO, WMM-S executes
that instruction. The following invariants hold after each
operation in FM+OOO and the corresponding operation in
WMM-S:
1) For each instruction committed in FM+OOO, the execution results in FM+OOO and WMM-S are the same.
2) The atomic memories in FM+OOO and WMM-S match.
3) The sb of each processor P i in WMM-S holds exactly all
the stores in FM+OOO that is observed by the commits
of P i but have not updated the atomic memory. (A store
is observed by the commits of P i if it has been either
committed by P i or returned by a load that has been
committed by P i).
4) The order of stores for the same address in the sb of any
processor in WMM-S is exactly the order of those stores
on the path from P i to m in FM+OOO.
It is easy to see how the invariants are maintained when
the atomic memory is updated or a non-load instruction is
committed in FM+OOO. To understand the commit of a load
L to address a with result v in processor P i in FM+OOO, we
still consider where ha, vi resides when L commits. Similar
to WMM, reading atomic memory m or local ib in the load

execution operation of WMM-S covers the cases that ha, vi
is still in the atomic memory of FM or has already been
overwritten by another store in the atomic memory of FM,
respectively. In case ha, vi is a store that has not yet updated
the atomic memory in FM, ha, vi must be on the path from
P i to m. In this case, if ha, vi has been observed by the
commits of P i before L is committed, then L can be executed
by reading the local sb in WMM-S. Otherwise, on the path
from P i to m, ha, vi must be younger than any other store
observed by the commits of P i. Thus, WMM-S can copy
ha, vi into the sb of P i without breaking any invariant. The
copy will not create any cycle in <co because of invariants 3
and 4 as well as the second property of FM+OOO mentioned
above. After the copy, WMM-S can have L read v from the
local sb.
Performance comparison with ARM and POWER: As
we have shown that WMM-S can be implemented using the
generalized memory system of ARM, we can turn an ARM
multicore into a WMM-S implementation by stopping Ld-St
reordering in the ROB. Since Section VII already shows
that Ld-St reordering does not affect performance, we can
conclude qualitatively that there is no discernible performance
difference between WMM-S and ARM implementations. The
same arguments apply to the comparison against POWER
and RC.

list tail req
list head req

FM

Atomic memory

Figure 19.

OOO+FM

Proc. P1
Proc P2
I1 : St a 1
I4 : r1 = Ld b
I2 : MEMBAR I5 : if(r1 6= 1) exit
I3 : St b 1
I6 : St c 1
I7 : r2 = Ld c
I8 : r3 = a+r2 −1
I9 : r4 = Ld r3
RMO forbids: r1 = 1, r2 = 1
r3 = a, r4 = 0
Figure 20. RMO dependency order

X. P ROBLEMS OF RC AND RMO
Here we elaborate the problems of RC (both RCsc and
RCpc ) and RMO, which have been pointed out in Section I.
RC: Although the RC definition [6] allows the behaviors of
WRC and IRIW (Figures 2b and 2d), it disallows the behavior
of WWC (Figure 2c). In WWC, when I2 reads the value of
store I1 , the RC definition says that I1 is performed with
respect to (w.r.t) P2. Since store I5 has not been issued due
to the data dependencies in P2 and P3, I1 must be performed
w.r.t P2 before I5 . The RC definition says that “all writes
to the same location are serialized in some order and are
performed in that order with respect to any processor” [6,
Section 2]. Thus, I1 is before I5 in the serialization order
of stores for address a, and the final memory value of a
cannot be 2 (the value of I1 ), i.e., RC forbids the behavior
of WWC and thus forbids shared write-through caches in
implementations.

RMO: The RMO definition [4, Section D] is incorrect in
enforcing dependency ordering. Consider the litmus test in
Figure 20 (MEMBAR is the fence in RMO). In P2, the
execution of I6 is conditional on the result of I4 , I7 loads
from the address that I6 stores to, and I9 uses the results
of I7 . According the definition of dependency ordering in
RMO [4, Section D.3.3], I9 depends on I4 transitively. Then
the RMO axioms [4, Section D.4] dictate that I9 must be
after I4 in the memory order, and thus forbid the behavior
in Figure 20. However, this behavior is possible in hardware
with speculative load execution and store forwarding, i.e., I7
first speculatively bypasses from I6 , and then I9 executes
speculatively to get 0. Since most architects will not be
willing to give up on these two optimizations, RISC-V should
not adopt RMO.
XI. C ONCLUSION
We have proposed two weak memory models, WMM and
WMM-S, for RISC-V with different tradeoffs between definitional simplicity and implementation flexibility. However
RISC-V can have only one memory model. Since there is
no obvious evidence that restricting to multi-copy atomic
stores affects performance or increases hardware complexity,
RISC-V should adopt WMM in favor of simplicity.
XII. ACKNOWLEDGMENT
We thank all the anonymous reviewers on the different
versions of this paper over the two years. We have also
benefited from the discussions with Andy Wright, Thomas
Bourgeat, Joonwon Choi, Xiangyao Yu, and Guowei Zhang.
This work was done as part of the Proteus project under the
DARPA BRASS Program (grant number 6933218).
A PPENDIX A.
P ROOF OF E QUIVALENCE BETWEEN WMM I2 E M ODEL
AND WMM A XIOMATIC M ODEL
Here we present the equivalence proof for the I2 E
definition and the axiomatic definition of WMM.
Theorem 1 (Soundness). WMM I2 E model ⊆ WMM axiomatic model.
Proof: The goal is that for any execution in the WMM
rf
I E model, we can construct relations h<po , <mo , −→i that
have the same program behavior and satisfy the WMM
axioms. To do this, we first introduce the following ghost
states to the I2 E model:
• Field source in the atomic memory: For each address a,
we add state m[a].source to record the store that writes
the current memory value.
• Fields source and overwrite in the invalidation buffer: For
each stale value ha, vi in an invalidation buffer, we add
state v.source to denote the store of this stale value, and
add state v.overwrite to denote the store that overwrites
v.source in the memory.
2

Per-processor list <po-i2e : For each processor, <po-i2e is
the list of all the instructions that has been executed by
the processor. The order in <po-i2e is the same as the
execution order in the processor. We also use <po-i2e to
represent the ordering relation in the list (the head of the
list is the oldest/minimum in <po-i2e ).
• Global list <mo-i2e : <mo-i2e is a list of all the executed
loads, executed fences, and stores that have been dequeued
from the store buffers. <mo-i2e contains instructions from
all processors. We also use <mo-i2e to represent the
ordering relation in the list (the head of the list is the
oldest/minimum in <mo-i2e ).
rf -i2e
rf -i2e
• Read-from relations −
−−−→: −−−−→ is a set of edges. Each
edge points from a store to a load, indicating that the load
had read from the store in the I2 E model.
m[a].source initially points to the initialization store, and
rf -i2e
<po-i2e , <mo-i2e , −−−−→ are all initially empty. We now show
how these states are updated in the operations of the WMM
I2 E model.
1) WMM-Nm, WMM-Com, WMM-Rec, WMM-St: Assume
the operation executes an instruction I in processor i. We
append I to the tail of list <po-i2e of processor i. If I is
a fence (i.e., the operation is WMM-Com or WMM-Rec),
then we also append I to the tail of list <mo-i2e .
2) WMM-DeqSb: Assume the operation dequeues a store S
for address a. In this case, we update m[a].source to be S.
Let S0 be the original m[a].source before this operation is
performed. Then for each new stale value ha, vi inserted
into any invalidation buffer, we set v.source = S0 and
v.overwrite = S. We also append S to the tail of list
<mo-i2e .
3) WMM-Ld: Assume the operation executes a load L for
address a in processor i. We append L to the tail of list
<po-i2e of processor i. The remaining actions depends
on how L gets its value in this operation:
• If L reads from a store S in the local store buffer, then
rf -i2e
we add edge S −−−−→ L, and append L to the tail of
list <mo-i2e .
• If L reads the atomic memory m[a], then we add edge
rf -i2e
m[a].source −−−−→ L, and append L to the tail of list
<mo-i2e .
• If L reads a stale value ha, vi in the local invalidation
rf -i2e
buffer, then we add edge v.source −−−−→ L, and we
insert L to be right before v.overwrite in list <mo-i2e
(i.e., L is older than v.overwrite, but is younger than
any other instruction which is older than v.overwrite).
As we will see later, at the end of the I2 E execution, <po-i2e ,
rf -i2e
rf
<mo-i2e and −−−−→ will become the h<po , <mo , −→i relations that satisfy the WMM axioms. Before getting there, we
show that the I2 E model has the following invariants after
each operation is performed:
1) For each address a, m[a].source in the I2 E model is the
•

youngest store for a in <mo-i2e .
2) All loads and fences that have been executed in the I2 E
model are in <mo-i2e .
3) An executed store is either in <mo-i2e or in store buffer,
i.e., for each processor i, the store buffer of processor i
contains exactly every store that has been executed in the
I2 E model but is not in <mo-i2e .
4) For any two stores S1 and S2 for the same address in the
store buffer of any processor i in the I2 E model, if S1 is
older than S2 in the store buffer, then S1 <po-i2e S2 .
5) For any processor i and any address a, address a cannot
be present in the store buffer and invalidation buffer of
processor i at the same time.
6) For any stale value v for any address a in the invalidation
buffer of any processor i in the I2 E model, the following
invariants hold:
a) v.source and v.overwrite are in <mo-i2e , and
v.source <mo-i2e v.overwrite, and there is no other
store for a between them in <mo-i2e .
b) For any Reconcile fence F that has been executed by
processor i in the I2 E model, F <mo-i2e v.overwrite.
c) For any store S for a that has been executed by
processor i in the I2 E model, S <mo-i2e v.overwrite.
d) For any load L for a that has been executed by
rf -i2e
processor i in the I2 E model, if store S −−−−→ L,
then S <mo-i2e v.overwrite.
7) For any two stale values v1 and v2 for the same address
in the invalidation buffer of any processor i in the I2 E
model, if v1 is older than v2 in the invalidation buffer,
then v1 .source <mo-i2e v2 .source.
8) For any instructions I1 and I2 , if I1 <po-i2e I2 and
order(I1 , I2 ) and I2 is in <mo-i2e , then I1 <mo-i2e I2 .
rf -i2e
9) For any load L and store S, if S −−−−→ L, then the
following invariants hold:
a) If S not in <mo-i2e , then S is in the store buffer of
the processor of L, and S <po-i2e L, and there is no
store S 0 for the same address in the same store buffer
such that S <po-i2e S 0 <po-i2e L.
b) If
S
is
in
<mo-i2e ,
then
S
=
maxmo-i2e {S 0 | S 0 .addr = L.addr ∧ (S 0 <po-i2e
L ∨ S 0 <mo-i2e L)}, and there is no other store
S 00 for the same address in the store buffer of the
processor of L such that S 00 <po-i2e L.
We now prove inductively that all invariants hold after each
operation R is performed in the I2 E model, i.e., we assume
all invariants hold before R is performed. In case performing
R changes some states (e.g., <mo-i2e ), we use superscript 0
to denote the state before R is performed (e.g., <0mo-i2e ) and
use superscript 1 to denote the state after R is performed
(e.g., <1mo-i2e ). Now we consider the type of R:
1) WMM-Nm: All invariants still hold.
2) WMM-St: Assume R executes a store S for address a

in processor i. R changes the states of the store buffer,
invalidation buffer, and <po-i2e of processor i. Now we
consider each invariant.
• Invariant 1, 2: These are not affected.
• Invariant 3: This invariant still holds for the newly
executed store S.
• Invariant 4: Since S becomes the youngest store in the
store buffer of processor i, this invariant still holds.
• Invariant 5: Since R will clear address a from the
invalidation buffer of processor i, this invariant still
holds.
• Invariant 6: Invariants 6a, 6b, 6d are not affected.
Invariant 6c still holds because there is no stale value
for a in the invalidation buffer of processor i after R
is performed.
• Invariant 7: This is not affected, because R can only
remove values from the invalidation buffer.
• Invariant 8: This is not affected because R is not in
<mo-i2e .
∗
∗
• Invariant 9: Consider load L and store S for address a
∗ rf -i2e
∗
∗
such that S −−−−→ L and L is from processor i. We
need to show that this invariant still holds for L∗ and
S ∗ . Since L∗ has been executed, we have L∗ <1po-i2e S.
Thus this invariant cannot be affected.
3) WMM-Com: Assume R executes a Commit fence F
in processor i. R adds F to the end of the <po-i2e of
processor i and adds F to the end of <mo-i2e . Now we
consider each invariant.
• Invariants 1, 3, 4, 5, 6, 7, 9: These are not affected.
• Invariant 2: This still holds because F is added to
<mo-i2e .
• Invariant 8: Consider instruction I in processor i such
that I <po-i2e F and order(I, F ). We need to show that
I <1mo-i2e F . Since order(I, F ), I can be a load, or
store, or fence. If I is a load or fence, since I has been
executed, invariant 2 says that I is in <0mo-i2e before R
is performed. Since F is added to the end of <mo-i2e ,
I <1mo-i2e F . If I is a store, the predicate of R says
that I is not in the store buffer. Then invariant 3 says
that I must be in <0mo-i2e , and we have I <1mo-i2e F .
4) WMM-Rec: Assume R executes a Reconcile fence F
in processor i. R adds F to the end of the <po-i2e of
processor i, adds F to the end of <mo-i2e , and clear the
invalidation buffer of processor i. Now we consider each
invariant.
• Invariants 1, 3, 4, 9: These are not affected.
• Invariant 2: This still holds because F is added to
<mo-i2e .
• Invariants 5, 6, 7: These invariant still hold because the
invalidation buffer of processor i is now empty.
• Invariant 8: Consider instruction I in processor i such
that I <po-i2e F and order(I, F ). We need to show that
I <1mo-i2e F . Since order(I, F ), I can be a load or

fence. Since I has been executed, I must be in <0mo-i2e
before R is performed according to invariant 2. Thus,
I <1mo-i2e F .
5) WMM-DeqSb: Assume R dequeues a store S for address
a from the store buffer of processor i. R changes the
store buffer of processor i, the atomic memory m[a], and
invalidation buffers of other processors. R also adds S
to the end of <mo-i2e . Now we consider each invariant.
• Invariant 1: This invariant still holds, because
m[a].source1 = S and S becomes the youngest store
for a in <1mo-i2e .
• Invariant 2: This is not affected.
• Invariant 3: This invariant still holds, because S is
removed from store buffer and added to <mo-i2e .
• Invariants 4: This is not affected because we only
remove stores from the store buffer.
• Invariant 5: The store buffer and invaliation buffer of
processor i cannot be affected. The store buffer and
invalidation buffer of processor j (6= i) may be affected,
because m[a]0 may be inserted into the invalidation
buffer of processor j. The predicate of R ensures that
the insertion will not happen if the store buffer of
processor j contains address a, so the invariant still
holds.
• Invariant 6: We need to consider the influence on both
existing stale values and the newly inserted stale values.
a) Consider stale value ha, vi which is in the invalidation buffer of processor j both before and after
operation R is performed. This implies j 6= i,
because the store buffer of processor i contains
address a before R is performed, and invariant 5
says that the invalidation buffer of processor i
cannot have address a before R is performed. Now
we show that each invariant still holds for ha, vi.
– Invariant 6a: This still holds because S is the
youngest in <mo-i2e .
– Invariant 6b: This is not affected.
– Invariant 6c: This is not affected because S is
not executed by processor j.
– Invariant 6d: Since S is not in <0mo-i2e , invariant 9a says that any load that has read S must
be from process i. Since i 6= j, this invariant
cannot be affected.
b) Consider the new stale value ha, vi inserted to
the invalidation buffer of process j (6= i). According to WMM-DeqSb, v = m[a]0 , v.source =
m[a].source0 , and v.overwrite = S. Now we check
each invariant.
– Invariant 6a: According to invariant 1,
v.source = m[a]0 .source is the youngest store
for a in <0mo-i2e . Since S (i.e., v.overwrite) is
appended to the tail of <0mo-i2e , this invariant
still holds.

•

•

– Invariant 6b: According to invariant 2, any
Reconcile fence F executed by processor j
must be in <0mo-i2e . Thus, F <1mo-i2e S =
v.overwrite, and the invariant still holds.
– Invariant 6c: The predicate of R says that the
store buffer of processor j cannot contain address
a. Therefore, according to invariant 3, any store
S 0 for a executed by processor j must be in
<0mo-i2e . Thus, S 0 <1mo-i2e S = v.overwrite, and
the invariant still holds.
– Invariant 6d: Consider load L for address a
that has been executed by processor j. Assume
rf -i2e
store S 0 −−−−→ L. The predicate of R says that
the store buffer of processor j cannot contain
address a. Thus, S 0 must be in <0mo-i2e according
to invariant 9a. Therefore, S 0 <1mo-i2e S =
v.overwrite, and the invariant still holds.
Invariant 8: Consider instruction I such that I <po-i2e S
and order(I, S). Since order(I, S), I can be a load,
fence, or store for a. If I is a load or fence, then
invariant 2 says that I is in <0mo-i2e , and thus I <1mo-i2e
S, i.e., the invariant holds. If I is a store for a, then
the predicate of R and invariant 4 imply that I is not
in the store buffer of processor i. Then invariant 3 says
that I must be in <0mo-i2e , and thus I <1mo-i2e S, i.e.,
the invariant holds.
Invariant 9: We need to consider the influence on both
loads that read S and loads that reads stores other than
S.
a) Consider load L for address a that reads from S,
rf -i2e
i.e., S −−−−→ L. Since S is not in <0mo-i2e before
R is performed, invariant 9a says that L must be
executed by processor i, S <po-i2e L, and there is
no store S 0 for a in the store buffer of processor
i such that S <po-i2e S 0 <po-i2e L. Now we show
rf -i2e
that both invariants still hold for S −−−−→ L.
– Invariant 9a: This is not affected because S is in
<1mo-i2e after R is performed.
– Invariant 9b: Since S <po-i2e L and S is the
youngest in <1mo-i2e , S satisfies the maxmo-i2e
formula. We prove the rest of this invariant by
contradiction, i.e., we assume there is store S 0
for a in the store buffer of processor i after R
is performed such that S 0 <po-i2e L. Note that
<po-i2e is not changed by R. The predicate of
R ensures that S is the oldest store for a in the
store buffer. Invariant 4 says that S <po-i2e S 0 .
Now we have S <po-i2e S 0 <po-i2e L (before R
is performed), contradicting with invariant 9a.
b) Consider load L for address a from processor j that
rf -i2e
reads from store S ∗ (6= S), i.e., S 6= S ∗ −−−−→ L.
Now we show that both invariants still hold for

rf -i2e

S ∗ −−−−→ L.
– Invariant 9a: This invariant cannot be affected,
because performing R can only remove a store
from a store buffer.
– Invariant 9b: This invariant can only be affected
when S ∗ is in <0mo-i2e . Since R can only remove
a store from a store buffer, the second half of
this invariant is not affected (i.e, no store S 00
in the store buffer and so on). We only need
to focus on the maxmo-i2e formula, i.e., S ∗ =
maxmo-i2e {S 0 | S 0 .addr = a ∧ (S 0 <po-i2e
L ∨ S 0 <mo-i2e L)}. Since L <1mo-i2e S, this
formula can only be affected when S <po-i2e L
and i = j. In this case, before R is performed, S
is in the store buffer of processor i, and S <po-i2e
L, and L reads from S ∗ 6= S. This contradicts
with invariant 9b which is assume to hold before
R is performed. Thus, the maxmo-i2e formula
cannot be affected either, i.e., the invariant holds.
6) WMM-Ld that reads from local store buffer: Assume R
executes a load L for address a in processor i, and L
reads from store S in the local store buffer. R appends
L to the <po-i2e of processor i, appends L to <mo-i2e ,
rf -i2e 1

and adds S −−−−→ L. Note that R does not change any
invalidation buffer or store buffer. Now we consider each
invariant.
• Invariants 1, 3, 4, 5, 7: These are not affected.
• Invariant 2: This still holds because L is added to
<mo-i2e .
• Invariant 6: We consider each invariant.
– Invariants 6a, 6b, 6c: These are not affected.
– Invariant 6d: L can only influence stale values for
a in the invalidation buffer of processor i. However,
since S is in the store buffer of processor i before
R is performed, invariant 5 says that the invalidation
buffer of processor i cannot contain address a.
Therefore this invariant still holds.
• Invariant 8: We consider instruction I such that
I <1po-i2e L and order(I, L). Since order(I, L), I can
only be a Reconcile fence or a load for a. In either
case, invariant 2 says that I is in <0mo-i2e . Since L is
appended to the end of <mo-i2e , I <1mo-i2e L, i.e., the
invariant still holds.
• Invariant 9: Since R does not change any store buffer
or any load/store already in <0mo-i2e , R cannot affect
this invariant for loads other than L. We only need to
rf -i2e 1

show that S −−−−→ L satisfies this invariant. Since
S is in the store buffer, invariant 3 says that S is
not in <mo-i2e . Therefore we only need to consider
invariant 9a. We prove by contradiction, i.e., we assume
there is store S 0 for a in the store buffer of processor i
and S <1po-i2e S 0 <1po-i2e L. Since R does not change

store buffer states, S and S 0 are both in the store buffer
before R is performed. We also have S <0po-i2e S 0
(because the only change in <po-i2e is to append L to
the end). According to the predicate of R, S should
be younger than S 0 , so S 0 <0po-i2e S (according to
invariant 4), contradicting with the previous conclusion.
Therefore, the invariant still holds.
7) WMM-Ld that reads from atomic memory: Assume R
executes a load L for address a in processor i, and
L reads from atomic memory m[a]. R appends L to
the <po-i2e of processor i, appends L to <mo-i2e , adds
rf -i2e 1

m[a].source −−−−→ L, and may remove stale values
from the invalidation buffer of processor i. Now we
consider each invariant.
• Invariants 1, 3, 4: These are not affected.
• Invariant 2: This still holds because L is added to
<mo-i2e .
• Invariants 5, 7: These are not affected because R only
remove values from an invalidation buffer.
• Invariant 6: We consider each invariant.
– Invariants 6a, 6b, 6c: These are not affected because
R only remove values from an invalidation buffer.
– Invariant 6d: L can only influence stale values for
a in the invalidation buffer of processor i. However,
R will remove address a from the the invalidation
buffer of processor i. Therefore this invariant still
holds.
• Invariant 8: We consider instruction I such that
I <1po-i2e L and order(I, L). Since order(I, L), I can
only be a Reconcile fence or a load for a. In either
case, invariant 2 says that I is in <0mo-i2e . Since L is
appended to the end of <mo-i2e , I <1mo-i2e L, i.e., the
invariant still holds.
• Invariant 9: Since R does not change any store buffer
or any load/store already in <0mo-i2e , R cannot affect
this invariant for loads other than L. We only need
rf -i2e 1

to show that m[a].source −−−−→ L satisfies this
invariant (m[a] is not changed before and after R is
performed). According to invariant 1, m[a].source is
the youngest store for a in <0mo-i2e . Therefore we
only need to consider invariant 9b. Since we also have
m[a].source <1po-i2e L, maxmo-i2e {S 0 | S 0 .addr =
a ∧ (S 0 <po-i2e L ∨ S 0 <mo-i2e L)} will return
m[a].source, i.e., the first half the invariant holds. The
predicate of R ensures that there is no store for a in
the store buffer of processor i, so the second half the
invariant also holds.
8) WMM-Ld that reads from the invalidation buffer: Assume
R executes a load L for address a in processor i, and L
reads from the stale value ha, vi in the local invalidation
buffer. R appends L to the <po-i2e of processor i, appends

rf -i2e 1

L to <mo-i2e , adds v.source −−−−→ L, and may remove
stale values from the invalidation buffer of processor i.
Now we consider each invariant.
• Invariants 1, 3, 4: These are not affected.
• Invariant 2: This still holds because L is added to
<mo-i2e .
• Invariants 5, 7: These are not affected because R can
only remove values from an invalidation buffer.
• Invariant 6: We consider each invariant.
– Invariants 6a, 6b, 6c: These are not affected because
R can only remove values from an invalidation buffer.
– Invariant 6d: Only stale values in the invalidation
buffer of processor i can be affected. Consider
stale value ha, v 0 i in the invalidation buffer of
processor i after R is performed. We need to
show that v.source <1mo-i2e v 0 .overwrite. Since
v 0 is not removed in R, v 0 must be either v or
younger than v in the invalidation buffer before
R is performed. According to invariant 7, either
v 0 .source = v.source or v.source <0mo-i2e v 0 .source.
Since v 0 .source <0mo-i2e v 0 .overwrite according to
invariant 6a, v.source <1mo-i2e v 0 .overwrite.
• Invariant 8: We consider instruction I such that
I <1po-i2e L and order(I, L), and we need to show
that I <1mo-i2e L. Since order(I, L), I can only be
a Reconcile fence or a load for a. If I is a Reconcile
fence, then invariant 6b says that I <0mo-i2e v.overwrite.
Since we insert L right before v.overwrite, we still have
I <1mo-i2e L. If I is a load for a, then invariant 6d
says that I <0mo-i2e v.overwrite, and thus we have
I <1mo-i2e L.
• Invariant 9: Since R does not change any store buffer
or any load/store already in <0mo-i2e , R cannot affect
this invariant for loads other than L. We only need to
rf -i2e 1

show that v.source −−−−→ L satisfies this invariant.
Since v.source is in <0mo-i2e , we only need to consider
invariant 9b. The predicate of R ensures that the store
buffer of processor i cannot contain address a, so the
second half of the invariant holds (i.e., there is no S 00
and so on).
Now we prove the first half of the invariant, i.e., consider maxmo-i2e {S 0 | S 0 .addr = a ∧ (S 0 <1po-i2e L ∨
S 0 <1mo-i2e L)}. First note that since v.source <0mo-i2e
v.overwrite, v.source <1mo-i2e L. Thus v.source is in
set {S 0 | S 0 .addr = a ∧ (S 0 <1po-i2e L ∨ S 0 <1mo-i2e
L)}. Consider any store S that is also in this set,
then S <1po-i2e L ∨ S <1mo-i2e L must be true.
If S <1po-i2e L, S is executed in processor i before
R is performed. Invariant 6c says that S <0mo-i2e
v.overwrite ⇒ S <1mo-i2e v.overwrite. If S <1mo-i2e L,
then S <1mo-i2e L <1mo-i2e v.overwrite. In either
case, we have S <mo-i2e v.overwrite. Since we have

proved invariant 6a holds after R is performed, either
S = v.source or S <mo-i2e v.overwrite. Therefore,
maxmo-i2e will return v.source.
It is easy to see that at the end of the I2 E execution
(of a program), there is no instruction to execute in each
processor and all store buffers are empty (i.e., all exected
loads stores and fences are in <mo-i2e ). At that time, if we
rf
define axiomatic relations <po , <mo , −→ as <po-i2e , <mo-i2e
rf -i2e
, −−−−→ respectively, then invariants 8 and 9b become
the Inst-Order and Ld-Val axioms respectively. That is,
rf -i2e
h<po-i2e , <mo-i2e , −−−−→i are the relations that satisfy the
WMM axioms and have the same program behavior as the
I2 E execution.
Theorem 2 (Completeness). WMM axiomatic model ⊆
WMM I2 E model.
Proof: The goal is that for any axiomatic relations
rf
h<po , <mo , −→i that satisfy the WMM axioms, we can
run the same program in the I2 E model and get the same
program behavior. We will devise an algorithm to operate
the I2 E model to get the same program behavior as in
rf
axiomatic relations h<po , <mo , −→i. In the algorithm, for
2
each instruction in the I E model, we need to find its
corresponding instruction in the <po in axiomatic relations.
Note that this mapping should be an one-to-one mapping, i.e.,
one instruction in the I2 E model will exactly correspond to
one instruction in the axiomatic relations and vice versa, so
we do not distinguish between the directions of the mapping.
The algorithm will create this mapping incrementally. Initially
(i.e., before the I2 E model performs any operation), for each
processor i, we only map the next instruction to execute
in processor i of the I2 E model to the oldest instruction in
the <po of processor i in the axiomatic relations. After the
algorithm starts to operate the I2 E model, whenever we have
executed an instruction in a processor in the I2 E model, we
map the next instruction to execute in that processor in the
I2 E model to the oldest unmapped instruction in the <po
of that processor in the axiomatic relations. The mapping
scheme obviously has the following two properties:
•

•

The k-th executed instruction in a processor in the I2 E
model is mapped to the k-th oldest instruction in the <po
of that processor in the axiomatic relations.
In the I2 E model, when a processor has executed x instructions, only the first x + 1 instructions (i.e., the executed
x instructions and the next instruction to execute) of that
processor are mapped to instructions in the axiomatic
relations.

Of course, later in the proof, we will show that the two corresponding instructions (one in the I2 E model and the other
in the axiomatic relations) have the same instruction types,
same load/store addresses (if they are memory accesses),
same store data (if they are stores), and same execution

results. In the following, we will assume the action of adding
new instruction mappings as an implicit procedure in the
algorithm, so we do not state it over and over again when
we explain the algorithm. When there is no ambiguity, we
do not distinguish an instruction in the I2 E model and an
instruction in the axiomatic relations if these two instructions
corresponds to each other (i.e., the algorithm has built the
mapping between them).
Now we give the details of the algorithm. The algorithm
begins with the I2 E model (in initial state), an empty set Z,
and a queue Q which contains all the memory and fence
instructions in <mo . The order of instructions in Q is the
same as <mo , i.e., the head of Q is the oldest instruction
in <mo . The instructions in Q and Z are all considered as
instructions in the axiomatic relations. In each step of the
algorithm, we perform one of the followings actions:
1) If the next instruction of some processor in the I2 E model
is a non-memory instruction, then we perform the WMMNm operation to execute it in the I2 E model.
2) Otherwise, if the next instruction of some processor in
the I2 E model is a store, then we perform the WMM-St
operation to execute that store in the I2 E model.
3) Otherwise, if the next instruction of some processor in
the I2 E model is mapped to a load L in set Z, then we
perform the WMM-Ld operation to execute L in the I2 E
model, and we remove L from Z.
4) Otherwise, we pop out instruction I from the head of Q
and process it in the following way:
a) If I is a store, then I must have been mapped to a
store in some store buffer (we will prove this), and
we perform the WMM-DeqSb operation to dequeue
I from the store buffer in the I2 E model.
b) If I is a Reconcile fence, then I must have been
mapped to the next instruction to execute in some
processor (we will prove this), and we perform the
WMM-Rec operation to execute I in the I2 E model.
c) If I is a Commit fence, then I must have been mapped
to the next instruction to execute in some processor
(we will prove this), and we perform the WMM-Com
operation to execute I in the I2 E model.
d) I must be a load in this case. If I has been mapped,
then it must be mapped to the next instruction to
execute in some processor in the I2 E model (we will
prove this), and we perform the WMM-Ld operation
to execute I in the I2 E model. Otherwise, we just
add I into set Z.
For proof purposes, we introduce the following ghost states
to the I2 E model:
•

•

Field source in atomic memory: For each address a, we
add state m[a].source to record the store that writes the
current memory value.
Fields source in invalidation buffer: For each stale value
ha, vi in an invalidation buffer, we add state v.source to

denote the store of this stale value.
These two fields are set when a WMM-DeqSb operation is
performed. Assume the WMM-DeqSb operation dequeues a
store S for address a. In this case, we update m[a].source
to be S. Let S0 be the original m[a].source before this
operation is performed. Then for each new stale value ha, vi
inserted into any invalidation buffer, we set v.source = S0 .
It is obvious that memory value m[a] is equal to the value
of m[a].source, and stale value v is equal to the value of
v.source.
For proof purposes, we define a function overwrite. For
each store S in <mo , overwrite(S) returns the store for the
same address such that
• S <mo overwrite(S), and
0
• there is no store S for the same address such that S <mo
0
S <mo overwrite(S).
In other words, overwrite(S) returns the store that overwrites
S in <mo . (overwrite(S) does not exist if S is the last store
for its address in <mo .)
Also for proof purposes, at each time in the algorithm,
we use Vi to represent the set of every store S in <mo that
satisfies all the following requirements:
1) The store buffer of processor i does not contain the
address of S.
2) overwrite(S) exists and overwrite(S) has been popped
from Q.
3) For each Reconcile fence F that has been executed by
processor i in the I2 E model, F <mo overwrite(S).
4) For each store S 0 for the same address that has been
executed by processor i in the I2 E model, S 0 <mo
overwrite(S).
5) For each load L for the same address that has been
rf
executed by processor i in the I2 E model, if store S 0 −→ L
0
in the axiomatic relations, then S <mo overwrite(S).
With the above definitions and new states, we introduce the
invariants of the algorithm. After each step of the algorithm,
we have the following invariants for the states of the I2 E
model, Z and Q:
1) For each processor i, the execution order of all executed
instructions in processor i in the I2 E model is a prefix
of the <po of processor i in the axiomatic relations.
2) The predicate of any operation performed in this step is
satisfied.
3) If we perform an operation to execute an instruction in
the I2 E model in this step, the operation is able to get
the same instruction result as that of the corresponding
instruction in the axiomatic relations.
4) The instruction type, load/stores address, and store data of
every mapped instruction in the I2 E model are the same
as those of the corresponding instruction in the axiomatic
relations.
5) All loads that have been executed in the I2 E model are
mapped exactly to all loads in <mo but not in Q or Z.

6) All fences that have been executed in processor i are
mapped exactly to all fences in <mo but not in Q.
7) All stores that have been executed and dequeued from
the store buffers in the I2 E model are mapped exactly to
all stores in <mo but not in Q.
8) For each address a, m[a].source in the I2 E model is
mapped to the youngest store for a, which has been
popped from Q, in <mo .
9) For each processor i, the store buffer of processor i
contains exactly every store that has been executed in the
I2 E model but still in Q.
10) For any two stores S1 and S2 for the same address in
the store buffer of any processor i in the I2 E model, if
S1 is older than S2 in the store buffer, then S1 <po S2 .
11) For any processor i and any address a, address a cannot
be present in the store buffer and invalidation buffer of
processor i at the same time.
12) For any processor i, for each store S in Vi , the invalidation
buffer of processor i contains an entry whose source field
is mapped to S.
13) For any stale value ha, vi in any invalidation buffer,
v.source has been mapped to a store in <mo , and
overwrite(v.source) exists, and overwrite(v.source) is not
in Q.
14) For any two stale values v1 and v2 for the same address
in the invalidation buffer of any processor i in the I2 E
model, if v1 is older than v2 in the invalidation buffer,
then v1 .source <mo v2 .source.
These invariants guarantee that the algorithm will operate
the I2 E model to produce the same program behavior as the
axiomatic model. We now prove inductively that all invariants
hold after each step of the algorithm, i.e., we assume all
invariants hold before the step. In case a state is changed in
this step, we use superscript 0 to denote the state before this
step (e.g., Q0 ) and use superscript 1 to denote the state after
this step (e.g., Q1 ). We consider which action is performed
in this step.
•

•

Action 1: We perform a WMM-Nm operation that executes
a non-memory instruction in the I2 E model. All the
invariants still hold after this step.
Action 2: We perform a WMM-St operation that executes
a store S for address a in processor i in the I2 E model.
We consider each invariant.
– Invariants 1, 2, 4: These invariants obviously hold.
– Invariants 3, 5, 6, 7, 8: These are not affected.
– Invariant 9: Note that S is mapped before this step. Since
S cannot be dequeued from the store buffer before this
step, invariant 7 says that S is still in Q. Thus, this
invariant holds.
– Invariant 10: Since S is the youngest store in store buffer
and invariant 1 holds after this step, this invariant also
holds.
– Invariant 11: Since the WMM-St operation removes

•

all stale values for a from the invalidation buffer of
processor i, this invariant still holds.
– Invariant 12: For any processor j (j 6= i), the action
in this step cannot change Vj or the invalidation buffer
of processor j. We only need to consider processor i.
The action in this step cannot introduce any new store
into Vi , i.e., Vi1 ⊆ Vi0 . Also notice that Vi1 does not
contain any store for a due to requirement 1. Since the
action in this step only removes values for address a
from the invalidation buffer of processor i, this invariant
still holds for i.
– Invariants 13, 14: These still hold, because we can only
remove values from the invalidation buffer in this step.
Action 3: We perform a WMM-Ld operation that executes
a load L in Z. (Note that L has been popped from Q
before.) We assume L is in processor i (both the axiomatic
relations and the I2 E model agree on this because of
the way we create mappings). We also assume that L has
rf
address a in the axiomatic relations, and that store S −→ L
in the axiomatic relations. According to invariant 4, L also
has load address a in the I2 E model. We first consider
several simple invariants:
– Invariants 1, 2, 5: These invariants obviously hold.
– Invariants 6, 7, 8, 9, 10: These are not affected.
– Invariant 11: Since the WMM-Ld operation does not
change store buffers and can only remove values from
the invalidation buffers, this invariant still holds.
– Invariants 13, 14: These still hold, because we can only
remove values from the invalidation buffer in this step.
We now consider the remaining invariants, i.e., 3, 4 and
12, according to the current state of Q (note that Q is not
changed in this step):
1) S is in Q: We show that the WMM-Ld operation can
read the value of S from the store buffer of processor
i in the I2 E model. We first show that S is in the store
buffer of processor i. Since L is not in Q, we have
L <mo S. According to the Ld-Val axiom, we know
S <po L, so S must have been executed. Since S is in
Q, invariant 7 says that S cannot be dequeued from the
store buffer, i.e., S is in the store buffer of processor i.
Now we prove that S is the youngest store for a in
the store buffer of processor i by contradiction, i.e.,
we assume there is another store S 0 for a which is in
the store buffer of processor i and is younger than S.
Invariant 10 says that S <po S 0 . Since S and S 0 are
stores for the same address, the Inst-Order axiom says
that S <mo S 0 . Since S 0 is in the store buffer, it is
executed before L. According to invariant 1, S 0 <po L.
rf
Then S −→ L contradicts with the Ld-Val axiom.
Now we can prove the invariants:
– Invariant 3: This holds because the WMM-Ld operation reads S from the store buffer.

– Invariant 4: This holds because invariant 3 holds after
this step.
– Invariant 12: The execution of L in this step cannot
introduce new stores into Vj for any j, i.e., Vj1 ⊆ Vj0 .
Since there is no change to any invalidation buffer
when WMM-Ld reads from the store buffer, this
invariant still holds.
2) S is not in Q but overwrite(S) is in Q: We show that
the WMM-Ld operation can read the value of S from
the atomic memory. Since S has been popped from Q
while overwrite(S) is not, S is the youngest store for
a in <mo that has been popped from Q. According to
invariant 8, the current m[a].source in the I2 E model is
S. To let WMM-Ld read m[a], we only need to show
that the store buffer of processor i does not contain any
store for a. We prove by contradiction, i.e., we assume
there is a store S 0 for a in the store buffer of processor
i. According to invariant 9, S 0 has been executed in
the I2 E model, and S 0 is still in Q. Thus, we have
S 0 <po L (according to invariant 1), and S <mo S 0 .
rf
Then S −→ L contradicts with the Ld-Val axiom.
Now we can prove the invariants:
– Invariant 3: This holds because the WMM-Ld operation reads S from the atomic memory m[a].
– Invariant 4: This holds because invariant 3 holds after
this step.
– Invariant 12: The execution of L in this step cannot
introduce new stores into Vj for any j, i.e., Vj1 ⊆ Vj0 .
Since there is no change to any invalidation buffer of
any processor other than i, we only need to consider
processor i. The WMM-Ld removes all values for
a from the invalidation buffer of processor i, so
the goal is to show that there is no store for a in
Vi1 . We prove by contradiction, i.e., assume there
is store S 0 for a in Vi1 . Requirement 5 for Vi says
that S <mo overwrite(S 0 ). Since overwrite(S) is in
Q, overwrite(S 0 ) is also in Q. This contradicts with
requirement 2. Therefore, there is no store for a in
Vi1 , and this invariant holds.
3) Both S and overwrite(S) are not in Q: We show that
the WMM-Ld operation can read the value of S from
the invalidation buffer of processor i. That is, we need
to show S ∈ Vi0 . We now prove that S satisfies all the
requirements for Vi0 :
– Requirement 1: We prove by contradiction, i.e., we
assume there is store S 0 for a in the store buffer of
processor i. Invariant 9 says that S 0 has been executed
but not in Q. Then we have S 0 <po L (invariant 1)
rf
and S <mo S 0 . Then S −→ L contradicts with the
Ld-Val axiom.
– Requirement 2: This satisfied because we assume
overwrite(S) is not in Q.

•

– Requirement 3: We prove by contradiction, i.e., we
assume that Reconcile fence F has been executed
by processor i, and overwrite(S) <mo F . Since F
is executed before L, invariant 1 says that F <po L.
Since order(F, L), the Inst-Order axiom says that
F <mo L. Now we have S <mo overwrite(S) <mo
rf
F <mo L. Thus, S −→ L contradicts with the Ld-Val
axiom.
– Requirement 4: We prove by contradiction, i.e.,
we assume that store S 0 for a has been executed
by processor i, and either S 0 = overwrite(S) or
overwrite(S) <mo S 0 . According to the definition
of overwrite, we have S <mo S 0 . Since S 0 has
been executed, invariant 1 says that S 0 <po L. Then
rf
S −→ L contradicts with the Ld-Val axiom.
– Requirement 5: We prove by contradiction, i.e., we
assume that store S 0 and load L0 are both for address
rf
a, L0 has been executed by processor i, S 0 −→ L0 ,
and either S 0 = overwrite(S) or overwrite(S) <mo
S 0 . According to the definition of overwrite, we have
S <mo S 0 . Since L0 has been executed, invariant 1
says that L0 <po L. Since order(L0 , L), the Instrf
Order axiom says that L0 <mo L. Since S 0 −→ L,
0
0
0
0
0
we have S <po L or S <mo L . Since L <po L
and L0 <mo L, we have S 0 <po L or S 0 <mo L.
rf
Since S <mo S 0 , S −→ L contradicts with the LdVal axiom.
Now we can prove the invariants:
– Invariant 3: This holds because the WMM-Ld operation reads S from the invalidation buffer of processor
i.
– Invariant 4: This holds because invariant 3 holds after
this step.
– Invariant 12: The execution of L in this step cannot
introduce new stores into Vj for any j, i.e., Vj1 ⊆ Vj0 .
Since there is no change to any invalidation buffer
of any processor other than i, we only need to
consider processor i. Assume the invalidation buffer
entry read by the WMM-Ld operation is ha, vi, and
v.source = S. The WMM-Ld rule removes any stale
value ha, v 0 i that is older than ha, vi from the invalidation buffer of processor i. The goal is to show that
v 0 .source cannot be in Vi1 . We prove by contradiction,
i.e., we assume that v 0 .source ∈ Vi1 . Since L has
been executed after this step, requirement 5 says that
S <mo overwrite(v 0 .source). Since v 0 is older than v
in the invalidation buffer before this step, invariant 14
says that v 0 .source <mo v.source = S. The above
two statements contradict with each other. Therefore,
this invariant still holds.
Action 4a: We pop a store S from the head of Q, and
we perform a WMM-DeqSb operation to dequeue S from

the store buffer. Assume that S is for address a, and
in processor i in the axiomatic relations. We first prove
that S has been mapped before this step. We prove by
contradiction, i.e., we assume S has not been mapped to
any instruction in the I2 E model before this step. Consider
the state right before this step. Let I be the next instruction
to execute in processor i in the I2 E model. We know I
is mapped and I <po S. The condition for performing
action 4a in this step says that I can only be a fence or
load, and we have order(I, S). According to the Inst-Order
axiom, I <mo S, so I has been popped from Q0 .
1) If I is a fence, since I is in <mo but not in Q0 ,
invariant 6 says that I must be executed, contradicting
our assumption that I is the next instruction to execute.
2) If I is a load, since I is not executed, and I is in <mo ,
and I is not in Q0 , invariant 5 says that I must be
in Z 0 . Then this algorithm step should use action 3
instead of action 4a.
Due to the contradictions, we know S must have been
mapped. Note that the next instruction to execute in
processor i cannot be store, because otherwise this step
will use action 2. According to invariant 4, S cannot be
mapped to the next instruction to execution in processor
i. Therefore S must have been executed in processor i in
the I2 E model before this step.
Also according to invariant 4, the address and data of S
in the I2 E model are the same as those in the axiomatic
relations. Now we consider each invariant.
– Invariants 1, 4, 7, 9, 10: These invariants obviously hold.
– Invariants 3, 5, 6: These are not affected.
– Invariant 2: We prove by contradiction, i.e., we assume
there is a store S 0 for a younger than S 0 in the store
buffer of processor i (before this step). According to
invariant 9, S 0 is in Q. Since S is the head of Q0 ,
S <mo S 0 . According to invariant 10, S 0 <po S. Since
order(S 0 , S), S 0 <mo S, contradicting with previous
statement. Thus, the predicate of the WMM-DeqSb
operation is satisfied, and the invariant holds.
– Invariant 8: S is the youngest instruction in <mo that
has been popped from Q, and m[a].source is updated
to S. Thus, this invariant still holds.
– Invariant 11: Since the WMM-DeqSb operation will not
insert the stale value into an invalidation buffer of a
processor if the store buffer of that processor contains
the same address, this invariant still holds.
– Invariant 12: For any processor j, the action this step
will not remove stores from Vj but may introduce new
stores to Vj , i.e., Vj0 ⊆ Vj1 . We consider the following
two types of processors.
1) Processor i: We show that Vi0 = Vi1 . We prove
by contradiction, i.e., we assume there is store S 0
such that S 0 ∈ Vi1 but S 0 ∈
/ Vi0 . Since S 0 satisfies
requirements 3, 4, 5 after this step, it also satisfies

these three requirements before this step. Then S 0
must fail to meet at least one of requirements 1 and
2 before this step.
a) If S 0 does not meet requirement 1 before this step,
then S 0 .addr is in the store buffer of processor i
before this step and S 0 .addr is not in this store
buffer after this step. Thus, S 0 .addr must be a.
Since S 0 meets requirement 4 before this step and
S has been executed by processor i before this
step, we know S <mo overwrite(S 0 ). Since S 0
meets requirement 2 after this step, overwrite(S 0 )
is not in Q1 . Since Q1 is derived by popping the
oldest store form Q0 , we know S is not in Q0 .
Since S is in the store buffer before this step,
this contradicts invariant 9. Therefore this case
is impossible.
b) If S 0 does not meet requirement 2 before this step,
then overwrite(S 0 ) is in Q0 but not in Q1 . Then
overwrite(S 0 ) = S. Since S has been executed
by processor i, S 0 will fail to meet requirement 4
after this step. This contradicts with S 0 ∈ Vi1 , so
this case is impossible either.
Now we have proved that Vi0 = Vi1 . Since the WMMDeqSb operation does not change the invalidation
buffer of processor i, this invariant holds for processor i.
2) Processor j (6= i): We consider any store S 0 such
that S 0 ∈ Vj1 but S 0 ∈
/ Vj0 . Since S 0 satisfies
requirements 1, 3, 4, 5 after this step, it also satisfies
these four requirements before this step. Then S 0
must fail to meet requirement requirement 2 before
this step, i.e., overwrite(S 0 ) is in Q0 but not in Q1 .
Then overwrite(S 0 ) = S. According to invariant 8,
we know S 0 is m[a].source. Consider the following
two cases.
a) The store buffer of processor j contains address
a: Since S 0 cannot meet requirement 1, Vj1 = Vj0 .
Since WMM-DeqSb cannot remove any value
from the invalidation buffer of processor j, this
invariant holds.
b) The store buffer of processor j does not contain
address a: In this case, the WMM-DeqSb operation will insert stale value ha, m[a]0 i into the
invalidation buffer of processor j, so the invariant
still holds.
– Invariant 13: The source field of all the newly inserted
stale values in this step are equal to m[a].source0 .
According to invariant 8, m[a].source0 is the youngest
store for a in <mo that is not in Q0 . Since S is the head
of Q0 , we know overwrite(m[a].source0 ) = S. Since S
is not in Q1 , this invariant still holds.
– Invariant 14: Assume ha, vi is the new stale value
inserted into the invalidation buffer of processor j in

•

•

this step. We need to show that for any stale value
ha, v 0 i that is in this invalidation buffer before this
step, v 0 .source <mo v.source. According to invariant 13,
overwrite(v 0 .source) is not in Q0 . Since v.source =
m[a].source0 , according to invariant 8, v.source is the
youngest store for a in <mo that is not in Q0 . Therefore
v 0 .source <mo v.source.
Action 4b: We pop a Reconcile fence F from Q, and
perform a WMM-Rec operation to execute it in the I2 E
model. Assume F is in processor i in the axiomatic
relations. We first prove that F has been mapped before
this step. We prove by contradiction, i.e., we assume F
is not mapped before this step. Consider the state right
before this step. Let I be the next instruction to execute in
processor i in the I2 E model. We know I is mapped and
I <po F . The condition for performing action 4b in this
step says that I can only be a fence or load, so we have
order(I, F ). According to the Inst-Order axiom, I <mo F ,
so I has been popped from Q0 .
1) If I is a fence, since I is in <mo but not in Q0 ,
invariant 6 says that I must be executed, contradicting
our assumption that I is the next instruction to execute.
2) If I is a load, since I is not executed, and I is in <mo ,
and Ik is not in Q0 , invariant 5 says that I must be
in Z 0 . Then this algorithm step should use action 3
instead of action 4a.
Due to the contradictions, we know F must have been
mapped before this step. According to invariant 6, since F
is in Q0 , F must have not been executed in the I2 E model.
Thus, F is mapped to the next instruction to execute in
processor i in the I2 E model.
Now we consider each invariant:
– Invariants 1, 2, 4, 6: These obviously hold.
– Invariants 3, 5, 7, 8, 9, 10: These are not affected.
– Invariants 11, 13, 14: These invariants hold, because
the invalidation buffer of any processor j (6= i) is not
changed, and the invalidation buffer of processor i is
empty after this step.
– Invariant 12: For any processor j (6= i), Vj1 = Vj0 and
the invalidation buffer of processor j is not changed in
this step. Thus, this invariant holds for any processor j
(6= i). We now consider processor i. The invalidation
buffer of processor i is empty after this step, so we need
to show that Vi1 is empty. We prove by contradiction, i.e.,
we assume there is a store S ∈ Vi1 . Since F has been
executed in processor i after this step, requirement 3
says that F <mo overwrite(S). Since F is the head of
Q0 , overwrite(S) must be in Q1 . Then S fails to meet
requirement 2 after this step, contradicting with S ∈ Vi1 .
Therefore Vi1 is empty, and this invariant also holds for
processor i.
Action 4c: We pop a Commit fence F from Q, and perform
a WMM-Com operation to execute it in the I2 E model.

•

Assume F is in processor i in the axiomatic relations.
Using the same argument as in the previous case, we can
prove that F is mapped to the next instruction to execute
in processor i in the I2 E model (before this step). Now
we consider each invariant:
– Invariants 1, 4, 6: These obviously hold.
– Invariants 3, 5, 7, 8, 9, 10, 11, 12, 13, 14: These are
not affected.
– Invariants 2: We prove by contradiction, i.e., we assume
there is store S in the store buffer of processor i before
this step. According to invariant 9, S has been executed
in processor i and is in Q0 . Thus, we have S <po F .
Since order(S, F ), the Ld-Val axiom says that S <mo F .
Then F is not the head of Q0 , contradicting with the
fact that we pop F from the head of Q0 .
Action 4d: We pop a load L from Q. Assume that L
is for address a and is in processor i in the axiomatic
relations. If we add L to Z, then all invariants obviously
hold. We only need to consider the case that we perform
a WMM-Ld operation to execute L in the I2 E model. In
this case, L is mapped before this step. Since L is in
Q0 , according to invariant 5, L must be mapped to an
unexecuted instruction in the I2 E model. That is, L is
mapped to the next instruction to execute in processor i
in the I2 E model. Invariant 4 ensures that L has the same
load address in the I2 E model. We first consider several
simple invariants:
– Invariants 1, 2, 5: These invariants obviously hold.
– Invariants 6, 7, 8, 9, 10: These are not affected.
– Invariant 11: Since the WMM-Ld operation does not
change store buffers and can only remove values from
the invalidation buffers, this invariant still holds.
– Invariants 13, 14: These still hold, because we can only
remove values from the invalidation buffer in this step.
rf

Assume store S −→ L in the axiomatic relations. We prove
the remaining invariants (i.e., 3, 4 and 12) according to
the position of S in <mo .
1) L <mo S: We show that the WMM-Ld can read S
from the store buffer of processor i in the I2 E model.
The Ld-Val axiom says that S <po L. Then S must
have been executed in processor i in the I2 E model
according to invariant 1. Since S is in Q0 , invariant 9
ensures that S is in the store buffer of processor i
before this step.
To let WMM-Ld read S from the store buffer, we
now only need to prove that S is the youngest store
for a in the store buffer of processor i. We prove by
contradiction, i.e., we assume there is another store S 0
for a which is in the store buffer of processor i and
is younger than S. Invariant 10 says that S <po S 0 .
Since S and S 0 are stores for the same address, the
Inst-Order axiom says that S <mo S 0 . Since S 0 is in

the store buffer, it is executed before L. According to
rf
invariant 1, S 0 <po L. Then S −→ L contradicts with
the Ld-Val axiom.
Now we can prove the invariants:
– Invariant 3: This holds because the WMM-Ld operation reads S from the store buffer.
– Invariant 4: This holds because invariant 3 holds after
this step.
– Invariant 12: The execution of L in this step cannot
introduce new stores into Vj for any j, i.e., Vj1 ⊆ Vj0 .
Since there is no change to any invalidation buffer
when WMM-Ld reads from the store buffer, this
invariant still holds.
2) S <mo L: We show that the WMM-Ld operation can
read the value of S from the atomic memory. Since L
is the head of Q0 , S is not in Q0 . According to the
Ld-Val axiom, there cannot be any store for a between
S and L in <mo . Thus, S is the youngest store for a
in <mo that has been popped from Q. According to
invariant 8, the current m[a].source in the I2 E model
is S.
To let WMM-Ld read m[a], we only need to show
that the store buffer of processor i does not contain
any store for a. We prove by contradiction, i.e., we
assume there is a store S 0 for a in the store buffer of
processor i. According to invariant 9, S 0 has executed
in the I2 E model, and S 0 is in Q0 . Thus, we have
S 0 <po L (according to invariant 1), and S <mo S 0 .
rf
Then S −→ L contradicts with the Ld-Val axiom.
Now we can prove the invariants:
– Invariant 3: This holds because the WMM-Ld operation reads S from the atomic memory m[a].
– Invariant 4: This holds because invariant 3 holds after
this step.
– Invariant 12: The execution of L in this step cannot
introduce new stores into Vj for any j, i.e., Vj1 ⊆ Vj0 .
Since there is no change to any invalidation buffer of
any processor other than i, we only need to consider
processor i. The WMM-Ld removes all values for
a from the invalidation buffer of processor i, so
the goal is to show that there is no store for a in
Vi1 . We prove by contradiction, i.e., assume there
is store S 0 for a in Vi1 . Requirement 5 for Vi says
that S <mo overwrite(S 0 ). Since S is the youngest
store for a that is in <mo but not Q0 , overwrite(S 0 )
must be in Q0 . This contradicts with requirement 2.
Therefore, there is no store for a in Vi1 , and this
invariant holds.
By combining Theorems 1 and 2, we prove the equivalence
between the I2 E model and the axiomatic model of WMM.
Theorem 3 (Equivalence). WMM I2 E model ≡ WMM

axiomatic model.
R EFERENCES
[1] L. Lamport, “How to make a multiprocessor computer that
correctly executes multiprocess programs,” Computers, IEEE
Transactions on, vol. 100, no. 9, pp. 690–691, 1979.
[2] P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O.
Myreen, “x86-tso: a rigorous and usable programmer’s model
for x86 multiprocessors,” Communications of the ACM, vol. 53,
no. 7, pp. 89–97, 2010.
[3] SPARC International, Inc., The SPARC Architecture Manual:
Version 8. Prentice-Hall, Inc., 1992.
[4] D. L. Weaver and T. Gremond, The SPARC architecture
manual (Version 9). PTR Prentice Hall Englewood Cliffs,
NJ 07632, 1994.
[5] Alpha Architecture Handbook, Version 4. Compaq Computer
Corporation, 1998.
[6] K. Gharachorloo, D. Lenoski, J. Laudon, P. Gibbons, A. Gupta,
and J. Hennessy, “Memory consistency and event ordering in
scalable shared-memory multiprocessors,” in Proceedings of
the 17th International Symposium on Computer Architecture.
ACM, 1990, pp. 15–26.
[7] S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams,
“Understanding power multiprocessors,” in ACM SIGPLAN
Notices, vol. 46, no. 6. ACM, 2011, pp. 175–186.
[8] S. Flur, K. E. Gray, C. Pulte, S. Sarkar, A. Sezgin, L. Maranget,
W. Deacon, and P. Sewell, “Modelling the armv8 architecture,
operationally: Concurrency and isa,” in Proceedings of
the 43rd Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, ser. POPL 2016.
New York, NY, USA: ACM, 2016, pp. 608–621. [Online].
Available: http://doi.acm.org/10.1145/2837614.2837615
[9] S. Mador-Haim, L. Maranget, S. Sarkar, K. Memarian,
J. Alglave, S. Owens, R. Alur, M. M. Martin, P. Sewell,
and D. Williams, “An axiomatic memory model for power
multiprocessors,” in Computer Aided Verification. Springer,
2012, pp. 495–512.
[10] J. Alglave, L. Maranget, and M. Tautschnig, “Herding cats:
Modelling, simulation, testing, and data mining for weak
memory,” ACM Transactions on Programming Languages and
Systems (TOPLAS), vol. 36, no. 2, p. 7, 2014.
[11] IBM, Power ISA, Version 2.07, 2013.
[12] J. Alglave, A. Fox, S. Ishtiaq, M. O. Myreen, S. Sarkar,
P. Sewell, and F. Z. Nardelli, “The semantics of power and
arm multiprocessor machine code,” in Proceedings of the 4th
workshop on Declarative aspects of multicore programming.
ACM, 2009, pp. 13–24.
[13] J. Alglave and L. Maranget, Computer Aided Verification:
23rd International Conference, CAV 2011, Snowbird, UT,
USA, July 14-20, 2011. Proceedings. Berlin, Heidelberg:
Springer Berlin Heidelberg, 2011, ch. Stability in Weak
Memory Models, pp. 50–66. [Online]. Available: http:
//dx.doi.org/10.1007/978-3-642-22110-1 6

[14] J. Alglave, “A formal hierarchy of weak memory models,”
Formal Methods in System Design, vol. 41, no. 2, pp. 178–
210, 2012.
[15] S. Sarkar, K. Memarian, S. Owens, M. Batty, P. Sewell,
L. Maranget, J. Alglave, and D. Williams, “Synchronising
c/c++ and power,” in ACM SIGPLAN Notices, vol. 47, no. 6.
ACM, 2012, pp. 311–322.
[16] J. Alglave, D. Kroening, V. Nimal, and M. Tautschnig,
“Software verification for weak memory via program transformation,” in Programming Languages and Systems. Springer,
2013, pp. 512–532.
[17] “The risc-v instruction set,” https://riscv.org/.
[18] A. Waterman, Y. Lee, D. A. Patterson, and K. Asanovi,
“The risc-v instruction set manual. volume 1: User-level isa,
version 2.1,” Technical Report UCB/EECS-2016-118, EECS
Department, University of California, Berkeley, May 2014.
[Online]. Available: https://people.eecs.berkeley.edu/∼krste/
papers/riscv-spec-v2.1.pdf
[19] D. Lustig, C. Trippel, M. Pellauer, and M. Martonosi, “Armor:
defending against memory consistency model mismatches
in heterogeneous architectures,” in Proceedings of the 42nd
Annual International Symposium on Computer Architecture.
ACM, 2015, pp. 388–400.
[20] M. H. Lipasti, C. B. Wilkerson, and J. P. Shen, “Value locality
and load value prediction,” ACM SIGOPS Operating Systems
Review, vol. 30, no. 5, pp. 138–147, 1996.
[21] M. M. K. Martin, D. J. Sorin, H. W. Cain, M. D.
Hill, and M. H. Lipasti, “Correctly implementing value
prediction in microprocessors that support multithreading
or multiprocessing,” in Proceedings of the 34th Annual
ACM/IEEE International Symposium on Microarchitecture,
ser. MICRO 34. Washington, DC, USA: IEEE Computer
Society, 2001, pp. 328–337. [Online]. Available: http:
//dl.acm.org/citation.cfm?id=563998.564039
[22] W. J. Ghandour, H. Akkary, and W. Masri, “The potential of
using dynamic information flow analysis in data value prediction,” in Proceedings of the 19th international conference
on Parallel architectures and compilation techniques. ACM,
2010, pp. 431–442.
[23] A. Perais and A. Seznec, “Eole: Paving the way for an effective
implementation of value prediction,” in Computer Architecture
(ISCA), 2014 ACM/IEEE 41st International Symposium on.
IEEE, 2014, pp. 481–492.
[24] A. Perais and A. Seznec, “Practical data value speculation
for future high-end processors,” in High Performance Computer Architecture (HPCA), 2014 IEEE 20th International
Symposium on. IEEE, 2014, pp. 428–439.
[25] S. Owens, S. Sarkar, and P. Sewell, “A better x86 memory
model: x86-tso,” in Theorem Proving in Higher Order Logics.
Springer, 2009, pp. 391–407.

[26] J. Kang, C.-K. Hur, O. Lahav, V. Vafeiadis, and D. Dreyer,
“A promising semantics for relaxed-memory concurrency,”
in Proceedings of the 44th ACM SIGPLAN Symposium on
Principles of Programming Languages, ser. POPL 2017.
New York, NY, USA: ACM, 2017, pp. 175–189. [Online].
Available: http://doi.acm.org/10.1145/3009837.3009850
[27] H.-J. Boehm and B. Demsky, “Outlawing ghosts: Avoiding
out-of-thin-air results,” in Proceedings of the Workshop on
Memory Systems Performance and Correctness, ser. MSPC
’14. New York, NY, USA: ACM, 2014, pp. 7:1–7:6. [Online].
Available: http://doi.acm.org/10.1145/2618128.2618134
[28] S. V. Adve and M. D. Hill, “Weak ordering a new definition,”
in ACM SIGARCH Computer Architecture News, vol. 18, no.
2SI. ACM, 1990, pp. 2–14.
[29] K. Gharachorloo, A. Gupta, and J. L. Hennessy, “Two
techniques to enhance the performance of memory consistency
models,” in Proceedings of the 1991 International Conference
on Parallel Processing, 1991, pp. 355–364.
[30] P. Ranganathan, V. S. Pai, and S. V. Adve, “Using speculative
retirement and larger instruction windows to narrow the
performance gap between memory consistency models,” in
Proceedings of the ninth annual ACM symposium on Parallel
algorithms and architectures. ACM, 1997, pp. 199–210.
[31] C. Guiady, B. Falsafi, and T. N. Vijaykumar, “Is sc+ ilp=
rc?” in Computer Architecture, 1999. Proceedings of the 26th
International Symposium on. IEEE, 1999, pp. 162–171.
[32] C. Gniady and B. Falsafi, “Speculative sequential consistency
with little custom storage,” in Parallel Architectures and Compilation Techniques, 2002. Proceedings. 2002 International
Conference on. IEEE, 2002, pp. 179–188.
[33] L. Ceze, J. Tuck, P. Montesinos, and J. Torrellas, “Bulksc: bulk
enforcement of sequential consistency,” in ACM SIGARCH
Computer Architecture News, vol. 35, no. 2. ACM, 2007, pp.
278–289.
[34] T. F. Wenisch, A. Ailamaki, B. Falsafi, and A. Moshovos,
“Mechanisms for store-wait-free multiprocessors,” in ACM
SIGARCH Computer Architecture News, vol. 35, no. 2. ACM,
2007, pp. 266–277.
[35] C. Blundell, M. M. Martin, and T. F. Wenisch, “Invisifence:
performance-transparent memory ordering in conventional
multiprocessors,” in ACM SIGARCH Computer Architecture
News, vol. 37, no. 3. ACM, 2009, pp. 233–244.
[36] A. Singh, S. Narayanasamy, D. Marino, T. Millstein, and
M. Musuvathi, “End-to-end sequential consistency,” in ACM
SIGARCH Computer Architecture News, vol. 40, no. 3. IEEE
Computer Society, 2012, pp. 524–535.

[39] S. Sarkar, P. Sewell, F. Z. Nardelli, S. Owens, T. Ridge,
T. Braibant, M. O. Myreen, and J. Alglave, “The semantics
of x86-cc multiprocessor machine code,” SIGPLAN Not.,
vol. 44, no. 1, pp. 379–391, Jan. 2009. [Online]. Available:
http://doi.acm.org/10.1145/1594834.1480929
[40] J. R. Goodman, Cache consistency and sequential consistency. University of Wisconsin-Madison, Computer Sciences
Department, 1991.
[41] M. Dubois, C. Scheurich, and F. Briggs, “Memory access
buffering in multiprocessors,” in ACM SIGARCH Computer
Architecture News, vol. 14, no. 2. IEEE Computer Society
Press, 1986, pp. 434–442.
[42] X. Shen, Arvind, and L. Rudolph, “Commit-reconcile and
fences (crf): A new memory model for architects and compiler
writers,” in Computer Architecture, 1999. Proceedings of the
26th International Symposium on. IEEE, 1999, pp. 150–161.
[43] Arvind and J.-W. Maessen, “Memory model = instruction
reordering + store atomicity,” in ACM SIGARCH Computer
Architecture News, vol. 34, no. 2. IEEE Computer Society,
2006, pp. 29–40.
[44] ARM, ARM Architecture Reference Manual, ARMv7-A and
ARMv7-R edition, 2013.
[45] S. V. Adve and K. Gharachorloo, “Shared memory consistency
models: A tutorial,” computer, vol. 29, no. 12, pp. 66–76, 1996.
[46] L. Maranget, S. Sarkar, and P. Sewell, “A tutorial introduction
to the arm and power relaxed memory models,” http://www.
cl.cam.ac.uk/∼pes20/ppc-supplemental/test7.pdf, 2012.
[47] R. Smith, Ed., Working Draft, Standard for Programming
Language C++. http://open-std.org/JTC1/SC22/WG21/docs/
papers/2015/n4527.pdf, May 2015.
[48] H.-J. Boehm and S. V. Adve, “Foundations of the c++
concurrency memory model,” in ACM SIGPLAN Notices,
vol. 43, no. 6. ACM, 2008, pp. 68–78.
[49] M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber,
“Mathematizing c++ concurrency,” in ACM SIGPLAN Notices,
vol. 46, no. 1. ACM, 2011, pp. 55–66.
[50] M. Batty, A. F. Donaldson, and J. Wickerson, “Overhauling
sc atomics in c11 and opencl,” SIGPLAN Not., vol. 51,
no. 1, pp. 634–648, Jan. 2016. [Online]. Available:
http://doi.acm.org/10.1145/2914770.2837637

[37] C. Lin, V. Nagarajan, R. Gupta, and B. Rajaram, “Efficient sequential consistency via conflict ordering,” in ACM SIGARCH
Computer Architecture News, vol. 40, no. 1. ACM, 2012, pp.
273–286.

[51] J. Manson, W. Pugh, and S. V. Adve, “The java
memory model,” in Proceedings of the 32Nd ACM
SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, ser. POPL ’05. New York, NY, USA:
ACM, 2005, pp. 378–391. [Online]. Available: http:
//doi.acm.org/10.1145/1040305.1040336

[38] D. Gope and M. H. Lipasti, “Atomic sc for simple in-order
processors,” in High Performance Computer Architecture
(HPCA), 2014 IEEE 20th International Symposium on. IEEE,
2014, pp. 404–415.

[52] P. Cenciarelli, A. Knapp, and E. Sibilio, “The java memory model: Operationally, denotationally, axiomatically,” in
Programming Languages and Systems. Springer, 2007, pp.
331–346.

[53] J.-W. Maessen, Arvind, and X. Shen, “Improving the java
memory model using crf,” ACM SIGPLAN Notices, vol. 35,
no. 10, pp. 1–12, 2000.
[54] “Wwc+addrs test result in power processors,” http://www.cl.
cam.ac.uk/∼pes20/ppc-supplemental/ppc051.html#toc11.
[55] J. F. Cantin, M. H. Lipasti, and J. E. Smith, “The complexity
of verifying memory coherence,” in Proceedings of the
fifteenth annual ACM symposium on Parallel algorithms and
architectures. ACM, 2003, pp. 254–255.
[56] M. Batty, K. Memarian, S. Owens, S. Sarkar, and P. Sewell,
“Clarifying and compiling c/c++ concurrency: from c++ 11 to
power,” in ACM SIGPLAN Notices, vol. 47, no. 1. ACM,
2012, pp. 509–520.
[57] M. Vijayaraghavan, A. Chlipala, Arvind, and N. Dave,
Computer Aided Verification: 27th International Conference,
CAV 2015, San Francisco, CA, USA, July 18-24, 2015,
Proceedings, Part II. Cham: Springer International Publishing,
2015, ch. Modular Deductive Verification of Multiprocessor
Hardware Designs, pp. 109–127. [Online]. Available:
http://dx.doi.org/10.1007/978-3-319-21668-3 7
[58] D. J. Sorin, M. D. Hill, and D. A. Wood, “A primer on
memory consistency and cache coherence,” Synthesis Lectures
on Computer Architecture, vol. 6, no. 3, pp. 1–212, 2011.
[59] S. C. Woo, M. Ohara, E. Torrie, J. P. Singh, and A. Gupta,
“The splash-2 programs: Characterization and methodological
considerations,” in ACM SIGARCH Computer Architecture
News, vol. 23, no. 2. ACM, 1995, pp. 24–36.
[60] “Splash-2x benchmarks,”
parsec3-doc.htm#splash2x.

http://parsec.cs.princeton.edu/

[61] E. K. Ardestani and J. Renau, “Esesc: A fast multicore
simulator using time-based sampling,” in High Performance
Computer Architecture (HPCA2013), 2013 IEEE 19th International Symposium on. IEEE, 2013, pp. 448–459.

