A Promising Semantics for Relaxed-Memory Concurrency
Viktor Vafeiadis

Derek Dreyer†

Artifactten* Completeeu* Easy toed
Rnt

at e dmemory shared by all threads. To simulate SC semantics on thesearchitectures, one must therefore insert expensive fence instructions
to subvert the efforts of the hardware. Secondly, a number of common compiler optimizations—such as constant propagation—arerendered unsound by a naive SC semantics because they effectively
reorder memory operations. Moreover, SC semantics is stronger (i.e.,
more restrictive) than necessary for many concurrent algorithms.
Hence, languages like Java and C++ have opted instead toprovide relaxed (aka weak) memory models [21, 13], which enable
programmers to demand SC semantics when they need it, but which
also support a range of cheaper memory operations that trade off
strongly consistent and/or well-defined behavior for efficiency.

Despite many years of research, it has proven very difficult to develop a memory model for concurrent programming languages that
adequately balances the conflicting desiderata of programmers, compilers, and hardware. In this paper, we propose the first relaxed
memory model that (1) accounts for a broad spectrum of featuresfrom the C++11 concurrency model, (2) is implementable, in thesense that it provably validates many standard compiler optimizations and reorderings, as well as standard compilation schemes to
x86-TSO and Power, (3) justifies simple invariant-based reasoning,
thus demonstrating the absence of bad “out-of-thin-air” behaviors,(4) supports “DRF” guarantees, ensuring that programmers who use
sufficient synchronization need not understand the full complexities of relaxed-memory semantics, and (5) defines the semantics ofracy programs without relying on undefined behaviors, which is aprerequisite for applicability to type-safe languages like Java.
The key novel idea behind our model is the notion of promises:
a thread may promise to execute a write in the future, thus enablingother threads to read from that write out of order. Crucially, toprevent out-of-thin-air behaviors, a promise step requires a threadlocal certification that it will be possible to execute the promised
write even in the absence of the promise. To establish confidence inour model, we have formalized most of our key results in Coq.

1.1

Criteria for a Programming Language Memory Model

Unfortunately, despite many years of research, it has proven very
difficult to develop a memory model for concurrent programming
languages that adequately balances the conflicting desiderata ofprogrammers, compilers, and hardware. In particular, we would liketo find a memory model that satisfies the following properties:• The model should be implementable, i.e., it should validate common compiler optimizations, as well as standard compilation
schemes to the major modern architectures. To be implementable,
it must justify many kinds of instruction reordering and merging.
• The model should support high-level reasoning principles that

Categories and Subject Descriptors D.1.3 [Concurrent Programming]: Parallel programming; D.3.1 [Programming Languages]:
Formal Definitions and Theory—Semantics

programmers and compiler analyses depend on. At a bare minimum, it should validate simple invariant-based verification,and should provide some “DRF” guarantees [4], ensuring that
programmers who employ sufficient synchronization need notunderstand the full complexities of relaxed-memory semantics.

Keywords Weak memory models; C++11; operational semantics

1.

e

Abstract*

MPI-SWS, Germany{orilahav,viktor,dreyer}@mpi-sws.org

A EC * E* Well Docum v

Seoul National University, Korea{jeehoon.kang,gil.hur}@sf.snu.ac.krstOri Lahav

OPL ** P se * Consi

Chung-Kil Hur ∗alu

Jeehoon KangIntroduction• The model should ideally avoid relying on undefined behavior

to define the semantics of racy programs. This is a prerequisite
for applicability to type-safe languages like Java, in which welltyped programs may contain data races but are neverthelessexpected to have safe, well-defined semantics.
Both Java and C++ fail to achieve some of these criteria.
In the case of Java, the memory model fails to validate anumber of common program transformations performed by real Javacompilers, such as redundant read-after-read elimination and “roach
motel” reordering [26]. Although this problem has been known forsome time, a satisfactory solution has yet to be developed.
In the case of C++, the memory model relies crucially on
undefined behaviors to give semantics to racy programs. Moreover,it permits certain “out-of-thin-air” executions which violate basic
invariant-based reasoning (and DRF guarantees) [7].

What is the right semantics for concurrent shared-memory programs
written in higher-level languages? For programmers, the simplest
answer would be a sequentially consistent (SC) semantics, in which
all threads in a program share a single view of memory and writes
to memory take immediate global effect.
However, a naive SC semantics is costly to implement. First ofall, commodity architectures (such as x86, Power, and ARM) arenot SC: they execute memory operations speculatively or out oforder, and they employ hierarchies of buffers to reduce memory
latency, with the effect that there is no globally consistent view of∗ Corresponding author. † Saarland Informatics Campus.

1.2

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored.
Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, contact
the Owner/Author(s). Request permissions from permissions@acm.org or Publications Dept., ACM, Inc., fax +1 (212)869-0481.

The “Out of Thin Air” Problem

To illustrate the problem with C++, consider these two variants ofthe classic “load buffering” litmus test (with two threads in parallel):a := x;y := 1;

Copyright © held by owner/author(s). Publication rights licensed to ACM.
ACM [to be supplied]. . . $15.00

1

x := y;(LB)a := x;y := a;x := y;(LBd)Here, we assume that all variables are initially 0, and that all
memory accesses are of the weakest consistency level, i.e., they
are compiled down to plain loads and stores at the hardware levelwith no additional synchronization (in C++ this is called “relaxed”).
The question is: should it be possible for these programs to assign 1
to a? In the case of LB, the answer is yes: architectures like Power
and ARM may reorder the write of y before the read of x in the firstthread (since these are accesses to distinct variables), after which a
can be assigned 1 by a standard interleaving execution. In the case of
LBd, however, the answer ought to be no: all the operations simply
copy one variable to another and all are initially 0, so if a could
receive 1, it would come “out of thin air”. No hardware reorderings
or reasonable compiler optimizations will produce this behavior. Ifthey did, it would cause major problems: one would not be able toestablish even basic invariants (such as x = y = 0), and basic sanity
results like the aforementioned DRF theorems would cease to hold.
It is therefore a serious problem that the formal memory model of
C++ allows such out-of-thin-air (OOTA) behavior.
Intuitively, the reason C++ allows OOTA behaviors is that it
is not clear how to distinguish them from acceptable behaviors.
The C++ model formalizes valid executions as graphs of memory
access events (think: partially-ordered traces) subject to a set ofcoherence axioms, and the same coherent event graph that describes
a valid execution of LB in which a receives 1 also describes a valid
execution of LBd in which a receives 1.
Hardware memory models (e.g., Power and ARM) handle thisproblem by taking syntactic dependencies between instructions into
account in determining program semantics. Under such models,the out-of-order execution in LB is valid because the write to y isindependent of the read from x, whereas in LBd such out-of-order
execution is prevented by the syntactic dependency between thetwo instructions. Although this approach is suitable for modeling
hardware, it is too brittle for a language-level semantics because
it fails to validate standard compiler optimizations that remove
syntactic dependencies (see also [7]). As a very simple example,
consider the following variant of LB and LBd:a := x;y := a + 1 − a;x := y;to a memory location x at some point in the future. From the pointof view of other threads, a promise is no different from an ordinary
write: once T has promised to write v to x, other threads can readfrom that write. (In contrast, T cannot read from its own promised
write until T has fulfilled the promise: this is crucial to preserve basic
sanity of the semantics.) Intuitively, promises simulate the effect ofread-write reorderings by allowing write events to be visible to otherthreads before the point at which they occur in the program order.
We must, however, ensure that promises do not introduce bad
OOTA behaviors. Toward this end, we only allow T to promise
to write v to x if it is possible to thread-locally certify that thepromise can be fulfilled in a finite number of steps. That is, wemust show that T will be able to write v to x after some finite
sequence of steps of T ’s execution (i.e., with no help from otherthreads). The certification requirement guarantees absence of bad
OOTA executions by ensuring that T can only promise to write avalue v to x if T could have written v to x anyway.
Returning to the examples from §1.2, it is easy to see how
promises give us the desired semantics:• In LB, the first thread can promise to write 1 to y (since it will

indeed write 1 to y no matter what value is assigned to a), after
which the second thread can read from that promise and write 1
to x. Subsequently, the first thread can execute normally, reading
1 from x and assigning it to a.
• The execution of LBfd may proceed in exactly the same way. The

fact that the write of y depends syntactically on a is irrelevant,because during certification of the promised write of 1 to y, theexpression a + 1 − a will always evaluate to 1.
• By contrast, the OOTA behavior will not be allowed for LBd. Inorder for the first thread to promise to write 1 to y, it would needto certify that it can write 1 to y without promises. But since all
variables are initially 0, this is not possible.
Our model supports all features of C++ concurrency except consume reads and SC accesses. Consume reads are widely considereda premature aspect of the C++11 standard and are currently implemented the same as acquire reads in mainstream compilers. In
contrast, SC accesses are a major feature of C++, and originally
our model included an account of SC accesses as well. However,in the course of trying to mechanize correctness of compilation toPower (§5.3), we discovered that our semantics of SC accesses wasflawed, and this led us to discover a flaw in the C++11 standard as
well! (See [19] for further details.) Thus, a proper handling of SC
accesses remains an open and important problem for future work.
In the rest of the paper, we will flesh out the idea of promises—
as well as the other elements of our model—in layers. We begin
in §2 by presenting the details of our model restricted to relaxed
reads and writes. In §3, we extend this base model further to support
atomic updates (i.e., read-modify-write operations, like CAS). Then,in §4, we scale the model up to handle most features of the C++
memory model. In §5, we present our formal results—validating
many program transformations, compilation to x86-TSO and Power,
DRF theorems, and an invariant-based logic—most of which are
fully mechanized in the Coq proof assistant (totalling about 37K
lines of Coq). In §6, we compare with related work, and in §7, weconclude with discussion of future work.

(LBfd)

Under the hardware models, this LBfd program would be treatedsimilarly to LBd due to the syntactic data dependency, so a could
not receive 1. But even a basic optimizing compiler could triviallytransform LBfd to LB, in which case a could receive 1.
As a result, we still to this day lack a semantics for relaxedmemory concurrency in Java and C++ that corresponds to how
these languages are implemented and that provides sufficient reasoning guarantees to programmers and compiler-writers. Several
proposals have recently been made for how to fix the Java and C++
memory models (some of which are discussed in §6), but none
have been proven to validate the full range of standard optimizations/reorderings performed by Java and C++ compilers and bycommodity hardware like Power and ARM. Furthermore, for mostof the existing proposals, it is known that indeed they do not validate
some important reorderings.
1.3

A “Promising” Semantics for Relaxed Memory

In this paper, we present what we believe is a very promising way
forward: the first relaxed memory model to support a broad spectrumof features from the C++ concurrency model while also satisfying
all three criteria listed in §1.1.
We achieve these ends through a combination of mechanisms(some standard, some not), but the most important and novel idea
for the reader to take away from this paper is the notion of promises.
Under our model, which is defined by an operational semantics,
a thread T may nondeterministically “promise” to write a value v

2.

Basic Model for Handling Relaxed Accesses

In this section, we introduce the key ideas of our memory model, firstby example and then more formally. At first we will only consider
a semantics for fully “relaxed” atomic read and write accesses (inthe sense of C++). This is a natural starting point, since the OOTA
problem is fundamentally about how to give a reasonable semantics
for these relaxed accesses, and the key elements of our solution2

T has observed. Hence, when T reads from a location x, it must
read from a message with a timestamp at least as large as the one
recorded for x in T ’s view. And when T writes to x, it must pick atimestamp strictly larger than the one recorded for x in its view.
Let us see now how our semantics, as explained thus far, alreadysuffices to justify desirable reorderings while ruling out violationsof coherence. First, recall the write-read reordering exhibited by
the “store buffering” SB example above, and let us see how the
behavior can be justified. Initially, assume the memory contains theinitialization messages hx : 0@0i and hy : 0@0i, and both threads
maintain a view of x and y that maps them to 0. When T1 performs
the assignment x := 1, it will choose some timestamp t > 0, add
the message hx : 1@ti to the memory, and update its view of x to t.
But this will have no effect on its view of y or T2 ’s view of x, which
remain at 0. Thus, when T1 subsequently reads y, it is free to read 0.
(And analogously for T2 .)On the flip side, per-location timestamps also explain why thefollowing coherence violation is forbidden.

are easiest to understand in this simpler setting. We will see insubsequent sections how to extend and generalize this base modelto account for a much richer variety of memory operations.
To illustrate our semantics, we will write small programs suchas the following:
x := 1;a := y; // 0

y := 1;b := x; // 0

(SB)As a convention, we write a, b, c for local variables (registers) andx, y, z for (distinct) shared memory locations, and assume that all
variables are initialized to 0. We refer to thread i as Ti . Moreover, inorder to refer to a specific observation of the program, we annotate
the corresponding reads with the values expected to be read (e.g.,in the above program, the comment notation indicates the observed
result that a = b = 0).
2.1

Main Ideas

High-Level Requirements: Reorderings and Coherence Relaxed read and write operations are intended to be compiled down
directly to plain loads and stores at the machine level, so one of
the main requirements of our semantics is that it be at least as
permissive as commodity hardware. Toward this end, our semantics
must justify reordering of independent memory operations (i.e.,
operations that access distinct locations), since the more weakly
consistent architectures (like ARM) may potentially perform such
reorderings. There are four such classes of reorderings—write-read,
write-write, read-read, and read-write—and in §5 we will proveformally that our semantics justifies all of them.
On the other hand, it is also important that our semantics not be
unnecessarily weak. In particular, all the existing implementations of
C++, even for weaker architectures like Power and ARM, guarantee
at a bare minimum a property we call per-location coherence (akaSC-per-location). Per-location coherence says that, even thoughthreads may observe writes to different locations in different orders,
they must observe writes to the same location in a single totalorder (called the “modification order” in C++ lingo). In addition to
being supported by hardware, per-location coherence is preservedby common compiler optimizations as well. Hence, we want oursemantics of relaxed accesses to guarantee it. (In §4.3 we will
present an even weaker mode of accesses that does not provide
full per-location coherence.)

x := 1;a := x; // 2

x := 2;b := x; // 1

(COH)

Here, the two writes to x must be totally ordered. Suppose, without
loss of generality, that the x := 1 was written at timestamp 1 andx := 2 at timestamp 2. Then, although T1 may read value 2, T2
cannot read 1, because 1 was written at a smaller timestamp thanthe one that T2 already recorded in its view when it wrote x := 2.
One subtle point is that, when writing to a location x, a thread
T may select any unused timestamp t larger than the one recorded
in its view of x, but t need not be globally maximal. That is, t may
be smaller than the timestamp that another thread has already used
for a write to x. This freedom is in fact crucial in order to permit
write-write reorderings, as exemplified by the following test case:x := 2;y := 1;a := y; // 2

y := 2;x := 1;b := x; // 2

(2+2W)

To get the desired weak outcome, the writes of x := 1 and y := 1
must pick smaller timestamps than the x := 2 and y := 2 writes,
respectively, but at least one of the 1-writes must be executed after
the 2-write to the same location. Thus, it is essential to be able towrite using a timestamp that is not globally maximal.

Operational Semantics with Timestamps In contrast to the C++
memory model, which relies on declarative semantics over event
graphs, ours employs a more standard SC-style operational semantics for concurrency, in which the executions of different threads arenondeterministically interleaved. However, in order to account for
weak memory behaviors, we use a more elaborate memory representation than the standard SC semantics does. Instead of being aflat map from addresses to values, our memory records the set of all
writes ever performed. It may help to think of writes as messages,
and memory as a message pool which grows monotonically. When athread T reads from a location x, it need not read “the latest” write
to x, since there is no shared understanding among threads of what
the latest write is. The thread T thus retains flexibility in terms ofwhich message it reads, but we must place some restrictions on thisflexibility in order to guarantee per-location coherence.
Specifically, we totally order the writes to each location by attaching a (unique) timestamp to each write message. Thus, messages
are triples of the form hx : v @ti (where x is a location, v a value,
and t a timestamp). (The modification order for a location x is thus
implicitly derivable from the order of timestamps on x’s messages.)
In addition, for each thread T , we keep track of a map from locations
x to the largest timestamp of a write to x that T has observed or
executed. We refer to this map as T ’s view of memory, and one canthink of it as recording the set of most recent write messages that

Promises Unfortunately, our timestamp semantics alone does not
suffice to explain read-write reorderings, as exemplified by the (LB)
and (LBfd) programs from §1.2. It is precisely these reorderings
that motivate our introduction of promises.
As explained in §1.3, a thread T may at any point promise towrite x := v at some timestamp t (provided that t is greater than T ’s
current view of x). This promise is treated to a large extent like an
actual write operation. In particular, it adds a new message hx : v @ti
to memory, which may then be read by other threads. However,in order to make such a promise, T must thread-locally certify
it—that is, T must demonstrate that it will be able to fulfill thispromise (writing x := v at timestamp t) in a finite number of threadlocal steps. Certification is needed to guarantee plausibility of thepromise, but crucially, there is no requirement that the specific steps
of execution taken during certification must match the subsequent
steps of actual execution. Indeed, we already witnessed this with the(LB) and (LBfd) executions, where T1 read x = 0 during the initialcertification of its promised write to y, but read x = 1 during theactual execution.
Let us now briefly touch on a few technical points concerning
the interaction of promises and timestamps.
First of all, it is important that T cannot directly read its own
promises, because this would violate per-location coherence: forexample, the single-threaded program a := x; x := 1 would be able3the minimum element. A timemap is a function T : Loc → Time.
The order ≤ is extended pointwise to timemaps.

to return a = 1! Note that we do not need to explicitly enforce thisrestriction—it just falls out from our rules concerning timestamps.
In particular, if T were to promise hx : v @ti, and then were to readfrom its own promise, then T ’s view of x would be updated to t,
and there would be no way for T to subsequently fulfill the promise
because it would have to pick a timestamp strictly greater than twhen performing the assignment x := v.
That said, it is possible for T to read its promised value indirectly
via another thread, as in the LB and LBfd programs. It may evenread the promised value from the same location where it promised
to write it, as in the following example [18].
a := x; // 1
x := 1;y := x;x := y;Programming Language To keep the presentation abstract, we
do not fix a particular programming language; we simply consider
each thread i as a transition system with a set of states Statei , initialstate σi0 ∈ Statei and final state σifinal ∈ Statei . Intuitively, thesestates store the values of the local registers and the program counter.
Transitions are labeled: the label R(x, v) corresponds to a transition
that reads the value v from location x, and W(x, v) denotes a writeof the value v to x, while local transitions that do not access thememory are labeled with “Silent”. We assume receptiveness of thetransition systems—whenever an R(x, v)-transition is possible froma state σi , so is an R(x, v 0 )-transition for every value v 0 —and thatthey only get stuck in the σifinal states.

(ARM-weak)This outcome can be explained by T1 promising hx : 1@2i, thenT2 reading x = 1 and storing it to y, and T3 reading y = 1 andwriting x := 1 at timestamp 1, which T1 can read before fulfillingits promise. Such behavior, strange though it may seem, is actually
allowed (though not yet observed) by the ARM memory model [11].
Last but not least, we wish to ensure that promises do not lead to
impossible situations later down the road, i.e., that making a promise
cannot cause the execution of a program to get stuck. The threadlocal certification that accompanies a promise step goes some way
toward ensuring this progress condition, but it is not enough. We
also amend the semantics in the following two ways:

Messages A message m is a tuple hx : v @ti, where x ∈ Loc,v ∈ Val and t ∈ Time. We denote by m.loc, m.val, and m.t thecomponents of a message m. Two messages m and m0 are called
disjoint, denoted m # m0 , if m.loc 6= m0 .loc or m.t 6= m0 .t.
Two sets M and M 0 of messages are called disjoint, denoted
M # M 0 , if m # m0 for every m ∈ M and m0 ∈ M 0 .
Memory A memory is a pairwise disjoint finite set of messages.
A message m may be (additively) inserted into memory M if m isdisjoint from every message in M . Formally, the additive insertionA
M ←m is given by M ∪ {m} and is only defined if M #{m}.

1. Every step a thread takes, it must re-certify all its outstandingpromises to make sure they can still be fulfilled. To see why,
consider a possible execution of the following program:a := x;x := 1;Thread States and Configurations A thread state is a triple
TS = hσ, V, P i, where σ is the thread’s local state, V is a timemap
representing the thread’s view of memory, and P is a memory thatkeeps track of the thread’s outstanding promises. We denote by
TS .st, TS .view, and TS .prm the components of a thread state
TS . In turn, a thread configuration is a pair TC = hTS , M i, where
TS is a thread state and M is a memory, called the global memory.
Note that we will always have TS .prm ⊆ M .
Figure 1 shows the five reduction rules for thread configurations.
The SILENT rule handles the case when the program performs somelocal computation that does not affect memory. The READ rule
handles the case when the program reads from a location x. The rulenondeterministically selects some message m in the memory, whosetimestamp is greater than or equal to the timestamp recorded for x
in the thread’s view, and returns its value; it also updates the thread’sview of x to the timestamp of m. The WRITE rule handles thecase when the program writes to location x. It extends the memory
with a new message for x, whose timestamp t is greater than the
one recorded for x in the thread’s view, and it updates the thread’sview of x to match t. The PROMISE rule extends the memory andthe thread’s promise set with an arbitrary new message m, whosetimestamp is not already present in the memory. (The promise
certification is handled separately, as described below.) Finally, the
FULFILL rule is similar to the WRITE rule, except that instead of
adding a message to the memory, it removes an appropriate message
from the thread’s promise set P .
We note that the WRITE rule is redundant; we merely included it
to improve readability. Any application of WRITE can be simulated
by first promising the appropriate message with the PROMISE ruleand then immediately fulfilling the promise with the FULFILL rule.
As we have already mentioned, we have to restrict thread executions so that all promises a thread makes are fulfillable. Thread
configurations satisfying this property are called consistent. Formally, a thread configuration hTS , M i is consistent if hTS , M i −→∗hTS 0 , M 0 i for some TS 0 and M 0 such that TS 0 .prm = ∅. Noticethat in the certification of a promise, it is formally possible to makefurther promises. Since, however, in the end all such promises mustbe fulfilled, it is useless to make such promises. (A proof of thisproperty is included in our formal development.)

x := 2;

Suppose that T1 (for no particularly good reason) promiseshx : 1@1i. At first, this is easy to certify: T1 can read theinitial value of x (the message hx : 0@0i), and then performthe assignment x := 1 picking timestamp 1. Suppose thenthat T2 picks the timestamp 2 when performing x := 2. If
at this point in the execution T1 were permitted to read themessage hx : 2@2i, it would have the effect of bumping up
T1 ’s view of x to timestamp 2, which would prevent it from
subsequently fulfilling its promise. It is thus crucial that T1
not be allowed to read x = 2 (in this particular execution),and indeed our semantics will not allow it to do so because
the re-certification check would fail. As the example illustrates,
promises can restrict a thread’s future nondeterministic choices
concerning the messages it reads.
2. We require the total order on timestamps to be dense (e.g.,choosing timestamps to be rational numbers), so that there
is always a place to put intermediate writes before a promise.
Consider, for example, the following program:
x := 1;x := 2;x := 3;Here, T1 may promise hx : 2@2i—when validating this promise,
T1 might write hx : 1@1i before writing hx : 2@2i. If, however,T2 subsequently writes hx : 3@1i before T1 has actually written
x := 1, then T1 can no longer pick 1 as a timestamp for
x := 1. To make progress here, T1 needs a timestamp for x := 1strictly between 0 and 2, and 1 is already taken. By requiring
the timestamp order to be dense, we ensure that there is always
some free timestamp (e.g., 1.5) that T1 can use.
2.2

Formal Definition

We now define our model for relaxed accesses formally. Let Loc be
the set of memory locations, Val be the set of values, and Time be an
infinite set of timestamps, densely totally ordered by ≤, with 0 being

4

( THREAD : READ )R(x,v)( THREAD : SILENT )Silent( THREAD : WRITE )0

σ −−−−→ σ
hx : v@ti ∈ M
V (x) ≤ t
V 0 = V [x 7→ t]hhσ, V, P i, M i −→ hhσ 0 , V 0 , P i, M i0

σ −−−→ σhhσ, V, P i, M i −→ hhσ 0 , V, P i, M i

W(x,v)

A
σ −−−−→ σ 0
M 0 = M ←hx : v@ti
V (x) < t
V 0 = V [x 7→ t]hhσ, V, P i, M i −→ hhσ 0 , V 0 , P i, M 0 i( THREAD : FULFILL )( THREAD : PROMISE )AA
M 0 = M ←m
P 0 = P ←mhhσ, V, P i, M i −→ hhσ, V, P 0 i, M 0 i

W(x,v)

σ −−−−→ σ 0

hx : v@ti ∈ P
P 0 = P \ {hx : v@ti}
V (x) < t
V 0 = V [x 7→ t]hhσ, V, P i, M i −→ hhσ 0 , V 0 , P 0 i, M i( MACHINE STEP )hTS(i), M i −→+ hTS 0 , M 0 i
hTS 0 , M 0 i is consistenthTS, M i −→ hTS[i 7→ TS 0 ], M 0 i

Figure 1. Operational semantics for the simplified model handling only relaxed read and write accesses.
Machine States A machine state MS = hTS, M i consists of afunction TS assigning a thread state to every thread, and a (global)
memory M . The initial state MS0 (for a given program) consistsof the function TS 0 mapping each thread i to its initial state σi0 ,a current timestamp of 0 for every location, and an empty set ofpromises; and the initial memory M 0 that has one initial message
hx : 0@0i for each location x. A machine takes a step (see the last
rule in Figure 1) whenever a thread can take several steps to someconsistent configuration. Note that we allow multiple thread steps in
one machine step. This is convenient in our proofs, and can reduce
the number of certifications during an execution of a program.
Finally, we can easily show that a machine never gets stuck
unless each thread i has reached hσifinal , V, ∅i for some view V .
For non-final states, progress follows from the receptiveness andprogress assumptions about the programming language, together
with the invariant that no thread has a higher view of any x thanthe highest timestamp for x in memory. Another crucial invariant is
consistency: the MACHINE STEP rule demands that each machine
step taken by a thread must preserve consistency of the thread’s own
configuration, and it implicitly preserves the consistency of otherthreads’ configurations as well, since they are free to ignore any new
messages the thread has added. When all threads reach their final
states, consistency implies they must have no promises left to fulfill.

3.

x may not be assigned timestamps in between them. In the example
above, if both of the updates were to increment x from 0 to 1, thewrite timestamp for one of the updates would have to come between
the read and write timestamps for the other update.
To enforce this restriction, we extend messages to store acontinuous range of timestamps rather than a single timestamp.
Thus, messages are now tuples of the form hx : v @(f, t]i wherex ∈ Loc, v ∈ Val, and f, t ∈ Time satisfying f < t or f = t = 0.
We write m.from and m.to to denote the f and t components ofa message m. Intuitively, m can be thought of as reserving thetimestamps in the range (m.from, m.to]; among these, m.to is the“real” timestamp of m, but the remaining timestamps in the range
are reserved so that other messages cannot use them. Timestamp
reservation is reflected in the following revised definition of message
disjointness, which enforces that disjoint messages for the same
location must have disjoint ranges:
hx : v @(f, t]i # hx0 : v 0 @(f 0 , t0 ]i ,x 6= x0 ∨ t ≤ f 0 < t0 ∨ t0 ≤ f < t
With timestamp reservation, we can easily ensure that the write
timestamp of an update is adjacent to its read timestamp in themodification order. Formally, we will say two messages m and
m0 are adjacent, denoted Adj(m, m0 ), if m.loc = m0 .loc andm.to = m0 .from. In defining the semantics of updates, we willthen insist that the message that the update inserts into memory must
appear adjacently after the message that it reads from. This suffices
to guarantee the correct outcome in the Par-Inc program above.
Although the introduction of timestamp reservation enables us toeasily model updates, it creates a complication for promises, namelythat timestamp reservations may invalidate the promise certifications
already performed by other threads. Consider, for example, thefollowing program:

Supporting Atomic Updates

In this section, we extend our basic model for relaxed accesses
to also handle (relaxed) atomic update—aka read-modify-write(RMW)—instructions, such as fetch-and-add and compare-andswap. Updates are essential as a means to implement synchronization (e.g., mutual exclusion) between threads, but this also makes
them tricky to model semantically. In particular, a successful update
operation performed by one thread will often have the effect of“winning a race” and hence blocking (previously possible) update
operations performed by other “losing” threads. This stands in contrast to the updates-free fragment in §2, in which threads are free
to ignore the messages of other threads. Thus, to extend our model
to support updates, we must ensure that threads performing updates
cannot invalidate the already-certified promises of other threads.
An update is an atomic composition of a read and a write to
the same location x. However, unlike under SC, atomicity requires
more than just avoiding interference of other threads between thetwo operations. Consider the following example (taking FAA(x, 1)
to be an atomic fetch-and-add of 1 to x, which returns the value ofx before the increment):
a := FAA(x, 1);

b := FAA(x, 1);

a := x; // 1
b := FAA(z, 1); // 0
y := b + 1;

x := y;FAA(z, 1);(Upd-Stuck)

This behavior ought to be allowed, since hardware could reorder
the read of x after the independent accesses to z and y. To produce
this behavior, following our semantics from the previous section,
T1 could promise to write y := 1 because it can thread-locallycertify that the promise can be fulfilled (the certification will involve
updating z from 0 to 1). If, however, T3 then updates z from 0 to 1,
that will mean that T1 can no longer perform the update it needs tofulfill its promise, and its execution will eventually get stuck.
To avoid such stuck executions, we strengthen the check performed by promise certification, i.e., the consistency requirementon thread configurations. We require that each thread’s promises are
locally fulfillable not only in the current memory, but also in any
future memory, i.e., any extension of the memory with additional
messages. This quantification over future memories ensures thatthread configurations remain consistent whenever another thread
performs an execution step, and thus the machine cannot get stuck.

(Par-Inc)

Atomicity ensures that it is not possible for both threads to increment
x from 0 to 1 (we must either get a = 1 or b = 1). To obtain this, we
require that the read timestamp of the update (i.e., the timestamp of
the write message that the update reads from) immediately precede
its write timestamp (i.e., the timestamp of the write message that the
update generates) in x’s modification order, and that future writes to5

First, we refine each thread’s view. Rather than having a single
view of which messages it has observed, a thread now has threeviews: V = hcur, acq, reli. We denote by V.cur, V.acq and V.rel
the components of a thread view V. A thread’s current view, cur,is as before: it records which messages the thread has observed
and restricts which messages a read may return and a write may
create. Its release view, rel, records what the thread’s cur view
was at the point of its last release fence. Dually, its acquire view,acq, records what the thread’s cur view will become if it performs
an acquire fence. Consequently, the views are related as follows:rel ≤ cur ≤ acq.
Second, we extend write messages to record a message view R,
which records the release view of the writing thread at the time thewrite occurred (updated to include the write itself). Thus, a message
now takes the form m = hx : v @(f, t], Ri, where R(x) = t. We
write m.view for the message view of m.
During execution of relaxed accesses, a thread’s views drift apart.
When a thread reads a message, it incorporates the message’s view
into the thread’s acq view, but not into its cur or rel views. Whena thread writes a message, it uses the thread’s rel view as the basis
for the message’s view, but only incorporates the message itself into
the thread’s cur and acq views, not its rel view.
Fence commands bring these diverging views closer to one
another. Specifically, an acquire fence increases the thread’s curview to match its acq view, thereby ensuring that the thread is up todate with respect to views of all the messages read before the fence.
Symmetrically, a release fence increases the thread’s rel view tomatch its cur view, thereby ensuring that the views of all messages
the thread writes after the release fence will contain the messages
observed before the fence.
Returning to the MP+fences program, suppose that T1 emitted
messages hx : 1@(_, tx ], _i and hy : 1@(_, ty ], Ry i. Then, T1 ’s curview before the release fence maps x to tx . The fence then updates
T1 ’s rel view to match its cur view, so that the message viewaccompanying the subsequent write to y will map x to tx as well.
(Without the release fence, this message view would map x to 0.) On
T2 ’s side, the read of y = 1 updates T2 ’s cur view to [x@0, y @ty ],and its acq view to [x@tx , y @ty ]. The acquire fence then updates
T2 ’s cur view to match its acq view, and hence the subsequent readof x must see the x := 1 write. If either the release or the acquire
fence were missing, then T2 ’s cur view at the read of x would havebeen [x@0, y @ty ], allowing it to read x = 0.

( THREAD : FULFILL UPDATE )U(x,vr ,vw )σ −−−−−−−→ σ 0
hx : vr @(fr , tr ]i ∈ M
mw = hx : vw @(tr , tw ]imw ∈ PP 0 = P \ {mw }V (x) ≤ tr
V 0 = V [x 7→ tw ]hhσ, V, P i, M i −→ hhσ 0 , V 0 , P 0 i, M i

Figure 2. Additional rule for updates (all other rules are as before
except all messages hx : v @ti are replaced by hx : v @(f, t]i).
Returning to the above example, T1 will not be permitted topromise to write y := 1 in the initial state, precisely because thatpromise could not be fulfilled under an arbitrary future memory(e.g., one containing the update of T3 , as we showed). T1 may,
however, first promise hz : 1@(0, 1]i, reserving the time range fromthe initialization of z up to its increment. T1 can fulfill that promise,
because no future extension of the memory will be able to add
any messages in between. After making that promise, T1 may thenpromise, e.g., hy : 1@(3, 4]i, which it can now fulfill under any
extension of the memory. With these promises in place, T3 will be
prevented from updating z from 0 to 1; it will be forced to update z
from 1 to 2, which will not block the future execution of T1 .
Our quantification here over all future memories may seem rather
restrictive in that it completely ignores what can or cannot happen
in a particular program. That said, we find it a simple and natural
way of ensuring “thread locality”. The latter is a guiding principle
in our semantics, according to which the set of actions a thread cantake is determined only by the current memory and its own state.
Formally, we say that Mfuture is a future memory of M if
AAA
Mfuture = M ←m1 ←... ←mn for some n ≥ 0 and messages
m1 , ... , mn . And we now say a thread configuration hTS , M i is
consistent if, for every future memory Mfuture of M , there exist TS 0
and M 0 such that hTS , Mfuture i →− ∗ hTS 0 , M 0 i and TS 0 .prm = ∅.
Finally, we extend the operational semantics for thread configurations with one additional rule for update fulfillment shown in
Figure 2. This rule forces its write to be adjacent in modification
order to its read. As with ordinary writes, a normal (non-promised)
update step can be simulated by a promise step immediately followed by fulfillment. Note that the other rules remain exactly thesame; they simply ignore the m.from component of messages m.

4.

Full Model

Interaction with Promises Promises (like every other message)
now carry a view, and threads reading a promise are subject tothe same constraints as if they were reading a normal message.
In particular, after reading a promise and performing an acquire
fence, a thread can only read messages with timestamp greater thanor equal to the view carried in the promise message. In order toavoid cases where execution gets stuck, we must ensure that somemessage can be read for every location. Thus we require that theview attached to a promise message includes only timestamps ofmessages that exist in memory at the time the promise is made.
Going back to MP+fences, note that T1 cannot promise y := 1
before performing x := 1. Indeed, because of the release fence,the view in the y := 1 message must include the message that will
be produced for the x := 1 assignment, but at the beginning theonly message for x in memory is the initial one (at timestamp 0).
Hence, release fences effectively serve also as barriers for promises.
We find it convenient to explicitly require this in our semantics:
whenever a release fence is performed, the set of promises of theexecuting thread must be empty. This may seem restrictive, but notethat the main reason for introducing promises was to allow readwrite reorderings, as in the LB example of §1.2. If there is a releasefence in between the read and write, then the reordering is no longer
possible, and thus our motivation for promising the write is void.

In this section, we extend the basic model of §2-3 to handle all thefeatures of the C++ concurrency model except SC accesses andconsume reads.
4.1

Release/Acquire Synchronization

Release/Acquire Fences A crucial feature of the C++ model is theability for threads to synchronize using memory fences or stronger
kinds of atomic accesses. Consider the message-passing test case:x := 1;fence-rel;
y := 1;a := y; // 1
fence-acq;
b := x; //6= 0(MP+fences)

The release fence between the writes, together with the acquire
fence between the reads, prevents the weak behavior of the example(i.e., that of returning a = 1 and b = 0). Roughly speaking, theC++ model forbids this behavior by requiring that whenever a read
before an acquire fence reads from a write after a release fence, thetwo fences synchronize, which in turn means that any write that
happens-before the release fence must be visible to any read that
happens-after the acquire fence. So, if T2 reads y = 1, then after
the acquire fence it must read x = 1.
To implement this semantics, we extend our model in two ways.

6

Release/Acquire Accesses In addition to release and acquire
fences, C++ offers a more fine-grained way of achieving synchronization, via acquire reads and release writes. Intuitively speaking,an acquire read is a relaxed read followed by an acquire fence,
whereas a release write is a release fence followed by a relaxed
write, with the restriction that these fences induce synchronization
only on the location of the access. For example, in the following
program,1 only the second thread synchronizes with the first one.
x := 1;yrel := 1;z := 1;a := yacq ; // 1
b := x; //6= 0

possible under the usual compilation of release writes to Power
and ARM (using a lwsync/dmb_sy fence in the first thread).2 Moregenerally, our model forbids promises over release writes to thesame location.
In the second variant (LBa), we allow the promise of y := 1and thus the a = 1 outcome. The reason is that we want to enableoptimizations that result in the elimination of an acquire read andthus remove the reordering constraints of the acquire. Consider, forexample, the following program transformation:c := zacq ; // 1
d := x; // 0a := x; // 2
y := 1;b := yacq ;y := 2;Hence, b must get the value 1, while d may get 0.
To model these accesses, we treat the rel view of each thread
not as a single view, but rather as one separate view per location,
recording the thread’s current view at the latest release fence orrelease write to that location. Thus, when a thread performs a releasewrite to location x, we update its release view of x to match its curview, while a release fence effects this update on the release viewsof all locations. Then, a write to x (either release or relaxed) will use
the release view of x (newly updated, if it is a release write) to form
the view of the write message, and an acquire read will incorporate
the message’s view into the reading thread’s current view.
In the example above, at the end of T1 ’s execution, its threadview has rel(y) = [x@tx , y @ty , z @0], whereas rel(z) =[x@0, y @0, z @tz ]. As a result, the yacq read increases T2 ’s curview to [x@tx , y @ty , z @0], which forces it to then read x = 1,
whereas the zacq read increases T3 ’s cur view to [x@0, y @0, z @tz ],which allows it to later read x = 0.

FAA(y, 1);;

x := y;(LBa0 )

which may in effect reorder the y := 2 write before the a := x readeven though there is an acquire read in between (by first replacing
yacq with 1 and then reordering a := x past both writes to y). Thus,
our semantics has to allow promises over acquire actions. Note that
there is no need to do so for release writes, because release writes
cannot simply be eliminated in this way.
4.2

Sequentially Consistent (SC) Fences

We now extend the model with sequentially consistent (SC) fences,whose purpose is to allow the programmer to enforce strong ordering
guarantees among memory accesses. In particular, full sequentialconsistency is restored if an SC fence is placed between every twoshared memory accesses of a program.3
To handle SC fences, we extend our machine state with a global
timemap S, which records the latest messages written by any thread
before an SC fence. When a thread T executes an SC fence, in
addition to the effect of both an acquire and a release fence, T
increases both its cur view and the global timemap to the maximumof the two. Consider the following variant of the SB example:

Release Sequences Using the per-location release views, we canstraightforwardly handle C++-style release sequences (following
the definition of release sequences given in [28]). In C++, an acquire
read synchronizes with a release write w to x not only if it reads
from w but also if it reads from a write in w’s release sequence. The
release sequence of w is inductively defined to include all the samethread writes/updates to x after w, as well as all updates readingfrom an event in the release sequence of w. For example, in thefollowing program, the yacq synchronizes with the yrel := 1 because
it reads from the FAA(y, 1), which in turn reads from the y := 2.
x := 1;yrel := 1;
y := 2;x := y;y := 1;b := 1;y := 2;a := x; // 2

x := 1;fence-sc;
a := y; // 0

y := 1;fence-sc;
b := x; //6= 0(SB+fences)

Here, the current views of the two threads just before their SC
fences are [x@tx , y @0] and [x@0, y @ty ], respectively, while theglobal view is [x@0, y @0]. If the fence of T1 is executed first, it
will update S to [x@tx , y @0]. So, when the fence of T2 is executed,
both its cur view and S become [x@tx , y @ty ], from which point
onwards T2 must read x = 1.

a := yacq ; // 3
b := x; //6= 0

Our operational semantics already handles the case of reading froma later write of the same thread, because the thread’s release viewfor y is included in the message’s view. To handle the updates that
read from elements of the release sequence, we insist that the viewof the write message of an update must incorporate the view of theread message of the update. Thus, in this example, the views of all
the y messages contain x@tx , and hence T3 must read x = 1.

4.3

“Plain” Non-Synchronizing Accesses

Both C++ and Java provide some form of non-synchronizing accesses, i.e., accesses that are meant to be used only for non-racy
data accesses (C++’s non-atomic accesses and Java’s normal accesses). Such accesses can never achieve synchronization, even together with fences. Consequently, compilers are free to reorder nonsynchronizing reads across acquire fences, and to reorder releasefences across non-synchronizing writes. These non-synchronizing
accesses, which we refer to as plain accesses, are easily supported
in our model. The difference from relaxed accesses is simple: aplain read from a message m should not incorporate m.view into
the thread’s acq view; and a message m produced by a plain write
should only carry the 0-view (i.e., ⊥ in the lattice of views). Moreover, plain writes can be promised even beyond a release fence or arelease write to the same location.

Promises Over Release/Acquire Accesses We finally point out
another delicate issue related to the interaction between promises
and release/acquire accesses. Consider the following variants of the
LB example:
a := x; //6= 1
a := xacq ; // 1
x := y; (LBr)
x := y; (LBa)
yrel := 1;
y := 1;In the first variant (LBr), the promise of yrel := 1 should be
forbidden for the same reason that a promise over a release fence
is forbidden, and hence the specified behavior is disallowed. We
note that this behavior is possible under the C++ model, but is not

2 Moreover, we observe that even the C++ model forbids this outcome, if we

additionally make the read of y in the second thread into a consume read(which is supposed to be compiled exactly as a relaxed read, but preserving
syntactic dependencies).
3 In this regard, our semantics is stronger than the C++ model [6], whichfails to validate this basic property, and follows Lahav et al. [17, 19] instead.

1 In this and in following code snippets, we annotate non-relaxed accesses

with their access mode; all non-annotated accesses are relaxed.

7

can be merged to FAA(y, 2), and then the whole if-then-else statement can be replaced by FAA(y, 2). Nevertheless, the model described so far forbids this behavior. Indeed, clearly, an execution
obtaining this behavior must start with T1 promising hy : 2@(f, t]i.
Since this promise must be certified under an arbitrary future memory, T1 must pick f = 0 (or else, it cannot fulfill its promise for amemory that includes, say, hy : 42@(0, 5]i). Then, T2 can read thepromise and add a message of the form hx : 2@(_, tx ]i to the memory. Now, T1 would like to read this message. However, if it does so,
it will not be able to fulfill its promise hy : 2@(0, t]i, simply because
there is no available timestamp interval in which it can put the firsty = 1 message. To solve this, we allow threads to split their own
promises in two pieces, keeping the original promise with the same
m.to value. For the example above, T1 could proceed by splitting
its promise hy : 2@(0, t]i into hy : 1@(0, t/2]i and hy : 2@(t/2, t]i,
reading the message hx : 2@(_, tx ]i and fulfilling both promises.

Besides the reordering mentioned above, compilers can (anddo) utilize further the assumption that some accesses are intended
to be non-racy. Indeed, assuming two non-racy reads, a compiler
may reorder them even if they are reading the same location. In a
broader context, it may pave the way to further optimizations (e.g.,
a compiler may prefer to unconditionally optimize a := x; b := ∗p;c := x to b := ∗p; a := x; c := a, without the burden of analyzing
whether the pointer p points to x or not). Since we followed C++’sassumption of full per-location coherence for our relaxed accesses,
the reordering of two reads from the same location is unsound forthem. Concretely, consider the following example:
x := 1;x := 2;a := x; // 2
b := x; // 1;

x := 1;x := 2;b := x; // 1
a := x; // 2

The target program obviously allows the specified behavior, while
the source does not. Fortunately, it is not hard to adapt our plain
accesses to provide only partial per-location coherence (in C++11
terms, dropping “coherence-RR” for plain accesses), consequently
allowing this reordering. The idea is to extend the notion of a view
V —both message views R and the three component views of athread (cur, acq, rel)—from being a single timemap to a pair oftimemaps: a “normal” one (V.rlx) as before, and one for plain
accesses (V.pln). The V.pln timemap is generally smaller than
the normal timemap (V.pln ≤ V.rlx), and restricts the possible
timestamps available to plain reads. A plain read from a message mwith location x and time t only consults this new timemap, checking
that cur.pln(x) ≤ t, and only updates cur.rlx(x) to include t. A
plain write, on the other hand, cannot pick a timestamp smaller thancur.rlx(x) (since we do maintain the other coherence properties
besides “coherence-RR”).
Importantly, we do not exploit “catch-fire” semantics (à la C++)to accommodate our plain accesses, but rather give a well-definedsemantics to arbitrary racy programs. In addition, we note that it iseasy to decouple the two weaknesses of plain accesses compared torelaxed ones, by introducing a middle access mode that allows
synchronization (together with release and acquire fences) but
supports only partial per-location coherence.

Lower The second form of promise adjustment is lowering of
the promised message’s view. Note that by promising a message
carrying a high view, a thread places more restrictions on the readersof that promise. Thus, changing the view of a promise m to a viewR0 ≤ m.view can never cause any harm. Technically, including
this option simplifies our simulation arguments used to prove thesoundness of program transformations, by allowing us to have asimpler simulation relation between the source and target memories.
More generally speaking, it allows us to prove and use the following
natural property: if all the views included in some machine state
MS (in its memory’s messages and its threads’ views) are less thanor equal to all views in another machine state MS0 , then every
behavior of MS0 is also a behavior of MS.
4.6

pln @ rlx @ ra
We use o as a metavariable for access mode. The programming
language is modeled by a transition system whose transition labels(see §2.2) are: “Silent” for local transitions; R(o, x, v) for reads;
W(o, x, v) for writes; U(or , ow , x, vr , vw ) for updates; Facq , Frel , Fsc
for fences; and SysCall(v) for system calls. Note that updates have
two access modes, one for the read and one for the write; and that
only fences may have the sc mode.

Remark 1. Our model handles only hardware-atomic memory accesses. To handle non-atomic reads/writes, such as Java double andC struct accesses, our semantics could be extended by introducing“garbage values” (LLVM-style undefined values [2]) as in [8].
4.4System Calls

For the purpose of defining the behaviors of programs (as needed
to prove soundness of transformations), we augment our language
and semantics with system calls labeled with “SysCall(v)”. These
are operations that are visible to an external observer (e.g., printing
statements). For simplicity, we assume that these take one value(input or output), and more importantly, that they do not access thememory, and serve as the strongest barrier for reordering. Thus, we
simply model system calls as SC fences.
4.5

Formal Model

Finally, we formally present our full model, combining and making
precise all the ideas outlined above. The model employs three modes
for memory accesses, naturally ordered as follows:

View A view is a pair V = hTpln , Trlx i of timemaps (see §2.2)
satisfying Tpln ≤ Trlx . We denote by V.pln and V.rlx thecomponents of V . View denotes the set of all views.
Messages A message m is a tuple hx : v @(f, t], Ri, where x ∈Loc, v ∈ Val, f, t ∈ Time, and R ∈ View, such that f < t or
f = t = 0, and R.rlx(x) = t or R = ⊥. We denote by m.loc,
m.val, m.from, m.to, and m.view the components of m.
Memory A memory is a (nonempty) pairwise disjoint finite set of
messages (see §3 for def. of disjointness). A memory M supports
the following insertions of a message m = hx : v @(f, t], Ri :Modifying Existing Promises

So far, our model does not allow promises, once made, to bechanged. However, our full model does allow two forms of promise
adjustment, both of which are defined in such a way that threads
that have already read from the promised message are unaffected.

A• The additive insertion, denoted by M ←m, is only defined if{m} # M , in which case it is given by {m} ∪ M .

Split The first form of promise adjustment is splitting. Consider
the following example:

S• The splitting insertion, denoted by M ←m, is only defined0000
if there exists m = hx : v @(f, t ], R i with t < t0 in M , inwhich case it is given by M \{m0 } ∪ {m, hx : v 0 @(t, t0 ], R0 i}.

a := x; // 2
if a = 2 then FAA(y, 1); FAA(y, 1); else FAA(y, 2);U• The lowering insertion, denoted by M ←m, is only defined
if there exists m0 = hx : v @(f, t], R0 i with R ≤ R0 in M , inx := y;which case it is given by M \{m0 } ∪ {m}.

We find it natural to allow the specified behavior, as it can be obtained by benign compiler optimizations: first FAA(y, 1); FAA(y, 1)

We write M (x) for the sub-memory { m ∈ M | m.loc = x }.

8( MEMORY: FULFILL )S
U←-∈ {←, ←}P 0 = P ←- m

( MEMORY: NEW )mmhP, M i −→ hP, M ←- mi

00( WRITE - HELPER )cur.rlx(x) < t
cur0 = cur t V
acq 0 = acq t cur00
rel = rel[x 7→ rel(x) t V t (o w ra ? cur0 )]Rw = (o w rlx ? (rel0 (x) t Rr ))where V = [pln : {x@t}, rlx : {x@t}]( READ - HELPER )o = pln=⇒ cur.pln(x) ≤ to ∈ {rlx, ra} =⇒ cur.rlx(x) ≤ t
cur0 = cur t V t (o w ra ? R)
acq 0 = acq t V t (o w rlx ? R)
where V = [pln : (o w rlx ? {x@t}), rlx : {x@t}]
R:o,x,t,R

M 0 = M ←- mhP, M i −→ hP \ {m}, M 0 i

A

W:o,x,t,Rr ,Rw

0

0

0

( SC - FENCE - HELPER )S 0 = acq.rlx t S
cur0 = acq 0 = hS 0 , S 0 i
rel0 = λ_.hS 0 , S 0 i
Fschhcur, acq, reli, Si −−→
hhcur0 , acq 0 , rel0 i, S 0 i

0hcur, acq, reli −−−−−−−−−→ hcur , acq , rel ihcur, acq, reli −−−−−−→ hcur , acq , reli

( UPDATE )( WRITE )U(or ,ow ,x,vr ,vw )σ −−−−−−−−−−→ σ 0
ow = ra =⇒ ∀m0 ∈ P (x). m0 .view = ⊥hx : vr @(_ , tr ], Rr i ∈ M
mw =hx : vw @(tr , tw ], Rw i
mw
hP, M i −−→
hP 0 , M 0 i

W(o,x,v)( READ )R(o,x,v)

σ −−−−−→ σ 0
hx : v@(_, t], Ri ∈ M
R:o,x,t,R

V −−−−−−→V 0hhσ, V, P i, S, M i −→ hhσ 0 , V 0 , P i, S, M i

σ −−−−−→ σ 0
o = ra =⇒ ∀m0 ∈ P (x). m0 .view = ⊥m = hx : v@(_, t], RimhP, M i −→ hP 0 , M 0 i

R:or ,x,tr ,Rr

W:o,x,t,⊥,R( SYSTEM CALL )( SC - FENCE )( ACQ - FENCE )

Frel

Facq

σ −−→ σ 0
cur0 = acq
hhσ, hcur, acq, reli, P i, S, M i −→hhσ 0 , hhcur0 , acq, reli, P i, S, M ii

( SILENT )Silentσ −−−→ σ 0hhσ, V, P i, S, M i −→ hhσ 0 , V, P i, S, M i

SysCall(v)

F

sc
σ −−
→ σ0

( REL - FENCE )00

σ −−→ σrel = λ_.cur∀m ∈ P. m.view = ⊥hhσ, hcur, acq, reli, P i, S, M i −→hhσ 0 , hhcur, acq, rel0 i, P i, S, M ii

Fscσ −−−−−−→ σ 0
0

F

0

sc
hV, Si −−→ hV 0 , S 0 i∀m ∈ P. m.view = ⊥hV, Si −−→ hV , S i∀m ∈ P. m.view = ⊥hhσ, V, P i, S, M i −→hhσ 0 , V 0 , P i, S 0 , M i( PROMISE )ASU←-∈ {←, ←, ←}P 0 = P ←- m
M 0 = M ←- mm.view ∈ M 0hhσ, V, P i, S, M i −→ hhσ, V, P 0 i, S, M 0 i

W:ow ,x,tw ,Rr ,Rw

V −−−−−−−→−−−−−−−−−−−→V 0hhσ, V, P i, S, M i −→ hhσ 0 , V 0 , P 0 i, S, M 0 i

V −−−−−−−−→V 0hhσ, V, P i, S, M i −→ hhσ 0 , V 0 , P 0 i, S, M 0 i

SysCall(v)hhσ, V, P i, S, M i −−−−−−→
hhσ 0 , V 0 , P i, S 0 , M i( MACHINE STEP )hTS(i), S, M i −→∗ hTS 0 , S 0 , M 0 i
000 e→ hTS 00 , S 00 , M 00 i
hTS , S , M i −hTS 00 , S 00 , M 00 i is consistente→ hTS[i 7→ TS 00 ], S 00 , M 00 i
hTS, S, M i −Figure 3. Full operational semantics.
Closed Memory Given a timemap T and a memory M , we write
T ∈ M if, for every x ∈ Loc, we have T (x) = m.to for somem ∈ M with m.loc = x. For a view V , we write V ∈ M if
T ∈ M for each component timemap T of V . A memory M isclosed if m.view ∈ M for every m ∈ M .

The write and the update steps cover two cases: a fresh write
to memory (MEMORY: NEW) and a fulfillment of an outstandingpromise (MEMORY: FULFILL). The latter allows to split the promise
or lower its view before its fulfillment (note that when m ∈ P ⊆ M ,U
UU
we have P = P ←m and M = M ←m by def. of ←).

Future Memory For memories M, M 0 , we write M −→ M 0 ifASU
M 0 ∈ {M ←m, M ←m, M ←m} for some message m, andM 0 is closed. We say M is a future memory of M w.r.t. a memory
P , if P ⊆ M 0 and M −→∗ M 0 .

Consistency A thread configuration hTS , S, M i is called consistent if for every future memory Mfuture of M w.r.t. TS .prm andevery timemap Sfuture with S ≤ Sfuture ∈ Mfuture , there exist TS 0 ,S 0 , M 0 such that:Threads A thread view is a triple V = hcur, acq, reli, where
cur, acq ∈ View and rel ∈ Loc → View satisfying rel(x) ≤cur ≤ acq for all x ∈ Loc. We denote by V.cur, V.acq, and V.rel
the components of V. A thread state is a triple TS = hσ, V, P idefined just as in §2.2 except with a thread view V instead of asingle timemap (σ is a local state and P is a memory). We denoteby TS .st, TS .view, and TS .prm the components of TS .

hTS , Sfuture , Mfuture i →− ∗ hTS 0 , S 0 , M 0 i ∧ TS 0 .prm = ∅Machine and Behaviors A machine state is a triple MS =hTS, S, M i consisting of a function TS assigning a thread state to
every thread, an SC timemap S, and a memory M . The initialstate MS0 (for a given program) consists of the function TS 0
mapping each thread i to its initial state σi0 , the zero thread view (alltimestamps in all timemaps are 0), and an empty set of promises;
the zero timemap S 0 ; and the initial memory M 0 consisting of one
message hx : 0@(0, 0], ⊥i for each location x. The machine step isdefined by the last rule in Figure 3. The variable e in the final thread
configuration step can either be a usual step (e is empty), or denotea system call (e = SysCall(v)).
To define the set of behaviors of a program P (namely, what isexternally observable during P’s executions), we use the system
calls that P’s executions perform. More precisely, every execution
induces a sequence of system calls (each includes a specific value
for input/output), and the set of behaviors of P is taken to be the setof all system call sequences induced by executions of P.

Thread Configuration Steps A thread configuration is a triple
hTS , S, M i, where TS is a thread state, S is a timemap (the global
SC timemap), and M is a memory.
Figure 3 presents the full list of thread configuration steps. To
avoid repetition, we use the additional rules READ - HELPER, WRITE HELPER , and SC - FENCE - HELPER . These employ several helpful
notations: ⊥ and t denote the natural bottom elements and join
operations for timemaps and for views (pointwise extensions of theinitial timestamp 0 and the t—i.e., max—operation on timestamps);{x@t} denotes the timemap assigning t to x and 0 to other locations;and (cond ? X) is defined to be X if cond holds, and ⊥ otherwise.

9

LRvrlx M = ld
LRra M= ld; lwsync
LWvrlx M = st
LWra M= lwsync; st
LF@sc M= lwsync
LFsc M= sync
LUvrlx,vrlx M = L: lwarx; cmp; bc Lout; stwcx.; bc L; Lout:
LUra,vrlx M = LUrlx,rlx M; lwsync LUvrlx,ra M = lwsync; LUrlx,rlx M
LUra,ra M = lwsync; LUrlx,rlx M; lwsync

Promise-Free Machine In several of our results below, we makeuse of the fragment of our model obtained by revoking the ability tomake promises (i.e., omitting the PROMISE rule). We call this thepromise-free machine.

5.

Results

Figure 4. Compilation to Power.

In this section, we outline a number of important results we have
proven to hold of our “promising” model.
All the results of this section are fully validated in Coq except
for §5.3 and Theorems 2 and 3, for which we provide proof outlines.
The Coq development and all proof outlines are available at [1].
5.1

R-after-R: Ro ; Ro

Compiler Transformations

A transformation Psrc ; Ptgt is sound if it does not introduce new
behaviors under any (parallel and sequential) context, that is, forevery context C, every behavior of C[Ptgt ] is a behavior of C[Psrc ].
Next, we list the program transformations proven to be soundin our model. To streamline the presentation, we refer to transformations on the semantic level, as if they are applied to actions,
namely fences and (valueless) memory accesses. Thus, we presuppose adequate syntactic manipulations on the program level that
implement these semantic transformations. For example, a syntactictransformation implementing Rxrlx ; Ryrlx ; Ryrlx ; Rxrlx is a reordering
a := x; b := y ; b := y; a := x on the program code (assuming
a 6= b); while a merge of a write and an update correspond, e.g., to atransformation of the form x := a; FAA(x, 1) ; x := a + 1. Nevertheless, our formal development proves soundness of transformations on the purely syntactic level, assuming a simple programming
language with memory operations, conditionals, and loops.

Introducing and Eliminating Unused Reads Introduction of irrelevant read accesses is sound in our model, unlike in the Java
memory model [26]. Eliminating plain read accesses whose readvalues are never used in the program is also sound in our model. In
contrast, eliminating relaxed or acquire reads is not generally soundbecause it may remove synchronization.
Proof Technique Our proof of these results employs the wellknown approach of simulation relations between the target and thesource programs. Importantly, our definitions ensure thread-locality,
thus allowing us to define a simulation relation on thread configurations, which (as we prove) can be composed into a simulation
relation on full machine states. Additionally, for thread configurations, we prove the adequacy of simulation up-to context, which lets
us ignore the certification processes in the source and the target, andjust provide simulations between simple “code snippets”.

Reordering Next we consider transformations of the form X; Y ;Y; X, and specify the set of reorderable pairs, that is the set of pairs
X; Y for which we proved this reordering transformation to be soundin our model. First, the following pairs are reorderable (where x andy denote distinct locations):
•

W ;R

•

Rxvrlx ; Ry and Rxpln ; Rxpln•

Frel ; W6=rlxy• W ;Wvrlx
yx• R
vrlx ; Wvrlx
x•

Frel ; R•

W; Facq•

R6=rlx ; Facq•

Frel ; Facq

W; R

Note that read-after-update does not allow the read to be an acquire
read unless the update includes an acquire read (unlike read-afterwrite elimination). This is due to release sequences: eliminating an
acquire read after a relaxed update may remove the synchronization
due to a release sequence ending in this update.
Finally, two fences of the same type can obviously be merged.
The set of mergeable pairs in our model contains all pairs
intended to be mergeable in the C++ and Java models [28, 26].
In particular, we support R-after-W merging, which is the effect of
local satisfaction of reads in hardware like TSO, Power, and ARM.

Strengthening A simple transformation that is sound in our modelis strengthening of access modes. A read/write action Xo can betransformed to Xo0 provided that o v o0 . Similarly, it is sound to
replace Uor ,ow by Uo0r ,o0w provided that or v o0r and ow v o0w , or tostrengthen Frel or Facq to Fsc .

y

R-after-W:

R-after-U: Urlx,o ; Rrlx , and Ura,o ; Rra
U-after-W: Wo ; Uor ,oU-after-U: Uo1 ,o ; Uo2 ,o , provided that Uo1 ,o ; Ro2 is mergeable

Trace-Preserving Transformations Transformations that do notchange the set of traces of actions in a given thread are clearly sound.
For example, y := a + 1 − a ; y := 1 is a sound transformation(recall that a denotes a local register; see §1:LBfd). Indeed, thisis the crucial property that distinguishes a memory model for ahigher-level language from a hardware memory model.

x

W-after-W: Wo ; Wo

Using the strengthening transformation, the access modes here
can be read as upper bounds (e.g., Rra ; Rrlx can be first strengthened
to Rra ; Rra and then merged). Note that the R-after-W merge allows
even to eliminate a redundant acquire read after a plain/relaxed write(as in Example LBa0 in §4.1).
In addition, the following pairs involving updates are mergeable:

5.2

Compilation to TSO

Like C++11, our model can be efficiently compiled to x86-TSO.
Since this architecture provides relatively strong guarantees, every
memory access can be compiled to a primitive hardware instruction. Moreover, release/acquire fences are ignored during compilation, and SC fences are mapped to an MFENCE instruction. Correctness of this mapping follows from a recent result by Lahav andVafeiadis [18], which shows that all weak behaviors of TSO are
explained by store-load reordering and merging. Accordingly, it reduces the correctness proof of compilation to TSO to: (i) supporting
write-read reordering and write-read merge; and (ii) a correctness
proof of compilation to SC. Since we proved the soundness of writeread reordering and merge (regardless of the access modes of thetwo events), and since clearly our model is weaker than SC, we
immediately derive the correctness of compilation to TSO.

In addition, for the purpose of specifying reorderable pairs,
an update is just a combination of a read and a write. Thus,
X; Uor ,ow is reorderable if both X; Ror and X; Wow are reorderable,
and symmetrically Uor ,ow ; X is reorderable if both Ror ; X and Wow ; X
are reorderable. In particular, a pair Uxoxr ,oxw ; Uyoy ,oy is reorderable ifrw
x 6= y, oxr v rlx, oyw v rlx.
The set of reorderable pairs in our model contains all pairs thatare intended to be reorderable in the C++ and Java memory models,
including in particular all “roach-motel reorderings” [28, 26].
Merging These are transformations that completely eliminate an
action. Clearly, the two actions in mergeable pairs (pairs for which
we proved the merge to be sound in our model) should access thesame location. The following three kinds of pairs are mergeable:

5.3

Compilation to Power

Figure 4 provides the compilation scheme of our model to Power,
following the C++11 one. We denote by LPM the Power program10obtained by applying this mapping to a source program P. To provecompilation correctness, we again utilize a result of [18], whichshows that every allowed behavior of a Power program Q (assuming
its recent declarative model of Alglave et al. [5]) is a behavior of a
Power program Q0 under a stronger model, called “StrongPower”,
where Q0 is obtained from Q by applying a sequence of local
reorderings of independent memory accesses to distinct locations.
Accordingly, it suffices to show that, given a source program P,
our model allows all behaviors that StrongPower allows for somereordering of LPM. We split this into two steps, outlined below.

LP2 M = Q, and P2 is obtained from P1 by applying a sequence ofreorderings at the source level. Crucially, the reorderings that take P1
to P2 are all sound in our model: in addition to those already coveredin §5.1, the reorderings of Wxsrlx /Uxrlx,srlx past a Ryrlx /Wyrlx /Uyrlx,rlx(where x 6= y) have also been proven sound in Coq. (Note thatthe reverse reorderings—moving accesses past a srlx—are notneeded because of the aforementioned property that all srlx’s in
P1 come immediately after a release fence.) Returning to the above
example, when matching the reordering of lwsync;st x 1;st y 2
to lwsync;st y 2;st x 1 in the target, these new reorderings
validate the transformation of fence-rel; x :=srlx 1; y :=rlx 2 tofence-rel; y :=rlx 2; x :=srlx 1 in the source.
Putting it all together: by the compilation to StrongPower result,
we know that any behavior of Q under StrongPower is also a
behavior of P2 in our model; by soundness of the reorderings,
we know this is also a behavior of P1 ; and by soundness of thesource-to-source mappings, it is also a behavior of the original P.
Finally, we note that for C++11, there is a more efficient compilation scheme of acquire reads and updates, which uses a control
dependency and an isync fence instead of a lightweight fence(lwsync). We believe that our model is also correctly compiled using this scheme. Nevertheless, this will require a more direct proof(isync fences are beyond the reach of [18]), which we leave tofuture work.

Compilation to StrongPower First, we show that the compilation
to StrongPower is correct, that is: every behavior of LPM under
StrongPower is allowed for P in our model. StrongPower strengthens the Power model by forbidding “load buffering” behaviors (formally, it disallows cycles in the entire program order together withthe reads-from relation). Consequently, we do not actually needpromises in order to explain StrongPower behaviors—instead, we
can just show that behaviors of LPM under StrongPower are allowed
for P under our promise-free machine (see end of §4.6). (Notethat this does not contradict the fact that promises are necessary
to explain weak behaviors of the (non-strong) Power model, suchas the LB.) To ease the proof, we use an alternative, declarative
presentation of our promise-free machine (§5.6), which can straightforwardly be shown to be weaker than the StrongPower model under
the compilation scheme in Figure 4. See [1] for details.

5.4

Reorderings in the Compiled Program Second, to account for sequences of reorderings of independent memory accesses to distinct
locations in LPM, we would like to relate them to the reorderings in
the source program P that we proved sound in §5.1. But there is a
subtle complication here: some reorderings in LPM do not correspondto reorderings in P! For example, if P is x :=ra 1; y :=rlx 2, its
compilation LPM has the form lwsync;st x 1;st y 2, but reordering the stores in LPM would produce lwsync;st y 2;st x 1, which
does not correspond to the reordering of P to y :=rlx 2; x :=ra 1(compiling the latter would yield st y 2;lwsync;st x 1).
To solve this issue, we slightly extend our model and consider
compilation as if it happens in two stages. First, all release/acquire
accesses in P are split into weaker accesses and corresponding
fences as follows:• Rra ; Rrlx ; Facq and Wra ; Frel ; Wsrlx• Ura,o ; Urlx,o ; Facq and Uo,ra ; Frel ; Uo,srlx where o v rlx
Here, we introduced a new srlx (“strong relaxed”) mode, which has
the same semantics as rlx but blocks promises like ra writes (i.e.,
in write/update steps, we require that ∀m0 ∈ P (x). m0 .view = ⊥if o w srlx). The reason for this is technical: we would have liked
to just use rlx rather than srlx, but at least for Uo,ra , the mapping
to Frel ; Uo,rlx is unsound. Using srlx, however, we have proved thesoundness of the above source-to-source mappings (in Coq) using astraightforward simulation argument (the target program’s promises
are subject to the same constraints as the source’s), and srlx is
sufficient for the rest of the proof.
After this first step, we obtain a program P1 , which has nora accesses except possibly for Ura,ra ’s (which are surroundedby fences after compilation), and which has srlx accesses only
immediately after release fences. (The relevance of this property
will become clearer below.) For instance, in the example given
above, P1 would be fence-rel; x :=srlx 1; y :=rlx 2. We then apply
the compilation scheme of Figure 4, where srlx is compiled likerlx. Clearly, by construction of P1 , the result LP1 M is identical to
LPM. Moreover, sequences of reorderings of accesses applied to LPM
now correspond directly to sequences of reorderings in P1 .
Thus, suppose Power program Q is the result of applying
some sequence of reorderings of accesses to the compilation result
LPM = LP1 M. Then, there exists a source program P2 such that

DRF Theorems

We proceed with an explanation of our DRF theorems. These
theorems provide ways of restricting attention to better-behaved
subsets of the model assuming certain conditions on programs.
Evidently, the most complicated part of our semantics is thepromises. Without promises, our model amounts to a usual operational model, where thread steps only arise because of program
instructions. Hence, our first DRF result (and the one that is by
far the most challenging to prove) identifies a set of programs forwhich promises cannot introduce additional behaviors. Specifically,
we show that this holds for programs in which all racy accesses
are release/acquire, assuming a promise-free semantics. Crucially,as usual in DRF guarantees, the races are considered under thestronger semantics (promise-free), not the full model, thus allowing
programmers to adhere to this programming discipline while being
completely ignorant of the weak semantics (promises).
More precisely, we say that a machine state MS is o-race-free,
if whenever two different threads may take a (non-promise) step
accessing the same location, then both accesses are reads or bothhave access mode strictly stronger than o.
Theorem 1 (Promise-Free DRF). Let =⇒ denote the steps of thepromise-free machine (see end of 4.6). Suppose that every machinestate that is =⇒-reachable from the initial state of a program P is rlxrace-free. Then, the behaviors of P according to the full machine
coincide with those according to the =⇒-machine.
Putting promises aside, a counter-intuitive part of weak memory
models are the relaxed accesses, which allow threads to observe
writes without observing previous writes to other locations. Removing pln/rlx accesses, namely keeping only ra, substantiallysimplifies our machine (in particular, its thread views would consistof just one view, the cur one). Accordingly, our second DRF result
strengthens Theorem 1 and states that it suffices to show that there
are only races on ra accesses under release/acquire semantics toconclude that a program has only release/acquire behaviors.
ra

Theorem 2 (DRF-RA). Let =⇒ be identical to =⇒ in Theorem 1,
except for interpreting rlx and pln accesses in program transitions
as if they are all ra-accesses. Suppose that every machine staterathat is =⇒-reachable from the initial state of a program P is rlx-

11

race-free. Then, the behaviors of P according to the full machineracoincide with those according to the =⇒-machine.

J
a := x;J ∧ (a = 0)y
 := a;J

We observe that promise re-certification is necessary for the
proofs of Theorems 1 and 2: in [1] we show a counterexample in
the absence of promise re-certification.
To state a more standard DRF theorem, we assume programs
are well-locked: (1) locations are partitioned into normal and locklocations, and (2) lock locations are accessed only by matching pairsof the following lock/unlock operations:lock(l) :unlock(l) :def

J = (x = 0) ∧ (y = 0)

Figure 5. A simple derivation in the invariant-based program logic.
describe the possible behaviors of programs. This presentation
abstracts away particular timestamp choices and thread views, andreplaces them by formal conditions on partial orders in execution
graphs. The promise mechanism has an inherent operational nature,and thus our declarative presentation only applies to the promise-freemachine (see end of §4.6). Nevertheless, this presentation is usefulfor comparing our model to C++11, and it is used for establishing
the correctness of compilation (see §5.3). We also find this useful asa technical device for analyzing possible behaviors of the promisefree machine and applying Theorem 1.
The nodes of execution graphs are called events. An event
consists of an identifier (natural number), a thread identifier (takenfrom a finite set Tid of thread identifiers, or 0 for initialization
events), and a label. Labels have the form R(o, x, v) or W(o, x, v)(where o is the access mode, x is the location accessed, and v is thevalue read/written), as well as Facq , Frel , or Fsc (for fences). The
functions tid, lab, typ, and loc return (when applicable) the thread
identifier, label, type (R, W, F), and location of an event.
In turn, an execution graph G consists of:• a set E of events. This set always contains a set E0 of initialization
events, consisting of one plain write event assigning the initialvalue for every location. We assume that all initial values are 0.
For T ∈ {R, W, F}, we denote by T the set {a ∈ E | typ(a) = T}.
We also use subscript for access modes (e.g., Wwrlx denotes theset of all events a ∈ W with whose access mode is at least rlx).
• a relation sb, called sequenced before, which is a union ofrelations (E0 × (E \ E0 )) ∪ {sbi | i ∈ Tid}, where every sbi(i ∈ Tid) is a strict total order on {a ∈ E | tid(a) = i}.
• a relation rmw, called read-modify-write pairs, consisting of
immediate sb-edges (i.e., if ha, bi ∈ rmw then no c satisfies bothha, ci ∈ sb and hc, bi ∈ sb). In addition, for every ha, bi ∈ rmw,
we have typ(a) = R, typ(b) = W, and loc(a) = loc(b).
• a relation rf, called reads-from, which relates every read event in
E with one write event in E that has the same location and value.
• a relation mo, called modification order, which is a disjoint unionof relations {mox }x∈Loc , such that each relation mox is a strict
total order on Wx .
• a relation sc, called SC order, which is a strict total order on Fsc(the set of all SC fence events in E).

while !CAS(l, 0, 1, acqrel) do skip;
lrel := 0;

The theorem forbids any weak behavior in programs that, under
SC semantics, race only on lock locations. For the SC semantics, weconsider “an interleaving machine”, where reads read from the latest
write to the appropriate location (regardless of the access modes).
sc⇒ denote the steps of the interleavTheorem 3 (DRF-LOCK). Let =sc
ing machine. Suppose that every machine state that is =⇒-reachable
from the initial state of a well-locked program P is race-free on
normal locations. Then, the behaviors of P according to the fullscmachine coincide with those according to the =⇒-machine.
5.5


J
x
 := y;J

An Invariant-Based Program Logic

Besides the DRF guarantees, to demonstrate that our model does
not suffer from the disastrous consequences of OOTA, we provesoundness of a very simple program logic for concurrent programswith respect to our model. In particular, it can be trivially used toshow that LBd must return a = 0, and more generally, that programs
cannot read values they never wrote. Note that even this basic logic
is unsound for C++’s relaxed accesses (whereas it is sound in ourmodel even if all accesses are plain).
We take a program proof to be a tuple hJ, S1 , S2 , ...i, where J
is a global invariant over the shared variables and each Si ⊆ Statei
is a set of local states (intuitively describing the reachable states of
thread i) such that the following conditions hold:V• σi0 ∈ Si and x∈Loc x = 0 ` J.
R(o,x,v)• If σi −−−−−→ σi0 then σi ∈ Si ∧ J ∧ x = v ` σi0 ∈ Si .
W(o,x,v)• If σi −−−−−→ σi0 then σi ∈ Si ∧ J ` σi0 ∈ Si ∧ J[v/x].
U(o ,o ,x,v ,v )r w
r w
• If σi −−−−−−−−−−→ σi0 thenσi ∈ Si ∧ J ∧ x = vr ` σi0 ∈ Si ∧ J[vw /x].
e

• For e ∈ {Facq , Frel , Fsc , Silent, SysCall(v)}, if σi −→ σi0 thenσi ∈ Si ` σi0 ∈ Si .

Figure 5 provides an illustration of a program proof showing that
LBd does not exhibit weak behaviors.
Now, given a program proof for a program P, we can show that
all the reachable states MS from the initial state MS0 of P satisfy
the global invariant J:

Notation 1. R? , R+ , and R∗ respectively denote the reflexive,transitive, and reflexive-transitive closures of a binary relation
R. R−1 denotes its inverse relation. We denote by R1 ; R2 theleft composition of two relations R1 , R2 . Finally, [A] denotes theidentity relation on a set A. In particular, [A]; R; [B] = R∩(A×B).

Theorem 4 (Soundness). Let hJ, S1 , S2 , ...i be a program proof,0
and let MS = hTS , S, M i such that→∗ MS. Then,
V MS −TS (i).st ∈ Si for every thread i, and x∈Loc x = f (x).val ` J
for every function f that assigns to every location x a message
m ∈ M such that m.loc = x.

Now, to define which execution graphs are allowed, we derive
an happens-before order hb, which is defined as in C++11 (after
applying the correction suggested in [28] for release sequences):
sb|loc = {ha, bi ∈ sb | loc(a) = loc(b)}Our Coq proof of this theorem is simple: it holds trivially forpromise-free executions, and extends easily to promise steps, since
every promise step has a promise-free certification.
5.6(sb-loc)

rs = [W]; sb|?loc ; [Wwrlx ]; (rf; rmw; [Wwrlx ])∗rel = ([Wra ] ∪ ([Frel ∪ Fsc ]; sb)); rs(release-seq)(to-be-released)

sw = rel; rf; ([Rra ] ∪ ([Rwrlx ]; sb; [Facq ∪ Fsc ]))hb = (sb ∪ sw)

Declarative Presentation of the Promise-Free Machine+(sync)(happens-before)

Given the definition of hb, an execution graph G is consistent if
the following hold:In this section, we provide a declarative presentation of our model,
in the style of C++11, namely using sets of execution graphs to12• mo; hb is irreflexive.

(WW-coherence)• mo; rf; hb is irreflexive.

(RW-coherence)• mo; hb; rf−1 is irreflexive.

(WR-coherence)U(x,vr ,vw ,or ,ow )lab(a)• mo; rf; R; rf−1 is irreflexive,

Silent(RR-coherence)
where R = ([Rwrlx ]; hb) ∪ (hb; [Rwrlx ]) ∪ (hb; [Fsc ]; hb).

• (rf; rmw) ∩ (mo; mo) = ∅.
• mo; rf? ; hb; sc; hb; (rf−1 )? is irreflexive.
• sb ∪ rf ∪ sc is acyclic.

σ −−−→ σ 0ihσ, Gi −→ hσ 0 , Gi

(Atomicity)ihσ, Gi −→ hσ 0 , G0 i

SysCall(v)(No-promises)

i,SysCall(v)hσ, Gi −−−−−−−→ hσ 0 , G0 i

Putting aside differences in presentation (e.g., instead of aprimitive RMW event, we have two events related by an rmw-edge),
there are three essential differences between this model and theC++11 one [6]:σ −−−−−−−−−−→ σ 0lab(ar ) = R(or , x, vr )lab(aw ) = W(ow , x, vw )tid(ar ) = tid(aw ) = i
G0 ∈ AddRMW(G, ar , aw )ihσ, Gi −→ hσ 0 , G0 i
( MACHINE STEP )i,ehΣ(i), Gi −−→ hσ 0 , G0 i
G0 is consistentehΣ, Gi −→ hΣ[i 7→ σ 0 ], G0 i

Figure 6. Operational semantics based on the declarative model.
but ours is the first to come with formal (and machine-checked)
validation of a wide range of essential local transformations (§5.1)
concerning a broad spectrum of features from the C++ model.
The first major attempt to solve the “out of thin air” problem wasby the Java memory model (JMM) [21] (see also [20]). The JMM intended to validate all the compiler optimizations that Java compilers
and just-in-time compilers might perform, but its formal definition
failed to validate them [26]. Subsequent fixes were proposed to themodel, which improved the set of enabled optimizations, but still
falling short of what actual Java compilers were performing.
Interestingly, an early glimpse of our idea of promises may beseen in version 1.0 of the JMM [12], which describes a form of“prescient store actions” (§17.8). However, their description is very
brief and vague, and the feature was removed for JSR 133 [3].
To resolve some of the problems with the JMM definition,
Jagadeesan et al. [14] proposed an operational model following
quite closely the intended behavior of the JMM, but employing
the notion of a speculation. Speculations are similar to our notion ofpromises, but unlike promises they are not certified thread-locally:
whereas we model interference conservatively by quantifying over
all future memories during certification, they model interference
from other threads more precisely by executing multiple threads
together during certification. We believe our conservative approachis sufficient for justifying standard compiler optimizations, which
are typically thread-local, and moreover it simplifies the presentationof the semantics and the development of the metatheory because it
avoids the need for nested certifications.
Jagadeesan et al.’s model satisfies the standard DRF theorem,
as well as a DRF theorem saying that speculations are unnecessary
for programs without read-write races. They also develop a simulation proof technique, with which they verify three optimizations:write-write reordering, roach-motel reordering, and read-after-readelimination. We have applied our simulation method to a muchwider variety of optimizations, and our proofs are machine-checkedin Coq. They also do not provide any compilation correctness results,
and their model omits release-acquire accesses, updates, and fences.
More recently, Jeffrey and Riely [15] presented a weak memory
model based on event structures. Their model admits a standard DRF
theorem, but does not fully allow the reordering of independent
memory accesses, and thus cannot be compiled to Power/ARM
without extra fences. The paper suggests an idea about how to fix
the model to support such reorderings, but it is not known whether
the suggested fixed model avoids OOTA behaviors. Relating to ourwork, their model seems to be “promising” reads (instead of writes)
and restricting the quantification over possible futures to only thosethat could arise from further execution of the current program. The
model only supports relaxed accesses and locks.
Pichon-Pharabod and Sewell [24] introduced an event structure
model with both a normal reduction rule, which executes an initial
event of the event structure, and special reduction rules that mimic• Our model disallows cycles in sb ∪ rf ∪ sc, and hence it does

not permit load buffering behaviors (which are not possible in
the promise-free machine).
• Our model lacks SC accesses, and its condition for SC fences

is stronger than the one of C++11. In particular, unlike in
C++11, placing an SC fence between every two commands
does guarantee SC semantics.
• Our model does not have non-atomic accesses on which races im-

ply undefined behavior. It does have plain accesses for which RRcoherence does not apply (unless an SC fence is hb-between).
Now, to define behaviors of programs using consistent execution
graphs and programs, we present a “declarative machine”, which
incrementally builds a consistent execution graph following someinterleaving of the program’s threads operations. Formally, thedeclarative machine state is a pair hΣ, Gi, where Σ assigns a local
state σ to every thread (as described in §2), and G is some consistentexecution graph. The possible steps of this machine are given
in Figure 6, assuming the same abstract programming language
discussed in §4.6. To define these steps, we use the following
notation for execution graph extension.
Notation 2. For two execution graphs G and G0 , we write G0 ∈Add(G, a) if G0 extends G with one event a, which is sb ∪ rf ∪ sc
maximal in G0 . We write G0 ∈ AddRMW(G, ar , aw ) if G0 extends
some Gmid ∈ Add(G, ar ) with one event aw and an rmw-edge
har , aw i, and aw is sb ∪ rf ∪ sc maximal in G0 .
The initial machine state is given by hλi.σi0 , G0 i, where G0
contains only the initialization events E0 (its relations are empty). A
behavior of a program under the declarative machine is again taken
to be the set of sequences of system calls induced by its executions.
Remark 2. In a purely declarative style, one considers only full runsof a program and checks consistency only once at the end. However,the definition of consistent execution graphs above is “prefix-closed”(that is, every sb ∪ rf ∪ sc-prefix of a consistent execution graphforms a consistent execution graph). As a result, we were able topresent our declarative semantics in a more operational style, which
can be conveniently related to the promise-free machine.
Theorem 5. For every program P, the behaviors of P according
to the promise-free machine coincide with the behaviors of P
according to the declarative machine.
The Coq proof of this theorem involves a non-trivial simulationargument. The simulation relation is presented in [1].

6.

σ −−−−→ σtyp(a) ∈ {R, W, F}
tid(a) = i
G0 ∈ Add(G, a)

σ −−−−−−→ σ 0lab(a) = Fsctid(a) = i
G0 ∈ Add(G, a)

(SC)

0

Related Work

There have been many proposals for solving the “out of thin air”
problem. Several of them have come with proofs of DRF guarantees,13the effect of standard compiler optimizations on the event structure.
These optimization rules include a rather complex rule for nonthread-local optimizations that can declare a whole branch of theevent structure unreachable. The paper does not present any formal
results about the model. It is worth noting that the model does notsupport the weak behavior of the ARM-weak program and thus may
not be compiled to ARM without additional fences. The model only
handles relaxed and non-atomic accesses and locks.
Podkopaev et al. [25] proposed an operational model coveringa large subset of the features of the C++ model. They provide
many litmus tests to demonstrate the suitability of their model,
but do not prove any formal results about it. Their model ensuresper-location coherence in a very similar way to our model: using
timestamps. In order to handle read-write reorderings, they allow
reads to return symbolic values, which are then evaluated at a later
point in time when their value is actually needed. This approachgives the expected behaviors to the LB and LBd programs, andmay be extended with a set of syntactic symbolic simplification
rules to also give the expected result to the LBfd program. It
seems, however, very difficult to extend this approach to enable
code motion optimizations, where some common code is pulled
out of two branches of a conditional. What makes code motion
more challenging is that the common code may become apparent
only after some earlier transformations, like for example the y := 1
assignment in the following code:
a := x; // 1
if a = 1 then y := a; else (z := 1; y := z; )be written by a future store. Norris and Demsky’s promises looksuperficially quite similar to ours, but their purpose is to support
practical model checking of C++ programs, not to change the semantics of the language, so the paper does not present any formal
model or metatheory of promises.

7.

Future Work

Besides extending our model with SC accesses (see §1.3), there are
a number of interesting issues remaining for future work.
Compilation Correctness Establishing the correctness of compilation of our model to ARM, as well as to Power using the more
efficient compilation scheme for acquire reads and updates (see§5.3), is an important future goal. To the best of our knowledge, weknow of no counterexamples for correctness of compilation to thesearchitectures.
Global Optimizations In our model, we insist that promises canalways be certified thread-locally. This decision enables threadlocal reasoning about our semantics and suffices to justify all
the known thread-local program transformations that a compiler
or the hardware may perform. It does, however, render unsoundsome transformations of a global nature, such as sequentialization(aka “thread inlining”), which merges threads together. To see this,consider the following:a := x; // 1
if a = 0 thenx := 1;x := y;Our model allows the annotated behavior of the program above,
precisely because our promises are semantic in nature and thus
avoid the brittle tracking of syntactic data dependencies.
Zhang and Feng [29] suggested an operational model for Java
accesses in which threads may re-execute some memory events. The
model admits a standard DRF theorem, and its replay mechanism
enables it to support local transformations. However, to avoid OOTA,
this mechanism is limited by its tracking of syntactic dependencies
between instructions, and thus it fails to validate behaviors resulting
from trace-preserving transformations like the one above.
Other proposals for language-level memory models have tried
not to solve the OOTA problem, but to avoid it, by introducing
stronger models where read-write reordering is not allowed. For
example, Ševčík et al. [27] and Demange et al. [10] proposed using TSO as the memory model for C and Java, respectively. These
proposals may be reasonable compromises if the only target machines of interest also follow the TSO model, but are prohibitively
expensive on weaker architectures, such as Power and ARM, because enforcing TSO on those machines requires essentially as many
fences as enforcing SC. In a similar line of work, Lahav et al. [17]introduced a strengthening of the release/acquire fragment of theC++ memory model, which they called SRA, together with an operational semantics for SRA. Compiling SRA to Power and ARM
is cheaper than TSO, but still requires some fences before or after every shared variable access, and may thus not be suitable for
performance-critical code.
Another approach is to simply allow OOTA behaviors. This was
the approach taken by Batty et al.’s formalization of C++ [6], andby the OpenCL model [16], as well as by Crary and Sullivan [9],who introduced a more fine-grained specification of the orders thatthe model is supposed to preserve. All of these models allow the
weak behavior of the LBd example, thereby invalidating standard
reasoning principles and DRF theorems.
Finally, Norris and Demsky [22] presented a tool that exhaustively enumerates the behaviors of concurrent C++ programs. To
account for speculative reads, the tool may establish “promised future values”, which a load can read from, and which must eventually

y := x; x := y;;a := x; // 1
if a = 0 thenx := 1;y := x;x := y;This source program disallows the specified behavior because if T1
reads 1 for x after promising x := 1, then it will not be able tofulfill its promise. Nevertheless, the result a = 1 is allowed in thetarget program (obtained by sequentializing T1 before T2 ). Here,T1 can safely promise y := 1, and later read x = 1 from T2 ’s
write.4 While sequentialization seems like a transformation that nocompiler would perform, there might be other more useful global
optimizations. Investigating what global optimizations are supported
in our model is left for future work.
Liveness It is natural to extend our operational model with livenessguarantees, and it is useful and interesting to study their interaction with program transformations and DRF theorems. Livenessproperties are currently mostly ignored in weak memory research.
Program Logic The program logic presented in §5.5 only establishes the very basic sanity of our memory model. Developing a
useful program logic for this model is a direction for future work.
Simulation and Model Checking The high degree of nondeterminism in our model makes it hard to exhaustively explore all
possible behaviors of a given program. Further work is required todevelop efficient methods and tools for this purpose.

Acknowledgments
We thank Doug Lea, Alan Jeffrey, Andreas Lochbihler, James Riely,
Peter Sewell, and Joe Tassarotti for very helpful feedback. This research was supported in part by Samsung Research Funding Centerof Samsung Electronics under Project Number SRFC-IT1502-07,
and in part by an ERC Consolidator Grant for the project “RustBelt”(grant agreement no. 683289). The first author has been supported
by a Korea Foundation for Advanced Studies Scholarship.
4 Though sequentialization is a very intuitive property that one might

expect a memory model to validate, we observe that TSO [23], Power [5],ARMv8 [11], Java [21], and C/C++11 [6] (without the corrections proposedin [28]) all do not allow sequentialization.

14

References[16] Khronos Group. The OpenCL specification, Version 2.1, 2015.

[1] Coq development and supplementary material for this paper available
at: http://sf.snu.ac.kr/promise-concurrency.

[17] Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. Taming releaseacquire consistency. In Proc. 43rd Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2016,
pages 649–662. ACM, 2016.

[2] LLVM documentation. LLVM atomic instructions and concurrency
guide. http://llvm.org/docs/Atomics.html.

[18] Ori Lahav and Viktor Vafeiadis. Explaining relaxed memory models
with program transformations. In Proc. 21st International Symposium
on Formal Methods, FM 2016, 2016.

[3] JSR 133. Java memory model and thread specification revision, 2004.
http://jcp.org/jsr/detail/133.jsp.
[4] Sarita V. Adve and Mark D. Hill. Weak ordering—A new definition. In
Proc. 17th Annual International Symposium on Computer Architecture,
ISCA 1990, pages 2–14. ACM, 1990.

[19] Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek
Dreyer. Repairing sequential consistency in C/C++11. Technical
Report MPI-SWS-2016-011, MPI-SWS, November 2016.

[5] Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats:
Modelling, simulation, testing, and data mining for weak memory.
ACM Trans. Program. Lang. Syst., 36(2):7:1–7:74, July 2014.

[20] Andreas Lochbihler. Making the Java memory model safe. ACM Trans.
Program. Lang. Syst., 35(4):12:1–12:65, 2014.
[21] Jeremy Manson, William Pugh, and Sarita V. Adve. The Java memory
model. In Proc. 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pages 378–391. ACM,
2005.

[6] Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark
Weber. Mathematizing C++ concurrency. In Proc. 38th Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2011, pages 55–66. ACM, 2011.

[22] Brian Norris and Brian Demsky. CDSchecker: Checking concurrent
data structures written with C/C++ atomics. In Proc. 2013 ACM
SIGPLAN International Conference on Object Oriented Programming
Systems Languages & Applications, OOPSLA 2013, pages 131–150.
ACM, 2013.

[7] Hans-Juergen Boehm and Brian Demsky. Outlawing ghosts: Avoiding
out-of-thin-air results. In Proc. Workshop on Memory Systems Performance and Correctness, MSPC 2014, pages 7:1–7:6. ACM, 2014.
[8] Soham Chakraborty and Viktor Vafeiadis. Formalizing the concurrency semantics of an LLVM fragment. In Proc. 15th IEEE/ACM
International Symposium on Code Generation and Optimization, CGO
2017, 2017.

[23] Scott Owens, Susmit Sarkar, and Peter Sewell. A better x86 memory
model: x86-TSO. In Proc. 22nd International Conference on Theorem
Proving in Higher Order Logics, TPHOLs 2009, pages 391–407.
Springer, 2009.

[9] Karl Crary and Michael J. Sullivan. A calculus for relaxed memory. In
Proc. 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, POPL 2015, pages 623–636. ACM, 2015.

[24] Jean Pichon-Pharabod and Peter Sewell. A concurrency semantics
for relaxed atomics that permits optimisation and avoids thin-air
executions. In Proc. 43rd Annual ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, POPL 2016, pages 622–633.
ACM, 2016.

[10] Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan,David Pichardie, and Jan Vitek. Plan B: A buffered memory model forJava. In Proc. 40th Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL 2013, pages 329–342.
ACM, 2013.

[25] Anton Podkopaev, Ilya Sergey, and Aleksandar Nanevski. Operational
aspects of C/C++ concurrency. CoRR, abs/1606.01400, 2016.

[11] Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali
Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. Modelling theARMv8 architecture, operationally: Concurrency and ISA. In Proc.
43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, POPL 2016, pages 608–621. ACM, 2016.

[26] Jaroslav Ševčík and David Aspinall. On validity of program transformations in the Java memory model. In Proc. 22nd European Conference
on Object-Oriented Programming, ECOOP 2008, volume 5142 of
LNCS, pages 27–51. Springer, 2008.
[27] Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh
Jagannathan, and Peter Sewell. CompCertTSO: A verified compiler
for relaxed-memory concurrency. J. ACM, 60(3):22, 2013.

[12] James Gosling, Bill Joy, and Guy Steele. The Java language specification, Edition 1.0, August 1996. http://titanium.cs.berkeley.
edu/doc/java-langspec-1.0/.

[28] Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin
Morisset, and Francesco Zappa Nardelli. Common compiler optimisations are invalid in the C11 memory model and what we can doabout it. In Proc. 42nd Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL 2015, pages 209–220.
ACM, 2015.

[13] ISO/IEC 14882:2011. Programming language C++, 2011.
[14] Radha Jagadeesan, Corin Pitcher, and James Riely. Generative
operational semantics for relaxed memory models. In ESOP, pages
307–326, 2010.
[15] Alan Jeffrey and James Riely. On thin air reads: Towards an event
structures model of relaxed memory. In Proc. IEEE Logic in Computer
Science, LICS 2016, 2016.

[29] Yang Zhang and Xinyu Feng. An operational happens-before memory
model. Frontiers of Computer Science, 10(1):54–81, 2016.

15

A.

Proofs of DRF Theorems

We define the set of memory events α ∈ ME as follows:{ silent }∪ { read(o, x, t) | o ∈ AM, x ∈ Loc, t ∈ Time }∪ { write(o, x, t) | o ∈ AM, x ∈ Loc, t ∈ Time }∪ { update(or , ow , x, tr , tw ) | or , ow ∈ AM, x ∈ Loc, tr , tw ∈ Time }∪ { fence(T ) | T ∈ {acq, rel, sc} }∪ { syscall(v) | v ∈ ... }where AM = {pln, rlx, ra}.
We call the following events globally synchronizing:{ fence(sc) }∪ { syscall(v) | v ∈ ... }

ra

MS0 =
⇒(i1 ,α1 ) MS1 =⇒(i2 ,α2 ) · · · =⇒(in ,αn ) MSn ,1. ∀k, j. MSk .ths(j).st = MS0k .ths(j).st ;2. ∀k, j. MSk .ths(j).view.cur = MS0k .ths(j).view.cur ;3. ∀k, j. MSk .ths(j).view.acq = MS0k .ths(j).view.acq ;4. ∀k. MSk .gsc = MS0k .gsc ; and5. ∀k. MSk .mem and MS0k .mem have the same messages, except
rathat the released view of a message in the =⇒-execution may
be higher than that of the corresponding message in the =⇒execution.

rasuch that∀k ≥ 2. MSk .ths(ik ).view 6≥ MS1 .ths(i1 ).view .
Then we have ik 6= i1 for all k ≥ 2 and the following execution

This simulation proves (i), as a rlx-race in MSk in the =⇒raexecution is also a rlx-race in MS0k in the =⇒-machine, thanks tothe condition 1. It also proves (ii) by the adequacy of the simulation
relation.
Now we prove the simulation. Consider a =⇒-step:MS =⇒(i2 ,α2 ) MS02 =⇒(i3 ,α3 ) · · · =⇒(in ,αn ) MS0nrara

for some machine states MS0k satisfying∀k ≥ 2. ∀i 6= i1 . MS0k .ths(i).st = MSk .ths(i).st .

MSn =⇒(in+1 ,αn+1 ) MSn+1 ,Proof. There are only two cases where the first step with (i1 , α1 )affects a subsequent step with (ik , αk ): either (i) the latter reads
what the former wrote; or (ii) the former globally synchronizes.
In case (i), the view MSk .ths(ik ).view becomes as high as
the view MS1 .ths(i1 ).view because the read and write are rasynchronized. This is impossible because it conflicts with theassumption. In case (ii), the effect is limited: MS0k is the sameas MSk except the effect of the event α1 . More specifically, MSk ’s
memory may contain an extra message produced by α1 and thethreads other than i1 in MS0k are the same as those in MSk exceptthat every view in the former may be less than the corresponding
view in the latter. By monotonicity, MS0k has more behaviors thanMSk and thus we can construct such an execution.

raand we will find a corresponding =⇒-step that preserves the simulation relation:
MS0n =⇒(in+1 ,αn+1 ) MS0n+1 .
raThanks to the simulation relation, there exists MS0n+1 such thatraMS0n =⇒(in+1 ,αn+1 ) MS0n+1 . If αn+1 is not reading (i.e., neithera read nor an update event), it is immediate from the semantics thatthe simulation relation is preserved. Now suppose αn+1 is reading
hx@ti with the access mode or , and let k be such an index that
αk is writing hx@ti with the access mode ow , and R (and Rra ) bera
the released view of hx@ti in the =⇒-execution (and =⇒-execution,
respectively).
Now we proceed by a case analysis:

Lemma 7 (Step reorder). Suppose we have a release-acquire
executionraCase ow , or w ra.
Note that the current & acquire views of MSn+1 .ths(in+1 )and MS0n+1 .ths(in+1 ) may diverge only due to the discrepancy of the hx@ti’s released views (R and Rra ), and theread’s access mode (or for the =⇒-machine, and or t ra forra⇒-machine). A similar argument applies to the other mathe =chine state components in the simulation relation. Hence itsuffices to show that R = Rra and or = or t ra, whichcome clearly from the assumption: in particular we have R =MSk .ths(ik ).view.cur = MS0k .ths(ik ).view.cur = Rrathanks to ow w ra.
Case MS0k .ths(ik ).view.cur ≤ MS0n .ths(in ).view.cur.
Since the released view Rra = MS0k .ths(ik ).view.cur ofhx@ti is already incorporated in the current view, a similarargument also applies here.

ra

MS =
⇒(i1 ,α1 ) MS1 =⇒(i2 ,α2 ) MS2
such that one of α1 and α2 is not globally synchronizing andMS1 .ths(i1 ).view 6≤ MS2 .ths(i2 ).view .
Then we have i1 6= i2 and MS01 satisfying
MS =⇒(i2 ,α2 ) MS01 =⇒(i1 ,α1 ) MS2 .
raraif the following conditions hold:MS =⇒(i1 ,α1 ) MS1 =⇒(i2 ,α2 ) · · · =⇒(in ,αn ) MSnrarasimulates a =⇒-execution

Lemma 6 (Step removal). Suppose we have a release-acquire
executionra

Proof of DRF-RA (Theorem 2). It suffices to show that (i) the exra
istence of a rlx-race in the =⇒-machine implies that in the =⇒ramachine, and (ii) the behavior in the =⇒-machine and that in thera⇒-machine coincide if P is rlx-race-free in the ==⇒-machine. Then
Theorem 1 concludes the proof.
We prove both (i) and (ii) by a single simulation argument. Werasay an =⇒-execution
MS00 =⇒(i1 ,α1 ) MS01 =⇒(i2 ,α2 ) · · · =⇒(in ,αn ) MS0n

Then we annotate promise-free and release-acquire steps withthe executed thread ids and memory events, denoted =⇒(i,α) andra=⇒(i,α) .
raFirst, we prove two key lemmas for =⇒: one for removing anintermediate step, and another for reordering adjacent steps.

rainterpreted as if they are all ra-accesses, and (ii) a machine step
consists only of one thread step. Note that the second condition does
not affect the semantics, since a machine state without promises isvacuously consistent.

raProof. Basically a similar argument as in the previous lemma applies
here: (i) α2 should not read α1 ; and (ii) the earlier step with α2does not affect the later step with α1 since α1 or α2 is not globally
synchronizing.
ra

Now we prove DRF-RA. Let =⇒ be identical to =⇒ in Theorem 1,
except that (i) rlx and pln accesses in program transitions are16

its interleaving behaviors if P is properly locked in all interleaving
executions.
We prove both (i) and (ii) by a single simulation argument. We
say an interleaving execution

Otherwise.
ra⇒-execution by reIn this case, we construct a rlx-race in the =peatedly applying the step-removing Lemma 6 to the execution:MS0k−1 =⇒(ik ,αk ) MS0k =⇒(ik+1 ,αk+1 ) · · · =⇒(in ,αn ) MS0n ,
ra

ra

ra

ra
ra
MS0j−1 =⇒(ij+1 ,αj+1 ) MS00j+1 · · · =⇒(in ,αn ) MS00n ,

ra

ra

ra

nfra

simulates an ==⇒-execution
ra

MS0 =
⇒(i1 ,α1 ) MS1 =⇒(i2 ,α2 ) · · · =⇒(in ,αn ) MSn ,if the following conditions hold:If we prove that given any ==⇒-execution of length n there exists
a simulating interleaving execution, then we are done as follows.
nfra
Given any (possibly infinite) ==⇒-execution and any number ofsteps n, we can find an interleaving execution of length n leading to
the same machine state with the same sequence of observable events(i.e., system calls). Thus, any arbitrarily long observation on an
nfra==⇒-execution cannot be distinguished from that on an interleaving
nfra
execution. Also, if there is any ==⇒-execution leading to a ra-racymachine state, we can find a simulating interleaving execution to an
improperly locked machine state by the simulation argument.
Now it suffices to prove the simulation theorem by induction
on the length n. The base case is trivial. For an induction step,
let’s assume that we have a simulating execution of length n, given
as in the above definition of simulation. Suppose we have a stepnfra
MSn ==⇒in+1 ,αn+1 MSn+1 . Then we need to find a simulatinginterleaving execution of length n + 1 that starts from MS0 andending in MSn+1 . If the event αn+1 is neither a read, a write, norraan update, then the execution MS00 ... MS0n =⇒(in+1 ,) MSn+1 isinterleaving, so we are done.
Thus suppose that αn+1 is accessing (i.e., a read, a write, or an
update event on) a location x and does not satisfy the interleaving
condition (i.e., does not read the latest message nor writes with agreatest timestamp). By definition of the interleaving condition, we
can find an event writing to x whose timestamp is bigger than thatof the event αn+1 . Let’s write αk and tk for the first such event (i.e.,with the smallest index k) and its timestamp.
Now, by exactly the same argument as in Theorem 2, we can remove all steps MSj such that k ≤ j ≤ n and MSj .ths(ij ).view ≥MSk .ths(ik ).view. Then we have a race between αk and αn+1 .
The resulting execution is also interleaving because removing a stepfrom an interleaving execution always results in an interleaving
execution. Thus, by the proper locking assumption, it follows that
αk and αn+1 are accessing the same lock location.
Now we will construct an interleaving execution from MS0 to
MSn+1 that simulates the given execution. For this, we repeatedly
apply the step-reordering using Lemma 7 as follows. First, wefind the first event, say αj , such that k ≤ j ≤ n + 1 andMSj .ths(ij ).view.cur.rlx(x) < tk . Then we can move down
the event to just before αk using Lemma 7. We repeat this processuntil we move αn+1 down to just before αk . This is possible
because we have MSn+1 .ths(in+1 ).view.cur.rlx(x) < tk . Also
note that this process does not reorder system calls because we
assume that system calls synchronize on lock locations (i.e., making
the view on lock locations to be up-to date).
Finally we will show that such a reordering does not breakthe interleaving condition for all existing events and furthermore
make αn+1 to satisfy the interleaving condition. The latter holds
trivially by construction because αk was the first event with respect
to which αn+1 violates the interleaving condition. The former holds
as follows. In order to break the interleaving condition, we need to0such that MS000
n .ths(in+1 ).st = MSn .ths(in+1 ).st and0
ik is not executed at all from MSk−1 to MS000
n . Hence
0MS000
n .ths(ik ).st = MSk−1 .ths(ik ).st, thus ik and in+1
race in MS000
n .

A.1

ra

nfra

MS0k−1 =⇒(il ,αl ) MS000⇒(iu ,αu ) · · · =⇒(in ,αn ) MS000
l =
n ,
ra

ra

0
1. (i01 , α10 ), ... , (i0n , αn
) is a reordering of (i1 , α1 ), ... , (in , αn )such that the order of system calls is preserved; and2. MS0 = MS00 and MS0n = MSn .

such that MS00n .ths(in+1 ).st = MS0n .ths(in+1 ).st. By repra
etition, we have an =⇒-execution:raMS00 =⇒(i01 ,α01 ) MS01 =⇒(i02 ,α02 ) · · · =⇒(i0n ,α0n ) MS0nraso that ik (attempting to write to x with ow ) and in+1 (attempting to read from x with or ) race in a reachable machine state.
Let j ∈ [k, n) be the last such an index that MS0j .ths(ij ).view.curra⇒6≤ MS0n .ths(in ).view.cur. By Lemma 6 there exists an =execution:

Proof for DRF-LOCK

In this section, we assume that we do not have sc-operations.
To state a DRF theorem on properly locked programs, we classify
locations into normal locations and lock locations and suppose locklocations are accessed only by the acquire and release operations, as
defined as follows:
acquire(l) {release(l) {while !CAS(l, 0, 1, acqrel) do skip;
lrel := 0;}}
Furthermore, we say a machine state MS is properly locked, if:
1. If two different threads can take a step accessing the same
location, then both accesses are reads, or the location is a locklocation; and2. If a thread can release a lock, say l, then the value of l in MS’s
memory is 1.
sc

Theorem 8 (DRF-LOCK). Let =⇒ denote the steps of the interleavsc
ing machine. Suppose that every machine state that is =⇒-reachable
from the initial state of a program P is properly locked. Then, thebehaviors of P according to the full machine coincide with thosescaccording to the =⇒-machine.
ra⇒-execution is interleaving if any reading
Proof. We say that an =step reads from the message with the greatest timestamp and any
writing step writes a message with a timestamp greater than any
scexisting message’s timestamp. It is obvious that the =⇒-machine israequivalent to the interleaving =⇒-machine (which we simply callthe interleaving machine), and thus we identify them.
raFirst of all, for any =⇒-execution E (i.e., a finite or infinitera⇒-steps), it is easy to see that removing all failed
sequence of =raacquire steps from the execution still yields a valid =⇒-execution
E 0 with the same behavior (i.e., the same sequence of system calls).
Furthermore, if E is a finite execution leading to a ra-racy machinenfra
rastate, then so is E 0 . We will simply say ==⇒-executions for =⇒executions with no failed acquire steps.
From this observation and Theorem 2, we can easily see thatnfra
it suffices to prove that (i) the existence of a ra-race in an ==⇒execution of P implies a violation of proper locking in an interleavnfra
ing execution of P; and (ii) the ==⇒-behaviors of P coincide with17

reorder two events α, β to β, α such that they are accessing the same
location and at least one of them is writing. During the reordering
process, suppose we meet such a reordering for the first time. Then,the execution before the reordering is interleaving because we areabout to break the condition for the first time. Since α and β are
racing on the same location, they both have to be lock operations (i.e.,
successful acquire or release). By the proper locking assumption,
we have only two possibilities: α is a release and β is an acquire; or
α is an acquire and β is a release. The former case is a contradiction
because β reads what α writes due to the interleaving condition,
which makes β’s view as high as α’s. The latter is a contradiction
too because after reordering the execution up to β is still interleaving
but the machine state before β is not properly locked. Thus we canconclude that the reorderings do not break the interleaving condition.
A.2

if (y_acq) {if (z) {
x = 1
}
}
||
Thread 3:
if (w_acq) {z=1} else {y=1 rel}Counterexample to Promise-Free DRF & DRF-RA

if (x) {
z=1;
a=1
}

Re-certifying promises at each step is necessary for PromiseFree DRF (Theorem 1) and DRF-RA (Theorem 2). Without recertification, one can get additional behaviors:
Thread 1:

The outcome a=1 (which contradicts both the Promise-Free DRF
and the DRF-RA theorems) would be allowed by first executing
w=1 and then promising z=1 in thread 3. Then, thread 3 can read
w=0 (now the promise can no longer be certified) and write y=1. At
the end, the promise can be fulfilled by the final z=1 write.

w=1 rel||Thread 2:18

B.

Proof of Theorem 5

Our proof of equivalence between the “declarative machine” and the promise-free machine shows that each machine simulates the other. Next,
we provide the simulation relation.
Definition 1. A timestamp assignment for an execution G is a function f : W → Time. A timestamp assignment f is extended for sets ofwrite events by f (A) = maxa∈A f (a).
Definition 2. An execution G induces the following additional derived relations:• G.urr = (rf? ; hb; [Fsc ])? ; (sc; [F])? ; hb? ∪ (rf; [Rwrlx ]; hb? ).
• G.rwr = urr ∪ (rf; hb? ).

Definition 3. An axiomatic machine state hΣ, Gi relates to a machine state MS = hTS, S, M i, denoted by hΣ, Gi ∼ MS , if the following
hold:• G is coherent.
• MS is well-formed.
• TS(i).prm = ∅ for every i ∈ Tid.
• Σ(i) = TS(i).st for every i ∈ Tid.
• There exists two timestamp assignments ffrom , fto for G for which the following hold:For every x ∈ Loc and a, b ∈ Wx , we have fto (a) < fto (b) iff ha, bi ∈ mo.
For every x ∈ Loc and a, b ∈ Wx , if ha, bi ∈ mo \ rf; rmw, then fto (a) 6= ffrom (b).
For every b ∈ W, if ha, bi 6∈ mo \ rf; rmw for all a, then ffrom (b) 6= 0.
For every x ∈ Loc, M (x) = {mb | b ∈ Wx }, where each mb satisfies:− mb .val = val(b).
− mb .to = fto (b) and mb .from = ffrom (b).
− mb .from = fto (a) if ha, bi ∈ rf; rmw.
− For every y ∈ Loc:
· mb .view.pln(y) = fto ({a ∈ Wy | ha, bi ∈ urr; rel}).
· mb .view.rlx(y) = fto ({a ∈ Wy | ha, bi ∈ rwr; rel}).
?
sc
For every x ∈ Loc, S(x) = fto (Wscx ∪ dom([Wx ]; rf ; hb; [F ])).
For every i ∈ Tid, TS(i) = hΣ(i), Vi , ∅i where Vi satisfies the following conditions for every x, y ∈ Loc:
− Vi .rel(y).pln(x) = fto (dom([Wx ]; urr; [WAra∪ Frel ]; [Ei ])).
y− Vi .rel(y).rlx(x) = fto (dom([Wx ]; rwr; [WAra∪ Frel ]; [Ei ])).
y− Vi .cur.pln(x) = fto (dom([Wx ]; urr; [Ei ])).
− Vi .cur.rlx(x) = fto (dom([Wx ]; rwr; [Ei ])).
− Vi .acq.pln(x) = fto (dom([Wx ]; urr; (rel; rf; [RArlx ])? ; [Ei ])).
− Vi .acq.rlx(x) = fto (dom([Wx ]; rwr; (rel; rf; [RArlx ])? ; [Ei ])).

19