A separation logic for a promising semantics
Kasper Svendsen, Jean Pichon-Pharabod1 , Marko Doko2 , Ori Lahav3 , andViktor Vafeiadis2
1

University of Cambridge
2
MPI-SWS
3
Tel Aviv University

Abstract. We present SLR, the first expressive program logic for reasoning about concurrent programs under a weak memory model addressing
the out-of-thin-air problem. Our logic includes the standard featuresfrom existing logics, such as RSL and GPS, that were previously known
to be sound only under stronger memory models: (1) separation, (2)per-location invariants, and (3) ownership transfer via release-acquire
synchronisation—as well as novel features for reasoning about (4) the
absence of out-of-thin-air behaviours and (5) coherence. The logic isproved sound over the recent “promising” memory model of Kang et al.,using a substantially different argument to soundness proofs of logics for
simpler memory models.

1

Introduction

Recent years have seen the emergence of several program logics [1, 5, 7, 15, 22,
23, 25–27] for reasoning about programs under weak memory models. These
program logics are valuable tools for structuring program correctness proofs, andenabling programmers to reason about the correctness of their programs without
necessarily knowing the formal semantics of the programming language. However,they have so far focused on reasoning about relatively strong memory models(such as TSO [18] or release/acquire consistency [14] that can be expressed as aconstraint on individual candidate program executions) and provide little to noreasoning principles to deal with C/C++ “relaxed” accesses.
The main reason for this gap is that the behaviour of relaxed accesses isnotoriously hard to specify [2, 4]. Up until recently, memory models have either
been too strong (e.g., [4, 13, 16]), forbidding some behaviours observed withmodern hardware and compilers, or they have been too weak (e.g., [3]), allowing
so-called out-of-thin-air (OOTA) behaviour even though it does not occur inpractice and is highly problematic.
One observable behaviour forbidden by the strong models is the load buffering
behaviour illustrated by the example below, which, when started with both
locations x and y containing 0, can end with both r1 and r2 containing 1. Thisbehaviour is observable on certain ARMv7 processors after the compiler optimises
r2 + 1 − r2 to 1.
r1 := [x]rlx ; // reads 1[y]rlx := r1

r2 := [y]rlx ; // reads 1[x]rlx := r2 + 1 − r2

(LB+data+fakedep)

2

K. Svendsen et al.

However, one OOTA behaviour they should not allow is the following example
by [4]. When started with two completely disjoint lists a and b, by updating themseparately in parallel, it should not be allowed to end with a and b pointing toeach other, as that would violate physical separation (for simplicity, in these lists,
a location just holds the address of the next element):
r1 := [a]rlx ; // reads b[r1 ]rlx := ar2 := [b]rlx ; // reads a[r2 ]rlx := b

(Disjoint-Lists)

Because of this specification gap, program logics either do not reason aboutrelaxed accesses, or they assume overly strengthened models that disallow somebehaviours that occur in practice (as discussed in Section 5).
Recently, there have been several proposals of programming language memory
models that allow load buffering behaviour, but forbid obvious out-of-thin-air
behaviours [9, 12, 19]. This development has enabled us to develop a programlogic that provides expressive reasoning principles for relaxed accesses, without
relying on overly strong models.
In this paper, we present SLR, a separation logic based on RSL [26], extended
with strong reasoning principles for relaxed accesses, which we prove sound over
the recent “promising” semantics of Kang et al. [12]. SLR features per-location
invariants [26] and physical separation [21], as well as novel assertions that we use
to show the absence of OOTA behaviours and to reason about various coherence
examples. (Coherence is a property of memory models that requires the existenceof a per-location total order on writes that reads respect.)
There are two main contributions of this work.
First, SLR is the first logic which can prove absence of OOTA in all thestandard litmus tests. As such, it provides more evidence to the claim that thepromising semantics solves the out-of-thin-air problem in a satisfactory way.
The paper that introduced the promising semantics [12] comes with three DRF
theorems and a simplistic value logic. These reasoning principles are enough toshow absence of some very simple out-of-thin-air behaviours, but it is still very
easy to end up beyond the reasoning power of these two techniques. For instance,
they cannot be used to prove that r1 = 0 in the following “random number
generator” litmus test4 , where both the x and y locations initially hold 0.
r1 := [x]rlx ;[y]rlx := r1 + 1

r2 := [y]rlx ;[x]rlx := r2(RNG)

The subtlety of this litmus test is the following: if the first thread reads a certain
value v from x, then it writes v + 1 to y, which the second thread can read, andwrite to x; this, however, does not enable the first thread to read v + 1. SLR
features novel assertions that allow it to handle those and other examples, as
shown in the following section.
4

The litmus test is called this way because some early attempts to solve the OOTA
problem allowed this example to return arbitrary values for x and y.

A separation logic for a promising semantics

3

The second major contribution is the proof of soundness of SLR over thepromising semantics [12]5 . The promising semantics is an operational modelthat represents memory as a collection of timestamped write messages. Besides
the usual steps that execute the next command of a thread, the model has a
non-standard step that allows a thread to promise to perform a write in the
future, provided that it can guarantee to be able to fulfil its promise. After awrite is promised, other threads may read from that write as if it had alreadyhappened. Promises allow the load-store reordering needed to exhibit the load
buffering behaviour above, and yet seem, from a series of litmus tests, constrained
enough so as to not introduce out-of-thin-air behaviour.
Since the promising model is rather different from all other (operational andaxiomatic) memory models for which a program logic has been developed, noneof the existing approaches for proving soundness of concurrent program logics
are applicable to our setting. Two key difficulties in the soundness proof comefrom dealing with promise steps.
1. Promises are very non-modular, as they can occur at every execution pointand can affect locations that may only be accessed much later in the program.
2. Since promised writes can be immediately read by other threads, the soundness proof has to impose the same invariants on promised writes as the ones
it imposes on ordinary writes (e.g., that only values satisfying the location’s
protocol are written). In a logic supporting ownership transfer,6 however,establishing those invariants is challenging, because a thread may promise towrite to x even without having permission to write to x.
To deal with the first challenge, our proof decouples promising steps fromordinary execution steps. We define two semantics of Hoare triples—one “promising”, with respect to the full promising semantics, and one “non-promising”, withrespect to the promising semantics without promising steps—and prove that every
Hoare triple that is correct with respect to its non-promising interpretation is
also correct with respect to its promising interpretation. This way, we modularise
reasoning about promise steps. Even in the non-promising semantics, however,
we do allow threads to have outstanding promises. The main difference in the
non-promising semantics is that threads are not allowed to issue new promises.
To resolve the second challenge, we observe that in programs verified by SLR,a thread may promise to write to x only if it is able to acquire the necessary
write permission before performing the actual write. This follows from promise
certification: the promising semantics requires all promises to be certifiable; thatis, for every state of the promising machine, there must exist a non-promising
execution of the machine that fulfils all outstanding promises.
We present the SLR assertions and rules informally in Section 2. We thengive an overview of the promising semantics of Kang et al. [12] in Section 3, and5

As the promising semantics comes with formal proofs of correctness of all the expected
local program transformations and of compilation schemes to the x86-TSO, Power,and ARMv8-POP architectures [20], SLR is sound for these architectures too.
6
Supporting ownership transfer is necessary to provide useful rules for C11 releaseand acquire accesses.

4

K. Svendsen et al.
s ∈ Stm ::= skip | s1 ; s2 | if e then s1 else s2
e ∈ Expr ::= ninteger| while e do s | r := e | r := [e]rlx| rregister| e1 op e2 arithmetic| r := [e]acq | [e1 ]rlx := e2 | [e1 ]rel := e2Fig. 1. Syntax of the programming language.

use it in Section 4 to explain the proof of soundness of SLR. We discuss related
work in Section 5. The technical appendix includes details of the rules of SLR
and its soundness proof in terms of the complete promising semantics.

2

Our logic

The novelty of our program logic is to allow non-trivial reasoning about relaxedaccesses. This is challenging because relaxed accesses do not induce synchronisation between threads, so the usual approach of program logics, which relies onownership transfer, does not apply. Therefore, in addition to reasoning aboutownership transfer like a standard separation logic, our logic supports reasoning
about relaxed accesses by collecting information about what reads have been
observed, and in which order. When combined with information about which
writes have been performed, we can deduce that certain executions are impossible.
For concreteness, we consider a minimal “WHILE” programming languagewith expressions, e ∈ Expr, and statements, s ∈ Stm, whose syntax is given in
Fig. 1. Besides local register assignments, statements also include memory reads
with relaxed or acquire mode, and memory writes with relaxed or release mode.
2.1

The assertions of the logic

The SLR assertion language is generated by the following grammar, where N ,l, v, t, π and X all range over a simply-typed term language which we assume
includes booleans, locations, values and expressions of the programming language,
fractional permissions, and timestamps, and is closed under pairing, finite sets,
and sequences. By convention, we assume that l, v, t, π and X range over termsof type location, value, timestamp, permission and sets of pairs of values, andtimestamps, respectively.
P, Q ∈ Assn ::= ⊥ | > | P ∨ Q | P ∧ Q | P ⇒ Q | ∀x. P | ∃x. P | N1 = N2 | φ(N )| P ∗ Q | Rel(l, φ) | Acq(l, φ) | O(l, v, t) | Wπ (l, X) | ∇P
φ ∈ Pred ::= λx. P
This includes the standard operators from first order logic and separation logic,
the Rel and Acq assertions from RSL [26], and a few novel constructs.
Rel(l, φ) grants permission to perform a release write to location l and transfer
away the invariant φ(v), where v is the value written to that location. Conversely,
Acq(l, φ) grants permission to perform an acquire read from location l and gain
access to the invarant φ(v), where v is the value returned by the read.

A separation logic for a promising semantics

5

The first novel assertion form, O(l, v, t), records the fact that location l wasobserved to have value v at timestamp t. The timestamp is used to order it withother reads from the same location. The information this assertion provides isvery weak: it merely says that the owner of the assertion has observed that value,
it does not imply that any other thread has ever observed it.
The other novel assertion form, Wπ (l, X), asserts ownership of location l
and records a set of writes X to that location. The fractional permission π ∈ Q
indicates whether ownership is shared or exclusive. Full permission, π = 1, confers
exclusive ownership of location l and ensures that X is the set of all writes tolocation l; any fraction, 0 < π < 1, confers shared ownership and enforces that
X is a lower-bound on the set of writes to location l. The order of writes to l istracked through timestamps; the set X is thus a set of pairs consisting of thevalue and the timestamp of the write.
In examples where we only need to refer to the order of writes and not theexact timestamps, we write Wπ (x, `), where ` = [v1 , ..., vn ] is a list of values, as
shorthand for ∃t1 , ..., tn . t1 > t2 > · · · > tn ∗ Wπ (x, {(v1 , t1 ), ..., (vn , tn )}). The
Wπ (x, `) assertion thus expresses ownership of location x with permission π, andthat the writes to x are given by the list ` in order, with the most recent writeat the front of the list.
Relation between reads and writes. Records of reads and writes can be confronted
by the thread owning the exclusive write assertion: all reads must have readvalues that were written. This is captured formally by the following property:
W1 (x, X) ∗ O(x, a, t) V W1 (x, X) ∗ O(x, a, t) ∗ (a, t) ∈ X (Reads-from-Write)
Random number generator. These assertions allow us to reason about the “random
number generator” litmus test from the Introduction, and to show that it cannot
read arbitrarily large values. As discussed in the Introduction, capturing the setof values that are written to x, as made possible by the “invariant-based programlogic” of Kang et al. [12, §5.5] and of Jeffrey and Riley [9, §6], is not enough, andwe make use of our stronger reasoning principles. We use O(x, a, t) to record whatvalues reads read from each location, and W1 (x, `) to record what sequences ofvalues were written to each location, and then confront these records at the endof the execution. The proof sketch is then as follows: 1
 1
W (y, [0]) ∗ . . .
W (x, [0]) ∗ . . .
r1 := [x]rlx ;r2 := [y]rlx ;W1 (y, [0]) ∗ O(x, r1 , ) ∗ . . .
W1 (x, [0]) ∗ O(y, r2 , ) ∗ . . .
[y]rlx := r1 + 1
[x]
:= r2

 rlx
W1 (y, [r1 + 1; 0]) ∗ O(x, r1 , ) ∗ . . .
W1 (x, [r2 ; 0]) ∗ O(y, r2 , ) ∗ . . .
At the end of the execution, we are able to draw conclusions about the valuesof the registers. From W1 (x, [r2 ; 0]) and O(x, r1 , ), we know that r1 ∈ {r2 , 0} by
rule Reads-from-Write. Similarly, we know that r2 ∈ {r1 + 1, 0}, and so we canconclude that r1 = 0. We discuss the distribution of resources at the beginningof a program, and their collection at the end of a program, in Theorem 2. Note

6

K. Svendsen et al.

that we are unable to establish what values the reads read before the end of thelitmus test. Indeed, before the end of the execution, nothing enforces that there
are no further writes that reads could read from.
2.2

The rules of the logic for relaxed accesses

We now introduce the rules of our logic by focusing on the rules for relaxed accesses.
In addition, we support the standard rules from separation logic and Hoare logic,
rules for release/acquire accesses (§2.4), and the following consequence rule: 0  0P c Q
P V P0Q0 V Q
(conseq)` P c Q
which allows one to use “view shifting” implications to strengthen the precondition
and weaken the postcondition.
The rules for relaxed accesses are adapted from the rules of RSL [26] forrelease/acquire accesses, but use our novel resources to track the more subtle
behaviour of relaxed accesses. Since relaxed accesses do not introduce synchronisation, they cannot be used to transfer ownership; they can, however, be used totransfer information. For this reason, as in RSL [26], we associate a predicate φ on
values to a location x using paired Rel(x, φ) and Acq(x, φ) resources, for writers
and readers, respectively. To write v to x, a writer has to provide φ(v), and in
exchange, when reading v from x, a reader obtains φ(v). However, here, relaxed
writes can only send pure predicates (i.e., ones which do not assert ownership of
any resources), and relaxed reads can only obtain the assertion from the predicate
guarded by a modality ∇7 that only pure assertions filter through: if P is pure,then ∇P =⇒ P . All assertions expressible in first-order logic are pure.
Relaxed write rule. To write value v (to which the value expression e2 evaluates) tolocation x (to which the location expression e1 evaluates), the thread needs to own
a write permission Wπ (x, X). Moreover, it needs to provide φ(v), the assertion
associated to the written value, v, to location x by the Rel(x, φ) assertion. Because
the write is a relaxed write, and therefore does not induce synchronisation, φ(v)has to be a pure predicate. The write rule updates the record of writes with thevalue written, timestamped with a timestamp newer than any timestamp forthat location that the thread has observed so far; this is expressed by relating
it to a previous timestamp that the thread has to provide through an O(x, , t)assertion in the precondition.
`

φ(v) is pure 0
e1 = x ∗ e2 = v ∗ Wπ (x, X)∃t > t.
[e1 ]rlx := e2∗ Rel(x, φ) ∗ φ(v) ∗ O(x, , t)Wπ (x, {(v, t0 )} ∪ X)

(w-rlx)The Rel(x, φ) assertion is duplicable, so there is no need for the rule to keep it.
7

This ∇ modality is similar in spirit, but weaker than that of FSL [7].

A separation logic for a promising semantics

7

In practice, O(x, , t) is taken to be that of the last read from x if it was thelast operation on x, and O(x, fst(max(X)), snd(max(X))) if the last operation
on x was a write, including the initial write. The latter can be obtained by
Wπ (x, X) ∗ (v, t) ∈ X V Wπ (x, X) ∗ O(x, v, t)(Write-Observed)

Relaxed read rule. To read from location x (to which the location expression eevaluates), the thread needs to own an Acq(x, φ) assertion, which gives it theright to (almost) obtain assertion φ(v) upon reading value v from location x.
The thread then keeps its Acq(x, φ), and obtains an assertion O(x, r, t0 ) statingthat it has read the value now in register r from location x, timestamped with t0 .
This timestamp is no older than any timestamp for that location that the thread
has observed so far, expressed again by relating it to an O(x, , t) assertion in theprecondition. Moreover, it obtains the pure portion ∇φ(r) of the assertion φ(r)corresponding to the value read in register r` e = x ∗ Acq(x, φ) ∗ O(x, , t)r := [e]rlx
0(r-rlx)0∃t ≥ t. Acq(x, φ) ∗ O(x, r, t ) ∗ ∇φ(r)Again, we can obtain O(x, v0x , 0), where v0x is the initial value of x, from theinitial write permission for x, and distribute it to all the threads that will readfrom x, expressing the fact that the initial value is available to all threads, anduse it as the required O(x, , t) in the precondition of the read rule.
Moreover, if a thread owns the exclusive write permission for a location x,
then it can take advantage of the fact that it is the only writer at that location
to obtain more precise information about its reads from that location: they will
read the last value it has written to that location.
`

e = x ∗ Acq(x, φ) ∗ W1 (x, X)∃t. (r, t) = max(X) ∗ Acq(x, φ) ∗ W1 (x, X) ∗ O(x, r, t) ∗ ∇φ(r)r := [e]rlx(r-rlx*)

Separation. With these assertions, we can straightforwardly specify and verify
the Disjoint-Lists example. Ownership of an element of a list is simply expressedusing a full write permission, W1 (x, X). This allows including the Disjoint-Lists
as a snippet in a larger program where the lists can be shared before or after, andstill enforce the separation property we want to establish. While this reasoning
sounds underwhelming (and we elide the details), we remark that it is unsoundin models that allow OOTA behaviours.
2.3

Reasoning about coherence

An important feature of many memory models is coherence, that is, the existenceof a per-location total order on writes that reads respect. Coherence becomes8

K. Svendsen et al.

interesting where there are multiple simultaneous writers to the same location(write/write races). In our logic, write assertions can be split and combined asfollows: if π1 + π2 ≤ 1, 0 < π1 and 0 < π2 thenWπ1 +π2 (x, X1 ∪ X2 ) ⇔ Wπ1 (x, X1 ) ∗ Wπ2 (x, X2 )(Combine-Writes)

To reason about coherence, the following rules capture the fact that thetimestamps of the writes at a given location are all distinct, and totally ordered:Wπ (x, X) ∗ (v, t) ∈ X ∗ (v 0 , t0 ) ∈ X ∗ v 6= v 0 V Wπ (x, X) ∗ t 6= t0(Different-Writes)Wπ (x, X) ∗ ( , t) ∈ X ∗ ( , t0 ) ∈ X V Wπ (x, X) ∗ (t < t0 ∨ t = t0 ∨ t0 < t)(Writes-Ordered)
CoRR2. One of the basic tests of coherence is the CoRR2 litmus test, whichtests whether two threads can disagree on the order of two writes to the same
location. The following program, starting with location x holding 0, should not
be allowed to finish with r1 = 1 ∗ r2 = 2 ∗ r3 = 2 ∗ r4 = 1, as that would meanthat the third thread sees the write of 1 to x before the write of 2 to x, but thatthe fourth thread sees the write of 2 before the write of 1:[x]rlx := 1[x]rlx := 2

r1 := [x]rlx ;r2 := [x]rlx

r3 := [x]rlx ;r4 := [x]rlx(CoRR2)

Coherence enforces a total order on the writes to x that is respected by the reads,
so if the third thread reads 1 then 2, then the fourth cannot read 2 then 1.
We use the timestamps in the O(x, a, t) assertions to record the order in whichreads read values, and then link the timestamps of the reads with those of thewrites. Because we do not transfer anything, the predicate for x is λv. > again,
and we elide the associated clutter below.
The proof outline for the writers just records what values have been written:
 1/2
 1/2
W (x, {(0, 0)}) ∗ . . .
W (x, {(0, 0)}) ∗ . . .
[x]
:=
1
[x]
2
 rlx 1/2
 rlx :=1/2∃t1 . W (x, {(1, t1 ), (0, 0)}) ∗ . . .
∃t2 . W (x, {(2, t2 ), (0, 0)}) ∗ . . .
The proof outline for the readers just records what values have been read,and — crucially — in which order.

Acq(x, λv. >) ∗ O(x, 0, 0)r1 := [x]rlx ;r3 := [x]rlx ;∃ta . Acq(x, λv. >) ∗ O(x, r1 , ta ) ∗ 0 ≤ ta ∗ . . .
r4 := [x]rlx
r2 := [x]rlx
∃ta , tb . O(x, r1 , ta ) ∗ O(x, r2 , tb ) ∗ 0 ≤ ta ∗ ta ≤ tb
At the end of the program, by combining the two write permissions using rule
Combine-Writes, we obtain W1 (x, {(1, t1 ), (2, t2 ), (0, 0)}). From this, we havet1 < t2 or t2 < t1 by rules Different-Writes and Writes-Ordered. Now, assuming
r1 = 1 and r2 = 2, we have ta < tb , and so t1 < t2 by rule Reads-from-Write.
Similarly, assuming r3 = 2 and r4 = 1, we have t2 < t1 . Therefore, we cannot
have r1 = 1 ∗ r2 = 2 ∗ r3 = 2 ∗ r4 = 1, so coherence is respected, as desired.

A separation logic for a promising semantics

2.4

9Handling release and acquire accesses

Next, consider release and acquire accesses, which, in addition to coherence,
provide synchronisation and enable the message passing idiom.
[x]rlx := 1;[y]rel := 1

r1 := [y]acq ;if r1 = 1 then r2 := [x]rlx(MP)

The first thread writes data (here, 1) to a location x, and signals that the data isready by writing 1 to a “flag” location y with a release write. The second thread
reads the flag location y with an acquire read, and, if it sees that the first thread
has signalled that the data has been written, reads the data. The release/acquire
pair is sufficient to ensure that the data is then visible to the second thread.
Release/acquire can be understood abstractly in terms of views [14]: a releasewrite contains the view of the writing thread at the time of the writing, and an
acquire read updates the view of the reading thread with that of the release write
it is reading from. This allows one-way synchronisation of views between threads.
To handle release/acquire accesses in SLR, we can adapt the rules for relaxedaccesses by enabling ownership transfer according to predicate associated with
the Rel and Acq permissions. The resulting rules are strictly more powerful thanthe corresponding RSL [26] rules, as they also allow us to reason about coherence.
Release write rule. The release write rule is the same as for relaxed writes, butdoes not require the predicate to be a pure predicate, thereby allowing sendingof actual resources, rather than just information:` e1 = x ∗ e2 = v ∗ Wπ (x, X) ∗ Rel(x, φ) ∗ φ(v) ∗ O(x, , t)[e1 ]rel := e20π(w-rel)0∃t ≥ t. W (x, {(v, t )} ∪ X)

Acquire read rule. Symmetrically, the acquire read rule is the same as for relaxed
reads, but allows the actual resource to be obtained, not just its pure portion:` e = x ∗ Acq(x, φ) ∗ O(x, , t)r := [e]acq 0∃t ≥ t. Acq(x, φ[r 7→ >]) ∗ O(x, r, t0 ) ∗ φ(r)(r-acq)We have to update φ to record the fact that we have obtained the resource
associated with reading that value, so that we do not erroneously obtain that
resource twice; φ[v 0 7→ P ] stands for λv. if v = v 0 then P else φ(v).
As for relaxed accesses, we can strengthen the read rule when the reader isalso the exclusive writer to that location:` Acq(x, φ) ∗ W1 (x, X)
 r := [x]acq
(r-acq*)∃t. (r, t) = max(X) ∗ Acq(x, φ[r 7→ >])1∗ W (x, X) ∗ O(x, r, t) ∗ φ(r)

10

K. Svendsen et al.

Additionally, we allow duplicating of release assertions and splitting of acquire
assertions, as expressed by the following two rules.
Rel(x, φ) ⇔ Rel(x, φ) ∗ Rel(x, φ)(Release-Duplicate)

Acq(x, λv. φ1 (v) ∗ φ2 (v)) V Acq(x, φ1 ) ∗ Acq(x, φ2 )(Acquire-Split)

Message passing. With these rules, we can easify verify the message passing
example. Here, we want to transfer a resource from the writer to the reader,namely the state of the data, x. By transferring the write permission for the data
to the reader over the “flag” location, y, we allow the reader to use it to read thedata precisely. We do that by picking the predicate
φy = λv. if v = 1 then W1 (x, [1; 0]) else >for y. Since we do not transfer any resource using x, the predicate for x is λv. >.
The writer transfers the write permissions for x away on y using φy :W1 (x, [0]) ∗ Rel(x, λv. >) ∗ W1 (y, [0]) ∗ Rel(y, φy )
[x]
:= 1;
 rlx
1
1
W
(x,
 1 [1; 0]) ∗ W (y, [0]) ∗ Rel(y, φy )W (y, {(0, 0)}) ∗ Rel(y, φy ) ∗ φy (1) ∗ O(x, 0, 0)[y]
rel := 11
 1∃t1 . W (y, {(1, t1 )} ∪ {(0, 0)}) ∗ 0 < t1
W (y, [1; 0]) ∗ Rel(y, φy )
The proof outline for the reader uses the acquire permission φy for y to obtain
W1 (x, [1; 0]), which it then uses to know that it reads 1 from x.
Acq(y, φy )) ∗ O(y, 0, 0) ∗ Acq(x, λv. >)r1 := [y]acq ;yy∃t1 ≥ 0. Acq(y, φy [r1 7→ >]) ∗ O(y, r1 , t1 ) ∗ φy (r1 ) ∗ Acq(x, λv. >)φy (r1 ) ∗ Acq(x, λv. >)if r1 = 1 thenW1 (x, [1; 0]) ∗ Acq(x, λv. >)r2 := [x]rlx1
 Acq(x, λv. >) ∗ W (x, [1; 0]) ∗ (r2 = 1)
r1 = 1 =⇒ r2 = 1

2.5

Plain accesses

Our formal development (in the technical appendix) also features the usualπ“partial ownership” x 7→ v assertion for “plain” (non-atomic) locations, and theusual corresponding rules.

A separation logic for a promising semantics

3

11

The promising semantics

In this section, we provide an overview of the promising semantics [12], theoperational model for which we prove SLR sound. The formal semantics isavailable in our technical appendix as well as in [12].
The promising semantics is an operational semantics that interleaves executionof the threads of a program. Relaxed behaviour is introduced in two ways:– As in the “strong release/acquire” model [14], the memory is a pool oftimestamped messages, and each thread maintains a “view” thereof. A thread
may read any value that is not older than the latest value observed by thethread for the given location; in particular, this may well not be the latest
value written to that particular location. Timestamps and views model nonmultiple-copy-atomicity: propagation effects of weak memory models means
the writes do not necessarily become simultaneously visible by all threads.
– The operational semantics contains a non-standard step: at any point a thread
can nondeterministically promise a write, provided that, at every point before
the write is actually performed, the thread can certify the promise, that is,
execute the write by running on its own from the current state. Promises areused to enable load-store reordering.
The behaviour of promising steps can be illustrated on the LB+data+fakedep
litmus test from the Introduction. The second thread can, at the very start ofthe execution, promise a write of 1 to x, because it can, by running on its own
from the current state, read from y (it will read 0), then write 1 to x (because
0 + 1 − 0 = 1), thereby fulfilling its promise. On the other hand, the first threadcannot promise a write of 1 to y at the beginning of the execution, because, byrunning on its own, it can only read 0 from x, and therefore only write 0 to y.
3.1

Storage subsystem

Formally, the semantics keeps track of writes and promises in a global configuration,
gconf = hM, P i, where M is a memory and P ⊆ M is the promise memory. We
denote by gconf .M and gconf .P the components of gconf . Both memories are
finite sets of messages, where a message is a tuple hx :oi v, R@t]i, where x ∈ Loc
is the location of the message, v ∈ Val its value, i ∈ Tid its originating thread,t ∈ Time its timestamp, R its message view, and o ∈ {rlx, rel} its message mode
(we return to timestamps and views later). We denote m.loc, m.val, m.time,m.view and m.mod the components of a message m. We use the following notation
to restrict memories:def

M (rel) = {m ∈ M | m.mod = rel}def

M (rlx) = {m ∈ M | m.mod = rlx}

M (i) = {m ∈ M | m.tid = i}M (x) = {m ∈ M | m.loc = x}

def

def

def

M (i, x) = M (i) ∩ M (x)A global configuration gconf evolves in two ways. First, a message can be“promised” and be added both to gconf.M and gconf.P. Second, a message can be12

K. Svendsen et al.

written, in which case it is either added to gconf.M, or removed from gconf.P (ifit was promised before).
3.2

Thread subsystem

A thread state is a pair TS = hσ, V i, where σ is the internal state of the thread
and V is a view. We denote by TS .σ and TS .V the components of TS .
Thread internal state. The internal state σ consists of a thread store (denotedσ.µ) that assigns values to local registers and a statement to execute (denotedσ.s). The transitions of the thread internal state are labeled with memory actions
and are given by an ordinary sequential semantics. As these are routine, we leave
their description to the technical appendix.
Views. Thread views are used to enforce coherence, that is, the existence of a perlocation total order on writes that reads respect. We assume an infinite set Timeof timestamps, densely totally ordered by ≤, with a minimum element, 0. A viewis a function V : Loc → Time, which records how far the thread has seen in thehistory of each location. To ensure that it does not read stale messages, the view ofa thread restricts the messages the thread may read, and it is increased whenevera thread observes a new message. Note also that messages themselves carry aview (the thread’s view when the message comes from a release write) which isincorporated in the thread view when the message is read by an acquire read.
Additional notations views. The order on timestamps, ≤, is extended pointwise
to views. ⊥ and t denote the natural bottom elements and join operations forviews. {x@t} denotes the view assigning t to x and 0 to other locations.
3.3

Interaction between a thread and the storage subsystem

The interaction between a thread and the storage subsystem is given in terms oftransitions of thread configurations. Thread configurations are tuples hTS , hM, P ii,
where TS is a thread state, and hM, P i is a global configuration. These transitions
are labelled with β ∈ {NP, prom} in order to distinguish whether they involve
promises or not. A thread can:
– Make an internal transition with no effect on the storage subsystem.
– Read the value v from location x, while internally taking a Ro x v-labelled
step, when there is a matching message in memory that is not outdated
according to the thread’s view. It then needs to update its view accordingly:
update the timestamp for location x and, in addition, incorporate the message
view if the read is an acquire read.
– Write the value v to location x while internally taking a Wo x v-labelled step.
Here, the thread needs to pick a timestamp greater than the one of its current
view for the message it adds to memory (or removes from the promise set).
If the write is a release write, the message needs to carry the view of thewriting thread. Moreover, a release write to x can only be performed when
the thread has already fulfilled all its promises to x.

A separation logic for a promising semantics

···

j

i

i

k

j

i
NP

NP

···
k

i
NP

NP

i

i

NP

13

NP

k
NP

i

k

NP

NP

Fig. 2. Promise machine run with certification runs.

– Non-deterministically promise a relaxed write by adding a message to both
M and P .

3.4

Constraining promises

Now that we have described how threads and promises interact with memory, we
can present the certification condition for promises, which is essential to avoid outof-thin-air behaviours. Accordingly, we define another transition system, =⇒, on
top of the previous one, which enforces that the memory remains “consistent”, that
is, all the promises that have been made can be certified. A thread configurationhTS , hM, P ii is called consistent w.r.t. i ∈ Tid if thread i can fulfil its promises
NP ∗by executing on its own, or more formally if hTS , hM, P ii −→i hTS 0 , hM 0 , P 0 ii
for some TS 0 , M 0 , P 0 such that P 0 (i) = ∅. Certification is local, that is, only
thread i is executing during its certification; this is crucial to avoid out-of-thin-air.
Further, the certification itself cannot make additional promises, as it is restricted
to NP-steps.
The thread configuration =⇒-transitions allow a thread to (1) take any
number of non-promising steps, provided its thread configuration at the endof the sequence of step (intuitively speaking, when it gives control back to thescheduler) is consistent, or (2) take a promising step, again provided that its
thread configuration after the step is consistent.
Figure 2 shows a visual representation of a promise machine run, together
with certifications.

3.5

Full machine

Finally, the full machine transitions simply lift the thread configuration =⇒transitions to the machine level. A machine state is a tuple MS = hTS, hM, P ii,
where TS is a function assigning a thread state TS to every thread, and hM, P i
is a global configuration. The initial state MS0 (for a given program) consists ofthe function TS 0 mapping each thread i to its initial state hσi0 , ⊥i, where σi0 is
the thread’s initial local state and ⊥ is the zero view (all timestamps in views
are 0); the initial memory M 0 consisting of one message hx :rlx
0 0, ⊥@0]i for eachlocation x; and the empty set of promises.

14

4

K. Svendsen et al.

Semantics and soundness

In this section, we present the semantics of SLR, and give a short overview ofthe soundness proof. Our focus is not on the technical details of the proof, buton the two main challenges in defining the semantics and proving soundness:
1. Reasoning about promises. This difficulty arises because promise steps canbe nondeterministically performed by the promise machine at any time.
2. Reasoning about release-acquire ownership transfer in the presence of promises.
The cause of the difficulty in this case is the possibility for writes to bepromised before the thread has acquired enough resources to allow it toactually perform the write.
4.1

The intuition

SLR assertions are interpreted by (sets of) resources, which represent permissions
to write to a certain location and/or to obtain further resources by reading acertain message from memory. As is common in semantics of separation logics, theresources form a partial commutative monoid, and SLR’s separating conjunction
is interpreted as the composition operation of the monoid.
When defining the meaning of a Hoare triple {P } s {Q}, we think of thepromise machine as if it were manipulating resources: each thread owns someresources, and operates using them. The intuitive description of the Hoare triple
semantics is that every run of the program s starting from a state containing theresources described by the precondition, P , will be “correct” and, if it terminates,
will finish in a state containing the resources described by the postcondition, Q.
The notion of a program running correctly can be described in terms of threads“respecting” the resources they own; for example, if a thread is executing a writeor fulfilling a promise, it should own a resource representing the write permission.
4.2

A closer look at the resources and the assertion semantics

We now take a closer look at the structure of resources and the semantics ofassertions, whose formal definitions can be found in Figs. 3 and 4.
The idea is to interpret the assertions as predicates over triples consistingof memory, a view, and a resource. We use the resource component to model
assertions involving ownership (i.e., write assertions and acquire assertions), andmodel other assertions using the memory and view components. Since our logic is
intuitionistic, we interpret assertions as upwards-closed predicates. The ordering
on memories and views is given by the promising semantics, and the ordering on
resources is induced by the composition operation in the resource monoid. For
now, we leave the resource composition unspecified, and return to it later.
In addition, however, we have to deal with assertions that are parametrised by
predicates (in our case, Rel(x, φ) and Acq(x, φ)). Doing so is not straightforward
because naı̈ve attempts of giving semantics to such assertions result in circulardefinitions. A common technique used in order to avoid circularity is to treat
predicates stored in assertions syntactically, and to interpret assertions relativeA separation logic for a promising semantics

15

def

ι ∈ PredId = N (predicate identifiers)
defPerm = {π ∈ Q | 0 ≤ π ≤ 1} (fractional permissions)defWrite = P(Val × Time)def
WrPerm = Loc → {(π, X) ∈ Perm × Write | π = 0 ⇒ X = ∅}def
AcqPerm = Loc → P(PredId)defr = (r.wr, r.acq) ∈ Res = WrPerm × AcqPerm (resources)def
W = (W.rel, W.acq) ∈ World = (Loc → Pred) × (PredId *fin Pred) (worlds)
def
Prop = World →mon P ↑ (Mem × View × Res)
Fig. 3. Semantic domains used in this section.

to a world, which is used to interpret those syntactic predicates. In our case,worlds consist of two components: the first component associates a syntactic
SLR predicate with every location (this component is used to interpret release
permissions), while the second component associates a syntactic predicate with afinite number of currently allocated predicate identifiers (this component is used
to interpret acquire permissions). The reason for the more complex structure foracquire permissions is that they can be split (see (Acquire-Split)). Therefore, weallow multiple predicate identifiers associated with a single location. As acquire
permissions are divided and split between threads, new predicate identifiers
are allocated and associated with predicates in the world. The world ordering,W1 ≤ W2 , expresses that world W2 is an extension of W1 in which new predicate
identifiers may have been allocated, but all existing predicate identifiers areassociated with the same predicates.
Let us now focus our attention on the assertion semantics. The semantics ofη
assertions, JP Kµ , is relative to a thread store µ that assigns values to registers,
and an environment η that assigns values to logical variables.
The usual logical connectives and quantifiers are interpreted following theirusual intuitionistic semantics. The intuition for our novel assertions, whose formal
semantics is given in Fig. 4, is as follows:– The observed assertion O(x, v, t) says that there exists a message at location
x with value v and timestamp t in the current memory, and the view of thecurrent thread contains it.
– The write assertion Wπ (x, X) asserts ownership of a (partial, with fraction π)
write resource at location x, and requires that the largest timestamp recorded
in X does not exceed the view of the current thread.
– The acquire assertion, Acq(x, φ), asserts that location x has some predicate
identifier ι associated with the φ predicate in the current world W.
– The release assertion, Rel(x, φ), asserts that location x is associated withsome predicate φ0 in the current world such that there exists a syntactic
proof of the entailment, ` ∀v. φ(v) ⇒ φ0 (v). The implication allows us tostrengthen the predicate in release assertions.
– Finally, ∇P states that P is satisfiable in the current world.

16

K. Svendsen et al.
defJO(x, v, t)Kηµ (W) = {(M, V, r) |∃j, R, o. hJxKηµ :oj JvKηµ , R@JtKηµ ]i ∈ M ∧ JtKηµ ≤ V (x)}JWπ (x, X)Kηµ (W) = {(M, V, r) | ∃π 0 ≥ JπKηµ . r.wr(JxKηµ ) = (π 0 , JXKηµ )def∧ snd(max(JXKηµ )) ≤ V (JxKηµ )}defηη
JAcq(x, φ)Kµ (W) = {(M, V, r) | ∃ι ∈ r.acq(JxKµ ). W.acq(ι) = φ}defJRel(x, φ)Kηµ (W) = {(M, V, r) | ` ∀v. φ(v) ⇒ W.rel(JxKηµ )(v)}def
J∇P Kηµ (W) = {(M, V, r) | JP Kηµ (W) 6= ∅}Fig. 4. Interpretation of SLR assertions, J Kηµ : Assn → Prop

Note that Wπ (x, X), Acq(x, φ), and Rel(x, φ) only talk about owning certain
resources, and do not constrain the memory itself at all. In the next subsection,
we explain how we relate the abstract resources with the concrete machine state.
4.3

Relating concrete state and resources

Before giving a formal description of the relationship between abstract resources
and concrete machine states, we take another look at the intuitive view of threads
manipulating resources presented in Section 4.1.
Consider what happens when a thread executes a release write to a location x.
At that point, the thread has to own a release resource represented by Rel(x, φ),and to store the value v, it has to own the resources represented by φ(v). As thewrite is executed, the thread gives up the ownership of the resources correspondingto φ(v). Conversely, when a thread that owns the resource represented by Acq(x, φ)
performs an acquire read of a value v from location x, it will gain ownershipof resources satisfying φ(v). However, this picture does not account for what
happens to the resources that are “in flight”, i.e., the resources that have beenreleased, but not yet acquired.
Our approach is to associate in-flight resources to messages in the memory.
When a thread does a release write, it attaches the resources it released tothe message it just added to the memory. That way, a thread performing an
acquire read from that message can easily take ownership of the resources thatare associated to the message. Formally, as the execution progresses, we update
the assignment of resources to messages,u : M (rel) → (PredId → Res) .
For every release message in memory M , the message resource assignment u
gives us a mapping from predicate identifiers to resources. Here, we again use
predicate identifiers to be able to track which acquire predicate is being satisfied
by which resource. The intended reading of u(m)(ι) = r is that the resource r
attached to the message m satisfies the predicate with the identifier ι.
We also require that the resources attached to a message (i.e., the resources
released by the thread that wrote the message) suffice to satisfy all the acquirepredicates associated with that particular location. Together, these two properties

A separation logic for a promising semantics

17

def

M |= r, u, W =∀m ∈ M (rel). r.acq(m.loc) = dom(u(m))
 attached resources∧ ∀ι ∈ dom(u(m)).
satisfy predicates they are supposed to[](M, m.view, u(m)(ι)) ∈ JW.acq(ι)(m.val)K[] (W)∧ ∀x, v. ` W.rel(x)(v) ⇒ ~ι∈r.acq(x) W.acq(ι)(v)released resources areenough to satisfy acquires∧ ∀m ∈ dom(u). dom(u(m)) ⊆ dom(W.acq))∧ ∀m ∈ M (rlx).
no ownership transfer[]
via relaxed accesses(h∅, ∅i, λx. 0, ε) ∈ JW.rel(m.loc)(m.val)K[] (W.rel, [])Fig. 5. Message resource satisfaction.

of our message resource assignment, as formalised in Fig. 5, allows us to describe
the release/acquire ownership transfer.
The last condition in the message resource satisfaction relation has to dowith relaxed accesses. Since relaxed accesses do not provide synchronisation, we
disallow ownership transfer through them. Therefore, we require that the releasepredicates connected with the relaxed messages are satisfiable with the empty
resource. This condition, together with the requirement that the released resources
satisfy acquire predicates, forbids ownership transfer via relaxed accesses.
The resource missing from the discussion so far is the write resource (modelling the Wπ (x, X) assertion). Intuitively, we would like to have the following
property: whenever a thread adds a message to the memory, it has to own thecorresponding write resource. However, recall there are two ways a thread can
produce a new message:
1. A thread performs a write. This is the straightforward case: we simply require
the thread to own the write resource and to update the set of value-timestamp
pairs recorded in the resource accordingly.
2. A thread promises a write. Here the situation is more subtle, because thethread might not own the write resource at the time it is issuing the promise,
but will acquire the appropriate resource by the time it fulfils the promise.
So, in order to assert that the promise step respects the resources owned by
the thread, we also need to be able to talk about the resources which thethread can acquire in the future.
When dealing the promises, the saving grace comes from the fact that all
promises have to be certifiable, i.e., when issuing a promise a thread has to beable to fulfil it without interference from other threads.
Intuitively, the existence of a certification run tells us that even though at
the moment a thread issues a promise, it might not have the resources necessary
to actually perform the corresponding write, the thread should, by running
uninterrupted, still be able to obtain the needed resources before it fulfils thepromise. This, in turn, tells us that the needed resources have to be alreadyreleased by the other threads by the time the promise is made: only resources
attached to messages in the memory are available to be acquired, and only thethread that made the promise is allowed to run during the certification; therefore
all the available resources have already been released.

18

K. Svendsen et al.
def

def

r1 • r2 = (r1 .wr •wr r2 .wr, r1 .acq •acq r2 .acq)
ε = ([], λ . ∅)
λx. (f1 (x).perm + f2 (x).perm, f1 (x).msgs ∪ f2 (x).msgs)
def
f1 •wr f2 =if f1 (x).perm + f2 (x).perm ≤ 1 for all locations x
undefined otherwise
def

g1 •acq g2 = if ∀x. g1 (x) ∩ g2 (x) = ∅ then λx. g1 (x) ∪ g2 (x) else undefinedFig. 6. Resource composition.
Q
Q
Q
def
brF , u, WcT = {hM, P i | let r = i∈TId rF (i) • m∈M ι∈dom(u(m)) u(m)(ι) in(1) M |= r, u, W ∧(2) ∀x. {(m.val, m.time) | m ∈ M (x) \ P } = r.wr(x).msgs ∧(3) ∀m ∈ P. m.tid 6∈ T ⇒(rF (m.tid) • canAcq(rF (m.tid), u)).wr(m.loc).perm > 0}
rF : ThreadId → Res maps threads to the resources they own.
r is the sum of all the resources distributed among the threads and messages.
Fig. 7. Erasure.

The above reasoning shows what it means for the promise steps to “respect
resources”: when promises are issued, the resources currently owned by a thread,
together with all the resources it is able to acquire according to the resources it
owns and the current assignment of resources to messages, have to contain theappropriate write resource for the write being promised. The notion of “resourcesa thread is able to acquire” is expressed through the canAcq(r, u) predicate.
canAcq(r, u) performs a fixpoint calculation: the resources we have (r) allow us
to acquire some more resources from the messages in memory (assignment of
resources to messages is given by u), which allows us to acquire some more, andso on. Its formal definition can be found in the technical appendix, and hinges
on the fact that u precisely tracks which resources satisfy which predicates.
An important element that was omitted from the discussion so far is the definition of the composition in the resource monoid Res. The resource composition,
defined in Fig. 6, follows the expected notion of per-component composition. The
most important feature is in the composition of write resources: a full permission
write resource is only composable with the empty write resource.
At this point, we are equipped with all the necessary ingredients to relate
abstract states represented by resources to concrete states hM, P i (where M ismemory, and P is the set of promised messages). We define a function, callederasure, that given an assignment of resources to threads, rF : ThreadId → Res,an assignment of resources to messages, u, and a world, W, gives us a set ofconcrete states satisfying the following conditions:
1. Memory M is consistent with respect to the total resource r and the message
resource assignment u at world W.
2. The set of fulfilled writes to each location x in hM, P i must match the set ofwrites of all write permissions owned by any thread or associated with any
messages, when combined.

A separation logic for a promising semantics

19

3. For all unfulfilled promises to a location x by thread i, thread i must currently
own or be able to acquire from u at least a shared write permission for x.
Our formal notion of erasure, defined in Fig. 7, has an additional parameter, a
set of thread identifiers T . This set allows us to exclude promises of threads T fromthe requirement of respecting the resources. As we will see in the following subsection, this additional parameter plays a subtle, but key, role in the soundness proof.
(The notion of erasure described above corresponds to the case when T = ∅.)Note also that the arguments of erasure very precisely account for who
owns which part of the total resource. This diverges from the usual approachin separation logic, where we just give the total resource as the argument to
the erasure. Our approach is motivated by Lemma 1, which states that a reader
that owns the full write resource for location x knows which value it is going toread from x. This is the key lemma in the soundness proof of the (r-rlx*) and(r-acq*) rules.
qyηLemma 1. If (M, V, rF (i)) ∈ W1 (x, X) µ (W), and hM, P i ∈ brF , u, Wc{i}then for all messages m ∈ M (x) \ P (i) such that V (x) ≤ m.time, we havem.val = fst(max(X)).
Lemma 1 is looking from the perspective of thread i that owns
q the fullyηwrite
resource for the location x. This is expressed by (M, V, rF (i)) ∈ W1 (x, X) µ (W)(recall that rF (i) are the resources owned by the thread i). Furthermore, thelemma assumes that the concrete state respects the abstract resources, expressedby hM, P i ∈ brF , u, Wc{i} . Under these assumptions, the lemma intuitively tells
us that the current thread knows which value it will read from x. Formally, thelemma says that all the messages thread i is allowed to read (i.e., messages in
the memory that are not outstanding promises of thread i and whose timestamp
is greater or equal to the view of thread i) have the value that appears as the
maximal element in the set X.
To see why this lemma holds, consider a message m ∈ M (x) \ P (i). If m
is an unfulfilled promise by a different thread j, then, by erasure, it follows
that j currently owns or can acquire at least a shared write permission for x.
However, this is a contradiction, since thread i currently owns the exclusive
write permission, and, by erasure, rF (i) is disjoint from the resources of all otherthreads and all resources currently associated with messages by u. Hence, mmust be a fulfilled write. By erasure, it follows that the set of fulfilled writes
to x is given by the combination of all write permissions. Since rF (i) owns the
exclusive write permission, this is just rF (i).wr. Hence, the set of fulfilled writes
is X, and the value of the last fulfilled write is fst(max(X)).
Note that in the reasoning above, it is crucial to know which thread andwhich message owns which resource. Without precisely tracking this information,
we would be unable to prove Lemma 1.
4.4

Soundness

Now that we have our notion of erasure, we can proceed to formalise the meaningof triples, and present the key points of the soundness proof.

20

K. Svendsen et al.
def

safe0 (σ, B)(W1 ) = Mem × View × Res
defsafen+1 (σ, B)(W1 ) = {(M1 , V1 , r1 ) | ∀(M, V, r) ≥ (M1 , V1 , r1 ). ∀W ≥ W1 .
(σ.s = skip ⇒ (M, V, r) ∈ vs(B(σ.µ))(W))∧ (∀P, rF , σ 0 , M 0 , P 0 , V 0 , u, i. hM, P i ∈ brF [i 7→ r], u, Wc∅ ∧hhσ, V i, hM, P ii =⇒i hhσ 0 , V 0 i, hM 0 , P 0 ii ∧ n > 0⇒ ∃r0 , u0 , W 0 ≥ W. hM 0 , P 0 i ∈ brF [i 7→ r0 ], u0 , W 0 c∅ ∧(hM 0 , P 0 i, V 0 , r0 ) ∈ safen (σ 0 , B)(W 0 ))}Fig. 8. Safety.

Recall our intuitive view of Hoare triples saying that the program only makes
steps which respect the resources it owns. This notion is formalised using thesafety predicate: safety (somewhat simplified; we give its formal definition in
Fig. 8) states that it is always safe to perform zero steps, and performing n + 1
steps is safe if the following two conditions hold:
1. If no more steps can be taken, the current state and resources have to satisfy
the postcondition B.
2. If we can take a step which takes us from the state hM, P i (which respects
our current resources r, assignment of resources to messages u, and world W)
to the state hM 0 , P 0 i, then(a) there exist resources r0 , assignment of resources to messages u0 , and afuture world W 0 , such that hM 0 , P 0 i respects r0 , u0 , and W 0 , and(b) we are safe for n more steps starting in the state hM 0 , P 0 i with resources
given by r0 , u0 and W 0 .
Note the following:– Upon termination, we are not required to satisfy exactly the postcondition B,
but its view shift. A view shift is a standard notion in concurrent separation
logics, which allows updates of the abstract resources which do not affect theconcrete state. In our case, this means that resource r can be view-shifted
into r0 satisfying B as long as the erasure is unchanged. The formal definitionof view shifts is given in the appendix.
– Again as is standard in separation logics, safety requires framed resources tobe preserved. This is the role of rF in the safety definition. Frame preservation
allows us to compose safety of threads that own compatible resources. However,departing from the standard notion of frame preservation, we precisely track
who owns which resource in the frame, because this is important for erasure.
The semantics of Hoare triples is simply defined in terms of the safety predicate.
The triple {P } s {Q} holds if every logical state satisfying the precondition issafe for any number of steps:ηηJ` {P } s {Q}K = ∀n, µ, η, W. JP Kµ (W) ⊆ safen ((µ, s), λµ0 . JQKµ0 )(W)def

To establish soundness of the SLR proof rules, we have to prove that thesafety predicate holds for arbitrary number of steps, including promise steps. The

A separation logic for a promising semantics

21

trouble with reasoning about promise steps is that they can nondeterministicallyappear at any point of the execution. Therefore, we have to account for them inthe soundness proof of every rule of our logic. To make this task manageable,
we encapsulate reasoning about the promise steps, thus enabling the proofs ofsoundness for proof rules to consider only the non-promise steps. The technique
we use for encapsulating the reasoning about promise steps, which we present inthis section, is one of the key contributions of this work.
Once again (as when we discussed the promise steps at the end of Section 4.3),
certification runs for promises play a pivotal role. As we discussed before, whenevera thread makes a step, it has to be able to fulfil its promises without interference
from other threads (recall Fig. 2). Moreover, since there will be no interference byother threads, performing promise steps during certification is of no use (because
promises can only be used by other threads). Therefore, we can assume that thecertification runs are always promise-free.
Now that we noted that certifications are promise-free, the key idea behind
encapsulating the reasoning about promises is as follows. If we know that all
executions of our program are safe for arbitrarily many non-promising steps, thenwe can use this to conclude that they are safe for promising steps too. Here, we
use the fact that certification runs are possible runs of the program, and the factthat certifications are promise-free.
Let us now formalise our key idea. First, we need a way to state that executions
are safe for non-promising steps. This is expressed by the non-promising safety
predicate defined in Fig. 9. What we want to conclude is that non-promisingsafety is enough to establish safety, as expressed by Theorem 1:
Theorem 1 (Non-promising safety implies safety).
∀n, σ, B, W. npsafe(n+1,0) (σ, B)(W) ⊆ safen (σ, B)(W)
We now discuss several important points in the definition of non-promising safety
which enable us to prove this theorem.
Non-promising safety is indexed by pairs of natural numbers. When proving
Theorem 1, we use promise-free certification runs to establish the safety of thepromise steps. A problem we face here is that the length of certification runs is
unbounded. Somehow, we have to know that whenever the thread makes a step,
it is npsafe for arbitrarily many steps. Our solution is to have npsafe transfinitely
indexed over pairs of natural numbers ordered lexicographically. That way, if weare npsafe at index (n + 1, 0) and we take a step, we know that we are npsafe
at index (n, m) for every m. We are then free to choose a sufficiently large mdepending on the length of the certification run we are considering.
Non-promising safety considers configurations that may contain promises. It is
important to note that the definition of non-promising safety does not requirethat there are no promises in the starting configuration. The only thing that isrequired is that no more promises are going to be issued. This is very important
for Theorem 1, since safety considers all possible starting configurations (including

22

K. Svendsen et al.

defnpsafe(0,m) (σ, B)(W) = Mem × View × Res
def T
npsafe(n+1,0) (σ, B)(W) = m∈N npsafe(n,m) (σ, B)(W)
defnpsafe(n+1,m+1) (σ, B)(W1 ) = {(M1 , V1 , r1 ) | ∀(M, V, r) ≥ (M1 , V1 , r1 ). ∀W ≥ W1 .
(σ.s = skip ⇒ (M, V, r) ∈ vs(B(σ.µ))(W))∧ (∀P, rF , f, σ 0 , M 0 , P 0 , V 0 , u, i.
hM, P i ∈ brF [i 7→ r • f ], u, Wc{i}
∧

NP

0

(weak erasure)0hhσ, V i, hM, P ii −→i hhσ , V i, hM 0 , P 0 ii
00

∧ wf prom (P (i), V ) ∧ wf prom (P (i), V )(only non-promising steps allowed)(promises well formed)⇒ ∃r0 , u0 , W 0 ≥ W. M 0 ∈ brF [i 7→ r0 • f ], u0 , W 0 c{i}
0

0

0

0

(weak erasure)0∧ (M , V , r ) ∈ npsafe(n+1,m) (σ , B)(W )∧ r0 • canAcq(r0 , u0 ) ≤o r • canAcq(r, u) (no new res. acquirable after taking a step)∧ ∀m ∈ (M 0 \ P 0 ) \ (M \ P ). r.wr(m.loc).perm > 0} (when performing a writeor fulfiling a promise
the thread has to own
the appropriate write res.)def

r1 ≤o r2 = ∀x. r1 .wr(x).perm ≤ r2 .wr(x).perm
def

wf prom (P, V ) = ∀m ∈ P. V (m.loc) < m.time
Fig. 9. Non-promising safety.

the ones with existing promises), and if we want the lemma to hold, non-promisingsafety has to consider all possible starting configurations too.
Erasure used in the non-promising safety does not constrain promises of thecurrent thread. Non-promising safety does not require promises by the thread
being reduced (i.e., thread i) to respect resources. Thus, when reasoning about
non-promising safety of thread i, we cannot assume that existing promises bythread i respect resources, but crucially we also do not have to worry aboutNP
recertifying thread i’s promises. However, since the −→ reduction does notrecertify promises, we explicitly require that the promises are well formed (via
wf prom predicate) in order to ensure that we still only consider executions where
threads do not read from their own promises.
Additional constraints by the non-promising safety. Non-promising safety also
imposes additional constraints on the reducing thread i. In particular, any write
permissions owned or acquirable by i after the reduction were already owned or
acquirable by i before the reduction step. Intuitively, this holds because thread i
can only transfer away resources and take ownership of resources it was alreadyallowed to acquire before reducing. Lastly, non-promising safety requires that if
the reduction of i performs any new writes or fulfils any old promises, it must own
the write permission for the location of the given message. Together, these twoA separation logic for a promising semantics

23

conditions ensure that if a promise is fulfilled during a thread-local certificationand the thread satisfies non-promising safety, then the thread already owned
or could acquire the write permission for the location of the promise. This isexpressed formally in Lemma 2.
Lemma 2. Assuming that (hM, P i, V, r) ∈ npsafe(n+1,k) (σ, B)(W ) and hM, P i ∈NP k

brF [i 7→ r • f ], u, W c{i} and hhσ, V i, hM, P ii −→i hhσ 0 , V 0 i, hM 0 , P 0 ii and m ∈(M 0 \ P 0 ) \ (M \ P ), we have (r • canAcq(r, u)).wr(m.loc).perm > 0.
The intuition for why Lemma 2 holds is that since only thread i executes, we know
by the definition of non-promising safety that any write permission owned or
acquirable by i when the promise is fulfilled, it already owns or can acquire in theinitial state. Furthermore, whenever a promise is fulfilled, the non-promising safety
definition explicitly requires ownership of the corresponding write permission. It
follows that the thread already owns or can acquire the write permission for thelocation of the given promise in the initial state.
Lemma 2 gives us exactly the property that we need to reestablish erasure
after the operational semantics introduces a new promise. This makes Lemma 2
the key step in the proof of Theorem 1, which allows us to disentangle reasoning
about promising steps and normal reduction steps. Theorem 1 tells us that, inorder to prove a proof rule sound, it is enough to prove that the non-promisingsafety holds for arbitrary indices. This liberates us of the cumbersome reasoning
about promise steps and allows us to focus on non-promising reduction steps
when proving the proof rules sound.
We can now state our top-level correctness theorem, Theorem 2. Since ourlanguage only has top-level parallel composition, we need a way to distributeinitial resources to the various threads, and to collect all the resources once all
the threads have finished. The correctness theorem gives us precisely that:
Theorem 2 (Correctness). If A is a finite set of locations and1. ` ∀x ∈ A. φx (0)2. ` ~x∈A Rel(x, φx ) ∗ Acq(x, φx ) ∗ W1 (x, {(0, 0)}) V ~i∈Tid Pi
3. ` {Pi } si {Qi } for all i
4. hλi. h(µi , si ), ⊥i, hM 0 , ∅ii =⇒∗ hTS, gconf i and TS(i).σ = skip for all i
5. ` ~i∈Tid Qi V Q
6. FRV (Qi ) ∩ FRV (Qj ) = ∅ for all distinct i, j ∈ Tid[]
then there exist µ, r, and W such that (gconf.M, ti TS(i).V, r) ∈ JQKµ (W) and∀i ∈ Tid. ∀a ∈ FRV(Qi ). µ(a) = TS(i).µ(a), where FRV(P ) denotes the set offree register variables in P .

5Related work

There are a number of techniques for reasoning under relaxed memory models,
but besides the DRF theorems and some simple invariant logics [9, 12], no othertechniques have been proved sound for a model allowing the weak behaviour of
LB+data+fakedep from the introduction. The “invariant-based program logics”

24

K. Svendsen et al.

are by design unable to reason about programs like the random number generator,
where having a bound on the set of values written to a location is not enough,let alone reasoning about functional correctness of a program.
Relaxed separation logic (RSL) Among program logics for relaxed memory,the most closely related is RSL [26]. There are two versions of RSL: a weak
one that is sound with respect to the C/C++11 memory model, which features
out-of-thin-air reads, and a stronger one that is sound with respect to a variantof the C/C++11 memory that forbids load buffering.
The weak version of RSL forbids relaxed writes completely, and does notconstrain the value returned by a relaxed read. The stronger version provides
single-location invariants for relaxed accesses, but its soundness proof relies
strongly on a strengthened version of C/C++11 without po ∪ rf cycles (where pois program order, and rf is the reads-from relation), which forbids load buffering.
When it comes to reasoning about coherence properties, even the strong
version of RSL is surprisingly weak: it cannot be used to verify any of thecoherence examples in this paper. In fact, RSL can be shown sound with respect
to much weaker coherence axioms than what C/C++11 relaxed accesses provide.
One notable feature of RSL which we do not support is read-modify-write(RMW) instructions (such as compare-and-swap and fetch-and-add). However, thesoundness proof of SLR makes no simplifying assumptions about the promising
semantics which would affect the semantics of RMW instructions. Therefore, weare confident that enhancing SLR with rules for RMW instructions would not
substantially affect the structure of the soundness proof, presented in Section 4.
Other program logics FSL [7] extends (the strong version of) RSL withstronger rules for relaxed accesses in the presence of release/acquire fences. In
FSL, a release fence can be used to package an assertion with a modality, which arelaxed write can then transfer. Conversely, the ownership obtained by a relaxed
read is guarded by a symmetric modality than needs an acquire fence to be
unpacked. The soundness proof of FSL also relies on po ∪ rf acyclicity. Moreover,
it is known to be unsound in models where load buffering is allowed [8, §5.2].
A number of other logics—GPS [25], iGPS [11], OGRA [15], iCAP-TSO [23],the rely-guarantee proof system for TSO of Ridge [22], and the program logic
for TSO of Wehrman and Berdine [27]—have been developed for even stronger
memory models (release/acquire or TSO), and also rely quite strongly on—andtry to expose—the stronger consistency guarantees provided by those models.
The framework of Alglave and Cousot [1] for reasoning about relaxed concurrent programs is parametric with respect to an axiomatic “per-execution”
memory model. By construction, as argued by Batty et al. [2], such models
cannot be used to define a language-level model allowing the weak behaviourof LB+data+fakedep and similar litmus tests while forbidding out-of-thin-air
behaviours. Moreover, their framework does not provide the usual abstraction
facilities of program logics.

A separation logic for a promising semantics

25

The lace logic of Bornat et al. [5] targets hardware memory models, inparticular Power. It relies on annotating the program with “per-execution” constraints, and on syntactic features of the program. For example, it distinguishes
LB+data+fakedep from LB+data+po, its variant where the write of second
thread is [x]rlx := 1, and is thus unsuitable to address out-of-thin-air behaviours.
Other approaches Besides program logics, another way to reason about programs under weak memory models is to reduce the act of reasoning under amemory model M to reasoning under a stronger model M 0 —typically, but notnecessarily, sequential consistency [6, 17]. One can often establish DRF theorems
stating that a program without any races when executed under M 0 has thesame behaviours when executed under M as when executed under M 0 . For thepromising semantics, Kang et al. [12, §5.4] have established such theorems for M 0
being release-acquire consistency, sequential consistency, and the promise-freepromising semantics, for suitable notions of races. The last one, the “Promise-Free
DRF” theorem, is applicable to the Disjoint-Lists program from the introduction,
but none of these theorems can be applied to any of the other examples of thispaper, as they are racy. Moreover, these theorems are not compositional, as they
do not state anything about the Disjoint-Lists program when put inside a larger,
racy program—for example, just an extra read of a from another thread.

6

Conclusion

In this paper, we have presented the first expressive logic that is sound under thepromising semantics, and have demonstrated its expressiveness with a number ofexamples. Our logic can be seen both as a general proof technique for reasoning
about concurrent programs, and also as tool for proving the absence of out-ofthin-air behaviour for challenging examples, and reasoning about coherence. In
the future, we would like to extend the logic to cover more of relaxed memory,
more advanced reasoning principles, such as those available in GPS [25], andmechanise its soundness proof.
Interesting aspects of relaxed memory we would like to also cover are readmodify-writes and fences. These would allow us to consider concurrent algorithms
like circular buffers and the atomic reference counter verified in FSL++ [8]. This
could be done by adapting the corresponding rules of RSL and GPS; moreover,
we could adapt them with our new approach to reason about coherence.
To mechanise the soundness proof, we intend to use the Iris framework [10],which has already been used to prove the soundness of iGPS [11], a variant of
the GPS program logic. To do this, however, we have to overcome one technicallimitation of Iris. Namely, the current version of Iris is step-indexed over N, while
our semantics uses transfinite step-indexing over N × N to define non-promisingsafety and allow us to reason about certifications of arbitrary length for eachreduction step. Progress has been made towards transfinitely step-indexed logicalrelations that may be applicable to a transfinitely step-indexed version of Iris [24].

26

K. Svendsen et al.

References
1. Alglave, J., Cousot, P.: Ogre and Pythia: an invariance proof method for weak
consistency models. In: POPL 2017. pp. 3–18. ACM, New York (2017), http://doi.acm.org/10.1145/2994593
2. Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The
problem of programming language concurrency semantics. In: ESOP 2015. LNCS,
vol. 9032, pp. 283–307. Springer, Heidelberg (2015)
3. Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++
concurrency. In: POPL 2011. pp. 55–66. ACM, New York, NY, USA (2011), http://doi.acm.org/10.1145/1926385.1926394
4. Boehm, H.J., Demsky, B.: Outlawing ghosts: Avoiding out-of-thin-air results. In:
Proceedings of the Workshop on Memory Systems Performance and Correctness.
pp. 7:1–7:6. MSPC ’14, ACM, New York, NY, USA (2014), http://doi.acm.org/
10.1145/2618128.2618134
5. Bornat, R., Alglave, J., Parkinson, M.: New lace and arsenic (2016), https://
arxiv.org/abs/1512.01416
6. Bouajjani, A., Derevenetc, E., Meyer, R.: Robustness against relaxed memory models. In: Software Engineering 2014, Fachtagung des GI-Fachbereichs Softwaretechnik,
25. Februar - 28. Februar 2014, Kiel, Deutschland. pp. 85–86 (2014)
7. Doko, M., Vafeiadis, V.: A program logic for C11 memory fences. In: Jobstmann,
B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation- 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January
17-19, 2016. Proceedings. Lecture Notes in Computer Science, vol. 9583, pp. 413–430.
Springer, Heidelberg (2016)
8. Doko, M., Vafeiadis, V.: Tackling real-life relaxed concurrency with FSL++. In:
ESOP 2017. LNCS, vol. 10201, pp. 448–475. Springer, Heidelberg (2017)
9. Jeffrey, A., Riely, J.: On thin air reads towards an event structures model of relaxed
memory. In: LICS 2016. pp. 759–767. ACM, New York (2016)
10. Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris
from the ground up (2017)
11. Kaiser, J.O., Dang, H.H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong logic forweak memory: Reasoning about release-acquire consistency in Iris. In: ECOOP2017 (2017)
12. Kang, J., Hur, C.K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics
for relaxed-memory concurrency. In: POPL 2017. ACM, New York (2017), http://doi.acm.org/10.1145/3009837.3009850
13. Lahav, O., Vafeiadis, V., Kang, J., Hur, C.K., Dreyer, D.: Repairing sequentialconsistency in C/C++11. In: PLDI (2017)
14. Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In:
POPL 2016. pp. 649–662. ACM, New York, NY, USA (2016), http://doi.acm.
org/10.1145/2837614.2837643
15. Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for weak memory models. In:
Automata, Languages, and Programming, ICALP’15, LNCS, vol. 9135, pp. 311–323.
Springer, Berlin, Heidelberg (2015)
16. Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL. pp. 378–391.
ACM, New York (2005)
17. Owens, S.: Reasoning about the implementation of concurrency abstractions on
x86-TSO. In: ECOOP 2010: 24th European Conference on Object-Oriented Programming. LNCS, vol. 6183, pp. 478–503. Springer, Heidelberg (2010)

A separation logic for a promising semantics

27

18. Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In:
Proceedings of the 22Nd International Conference on Theorem Proving in Higher
Order Logics. pp. 391–407. TPHOLs ’09, Springer-Verlag, Berlin, Heidelberg (2009)19. Pichon-Pharabod, J., Sewell, P.: A concurrency semantics for relaxed atomics that
permits optimisation and avoids thin-air executions. In: POPL 2016. pp. 622–633.
ACM, New York (2016)20. Podkopaev, A., Lahav, O., Vafeiadis, V.: Promising compilation to armv8 POP. In:
ECOOP 2017. LIPIcs, vol. 74, pp. 22:1–22:28. Schloss Dagstuhl - Leibniz-Zentrum
fuer Informatik (2017)
21. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In:
17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July
2002, Copenhagen, Denmark, Proceedings. pp. 55–74 (2002), https://doi.org/10.
1109/LICS.2002.1029817
22. Ridge, T.: A rely-guarantee proof system for x86-TSO. In: VSTTE 2010. LNCS,
vol. 6217, pp. 55–70. Springer (2010)23. Sieczkowski, F., Svendsen, K., Birkedal, L., Pichon-Pharabod, J.: A separation logic
for fictional sequential consistency. In: ESOP 2015. LNCS, vol. 9032, pp. 736–761.
Springer (2015)24. Svendsen, K., Sieczkowski, F., Birkedal, L.: Transfinite step-indexing: Decoupling
concrete and logical steps. In: Proceedings of ESOP 2016. pp. 727–751 (2016)
25. Turon, A., Vafeiadis, V., Dreyer, D.: GPS: Navigating weak memory with ghosts,
protocols, and separation. In: 2014 ACM International Conference on Object
Oriented Programming Systems Languages and Applications. pp. 691–707. OOPSLA’14, ACM, New York (2014)
26. Vafeiadis, V., Narayan, C.: Relaxed separation logic: A program logic for C11
concurrency. In: OOPSLA 2013. pp. 867–884. ACM, New York (2013)
27. Wehrman, I., Berdine, J.: A proposal for weak-memory local reasoning. In: LOLA
(2011)