Promising Compilation to ARMv8 POP∗
Anton Podkopaev1 , Ori Lahav2 , and Viktor Vafeiadis2
1
2

a.podkopaev@2009.spbu.ru, SPbU, JetBrains Research, St. Petersburg, Russia{orilahav,viktor}@mpi-sws.org, MPI-SWS, Kaiserslautern, Germany

Abstract
We prove the correctness of compilation of relaxed memory accesses and release-acquire fencesfrom the “promising” semantics of Kang et al. [12] to the ARMv8 POP machine of Flur et al. [9].
The proof is highly non-trivial because both the ARMv8 POP and the promising semantics
provide some extremely weak consistency guarantees for normal memory accesses; however, they
do so in rather different ways. Our proof of compilation correctness to ARMv8 POP strengthens
the results of the Kang et al., who only proved the correctness of compilation to x86-TSO andPower, which are much simpler in comparison to ARMv8 POP.
1998 ACM Subject Classification F.3.1 Specifying and Verifying and Reasoning about Programs
Keywords and phrases ARM, Compilation Correctness, Weak Memory Model
Digital Object Identifier 10.4230/LIPIcs.ECOOP.2017.69

1

Introduction

One of the major unresolved topics in the semantics of programming languages has to dowith giving semantics to concurrent shared-memory programs. While it is well understoodthat such programs cannot follow the naive paradigm of sequential consistency (SC) [15], it
is not completely clear what the right semantics of such concurrent programs should be.
At the level of machine code, the semantics varies a lot depending on the hardware
architecture, which is only loosely specified by the vendor manuals. In the last decade,academic researchers have produced formal models for the mainstream hardware architectures(e.g., x86-TSO [23], Power [22, 5], ARMv8 POP [9]) by engaging in discussions with hardware
architects and subjecting existing hardware implementations to extensive tests.
In this paper, we will focus on the ARMv8 POP model due to Flur et al. [9], whichis arguably the most advanced such hardware memory model.1 Operational in nature, it
models many low-level hardware features that affect the execution of concurrent programs.
These include the hardware topology, the non-uniform propagation of messages to otherprocessors, the reordering of messages, processor-level out-of-order instruction execution,
branch prediction, local decisions on the coherence of overwritten writes, and so on. The
ARMv8 POP model is in certain ways substantially weaker than other hardware memory
models. For example, it allows the outcome a = 1 of the following program (see [13]):a := [x]; //1[x] := 1;∗1

b := [x];[y] := b;c := [y];[x] := c;(ARM-weak)An extended version of this paper with a technical appendix can be found in [20].
We would like to point out that the ARMv8 POP model is not the latest model for ARM. In March 2017,
version 8.2 of the ARM reference manual [1] introduced a substantially stronger “multi-copy-atomic”
model, whose formal axiomatic definition became available on 27 April 2017 [3]. The new model
disallows the weak behaviors of the ARM-weak and WRC+data+addr examples discussed in this paper.

© Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis;
licensed under Creative Commons License CC-BY
31st European Conference on Object-Oriented Programming (ECOOP 2017).
Editor: Peter Müller; Article No. 69; pp. 69:1–69:28
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

69:2

Promising Compilation to ARMv8 POP

where all variables are initially 0. In essence, as we will explain in Section 2, the hardware
may propagate the [x] := 1 store to the second thread, then write [y] := 1 and propagate
it to the third thread, execute the third thread, and propagate its store to the first thread
before the a := [x] load returns. In contrast, Power and x86-TSO both forbid this outcome.
At the level of programming languages, the main problem is to design a memory modelthat enables efficient compilation across a wide range of hardware platforms and yet provides
suitable high-level guarantees, such as reduction to SC in the absence of data races andtype safety even in the presence of racy code. While many attempts to solve this problem
have been made in the past [8, 19, 25, 11, 21], including the Java [18] and C/C++11 [7]memory models, almost all have been found to be lacking in one way or another, either notsupporting certain compiler optimizations or allowing “out of thin air” behaviors.
Recently, however, Kang et al. [12] made a breakthrough and introduced a memory
model that claims to satisfy both desiderata. Their model is also operational, but includes arather non-standard step, according to which a thread can promise to perform a write in
the future. While such promise steps are suitably restricted, once a promise is made, otherthreads can read from the promised write, even before the promise is fulfilled. Promises
allow the weak behavior of the ARM-weak program: intuitively, the first thread may promise
to write [x] := 1, the second and third threads may then execute writing 1 to y and x
respectively, and the first thread can then execute reading a = 1 from the third thread andfinally fulfilling its promise to write [x] := 1.
While the Promise machine allows this surprisingly weak behavior of the ARM-weakexample, compilation from the promise semantics to the ARMv8 POP machine has not yet
been shown to be sound. In their paper, Kang et al. mention the ARM-weak program, but
do not verify compilation to ARMv8 POP; they only prove compilation correctness to thesubstantially simpler x86-TSO and Power models.
In this paper, we fill this gap and prove the correctness of compilation from a subset of thepromise model to the ARMv8 POP model. The subset of promise model we handle is quite
minimal—it contains relaxed loads and stores, as well as release and acquire fences—but
exposes the following three main challenges we had to overcome in the compilation proof.
Firstly, the two machines are very different. The ARM machine executes instructions
possibly out of program order and in multiple steps: it issues the instruction, propagatesit to one thread at a time, satisfies read instructions—all in different steps. In contrast,
the Promise machine executes instructions in a single step and according to program
order (except for promised writes).
Secondly, the key technical device used in the compilation proof to the Power model is notapplicable to the ARMv8 POP model because it can execute anti-dependent instructions
out of order as in the ARM-weak program (see discussion in Section 10).
Thirdly, although both memory models are operational, compilation correctness cannot
be shown by a standard forward simulation. The reason is that in the ARM machine
writes to a specific location are not necessarily totally ordered during the execution;
they only become totally ordered once they are all propagated to the memory, which
may happen at the very end of the execution. In the Promise machine, however, writes
are totally ordered by timestamps from the point they are issued (or promised); so asimulation proof would have to “guess” the correct ordering of the writes.
To overcome this final challenge, we introduce an intermediate machine, which extends the
ARM machine recording timestamps for each write, and views for each threads and message.
We show that this intermediate machine has the same behaviors as the ARM machine, andthat the Promise machine can simulate the intermediate machine’s behaviors.

Promising Compilation to ARMv8 POP

69:3

A secondary contribution of this paper is to provide a number of results about the ARMv8
POP model, which may be of general interest, e.g., in compiling from other language-level
memory models to ARMv8 POP.
In the remainder of this paper, we first introduce the ARMv8 POP and Promise models
informally (Section 2), and present the high-level structure of the proof (Section 3). Then, in
Sections 4 to 9 we present the ARMv8 POP, intermediate, and Promise machines formally,
and relate them to one another. We conclude with a discussion of related and future work.

2

Models through Examples

We start by discussing the ARM [9] and the Promise [12] machines on a couple of small
programs, litmus tests, like this:[x] := 1;[y] := 1;

a := [y]; //1
b := [x]; //0(MP)

Here a, b stand for local variables (registers) and x, y are distinct memory locations shared
between threads. The program syntax of the ARM machine programs slightly differs fromthe syntax of the Promise machine programs. We apply the following compilation scheme:
Promise:[x]rlx := aa := [x]rlx

fence(acquire)fence(release)ARM:[x] := aa := [x]dmb LD

dmb SYAs the compilation scheme is a bijection, we present programs in the ARM syntax only. For
every program we suppose that locations are initialized with 0. To refer to a specific behaviorof the program, we annotate read instructions with values expected to be read (e.g., //1).
The ARM Machine The ARM machine [9] consists of two components, a thread subsystem
and a storage subsystem. Roughly speaking, the former corresponds to processors’ per-thread
control units [10], which fetch and execute instructions, and send store/load memory requests
to the storage subsystem. The latter represents the memory hierarchy including caches,
store/load buffers, and the main memory. A state of the storage subsystem can be represented
graphically as a hierarchy of buffers, which are lists of memory requests.
Let’s execute the MP program in the ARM machine and get a = 1 and b = 0. One wayof getting this behavior is for the thread subsystem to issue the write (or read) requests
out-of-order to the storage subsystem. However, there is another way in which the outcome
a = 1, b = 0 is possible. First, the thread subsystem issues all requests in program order.
Thread 1
Thread 2[y] := 1
b := [x][x] := 1
a := [y]The main memory[x] := 0; [y] := 0

Thread 1

Thread 2[x] := 1

Thread 1

Thread 2[x] := 1

b := [x]a := [y][y] := 1

b := [x][y] := 1

The main memory[x] := 0; [y] := 0

The main memory[x] := 0; [y] := 0

After that, the storage subsystem reorders the independent requests [x] := 1 and [y] := 1,
and flows the requests [y] := 1, a := [y], and b := [x] from the bottom of the corresponding
buffers to the common buffer. Once the read request a := [y] follows [y] := 1 directly ina buffer, the storage subsystem is able to satisfy the read from the write and send a read

ECOOP 2017

69:4

Promising Compilation to ARMv8 POP

response, a = 1, to the thread subsystem. Finally, the storage subsystem flows [y] := 1 andb := [x] to the main memory, satisfying the latter from the initial write [x] := 0.
Suppose that the outcome a = 1, b = 0 is undesirable. To outlaw it, one can put dmb SY,
a full fence, between the writes2 in the first thread and dmb LD, a load fence, between thereads in the second thread:[x] := 1;
dmb SY;[y] := 1;

a := [y]; //1
dmb LD;b := [x]; //0 – impossible(MP-SY-LD)

The fence in the first thread forces the thread to issue [x] := 1, dmb SY, and [y] := 1
to the storage subsystem in order. Reordering of [x] := 1 and [y] := 1 in the storage
subsystem is also impossible, as the request dmb SY is not reorderable with any request andstays between them. It guarantees that once [y] := 1 is propagated to the common buffer,[x] := 1 is propagated there as well. The fence dmb LD forbids to issue b := [x] until
a := [y] is satisfied. So if a := [y] is satisfied from [y] := 1, [x] := 1 is propagated to thecommon buffer or to the main memory, and b := [x] can be satisfied only from it. So, if
a = 1 then b = 1.
In the discussed executions, it is very important that the storage subsystem is able toreorder some requests but not others. The definition of the reordering relation ,→ is following:
I Definition. A request eold and a request enew are reorderable, denoted eold ,→ enew , ifneither of them is an SY fence and they operate on different locations.
In this paper, we consider a slightly weakened version of Flur et al.’s model [9], whichissues dmb SY requests to the storage subsystem but not dmb LD requests. This allows more
behaviors than the original model.3 As we managed to prove compilation correctness to a
weaker model, the result is also applicable to the original model.
The Promise Machine The Promise machine [12] is very different from the ARM machine.
There is no sophisticated storage subsystem. The memory, M , is simply a set of annotatedwrites, so-called messages, issued by all threads up to the moment. Each message has atimestamp, an element of a totally ordered set, which is unique among messages to the same
location in the memory. Except for promises, which we discuss later in the section, the Promise
machine executes instructions in program order. However, reads have a nondeterministic
semantics: when a thread performs a read, it chooses any message from the memory subject
to some conditions. The message has to be to the corresponding location and not to be too“old”: if a thread has observed (i.e., read from) a message to location x with timestamp τ , itcannot subsequently read from a message to x with timestamp τ 0 < τ .
To enforce this restriction, as well as similar restrictions on timestamps of read messages
that arise from the use of fences, the Promise machine uses so-called views—maps fromlocations to timestamps. Each message in the memory is annotated with a message view,and each thread maintains three views: view cur , view acq , and view rel . The main thread view,
view cur , maps each location to the greatest timestamp of all messages of this location thatwere observed by the thread. For example, if a thread’s view cur equals to [z@2, w@4], it2

One could equivalently put a store fence, dmb ST, but that does not correspond to anything in thepromise model, as well as in the C/C++ model.
3
To show this, consider that dmb LD requests are issued, but are reorderable with any request. Thatwould weaken the original semantics. But this is the same as not issuing the dmb LD requests at all.

Promising Compilation to ARMv8 POP

69:5

means the thread has observed the write to the location w with the timestamp 4. The otherviews— those included in messages, as well as the thread views view acq and view rel — areused in combination with fences.
The weak behavior of MP is observable on the Promise machine quite easily. At the
beginning of the execution, the memory contains only initial writes:
M = {hx : 0@0, [x@0]i, hy : 0@0, [y@0]i}
T 1.view cur = [x@0, y@0]; T 2.view cur = [x@0, y@0]
The first thread T 1 may perform the writes:
M = {hx : 0@0, [x@0]i, hy : 0@0, [x@0]i,
hx : 1@1, [x@1, y@0]i , hy : 1@1, [x@0, y@1]i }T 1.view cur = [x@ 1 , y@ 1 ]; T 2.view cur = [x@0, y@0]
Now the second thread T 2 can read from the newly added message hy : 1@1, [x@0, y@1]iand the initial write hx : 0@0, [x@0]i.
The Promise machine counterparts of the SY and LD fences, release and acquire fences
correspondingly, are sufficient to outlaw a = 1, b = 0 as in the case of the ARM machine.
The fence(release) in the first thread T 1 enforces the message view of [y] := 1 to include
the timestamp of [x] := 1, and if the second thread T 2 reads from the message, then thefence(acquire) updates the second thread’s view cur with the message view. Let’s see how it
works.
In the beginning, all views are the same. When the first thread T 1 performs the firstwrite, it updates view cur , but view rel remains the same. The message view of the newly
added write equals to the pointwise maximum of view rel and the timestamp of the write
itself, [x@1] = (λ`. if ` = x then 1 else 0) (the latter is called a singleton view).
M = {hx : 0@0, [x@0]i, hy : 0@0, [y@0]i, hx : 1@1, [x@1, y@0]i }T 1.view cur = [x@ 1 , y@0]; T 1.view acq = [x@ 1 , y@0]; T 1.view rel = [x@0, y@0];
T 2.view cur = [x@0, y@0]; T 2.view acq = [x@0, y@0]; T 2.view rel = [x@0, y@0];
After that the first thread T 1 executes the release fence, which makes its view rel to be equal
to view cur :M = {hx : 0@0, [x@0]i, hy : 0@0, [y@0]i, hx : 1@1, [x@1, y@0]i}
T 1.view cur = [x@1, y@0]; T 1.view acq = [x@1, y@0]; T 1.view rel = [x@ 1 , y@0];
T 2.view cur = [x@0, y@0]; T 2.view acq = [x@0, y@0]; T 2.view rel = [x@0, y@0]
Then, the first thread T 1 performs the second write, again attaching to it a view which isthe pointwise maximum of T 1.view rel and the timestamp of the write itself:
M = {hx : 0@0, [x@0]i, hy : 0@0, [y@0]i,
hx : 1@1, [x@1, y@0]i, hy : 1@1, [x@1, y@1]i }T 1.view cur = [x@1, y@ 1 ]; T 1.view acq = [x@1, y@ 1 ]; T 1.view rel = [x@1, y@0];
T 2.view cur = [x@0, y@0]; T 2.view acq = [x@0, y@0]; T 2.view rel = [x@0, y@0];
When the second thread T 2 reads from the newly added write, it updates its view acq withthe message view:
M = {hx : 0@0, [x@0]i, hy : 0@0, [y@0]i,
hx : 1@1, [x@1, y@0]i, hy : 1@1, [x@1, y@1]i}
T 1.view cur = [x@1, y@1]; T 1.view acq = [x@1, y@1];
T 1.view rel = [x@1, y@0];
T 2.view cur = [x@0, y@0]; T 2.view acq = [x@ 1 , y@ 1 ]; T 2.view rel = [x@0, y@0];

ECOOP 2017

69:6

Promising Compilation to ARMv8 POP

The execution of the acquire fence makes the second thread’s view cur to be equal to its
view acq :M = {hx : 0@0, [x@0]i, hy : 0@0, [y@0]i,
hx : 1@1, [x@1, y@0]i, hy : 1@1, [x@1, y@1]i}
T 1.view cur = [x@1, y@1];
T 1.view acq = [x@1, y@1]; T 1.view rel = [x@1, y@0];
T 2.view cur = [x@ 1 , y@ 1 ] T 2.view acq = [x@1, y@1] T 2.view rel = [x@0, y@0]
And now thread T 2 is not able to read from hx : 0@0, [x@0]i, as T 2.view cur (x) = 1 > 0,
which rules out the outcome a = 1, b = 0.

2.1

A More Complex Behavior

Both machines guarantee that a read instruction cannot be satisfied from a same thread’s
write which follows the read in program order. They do, however, allow to get a = 1 during
an execution of the program presented in Section 1:
a := [x]; //1[x] := 1;

b := [x];[y] := b;c := [y];[x] := c;(ARM-weak)

The ARM Machine The behavior may be reproduced by the ARM machine if the first
and the second threads share a common buffer, which is not observable by the third thread.
The machine issues the two requests of the first thread and the read request of the second
thread, and propagates them to the common buffer. Then, the storage subsystem satisfies
read b := [x] from [x] := 1, and the second thread issues [y] := 1. The storage
subsystem propagates it to the common buffer, reorders it with the first thread’s requests,
and propagates it to the lowest buffer and to the memory.
Thread 1

Thread 2

Thread 3

Thread 1

b := [x][x] := 1
a := [x]Thread 2

Thread 3[x] := 1
a := [x]The main memory[x] := 0; [y] := 0

The main memory[x] := 0; [y] := 1

Next, the third thread issues c := [y], and the storage propagates it to the memory, where
it is satisfied with response c = 1. Now the storage sends response c = 1 to the third thread,
it issues [x] := 1, and the storage subsystem propagates it to the lowest buffer.
Thread 1

Thread 2

Thread 3[x] := 1
a := [x]c := [y]The main memory[x] := 0; [y] := 1

Thread 1

Thread 2

Thread 3[x] := 1
a := [x][x] := 1
The main memory[x] := 0; [y] := 1

The storage subsystem propagates a := [x] to the lowest buffer and satisfies it from [x] := 1.

Promising Compilation to ARMv8 POP

69:7

The Promise Machine Conforming to its name, the Promise machine uses promises toachieve the same behavior: a thread T may nondeterministically promise to write a value
val to a location ` at some point in the future. When a thread T makes a promise, it addsh` : val@τ, _i, where τ has not been used as a timestamp yet and is greater than T.view cur (`),
to the memory, making the promise available to read from for other threads. The promisetransition also adds the promise to a thread’s set of promises, T.promises, but it does not
update the thread’s views. After each transition of the machine, the thread which makesa step has to certify that it is able to fulfill all promises it made in the current state of
the memory running in isolation. The certification is used to outlaw self-satisfaction andcausality cycles [8] in an execution.
To get a = 1 in the program ARM-weak, the first thread has to promise, e.g., hx :1@2, [x@2]i. The thread can certify the promise—to read from the initial write to x withtimestamp 0 and then fulfill the promise by the second instruction. After the first threadpromised a write to x, the second thread reads from the promise, and adds hy : 1@1, [y@1]ito the memory. The third thread reads from it, and adds hx : 1@1, [x@1]i. Now the firstthread can read from hx : 1@1, [x@1]i getting a = 1 and fulfill the promise hx : 1@2, [x@2]i.

2.2More Abstract Storage Subsystem: POP

Flur et al. [9] present two versions of the storage subsystem for the ARM machine: Flowing
and POP (partial order propagation). We used the Flowing model to describe the previous
examples because it is more intuitive and easier to understand. However, the Flowing model
has a couple of features that make it hard to reason about the model. First, it is much easier
to have a partial order on requests inside of a buffer than to keep track of reorderings inside
it. Second, if we want to show that for every execution of a program in the ARM machinesome invariant holds, we have to consider every possible topology of buffers.
The POP model solves the aforementioned obstacles. There are no linear buffers andfixed topologies. The state of the POP storage consists of three components: Evt—a set ofrequests observed by the storage, Ord—a partial order on requests from Evt, and Prop—afunction mapping each thread identifier to a subset of Evt requests propagated to the thread.
If two requests e and e0 are ordered by Ord, Ord(e, e0 ), we write e <Ord e0 .
To understand how the POP model works and its connection to the Flowing model,
consider an execution of the following program:[x] := 1;

a := [x]; //1[y] := a;b := [y]; //1
c := [x + b ∗ 0]; //0(WRC+data+addr)

Here is a fake address dependency between reads in the third thread, so the thread does notknow the target address of the second read until b := [y] is satisfied. For this reason, thethird thread cannot issue the second read request before the first one is satisfied. Nevertheless,the behavior a = 1, b = 1, c = 0 is allowed due to the storage subsystem.
To reproduce the intended behavior in the Flowing model we have to choose the same
topology as in the previous example, which has a buffer observable to the first and the second
threads, but non-observable for the third one. Suppose that each thread issued a request
corresponding to its first instruction. Then we get the following Flowing state (on the left)
and the following POP state (on the right):44

For the sake of brevity we annotate the requests with labels and use the labels in the POP components.

ECOOP 2017

69:8

Promising Compilation to ARMv8 POP

Thread 1

Thread 2

m : [x] := 1

Thread 3

n : a := [x]o : b := [y]Evt = {k, l, m, n, o}
Ord = {(k, m), (k, n), (l, o)}Prop(T 1) = {k, l, m}Prop(T 2) = {k, l, n}Prop(T 3) = {k, l, o}k : [x] := 0; l : [y] := 0

When a request e is issued to the storage by a thread T , we add an Ord-edge (e0 , e) for eache0 , which is propagated to T and is not reorderable with e, e0 6,→ e. That is why there are
entries in Ord.
At this point the request m : [x] := 1 might be propagated to the (T 1, T 2) common
buffer. In terms of the POP model, this step corresponds to propagation of m : [x] := 1 toT 2:
Thread 1

Thread 2

Thread 3

n : a := [x]o : b := [y]m : [x] := 1

Evt = {k, l, m, n, o}
Ord = {(k, m), (k, n), (l, o), (m, n) }Prop(T 1) = {k, l, m}Prop(T 2) = {k, l, n, m }Prop(T 3) = {k, l, o}k : [x] := 0; l : [y] := 0

The propagation step adds m to Prop(T 2) and the (m, n) edge to Ord.
In general, when a request e issued by a thread T is propagated to a thread T 0 , we add(e, e0 ) to Ord for every request e0 , which is propagated to T 0 but not to T , if e and e0 are notreorderable (i.e., e 6,→ e0 ) and there is no backward edge (e0 , e) in Ord. In the execution, them and n requests are not reorderable because they operate on the same location x.
The storage subsystem may propagate n : a := [x] to the common buffer (in the Flowing
model) or, correspondingly, to thread T 1 in the POP model:
Thread 1

Thread 2

Thread 3
o : b := [y]n : a := [x]m : [x] := 1

Evt = {k, l, m, n, o}
Ord = {(k, m), (k, n), (l, o), (m, n)}Prop(T 1) = {k, l, m, n }Prop(T 2) = {k, l, n, m}
Prop(T 3) = {k, l, o}k : [x] := 0; l : [y] := 0

Now n : a := [x] can be satisfied from m : [x] := 1, as the former request follows the latterdirectly in the common buffer (the Flowing model), they are propagated to the same set of
threads (T 1, T 2) and there is no request in between them according to the Ord relation (thePOP model). After the read is satisfied, the second thread T 2 issues the write p : [y] := 1:
Thread 1

Thread 2

Thread 3

p : [y] := 1m : [x] := 1k : [x] := 0; l : [y] := 0o : b := [y]Evt = {k, l, m, o, p }Ord = {(k, m), (l, o), (l, p) }Prop(T 1) = {k, l, m}Prop(T 2) = {k, l, m, p }Prop(T 3) = {k, l, o}Promising Compilation to ARMv8 POP

69:9

The storage propagates p : [y] := 1 to the common buffer and then to the lowest buffer andto the main memory in the Flowing model, and to T 1 and T 3 in the POP model:5
Thread 1

Thread 2

Thread 3
o : b := [y]m : [x] := 1

Evt = {k, l, m, o, p}
Ord = {(k, m), (l, o), (l, p), (p, o) }Prop(T 1) = {k, l, m, p }Prop(T 2) = {k, l, m, p}
Prop(T 3) = {k, l, o, p }k : [x] := 0; p : [y] := 1

Then, o : b := [y] is propagated to the lowest buffer in the Flowing model, and to T 1 andT 2 in the POP model:
Thread 1

Thread 2

Thread 3

m : [x] := 1o : b := [y]Evt = {k, l, m, o, p}
Ord = {(k, m), (l, o), (l, p), (p, o)}Prop(T 1) = {k, l, m, p, o }Prop(T 2) = {k, l, m, p, o }Prop(T 3) = {k, l, o, p}k : [x] := 0; p : [y] := 1

After o : b := [y] is satisfied from p : [y] := 1, the machine may issue q : c := [x],propagate it to the main memory before m : [x] := 1 and satisfy it from k : [x] := 0.
At the end of the POP execution, all write and fence requests are propagated to all
threads. As a result, every pair of write requests to the same location is ordered by Ord,which induces a total order on writes to one location. We use this observation in our proof.
As the POP model is a sound relaxation of the Flowing model and it is more abstractand easier to reason about, we use the POP model in our proof.

3

Main Challenges and High-Level Proof Structure

A compilation scheme from one machine AM to another machine AM 0 is correct, if for any
program P and its compiled version P 0 each execution of P 0 on AM 0 corresponds to some
execution of P on AM . The standard way to prove it is to exhibit a simulation between themachines. This may be done by introducing execution invariants and mapping transitions of
AM 0 to transitions of AM .
There are three main problems one has to cope with to prove that the Promise machine
simulates the ARM machine:
1. Although all writes to a specific location are totally ordered in the end of an ARM
execution, they aren’t ordered during the execution. In the Promise machine, however,timestamps induce a total order on writes, which is decided much earlier—at the point
writes are issued (or promised).
2. In the ARM machine, while reading from a write request imposes restrictions on following
reads, there is no explicit counterpart of message views of the Promise machine.
3. The ARM machine allows out-of-order execution of instructions, whereas the Promise
machine, except for promises themselves, supports only in-order execution.

5

As there is no fixed topology in the POP model, p : [y] := 1 can even be propagated to T 3 before T 1.

ECOOP 2017

69:10Promising Compilation to ARMv8 POP

To address the first two challenges, we introduce an instrumented version of the ARM
machine, the ARM+τ machine. In this machine, each write request is annotated with (i) atimestamp, (ii) a set of writes and fences which are guaranteed to be observed by a thread
once it reads from the write request, and (iii) a view corresponding to the aforementioned
set. The timestamps of writes to a specific location have to reflect a total order in which
the writes are propagated to the main memory (in terms of the Flowing model) or to all
threads (in terms of the POP model). However, at the moment when the thread subsystem
issues a store request, the ARM machine cannot guarantee that the request will take any
specific position in the total order. It is, therefore, impossible to assign a timestamp to therequest at that moment. To solve this problem, the ARM+τ machine’s steps have additional
preconditions which guarantee acyclicity of the union of the partial order on requests in thestorage (the relation Ord) and the per-location timestamp order. These restrictions meanthat the ARM+τ machine may have potentially less behaviors than the ARM machine for agiven program. So we have to prove that the ARM+τ machine simulates the ARM machine
to be able to use it in the compilation correctness proof.
The third challenge makes it impossible to define a simple one-to-one or one-to-manycorrespondence between steps of the ARM and the Promise machines. To address thisproblem, we allow the Promise machine to “lag behind” the ARM machine. Consider thefollowing program fragment:[x] := 1;
dmb LD;a := [y];[z] := 1;
The ARM machine may first commit the fence dmb LD (step 1 ), then issue (propagate if
needed and satisfy) the read a := [y] (step 2 ), commit the write [z] := 1 (step 3 ), andonly after that commit the write [x] := 1 (step 4 ). The Promise machine cannot performthe corresponding steps in the same order. According to the simulation we propose for thecompilation correctness proof, the Promise machine does nothing when the ARM machine
performs the steps 1 and 2, so it starts to lag behind the ARM machine at this point. Thenit promises [z] := 1 at step 3. Finally, at step 4, it promises and fulfills the write [x] := 1and does everything left, as it is no longer blocked by the instruction [x] := 1.
To represent the lagging of the Promise machine, we have two simulation relations in
our proof, I and Ipre . The former relation forbids the Promise machine to lag behind too
much: if states of the ARM and the Promise machines are connected by I, then each threadof the Promise machine has executed all instructions from the maximal committed prefixof the corresponding ARM thread execution and is waiting for the next instruction to becommitted by the ARM thread. The latter relation states that there is one thread which isable to (and has to) execute the next instruction, as it is committed by the ARM thread.
We show that once states of the machines are related by Ipre , there is a finite number ofsteps, which the Promise machine has to make, to get to a state which satisfies I.
In our proof, we consider only terminating executions of the ARM machine, because
otherwise we would have to introduce “fairness” conditions on its speculative execution. For
instance, there is an execution of the following program, which infinitely issues read requests
to the storage without satisfying them:a := [x];if a 6= 0 goto −1;

Promising Compilation to ARMv8 POP

cmds
S: List S::= reg := [expr]| [expr 0 ] := expr 1| dmb ftype ARM| if expr goto k| reg := expr | nop
ftype ARM ::= SY | LD
expr::= reg | ` | uop expr
| bop expr 0 expr 1: Exprreg : Reg − a, b, c, ... (local variables)` : Loc− x, y, z, ... (locations)uop, bop − arithmetic operationsk∈Z
Figure 1 Syntax of ARM programs.

69:11

tapecell ::= R st read | W st write| F st fence ftype ARM| If st ifgoto k | Assign | Nop: TapeCell
sat-state ::= pln | inflight | com
st read::= none | requested `| sat sat-state htid, path, wr ` : vali
st write ::= none
| pending ` val| com bool ` val
st fence::= none | com
st ifgoto ::= none | taken | ignored
val : Val = Loc ∪ Z
Figure 2 ARM instruction state.

As we said in Section 2, the considered compilation scheme is bijection, so we assume
that programs for both machines are the same. Our compilation correctness theorem statesthat for every program and every terminating execution of the ARM machine there is aterminating execution of the Promise machine which ends with the same memory, i.e., thelast writes to each location are the same for both machines.
I Theorem 3.1. For all Prog and s, if Prog ` sinit −−−→∗ s and FinalARM (s, Prog),
ARMthen there exists p such that Prog ` pinit −−−−−→∗ p where FinalPromise (p, Prog) andPromisesame-memory(s, p).

4

The ARM Machine

In this section, we formalize the semantics of ARM POP machine of Flur et al. [9]. The
syntax of ARM machine programs is presented in Fig. 1. A program for the machine,
Prog : Tid → List S, consists of a list of instructions for each thread. Instructions arereads (reg := [expr]), writes ([expr 0 ] := expr 1 ), fences (dmb ftype ARM ), conditional
relative jumps (if expr goto k), local variable assignments (reg := expr), and no-operation
instructions (nop).
The thread subsystem of the ARM machine allows out-of-order and speculative executionof instructions. Moreover, it executes instructions non-atomically, i.e., many instructions
might be in the middle of their execution at the same moment. We represent a state of an
instruction instance via tapecell (see Fig. 2). Its syntax reflects the instruction syntax.
A read instance, st read , might be in one of the three following states: (i) none, the read is
fetched or restarted; (ii) requested `, the read has a load request from the location ` in thestorage subsystem; (iii) sat sat-state htid, path, wr ` : vali, the read has been satisfied from awrite instance (tid, path) with a value val. The sat-state field denotes if the read is satisfied
by an in-flight, i.e., not yet committed to the storage, write (inflight), the read is satisfied
from the committed write (pln), or the read is satisfied from the committed write and iscommitted itself (com).
A write instance, st write , might be (i) none, similarly to the read state; (ii) pending ` val,
the address and the value of the write is determined and a read from the same thread may

ECOOP 2017

69:12

Promising Compilation to ARMv8 POP

read from it; (iii) com bool ` val, the write is committed and, if bool = true, issued to thestorage subsystem (otherwise, it is observable only by same thread read instructions).
A fence instance, st fence , might be either committed (com) or not (none). A conditional
branch instance, st ifgoto , signifies that the control flow either jumps to k positions ahead(taken), proceeds to the next instruction (ignored), or is still undecided (none). Assignments
and nops instances are just fetched, but not executed.
Similarly to earlier work on the Power memory model [22], we may represent the instruction
state of a specific thread as a labeled direct acyclic graph (DAG), e.g.:c : If none (−2)
a : W (com true x 1)

b : If none 7
d : Assign

e : R (requested z)
f : Nopg : R (sat pln h5tid , [0, 1], wr y : 6i)

where vertices denote instruction instances, arrows represent the program order relation
between the instances, and vertices with two outgoing arrows signify branch instruction
instances, where the execution path has not yet been determined.
We identify an instruction instance by its thread identifier, tid, and a path : P ath , List N
from the root of the thread’s instruction DAG. It is encoded as a list of instruction positions
corresponding to the instruction instances on the path. For example, in the DAG above theinstruction instance a has a path [0], b—[0, 1], and f —[0, 1, 8, 9].
The instruction DAG of the thread is represented by a tape : Tape , P ath * TapeCell,a map from paths to tapecells. As a tape represents an instruction DAG, it is prefix-closed:
if a tape is defined for path, then it is defined for every (non-empty) prefix of path.
As multiple instructions may be in flight at any given moment, it is not possible to define
one per-thread state of local variables for a given moment of an execution. Consider thefollowing execution fragment:
i
0
1
2
3

cmds[i]a := [x];[y] := a;a := [z];[w] := a;

path
0
0, 1
0, 1, 20, 1, 2, 3tape(path)
R noneW noneR (sat pln h8tid , [0, 1, 2, 3], wr z : 9i)
W noneHere the read a := [z] is satisfied with a value 9, but a := [x] isn’t even issued to thestorage. It means that a is defined for the fourth instruction, but not for the second one.
To cope with these subtleties, we introduce two state functions regf, regf com : (List S ×Tape × P ath) → (Reg * Val), where regf(cmds, tape, path) and regf com (cmds, tape, path)
represent the state of the local variables just before the instruction instance indexed by path.
Their only difference is in the way they process satisfied but not yet committed reads (where
path : i denotes the extension of path with the instruction index i):6
∀i, j. cmds[i] = “reg := [expr]”∧tape(path) = R (sat sat-state h_, _, wr _ : vali) ∧ sat-state 6= com ⇒regf (cmds, tape, path : i : j) = regf (cmds, tape, path : i)[reg 7→ val] ∧regf com (cmds, tape, path : i : j) = regf com (cmds, tape, path : i)[reg 7→ ⊥].

6

The full inductive definition of the regf and regf com functions is given in the extended version of thepaper [20].

Promising Compilation to ARMv8 POP

69:13

For the previous example, the functions have the following values:
path
0
0, 1
0, 1, 20, 1, 2, 3

regf(cmds, tape, path)⊥⊥⊥[a 7→ val]

regf com (cmds, tape, path)⊥⊥⊥⊥

The variable maps is naturally extended to expression evaluators of type Expr * Val. For
path
path
the sake of brevity, we write [[−]]and [[−]]com (or [[−]] and [[−]]com ) for the evaluators
when values of the cmds, tape (and path) parameters are clear from the context.
The state of the storage subsystem, MPOP = hEvt, Ord, Propi, contains three components:
Evt ⊆ ReqSet—a set of memory requests in the storage; Ord ⊆ Evt × Evt—a partial orderon memory requests; and Prop ⊆ Tid × Evt—the set of requests that have been propagatedto each thread. A request, req, itself contains the thread, tid, and the instruction instance,
path, that issued the request, as well as some information, reqinfo, about the request:
reqinfo ::= rd ` | wr ` : val | dmb.
Specifically, read requests record the location to be read, while write requests record thelocation and the value to be written.
The full state of the ARM machine StateARM is a tuple hMPOP , iordf , tapef i, where MPOP
is the memory state, iordf : Tid → List ReqSet is a per-thread issuing order of read requests,
and tapef : Tid → Tape records the tape of each thread. The ARM machine allows to
issue read requests to the same location out-of-order, so it uses the issuing order to preserve
coherence among the reads (discussed in the Read satisfy description).
The initial state of the ARM machine contains initial writes to all locations, Evt init ,{h0tid , [], wr ` : 0i | ` ∈ Loc}, the writes are not ordered and propagated to all threads:
sinit , hMPOP = hEvt init , ∅, Tid × Evt init i, iordf = λtid. [], tapef = λtid. ⊥i.
Our version of the ARM machine has twelve possible transitions, which are shown in theextended version of the paper [20]. For simplicity, we present the transitions informally anddo not separate them into storage and thread transitions.
Fetch instruction tid path adds a new instruction instance with a none state to the tape ofthe thread tid.
Propagate e tid adds e to a set of requests propagated to tid. It has to check that all
requests e0 which are ordered before e by Ord, i.e., e0 <Ord e, are propagated to tid
as well. It also adds Ord-edges (e, e00 ) for every e00 , which isn’t reorderable with e andpropagated to e.tid but not to tid, to acknowledge that e is Ord-before e00 .
Branch commit tid path processes an if − goto instruction instance and chooses which
execution branch to drop, i.e., deletes instruction instances and storage requests belonging
to the branch.
Fence commit LD tid path checks if previous reads are committed.
Fence commit SY tid path checks if previous instruction instances in general are committed, and issues a fence request to the storage.
Write pending tid path ` val sets the write instruction instance to pending ` val, where `and val are an address and a value calculated by the corresponding evaluator.
Write commit tid path ` val sets the write instruction instance to com _ ` val. It issues awrite request to the storage in case there is no following committed writes to the same

ECOOP 2017

69:14

Promising Compilation to ARMv8 POP

location in thread’s tape. It restarts some satisfied load instances, which read from thesame location, and their dataflow dependents to preserve coherence. Previous branch
operators and fences have to be committed. All previous instructions must have fully
determined addresses, i.e., each address in a previous instruction instance has to be
determined by the corresponding com-evaluator.
Read issue tid path ` sends a read request to the storage, and adds it to the list of issued
read requests (the iordf (tid) component). It requires that previous fences are committed.
Read satisfy tid path tid 0 path 0 ` val and Read satisfy (fail) tid path tid 0 path 0 ` val
get the read request htid, path, rd `i satisfied from the write request htid 0 , path 0 , wr ` : vali,
if there are no requests between them in the storage. The transitions delete the readrequest from the storage. If there are no previous read instances, which issued a readrequest to the same location after the (tid, path) instance (according to iordf (tid)) andhave been satisfied from a different write, the former transition might be applied. It assigns
the instruction instance to sat pln htid 0 , path 0 , wr ` : vali and restarts some path-following
reads from the same location (and their dataflow dependents) to preserve coherence.
Otherwise, the latter transition might be applied, which restarts the (tid, path) instruction
instance.
Read satisfy from in-flight write tid path path 0 ` val assigns the corresponding instruction instance to sat inflight htid, path 0 , wr ` : vali, if there is a previous pending write(tid, path 0 ) and there are no writes to the same location in between the write and theread, as well as there are no same location reads satisfied from another write. It restarts
some path-following reads as in the case of the transition Read satisfy.
Read commit tid path checks that previous branches and fences are committed, all previous
instruction instances have a fully determined addresses, and assigns the instruction
instance to sat com _.

5

The Promise Machine

As mentioned in Section 2, the compilation scheme from Promise to ARM is a bijection; so
we may skip the definition of the Promise program syntax and use the ARM syntax.
The state of the Promise machine StatePromise is a tuple hMPromise , tsf i. The memory,
MPromise ⊂ Msg, is a set of write messages, h` : val@τ, viewi : Msg, which records thewrite’s location, ` : Loc, value, val : Val, timestamp, τ : Time = Q, and message view,
view : View = Loc → Time. The memory includes writes which are promised but not yet
fulfilled. In turn, tsf : Tid → T S is a per-thread state. A thread state, ts : T S, is a tuple
hpath, st, V , promisesi, where path is a pointer to the next instruction to be executed; st :Reg * Val is a variable state function; V = hview cur , view acq , view rel i : View × View × View
is a current, an acquire, and a release views of the thread; and promises ⊂ Msg is a set ofpromises which the thread made but has not fulfilled yet.
The initial memory of the Promise machine contains initial writes to all locations,init
MPromise, {h` : 0@0, view init i | ` ∈ Loc}, where view init , λ`. 0. The initial thread state’s
path points to the first instruction, variables are not defined, and the set of promises is
empty:
init
pinit , hMPromise, λtid. hpath = [0], st = ⊥, V = hview init , view init , view init i, promises = ∅ii.

Promising Compilation to ARMv8 POP

69:15

The main transition of the Promise machine is global:
label

0
Prog(tid) ` hMPromise , tsi −−−−−−−→ hMPromise, ts 0 i
Promise tid

000
Prog(tid) ` hMPromise, ts 0 i −−−−−−−→∗ hMPromise, ts 00 i

ts 00 .promises = ∅Promise tidlabel tid0
Prog ` hMPromise , tsf [tid 7→ ts]i −−−−−→ hMPromise, tsf [tid 7→ ts 0 ]i
PromiseOther transitions (−−−−−−−→) are defined for a specific thread. The main transition requires
Promise tid

a thread tid, which makes a transition, to certify that it is able to fulfill its promises, i.e.,there is an isolated execution of the thread with the current memory, which fulfills all thread’s
promises.7
The exact definitions of thread transitions might be found in the extended version of
the paper [20]. Here we present the transitions informally. All of them, except for Promise
write, execute the instruction pointed by the thread’s path component, and update path topoint to the next instruction.
Acquire fence commit makes the current view, view cur , of the thread to be equal to its
acquire view, view acq , which accumulates message views of writes read by the thread up
to the current point.
Release fence commit updates the release view, view rel , of the thread to match its current
view. Consequently, the message view of writes issued after executing the fence will
incorporate information about writes observed by the thread before the fence. In theoriginal version of the Promise machine [12] the Release fence commit transition has aprecondition that all unfulfilled promises of the thread must have empty message views.
In our version, the machine is even more restrictive: the thread cannot have any unfulfilledpromises. This restriction is easier to work with, and it is not too restrictive for thecompilation proof—the release fence is compiled to the full fence in the ARM machine,which forbids to commit following writes before the fence itself is committed.
Read from memory ` chooses a message, h` : val@τ, viewi, from memory with a timestamp,τ , greater than or equal to the current view value, view cur (`). The transition updates
thread’s view cur by [`@τ ], and view acq by view. It follows that such a message cannot bein the thread’s set of unfulfilled promises as it would make it impossible for the thread tofulfill the corresponding promise. Also, the transition updates the thread’s local variablemap, st.
Promise write h` : val@τ, viewi adds the message to the memory and to the thread’s setof promises. The target location, `, and the value, val, can be chosen arbitrarily. The
timestamp, τ , has to be unique among writes to the location. The message view equals
to a composition of the release view, view rel , and a singleton view [`@τ ].8 The transition
does not update the thread’s views. As we see, this transition is very non-deterministic.
However, it is restricted by certification.
Fulfill promise h` : val@τ, viewi removes the message from the thread’s promises, if (i)the current instruction is a write, (ii) its target location and value are ` and val, (iii) τis less than view cur (`), and (iv) view equals to view rel updated by [`@τ ]. The transition
updates view cur and view acq by [`@τ ].

7

In the original model, certification has to be made for all possible “future” memories. In the absenceof Read-Modify-Write operations, however, we can simplify that condition and perform certifications
starting only from the current memory.
8
This is more restrictive than in the original presentation [12], which allows to promise a write with anarbitrary message view.

ECOOP 2017

69:16

Promising Compilation to ARMv8 POP

The other rules (Branch commit, Local variable assignment, and Execution of nop) havestandard semantics.

6

Basic Properties of the ARM Storage

In this section we prove some properties of the ARM storage subsystem, which we use to
introduce timestamps to the ARM machine in the following section. In all lemmas we assume
some program Prog implicitly.
I Lemma 6.1. ∀s. sinit −−−→∗ s ⇒ s.Ord = (s.Ord \ ,→)+ ∧ s.Ord is acyclic.
ARM

Proof. The statement holds for the initial state, sinit . Consider possible mutations of thestorage. There are three types of storage operations. We assume that operations make atransition hEvt, Ord, Propi → hEvt 0 , Ord 0 , Prop0 i. Let’s check them:
Delete a read request e :Evt 0 = Evt\{e}, Prop0 = Prop\{(tid, e) | tid}, Ord 0 = (Ord\({e}×Evt)\(Evt×{e})\,→)+
Accept a request e from tid :Evt 0 = Evt∪{e}, Prop0 = Prop∪{(tid, e)}, Ord 0 = (Ord∪{(e0 , e) | Prop(tid, e0 ), e0 6,→ e})+Propagate a request e to tid :Evt 0 = Evt, Prop0 = Prop ∪ {(tid, e)},Ord 0 = (Ord ∪ {(e, e0 ) | Prop(tid, e0 ), ¬Prop(e.tid, e0 ), e 6,→ e0 , ¬(e0 <Ord e)})+Obviously, Ord 0 = (Ord 0 \,→)+ . As Ord 0 ⊆ Ord for the delete transition, the accept transition
adds edges only to a new request, and the propagate transitions checks if there is an edge(e, e0 ) in transitively closed Ord before adding (e0 , e), Ord 0 is acyclic.
J
The next two lemmas are proved in the similar way.
I Lemma 6.2. ∀s, e, e0 , tid. sinit −−−→∗ s ∧ e 6,→ e0 ∧ s.Prop(tid, e) ∧ s.Prop(tid, e0 ) ⇒ARM

e = e0 ∨ s.Ord(e, e0 ) ∨ s.Ord(e0 , e).

I Lemma 6.3. ∀s, s0 . s −−−→∗ s0 ⇒ s.Evt \ {e | e is a read request} ⊆ s0 .Evt.
ARM

I Lemma 6.4. ∀s, s0 . s −−−→∗ s0 ⇒ s.Ord ∩ (s0 .Evt × s0 .Evt) ⊆ s0 .Ord.
ARM

Proof. The following weaker version of the lemma holds as there is no storage transition
which deletes an Ord-edge between non-reorderable requests:∀s, s0 . s −−−→∗ s0 ⇒ (s.Ord ∩ (s0 .Evt × s0 .Evt)) \ ,→ ⊆ s0 .Ord
ARM

Now let’s prove the original statement. Fix e, e0 such that s.Ord(e, e0 ). If e 6,→ e0 , then thestatement holds as we have just shown. Otherwise, e and e0 are read or write requests todifferent locations. As s.Ord(e, e0 ) holds, by Lemma 6.1, there is a finite path in s.Ord frome to e0 such that each edge along the path connects non-reorderable requests.
Suppose that there is a fence request e00 in the path. Then, by transitivity of s.Ord,{(e, e00 ), (e00 , e0 )} ⊆ s.Ord. By the weaker version of the lemma and transitivity of s0 .Ord,{(e, e00 ), (e00 , e0 ), (e, e0 )} ⊆ s0 .Ord.
Consider that there is no fence request in the path. Then, by definition of ,→, the pathcomprises only requests to the same location. It contradicts that e 6,→ e0 .
JPromising Compilation to ARMv8 POP

7

69:17

Introduction of Timestamps to the ARM Machine

In this section, we show how to assign timestamps (τ ) represented by rational numbers to all
write requests in a terminating execution of the ARM machine. Let us fix some program
Prog, and consider a terminating execution:
Prog ` s0 −−−→ s1 −−−→ . . . −−−→ sn
ARM

ARM

ARM

where s0 = sinit , an initial state of the ARM machine, and sn = s is a final state, i.e., there
are no read requests in the storage, all requests are propagated to all threads, all instruction
instances are committed, and it is impossible to fetch any new instruction instance.
For a location ` and a set of memory requests Evt, we define Evt ` to be the set of all
write requests to the location ` in Evt. Formally,
Evt ` , {htid, path, wr ` : vali ∈ Evt | tid, path, val}.
There is no transition which deletes write requests from the storage, so s.Evt ` is the set of all
writes to a location ` which have been issued to the storage subsystem during the execution.
Fix a location `. We know that each request e from s.Evt ` is propagated to all threads,
as s is a final state. We also know that two different writes to the same location are notreorderable. As a consequence of it and Lemma 6.2, we have thatmo` , s.Ords.Evt `where RS , R ∩ (S × S)

S
is a total order on the writes to the location `. We define mo , ` mo` to be the union ofmo` for all locations mentioned in the execution. Using request indexes in the correspondingmo` sets, we define a timestamp mapping function:(index(mo` , e) if e = htid, path, wr ` : vali ∈ s.Evt;
mapτ (e) ,⊥otherwise.
Finally, we show that for every state si of the execution mosi .Evt ∪ si .Ord is acyclic.
I Theorem 7.1. ∀i ≤ n, mosi .Evt ∪ si .Ord is acyclic.
Proof. The statement obviously holds for s0 . Suppose that there exists j such that for alli < j the relation mosi .Evt ∪ si .Ord is acyclic, but mosj .Evt ∪ sj .Ord has a cycle. We knowthat mosn .Evt ∪ sn .Ord = sn .Ord has no cycles. So if there is a cycle in mosj .Evt ∪ sj .Ord,
it has to be “destructed” on the subexecution Prog ` sj −−−→∗ sn .
ARM

From this point on, we’ll distinguish Ord- and mo-edges. We call an edge an Ord-edge, if
it is in sj .Ord, and we call it an mo-edge, if it is in mosj .Evt \ sj .Ord.
Consider a shortest cycle in mosj .Evt ∪ sj .Ord. It has to contain an mo-edge, because
js .Ord is acyclic. The mo-edge (e, e0 ) connects two writes to some location ` and mapτ (e) <mapτ (e0 ). This edge is a part of the cycle, so there is a path from e0 to e by Ord- andmo-edges. We can break the path into mo-subpaths and Ord-subpaths. Let’s check thateach aforementioned Ord-subpath contains only one edge.
We pick an Ord-subpath, {e00i }i∈[0..k] . e000 and e00k are write requests, as they are connected
to other subpaths via mo-edges. By transitivity of sj .Ord (Lemma 6.1), sj .Ord(e000 , e00k ) holds,
so the subpath can be reduced to these two requests.
Thus, the shortest path from e0 to e in mosj .Evt ∪ sj .Ord contains only write requests.
ns .Ord contains all mo-edges from the path by definition of mo, and it contains each Ord-edge
from the path by Lemma 6.3 and Lemma 6.4. It contradicts acyclicity of sn .Ord.
J

ECOOP 2017

69:18

Promising Compilation to ARMv8 POP

Propagate e tid

label

Prog ` s −−−→ s0

Prog ` s −−−−−−−−−→ s0

label 6∈ {Propagate _ _, Write commit _ _ _ _}s0 .Ord ∪ tedges(s0 .Evt, Hτ ) is acyclic

ARM

ARM

label

Prog ` hs, H i −−−−−→ hs0 , H i
ARM+τPropagate e tid

Prog ` hs, H i −−−−−−−−−→ hs0 , H i
ARM+τWrite commit tid path ` val

0
Prog ` s −−−−−−−−−−−−−−−−−→ hMPOP, iordf 0 , tapef 0 i
ARM

tapef 0 (tid, path) = W (com im ` val)tape , s.tapef (tid)time-range(im, `, τ, tid, path, tape, H )coherent-thread(`, τ, path, tape, H )uniq-time-loc(`, τ, s.tapef , H )path SY , lastSY(tape, path)
SY
SY
S , if path 6= [] then {htid, path , dmbi} ∪ prev-Ord-req(tid, path SY , tape, H ) else ∅S 0 , if im then S ∪ {htid, path, wr ` : vali} else S
view , [`@τ ] t viewf(tid, path SY , path SY , tape, H )00
H 0 , H [(tid, path) 7→ (τ, S 0 , view)]
MPOP.Ord ∪ tedges(MPOP.Evt, Hτ0 ) is acyclic
Write commit tid path ` val τ0Prog ` hs, H i −−−−−−−−−−−−−−−−−−→ hhMPOP, iordf 0 , tapef 0 i, H 0 i
ARM+τ

Figure 3 Transitions of the ARM+τ machine.

8

The ARM+τ Machine

In the previous section, we showed that one may assign timestamps for every write or fence
request in a terminating execution of the ARM machine. Here, we introduce an instrumented
version of the ARM machine, the ARM+τ machine, which assigns timestamps to the requests
when it issues them to the storage.

8.1

Definition of the ARM+τ Machine

The ARM+τ machine state has one additional component H : Tid × P ath * Time ×
2ReqSet × View. The H component is defined for committed write instruction instances. For
each committed write, it assigns (i) a timestamp, (ii) a set of write and fence requests inthe storage, which are guaranteed to be Ord-before the committed write request, if there isone, and (iii) a Promise-style message view representation of the write and fence request
set—it maps a location to the greatest timestamp among write requests to the location in
the set. For the sake of brevity, we define projections for H —Hτ : Tid × P ath * Time,H≤ : Tid × P ath * 2ReqSet , and Hview : Tid × P ath * View. The H map component of
the ARM+τ initial state, ainit , hsinit , H init i, assigns zero timestamps to all initial writes:
H init , [(0tid , []) 7→ h0, λ`. 0, ∅i].
Transitions of the ARM+τ machine match the transitions of the plain ARM machine (seeFig. 3). There is a generic rule, which lifts all of the ARM transitions, except for Propagate
and Write commit, to ARM+τ ones, leaving the timestamp component unchanged. The
Write commit transition of ARM+τ mutates the timestamp component; and both Propagate
and Write commit transitions have a common additional precondition: the union of the Ord
relation and the order induced by timestamps, tedges, has to remain acyclic.
I Definition. tedges(Evt, Hτ ) ={(e, e0 ) ∈ Evt × Evt | e, e0 are writes, e.loc = e0 .loc, Hτ (e.tid, e.path) < Hτ (e0 .tid, e0 .path)}
The other rules cannot introduce cycles in the union, so we do not have to insert the additional
precondition to them.

Promising Compilation to ARMv8 POP

69:19

Let’s take a closer look to the Write commit transition. It chooses a timestamp τ , which
has to be unique among writes to the same location (the predicate uniq-time-loc). Also, thetimestamp has to be consistent with timestamps of thread’s committed writes to the location(the predicate coherent-thread): it has to be bigger than timestamps of the preceding writes
and smaller than timestamps of the following writes. The Write commit transition of theoriginal machine does not issue a write request to the storage in case there is a following
committed write to the location (im = false). Nevertheless, the ARM+τ machine assigns atimestamp to it. To distinguish write instances that have write requests in the storage fromthose that do not, timestamps of instances with requests in the storage are integers, whiletimestamps of instances without requests are in a range (τ 0 − 1, τ 0 ), where τ 0 is a timestampof the closest following write to the same location, which has a write request in the storage(the predicate time-range).
If the write request is issued (im = true) and there is a preceding SY fence (path SY 6= []),
then requests guaranteed to be Ord-before the issued write request (its H≤ entry) are thelast preceding fence request, htid, path SY , dmbi, and prev-Ord-req(tid, path SY , tape, H )—thewrite requests issued by the thread before path SY , and elements of H≤ (e.tid, e.path), for every
write request e which is read by the thread before path SY .
prev-Ord-req(tid, path SY , tape, H ) ,{htid : path 0 @`0 , val 0 i | path 0 < path SY , tape(path 0 ) = W (com _ `0 val 0 )} ∪S
{H≤ (e.tid, e.path) | path 00 < path SY , tape(path 00 ) = R (sat com e)}.
Why are these requests Ord-before the added write request?
First, all these requests, except for the fence request itself, are Ord-before the fence
request htid, path SY , dmbi, because when the storage accepts a fence request e, it adds (e0 , e)edges to the Ord relation for all requests e0 propagated to the thread, since no requests arereorderable with a fence request. Each write e0 , which was issued by the thread before thefence, was propagated to that thread, so the corresponding edge to htid, path SY , dmbi is added
to Ord. Each write e00 , which was read by the thread before the fence, was propagated tothat thread as well, so edges from e00 itself and elements of its H≤ -entry to htid, path SY , dmbi
are added to Ord. Second, when the storage subsystem accepts the write request, it adds anedge from the fence request to it, as the latter is issued by the same thread (i.e., propagatedto the thread). The others are Ord-before the write request by transitivity of Ord.
The Hview entry is equal to a pointwise maximum (the t operation) of a write timestamp
map [`@τ ] and viewf(tid, path SY , path SY , tape, H ), where
viewf(tid, path write , path read , tape, H ) ,F
F
com-writes-time(tid, path write , tape, H ) t sat-reads-view(path read , tape, H )which captures a composition of views corresponding to the elements of the H≤ entry:
com-writes-time(tid, path, tape, H ) ,{[`@τ ] | path 0 < path, tape(path 0 ) = W (com _ ` _), τ = Hτ (tid, path 0 )} ∪{[`@τ ] | tid 0 , path 0 , path 00 < path, τ = Hτ (tid 0 , path 0 ) 6= ⊥,tape(path 00 ) = R (sat sat-state htid 0 , path 0 , wr ` : _i), sat-state 6= inflight}.
sat-reads-view(path, tape, H ) ,{Hview (tid 0 , path 0 ) 6= ⊥ | ∃`, tid 0 , path 0 , path 00 < path,tape(path 00 ) = R (sat sat-state htid 0 , path 0 , wr ` : _i), sat-state 6= inflight}.

ECOOP 2017

69:20Promising Compilation to ARMv8 POP

8.2

Simulation of the ARM Machine

As we have just seen, the transitions of the ARM+τ machine are more restrictive than the
ARM transitions, which may potentially lead to fewer possible behaviors of the instrumented
machine. So, if we want to use the instrumented machine in the compilation proof, we haveto show that it is possible to simulate the original machine.
I Theorem 8.1. ∀Prog, {si }i∈[0..n] . s0 = sinit ∧ FinalARM (sn , Prog) ∧Prog ` s0 −−−→ . . . −−−→ sn ⇒ ∃{H i }i∈[0..n] . H 0 = ainit .H ∧
ARM

ARM

Prog ` hs0 , H 0 i −−−−−→ . . . −−−−−→ hsn , H n i.
ARM+τ

ARM+τ

Proof. In Section 7, we constructed the relation mo and the function mapτ : req * τ fromthe final state of an execution. Here, we do the same for sn , with a minor change: we supposethat the domain of mapτ is instruction instance identifiers tid × path instead of req. It is astylistic change, as each req in the storage is uniquely identified (except for initial writes) by
the instruction instance that issued it.
We construct {H i }i∈[0..n] inductively. The initial map H 0 is equal to ainit .H . We
introduce an invariant for the ARM+τ execution we are constructing:inv(s, H ) , ∀tid, path.
(s.tapef (tid, path) = W (com true _ _) ⇒ Hτ (tid, path) = mapτ (tid, path)) ∨(s.tapef (tid, path) 6= W (com _ _ _) ⇒ Hτ (tid, path) = ⊥).
The invariant says that the timestamps introduced during the instrumented execution are
given by the mapτ function. We will prove that the invariant is maintained while constructing{H i }i∈[0..n] . Suppose that we made the first i transitions and the invariant holds for thecorresponding states. Let’s perform a case analysis of the Prog ` si −−−→ si+1 step.
ARM

Propagate: We choose H i+1 to be equal to H i . Then, inv(si+1 , H i+1 ) holds as si+1 .tapef =si .tapef . In Section 7, we proved that for all j ∈ [0..n], mosj .Evt ∪ sj .Ord is acyclic.
inv(si+1 , H i+1 ) guarantees that mosi+1 .Evt is equal to tedges(si+1 .Evt, Hτi+1 ). Then
si+1 .Ord ∪tedges(si+1 .Evt, Hτi+1 ) is acyclic. The additional precondition of the Propagatetransition holds, and the ARM+τ machine can make the same step.
Write commit tid path: There are two subcases to consider.
If the write request is issued to the storage, then we choose τ , a parameter of the
ARM+τ transition, to be equal to mapτ (tid, path). We choose H i+1 as it is definedin the Write commit transition of ARM+τ . The invariant is obviously preserved. By
definition of mapτ , τ is unique among writes to the same location. The acyclicity ofsi+1 .Ord ∪ tedges(si+1 .Evt, Hτi+1 ) holds by the same reason as in the previous case. By
the acyclicity, τ is greater than timestamps of all writes to the same location, which
are issued by tid to the storage. It is also greater than timestamps of previous writes,
which do not have requests in the storage, as for each such write, there is a committed
write with a larger timestamp. There are no following committed writes to the same
location by the same thread, as the transition issues the request to the storage. Thus thetimestamp is coherent with other thread writes.
If there is no write request issued to the storage, then mapτ (tid, path) = ⊥. We know that
there is a following write by the same thread to the same location with some timestamp τ 0 .
We may choose the timestamp τ to be in (τ 0 − 1, τ 0 ) in a way that it does not violate thetransition preconditions. We choose H i+1 as it is defined in the Write commit transition.
The invariant is obviously preserved.

Promising Compilation to ARMv8 POP

69:21

Other transitions: We choose H i+1 to be equal to H i . As there are no additional preconditions in the instrumented machine rules, and no changes in the additional componentsof the state, the instrumented machine can take the corresponding transition and theinvariant is preserved.
J

8.3

View of the ARM+τ Machine

As we have seen for the MP-SY-LD example in Section 2, once a thread of the Promise
machine reads from a write and then executes an acquire fence, the view of the thread gets
updated with the message view of the write. The view update forbids subsequent reads
to read from too old writes (with too small timestamps). To show a simulation between
the Promise and the ARM+τ machines, we have to show a similar result for the ARM+τmachine.
We start with introducing viewARM , an analog of view cur :viewARM (a, tid, path) ,F
com-writes-time(tid, path, a.tapef (tid), a.Hτ ) tFsat-reads-view(lastCF(tape, path), a.tapef (tid), a.Hview ) .
Unlike view cur of the Promise machine, which is defined for a thread, viewARM is additionallyparametrized by path for the same reason that the variable state of the ARM machine isparametrized by path—the machine executes instructions out-of-order, so different instructions
which might be executed at the same time have different τ -related restrictions. The definition
itself is very similar to the definition of the Hview entry in the Write commit transition: it is
a composition of singleton views corresponding to writes committed by the thread before
path and Hview entries corresponding to writes read by the thread before the last committed
fence (lastCF(tape, path)). We count reads up to any fence as both SY and LD ARM fences
are strong enough to be a result of compilation of an acquire fence of the Promise machine.
Having this definition, we can define the aforementioned restrictions. If a read is satisfied
from a committed write, the write has a timestamp which is greater than or equal to thecorresponding value of viewARM at the read instruction instance. We do not restrict reads
satisfied from not yet committed writes this way, as such writes do not have timestamps
until they are committed. Similarly, each committed write has to have a timestamp which isgreater than the value of viewARM at the write instruction instance:
I Theorem 8.2. ∀Prog, a, tid, tape = a.tapef (tid), path. Prog ` ainit −−−−−→∗ a ⇒ARM+τ

(∀e. tape(path) = R (sat _ e) ∧ a.tapef (e.tid, e.path) is committed ⇒a.Hτ (e.tid, e.path) ≥ viewARM (a, tid, path, e.`)) ∧(∀`. tape(path) = W (com _ ` _) ⇒ a.Hτ (tid, path) > viewARM (a, tid, path, `)).
The proof of the theorem can be found in the extended version of the paper [20].

9The Compilation Correctness Proof

In this section, we prove the main theorem stated in Section 3.
I Theorem 3.1. For all Prog and s, if Prog ` sinit −−−→∗ s and FinalARM (s, Prog),
ARMthen there exists p such that Prog ` pinit −−−−−→∗ p where FinalPromise (p, Prog) andPromisesame-memory(s, p).

ECOOP 2017

69:22

Promising Compilation to ARMv8 POP

Here FinalPromise (p, Prog) means that the Promise machine cannot make a further transition (each thread’s path points out of the thread’s program instruction list) from p and all
promises are fulfilled.
Proof. Let’s fix the program Prog. In the remainder of the section we write “s −−−→ s0 ”
ARM

instead of “Prog ` s −−−→ s0 ” for all machines. We apply the result of Section 8.2, andARMchange the proof goal to the simulation for the ARM+τ machine:∀Prog, a. ainit −−−−−→∗ a ∧ FinalARM+τ (a, Prog) ⇒ARM+τ

∃p. pinit −−−−−→∗ p ∧ FinalPromise (p, Prog) ∧ same-memory(a, p).
PromiseTo prove it, we introduce a number of relations between ARM+τ and Promise states, which
are parts of the simulation relation.
The Iprefix relation states that every instruction instance, which has been executed by
the Promise machine, has been executed by the ARM+τ machine:
Iprefix (a, p) , ∀tid, path 0 < p.tsf (tid).path. a.tapef (tid, path 0 ) is committed.
The next relations connect the memories of the machines. Imem1 states that for every write,
which is committed by the ARM+τ machine, there is a message in the Promise memory to
the same location with the same value and timestamp, and its view is less or equal to thecorresponding view of the ARM request. If the path of the committed write is less than thecorresponding thread’s pointer to the next instruction (p.tsf (tid).path), then the write isfulfilled, otherwise it is promised but not fulfilled:
Imem1 (a, p) , ∀tid, `, val, τ, view 0 , path.
W (com _ ` val) = a.tapef (tid, path) ∧ hτ, _, view 0 i = a.H (tid, path) ⇒∃view ≤ view 0 .
(path ≥ p.tsf (tid).path ⇒ h` : val@τ, viewi ∈ p.tsf (tid).promises)∧(path < p.tsf (tid).path ⇒Sh` : val@τ, viewi ∈ p.MPromise \ p.tsf (tid).promises).
tid

Imem2 connects the memories in other direction: for every message in the Promise memory(except for initial ones) there is a committed write instruction instance in the ARM+τmachine:Imem2 (a, p) , ∀h` : val@τ, viewi ∈ p.MPromise . τ 6= 0 ⇒ ∃tid, path, view 0 ≥ view.
W (com _ ` val) = a.tapef (tid, path) ∧ a.H (tid, path) = hτ, _, view 0 i.
Imem3 relates initial writes to locations:
Imem3 (a, p) , ∀`. h0tid , [], wr ` : 0i ∈ a.MPOP ∧ h` : 0@0, λ`. 0i ∈ p.MPromise .
Iview says that views of a Promise thread are restricted by the composition of singleton
views of writes and reads committed by the ARM thread. For the acquire view, it counts all
the writes and reads up to path. For the current view, it counts all the writes up to pathand reads up to the latest committed LD fence (lastLD(tape, path)). For the release view, it
counts all writes up to the latest committed SY fence (lastSY(tape, path)) and reads up toPromising Compilation to ARMv8 POP

69:23

the latest committed LD fence before the SY fence (lastLDSY(tape, path)).
Iview (a, p) , ∀tid, tape = a.tapef (tid), path = p.tsf (tid).path.
let path LD , path SY , lastLD(tape, path), lastSY(tape, path) in
let path LDSY , lastLDSY(tape, path) inF(p.tsf (tid).view acq ≤ viewf(tid, path, path, tape, a.H ))∧F(p.tsf (tid).view cur ≤ viewf(tid, path LD , path, tape, a.H ))∧F(p.tsf (tid).view rel ≤ viewf(tid, path LDSY , path SY , tape, a.H ).
Istate declares that a variable state of a Promise thread is the same as the committed statefunction up to the corresponding path of the ARM thread:
Istate (a, p) , ∀tid, regf = regf com (Prog(tid), a.tapef (tid), p.tsf (tid).path).
∀reg, p.tsf (tid).st(reg) = regf (reg).
Icom-SY says that if an ARM thread committed a write, then all path-previous SY fences are
executed by the corresponding Promise thread:
Icom-SY (a, p) , ∀tid, tape = a.tapef (tid),
path write = last-write-com(tape), path SY < path write .
tape(path SY ) = F _ SY ⇒ path SY < p.tsf (tid).path.
where last-write-com(tape) is a path of a last write committed by the thread. The relation isnecessary for certification of the Promise machine steps.
Ireach asserts that states are reachable:
Ireach (a, p) , ainit −−−→∗ a ∧ pinit −−−−−→∗ p.
ARM

Promise

The relation Ibase combines the aforementioned relations:Ibase , Iprefix ∩ Imem1 ∩ Imem2 ∩ Imem3 ∩ Iview ∩ Istate ∩ Icom-SY ∩ Ireach .
In the simulation, either the Promise machine is waiting for the next step of the ARM+τmachine, or there is a Promise thread which should make at least one non-Promise write
step (corresponding to an instruction which the thread’s path component is pointing to). A
Promise thread tid is waiting for the corresponding ARM thread, if the next command to be
executed, which is pointed by path, is not fetched or committed in the ARM thread.
tid
IPromise
is up to ARM (tid, a, p) , let tape, path , a.tapef (tid), p.tsf (tid).path intape(path) = ⊥ ∨ tape(path) is not committed.
tid
IPromise is up to ARM (a, p) , ∀ tid. IPromise
is up to ARM (tid, a, p).
tid
IPromise isn’t up to ARM (a, p) , ∃! tid. ¬ IPromise is up to ARM (tid, a, p).

The relations are used to define two simulation relations:
Ipre , Ibase ∩ IPromise isn’t up to ARM

I , Ibase ∩ IPromise is up to ARM

If the states are related by Ipre , there is a thread of the Promise machine which may takea step (which is not Promise write) by executing the next instruction its path is pointing
to. After it either the thread has to make another step (Ipre (a, p0 )), or all threads of thePromise machine are waiting (I(a, p0 )):I Lemma 9.1. ∀(a, p) ∈ Ipre . ∃p0 .p −−−−−→ p0 ∧ (a, p0 ) ∈ Ipre ∪ I.
PromiseECOOP 2017

69:24

Promising Compilation to ARMv8 POP

As at every specific state of the ARM+τ machine it has committed a finite number of
instruction instances, we show that the Promise machine can make a finite number oftransitions to get its state to satisfy I:
I Lemma 9.2. ∀(a, p) ∈ Ipre . ∃p0 . p −−−−−→∗ p0 ∧ (a, p0 ) ∈ I.
PromiseSuppose, the ARM+τ and Promise machine states are related by I. Then, we show that the
ARM+τ machine may make a step. If the step is Write commit, then the Promise machine
has to promise the corresponding message, and the states of the machines are related byIpre ∪ I. If the step is not Write commit, then the Promise machine does not make a step,and the states are related by the same relation Ipre ∪ I.
I Lemma 9.3. ∀(a, p) ∈ I.
¬ Write commit(∀a0 . a −−−−−−−−−→ a0 ⇒ (a0 , p) ∈ Ipre ∪ I) ∧0

ARM+τWrite commit

Promise write

ARM+τ

Promise(∀a . a −−−−−−−−→ a0 ⇒ ∃p0 . p −−−−−−−−→ p0 ∧ (a0 , p0 ) ∈ Ipre ∪ I).
Then, we state the following lemma:
I Lemma 9.4. ∀(a, p) ∈ I. ∃p0 . p −−−−−→∗ p0 ∧ (a0 , p0 ) ∈ I.
PromiseIt straightforwardly follows from the three previous lemmas.9
The theorem is proved by induction on the ARM+τ execution using Lemma 9.4. The
machine memories are the same at the end due to Imem1 and Imem2 . The only thing, which
we need to show, is that FinalPromise (p, Prog) holds.
The Promise machine cannot make a further step (each thread’s path points out of thethread’s instruction list), as otherwise the ARM+τ machine would be able to fetch a new
instruction instance, and FinalARM+τ (a, Prog) would not hold. Each thread has fulfilled its
promises according to Imem1 and Imem2 .
J

10Related Work

The most closely related work is the correctness proof of compilation from the Promise
machine to the x86-TSO and Power models in the paper introducing the Promise machine[12].10 Those proofs were much simpler than our proof essentially because these models aresubstantially simpler than the ARMv8 POP model. To simplify the correctness proof, Kang
et al. use a result of Lahav and Vafeiadis [13], which reduces the soundness of compilation
to proving soundness of certain local program transformations and of compilation withrespect to stronger memory models (SC and Strong-Power respectively). Sadly, however,this reduction is not applicable to the ARMv8 POP model because of examples such as
ARM-weak, in which ARM may execute anti-dependent instructions out of order. As aresult, although Kang et al. do not use promise steps in the compilation part of their proof,
promise steps must be used to justify the correctness of compilation to ARMv8 POP, which
in turn renders our proof substantially more complicated than theirs.
In addition, there exist formal compilation proofs [6, 7] from the C++11 memory modelto x86-TSO and Power, although the latter proof was recently found to be flawed in the case910

Proofs of the lemmas can be found in the extended version of the paper [20].
Kang et al.’s proof for Power considers a compilation scheme that compiles acquire loads using Power’s
lwsync. This scheme is more expensive than the one implemented in existing compilers, which uses
control dependency and isync for acquire loads.

Promising Compilation to ARMv8 POP

69:25

of SC accesses [14, 17] indicating that the C++ semantics for SC accesses is too strong. Thisis also the reason why the Promise machine of Kang et al. [12] does not support SC accesses.
We introduced the intermediate ARM+τ machine to manage “lack of prescience”, i.e.,
absence of information about a final ordering of write messages in the storage during an
execution of the ARM machine. We could have used a backward simulation [16] and/or havetreated the timestamp mapping component of the ARM+τ state as a prophecy variable [4]to establish a connection between the ARM and ARM+τ machines, but we found it easier
to do the proof in a forward style.
Instead of proving the correctness of compilation schemes, one can resort to testing ormodel checking. Recently, Wickerson et al. [24] introduced an approach to automaticallycheck different properties of weak memory models, including compilation. The tool generates
all programs which size less than some given (small) parameter, and exhaustively checks
all executions of those programs. Their approach, however, only works for memory models
expressed in an axiomatic per-execution style, and is thus not directly applicable to neither
the Promise nor the ARMv8 POP semantics.

11

Conclusion

In this paper, we have proved soundness of the compilation of relaxed loads and stores, aswell as release and acquire fences, from the Promise machine to the ARMv8 POP machine.
Since the proof is already significantly complex, we have not attempted to model all thefeatures of the Promise machine. Specifically, we have not considered the compilation of
release/acquire accesses, read-modify-write (RMW) instructions, and SC fences. Extending
the proof to cover these instructions and mechanizing it are left for future work. In theremainder of this section, we outline the issues involved in extending our proof.
Another useful item for future work would be to consider the correctness of compilationfrom the Promise machine to the newer stronger ARMv8.2 model [1, 3]. As, however, the
new model is in many regards substantially stronger than ARMv8 POP, the compilation
proof should be much easier.
Handling Release and Acquire Accesses There are two proposed compilation schemes forrelease and acquire accesses [2]. A one of them involves fences considered in the paper:
Promise:a := [x]acq[x]rel := aARM:a := [x]; dmb LD

dmb SY; [x] := aCompilation correctness for a := [x]acq straightforwardly follows from results of Kang etal. [12] and the current paper, as a transformation a := [x]acq
a := [x]rlx ; fence(acquire)is sound for the Promise machine. To cover the aforementioned mapping of [x]rel := a, one
should be able to restrict the ARM machine to commit writes, which directly follow SY
fences, right after committing the fences without losing any observable behaviors. Then, thecompilation correctness proof is a straightforward extension of the current proof.
Another compilation scheme uses special acquire (a := [x]LDAR ) and release ([x]STLR := a)
ARM instructions, which were originally introduced to the architecture to cover SC accesses:
Promise:a := [x]acq[x]rel := aARM:a := [x]LDAR[x]STLR := aThese instructions induce rather strong synchronization. For instance, the ARM acquire
reads forbid program-following instructions to issue requests until the reads are satisfied, and

ECOOP 2017

69:26

Promising Compilation to ARMv8 POP

any satisfied acquire read requests are not removed from the storage, but start to act as afence request, i.e., become impossible to reorder with anything. To cover them one would
need to extend our definition of the ARM machine and Theorem 8.2.
Handling Read-Modify-Writes The Promise machine with RMW instructions represents
message timestamps as ranges of rational numbers, and maintains the invariant that all
messages in memory have disjoint timestamp ranges. If there is a message with a timestamp(τ, τ 0 ] in the memory and a thread T executes an RMW operation, which reads from thatmessage, the RMW message gets a timestamp range (τ 0 , τ 00 ] for some τ 00 > τ , which prevents
other threads from adding a message “in-between” in future.
RMWs are compiled to ARM as a combination of an exclusive load followed by an
exclusive store, typically inside a loop. The ARM-POP model [9] guarantees that whenan exclusive store issues a write request eexcl to the storage, there is no write request to
the same location Ord-between this write request and the write request eprev read by thecorresponding exclusive load. The machine guarantees that the property is preserved during
an ongoing execution as well. This enables us to keep the same timestamp representationin the ARM+τ machine: as all write requests in the storage of the ARM+τ machine haveinteger timestamps, it is easy to show that the timestamp of eexcl is equal to the timestampof eprev increased by one. In the simulation, when the ARM+τ machine commits a exclusive
store with a timestamp τ , the Promise machine will promise a RMW with a timestamp range(τ − 1, τ ].
A slight difficulty is that once RMWs are added to the source language, the compilation
scheme is no longer bijective, as RMWs get compiled to a sequence of ARM instructions.
For example, a compare-and-swap instruction cas(`, val old , val new ) may be compiled to thefollowing loop (on the left):
Loop : a := loadexcl (`);
if a = val old goto Exit;
storeexcl (flag, `, val new );if flag = 0 goto Loop;
Exit :

Loop : a := [`];
if a = val old goto Exit;flag := casrestricted (`, val old , val new );if flag = 0 goto Loop;
Exit :For the sake of preserving a simple mapping between source and target programs, one might
introduce a restricted version of the CAS instruction in the Promise machine. This restricted
CAS would be allowed to read only from a write read by a previous load instruction, i.e.,
the write whose timestamp is equal (not greater or equal) to the corresponding value ofthe thread’s current view. After that, one may show that the program transformation that
replaces cas(`, val old , val new ) with the loop shown above (on the right) is sound for theextended Promise machine and prove compilation correctness for the extended machine.
Handling SC Fences The Promise machine uses a global view to support SC fences. Whena thread executes an SC fence, it synchronizes its own views with the global view, i.e., assigns
to all of them (including the global one) the pointwise maximum. This models an existenceof a global order on SC fences.
SC fences are compiled to dmb SY fences in the ARM machine. As with write requests,
dmb SY fences are definitely ordered by Ord only at the end of an execution. Consequently,
one needs to extend the ARM+τ machine to calculate timestamps for dmb SY fences.
This, however, does not solve all problems. Currently in the simulation, when the ARM+τmachine commits a dmb SY instruction, the Promise machine executes the correspondingPromising Compilation to ARMv8 POP

69:27

release fence instruction. Doing this is necessary, because it enables promising programfollowing writes, when the ARM+τ machine commits them to the storage. In the same
situation, however, the Promise machine may not be able to execute the corresponding SC
fence, because the Promise machine has to execute them in the newly introduced timestamporder, which may not coincide with a commit order of the ARM+τ execution.
References
1

2
3
4
5

6

7

8
9

10
11
12

13
14
15

16
17

ARM architecture reference manual: ARMv8, for ARMv8-A architecture profile. Available
at https://developer.arm.com/docs/ddi0487/latest/arm-architecture-referencemanual-armv8-for-armv8-a-architecture-profile [Online; accessed 16-May-2017].
C/C++11 mappings to processors. Available at https://www.cl.cam.ac.uk/~pes20/cpp/
cpp0xmappings.html. [Online; accessed 16-May-2017].
The herdtools7 repository. Available at https://github.com/herd/herdtools7 [Online;
accessed 16-May-2017].
Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theor. Comput.
Sci., 82(2):253–284, 1991. doi:10.1109/LICS.1988.5115.
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, 2014. doi:10.1145/2627752.
Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter
Sewell. The problem of programming language concurrency semantics. In ESOP, volume9032 of LNCS, pages 283–307. Springer, 2015. doi:10.1007/978-3-662-46669-8_12.
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. Mathematizing C++ concurrency. In POPL 2011, pages 55–66. ACM, 2011. doi:10.1145/
1925844.1926394.
Hans-J. Boehm and Brian Demsky. Outlawing ghosts: Avoiding out-of-thin-air results. In
MSPC 2014, pages 7:1–7:6. ACM, 2014. doi:10.1145/2618128.2618134.
Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget,
Will Deacon, and Peter Sewell. Modelling the ARMv8 architecture, operationally: Concurrency and ISA. In POPL 2016, pages 608–621. ACM, 2016. doi:10.1145/2837614.2837615.
John L. Hennessy and David A. Patterson. Computer Architecture - A Quantitative Approach (5. ed.). Morgan Kaufmann, 2012.
Alan Jeffrey and James Riely. On thin air reads: Towards an event structures model ofrelaxed memory. In LICS 2016. IEEE, 2016. doi:10.1145/2933575.2934536.
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. A promising
semantics for relaxed-memory concurrency. In POPL 2017. ACM, 2017. doi:10.1145/
3009837.3009850.
Ori Lahav and Viktor Vafeiadis. Explaining relaxed memory models with program transformations. In FM 2016. Springer, 2016. doi:10.1007/978-3-319-48989-6_29.
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. Repairing
sequential consistency in C/C++11. In PLDI 2017. ACM, 2017.
Leslie Lamport. How to make a multiprocessor computer that correctly executes
multiprocess programs. IEEE Trans. Computers, 28(9):690–691, 1979. doi:10.1109/
TC.1979.1675439.
Nancy Lynch and Frits Vaandrager. Forward and backward simulations: I. Untimed systems. Inf. Comput., 121(2):214–233, 1995. doi:10.1006/inco.1995.1134.
Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret
Martonosi. Counterexamples and proof loophole for the C/C++ to POWER and ARMv7

ECOOP 2017

69:28

Promising Compilation to ARMv8 POP

18
19

20

21
22

23

24

25

trailing-sync compiler mappings. CoRR, abs/1611.01507, 2016. URL: http://arxiv.org/
abs/1611.01507.
Jeremy Manson, William Pugh, and Sarita V. Adve. The Java memory model. In POPL
2005, pages 378–391. ACM, 2005. doi:10.1145/1040305.1040336.
Jean Pichon-Pharabod and Peter Sewell. A concurrency semantics for relaxed atomics that
permits optimisation and avoids thin-air executions. In POPL 2016, pages 622–633. ACM,
2016. doi:10.1145/2837614.2837616.
Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. Promising compilation to ARMv8
POP. Extended version, 2017. Available at http://podkopaev.net/armpromise [Online;
accessed 16-May-2017].
Anton Podkopaev, Ilya Sergey, and Aleksandar Nanevski. Operational aspects of C/C++
concurrency. CoRR, abs/1606.01400, 2016. URL: http://arxiv.org/abs/1606.01400.
Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. Understanding POWER multiprocessors. In PLDI 2011, pages 175–186. ACM, 2011. doi:
10.1145/1993498.1993520.
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O.
Myreen. x86-TSO: A rigorous and usable programmer’s model for x86 multiprocessors.
Commun. ACM, 53(7):89–97, 2010. doi:10.1145/1785414.1785443.
John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides. Automatically comparing memory consistency models. In POPL 2017. ACM, 2017. doi:
10.1145/3009837.3009838.
Yang Zhang and Xinyu Feng. An operational happens-before memory model. Frontiers ofComputer Science, 10(1):54–81, 2016. doi:10.1007/s11704-015-4492-4.