Causal Linearizability: Compositionality for Partially
Ordered Executions
Simon Doherty∗1 , John Derrick†1 , Brijesh Dongol‡2 , and Heike Wehrheim§3
1

Department of Computer Science, University of Sheffield, UK
Department of Computer Science, Brunel University London, UK
3
Department of Computer Science, University of Paderborn, Germany

arXiv:1802.01866v1 [cs.LO] 6 Feb 2018

2

February 7, 2018
Abstract
In the interleaving model of concurrency, where events are totally ordered, linearizability
is compositional: the composition of two linearizable objects is guaranteed to be linearizable.
However, linearizability is not compositional when events are only partially ordered, as in
many weak-memory models that describe multicore memory systems. In this paper, we
present causal linearizability, a correctness condition for concurrent objects implemented in
weak-memory models. We abstract from the details of specific memory models by defining
our condition using Lamport’s execution structures. We apply our condition to the C11
memory model, providing a correctness condition for C11 objects. We develop a proof
method for verifying objects implemented in C11 and related models. Our method is an
adaptation of simulation-based methods, but in contrast to other such methods, it does
not require that the implementation totally order its events. We also show that causal
linearizability reduces to linearizability in the totally ordered case.

1

Introduction

Linearizability [18, 19] is a well-studied [12] condition that defines correctness of a concurrent
object in terms of a sequential specification. It ensures that for each history of an implementation, there is a history of the specification such that (1) each thread makes the same method
invocations in the same order, and (2) the order of non-overlapping operation calls is preserved.
The condition however, critically depends on the existence of a total order of memory events
(e.g., as guaranteed by sequential consistency (SC) [24]) to guarantee contextual refinement [15]
and compositionality [18]. Unfortunately most modern systems can only guarantee a partial order of memory events, e.g., due to the effects of relaxed memory [1, 3, 4, 25]. It is known that a
naive adaptation of linearizability to the partially ordered setting of weak memory is problematic
from the perspective of contextual refinement [13]. In this paper, we propose a compositional
generalisation of linearizability for partially ordered executions.
Figs. 1 and 2 show two examples1 of multi-threaded programs on which weak memory model
∗ s.doherty@sheffield.ac.uk
† j.derrick@sheffield.ac.uk
‡ Brijesh.Dongol@brunel.ac.uk
§ wehrheim@upb.de
1 Example

inspired by H.-J.Boehm talk at Dagstuhl, Nov. 2017

1

x = 0, y = 0
Process 2
Process 1
1 : x := 1;
1 : if(y = 1)
2 : y := 1;
2 : assert(x = 1);

S = h i, S′ = h i
Process 2
Process 1
1 : S.Push(1);
1 : if(S’.Pop = 1)
2 : S’.Push(1); 2 : assert(S.Pop = 1);

Figure 1: Writing to shared variables

Figure 2: Writing to shared stacks

effects can be observed. Fig. 1 shows two threads writing to and reading from two shared
variables x and y. Under SC, the assert in process 2 never fails: if y equals 1, x must also equal
1. However, in weak memory models like the C11 model [4, 21], this is not true: if the writes
to x and y are relaxed, process 2 may observe the write to y, yet also observe the initial value x
(missing the write to x by process 1).
Such effects are not surprising to programmers familiar with memory models [4, 21]. However,
programmer expectations for linearizable objects, even in a weak memory model like C11, are
different: if the two stacks S and S′ in Fig. 2 are linearizable, the expectation is that the
assert will never fail since linearizable objects are expected to be compositional [18, 19], i.e.,
any combination of linearizable objects must itself be linearizable. However, it is indeed possible
for the two stacks to be linearizable (using the classical definition), yet for the program to generate
an execution in which the assert fails. The issue here is that linearizability, when naively applied
to a weak memory setting, allows too many operations to be considered “overlapping”.
Our key contribution in this paper is the development of a new compositional notion of
correctness, called causal linearizability, which is defined in terms of an execution structure [23],
taking two different relations over operations into account: a “precedence order” (describing
operations that are ordered in time) and a “communication relation”. Applied to Fig. 2, for
a weak memory execution in which the assert fails, the execution restricted to stack S would
not be causally linearizable in the first place. Namely, causal linearizability ensures enough
precedence order in an execution to ensure that the method call S.Push(1) occurs before S.Pop,
meaning S.Pop is forced to return 1.
Execution structures are generic, and can be constructed for any weak memory execution
that includes method invocation/response events. Our second contribution is one such scheme
for mapping executions to execution structures based on the happens-before relation of the C11
memory model. Given method calls m1 and m2, we say m1 precedes m2 if the response of m1
happens before the invocation m2; we say m1 communicates with m2 if the invocation of m1
happens before the response of m2.
Our third contribution is a new inductive simulation-style proof technique for verifying causal
linearizability of weak memory implementations of concurrent objects, where the induction is over
linear extensions of the happens-before relation. This is the first such proof method for weak
memory, and one of the first that enables full verification, building on existing techniques for
linearizability in SC [26, 12, 8]. Our fourth contribution is the application of this proof technique
to causal linearizability of the Treiber Stack in the C11 memory model.
We present our motivating example, the Treiber Stack in C11 in Section 2; describe the
problem of compositionality and motivate our execution-structure based solution in Section 3;
and formalise causal linearizability and prove compositionality in Section 4. Causal linearizability
for C11 is presented in Section 5, and verification of the stack described in Section 6.

2

Treiber Stack in C11

The example we consider (see Algorithm 1) is the well-studied Treiber Stack [28], executing in
a recent version of the C11 [22] memory model. In C11, commands may be annotated, e.g., R
2

Algorithm 1 Release-Acquire Treiber Stack
1: procedure Init
2:
Top := null;
3:
4:
5:
6:
7:
8:
9:

procedure Push(v)
n := new(node) ;
n.val := v ;
repeat
top :=A Top ;
n.nxt := top ;
until CASR (&Top, top, n)

10:
11:
12:
13:
14:
15:
16:
17:

procedure Pop
repeat
repeat
top :=A Top ;
until top 6= null ;
ntop := top.nxt ;
until CASR (&Top, top, ntop)
return top.val ;

(for release) and A (for acquire), which introduces extra synchronisation, i.e., additional order
over memory events [4, 21]. We assume racy read and write accesses that are not part of an
annotated command are unordered or relaxed, i.e., we do not consider the effects of non-atomic
operations [4]. Full details of the C11 memory model are deferred until Section 5.
Due to weak memory effects, the events under consideration, including method invocation and
response events are partially ordered. As we show in Section 3, it turns out that one cannot simply
reapply the standard notion of linearizability in this weaker setting; compositionality demands
that we use modified form: causal linearizability that additionally requires “communication”
across conflicting operations.
In Algorithm 1, all accesses to the shared variable Top are via an annotated command. Thus,
any read of Top (lines 7, 13) reading from a write to Top (lines 9, 16) induces happens-before
order from the write to the read. This order, it turns out, is enough to guarantee invariants that
are in turn strong enough to guarantee2 causal linearizability of the Stack (see Section 6).
Note that we modify the Treiber Stack so that the Pop operation blocks by spinning instead
of returning empty. This is for good reason - it turns out that the standard Treiber Stack (with a
non-blocking Pop operation) is not naturally compositional if the only available synchronisation
is via release-acquire atomics (see Section 7).

3

Compositionality and execution structures

This section describes the problems with compositionality for linearizability of concurrent objects
under weak execution environments (e.g., relaxed memory) and motivates a generic solution using
execution structures [23].
Notation. First we give some basic notation. Given a set X and a relation r ⊆ X ×X, we say r is
a partial order iff it is reflexive, antisymmetric and transitive, and a strict order, iff it is irreflexive,
antisymmetric and transitive. The support of r is denoted support (r) = dom(r) ∪ ran(r). A
partial or strict order r is a total order iff either (a, b) ∈ r or (b, a) ∈ r for all a, b ∈ support (r).
We typically use notation such as <, ≤, ≺,
to denote orders, and write, for example, a < b
instead of (a, b) ∈ <.
The operations of an object are defined by a set of labels, Σ. For concurrent data structures,
Σ = Inv × Res, where Inv and Res are sets of invocations and responses (including their input
2 Note that a successful CAS operation comprises both a read and a write access to Top, but we only require
release synchronisation here. The corresponding acquire synchronisation is provided via the earlier read in the
same operation. This synchronisation is propagated to the CAS by sequenced-before (aka program order), which,
in C11, is included in happens-before (see Section 6 for details).

3

and return values), respectively. For example, for a stack S of naturals, the invocations are given
by {Push(n) | n ∈ N} ∪ {Pop}, and the responses by N ∪ {⊥, empty}, and
ΣS = {(Push(n), ⊥), (Pop, n) | n ∈ N} ∪ {(Pop, empty)}
The standard notion of linearizability is defined for a concurrent history, which is a sequence (or
total order) of invocation and response events of operations.
Since operations are concurrent, an invocation of an operation may not be directly followed
by its matching response, and hence, a history induces a partial order on operations. For linearizability, we focus on the real-time partial order (denoted ), where, for operations o and o′ , we
say o
o′ in a history iff the response of operation o happens before the invocation of operation
′
o in the history. A concurrent implementation of an object is linearizable if the real-time partial
order ( ) for any history of the object can be extended to a total order that is legal for the
object’s specification [18]. It turns out that linearizability in this setting is compositional [18, 19]:
any history of a family of linearizable objects is itself guaranteed to be linearizable.
Unfortunately, histories in modern executions contexts (e.g., due to relaxed memory or distributed computation) are only partially ordered since processes do not share a single global
view of time. It might seem that this is unproblematic for linearizability and that the standard
definition can be straightforwardly applied to this weaker setting. However, it turns out that a
naive application fails to satisfy compositionality. To see this, consider the following example.
Example 1. Consider a
S and S’ that are both
S’.Push happens before
the invocation of S.Pop.

history h, partially ordered by a happens-before relation, for two stacks
initially empty (denoted by ⊥). Suppose that in h, the response of
the invocation of S.Pop, and the response of S.Push happens before
History h induces a partial order over these operations as shown below:
(S’.Pop, 11)

(S.Push(42), ⊥)

(S.Pop, 42)

(S’.Push(11), ⊥)

If we restrict the execution above to S only, we can obtain a legal stack behaviour by linearizing
(S.Push(42), ⊥) before (S.Pop, 42) without contradicting the real-time partial order
in the
diagram above. Similarly, the execution when restricted to S′ is linearizable. However, the full
execution is not linearizable: ordering both pushes before both pops contradicts the induced
real-time partial order ( above).
A key contribution of this paper is the development of a correctness condition, causal linearizability, that recovers compositionality of concurrent objects with partially ordered histories.
Our definition is based on two main insights.
The first insight is that one must augment the real-time partial order with additional information about the underlying concurrent execution. In particular, one must introduce information
about the communication when linearizing conflicting operations. Two operations conflict if they
do not commute according to the sequential specification, e.g., for a stack data structure, Push
and Pop are conflicting. Causal linearizability states that for any conflicting operations, say o
and o′ , that are linearized in a particular order, say o o′ , there must exist some communication
from o to o′ . We represent communication by a relation .

4

Example 2. Consider the partial order in Example 1. For both stacks S and S′ , the Push
must be linearized before the Pop, and hence, we must additionally have communication edges
as follows:
(S’.Pop, 11)

(S.Push(42), ⊥)

(S.Pop, 42)

(S’.Push(11), ⊥)

The second insight is that the operations and the induced real-time partial order, , extended
with a communication relation, , must form an execution structure [23], defined below.
Definition 3 (Execution structure). Given that E is a finite3 set of events, and ,
⊆ E ×E
are relations over E, an execution structure is a tuple (E, , ) satisfying the following axioms
for e1 , e2 , e3 ∈ E.
A1 The relation

is a strict order.

A2 Whenever e1

e2 , then e1

A3 If e1

e2

e3 or e1

A4 If e1

e2

e3

e2 and ¬(e2

e2

e1 ).

e3 , then e1

e4 , then e1

e3 .

e4 .

Example 4. Consider the execution depicted in Example 2. The requirements of an execution
structure, in particular axiom A4 necessitate that we introduce additional real-time partial order
edges
as follows.
(S’.Pop, 11)

(S.Push(42), ⊥)

(S.Pop, 42)

(S’.Push(11), ⊥)

For example, the edge (S.Pop, 42)
(S.Push(42), ⊥) is induced by the combination of edges
(S.Pop, 42) (S’.Push(11), ⊥) (S’.Pop, 11) (S.Push(42), ⊥) together with axiom A4.
A consequence of these additional real-time partial order edges is that S (and symmetrically
S’) is not linearizable since the edge (S.Pop, 42) (S.Push(42), ⊥) must be present even when
restricting the structure to S only. Hence compositionality no longer fails.

4

Causal linearizability

This section provides a formal definition of causal linearizability, and the compositionality theorem. We define sequential objects in Section 4.1, then define causal linearizability in Section 4.2.

4.1

Sequential specifications

Causal linearizability defines correctness of a concurrent object with respect to a sequential object
specification.
Definition 5 (Sequential object). A sequential object is a pair (Σ, legal ), where legal ⊆ Σ∗ is a
prefix-closed sequence of labels.
3 The

original presentation allows for infinite execution structures, placing a well-foundedness condition on

5

.

For example, in each legal sequence of a stack, each pop operation returns the value from the
latest push operation that has not yet been popped, or empty if no such operation exists.
For each sequential object, we define a conflict relation, # ⊆ Σ × Σ, based on the legal
behaviours of the object. Two operations conflict if they do not commute in some legal history:
o#o′ = ¬(∀k1 , k2 ∈ Σ∗ . k1 o o′ k2 ∈ legal ⇔ k1 o′ ok2 ∈ legal )
For a stack, we have, for instance, (Push(n), ⊥)#(Pop, n′ ) for any n, n′ , and for n 6= n′ ,
(Push(n), ⊥)#(Push(n′ ), ⊥).
We now show (in Lemma 6 below) that the order of conflicting actions in a sequential history
captures all the orders in that history that matter. This is formalized and proved using order
relations derived from a legal sequence. However, since the same action can occur more than
once in a legal sequence, we lift actions to events by enhancing each action with a unique tag and
process identifier4 . Thus, given a sequential object S = (Σ, legal ) an S-event is a triple (g, p, a)
where g is an event tag (taken from a set of tags G), p is a process (taken from a set of processes
P ) and a is a label in Σ. We let Evt be the set of all S-events, and for a sequence k ∈ Evt ∗ , ev (k)
be the set of events in k.
The definitions of legality and conflict as well as sequential specifications can naturally be
lifted to the level of events by virtue of the action labels. That is, a sequence of events is legal
if the sequence of actions it induces is legal. In the following, we therefore use legal to refer
to sequences of actions and sequences of events interchangeably. From a sequence k ∈ Evt ∗ we
derive two relations on events, a temporal ordering ( k ) and a causal ordering (≺k ), where:
e

k

e′ = ∃k1 , k2 , k3 ∈ Evt ∗ . k = k1 ek2 e′ k3

e ≺k e′ = e

k

e′ ∧ e#e′

Any sequential history that extends the causal order of a legal history is itself legal. We formalize
this in the following lemma.
Lemma 6 (Legal linear extensions). For a sequential object (Σ, legal ), if k ∈ legal and k ′ ∈ Evt ∗ ,
such that ev (k) = ev (k ′ ) and ≺k ⊆ k′ , then k ′ ∈ legal .
Proof. We transform k into k ′ by reordering events in k to match the order k′ . We only reorder
events that are not conflicting and thus, each step of the transformation preserves legality. This
is sufficent to prove that k ′ ∈ legal . Let a mis-ordered pair be any pair of events e, e′ such that
e k e′ but e′ k′ e. Note that in this case, we have e 6≺k e′ , because ≺k ⊆ k′ . Let e1 , e2 be a
mis-ordered pair with minimal distance in k between the two elements (i.e., so that the number
of events in k between e1 and e2 is minimal). We will reorder non-conflicting events in k so as to
eliminate this mis-ordered pair, or reduce its size without creating a new mis-ordered pair. Once
all mis-ordered pairs have been eliminated, we will have transformed k into k ′ , while preserving
the legality of k.
If e1 and e2 are adjacent in k, then because e1 6≺k e2 , we have ¬(e1 #e2 ), and thus we can
reorder them to form a new sequence legal with fewer mis-ordered pairs.
If e′1 #e2 then we would have e1 ≺k e′1 ≺k e2 and so e1 ≺k e2 , which is a contradiction. The
same argument shows that there is no event between e′1 and e2 that conflicts with both. So let
k ′′ be the sequence derived from k by reordering e′1 forward just past e2 . Note that because there
were no conflicts, k ′′ ∈ legal. It remains to show that k ′′ has no mis-ordered pairs that were not
already present in k. This could only happen if there was some e′2 such that e′1 S e′2 S e2 and
e′1 k′ e′2 . Because e1 , e2 is the mis-ordered pair with minimal gap in k, it must be that e′2 k′ e2 ,
but then e′2 k′ e1 while e1 k e′2 . Thus, in this case, e1 , e′2 forms a smaller mis-ordered pair,
contrary to hypothesis.
4 Strictly speaking, the process identifier is unimportant for Lemma 6, but we introduce it here to simplify
compatibility with the rest of this paper.

6

As we shall see, this lemma is critical in the proof of our compositionality result, Theorem 10.

4.2

Concurrent executions and causal linearizability

We now define causal linearizability. For simplicity, we assume complete concurrent executions,
i.e., executions in which every invoked operation has returned. It is straightforward to extend
these notions to cope with incomplete executions.
In general, executions of concurrent processes might invoke operations on several concurrent
objects. To capture this, we define a notion of object family, which represents a composition of
sequential objects, indexed by some set X.
Definition 7 (Object family). Suppose X is an index set. For each x ∈ X, assume a sequential
object Sx = (Σx , legal x ) such that Σx is disjoint from Σy for all y ∈ X\{x}. We define the object
family over X, SX = (ΣX , legal X ) by:
S
• ΣX = x Σx
• legal X = {k ∈ Σ∗X | ∀x. k ⇂ x ∈ legal x }, where k ⇂ x is the sequence k restricted to actions
of object x. Thus the set legal X contains exactly the interleavings of elements of each of
the legal x .
N.B., the pairwise disjointness requirement on Σx can be readily achieved by attaching the object
identifier x to each operation in Σx .
An execution structure (E, , ) is a complete S-execution structure iff all events in E are
S-events.
Definition 8 (Causal linearizability). Let SX = (ΣX , legal X ) be an object family. A complete
SX -execution structure (E, , ) is causally linearizable if there exists a k ∈ legal X with ev (k) =
E such that
⊆ k , and
⊇ ≺k .
Condition
⊆ k ensures that the real-time (partial) order of operations is consistent with
the chosen k, while condition
⊇ ≺k captures the idea that the causal ordering in k (i.e.,
the ordering between conflicting actions) requires a communication in the concurrent execution.
Causal linearizability for single objects is a special case of Definition 8, where the family is a
singleton set.
To establish compositionality, we must first define an object family’s causal ordering. Note
that because an object family’s legal set is just an interleaving of the underlying object’s legal
sets, operations from distinct objects can always be reordered, and therefore they never conflict.
Thus, we have the following lemma.
Lemma
S 9. Suppose SX = (ΣX , legal X ) is an object family. For any k ∈ legal X , we have
≺k = x∈X ≺k ⇂ x .
For an object family SX = (ΣX , legal X ) and x ∈ X, we let Ex be the SX -execution structure
E restricted to Σx .
Theorem 10 (Compositionality). Suppose SX = (ΣX , legal X ) is an object family over X, and
let E = (E, , ) be a complete SX -execution structure. Then, Ex is causally linearizable w.r.t.
Sx for all x ∈ X iff E is causally linearizable w.r.t. SX .
Proof. The implication from right to left is straightforward. For the other direction, for each
x ∈ X, let kx be the legal sequential execution witnessing causal linearizability of Ex . Let
be
the irreflexive transitive relation defined by
[
=( ∪
≺kx )+
x∈X

7

We show that
is acyclic, and is therefore a strict partial order. Because
is a partial order,
there is some total order
⊇
,
where
m
∈
legal
.
This
total
order
defines
a sequence of
m
X
labels of SX . We prove that this sequence witnesses the causal linearizability of E. By definition,
⊆ m for all x, and so by Lemma 6, we have m ⇂ x ∈ legal x (where m ⇂ x
we have ≺kx ⊆
is the restriction of m to the events of object x). Furthermore,
1.

⊆

2.

⊇ ≺kx follows from causal linearizability of Ex , and hence

m

follows from

⊆

⊆

m,

⊇

S

x∈X

≺kx , as required.

Thus, E is causally linearizable, as required.
We show that
is acyclic by contradiction. Suppose
contains a cycle. Pick P = e1
e2
...
en to be the minimal cycle. Since
is acyclic, and each ≺x is acyclic, the cycle P
must contain accesses to least two different objects. Without loss of generality, assume e1 and
e2 access different objects, i.e., e1 ∈ Ey , e2 ∈ Ez for some y 6= z. Since each ≺x only orders
e2 . Observe that P must be of length greater than two, i.e.,
elements of Ex , we must have e1
it cannot be of the form e1
e2
e1 since we would then have e1 e2 e1 , which contradicts
the assumption that
is a partial order.
Hence P must contain a third (distinct) element e3 . Note that e2 6 e3 , because otherwise
we could shorten the cycle P , using the transitivity of . Thus e2 , e3 are from the same object
z and e2 ≺kz e3 . By the causal linearizability of Ez , we must have e2 e3 . Let e be the element
of P following e4 (so possibly e = e1 ). Note that e3 6≺kz e, because otherwise we could shorten
e, so we have
the cycle P , using the transitivity of ≺kz . Thus, e3
e1

e2

e3

By the execution structure axiom A4, we have e1
···
e1 contradicting minimality of P .

4.3

e
e, and hence there exists a cycle e1

e

Relationship with classical linearizability

In this section, we show that classical linearizablity, which is defined for totally ordered histories of invocations (events of type Inv ) and responses (events of type Res), degenerates to
causal linearizability. As in the previous section, for simplicity, we assume the histories under
consideration are complete; extensions to cope with incomplete histories are straightforward.
First, we describe a method, inspired by the execution structure constructions given by
Lamport [23], for constructing execution structures for any well-formed partially ordered history.
We let Hist = (Inv ∪ Res) × (Inv ∪ Res) denote the type of all histories. A history is well-formed
if it is a partial order and the history restricted to each process is a total order of invocations
followed by their matching response. The set of all matching pairs of invocations and responses in
a history h is given by mp(h). A history is sequential iff it is totally ordered and each invocation
is immediately followed by its matching response. Note that a history could be totally ordered,
but not sequential (as is the case for the concurrent histories considered under SC [19, 18]).
Definition 11. Let h ⊆ Hist be a well-formed (partially ordered) history. We say exec(h) =
(E, , ) is the execution structure corresponding to h if
E = mp(h)
= {((i1 , r1 ), (i2 , r2 )) ∈ E × E | (r1 , i2 ) ∈ h}
= {((i1 , r1 ), (i2 , r2 )) ∈ E × E | (i1 , r2 ) ∈ h}

8

We now work towards the standard definition of linearizability. Recall that a sequential object
(see Definition 5) is defined in terms of sequences of labels of type Σ∗ , where Σ = Inv × Res,
whereas sequential histories are of type Hist . Thus, we define a function γ : Hist → Σ∗ such that
for each pair (i, r), (i′ , r′ ) ∈ mp(hs) of sequential history hs we have (r, i′ ) ∈ hs iff (i, r) γ(hs)
(i′ , r′ ). Thus, the order of operations in hs and γ(hs) are identical.
A complete history h is linearizable w.r.t. a (family of) sequential object(s) S = (Σ, legal ) iff
there exists a sequential history hs such that γ(hs) ∈ legal , for each process p, h ⇂ p = hs ⇂ p and
h ⊆ hs [18].
Theorem 12. Suppose h is a totally ordered complete history and S a (family of ) sequential
object(s). Then h is linearizable w.r.t S iff exec(h) is causally linearizable w.r.t. S.

5

Causal linearizability of C11 implementations

We now introduce the C11 memory model, where we adapt the programming-language oriented
presentation of C11 [21, 10], but we ignore various features of C11 not needed for our discussion,
including non-atomic operations and fences.
The C11 memory-model. Let L be a set of locations (ranged over by x, y), let V be a set of
values (ranged over by u, v). Our model employs a set of memory events, which can be partitioned
into read events, R, write events, W , and update events, U . Moreover, let Mod = W ∪ U be
the set of events that modify a location, and Qry = R ∪ U be the set of events that query
a location. For any memory event e, let loc(e) be the event’s location, and let ann(e) be the
event’s annotation. Let Loc(x) = {e | loc(e) = x}. For any query event let rval(e) be the value
read; and for any modification event let wval(e) be the value written. An event may carry a
synchronisation annotation, which may either be a release, R, or an acquire, A, annotation.
A C11 execution (not to be confused with an execution structure) is a tuple D = (D, sb, rf , mo)
where D is a set of events, and sb, rf , mo ⊆ D × D define the sequence-before, reads-from and
modification order relations, respectively. We say a C11 execution is valid when it satisfies:
(V1) sb is a strict order, such that, for each process p, the projection of sb onto p is a total order;
(V2) for all (w, r) ∈ rf , loc(w) = loc(r) and wval(w) = rval(r);
(V3) for all r ∈ D ∩ Qry, there exists some w ∈ D ∩ Mod such that (w, r) ∈ rf ;
(V4) for all (w, w′ ) ∈ mo, loc(w) = loc(w′ ); and
(V5) for all w, w′ ∈ W such that loc(w) = loc(w′ ), (w, w′ ) ∈ mo or (w′ , w) ∈ mo.
Other relations can be derived from these basic relations. For example, assuming DR and DA
denote the sets of events with release and acquire annotations, respectively, the synchronises-with
relation, sw = rf ∩ (DR × DA ), creates interthread ordering guarantees based on synchronisation
annotations. The from-read relation, fr = (rf −1 ; mo) \ Id, relates each query to the events in
modification order after the modification that it read from. Our final derived relation is the
happens before relation hb = (sb ∪ sw )+ , which formalises causality. We say that a C11 execution
is consistent if
(C1) hb is acyclic, and
(C2) hb; (mo ∪ rf ∪ fr ) is irreflexive.

9

Method invocations and responses. So far, the events apearing in our memory model are
standard. Our goal is to model algorithms such as the Treiber stack. Thus, we add method events
to the standard model, namely, invocations, Inv , and responses, Res. Unlike weak memory at
the processor architecture level, where program order may not be preserved [13], program order
in C11 is consistent with happens-before order, and hence, these can be introduced here in a
straightforward manner. The only additional requirement is that validity also requires (V6) sb
for each process projected restricted Inv ∪ Res must be alternating sequence of invocations and
matching responses, starting with an invocation.
Dynamic memory. To describe the behaviour of algorithms, such as the Treiber Stack, we
must define reads and writes to higher-level structures. To this end, we develop a simple theory
of references to objects, the fields of those objects and memory allocations for the object. We
let F be the set of all fields and A be the set of all memory allocation events, which is an event
of the form A(l) for a location l. We let . : L × F → L be the function that returns a location
for a given location, field pair. We use infix notation x.f for .(x, f ), where x ∈ L and f ∈ F .
We then introduce three additional constraints: (A1) for every a, a′ ∈ E ∩ A, if loc(a) = loc(a′ )
then a = a′ ; and (A2) if l.f = l′ .f ′ then l = l′ and f = f ′ . (A3) for all locations l and fields f
there are no allocations of the form A(l.f ).
From C11 executions to execution structures. A C11 execution with method invocations
and responses naturally gives rise to an execution structure. First, for a C11 execution F, let the
history of D, denoted hist(D) be the happens-before relation for D restricted to the invocation and
response events. By (V6), hist(D) is a well-formed history. Thus, we can apply the construction
defined in Section 4.3 to build an execution structure exec(hist(D)).
Definition 13. We say that a C11 execution D is causally linearizable w.r.t a sequential object
if exec(hist(D)) is.
We can now state a compositionality result for a C11 execution D of an object family X. The
property follows from Theorem 10 and the fact that for any object x ∈ X, exec(hist(Dx )) =
exec(hist(D))x , where Dx is D restricted to events of object x. Note that Dx contains all events
of x, i.e., all invocations, responses and low-level memory operations of x.
Corollary 14 (Compositionality for C11 executions). Suppose that SX = (ΣX , legal X ) is an
object family over X, and let D be an execution. Then, Dx is causally atomic w.r.t. Sx for all
x ∈ X iff D is causally atomic w.r.t. SX .
Finally, note that because the sb relation is included in hb, hist(D) includes program order
on the invocations and responses of D.

6

Verification

We now describe an operational method for proving that a given C11 execution is causally
linearizable w.r.t a given sequential object. Accordingly, we give a state-based, operational
model of a sequential object that generates legal sequences of labels (Definition 5), then present
a simulation-based proof rule for causal linearizability (Section 6.1). Then, we illustrate our
technique on the Treiber Stack (Section 6.2).

6.1

A simulation relation over happens-before

An operational sequential object is a tuple (Γ, init , τ ) where: Γ is a set of states; init ∈ Γ is the
initial state and τ : Γ × H × Inv →
7 Γ × H, where H = (Inv × Res)∗ , is a partial update function
10

that applies an invocation to a state and a history, returning the resulting state and updated
history. We require that for s ∈ Γ, h ∈ H and i ∈ Inv , there exists some r ∈ Res, such that
τ (s, h, i) = ( , h · h(i, r)i), where we use · for sequence concatenation. This response r is the
object’s response to the invocation i.
Example 15 (Operational sequential stack). A stack containing natural numbers can be represented as an operational sequential object in the following way. Let Γ = N∗ , init = h i and
define the update function as follows
τ (s, h, Push(n)) = (n · s, h · h(Push(n), ⊥)i)

τ (n · s, h, Pop) = (s, h · h(Pop, n)i)

for n ∈ N and s ∈ Γ. Note that assuming i is a stack invocation (as per Section 3), τ (s, i) is
defined iff s 6= h i or i 6= Pop.
Given an operational sequential object S = (Γ, init , τ ), it is easy to construct a corresponding
sequential object (in the sense of Definition 5). Let ΣS = Inv × Res and let legal S be the set of
histories returned by τ . Thus (ΣS , legal S ) is a sequential object, and our method verifies causal
linearizability w.r.t that object.
For the remainder of this section, fix a C11 execution D = (D, sb, rf , mo), and an operational
sequential object S = (Γ, init , τ ). We describe a method for proving that D is causally linearizable
w.r.t S. Our proof method is an induction on the length of some linear extension of D’s hb order.
The proof proceeds by remembering the set Z ⊆ D of events that have already been considered
by the induction, i.e., Z defines the current stage of the induction. The set Z is assumed to be
downclosed with respect to hb, i.e., if z ∈ Z and (z ′ , z) ∈ hb, then z ′ ∈ Z. At each stage of the
induction, we add an arbitrary e ∈
/ Z to Z, where e’s hb predecessors are already in Z (i.e., the
set Z ∪ {e} is also downclosed w.r.t. hb).
Correctness of each inductive step is formalised by a simulation relation, ρ, relating the events
in the current state, Z, to a state of the operational sequential object. Each inductive step of
the implementation must match a “move” of the sequential object, i.e., be a stutter step, or a
state update as given by the update function of the sequential object. Moreover, assuming that
ρ holds for Z (before each inductive step), ρ must hold after the step (i.e., for Z ∪ {e}).
Following the existing verification literature [12], we refer to events corresponding to nonstuttering steps as linearization points: the points where the high-level operation appears to
take effect. The verifier must define a function lp : D ∩ Inv → D to determine the memory
event that linearizes the given invocation, and this function must satisfy certain constraints with
respect to the simulation relation ρ, as described in Definition 16, below.
For each low-level operation, we must also determine the invocation and response to which
it belongs. Thus we also define a function µ : D → D ∩ Inv that maps each event in D to the
invocation responsible for producing e, and a function and ν : D → D ∩ Res that that maps e to
the response produced by e’s invocation. More formally, µ(e) is the latest invocation in sb-order
prior to e, and ν(e) is the earliest response in sb-order after e.
Thus, we obtain the following definition.
Definition 16 (hb-simulation). Suppose D = (D, sb, rf , mo) is an execution and S = (Γ, init , τ )
an operational sequential object. An hb-simulation is a relation ρ ⊆ 2D × (Γ × H) such that:
1. ρ(∅, (init , h i)), and

(initialisation)

2. for all Z ⊆ D, and events e ∈ D\Z such that Z ∪{e} is down-closed w.r.t D’s happens-before
order, if ρ(Z, (s, h)) then
(a) if e 6= lp(µ(e)) then ρ(Z ∪ {e}, (s, h)),
11

(stutter step)

(b) if e = lp(µ(e))
provided i = µ(e), h′ = h · h(i, r)i, and τ (s, h, i) = (s′ , h′ ), then

(linearization step)

i. ρ(Z ∪ {e}, (s′ , h′ )), and
ii. ν(e) = r, and
iii. for all operations (i′ , r′ ) in h, if (i′ , r′ ) ≺h′ (i, r) then (lp(i′ ), e) ∈ hb.
The initialisation is straightforward, while the two inductive steps consider a new e for inclusion in Z following hb order. If e is a stutter step, we only have to prove that ρ is preserved
by adding e to Z. If e is a linearization step (that is, if e = lp(µ(e))), then there are three
obligations: prove that ρ is preserved (2(b)i); prove that the response of the high-level operation
matches that returned by the sequential object (2(b)ii); and prove that whenever some operation
that has already been linearized is causally prior to the newly linearized operation, then that
operation’s linearization point is hb-prior to the new event e (2(b)iii).
Theorem 17 (Soundness of hb-simulation). If ρ is an hb-simulation for a C11 execution D,
then D is causally linearizable.
Proof. The proof below uses a formulation of an operational sequential object where τ that does
not maintain a history.
Fix the operational sequential object S = (Γ, init , τ ). Fix the execution D, and let ≤E be
any linear extension of D’s hb relation. Assume that lp is the linearization function and ρ is the
simulation relation.
We perform an induction on the indexes of ≤E . Let en be the nth event in ≤E order, so we
are indexing from 0. Let Zn be the set of events strictly below the nth index. Thus,
Zn = {em | m < n}
Note that Z0 = ∅ and Zn+1 = Zn ∪ {en }. We define a function rep : {n | n < | ≤E |} → Γ
recursively as follows:
rep(0) = init

(1)

rep(n + 1) = rep(n)
rep(n + 1) = π1 (τ (rep(n), µ(en ))

when lp(µ(en )) 6= en
when lp(µ(en )) = en

(2)
(3)

By induction, we have ρ(Zn , rep(n)) for all n < | ≤E |.
• Because ρ(Z0 , rep(0)) = ρ(∅, init ), Proposition 1 ensures that ρ(Z0 , rep(0)).
• Assume ρ(Zn , rep(n)) and lp(µ(en )) 6= en . Then ρ(Zn+1 , rep(n+1)) = ρ(Zn ∪{en }, rep(n)),
and thus Property 2a ensures that ρ(Zn+1 , rep(n + 1)).
• Assume ρ(Zn , rep(n)) and lp(µ(en )) = en .
Then ρ(Zn+1 , rep(n + 1)) = ρ(Zn ∪ {en }, π1 (τ (rep(n), µ(en ))), and thus Property 2(b)i
ensures that ρ(Zn+1 , rep(n + 1)).
We turn now to defining k, the legal sequence we need to witness causal linearizability of D.
k0 = hi
kn+1 = kn
rep(n + 1) = kn · h(µ(e), ν(e))i

12

when lp(µ(en )) 6= en

(4)
(5)

when lp(µ(en )) = en

(6)

It is easy to see that this is a legal history, and that (kn , rep(n)) is a move.
We need to show that ≤H ⊆ k . Consider a response r and invocation i such that (r, i) ∈ hb.
Ley i′ be the invocation of r, and let r′ be the response of i.. Because µ(lp(i)) = i, we have
{(lp(i′ ), r), (i, lp(i))} ∈ sb ⊆ hb, and thus (lp(i′ ), lp(i)) ∈ hb and so lp(i′ ) appears at an earlier
point in ≤E than lp(i), and therefore (i′ , r) k (i, r′ ), as required.
Finally, we must show that ≺k ⊆ D . This is a simple induction on the length of k, with the
hypothesis that, for all operations (i, r), (i′ , r′ ) in k, if (i, r) ≺k (i′ , r′ ) then (lp(i), lp(i′ ) ∈ hb. At
each step we apply Property 2(b)iii. Thus, for each existing operation (i, r) and new operation
(i′ , r′ ), we have (i, r) ≺k (i′ , r′ ) =⇒ (lp(i), lp(i′) ∈ hb immediately. On the other hand,
(i′ , r′ ) ≺k (i, r) is impossible, because (i′ , r′ ) k (i, r) is false.
This completes oour proof.

6.2

Case-study: the Treiber Stack

We now outline an hb-simulation relation ρ for the Treiber stack. We fix some arbitrary C11
execution D = (D, sb, rf , mo) that contains an instance of the Treiber stack. That is, the
invocations in D are the stack invocations, and the responses are the stack responses (as given
in Section 3). Furthermore, the low-level memory operations between these invocations and
responses are generated by executions of the operations of the Treiber stack (Algorithm 1).
The main component of our simulation relation guarantees correctness of the data representation, i.e., the sequence of values formed by following next pointers starting with &T op forms an
appropriate stack, and we focus on this aspect of the relation. As is typical with verifications of
shared-memory algorithms, there are various other properties that would need to be considered
in a full proof.
In a sequentially consistent setting, the data representation can easily be obtained from
the state (which maps locations to values). However, for C11 executions calculating the data
representation requires a bit more work. In what follows, we define various functions that depend
on a set Z of events, representing the current stage of the induction.
We define the latest write in Z to a location x as latestZ (x) = max(mo ⇂(Z ∩ Loc(x))) and
the current value of a location x in some set Z as cvalZ (x) = wval(latestZ (x)), which is the
value written by the last write to x in modification order. It is now straightforward to construct
the sequence of values corresponding to a location as stackOf Z (x) = v · stackOf Z (y), where
v = cvalZ (x.val) and y = cvalZ (x.nxt).
Now, assuming that (s, h) is a state of the operational sequential stack, our simulation requires:
stackOf Z (cvalZ (&T op)) = s

(7)

Further, we require that all modifications of &T op are totally ordered by hb:
∀m, m′ ∈ Z ∩ M od(&T op). (m, m′ ) ∈ hb ∨ (m′ , m) ∈ hb

(8)

to ensure that any new read considered by the induction sees the most recent version of &T op.
The linearization function lp for the Treiber stack is completely standard: each operation is
linearized at the unique update operation generated by the unique successful CAS at line 9 (for
pushes) or line 16 (for pops).
In what follows, we illustrate how to verify the proof obligations given in Definition 16, for
the case where the new event e is a linearization point. Let e be an update operation that is
generated by the CAS at line 9 of the push operation in Algorithm 1. The first step is to prove
that every modification of &T op in Z is happens-before the update event e. Formally,
∀m ∈ Z ∩ Mod ∩ Loc(&T op). (m, e) ∈ hb
13

(9)

(S.Push(1), ⊥)

(S’.Pop, empty)

(S.Push(1), ⊥)

(S’.Push(2), ⊥)

(S.Pop, empty)

(S’.Push, ⊥)

Figure 3: Read-only operations without
communication (not compositional)

(S’.Pop, empty)

(S.Pop, empty)

Figure 4: Read-only operations with communication (compositional)

Proving this formally is somewhat involved, but the essential reason is as follows. Note that
there is an acquiring read r to &T op executed at line 7 of e’s operation and sb-prior to e. r reads
from some releasing update u. Thus, by Property 8, and the fact the hb contains sb, e is happens
after u, and all prior updates. If there were some update u′ of &T op such that (u′ , e) ∈
/ hb, then
(u′ , u) ∈
/ hb so by Property 8, (u, u′ ) ∈ hb. But it can be shown in this case that the CAS that
generated e could not have succeeded, because u′ constitutes an update intervening between r
and e. Therefore, there can be no such u′ .
Property 9 makes it straightforward to verify that Condition 2(b)iii of Definition 16 is satisfed.
To see this, note that every linearization point of every operation is a modification of &T op.
Thus, if (i′ , r′ ) is some operation such that lp(i′ ) ∈ Z (so that this operation has already been
linearized) then (lp(i′ ), e) ∈ hb.
Using Property 9 it is easy to see that both Property 7 and Property 8 are preserved. We
show by contradiction that latestZ ′ (&T op) = e. Otherwise, we have (e, latestZ ′ (&T op)) ∈ mo.
/ hb, but latestZ ′ (&T op) is a modification operation, so this
Therefore (latestZ ′ (&T op), e) ∈
contradicts Property 9.
It follows from latestZ ′ (&T op) = e that stackOf (cvalZ ′ ) = stackOf (wval(e)). Given this, it
is straightforward to show that Property 7 is preserved. This step of the proof relies on certain
simple properties of push operations. Specifically, we need to show that the current value of the
val field of the node being added to the stack (formally, cvalZ ((wval(e)).nxt)) is the value passed
to the push operation; and that the current value of the nxt field (formally, cvalZ ((wval(e)).nxt))
is the current value of &T op when the successful CAS occurs. These properties can be proved
using the model of dynamic memory given in Section 5.

7

A synchronisation pitfall

We now describe an important observation regarding failure of compositionality of read-only
operations caused by weak memory effects. The issue can be explained using our abstract notion
of an execution structure, however, a solution to the problem is not naturally available in C11
with only release-acquire annotations.
Consider the Treiber Stack in Algorithm 1 that returns empty instead of spinning; namely
where the inner loop (lines 12-14) is replaced by code block “top :=A Top ; if top = null then
return empty”. Such an implementation could produce executions such as the one in Fig. 3
which, like the examples in Section 3, is not compositional. Recovering compositionality requires
one to introduce additional communication edges as shown in Fig. 4. In the C11 memory model,
these correspond to “from-read” anti-dependencies from a read to a write overwriting the value
read. However, release-acquire synchronisation is not adequate for promoting from-read order in
the memory to happens-before.
One fix would be to disallow read-only operations, e.g., by introducing a release-acquire CAS
operation on a special variable that always succeeds at the start of each operation. However, such
a fix is somewhat unnatural. Another would be to use C11’s SC annotations, which can induce
14

synchronisation across from-read edges. However, the precise meaning of these annotations is
still a topic of active research [22, 6].

8

Conclusion and related work

We have presented causal linearizability, a new correctness condition for objects implemented
in weak-memory models, that generalises linearizability and addresses the important problem of
compositionality. Our condition is not tied to a particular memory model, but can be readily applied to memory models, such as C11, that feature a happens-before relation. We have presented
a proof method for verifying causal linearizability. We emphasise that our proof method can be
applied directly to a standard axiomatic memory model. Unlike other recent proposals [11, 20],
we model C11’s relaxed accesses without needing to prohibit their problematic dependency cycles
(so called “load-buffering” cycles).
Although causal linearizability has been presented as a condition for concurrent objects, we
believe it is straightforward to extend this condition to cover, for example, transactional memory.
We intend to develop our approach into a framework in which the behaviour of programs that
mix transactional memory, concurrent objects and primitive weak-memory operations can be
precisely described in a compositional fashion.
Causal linearizability is closely related to causal hb-linearizability defined in [13], which is a
causal relaxation of linearizability that uses specifications strengthened with a happens-before
relation. The compositionality result there requires that either a specification is commuting or
that a client is unobstructive (does not introduce too much synchronisation). Our result is more
general as we place no such restriction on the object or the client. Others [9] define a correctness
condition, also called causal linearizabilty, that is only compositional when the client satisfies
certain constraints; in contrast, we achieve full decoupling. Furthermore, that condition is only
defined when the underlying memory model is given operationally, rather than axiomatically like
C11. Early attempts, targetting TSO architectures, used totally ordered histories but allowed
the response of an operation to be moved to a corresponding “flush” event [16, 7, 27, 14]. Others
have considered the effects of linearizability in the context of a client abstraction. This includes a
correctness condition for C11 that is strictly stronger than linearizability under SC [5]. Although
we have applied causal linearizability to C11, causal linearizability itself is more general as it can
be applied to any weak memory model with a happens-before relation. Causal consistency [2] is
a related condition, aimed at shared-memory and data-stores, which has no notion of real-time
order and is not compositional.

References
[1] Sarita V. Adve and Kourosh Gharachorloo. Shared memory consistency models: A tutorial.
IEEE Computer, 29(12):66–76, 1996.
[2] Mustaque Ahamad, Gil Neiger, James E. Burns, Prince Kohli, and Phillip W. Hutto. Causal
memory: definitions, implementation, and programming. Distributed Computing, 9(1):37–
49, Mar 1995.
[3] J. Alglave, L. Maranget, and M. Tautschnig. Herding cats: Modelling, simulation, testing,
and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1–7:74, 2014.
[4] M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C++ concurrency.
In Thomas Ball and Mooly Sagiv, editors, POPL, pages 55–66. ACM, 2011.
15

[5] Mark Batty, Mike Dodds, and Alexey Gotsman. Library abstraction for C/C++ concurrency. In Roberto Giacobazzi and Radhia Cousot, editors, POPL, pages 235–248. ACM,
2013.
[6] Mark Batty, Alastair F. Donaldson, and John Wickerson. Overhauling SC atomics in C11
and opencl. In POPL, pages 634–648. ACM, 2016.
[7] Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang. Concurrent library correctness on the TSO memory model. In Helmut Seidl, editor, ESOP,
volume 7211 of Lecture Notes in Computer Science, pages 87–107. Springer, 2012.
[8] S. Doherty, L. Groves, V. Luchangco, and M. Moir. Formal verification of a practical lockfree queue algorithm. In FORTE, volume 3235 of Lecture Notes in Computer Science, pages
97–114. Springer, 2004.
[9] Simon Doherty and John Derrick. Linearizability and causality. In SEFM, volume 9763 of
Lecture Notes in Computer Science, pages 45–60. Springer, 2016.
[10] Marko Doko and Viktor Vafeiadis. A program logic for C11 memory fences. In VMCAI,
volume 9583 of Lecture Notes in Computer Science, pages 413–430. Springer, 2016.
[11] Marko Doko and Viktor Vafeiadis. Tackling real-life relaxed concurrency with FSL++. In
ESOP, pages 448–475, 2017.
[12] B. Dongol and J. Derrick. Verifying linearisability: A comparative survey. ACM Comput.
Surv., 48(2):19:1–19:43, 2015.
[13] B. Dongol, R. Jagadeesan, J. Riely, and A. Armstrong. On abstraction and compositionality
for weak-memory linearisability. In VMCAI, volume 10747 of Lecture Notes in Computer
Science, pages 183–204. Springer, 2018.
[14] Brijesh Dongol, John Derrick, and Graeme Smith. Reasoning algebraically about refinement
on TSO architectures. In ICTAC, volume 8687 of Lecture Notes in Computer Science, pages
151–168. Springer, 2014.
[15] Ivana Filipovic, Peter W. O’Hearn, Noam Rinetzky, and Hongseok Yang. Abstraction for
concurrent objects. Theor. Comput. Sci., 411(51-52):4379–4398, 2010.
[16] Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang. Show no weakness: Sequentially consistent specifications of TSO libraries. In Marcos K. Aguilera, editor, DISC, volume
7611 of Lecture Notes in Computer Science, pages 31–45. Springer, 2012.
[17] Rachid Guerraoui and Michal Kapalka. On the correctness of transactional memory. In
Siddhartha Chatterjee and Michael L. Scott, editors, PPoPP, pages 175–184. ACM, 2008.
[18] M. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects.
ACM TOPLAS, 12(3):463–492, 1990.
[19] Maurice Herlihy and Nir Shavit. The art of multiprocessor programming. Morgan Kaufmann,
2008.
[20] Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. Strong
logic for weak memory: Reasoning about release-acquire consistency in iris. In ECOOP,
pages 17:1–17:29, 2017.

16

[21] Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. Taming release-acquire consistency. In
Rastislav Bodı́k and Rupak Majumdar, editors, POPL, pages 649–662. ACM, 2016.
[22] Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. Repairing
sequential consistency in C/C++11. In PLDI, pages 618–632. ACM, 2017.
[23] L. Lamport. On interprocess communication. part I: basic formalism. Distributed Computing, 1(2):77–85, 1986.
[24] Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers, 28(9):690–691, 1979.
[25] J. Manson, W.Pugh, and S. V. Adve. The Java memory model. In POPL, pages 378–391.
ACM, 2005.
[26] Gerhard Schellhorn, John Derrick, and Heike Wehrheim. A sound and complete proof
technique for linearizability of concurrent data structures. ACM Trans. Comput. Log.,
15(4):31:1–31:37, 2014.
[27] Oleg Travkin and Heike Wehrheim. Handling TSO in mechanized linearizability proofs. In
Haifa Verification Conference, volume 8855 of Lecture Notes in Computer Science, pages
132–147. Springer, 2014.
[28] R. K. Treiber. Systems programming: Coping with parallelism. Technical Report RJ 5118,
IBM Almaden Res. Ctr., 1986.

17

A

Potentially incomplete executions

A complication with concurrent executions is that they may contain incomplete operations (that
have been invoked, but have not yet returned). Since the effect of an incomplete operation may
be globally visible, they cannot simply be ignored. This phenomenon has been well studied and
arises in the definitions of linearizability [18] and opacity [17]. This section describes how we
cope with incomplete operations in the context of causal linearizability.
We define the completable extension of a sequential object S = (Σ, legal ) to be a triple
T = (S, I, C), where I is a set of allowable incomplete actions and C : I → 2Σ is a completion
function that maps each I to a set of possible completions for I.
Example 18. If S = (Σ, legal ) is a concurrent object the set of allowable incomplete operations
and completion function is defined by:
I = {i ∈ Inv | ∃k1 , k2 ∈ Σ∗ . ∃r. k1 (i, r)k2 ∈ legal}

C = λi. {(i, r) ∈ Σ}

For the Treiber stack in Algorithm 1, we have IS = {Push(n) | n ∈ N}∪{Pop}, and CS (Push(n)) =
{⊥} and CS (Pop) = N ∪ {empty}.
S A completable extension of an object family SX is a triple TX = (SX , IX , CX ), where IX =
x Ix and CX (a) = Cx (a), with x being the unique element of X such that a ∈ Σx .
We say that E = (E, , ) is a T-execution structure iff E ⊆ Σ∪I such that dom( )∩I = ∅,
i.e., no element of E may depend (in real-time order) on an element in I. Note that there may be
edges both in and out of elements in E ∩ I and
edges into E ∩ I. A T-execution structure
is causally atomic if we can replace all incomplete events by complete events in a way that is
allowed by the corresponding sequential object. This process is analagous to the extension of
incomplete histories to complete histories, as allowed by linearizability and opacity in the classical
(i.e., sequentially consistent) setting.
Definition 19 (Causal linearizability). Let S = (Σ, legal ) be a family of sequential objects and T
its completable extension. A T-execution structure E = (E, , ) is causally atomic w.r.t. S iff
there exists a causally atomic S-execution structure E′ = (E ′ , ′ , ′ ) and an (order-preserving)
isomorphism ϕ : E → E′ such that:
• for each event e = (g, p, i) ∈ E, where i ∈ I, we have ϕ(e) = (g, p, a) for some a ∈ C(i),
and
• for each event e = (g, p, a) ∈ E, where a ∈ Σ, we have ϕ(e) = (g, p, a).
Theorem 10 extends directly to the case of incomplete histories. The fact that each individual
object history is causally atomic implies that we can assume the existence of a valid extension
for each incomplete event, which is itself causally atomic. Thus, we can apply these per-object
extensions to the object-family execution, and show, using the proof of Theorem 10, that the
resulting complete execution structure is causally atomic.

18

