Logical Methods in Computer Science
Vol. 9(3:12)2013, pp. 1–47
www.lmcs-online.org

Submitted
Published

Feb. 15, 2013
Sep. 9, 2013

LINEARIZABILITY WITH OWNERSHIP TRANSFER
ALEXEY GOTSMAN a AND HONGSEOK YANG b
a

IMDEA Software Institute, Madrid, Spain
e-mail address: Alexey.Gotsman@imdea.org

b

University of Oxford, Oxford, UK
e-mail address: Hongseok.Yang@cs.ox.ac.uk

Abstract. Linearizability is a commonly accepted notion of correctness for libraries of
concurrent algorithms. Unfortunately, it assumes a complete isolation between a library
and its client, with interactions limited to passing values of a given data type. This is
inappropriate for common programming languages, where libraries and their clients can
communicate via the heap, transferring the ownership of data structures, and can even
run in a shared address space without any memory protection.
In this paper, we present the first definition of linearizability that lifts this limitation
and establish an Abstraction Theorem: while proving a property of a client of a concurrent
library, we can soundly replace the library by its abstract implementation related to the
original one by our generalisation of linearizability. This allows abstracting from the
details of the library implementation while reasoning about the client. We also prove
that linearizability with ownership transfer can be derived from the classical one if the
library does not access some of data structures transferred to it by the client.

1. Introduction
The architecture of concurrent software usually exhibits some forms of modularity. For
example, concurrent algorithms are encapsulated in libraries and complex algorithms are
often constructed using libraries of simpler ones. This lets developers benefit from readymade libraries of concurrency patterns and high-performance concurrent data structures,
such as java.util.concurrent for Java and Threading Building Blocks for C++. To simplify
reasoning about concurrent software, we need to exploit the available modularity. In particular, in reasoning about a client of a concurrent library, we would like to abstract from
the details of a particular library implementation. This requires an appropriate notion of
library correctness.
Correctness of concurrent libraries is commonly formalised by linearizability [18], which
fixes a certain correspondence between the library and its specification. The latter is usually
just another library, but implemented atomically using an abstract data type; the two
libraries are called concrete and abstract, respectively. A good notion of linearizability
should validate an Abstraction Theorem [12, 14]: the behaviours of any client using the
2012 ACM CCS: [Theory of computation]: Semantics and reasoning.
Key words and phrases: Concurrency, Linearizability, Ownership Transfer, Semantics, Data Abstraction.

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.2168/LMCS-9(3:12)2013

CC

A. Gotsman and H. Yang
Creative Commons

2

A. GOTSMAN AND H. YANG

concrete library are contained in the behaviours of the client using the abstract one. This
makes it sound to replace a library by its specification in reasoning about its client.
Classical linearizability assumes a complete isolation between a library and its client,
with interactions limited to passing values of a given data type as parameters or return
values of library methods. This notion is not appropriate for low-level heap-manipulating
languages, such as C/C++. There the library and the client run in a shared address space;
thus, to prove the whole program correct, we need to verify that one of them does not corrupt
the data structures used by the other. Type systems [8] and program logics [23] usually
establish this using the concept of ownership of data structures by a program component:
the right to access a data structure is given only to a particular component or a set of them.
When verifying realistic programs, this ownership of data structures cannot be assigned
statically; rather, it should be transferred between the client and the library at calls to
and returns from the latter. The times when ownership is transferred are not determined
operationally, but set by the proof method: as O’Hearn famously put it, “ownership is in the
eye of the asserter” [23]. However, ownership transfer reflects actual interactions between
program components via the heap, e.g., alternating accesses to a shared area of memory.
Such interactions also exist in high-level languages providing basic memory protection, such
as Java. In this case, we need to ensure that a client does not subvert a library by accessing
a memory object after its ownership was transferred to the latter.
For an example of ownership transfer between concurrent libraries and their clients
consider a memory allocator accessible concurrently to multiple threads. We can think of
the allocator as owning the blocks of memory on its free-list; in particular, it can store
free-list pointers in them. Having allocated a block, a thread gets its exclusive ownership,
which allows accessing it without interference from the other threads. When the thread
frees the block, its ownership is returned to the allocator. Trying to write to a memory cell
after it was freed has dire consequences.
As another example, consider any container with concurrent access, such as a concurrent
set from java.util.concurrent or Threading Building Blocks. A typical use of such a container
is to store pointers to a certain type of data structures. However, when verifying a client of
the container, we usually think of the latter as holding the ownership of the data structures
whose addresses it stores [23]. Thus, when a thread inserts a pointer to a data structure into
a container, its ownership is transferred from the thread to the container. When another
thread removes a pointer from the container, it acquires the ownership of the data structure
the pointer identifies. If the first thread tries to access a data structure after a pointer to it
has been inserted into the container, this may result in a race condition. Unlike a memory
allocator, the container code usually does not access the contents of the data structures
its elements identify, but merely ferries their ownership between different threads. For this
reason, correctness proofs for such containers [1,10,29] have so far established their classical
linearizability, without taking ownership transfer into account.
We would like to use the notion of linearizability and, in particular, an Abstraction
Theorem to reason about the above libraries and their clients in isolation, taking into
account only the memory that they own. To this end, we would like the correctness of a
library to constrain not only pointers that are passed between it and the client, but also
the contents of the data structures whose ownership is transferred. So far, there has been
no notion of linearizability that would allow this. In the case of concurrent containers, we
have no way of using classical linearizability established for them to validate an Abstraction

LINEARIZABILITY WITH OWNERSHIP TRANSFER

3

Theorem that would be applicable to clients performing ownership transfer. This paper fills
in these gaps.
Contributions. In this paper, we generalise linearizability to a setting where a library and
its client execute in a shared address space, and boundaries between their data structures
can change via ownership transfers. Linearizability is usually defined in terms of histories,
which are sequences of calls to and returns from a library in a given program execution,
recording parameters and return values passed. To handle ownership transfer, histories
also have to include descriptions of memory areas transferred. However, in this case, some
histories cannot be generated by any pair of a client and a library: while generating histories of a library we should only consider its executions in an environment that respects
ownership. For example, a client that transfers an area of memory upon a call to a library
not communicating with anyone else cannot then transfer the same area again before getting it back from the library upon a method return. We propose a notion of balancedness
that characterises those histories that treat ownership transfer correctly. We then define a
linearizability relation between balanced histories, matching histories of a concrete and an
abstract library (Section 3).
This definition does not rely on a particular model of program states for describing
memory areas transferred in histories, but assumes an arbitrary model defined by a separation algebra [7]. By picking a model with so-called permissions [5, 9], we can allow clients
and libraries to transfer non-exclusive rights to access certain memory areas in particular
ways, instead of transferring their full ownership. This makes our results applicable even
when libraries and their clients share access to some areas of memory. Our definition of
balancedness for arbitrary separation algebras relies on a new formalisation of the notion of
a footprint of a state, describing the amount of permissions the state includes (Section 2).
The rest of our technical development relies on a novel compositional semantics for a
language with libraries that defines the denotation of a library or a client considered separately in an environment that communicates with the component correctly via ownership
transfers (Sections 4 and 5). In particular, the semantics allows us to generate the set of
all histories that can be produced by a library solely from its code, without considering
all its possible clients. This, in its turn, allows us to lift the linearizability on histories to
libraries and establish the Abstraction Theorem (Section 6). On the way, we also obtain
an insight into the original definition of linearizability without ownership transfer, showing
a surprising relationship between one of the ways of its formulation and the plain subset
inclusion on the sets of histories produced by concrete and abstract libraries.
We note that the need to consider ownership transfer makes the proof of the Abstraction
Theorem highly non-trivial. This is because proving the theorem requires us to convert a
computation with a history produced by the concrete library into a computation with a
history produced by the abstract one, which requires moving calls and returns to different
points in the computation. In the setting without ownership transfer, these actions are
thread-local and can be moved easily; however, once they involve ownership transfer, they
become global and the justification of their moves becomes subtle, in particular, relying on
the fact that the histories involved are balanced (Section 7).
To avoid having to prove the new notion of linearizability from scratch for libraries that
do not access some of the data structures transferred to them, such as concurrent containers,
we propose a frame rule for linearizability (Section 8). It ensures the linearizability of such
libraries with respect to a specification with ownership transfer given their linearizability
with respect to a specification without one.

4

A. GOTSMAN AND H. YANG

We provide a glossary of notation at the end of the paper.
2. Footprints of States
2.1. Separation Algebras. Our results hold for a class of models of program states called
separation algebras [7], which allow expressing the dynamic memory partitioning between
libraries and clients.
Definition 2.1. A separation algebra is a set Σ, together with a partial commutative,
associative and cancellative operation ∗ on Σ and a unit element e ∈ Σ. Here commutativity
and associativity hold for the equality that means both sides are defined and equal, or
both are undefined. The property of cancellativity says that for each σ ∈ Σ, the function
σ ∗ · : Σ * Σ is injective.
We think of elements of a separation algebra Σ as portions of program states and the ∗
operation as combining such portions. The partial states allow us to describe parts of the
program state belonging to a library or the client. When the ∗-combination of two states is
defined, we call them compatible. Incompatible states usually make contradictory claims
about the ownership of memory. We sometimes use a pointwise lifting ∗ : 2Σ × 2Σ → 2Σ of
∗ to sets of states: for p, q ∈ 2Σ we let p ∗ q = {σ1 ∗ σ2 | σ1 ∈ p ∧ σ2 ∈ q}.
Elements of separation algebras are often defined using partial functions. We use the
following notation: g(x)↓ means that the function g is defined on x, g(x)↑ means that it
is undefined on x, dom(g) denotes the set of arguments on which g is defined, [ ] denotes
a nowhere-defined function, and g[x : y] denotes the function that has the same value as g
everywhere, except for x, where it has the value y. We also write for an expression whose
value is irrelevant and implicitly existentially quantified.
Below is an example separation algebra RAM:
Loc = {1, 2, . . .};

Val = Z;

RAM = Loc *fin Val.

A (partial) state in this model consists of a finite partial function from allocated memory
locations to the values they store. The ∗ operation on RAM is defined as the disjoint function
union ], with the nowhere-defined function [ ] as its unit. Thus, ∗ combines disjoint pieces
of memory.
More complicated separation algebras do not split memory completely, instead allowing
heap parts combined by ∗ to overlap. This is done by associating so-called permissions [5]
with memory cells in the model, which do not give their exclusive ownership, but allow
accessing them in a certain way. Types of permissions range from read sharing [5] to
accessing memory in an arbitrary way consistent with a given specification [9]. We now
give an example of a separation algebra with permissions of the former kind.
We define the algebra RAMπ as follows:
Loc = {1, 2, . . .};

Val = Z;

Perm = (0, 1];

RAMπ = Loc *fin (Val × Perm).

A state in this model consists of a finite partial function from allocated memory locations
to values they store and so-called permissions—numbers from (0, 1] that show “how much”
of the memory cell belongs to the partial state [5]. The latter allow a library and its client
to share access to some of memory cells. Permissions in RAMπ allow only read sharing:
when defining the semantics of commands over states in RAMπ , the permissions strictly
less than 1 are interpreted as permissions to read; the full permission 1 additionally allows

LINEARIZABILITY WITH OWNERSHIP TRANSFER

5

writing. The ∗ operation on RAMπ adds up permissions for memory cells. Formally, for
σ1 , σ2 ∈ RAMπ , we write σ1 ] σ2 if:
∀x ∈ Loc. σ1 (x)↓ ∧ σ2 (x)↓ =⇒ (∃u, π1 , π2 . σ1 (x) = (u, π1 ) ∧ σ2 (x) = (u, π2 ) ∧ π1 + π2 ≤ 1).
If σ1 ] σ2 , then we define
σ1 ∗ σ2 = {(x, (u, π)) | (σ1 (x) = (u, π) ∧ σ2 (x)↑) ∨ (σ2 (x) = (u, π) ∧ σ1 (x)↑) ∨
(σ1 (x) = (u, π1 ) ∧ σ2 (x) = (u, π2 ) ∧ π = π1 + π2 )};
otherwise, σ1 ∗ σ2 is undefined. The unit for ∗ is the empty heap [ ]. This definition of ∗
allows us, e.g., to split a memory area into two disjoint parts. It also allows splitting a cell
with a full permission 1 into two parts, carrying read-only permissions 1/2 and agreeing on
the value stored in the cell. These permissions can later be recombined to obtain the full
permission, which allows both reading from and writing to the cell.
Since we develop all our results for an arbitrary separation algebra, by instantiating
it with algebras similar to RAMπ , we can handle cases when a library and its client share
access to some memory areas.
Consider an arbitrary separation algebra Σ with an operation ∗. We define a partial
operation \ : Σ × Σ * Σ, called state subtraction, as follows: σ2 \ σ1 is a state in Σ
such that σ2 = (σ2 \ σ1 ) ∗ σ1 ; if such a state does not exist, σ2 \ σ1 is undefined. The
cancellativity of ∗ implies that σ2 \ σ1 is determined uniquely, and hence, the \ operation
is well-defined. When reasoning about ownership transfer between a library and a client,
we use the ∗ operation to express a state change for the component that is receiving the
ownership of memory, and the \ operation for the one that is giving it up.
Proposition 2.2. For all σ1 , σ2 , σ3 ∈ Σ, if σ1 ∗ σ2 and σ1 \ σ3 are defined, then
(σ1 ∗ σ2 ) \ σ3 = (σ1 \ σ3 ) ∗ σ2 .
2.2. Footprints. Our definition of linearizability uses a novel formalisation of a footprint
of a state, which, informally, describes the amount of memory or permissions the state
includes.
Definition 2.3. A footprint of a state σ in a separation algebra Σ is the set of states
δ(σ) = {σ 0 | ∀σ 00 . (σ 0 ∗ σ 00 )↓ ⇐⇒ (σ ∗ σ 00 )↓}.
In the following, l ranges over footprints. The function δ computes the equivalence class
of states with the same footprint as σ. In the case of RAM, we have δ(σ) = {σ 0 | dom(σ) =
dom(σ 0 )} for every σ ∈ RAM. Thus, states with the same footprint contain the same memory
cells. Definitions of δ for separation algebras with permissions are more complicated, taking
into account not only memory cells present in the state, but also permissions for them. In
the case of the algebra RAMπ , for σ ∈ RAMπ we have
δ(σ) = {σ 0 | ∀x. (σ(x)↓ ⇐⇒ σ 0 (x)↓) ∧
∀u, π. (σ(x) = (u, π) ∧ π < 1 =⇒ σ(x) = σ 0 (x)) ∧ (σ(x) = (u, 1) =⇒ σ 0 (x) = ( , 1))}.
In other words, states with the same footprint contain the same memory cells with the
identical permissions; in the case of memory cells on read permissions, the states also have
to agree on their values.

6

A. GOTSMAN AND H. YANG

Let F(Σ) = {δ(σ) | σ ∈ Σ} be the set of footprints in a separation algebra Σ. We now lift
the ∗ and \ operations on Σ to F(Σ). First, we define the operation ◦ : F(Σ)×F(Σ) * F(Σ)
for adding footprints. Consider l1 , l2 ∈ F(Σ) and σ1 , σ2 ∈ Σ such that l1 = δ(σ1 ) and
l2 = δ(σ2 ). If σ1 ∗ σ2 is defined, we let l1 ◦ l2 = δ(σ1 ∗ σ2 ); otherwise l1 ◦ l2 is undefined.
Proposition 2.4. The ◦ operation is well-defined.
Proof. Consider l1 , l2 ∈ F(Σ) and σ1 , σ2 ∈ Σ such that l1 = δ(σ1 ) and l2 = δ(σ2 ). Take
another pair of states σ10 , σ20 ∈ Σ such that l1 = δ(σ10 ) and l2 = δ(σ20 ). Thus, σ10 ∈ δ(σ1 ) and
σ20 ∈ δ(σ2 ), which implies:
(σ10 ∗ σ20 )↓ ⇐⇒ (σ1 ∗ σ20 )↓ ⇐⇒ (σ1 ∗ σ2 )↓.
Furthermore, if σ10 ∗ σ20 and σ1 ∗ σ2 are defined, then for all σ 0 ∈ Σ,
(σ10 ∗ σ20 ∗ σ 0 )↓ ⇐⇒ (σ1 ∗ σ20 ∗ σ 0 )↓ ⇐⇒ (σ1 ∗ σ2 ∗ σ 0 )↓.
Hence, δ(σ1 ∗ σ2 ) = δ(σ10 ∗ σ20 ), so that ◦ is well-defined.
For RAM, ◦ is just the pointwise lifting of the disjoint function union ].
To define a subtraction operation on footprints, we use the following condition.
Definition 2.5. The ∗ operation of a separation algebra Σ is cancellative on footprints
when for all σ1 , σ2 , σ10 , σ20 ∈ Σ, if σ1 ∗ σ2 and σ10 ∗ σ20 are defined, then
(δ(σ1 ∗ σ2 ) = δ(σ10 ∗ σ20 ) ∧ δ(σ1 ) = δ(σ10 )) =⇒ δ(σ2 ) = δ(σ20 ).
For example, the ∗ operations on RAM and RAMπ satisfy this condition.
When the ∗ operation of an algebra Σ is cancellative on footprints, we can define
an operation \\ : F(Σ) × F(Σ) * F(Σ) of footprint subtraction as follows. Consider
l1 , l2 ∈ F(Σ). If for some σ1 , σ2 , σ ∈ Σ, we have l1 = δ(σ1 ), l2 = δ(σ2 ) and σ2 = σ1 ∗ σ, then
we let l2 \\ l1 = δ(σ). When such σ1 , σ2 , σ do not exist, l2 \\ l1 is undefined.
Proposition 2.6. The \\ operation is well-defined.
Proof. Consider l1 , l2 ∈ F(Σ) and σ1 , σ2 , σ10 , σ20 , σ, σ 0 ∈ Σ such that σ1 , σ10 ∈ l1 , σ2 , σ20 ∈ l2 ,
σ1 = σ2 ∗ σ and σ10 = σ20 ∗ σ 0 . We have:
δ(σ2 ∗ σ) = δ(σ1 ) = l1 = δ(σ10 ) = δ(σ20 ∗ σ 0 ).
Since δ(σ2 ) = δ(σ20 ), by Definition 2.5 this implies δ(σ) = δ(σ 0 ), so that \\ is well-defined.
For RAM, the \\ operation is defined as follows. For l1 , l2 ∈ F(RAM), take any σ1 , σ2 ∈
RAM such that δ(σ1 ) = l1 and δ(σ2 ) = l2 . Then l2 \\ l1 = {σ | dom(σ)]dom(σ1 ) = dom(σ2 )},
if dom(σ1 ) ⊆ dom(σ2 ); otherwise, l1 \\ l2 is undefined.
We say that a footprint l1 is smaller than l2 , written l1  l2 , when l2 \\ l1 is defined.
The ◦ and \\ operations on footprints satisfy an analogue of Proposition 2.2.
Proposition 2.7. For all l1 , l2 , l3 ∈ F(Σ), if l1 ◦ l2 and l1 \\ l3 are defined, then
(l1 ◦ l2 ) \\ l3 = (l1 \\ l3 ) ◦ l2 .
In the rest of the paper, we fix a separation algebra Σ with the ∗ operation cancellative on
footprints.

LINEARIZABILITY WITH OWNERSHIP TRANSFER

7

3. Linearizability with Ownership Transfer
In the following, we consider descriptions of computations of a library providing several
methods to a multithreaded client. We fix a set ThreadID of thread identifiers and a set
Method of method names. As we explained in Section 1, a good definition of linearizability
has to allow replacing a concrete library implementation with its abstract version while
keeping client behaviours reproducible. For this, it should require that the two libraries
have similar client-observable behaviours. Such behaviours are recorded using histories,
which we now define in our setting.
Definition 3.1. An interface action ψ is an expression of the form (t, call m(σ)) or
(t, ret m(σ)), where t ∈ ThreadID, m ∈ Method and σ ∈ Σ. We denote the sets of all call
and return actions by CallAct and RetAct, and the set of all interface actions by CallRetAct.
An interface action records a call to or a return from a library method m by thread t.
The component σ in (t, call m(σ)) specifies the part of the state transferred upon the call
from the client to the library; σ in (t, ret m(σ)) is transferred in the other direction. For
example, in the algebra RAM, the annotation σ = [42 : 0] implies the transfer of the cell at
the address 42 storing 0. In the algebra RAMπ , σ = [42 : (0, 1/2)] implies the transfer of a
read permission for this cell.
Definition 3.2. A history H is a finite sequence of interface actions such that for every
thread t, its projection H|t to actions by t is a sequence of alternating call and return actions
over matching methods that starts from a call action.
In the following, we use the standard notation for sequences: ε is the empty sequence,
τ (i) is the i-th element of a sequence τ , τ k is the prefix of τ of length k, and |τ | is the
length of τ .
Not all histories make intuitive sense with respect to the ownership transfer reading
of interface actions. For example, let Σ = RAM and consider the history in Figure 1(a).
The history is meant to describe all the interactions between the library and the client.
According to the history, the cell at the address 10 was first owned by the client, and then
transferred to the library by thread 1. However, before this state was transferred back to
the client, it was again transferred from the client to the library, this time by thread 2. This
is not consistent with the intuition of ownership transfer, as executing the second action
requires the cell to be owned both by the library and by the client, which is impossible in
RAM.
As we show in this paper, histories that do not respect the notion of ownership, such as
the one above, cannot be generated by any program, and should not be taken into account
when defining linearizability. We now use the notion of footprints of states from Section 2 to
characterise formally the set of histories that respect ownership. A finite history H induces
a partial function JHK] : F(Σ) * F(Σ), which tracks how a computation with the history
H changes the footprint of the library state:
JεK] l
JHψK] l
JHψK] l
JHψK] l

=
=
=
=

l;
JHK] l ◦ δ(σ), if ψ = ( , call (σ)) ∧ (JHK] l ◦ δ(σ))↓;
JHK] l \\ δ(σ), if ψ = ( , ret (σ)) ∧ (JHK] l \\ δ(σ))↓;
undefined,
otherwise.

Using this function, we characterise histories respecting the notion of ownership as follows.

8

A. GOTSMAN AND H. YANG

Definition 3.3. A history H is balanced from l ∈ F(Σ) if JHK] (l) is defined. We call
subsets of BHistory = {(l, H) | H is balanced from l} interface sets.
An interface set can be used to describe all the behaviours of a library relevant to its
clients. In the following, H ranges over interface sets.
To keep client behaviours reproducible when replacing a concrete library by an abstract
one, we do not need to require the latter to reproduce the histories of the former exactly:
the histories generated by the two libraries can be different in ways that are irrelevant for
their clients. We now introduce a linearizability relation that matches a history of a concrete
library with that of the abstract one that yields the same client-observable behaviour.
Definition 3.4. The linearization relation v on histories is defined as follows: H v H 0
holds if there exists a bijection ρ : {1, . . . , |H|} → {1, . . . , |H 0 |} such that
∀i, j. (H(i) = H 0 (ρ(i))) ∧ ((i < j ∧ ((∃t. H(i) = (t, ) ∧ H(j) = (t, )) ∨
(H(i) = ( , ret ) ∧ H(j) = ( , call )))) =⇒ ρ(i) < ρ(j)).
We lift v to BHistory as follows: (l, H) v (l0 , H 0 ) holds if l0  l and H v H 0 .
Finally, we lift v to interface sets as follows: H1 v H2 holds if
∀(l1 , H1 ) ∈ H1 . ∃(l2 , H2 ) ∈ H2 . (l1 , H1 ) v (l2 , H2 ).
Thus, a history H is linearized by a history H 0 when the latter is a permutation of
the former preserving the order of actions within threads and non-overlapping method
invocations. The duration of a method invocation is defined by the interval from the
method call action to the corresponding return action (or to the end of the history if there
is none). An interface set H1 is linearized by an interface set H2 , if every history in H1 may
be reproduced in a linearized form by H2 without requiring more memory. We now discuss
the definition in more detail.
Definition 3.4 treats parts of memory whose ownership is passed between the library and
the client in the same way as parameters and return values in the classical definition [18]:
they are required to be the same in the two histories. In fact, the setting of the classical
definition can be modelled in ours if we pass parameters and return values via the heap. Let
Σ = RAM and let us fix distinct locations argt ∈ Loc for t ∈ ThreadID meant for the transfer
of parameters and return values. Then histories of the classical definition are represented
in our setting by histories where all actions are of the form
(t, call m([argt : param])) or (t, ret m([argt : retval ])), where param, retval ∈ Val.
The novelty of our definition lies in restricting the histories considered to balanced ones,
which are the only ones that can be produced by programs (we formalise this fact in Section 5). The notion of balancedness also plays a key role in proving the Abstraction Theorem
in the presence of ownership transfer (Section 6.1).
The fact that the linearizability relation allows us to permute actions by different
threads lets us arrange method invocations into a linear sequence. For example the history in Figure 1(b) is linearized by that in Figure 1(c). The former might correspond to a
concurrent stack implementation, where threads 1 and 2 pass parameters and return values
via locations 1 and 2, respectively. Histories such as the one in Figure 1(c), where a call to
every method is immediately followed by the corresponding return, are called sequential.
Sequential histories correspond to abstract libraries with every method implemented atomically. When the histories in Figures 1(b) and 1(c) are members of interface sets defining the
behaviour of concurrent and atomic stack implementations, the linearizability relationship

LINEARIZABILITY WITH OWNERSHIP TRANSFER

9

(a):
(1, call m1 ([10 : 0]))
(1, ret m1 ([ ]))

(2, call m2 ([10 : 0]))
(2, ret m2 ([ ]))

(b):
(1, call push([1 : a]))

(1, call pop([1 : 0]))

(1, ret push([1 : OK]))

(1, ret pop([1 : EMPTY]))
(2, call push([2 : b]))

(2, call pop([2 : 0]))
(2, ret pop([2 : a]))

(2, ret push([2 : OK]))

(c):
(1, call push([1 : a]))
(1, ret push([1 : OK]))

(2, call pop([2 : 0]))

(1, call pop([1 : 0]))

(2, ret pop([2 : a]))

(2, call push([2 : b]))

(1, ret pop([1 : EMPTY])) (2, ret push([2 : OK]))

(d):
(1, call pop([1 : 0]))

(1, call push([1 : a]))
(1, ret push([1 : OK]))
(2, call pop([2 : 0]))

(1, ret pop([1 : EMPTY]))
(2, call push([2 : b]))

...

(2, ret pop([2 : a]))

(e):
(1, call push([1 : a]))

(1, call pop([1 : 0]))

(1, ret push([1 : OK]))

(1, ret pop([1 : EMPTY]))
(2, call pop([2 : 0]))

(2, call push([2 : b]))

(2, ret pop([2 : a]))

Figure 1: Example histories

...

10

A. GOTSMAN AND H. YANG

between them allows us to justify that the call to pop by thread 1 in Figure 1(b) can return
EMPTY, since this behaviour can be witnessed by the valid history of the atomic implementation in Figure 1(c). (In fact, the pop would also be allowed to return b, since the resulting
history would be linearized by a sequential history with the push of b preceding the pop.)
The requirement that the order of non-overlapping method invocations be preserved is
inherited from the classical notion of linearizability [18]. As shown by Filipović et al. [12],
this requirement is essential to validate an Abstraction Theorem for clients that can communicate via shared client-side variables. For example, since in Figure 1(b) the push of a
returns before the push of b is called, the order between these method invocations has to
stay the same in any linearizing history, such as the one in Figure 1(c).
Following Filipović et al. [12], we do not require the abstract history H 0 to be sequential, like in the classical definition of linearizablity. This allows our definition to compare
behaviours of two concurrent library implementations. We also allow a concrete history
to contain calls without matching returns, arising, e.g., because the corresponding method
invocation did not terminate. In this case, we require the same behaviour to be reproduced
in the abstract history [14], which is possible because the latter does not have to be sequential. For example, the history in Figure 1(d) is linearized by that in Figure 1(e). This yields
a simpler treatment of non-terminating calls than the use of completions in the classical
definition of linearizability [18].
Definition 3.4 requires that the initial footprint of an abstract history H 0 be smaller
than that of the concrete history H. This requirement is standard in data refinement [13]:
it ensures that, when we replace a concrete library by an abstract one in a program, the
library-owned memory stays disjoint from the client-owned one. It does not pose problems in
practice, as the abstract library generating H 0 usually represents some of the data structures
of the concrete library abstractly and, hence, more concisely.
So far we have defined the notion of linearizability on interface sets without taking
into account library implementations that generate them. In the rest of the paper, we
develop this notion for libraries written in a particular programming language and prove an
Abstraction Theorem, which guarantees that a library can be replaced by another library
linearizing it when we reason about its client program.
4. Programming Language
We consider a simple concurrent programming language:
C ::= c | m | C; C | C + C | C ∗
L ::= {m = C; . . . ; m = C}
S ::= let L in C k . . . k C
A program consists of a single library L implementing methods m ∈ Method and its client
C1 k . . . k Cn , given by a parallel composition of threads. The language is parameterised by
a set of primitive commands c ∈ PComm, meant to execute atomically. Commands also
include method calls m ∈ Method, sequential composition C; C 0 , nondeterministic choice
C + C 0 and finite iteration C ∗ . We use + and ∗ instead of conditionals and while loops
for theoretical simplicity: as we show below, the latter can be defined in the language as
syntactic sugar. Methods do not take arguments and do not return values, as these can
be passed via special locations on the heap associated with the identifier of the thread
calling the method (Section 3). We disallow nested method calls. We also assume that

LINEARIZABILITY WITH OWNERSHIP TRANSFER

11

every method called in the program is defined by the library, and thus call S a complete
program. An open program is a library L without a client, or a client C without a library
implementation:
C ::= let [−] in C k . . . k C
P ::= S | C | L
In C, we allow the client to call methods that are not defined in the program (but belong
to the missing library). An open program represents a library or a client considered in
isolation. The novelty of the kind of open programs we consider here is that we allow them
to communicate with their environment via ownership transfers. We now define a way to
specify a contract this communication follows.
4.1. Method Specifications. A predicate is a set of states from Σ, and a parameterised
predicate is a mapping from thread identifiers to predicates. We use the same symbols
p, q, r for ordinary and parameterised predicates; it should always be clear from the context
which one we mean. When p is a parameterised predicate, we write pt for the predicate
obtained by applying p to a thread t. Both kinds of predicates can be described syntactically,
e.g., using separation logic assertions [26].
We define possible ownership transfers between components with the aid of method
specifications Γ, which are sets of Hoare triples {p} m {q}, at most one for each method.
Here p and q are parameterised predicates such that pt describes pieces of state transferred
when thread t calls the method m, and qt , those transferred at its return. Note that the
intention of the pre- and postconditions in method specifications is only to identify the
areas of memory transferred; in other words, they describe the “type” of the returned data
structure, but not its “value”. As usual for concurrent algorithms, a complete specification
of a library is given by its abstract implementation (Section 6).
For example, as we discussed in Section 1, when programmers store pointers in a concurrent container, they often intend to transfer the ownership of the data structures these
pointers identify at calls to and returns from the container’s methods. In Figure 2(a) we
give an example of such a container—a bounded stack represented by an array. For readability, we write examples in C instead of the minimalistic language introduced above. The
library protects the array by a lock; more complicated algorithms allow a higher degree of
concurrency [17]. Take Σ = RAM and for x ∈ Loc let Obj(x) ⊆ RAM denote the set of
states representing all well-formed data structures of a certain type allocated at the address
x. For example, for objects with a single integer field we have Obj(x) = {[x : y] | y ∈ Val}.
Then the specification of the stack when it stores pointers to such data structures can be
given as follows:
{∃x. argt →
7 x ∗ Obj(x)} push {argt 7→ OK ∨ (argt 7→ FULL ∗ Obj(x))};
{argt 7→ } pop {∃x. argt 7→ x ∗ ((x = EMPTY ∧ emp) ∨ (x 6= EMPTY ∧ Obj(x)))}.

(4.1)

Here we use the separation logic syntax to describe predicates parameterised by the thread
identifier t. Thus, emp denotes the empty heap [ ], x 7→ y the heap [x : y], and ∗ the
combination of heaps with disjoint domains. In the following we also use the assertion
x..y 7→ for x ≤ y, denoting all the heaps with the domain {x, x + 1, . . . , y}. We use
distinguished locations argt , t ∈ ThreadID to pass parameters and return values. According
to the specification, the stack gets the ownership of an object when a pointer to it is pushed,
and gives it up when the pointer is popped.

12

A. GOTSMAN AND H. YANG

void *stack[SIZE];
int count = 0; // count of
// elements stored
Lock array_lock; // protects
// the array and the count
int push(void *arg) {
lock(array_lock);
if (count == SIZE) {
unlock(array_lock);
return FULL;
}
stack[count++] = arg;
unlock(array_lock);
return OK;
}
void *pop() {
lock(array_lock);
if (count == 0) {
unlock(array_lock);
return EMPTY;
}
void *obj = stack[--count];
unlock(array_lock);
return obj;
}
(a)

struct Node { Node *prev, *next; };
Node *free_list; // a cyclic doubly// linked list with a sentinel node
Lock *list_lock; // protects the list
void free(void *arg) {
Node *block = (Node*)arg;
lock(list_lock);
block->prev = free_list;
block->next = free_list->next;
free_list->next->prev = block;
free_list->next = block;
unlock(list_lock);
}
void *alloc() {
lock(list_lock);
if (free_list->next == free_list) {
unlock(list_lock);
return NULL;
}
Node *block = free_list->next;
free_list->next = block->next;
block->next->prev = free_list;
unlock(list_lock);
return block;
}
(b)

Figure 2: Example concurrent library implementations: (a) a bounded stack storing pointers to objects; (b) a memory allocator managing memory blocks of a fixed size
Now take size ∈ N and let

Obj(x) = σ | dom(σ) = {x, . . . , x + size − 1} .
We specify an allocator managing blocks of size memory cells as follows:
{∃x. argt →
7 x ∗ (x..(x + size − 1) 7→ )} free {argt 7→ };
{argt 7→ } alloc {∃x. argt 7→ x ∗ ((x = 0 ∧ emp) ∨ (x 6= 0 ∧ (x..(x + size − 1) 7→ )))}.
(4.2)
The specification corresponds to the ownership transfer reading of allocator calls explained
in Section 1. In Figure 2(b) we give an example allocator corresponding to the specification
(we have omitted initialisation code from the figure). Note that, unlike the stack, the
allocator does access the blocks of memory transferred to it by the client, since it stores
free-list pointers inside them.
To define the semantics of ownership transfers unambiguously (Section 5), we require
pre- and postconditions in method specifications to be precise [23].

LINEARIZABILITY WITH OWNERSHIP TRANSFER

13

Definition 4.1. A predicate r ∈ 2Σ is precise if for every state σ there exists at most one
substate σ1 satisfying r, i.e., such that σ1 ∈ r and σ = σ1 ∗ σ2 for some σ2 .
Since the ∗ operation is cancellative, when such a substate σ1 exists, the corresponding
substate σ2 is unique and is denoted by σ \ r. A parameterised predicate r is precise if so
is rt for every t.
Informally, a precise predicate carves out a unique piece of the heap. For example,
assuming the algebra RAM, the predicate {[42 : 0]} and those used in the allocator specification are precise. However, the predicate {[42 : 0], [ ]} is not: when σ = [42 : 0] we can
take either σ1 = [42 : 0] and σ2 = [ ], or σ1 = [ ] and σ2 = [42 : 0].
A specified open program is of the form Γ ` C or L : Γ. In the former, the specification
Γ describes all the methods that C may call. In the latter, Γ provides specifications for the
methods in the open program that can be called by its external environment. In both cases,
Γ specifies the type of another open program that can fill in the hole in C or L. When we
are not sure which form a program has, we write Γ ` P : Γ0 . In this case, if P does not
have a client, then Γ is empty; if P does not have a library, then Γ0 is empty; and if P is
complete, then both Γ and Γ0 are empty. For specified open programs
Γ ` C = Γ ` let [−] in C1 k . . . k Cn
and
L:Γ
agreeing on the specification Γ of library methods, we denote by C(L) the complete program
let L in C1 k . . . k Cn .
4.2. Primitive Commands. We now discuss primitive commands in more detail. Consider the set 2Σ ∪ {>} of subsets of Σ with a special element > used to denote an error
state, resulting, e.g., from dereferencing an invalid pointer. We extend the ∗ operation on
2Σ to 2Σ ∪ {>} by letting > ∗ p = p ∗ > = > ∗ > = > for all p ∈ 2Σ .
We assume an interpretation of every primitive command c ∈ PComm as a transformer
t
fc : Σ → (2Σ ∪ {>}), which maps pre-states to states obtained when thread t ∈ ThreadID
executes c from a pre-state. The fact that our transformers are parameterised by t allows
atomic accesses to areas of memory indexed by thread identifiers. This idealisation simplifies
the setting in that it lets us do without special thread-local or method-local storage for
passing method parameters and return values.
Some typical primitive commands are:
skip,

[E] = E 0 ,

assume(E),

where expressions E are defined as follows:
E ::= Z | tid | [E] | E + E | −E | !E | . . .
Here tid refers to the identifier of the thread executing the command, [E] returns the contents
of the address E in memory, and !E is the C-style negation of an expression E—it returns 1
when E evaluates to 0, and 0 otherwise. The assume(E) command filters out all the input
states where E evaluates to 0. Hence, after assume(E) is executed, E always has a non-zero

14

A. GOTSMAN AND H. YANG

;t
;t
;t
;t
;t

σ, skip
σ, [E] = E 0
σ, [E] = E 0
σ, assume(E)
σ, assume(E)

σ
σ[JEKσ,t : JE 0 Kσ,t ],
>,
σ,
>,

if
if
if
if

JEKσ,t
JEKσ,t
JEKσ,t
JEKσ,t

∈ dom(σ), JE 0 Kσ,t ∈ Val
6∈ dom(σ) or JE 0 Kσ,t = >
∈ Val − {0}
=>

Figure 3: Transition relation for sample primitive commands in the RAM model. The result
> indicates that the command faults.
σ, skip
σ, [E] = E 0
σ, [E] = E 0
σ, assume(E)
σ, assume(E)

;t
;t
;t
;t
;t

σ
σ[JEKσ,t : (JE 0 Kσ,t , 1)],
>,
σ,
>,

if
if
if
if

σ(JEKσ,t ) = ( , 1), JE 0 Kσ,t ∈ Val
the above condition does not hold
JEKσ,t ∈ Val − {0}
JEKσ,t = >

Figure 4: Transition relation for sample primitive commands in the RAMπ model. The
evaluation of expressions JEKσ,t ignores permissions in σ.
value. Using it, the standard commands for conditionals and loops can be defined in our
language as follows:
(if E then C1 else C2 ) = (assume(E); C1 ) + (assume(!E); C2 ),

(4.3)

∗

(while E do C) = (assume(E); C) ; assume(!E).
For the above commands c and t ∈ ThreadID, we define fct : RAM → 2RAM ∪ {>} using the
transition relation ;t : RAM × (RAM ∪ {>}) in Figure 3:
[
fct (σ) = if (σ, c ;t >) then > else
σ 0 | σ, c ;t σ 0 .
In the figure, JEKσ,t ∈ Val∪{>} denotes the result of evaluating the expression E in the state
σ with the current thread identifier t. When this evaluation dereferences illegal memory
addresses, it results in the error value >. We define fct : RAMπ → 2RAMπ ∪ {>} similarly,
but using the transition relation ;t : RAMπ × (RAMπ ∪ {>}) in Figure 4. The transformers
formalise the semantics of permissions explained in Section 2: permissions less than 1 allow
reading, and the full permission 1 additionally allows writing. Note that assume yields
an empty set of post-states when its condition evaluates to zero, leading to the program
getting stuck. Thus, even though, when executing the if statement (4.3), both branches of
the non-deterministic choice will be explored, only the branch where the assume condition
evaluates to true will proceed further.
For our results to hold, we need to place some restrictions on the transformers fct for
every primitive command c ∈ PComm and thread t ∈ ThreadID:
Footprint Preservation: ∀σ, σ 0 ∈ Σ. σ 0 ∈ fct (σ) =⇒ δ(σ 0 ) = δ(σ).
Strong Locality: ∀σ1 , σ2 ∈ Σ. (σ1 ∗ σ2 )↓ ∧ fct (σ1 ) 6= > =⇒ fct (σ1 ∗ σ2 ) = fct (σ1 ) ∗ {σ2 }.
Footprint Preservation prohibits primitive commands from allocating or deallocating memory. This does not pose a problem, since in the context of linearizability, an allocator is
just another library and should be treated as such. The Strong Locality of fct says that, if a

LINEARIZABILITY WITH OWNERSHIP TRANSFER

15

command c can be safely executed from a state σ1 , then when executed from a bigger state
σ1 ∗ σ2 , it does not change the additional state σ2 and its effect depends only on the state
σ1 and not on the additional state σ2 .
The Strong Locality is a strengthening of the locality property in separation logic [7]:
∀σ1 , σ2 ∈ Σ. (σ1 ∗ σ2 )↓ ∧ fct (σ1 ) 6= > =⇒ fct (σ1 ∗ σ2 ) ⊆ fct (σ1 ) ∗ {σ2 }.
Locality rules out commands that can check if a cell is allocated in the heap other than
by trying to access it and faulting if it is not allocated. For example, let Σ = RAM and
consider the following transformer f t : RAM → 2RAM ∪ {>}:
f t (σ) = if σ(1)↓ then {σ[1 : 0]} else {σ}.
The transformer f t defines the denotation of a ‘command’ that writes 0 to the cell at the
address 1 if it is allocated and acts as a no-op if it is not. This violates locality. Indeed,
take σ1 = [ ] and σ2 = [1 : 1]. Then
f t (σ1 ∗ σ2 ) = f t ([1 : 1]) = {[1 : 0]}
and

f t (σ1 ) ∗ {σ2 } = f t ([ ]) ∗ {[1 : 1]} = {[ ]} ∗ {[1 : 1]} = {[1 : 1]}.
Hence, f t (σ1 ∗ σ2 ) ⊆ f t (σ1 ) ∗ {σ2 } does not hold.
While locality prohibits the command from changing the additional state, it permits
the effect of the command to depend on this state [13]. The Strong Locality forbids such
dependencies. To see this, consider another ‘command’ defined by the following transformer
f t : RAM → 2RAM ∪ {>}:
f t (σ) = if σ(1)↑ then >
else if (σ(2)↓) then {σ[1 : 0]}
else {σ[1 : 0], σ[1 : 1]}.
The command does not access the cell at the address 2, since it does not fault if the cell
is not allocated. However, when the cell is allocated, the effect of the command depends
on its value. It is easy to check that f t is local. However, it is not strongly local, since for
σ1 = [1 : 0] and σ2 = [2 : 0], we have
f t (σ1 ∗ σ2 ) = f t ([1 : 0, 2 : 0]) = {[1 : 0, 2 : 0]}
and
f t (σ1 ) ∗ {σ2 } = f t ([1 : 0]) ∗ {[2 : 0]} = {[1 : 0], [1 : 1]} ∗ {[2 : 0]} = {[1 : 0, 2 : 0], [1 : 1, 2 : 0]},
so that f t (σ1 ∗ σ2 ) = f t (σ1 ) ∗ {σ2 } does not hold. The property of Strong Locality subsumes
the one of contents independence used in situations similar to ours in previous work on data
refinement in a sequential setting [13].
The transformers for standard commands, except memory (de)allocation, satisfy the
conditions of Footprint Preservation and Strong Locality.

16

A. GOTSMAN AND H. YANG

5. Client-Local and Library-Local Semantics
We now give the semantics to complete and open programs. In the latter case, we define
component-local semantics that include all behaviours of an open program under any environment satisfying the specification associated with it. In Section 6, we use these to lift
linearizability to libraries and formulate the Abstraction Theorem.
Programs in our semantics denote sets of traces, recording every step in a computation.
These include both internal actions by program components and calls and returns. We define
program semantics in two stages. First, given a program, we generate the set of the possible
execution traces of the program. This is done solely based on the structure of its statements,
without taking into account restrictions arising from the semantics of primitive commands
or ownership transfers. The next step filters out traces that are not consistent with the
above restrictions using a trace evaluation process and, for open programs, annotates calls
and returns appropriately.
5.1. Traces. Traces consist of actions, which include primitive commands performed internally by a component and calls or returns, possibly annotated with states. Thus actions,
include all interface actions ψ from Definition 3.1.
Definition 5.1. The set of actions is defined as follows:
ϕ ∈ Act ::= ψ | (t, c) | (t, call m) | (t, ret m),
where t ∈ ThreadID, m ∈ Method and c ∈ PComm.
Definition 5.2. A trace τ is a finite sequence of actions such that for every thread t, the
projection of τ to t’s call and return actions is a sequence of alternating call and return
actions over matching methods that starts from a call action.
We classify actions in a trace as those performed by the client and the library based on
whether they happen inside a method.
Definition 5.3. For a trace τ and an index i ∈ {1, . . . , |τ |}, an action τ (i) is a client
action if τ (i) = (t, c) for some thread t and a primitive command c and
∀j. j < i ∧ τ (j) = (t, call ) =⇒ ∃k. j < k < i ∧ τ (k) = (t, ret ).
An action τ (i) is a library action if τ (i) = (t, c) for some t and c but τ (i) is not a client
action, that is,
∃j. j < i ∧ τ (j) = (t, call ) ∧ ¬∃k. j < k < i ∧ τ (k) = (t, ret ).
A trace is a client trace, if all of its actions of the form (t, c) are client actions; it is a
library trace, if they all of them are library actions.
In the following, κ denotes client traces, λ, ζ, α, β library traces, and τ arbitrary ones.
We write client(τ ) for the projection of τ to client, call and return actions, lib(τ ) for that
to library, call and return actions, and history(τ ) for that to call and return actions.

LINEARIZABILITY WITH OWNERSHIP TRANSFER

LcMt η
LC1 + C2 Mt η
LC ∗ Mt η
LmMt η
LC1 ; C2 Mt η
LC1 k . . . k Cn Mη

17

= {(t, c)}
= LC1 Mt η ∪ LC2 Mt η
∗
= LC Mt η
= {(t, call m) τ (t, ret m) | τ ∈ η(m, t)}
= {τ1 τ2 | τ1 ∈ LC1 Mt η ∧ τ2 ∈ LC2 Mt η}
S
= {τ1 k . . . k τn | ∀t ∈ {1, . . . , n}. τt ∈ LCt Mt η}

Llet {m = Cm | m ∈ M } in C1 k . . . k Cn M = prefix(LC1 k . . . k Cn M(λ(m, t). LCm Mt ( )))
LΓ : let [−] in C1 k . . . k Cn M = prefix(LC1 k . . . k Cn M(λ(m, t). {ε}))
L{m = Cm | m ∈ {m1 , . . . , mj }} : ΓM =
S
prefix( k≥1 LCmgc k . . . (k times) . . . k Cmgc M(λ(m, t). LCm Mt ( )))
(where Cmgc = (m1 + . . . + mj )∗ )
Figure 5: Trace sets of commands and programs. Here prefix(T ) is the prefix closure of
T and τ ∈ τ1 k . . . k τn if and only if every action in τ is done by a thread
t ∈ {1, . . . , n} and for all such t, we have τ |t = τt . We use λ for functions, in
contrast to λ for library traces.
5.2. Trace Sets. Consider a program Γ ` P : Γ0 and let M ⊆ Method be the set of methods
implemented by its library or called by its client. We define the trace set LΓ ` P : Γ0 M ∈
2Trace of P in Figure 5. We first define the trace set LC Mt η of a command C, parameterised
by the identifier t of the thread executing it and a mapping η ∈ M × ThreadID → 2Trace
giving the trace set of the body of every method that C can call when executed by a given
thread. The trace set of a client LC1 k . . . k Cn Mη is obtained by interleaving traces of its
threads.
The trace set LC(L)M of a complete program is that of its client computed with respect
to a mapping λ(m, t). LCm Mt ( ) associating every method m with the trace set of its body
Cm . Since we prohibit nested method calls, LCm Mt η does not depend on η. We prefix-close
the resulting trace set to take into account incomplete executions. In particular, this allows
the thread scheduler to be unfair: a thread can be preempted and never scheduled again.
A program Γ ` C generates client traces LΓ ` C M, which do not include internal library
actions. This is achieved by associating an empty trace with every library method. Finally,
a program L : Γ0 generates all possible library traces LL : Γ0 M. This is achieved by running
the library under its most general client, where every thread executes an infinite loop,
repeatedly invoking arbitrary library methods.
5.3. Evaluation. The set of traces generated using L·M may include those not consistent
with the semantics of primitive commands or expected ownership transfers. We therefore
define the meaning of a program JΓ ` P : Γ0 K ∈ Σ → (2Trace ∪ {>}) by evaluating every
trace in LΓ ` P : Γ0 M from a given initial state to determine whether it is feasible. For open
programs, this process also annotates calls and returns in a trace with states transferred.
The formal definition of JΓ ` P : Γ0 K is given in Figure 6 with the aid of a trace
evaluation function JΓ ` τ : Γ0 K : Σ → 2Σ×Trace ∪ {>}. Given an initial state, this either
yields multiple final states and annotated traces, or fails and produces >. If the resulting set

18

A. GOTSMAN AND H. YANG

JΓ ` P : Γ0 K : Σ → (2Trace ∪ {>}):

JΓ ` P : Γ0 Kσ = if ∃τ ∈ LΓ ` P : Γ0 M. JΓ ` τ : Γ0 Kσ = > then >
else {τ 0 | ∃τ ∈ LΓ ` P : Γ0 M. ( , τ 0 ) ∈ JΓ ` τ : Γ0 Kσ}

JΓ ` τ : Γ0 K : Σ → (2Σ×Trace ∪ {>}):

JΓ ` ε : Γ0 Kσ = {(σ, ε)}
JΓ ` τ ϕ : Γ0 Kσ = if (JΓ ` τ : Γ0 Kσ = >) then >
else if (∃(σ 0 , ) ∈ JΓ ` τ : Γ0 Kσ. JΓ ` ϕ : Γ0 Kσ 0 = >) then >
else {(σ 00 , τ 0 ϕ0 ) | ∃σ 0 . (σ 0 , τ 0 ) ∈ JΓ ` τ : Γ0 Kσ ∧ (σ 00 , ϕ0 ) ∈ JΓ ` ϕ : Γ0 Kσ 0 }

JΓ ` ϕ : Γ0 K : Σ → (2Σ×Act ∪ {>}):
JΓ ` (t, c) : Γ0 Kσ
J(t, call m)Kσ
J(t, ret m)Kσ
J(t, call m) : ({p} m {q}), Γ0 Kσ
J(t, ret m) : ({p} m {q}), Γ0 Kσ
J({p} m {q}), Γ ` (t, call m)Kσ
J({p} m {q}), Γ ` (t, ret m)Kσ

=
=
=
=
=
=
=

if (fct (σ) = >) then > else {(σ 0 , (t, c)) | σ 0 ∈ fct (σ)}
{(σ, (t, call m))}
{(σ, (t, ret m))}
{(σ ∗ σp , (t, call m(σp ))) | σp ∈ pt ∧ (σ ∗ σp )↓ }
if (σ \ qt )↑ then > else {(σ \ qt , (t, ret m(σ \ (σ \ qt ))))}
if (σ \ pt )↑ then > else {(σ \ pt , (t, call m(σ \ (σ \ pt ))))}
{(σ ∗ σq , (t, ret m(σq ))) | σq ∈ qt ∧ (σ ∗ σq )↓ }

Figure 6: Semantics of programs
of state-trace pairs is empty, then the trace is infeasible and is discarded. If the evaluation
produces > on any trace from LΓ ` P : Γ0 M, then the program has no semantics for the
given initial state and its denotation is defined to be >. The evaluation of τ is defined
inductively on its length using a function JΓ ` ϕ : Γ0 K : Σ → 2Σ×Act ∪ {>} that evaluates a
single action ϕ. We explain this function by considering separately the cases of a complete
program, open program with a library and open program with a client.
The evaluation JϕK for an action in a complete program has the standard semantics,
with the effects of primitive commands computed using their transformers from Section 4.
In this case, calls and returns are left unannotated, since no ownership transfers to or from
the external environment are performed.
The function Jϕ : Γ0 K gives a library-local semantics to the program L : Γ0 , in the
sense that it generates library traces under any client respecting Γ0 . When a method m
from Γ0 is called by thread t, the library receives the ownership of any state consistent with
the method precondition pt . This state has to be compatible with that of the library. After
the method returns, the library has to give up the piece of state satisfying its postcondition.
Since qt is precise, this piece of state is determined uniquely. The evaluation faults if the
state to be transferred is not available; thus, a library has no semantics if it violates the
contract with its client given by Γ0 . This also ensures that the histories produced by a
library are balanced.
Proposition 5.4. If λ ∈ JL : Γ0 Kσ, then history(λ) is balanced from δ(σ).

The function JΓ ` ϕK gives a client-local semantics to Γ ` C, in the sense that it
generates traces of this client assuming any behaviour of the library consistent with Γ.
When a thread t calls a method m in Γ, it transfers the ownership of a piece of state

LINEARIZABILITY WITH OWNERSHIP TRANSFER

19

satisfying the method precondition pt to the library being called. As before, this piece
is defined uniquely, because preconditions are precise. When such a piece of state is not
available, the evaluation faults. This ensures that client respects the method specifications
of the libraries it uses. When the method returns, the client receives the ownership of an
arbitrary piece of state satisfying its postcondition qt , compatible with the current state of
the client.
5.4. Connection between Local and Global Semantics. We now formulate a lemma,
used in the proof of the Abstraction Theorem (Section 6), that states the connection between the library-local and client-local semantics on one side and the semantics of complete
programs on the other. We start by introducing some auxiliary definitions.
Definition 5.5. A program Γ ` P : Γ0 is safe at σ, if JΓ ` P : Γ0 Kσ 6= >; P is safe for
I ⊆ Σ, if it is safe at σ for all σ ∈ I.
For a set of initial states I ⊆ Σ, let
J(Γ ` P : Γ0 ), IK = {(σ, τ ) | σ ∈ I ∧ τ ∈ JΓ ` P : Γ0 Kσ}.

We define an operator ⊗ : 2Σ×Trace × 2Σ×Trace → 2Σ×Trace combining the resulting sets X
and Y of state-trace pairs produced by the client-local and library-local semantics into a
set corresponding to the complete program:
X ⊗ Y = {(σ ∗ σ 0 , τ ) | ∃κ, λ. (σ, κ) ∈ X ∧ (σ 0 , λ) ∈ Y ∧ (σ ∗ σ 0 )↓ ∧ cover(τ, κ, λ)},
where
cover(τ, κ, λ) ⇐⇒ history(κ) = history(λ) ∧ client(τ ) = ground(κ) ∧ lib(τ ) = ground(λ)
and ground is a function on traces that erases the state annotations from their interface
actions.
Lemma 5.6. Assume Γ ` C and L : Γ safe for I0 and I1 , respectively. Then C(L) is safe
for I0 ∗ I1 and
JC(L), I0 ∗ I1 K = JΓ ` C, I0 K ⊗ JL : Γ, I1 K.

The lemma shows that the set of traces produced by C(L) can be obtained by combining
pairs of traces with the same history produced by C and L. Note that, since the semantics
of C(L) does not annotate calls and returns with the states transferred, in cover we have
to erase these annotations from the local traces κ or λ before comparing the traces with τ .
Unpacking the definition of ⊗ and using the fact that
∀κ, λ. history(κ) = history(λ) =⇒ ∃τ. cover(τ, κ, λ),
from Lemma 5.6 we get the following two corollaries.
Corollary 5.7 (Decomposition). Assume Γ ` C and L : Γ safe for I0 and I1 , respectively.
Then C(L) is safe for I0 ∗ I1 and
∀(σ, τ ) ∈ JC(L), I0 ∗ I1 K. ∃(σ0 , κ) ∈ JΓ ` C, I0 K. ∃(σ1 , λ) ∈ JL : Γ, I1 K.

σ = σ0 ∗ σ1 ∧ cover(τ, κ, λ).

20

A. GOTSMAN AND H. YANG

Corollary 5.8 (Composition). If Γ ` C and L : Γ are safe for I0 and I1 , respectively, then
∀(σ1 , κ) ∈ JΓ : C, I0 K. ∀(σ2 , λ) ∈ JL : Γ, I1 K. ((σ0 ∗ σ1 )↓ ∧ history(κ) = history(λ)) =⇒

∃τ. (σ0 ∗ σ1 , τ ) ∈ JC(L), I0 ∗ I1 K ∧ cover(τ, κ, λ).

Corollary 5.7 can be viewed as carrying over properties of the local semantics, such as
safety, to the global one, and in this sense is the statement of the soundness of the former
with respect to the latter. The corollary also confirms that the client defined by LL : Γ0 M
and Jλ : Γ0 K is indeed most general, as it reproduces library behaviours under any possible
clients. Corollary 5.8 carries over properties of the global semantics to the local ones, stating
the adequacy of the latter.
Lemma 5.6 is proved in Appendix A. Most of the proof deals with maintaining a splitting of the state of C(L) into the parts owned by L and C, which changes during ownership
transfers. The proof relies crucially on the safety of the client and the libraries and the
Strong Locality property of primitive commands. In more detail, safety is defined by considering executions of a component in the library-local or the client-local semantics. These
execute the component code only on the memory it owns, whose amount only changes with
ownership transfers to and from its environment according to method specifications. Because of the Strong Locality property, commands fault when accessing memory cells that
are not present in the state they are run from, and their execution does not depend on any
additional memory that might be present in the state. Hence, when we use a component
inside a complete program, its safety guarantees that the component code does not touch
the part of the heap belonging to other components in the program, and its execution is not
affected by the state of such components. This guarantees that the behaviour a component
produces as part of the complete program can be reproduced when we execute it in isolation
and vice versa, allowing us to establish Lemma 5.6. In practice, the safety of a program
can be established using existing program logics, such as separation logic [23, 28].
6. Abstraction Theorem
We are now in a position to define the notion of linearizability on libraries and prove the
central technical result of this paper—the Abstraction Theorem. We define linearizability
between specified libraries L : Γ, together with their sets of initial states I. First, using the
library-local semantics of Section 5, we define the interface set describing all the behaviours
of a library L when run from initial states in I:
interf(L : Γ, I) = {(δ(σ0 ), history(τ )) | (σ0 , τ ) ∈ J(L : Γ), IK} ⊆ BHistory.

Definition 6.1. Consider L1 : Γ and L2 : Γ safe for I1 and I2 , respectively. We say that
(L1 : Γ, I1 ) is linearized by (L2 : Γ, I2 ), written (L1 : Γ, I1 ) v (L2 : Γ, I2 ), if, according to
Definition 3.4,
interf(L1 : Γ, I1 ) v interf(L2 : Γ, I2 ).
For an interface set H2 we say that (L1 : Γ, I1 ) is linearized by H2 , written (L1 : Γ, I1 ) v
H2 , if
interf(L1 : Γ, I1 ) v H2 .
Thus, (L1 : Γ, I1 ) is linearized by (L2 : Γ, I2 ) if every history generated by the librarylocal semantics of the former may be reproduced in a linearized form by the library-local
semantics of the latter without requiring more memory. The relation (L1 : Γ, I1 ) v (L2 :

LINEARIZABILITY WITH OWNERSHIP TRANSFER

21

Sequence<void*> stack;

Set<void*> free_list;

int push(void *arg) {
atomic {
if (nondet()) { return FULL; }
else {
add_to_head(stack, arg);
return OK;
}
}
}

void free(void *arg) {
atomic {
add(free_list, arg);
}
}

void *pop() {
atomic {
if (!isEmpty(stack)) {
void *obj = head(stack);
stack = tail(stack);
return obj;
} else { return EMPTY; }
}
}

void *alloc() {
atomic {
if (!isEmpty(free_list)) {
Node *block =
(Node*)take(free_list);
block->next = nondet();
block->prev = nondet();
return block;
} else {
return 0;
}
}
}

(a)

(b)

Figure 7: Specifications corresponding to the implementations in Figure 2: (a) a bounded
stack storing pointers to objects; (b) a memory allocator managing memory blocks
of a fixed size. The Node structure is defined in Figure 2(b).
Γ, I2 ) allows us to specify a library by another piece of code, but possibly simpler than
the original one. For example, the stack and the allocator from Figure 2 with method
specifications (4.1) and (4.2) can be specified by the libraries in Figure 7. The libraries
replace the array and the linked list in the implementations by the abstract data types of
a sequence and a set (we assume a trivial extension of the RAM algebra from Section 2
to allow memory cells to store values of such types). Thus, the abstract libraries use less
memory than the concrete ones. Instead of using locking, all operations on the abstract
data types are done atomically; formally, we assume primitive commands corresponding to
the code in the atomic blocks.
The other relation (L1 : Γ, I1 ) v H2 introduced in Definition 6.1 allows us to specify
a library directly by an interface set, without fixing a piece of code generating it. The
interface set H2 can still be simpler than that of (L1 : Γ, I1 ), e.g., containing only sequential
histories. Even though the two forms of defining linearizability may seem very similar, as
we show in Section 6.1, their mathematical properties are fundamentally different.
We now formulate two variants of the Abstraction Theorem, corresponding to the two
ways of specifying libraries (we prove them in Section 6.1).
Theorem 6.2 (Abstraction—specification by code). If
• L1 : Γ, L2 : Γ, Γ ` C are safe for I1 , I2 , I, respectively, and

22

A. GOTSMAN AND H. YANG

• (L1 : Γ, I1 ) v (L2 : Γ, I2 ),
then
• C(L1 ) and C(L2 ) are safe for I ∗ I1 and I ∗ I2 , respectively, and
• ∀(σ1 , τ1 ) ∈ JC(L1 ), I ∗ I1 K. ∃(σ2 , τ2 ) ∈ JC(L2 ), I ∗ I2 K. client(τ1 ) = client(τ2 ).

Thus, when reasoning about a client C(L1 ) of a library L1 , we can soundly replace L1 by
a library L2 linearizing it: if a safety property over client traces holds of C(L2 ), it will also
hold of C(L1 ). In practice, we are usually interested in atomicity abstraction, a special
case of this transformation when methods in L2 are atomic. An instance is replacing one
of the libraries from Figure 2 by its specification from Figure 7. The requirement that C
be safe in the theorem restricts its applicability to well-behaved clients that do not access
memory owned by the library: you cannot replace a library by another one if the client can
access its internal data structures and thereby “look inside the box”. Similarly, the safety
of the libraries ensures that they cannot corrupt the data structures owned by the client.
The other version of the Abstraction Theorem, allowing library specification by an
interface set, guarantees that replacing a library by its specification leaves all the original
client behaviours reproducible modulo the following notion of trace equivalence.
Definition 6.3. Client traces κ and κ0 are equivalent, written κ ∼ κ0 , if κ|t = κ0 |t for all
t ∈ ThreadID and the projections of κ and κ0 to non-interface actions are identical.

Theorem 6.4 (Abstraction—specification by an interface set). If
• L1 : Γ and Γ ` C are safe for I1 and I, respectively, and
• (L1 , I1 ) v H2 ,
then
• C(L1 ) is safe for I ∗ I1 and
• ∀(σ, τ1 ) ∈ JC(L1 ), I ∗ I1 K. ∃κ, l. (σ 0 , κ) ∈ JΓ ` C, IK ∧ (l, history(κ)) ∈ H2 ∧ (δ(σ 0 ) ◦ l)↓ ∧
client(τ1 ) ∼ ground(κ).
The theorem shows that client behaviours of C(L1 ) can be reproduced by the client-local
semantics of C projected to histories in H2 with initial footprints compatible with initial
client states. Note that client(τ1 ) = client(τ2 ) in Theorem 6.2 implies that history(τ1 ) =
history(τ2 ), i.e., C(L2 ) can reproduce the history of C(L1 ) exactly. In contrast, Theorem 6.4
does not guarantee this, since κ ∼ κ0 does not imply history(κ) = history(κ0 ); we only know
that the projection to non-interface actions is reproduced. We discuss the reason for this
discrepancy below.
6.1. The Rearrangement Lemma and the Proof of the Abstraction Theorem. The
key component used for establishing Theorem 6.2 is the Rearrangement Lemma: if H v H 0 ,
then every execution trace of a library producing H 0 can be transformed into another trace
of the same library that differs from the original one only in the order of interface actions
and produces H, instead of H 0 . Hence, the library specification can simulate any behaviour
of its implementation the client can expect.
Lemma 6.5 (Rearrangement—library). If (δ(σ), H) v (δ(σ 0 ), H 0 ) and L : Γ is safe at σ 0 ,
then
∀λ0 ∈ JL : ΓKσ 0 . history(λ0 ) = H 0 =⇒ ∃λ ∈ JL : ΓKσ 0 . history(λ) = H.

LINEARIZABILITY WITH OWNERSHIP TRANSFER

23

(a):
(1, call m1 ([10 : 0]))
(1, ret m1 ([10 : 0]))
(2, call m2 ([10 : 0]))
(2, ret m2 ([ ]))

(b):
(1, call m1 ([10 : 0]))

(2, call m2 ([10 : 0]))

(1, ret m1 ([10 : 0]))

(2, ret m2 ([ ]))

Figure 8: Counterexample showing the need for history balancedness in Lemma 6.5
The proof of the lemma is highly non-trivial and is a subject of Section 7. We point
out Lemma 6.5 would not hold had we included unbalanced histories in our definition of
linearizability. To show this, take Σ = RAM and consider the histories in Figure 8. In
Figure 8(b) the library receives the cell 10 from the client, then returns it and then receives
it again. Even though the history in Figure 8(a) is linearized by that in Figure 8(b), the
former is not balanced, and by Proposition 5.4, cannot be produced by L. This shows that
Lemma 6.5 does not hold for unbalanced H.
Note that we have H v H for any history H. As a consequence, from Lemma 6.5
we obtain the following surprising result, stating that linearizability between libraries is
equivalent to inclusion between the sets of histories they produce.
Corollary 6.6. If L1 : Γ and L2 : Γ are safe for I1 and I2 , respectively, then
(L1 : Γ, I1 ) v (L2 : Γ, I2 ) ⇐⇒
∀(l, H) ∈ interf(L1 : Γ, I1 ). ∃l0 . l0  l ∧ (l0 , H) ∈ interf(L2 : Γ, I2 ).
This fact is not a consequence of ownership transfer and also holds for the classical notion
of linearizability. Intuitively, Lemma 6.5, and hence, Corollary 6.6 hold due to a closure
property of the semantics of the language from Section 4. Namely, in this and other programming languages, there may always be a delay between the point when a library method
is called and when it starts executing and, conversely, when it ends executing and when the
control returns to the client. For example, when executing the code in Figure 7(a), there
may be delays between a call to push, the execution of the atomic block and the return
from push. Hence, this library can produce both of the histories in Figures 1(b) and 1(c).
Due to this property of the program semantics, a trace from LLM, e.g., one producing
the history in Figure 1(c), will stay valid if we execute some of the calls in it earlier and
returns later, like in Figure 1(b). This is also (usually) safe given the ownership transfer
reading of calls and returns in the library-local semantics defined by JL : ΓK: it just means
that the library receives state from the client earlier and gives it up later. The proof of
Lemma 6.5 uses such transformations on a history to “de-linearize” it, e.g., transforming

24

A. GOTSMAN AND H. YANG

the history in Figure 1(c) into that in Figure 1(b). The above closure property is also the
reason for Theorem 6.2 guaranteeing that C(L2 ) can reproduce the history of C(L1 ) exactly.
Given that replacing a library L1 by its linearization L2 does not simplify its interface
set, can Theorem 6.2 really simplify reasoning about a complete program C(L1 )? Fortunately, the answer is yes, since the point of the theorem is to simplify the code of this
program. For example, replacing the library in Figure 2(a) by the one in Figure 7(a) allows us to pretend in reasoning about a complete program that changes to the library
state, shared between different threads, are atomic, and thus consider fewer possible thread
interleavings. Calls and returns in such a complete program are merely thread-local operations that do not complicate reasoning. In Section 6.2, we discuss an example of using
Theorem 6.2 to simplify proofs of complicated algorithms.
Specifying a library by an interface set H2 instead of code, as in Theorem 6.4, does
not allow us to get results such as Lemma 6.5 and Corollary 6.6, since the set H2 is not
guaranteed to satisfy any closure properties. For example, it might contain only sequential
histories, where every call is immediately followed by the corresponding return without a
delay. In fact, H2 has to be simpler than the interface set of L1 for Theorem 6.4 to be useful,
since this is what the theorem replaces L1 by. Fortunately, to prove Theorem 6.4 we can
exploit a closure property of the client-local semantics, formalised by the following variant
of the Rearrangement Lemma: any client trace can be transformed into an equivalent one
with a given history linearizing the history of the original one.
Lemma 6.7 (Rearrangement—client). If (l, H) v (l0 , H 0 ) and Γ ` C is safe at σ, then
∀κ ∈ JΓ ` CKσ. (δ(σ) ◦ l)↓ ∧ history(κ) = H =⇒ ∃κ0 ∈ JCKσ. history(κ0 ) = H 0 ∧ κ ∼ κ0 .

Intuitively, the lemma holds because, in the client-local semantics, it is safe to execute calls
later and returns earlier. Like Lemma 6.5, this lemma would not hold if we allowed H 0 to
be unbalanced.
In summary, when a library is specified by the code of its abstract implementation,
the ability to linearize a concrete history while looking for a matching abstract one allowed
by Definition 3.4 is not strictly needed. However, it is indispensable when the library is
specified directly by a set of histories. We were able to obtain this insight into the original
definition of linearizability by formalising the guarantees the linearizability of a library
provides to its clients as Abstraction Theorems.
Using Lemmas 6.5 and 6.7, we now prove the two versions of the Abstraction Theorem.
Proof of Theorem 6.2. The safety of C(L1 ) and C(L2 ) follows from Corollary 5.7. Take
(σ, τ1 ) ∈ JC(L1 ), I ∗ I1 K. We transform the trace τ1 of C(L1 ) into a trace τ2 of C(L2 ) with
the same client projection using the local semantics of L1 , L2 and C. Namely, we first apply
Corollary 5.7 to generate a pair (σl1 , λ1 ) ∈ JL1 : Γ, I1 K of a library-local initial state and a
trace and a client-local pair (σc , κ) ∈ JΓ ` C, IK, such that
σ = σc ∗ σl1 ∧ client(τ1 ) = ground(κ) ∧ history(κ) = history(λ1 ).

Since (L1 : Γ, I1 ) v (L2 : Γ, I2 ), for some

(σl2 , λ2 )

(δ(σl1 ), history(λ1 )) v
δ(σl1 ). By Lemma 6.5,

(6.1)

∈ JL2 : Γ, I2 K, we have

(δ(σl2 ), history(λ2 )),

which implies δ(σl2 ) 
λ2 can be transformed into a trace λ02 such
that
((σl2 , λ02 ) ∈ JL2 : Γ, I2 K) ∧ (history(λ02 ) = history(λ1 ) = history(κ)).

LINEARIZABILITY WITH OWNERSHIP TRANSFER

25

Since δ(σl2 )  δ(σl1 ) and (σc ∗σl1 )↓, we have (σc ∗σl2 )↓. We then use Corollary 5.8 to compose
the library-local trace λ02 with the client-local one κ into a trace τ2 such that
((σc ∗ σl2 , τ2 ) ∈ JC(L2 ), I ∗ I2 K) ∧ (client(τ2 ) = ground(κ) = client(τ1 )).
The above proof scheme can be described mnemonically as ‘decompose, rearrange, compose’.
We reuse its first two steps to prove Theorem 6.4.
Proof of Theorem 6.4. Take (σ, τ1 ) ∈ JC(L1 ), I ∗ I1 K. Like in the proof of Theorem 6.2, we
apply Corollary 5.7 to generate (σl1 , λ1 ) ∈ JL1 , I1 K and (σc , κ) ∈ JΓ ` C, IK such that (6.1)
holds. Since (L1 : Γ, I1 ) v H2 , for some (l2 , H2 ) ∈ H2 , we have
(l2  δ(σl1 )) ∧ ((δ(σl1 ), history(κ)) = (δ(σl1 ), history(λ1 )) v (l2 , H2 )).
Then by Lemma 6.7, κ can be transformed into a trace κ0 , such that
(σc , κ0 ) ∈ JΓ ` C, IK ∧ history(κ0 ) = H2 ∧ κ ∼ κ0

Since client(τ1 ) = ground(κ), we thus have client(τ1 ) ∼ ground(κ0 ). Furthermore, since
l2  δ(σl1 ) and (σc ∗ σl1 )↓, we have (δ(σc ) ◦ l2 )↓. Hence, κ0 and l2 are the required trace and
footprint.
6.2. Establishing and Using Linearizability with Ownership Transfer. Our preliminary investigations show that linearizability with ownership transfer can be established by
generalising existing proof systems for proving classical linearizability based on separation
logic [28]. The details of such a generalisation are out of the scope of this paper; we plan
to report on it in the future.
The Abstraction Theorem is not just a theoretical result: it enables compositional
reasoning about complex concurrent algorithms that are challenging for existing verification methods. For example, the theorem can be used to justify Vafeiadis’s compositional
proof [28, Section 5.3] of the multiple-word compare-and-swap (MCAS) algorithm implemented using an auxiliary operation called RDCSS [16] (the proof used an abstraction of
the kind enabled by Theorem 6.2 without justifying its correctness). If the MCAS algorithm
were verified together with RDCSS, its proof would be extremely complicated. Fortunately,
we can consider MCAS as a client of RDCSS, with the two components performing ownership transfers between them. The Abstraction Theorem then makes the proof tractable by
allowing us to verify the linearizability of MCAS assuming an atomic specification of the
inner RDCSS algorithm.
7. Proof of the Rearrangement Lemma
We only give the proof of Lemma 6.5, as that of Lemma 6.7 is completely symmetric.
The proof transforms λ0 into λ by repeatedly swapping adjacent actions in it according
to a certain strategy to make the history of the trace equal to H. The most subtle place in
the proof is swapping
(t1 , ret m1 (σ1 )) (t2 , call m2 (σ2 ))
to yield
(t2 , call m2 (σ2 )) (t1 , ret m1 (σ1 )),

26

A. GOTSMAN AND H. YANG

where t1 6= t2 . This case is subtle for the following reason. Let the state of the library L
before the return action be θ; then (θ \ σ1 )↓ and the state of the library after executing the
return and the call is (θ \ σ1 ) ∗ σ2 . For the swapping to be possible, we need (θ ∗ σ2 )↓; then
by Proposition 2.2
(θ \ σ1 ) ∗ σ2 = (θ ∗ σ2 ) \ σ1 ,
(7.1)
which can be used to establish that the resulting trace is still produced by L. However,
(θ ∗ σ2 )↓ is not guaranteed if the history H is arbitrary. For example, take Σ = RAM and
let H and H 0 be defined by Figures 8(a) and 8(b). Since H is unbalanced, it cannot be
produced by any library, and hence, we cannot swap
(1, ret m1 ([10 : 0])) (2, call m2 ([10 : 0]))
H 0.

in
In our proof we use the fact that the history H is balanced to show that a situation
in which we cannot swap a return followed by a call while transforming λ0 into λ cannot
happen. This is non-trivial, as the problematic situation can potentially happen midway
through the transformation. We only know that the target history H of λ is balanced, but
this does not straightforwardly imply that the histories of the intermediate traces obtained
while transforming λ0 into λ are, since these histories might be quite different from H.
Inferring their balancedness from that of H represents the most challenging part of the
proof.
We therefore first do the proof under an assumption that allows swapping a return
followed by a call easily and consider the general case later. This lets us illustrate the overall
idea of the proof, which is then reused in the additional part of the proof dealing with the
challenge presented by the general case. Namely, we make the following assumption:
Σ = RAM and for any ζ ∈ JL : ΓKσ 0 and interface actions ψ1 = (t1 , (σ1 ))
(7.2)
and ψ2 = (t2 , (σ2 )) in ζ, if t1 6= t2 , then dom(σ1 ) ∩ dom(σ2 ) = ∅.
For example, this holds when states transferred between the client and the library are always
thread-local. It is easy to check that in RAM, if (θ \ σ1 )↓, ((θ \ σ1 ) ∗ σ2 )↓ and (σ1 ∗ σ2 )↓, then
(θ ∗ σ2 )↓ and thus (7.1) holds. Hence, (7.2) allows us to justify swapping a return followed
by a call in a trace easily. We now proceed to prove Lemma 6.5 under this assumption. In
our proof, we use the assumption in a single place, which we note explicitly; the rest of the
proof is independent from it.
Below we sometimes write vρ instead of v to make the bijection ρ used to establish
the relation between histories in Definition 3.4 explicit. For a bijection ρ between histories
H and H 0 , we write idk (ρ) if ρ is an identity on the first k actions in H.
Take σ, σ 0 ∈ Σ and consider a trace λ0 ∈ JL : ΓKσ 0 . Assume histories H, H 0 such that
history(λ0 ) = H 0 and (δ(σ), H) v (δ(σ 0 ), H 0 ), so that H is balanced from δ(σ) and H 0 from
δ(σ 0 ). We prove that there exists a trace λ ∈ JL : ΓKσ 0 such that history(λ) = H. To this
end, we define a finite sequence of steps that transforms λ0 into a such a trace λ. The main
idea of the transformation is to make progressively longer prefixes of the trace have histories
coinciding with prefixes of H. Namely, the transformation is done in stages, and on stage
k = 0, 1, 2, . . . , |H| we obtain a trace αk ∈ JL : ΓKσ 0 , where α0 = λ0 . Every one of these
traces is such that for some prefix βk of αk we have:
history(βk ) = Hk ;
∃ρ. ((δ(σ), H) vρ (δ(σ 0 ), history(αk ))) ∧ idk (ρ);
∀j. 0 ≤ j < k =⇒ (βj is a prefix of βk ).

LINEARIZABILITY WITH OWNERSHIP TRANSFER

27

We let β0 = ε, so that the above conditions are initially satisfied. Thus, during the transformation, progressively longer prefixes βk of αk have histories coinciding with prefixes of
H, while the linearizability relation between the history H and that of αk is preserved. We
then take α|H| as the desired trace λ.
The trace αk+1 is constructed from the trace αk by applying the following lemma for
λ1 = βk , λ1 λ2 = αk , H1 = Hk , H1 ψH2 = H, αk+1 = λ1 λ02 λ002 and βk+1 = λ1 λ02 .
Lemma 7.1. Assume (7.2) holds. Consider a history H1 ψH2 and a trace λ1 λ2 ∈ JL : ΓKσ 0
such that
history(λ1 ) = H1 ;

(7.3)

0

(7.4)

∃ρ. ((δ(σ), H1 ψH2 ) vρ (δ(σ ), history(λ1 λ2 ))) ∧ id|H1 | (ρ).
Then there exist traces λ02 and λ002 such that λ1 λ02 λ002 ∈ JL : ΓKσ 0 and
history(λ1 λ02 ) = H1 ψ;

0

∃ρ . ((δ(σ), H1 ψH2 ) vρ0 (δ(σ

0

), history(λ1 λ02 λ002 )))

(7.5)
0

∧ id|H1 ψ| (ρ ).

(7.6)

To prove Lemma 7.1, we convert λ1 λ2 into λ1 λ02 λ002 by swapping adjacent actions in the
trace a finite number of times while preserving its properties of interest. These transformations are described by the following proposition, which formalises the closure properties of
the library-local semantics we alluded to in Section 6.1.
Proposition 7.2. Let L : Γ be safe at σ0 and consider ζ ∈ JL : ΓKσ0 and a history S
such that S vρ history(ζ). Then swapping any two adjacent actions ϕ1 ϕ2 in ζ executed by
different threads such that
(i) ϕ1 ∈ Act − RetAct, ϕ2 ∈ CallAct; or
(ii) ϕ1 ∈ RetAct, ϕ2 ∈ CallAct, ϕ2 precedes ϕ1 in S, and (7.2) holds; or
(iii) ϕ1 ∈ RetAct, ϕ2 ∈ Act − CallAct
yields a trace ζ 0 ∈ JL : ΓKσ0 such that S vρ0 history(ζ 0 ) for the bijection ρ0 defined as follows.
If ϕ1 6∈ CallRetAct or ϕ2 6∈ CallRetAct, then ρ0 = ρ. Otherwise, let i be the index of ϕ1 in
S. Then ρ0 (i + 1) = ρ(i), ρ0 (i) = ρ(i + 1) and ρ0 (k) = ρ(k) for k 6∈ {i, i + 1}.
Since, in the library-local semantics, the library gains state at a call and gives it up at
a return, intuitively, the transformation in the proposition allows the library to gain state
earlier (i, ii) and give it up later (iii). The assumption that ϕ2 precede ϕ1 in case (ii) is
needed to ensure that the transformation does not violate the linearizability relation. The
proof of case (ii) is the only place where the assumption (7.2) is used.
Proof sketch for Proposition 7.2. Consider ζ = ζ1 ϕ1 ϕ2 ζ2 ∈ JL : ΓKσ0 and let ζ 0 = ζ1 ϕ2 ϕ1 ζ2 .
The proof of the required linearizability relationship is trivial. It therefore remains to show
that ( , ζ 0 ) ∈ JL : ΓKσ0 . We know that for some α we have α ∈ LLM and ( , ζ) ∈ JαKσ0 . Let
α = α1 ϕ01 ϕ02 α2 and α0 = α1 ϕ02 ϕ01 α2 , where ϕ01 and ϕ02 correspond to ϕ1 and ϕ2 . It is easy to
see that α0 ∈ LLM. It therefore remains to show that ζ 0 ∈ Jα0 Kσ0 . The proof proceeds by case
analysis on the kind of actions ϕ1 and ϕ2 . The justification of the case when ϕ1 is a return
and ϕ2 is a call follows from (7.2) by the argument given earlier. Out of the remaining
cases, we only consider a single illustrative one: ϕ1 = (t1 , c) and ϕ2 = (t2 , call m2 (σ)) for
t1 6= t2 .
Assume (θ0 , ζ1 ϕ1 ϕ2 ) ∈ Jα1 ϕ01 ϕ02 Kσ0 . Then for some θ we have (θ, ζ1 ) ∈ Jα1 Kσ0 , fct1 (θ) 6=
> and θ0 ∈ fct1 (θ) ∗ {σ}. By the Footprint Preservation property, we get (θ ∗ σ)↓. Then by

28

A. GOTSMAN AND H. YANG

H 1 H2 :

H1

H2
⇢

1 2:
1

3

4

Figure 9: Illustration of the proof of Lemma 7.1
the Strong Locality property,
θ0 ∈ fct1 (θ) ∗ {σ} = fct1 (θ ∗ σ).
Hence, (θ0 , ζ1 ϕ2 ϕ1 ) ∈ Jα1 ϕ02 ϕ01 Kσ0 . Thus, Footprint Preservation and Strong Locality guarantee that a call can be safely executed earlier than a primitive command.
Proof of Lemma 7.1. From (7.3) and (7.4) it follows that λ2 = λ3 ψλ4 for some traces λ3
and λ4 , where ρ maps ψ in H1 ψH2 to the ψ action shown in λ2 ; see Figure 9. We consider
two cases.
1. ψ ∈ CallAct. Let t be the thread executing ψ. By (7.4) we have (H1 ψH2 )|t =
(history(λ1 λ2 ))|t . Then, since λ1 λ2 is a library trace, (7.3) implies that there are no actions
by thread t in λ3 . Furthermore, for any return action ϕ in λ3 , the action in H1 ψH2
corresponding to it according to ρ is in H2 . Thus, we can move the action ψ to the
position between λ1 and λ3 by swapping it with adjacent actions a finite number of times
as described in Proposition 7.2(i, ii). As a result, we obtain the trace λ1 ψλ3 λ4 ∈ JL : ΓKσ 0 .
Conditions (7.5)–(7.6) then follow from Proposition 7.2(i, ii) for λ02 = ψ and λ002 = λ3 λ4 .
2. ψ ∈ RetAct. Assume that λ3 contains a call action ϕ, so that it precedes the return
action ψ in history(λ1 λ2 ). Then by (7.3) and (7.4) the action in H1 ψH2 corresponding to
ϕ according to ρ is in H2 and thus follows ψ in H1 ψH2 . This violates the preservation of
the order of non-overlapping method invocations required by (7.4). Hence, there are no call
actions in λ3 . Since λ1 λ2 is a library trace, this implies that for any action ϕ = (t, ret )
in λ3 there are no actions by the thread t in λ3 following ϕ. Thus, we can move all return
actions in the subtrace λ3 of λ1 λ2 to the position between ψ and λ4 by swapping them
with adjacent actions a finite number of times as described in Proposition 7.2(iii). We thus
obtain the trace λ1 λ03 ψλ04 λ4 ∈ JL : ΓKσ 0 , where λ04 consists of all return actions in λ3 , and λ03
of the rest of actions in the subtrace; in particular, λ03 does not contain any interface actions.
Conditions (7.5)–(7.6) then follow from Proposition 7.2(iii) for λ02 = λ03 ψ and λ002 = λ04 λ4 .
This completes the proof of Lemma 6.5 under the assumption (7.2). Let us now lift this
assumption and consider the only place in the proof of the lemma that relies on it—that
when we swap a return followed by a call using Proposition 7.2(ii) in case 1 in the proof of
Lemma 7.1. Let us now identify precise conditions under which this situation happens. Let
ψ = (t1 , call m1 (σ1 )) and let the adjacent return action with which we are trying to swap
it be (t2 , ret m2 (σ2 )). Let S 1 be the target history H1 ψH2 from Lemma 7.1 and S 2 be the
history of the trace in which we are trying to swap the return and the call. Then the two

LINEARIZABILITY WITH OWNERSHIP TRANSFER

histories are of the form
S 1 = S (t1 , call m1 (σ1 )) S1 (t2 , ret m2 (σ2 )) S2 ;
S 2 = SS10 (t2 , ret m2 (σ2 )) (t1 , call m1 (σ1 )) S20

29

(7.7)

for some S, S1 , S2 , S10 , S20 . Furthermore, from the conditions of Lemma 7.1, we have:
(i) t1 6= t2 ;
(ii) S 1 and S 2 are balanced from some l1 and l2 , respectively, such that l2  l1 ; and
(iii) S 1 vρ S 2 , where id|S| (ρ) and ρ maps (t1 , call m1 (σ1 )) and (t2 , ret m2 (σ2 )) in S 1 to the
corresponding actions shown in S 2 .
As the following proposition shows, we can always do the desired transformation if the
history
SS10 (t1 , call m1 (σ1 )) (t2 , ret m2 (σ2 )) S20
(7.8)
2
resulting from swapping the return and the call in S is balanced from l2 .
Proposition 7.3. Let L : Γ be safe at σ0 . Consider traces
and

ζ = ζ1 (t2 , ret m2 (σ2 )) (t1 , call m1 (σ1 )) ζ2 ∈ JL : ΓKσ0

ζ 0 = ζ1 (t1 , call m1 (σ1 )) (t2 , ret m2 (σ2 )) ζ2 .
If history(ζ 0 ) is balanced from δ(σ0 ), then ζ 0 ∈ JL : ΓKσ0 .

Thus, the only problematic case we have is when the history (7.8) is not balanced from
l2 . We summarise all the conditions under which such case can happen in the following
definition.
Definition 7.4. Histories S 1 and S 2 of the form (7.7) are conflicting if the conditions
(i)–(iii) above are satisfied and the history (7.8) is not balanced from l2 .
Given Proposition 7.3, the only case when the transformation in the proof of Lemma 7.1
can fail to convert the trace is when H1 ψH2 and the history currently being transformed
are conflicting. Thus, with the assumption (7.2) lifted, Lemma 7.1 turns into

Lemma 7.5. Consider a history H1 ψH2 , and a trace λ1 λ2 ∈ JL : ΓKσ 0 such that (7.3) and
(7.4) hold. Then either H1 ψH2 and another history composed of actions from history(λ1 λ2 )
are conflicting, or there exist traces λ02 and λ002 such that λ1 λ02 λ002 ∈ JL : ΓKσ 0 and (7.5)
and (7.6) hold.
We now show that no conflicting pairs of histories exist, hence guaranteeing that
Lemma 7.5 can always be used to construct αk+1 from αk in transforming λ0 into λ. This
completes the proof of Lemma 6.5 in the general case.
We first discuss the main idea of the proof. The history S 1 in (7.7) is similar to (7.8)
in that the call precedes the return. We would like to use the fact that S 1 is balanced to
prove that so is (7.8), thereby yielding a contradiction. As we noted at the beginning of this
section, this is not straightforward due to the differences in the form of the histories S 1 and
S 2 other than the precedence of the two call and return actions. We resolve this problem
by adjusting the strategy we used above to transform λ0 into λ under the assumption (7.2)
to iron out the differences between S 1 and S 2 . In particular, we use a variant of the
transformation that, when the process of moving the call action ψ to the left in λ1 λ2
gets stuck (Figure 9), leaves the corresponding action in H1 ψH2 unmatched and continues
bringing the rest of the trace λ1 λ2 in sync with the target history.

30

A. GOTSMAN AND H. YANG

Lemma 7.6. There are no conflicting pairs of histories.
Proof. Consider histories S 1 and S 2 satisfying the conditions in Definition 7.4. Since S 2 is
balanced from l2 ,
JSS10 (t2 , ret m2 (σ2 ))K] l2 = (JSS10 K] l2 ) \\ δ(σ2 )
is defined. Assume
JSS10 (t1 , call m1 (σ1 ))K] l2 = (JSS10 K] l2 ) ◦ δ(σ1 )

is defined. Since (JSS10 K] l2 ) \\ δ(σ2 ) is defined, by Proposition 2.7, we have:
JSS10 (t1 , call m1 (σ1 )) (t2 , ret m2 (σ2 ))K] l2 = ((JSS10 K] l2 ) ◦ δ(σ1 )) \\ δ(σ2 ) =

((JSS10 K] l2 ) \\ δ(σ2 )) ◦ δ(σ1 ) = JSS10 (t2 , ret m2 (σ2 )) (t1 , call m1 (σ1 ))K] l2 .

Then (7.8) is balanced from l2 , contradicting our assumptions. Hence, ((JSS10 K] l2 ) ◦ δ(σ1 ))↑.
A call action in S10 cannot be in S2 : in this case it would follow (t2 , ret m2 (σ2 )) in S 1 ,
but precede it in S 2 , contradicting S 1 v S 2 . Hence, all call actions in S10 are in S1 . Let
S1 = S3 S4 , where S3 is the minimal prefix of S1 containing all call actions from S10 . Then
S 1 = S (t1 , call m1 (σ1 )) S3 S4 (t2 , ret m2 (σ2 )) S2 ;
S 2 = SS10 (t2 , ret m2 (σ2 )) (t1 , call m1 (σ1 )) S20 .
If S3 is non-empty, any return action in it precedes its last call action, which is also in S10 .
Since S 1 v S 2 , such a return action also has to be in S10 . Thus, all return actions in S3 are
in S10 .
The traces S 1 and S 2 are of the following more general form, obtained by letting
S0 = S (t1 , call m1 (σ1 )) and S00 = S:
S 1 = S0 S3 S4 (t2 , ret m2 (σ2 )) S2 ;
S 2 = S00 S10 (t2 , ret m2 (σ2 )) (t1 , call m1 (σ1 )) S20 ,
where
• S 1 and S 2 are balanced from some l1 and l2 , respectively, such that l2  l1 ;
• S0 and S00 are identical, except S0 may have some extra call actions;
• S 1 vρ S 2 ;
• ρ−1 maps all call actions in S10 to actions in S3 ;
• ρ maps all return actions in S3 to actions in S10 ;
• ρ−1 maps actions in S00 to those in S0 , in particular (t1 , call m1 (σ1 )) to an action in S0 ,
and (t2 , ret m2 (σ2 )) to the same action shown in S 1 ; and
• ((JS00 S10 K] l2 ) ◦ δ(σ1 ))↑.
We denote this form by (F). The additional call actions in S0 are the ones for which the
transformation in Lemma 7.1 failed. The conditions relating S3 and S10 imply that S3 may
have more calls than S10 , and S10 more returns than S3 . Thus, intuitively, S0 S3 gains more
state than S00 S10 , including that transferred by (t1 , call m1 (σ1 )), and S00 S10 gives up more
than S0 S3 . In the following, we use this and the fact that S 1 is balanced from a bigger
footprint than S 2 to show that ((JS00 S10 K] l2 ) ◦ δ(σ1 ))↓, thereby yielding a contradiction.
To this end, we describe a process that transforms the histories S 1 and S 2 into another pair of histories satisfying the conditions above, but such that S3 is strictly smaller.

LINEARIZABILITY WITH OWNERSHIP TRANSFER

31

Repeatedly applying this process, we can make S3 empty, obtaining histories satisfying (F):
S0 S4 (t2 , ret m2 (σ2 )) S2 ;
S00 S10 (t2 , ret m2 (σ2 )) (t1 , call m1 (σ1 )) S20 .

(7.9)

In particular, ((JS00 S10 K] l2 ) ◦ δ(σ1 ))↑. Before describing the transformation process, we show
that, given the above pair of histories, we can obtain a contradiction. We use the following
simple proposition, proved in Appendix A.1.
Proposition 7.7. Assume S is identical to S 0 , except it may have extra calls, and S and
S 0 are balanced from l1 and l2 , respectively, such that l2  l1 . Then the ◦-combination lc of
footprints of states transferred at the extra call actions in S is defined, S 0 is balanced from
l1 and
JSK] l1 = (JS 0 K] l1 ) ◦ lc ∧ JS 0 K] l2  JS 0 K] l1 .

Consider the histories in (7.9). Since all calls from S10 are in S3 = ε, S10 contains only returns.
Since the histories are balanced from l1 and l2 , respectively, JS0 K] l1 and JS00 K] l2 are defined.
The history S0 is identical to S00 , except it may have extra calls. By Proposition 7.7, the
◦-combination of footprints of states transferred at the extra call actions in S0 is defined.
Since an action (t1 , call m1 (σ1 )) is in S0 , but not in S00 , this combination is of the form
δ(σ1 ) ◦ lc for some lc ; hence,
JS0 K] l1 = (JS00 K] l1 ) ◦ δ(σ1 ) ◦ lc ∧ JS00 K] l2  JS00 K] l1 .

Therefore, (JS00 K] l2 ) ◦ δ(σ1 ) is defined. Since S10 contains only return actions,
JS00 S10 K] l2 = (JS00 K] l2 ) \\ l0 ,

where l0 is the ◦-combination of the footprints of states transferred at these actions. This
implies
JS00 K] l2 = (JS00 S10 K] l2 ) ◦ l0 ,
where both expressions are defined. But then so is
(JS00 K] l2 ) ◦ δ(σ1 ) = (JS00 S10 K] l2 ) ◦ l0 ◦ δ(σ1 ).

Hence, (JS00 S10 K] l2 ) ◦ δ(σ1 ) is defined, contradicting the opposite fact established above. This
contradiction implies that a conflicting pair of histories does not exist.
Now assume arbitrary histories S 1 and S 2 satisfying (F):
S 1 = S0 S3 S4 (t2 , ret m2 (σ2 )) S2 ;
S 2 = S00 S10 (t2 , ret m2 (σ2 )) (t2 , call m1 (σ1 )) S20 ,
We show that from these we can construct another pair of histories satisfying (F), but with
S3 strictly smaller. We use the same transformation as in the proof of Lemma 7.1. When
this transformation gets stuck, we obtain another pair of histories of the form (F), but again
with a smaller S3 .
Let us make a case split on the next action in S3 .
• S3 = (t, call m(σ)) S5 , such that the action corresponding to (t, call m(σ)) according to ρ
is not in S10 . In this case we let S0 := S0 (t, call m(σ)) and S3 := S5 . Thus, the call action
(t, call m(σ)) unmatched in S10 becomes part of S0 .

32

A. GOTSMAN AND H. YANG

• S3 = (t, call m(σ)) S5 , such that the action corresponding to (t, call m(σ)) according to ρ
is in S10 . Let S10 = S30 (t, call m(σ))S40 , so that
S 1 = S0 (t, call m(σ)) S5 S4 (t2 , ret m2 (σ2 )) S2 ;
S 2 = S00 S30 (t, call m(σ)) S40 (t2 , ret m2 (σ2 )) (t2 , call m1 (σ1 )) S20 .
Using the transformations from case 1 in the proof of Lemma 7.1, we can try to move the
action (t, call m(σ)) to the position between S00 and S30 while preserving the balancedness
of the history. If this succeeds, we construct a new pair of histories of the form (F)
by letting S0 := S0 (t, call m(σ)), S3 := S5 , S00 := S00 (t, call m(σ)) and S10 := S30 S40 .
Otherwise, we get a pair of conflicting histories, which are of the form (F) but with a
smaller S3 . Again, in this case the unmatched call action (t, call m(σ)) becomes part of
S0 .
• S3 = (t, ret m(σ)) S5 . Then the action corresponding to (t, ret m(σ)) according to ρ is
also in S10 , so that S10 = S30 (t, ret m(σ)) S40 :
S 1 = S0 (t, ret m(σ)) S5 S4 (t2 , ret m2 (σ2 )) S2 ;
S 2 = S00 S30 (t, ret m(σ)) S40 (t2 , ret m2 (σ2 )) (t2 , call m1 (σ1 )) S20 .
Using the transformations from case 2 in the proof of Lemma 7.1, we can move the return
action to the position between S00 and S30 while preserving the balancedness of the history.
We thus obtain a pair of histories:
S 1 = S0 (t, ret m(σ)) S5 S4 (t2 , ret m2 (σ2 )) S2 ;
S 2 = S00 (t, ret m(σ)) S30 S40 (t2 , ret m2 (σ2 )) (t2 , call m1 (σ1 )) S20 .
Then we can let S0 := S0 (t, ret m(σ)), S3 := S5 , S00 := S00 (t, ret m(σ)) and S10 := S30 S40 .
8. Frame Rule for Linearizability
Libraries such as concurrent containers are used by clients to transfer the ownership of data
structures, but do not actually access their contents. We show that for such libraries, the
classical linearizability implies linearizability with ownership transfer.
Definition 8.1. A method specification Γ0 = {{rm } m {sm } | m ∈ M } extends a specifim
m
cation Γ = {{pm } m {q m } | m ∈ M }, if ∀t. rtm ⊆ pm
t ∗ Σ ∧ st ⊆ qt ∗ Σ.
For example, the method specification (4.1) of the stack in Figure 2(a) extends the
following specification:
{∃x. argt 7→ x} push {argt 7→ OK ∨ argt 7→ FULL};
{∃y. argt 7→ y} pop {∃x. argt 7→ x}.

(8.1)

According to this specification, push just receives an arbitrary pointer x as a parameter; in
contrast, the specification (4.1) additionally mandates that the object the pointer identifies
be transferred to the library. We now identify conditions under which the linearizability
between a pair of libraries satisfying Γ entails that of the same libraries satisfying an extended method specification Γ0 . This yields a result somewhat analogous to the frame rule
of separation logic [26].
We start by introducing some auxiliary definitions. We first define operations for mapping between histories corresponding to extended and non-extended method specifications.

LINEARIZABILITY WITH OWNERSHIP TRANSFER

33

For the method specification Γ from Definition 8.1, we define operations T·UΓ and V·WΓ on
interface actions as follows:
T(t, call m(σ))UΓ = (t, call m(σ \ (σ \ pm
t )));
m
T(t, ret m(σ))UΓ = (t, ret m(σ \ (σ \ qt )));
V(t, call m(σ))WΓ = (t, call m(σ \ pm
t ));
m
V(t, ret m(σ))WΓ = (t, ret m(σ \ qt ));

otherwise, the result is undefined. Thus, TψUΓ selects the part of the state in ψ that is
required by Γ and VψWΓ the extra piece of state not required by it. We then lift T·UΓ and
V·WΓ to traces by applying them to every interface action.
Given a history H0 produced by a library L : Γ0 , we need to be able to check that
the library does not modify the extra pieces of state not required by the original method
specification Γ, which are given by VH0 WΓ . To this end, we define an evaluation function
similar to h·i] from Section 3, which is meant to be applied to VH0 WΓ . For an interface
action ψ we define hψi : Σ → (Σ ∪ {>}) as follows:
h(t, call m(σ0 ))iσ = if (σ ∗ σ0 )↓ then σ ∗ σ0 else >;
h(t, ret m(σ0 ))iσ = if (σ \ σ0 )↓ then σ \ σ0 else >.
We then define the evaluation hHi : Σ → (Σ ∪ {>}) of a history H as follows:
hεiσ = σ;

hHψiσ = if (hHiσ 6= >) then hψi(hHiσ) else >.

Thus, if the evaluation does not fail, then the history respects the notion of ownership and
the pieces of state transferred to the library are returned to the client unmodified.
Theorem 8.2 (Frame rule). Assume
(1) Γ0 extends Γ;
(2) for all i ∈ {1, 2}, Li : Γ and Li : Γ0 are safe for Ii and Ii ∗ I, respectively;
(3) (L1 : Γ, I1 ) v (L2 : Γ, I2 ); and
(4) for every σ0 ∈ I1 , σ00 ∈ I and λ ∈ JL1 : Γ0 K(σ0 ∗ σ00 ), we have hVhistory(λ)WΓ iσ00 6= >.
Then (L1 : Γ0 , I1 ∗ I) v (L2 : Γ0 , I2 ∗ I).
The theorem allows us to establish the linearizability relation with respect to the extended specification Γ0 given the relation with respect to Γ. This enables the use of the
Abstraction Theorem for clients performing ownership transfer. However, the theorem does
not guarantee the safety of the libraries with respect to Γ0 for free, because it is not implied
by their safety with respect to Γ. Intuitively, this is because Γ0 extends both preconditions and postconditions in Γ; hence, not only does it guarantee to the library that the
client will provide extra pieces of state at calls, but it also requires the library to provide (possibly different) extra pieces of state at returns. For example, Γ might assign
the specification {argt 7→ } m {argt 7→ } to every method m, and Γ0 , the specification
{argt 7→ } m {∃x. argt 7→ x ∗ x 7→ }. Unless a library already has all the memory required
by the postconditions in Γ0 in its initial state, it has no way of satisfying Γ0 .
This situation is in contrast to the frame rule of separation logic [26], which guarantees
the safety of a piece of code with respect to an extended specification. However, the frame
rule requires the latter specification to extend both pre- and postconditions with the same
piece of state, so that the code returns it immediately after termination. In our setting,
a library can return the extra state to its client after a different method invocation and,
possibly, in a different thread.

34

A. GOTSMAN AND H. YANG

Finally, condition (4) in Theorem 8.2 ensures that the extra memory required by postconditions in Γ0 comes from the extra memory provided in its preconditions and the extension of the initial state, not from the memory transferred according to Γ.
It can be shown that for the library L1 in Figure 2(a), the library L2 in Figure 7(a)
and method specification Γ defined by (8.1), we have (L1 : Γ, I1 ) v (L2 : Γ, I2 ). It is
also not difficult to prove (e.g., using separation logic) that L1 : Γ0 and L2 : Γ0 are safe.
Condition (4) in Theorem 8.2 is satisfied, since the proof of safety of L1 : Γ0 would use only
the extra state provided in the preconditions of Γ0 to provide the extra state required by
its postconditions. Hence, by Theorem 8.2 we have (L1 : Γ0 , I1 ) v (L2 : Γ0 , I2 ).
However, Theorem 8.2 is not applicable to the memory allocators in Figures 2(b)
and 7(b): since the allocator implementation in Figure 2(b) stores free-list pointers inside
the memory blocks, it is unsafe with respect to the variant of the method specification (4.2)
that does not transfer their ownership.
The proof of Theorem 8.2 relies on the following two lemmas, proved in Appendices A.3
and A.4, that convert between library traces corresponding to extended and original method
specifications. The first lemma shows that for a trace λ produced by L : Γ0 , the trace TλUΓ
can be produced by L : Γ. The safety of the library with respect to Γ and condition (4)
from Theorem 8.2 guarantee that the smaller preconditions specified by Γ are enough for
the library to execute safely and that the extra pieces of state in Γ0 do not influence its
execution.
Lemma 8.3. If λ ∈ JL : Γ0 K(σ0 ∗ σ00 ), L : Γ is safe at σ0 , and hVhistory(λ)WΓ iσ00 6= >, then
TλUΓ ∈ JL : ΓKσ0 .
The other lemma gives conditions under which we can conclude that a trace λ is produced by L : Γ0 given that TλUΓ is produced by L : Γ.

Lemma 8.4. Assume TλUΓ ∈ JL : ΓKσ0 , (σ0 ∗ σ00 )↓, history(λ) is balanced from δ(σ000 ∗ σ00 )
for δ(σ0 )  δ(σ000 ), and hVhistory(λ)WΓ iσ00 6= >. Then λ ∈ JL : Γ0 K(σ0 ∗ σ00 ).
Proof of Theorem 8.2. Consider a trace λ1 ∈ JL1 : Γ0 K(σ1 ∗σ), where σ1 ∈ I1 and σ ∈ I. Then
by (4) we have hVhistory(λ1 )WΓ iσ 6= >, and hence by Lemma 8.3 we have Tλ1 UΓ ∈ JL1 : ΓKσ1 .
Since (L1 : Γ, I1 ) v (L2 : Γ, I2 ), for some σ2 ∈ I2 and λ2 ∈ JL2 : ΓKσ2 we have
(δ(σ1 ), history(Tλ1 UΓ )) v (δ(σ2 ), history(λ2 )).

By Lemma 6.5, there exists λ02 ∈ JL2 : ΓKσ2 such that history(λ02 ) = history(Tλ1 UΓ ). Let λ002
be the trace λ02 with its interface actions replaced so that they form the history history(λ1 ).
Then Tλ002 UΓ = λ02 and Vhistory(λ002 )WΓ = Vhistory(λ1 )WΓ . Since δ(σ2 )  δ(σ1 ), we have
(σ2 ∗ σ)↓. Hence, by Lemma 8.4, λ002 ∈ JL2 : Γ0 K(σ2 ∗ σ), from which the required follows.
9. Related Work
The original definition of linearizability [18] was proposed in an abstract setting that did not
consider a particular programming language and implicitly assumed a complete isolation
between the states of the client and the library. Furthermore, at the time it was not clear
what the linearizability of a library entails for its clients. Filipović et al. [12] were the first
to observe that linearizability implies a form of contextual refinement; technically, their
result is similar to our Lemma 6.7, but formulated over a highly idealistic semantics. In a

LINEARIZABILITY WITH OWNERSHIP TRANSFER

35

previous work [14], we generalised their result to a compositional proof method, formalised
by an Abstraction Theorem, that allows one to replace a concrete library by an abstract
one in reasoning about a complete program.
This paper is part of our recent push to propose notions of concurrent library correctness for realistic programming languages. So far we have developed such notions together
with the corresponding Abstraction Theorems for supporting reasoning about liveness properties [14] and weak memory models [4, 6, 15]. All these results assumed that the library
and its client operate in disjoint address spaces and, hence, are guaranteed not to interfere
with each other and cannot communicate via the heap. Lifting this restriction is the goal
of the present paper. Although the basic proof structure of Theorems 6.2 and 6.4 is the
same as in [6,14], the formulations and proofs of the Abstraction Theorem and the required
lemmas here have to deal with technical challenges posed by ownership transfer that did
not arise in previous work. First, their formulations rely on the novel forms of client-local
and library-local semantics (Section 5) that allow a component to communicate with its
environment via ownership transfers. Proving Lemma 5.6 then involves a delicate tracking
of a splitting between the parts of the state owned by the library and the client, and how
ownership transfers affect it. Second, the key result needed to establish the Abstraction
Theorem is the Rearrangement Lemma (Lemmas 6.5 and 6.7). What makes the proof of
this lemma difficult in our case is the need to deal with subtle interactions between concurrency and ownership transfer that have not been considered in previous work. Namely,
changing the history in the lemma requires commuting ownership transfer actions; justifying the correctness of these transformations is non-trivial and relies on the notion of history
balancedness that we propose. These differences notwithstanding, we hope that techniques
for handling ownership transfer proposed in this paper can be combined with the ones for
handling other types of client-library interactions considered so far [4, 6, 14, 15].
Recently, there has been a lot of work on verifying linearizability of common algorithms;
representative papers include [1, 10, 28]. All of them proved classical linearizability, where
libraries and their clients exchange values of a given data type and do not perform ownership
transfers. This includes even libraries, such as concurrent containers, that are actually
used by client threads to transfer the ownership of data structures. The frame rule for
linearizability we propose (Theorem 8.2) justifies that classical linearizability established
for concurrent containers entails linearizability with ownership transfer. This makes our
Abstraction Theorem applicable, enabling compositional reasoning about their clients.
Turon and Wand [27] have proposed a logic for establishing refinements between concurrent modules, likely equivalent to linearizability [12]. Their logic considers libraries and
clients residing in a shared address space, but not ownership transfer. As a result, they do
not support separate reasoning about a library and its client in realistic situations of the
kind we consider.
Elmas et al. [10,11] have developed a system for verifying concurrent programs based on
repeated applications of atomicity abstraction. They do not use linearizability to perform
the abstraction. Instead, they check the commutativity of an action to be incorporated
into an atomic block with all actions of other threads. In particular, to abstract a library
implementation in a program by its atomic specification, their method would have to check
the commutativity of every internal action of the library with all actions executed by the
client code of other threads. Thus, the method of Elmas et al. does not allow decomposing
the verification of a program into verifying libraries and their clients separately. In contrast,
our Abstraction Theorem ensures the atomicity of a library under any safe client.

36

A. GOTSMAN AND H. YANG

The most common approach of decomposing the verification of concurrent programs
is using thread-modular reasoning methods, which consider every thread in the program
in isolation under some assumptions on its environment [20, 24]. However, a single thread
would usually make use of multiple program components. This work goes further by allowing
a finer-grain intrathread-modular reasoning: separating the verification of a library and its
client, the code from both of which may be executed by a single thread. Note that this
approach is complementary to thread-modular reasoning, which can still be used to carry
out the verification subtasks, such as establishing the linearizability of libraries and proving
the safety of clients. Thread-modular techniques do enable a restricted form of intrathreadmodular reasoning, since they allow reasoning about the control of a thread in a program
while ignoring the possibility of its interruption by the other threads. Hence, they allow
considering a library method called by the thread in isolation, e.g., by using the standard
proof rules for procedures. However, such a decomposition is done under fixed assumptions
on the environment of the thread and thus does not allow, e.g., increasing the atomicity of
the environment’s actions. As the example of MCAS shows (Section 6.2), this is necessary
to deal with complex algorithms.
Ways of establishing relationships between different sequential implementations of the
same library have been studied in data refinement [19, 25], including cases of interactions
via ownership transfer [3, 13, 22]. Our results can be viewed as generalising data refinement
to the concurrent setting. Moreover, when specialised to the sequential case, they provide
a more flexible method of performing it in the presence of the heap and ownership transfer
than previously proposed ones. In more detail, the way we define client safety (Section 5)
is more general some of the ways used in data refinement [13]. There, it is typical to fix a
(precise) invariant of a library and check that the client does not access the area of memory
fenced off by the invariant. Here we do not require an explicit library invariant, using the
client-local semantics instead: since primitive commands fault when accessing non-existent
memory cells, the safety of the client in this semantics ensures that it does not access the
internals of the library. We note that the approach requiring an invariant for library-local
data structures does not generalise to the concurrent setting: while a precise invariant for
the data structures shared among threads executing library code is not usually difficult to
find, the state of data structures local to the threads depends on their program counters.
Thus, an invariant insensitive to program positions inside the library code often does not
exist. Such difficulties are one of reasons for using client- and library-local semantics in this
paper.
Finally, we note that the applicability of our results is not limited to proving existing
programs correct: they can also be used in the context of formal program development.
In this case, instead of abstracting an existing library to an atomic specification while
proving a complete program, the Abstraction Theorem allows refining an atomic library
specification to a concrete concurrent implementation while developing a program topdown [2, 21]. Our work thus advances the method of atomicity refinement to a setting
with concurrent components sharing an address space and communicating via ownership
transfers.
Acknowledgements
We would like to thank Anindya Banerjee, Josh Berdine, Xinyu Feng, Hongjin Liang, Victor
Luchangco, David Naumann, Peter O’Hearn, Matthew Parkinson, Noam Rinetzky and

LINEARIZABILITY WITH OWNERSHIP TRANSFER

37

Julles Villard for helpful comments. Gotsman was supported by the EU FET project
ADVENT. Yang was supported by EPSRC.
References
[1] D. Amit, N. Rinetzky, T. W. Reps, M. Sagiv, and E. Yahav. Comparison under abstraction for verifying
linearizability. In CAV’07: Conference on Computer Aided Verification, volume 4590 of LNCS, pages
477–490. Springer, 2007.
[2] R.-J. Back. On correct refinement of programs. J. Comput. Syst. Sci., 23(1):49–68, 1981.
[3] A. Banerjee and D. A. Naumann. Ownership confinement ensures representation independence in objectoriented programs. J. ACM, 52(6):894–960, 2005.
[4] Mark Batty, Mike Dodds, and Alexey Gotsman. Library abstraction for C/C++ concurrency. In
POPL’13: Symposium on Principles of Programming Languages, pages 235–248. ACM Press, 2013.
[5] R. Bornat, C. Calcagno, P. O’Hearn, and M. Parkinson. Permission accounting in separation logic. In
POPL’05: Symposium on Principles of Programming Languages, pages 259–270. ACM Press, 2005.
[6] S. Burckhardt, A. Gotsman, M. Musuvathi, and H. Yang. Concurrent library correctness on the TSO
memory model. In ESOP’12: European Symposium on Programming, volume 7211 of LNCS, pages
87–107. Springer, 2012.
[7] C. Calcagno, P. O’Hearn, and H. Yang. Local action and abstract separation logic. In LICS’07: Symposium on Logic in Computer Science, pages 366–378. IEEE, 2007.
[8] D. G. Clarke, J. Noble, and J. M. Potter. Simple ownership types for object containment. In ECOOP’01:
European Conference on Object-Oriented Programming, volume 2072 of LNCS, pages 53–76. Springer,
2001.
[9] M. Dodds, X. Feng, M. Parkinson, and V. Vafeiadis. Deny-guarantee reasoning. In ESOP’09: European
Symposium on Programming, volume 5502 of LNCS, pages 363–377. Springer, 2009.
[10] T. Elmas, S. Qadeer, A. Sezgin, O. Subasi, and S. Tasiran. Simplifying linearizability proofs with
reduction and abstraction. In TACAS’10: Conference on Tools and Algorithms for the Construction
and Analysis of Systems, volume 6015 of LNCS, pages 296–311. Springer, 2010.
[11] T. Elmas, S. Qadeer, and S. Tasiran. A calculus of atomic actions. In POPL’09: Symposium on Principles of Programming Languages, pages 2–15. ACM Press, 2009.
[12] I. Filipović, P. O’Hearn, N. Rinetzky, and H. Yang. Abstraction for concurrent objects. Theor. Comput.
Sci., 411(51-52):4379–4398, 2010.
[13] I. Filipović, P. O’Hearn, N. Torp-Smith, and H. Yang. Blaiming the client: On data refinement in the
presence of pointers. Form. Asp. Comput., 22(5):547–583, 2010.
[14] A. Gotsman and H. Yang. Liveness-preserving atomicity abstraction. In ICALP’11: International Colloquium on Automata, Languages and Programming, volume 6756 of LNCS, pages 453–465. Springer,
2011.
[15] Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang. Show no weakness: sequentially consistent
specifications of TSO libraries. In DISC’12: Symposium on Distributed Computing, volume 7611 of
LNCS, pages 31–45. Springer, 2012.
[16] T. Harris, K. Fraser, and I. Pratt. A practical multi-word compare-and-swap operation. In DISC’02:
Symposium on Distributed Computing, volume 2508 of LNCS, pages 265–279. Springer, 2002.
[17] M. Herlihy and N. Shavit. The art of multiprocessor programming. Morgan Kaufmann, 2008.
[18] M. Herlihy and J. M. Wing. Linearizability: a correctness condition for concurrent objects. ACM Trans.
Program. Lang. Syst., 12(3):463–492, 1990.
[19] C. A. R. Hoare. Proof of correctness of data representations. Acta Inf., 1:271–281, 1972.
[20] C. B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321–332, 1983.
[21] C. B. Jones. Splitting atoms safely. Theor. Comput. Sci., 375(1-3):109–119, 2007.
[22] I. Mijajlovic and H. Yang. Data refinement with low-level pointer operations. In APLAS’05: Asian
Symposium on Programming Languages and Systems, volume 3780 of LNCS, pages 19–36. Springer,
2005.
[23] P. O’Hearn. Resources, concurrency and local reasoning. Theor. Comput. Sci., 375(1-3):271–307, 2007.
[24] A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and
Models of Concurrent Systems, pages 123–144. Springer, 1985.

38

A. GOTSMAN AND H. YANG

[25] J. C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP Congress, pages 513–523,
1983.
[26] J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS’02: Symposium
on Logic in Computer Science, pages 55–74. IEEE, 2002.
[27] A. Turon and M. Wand. A separation logic for refining concurrent objects. In POPL’11: Symposium
on Principles of Programming Languages, pages 247–258. ACM Press, 2011.
[28] V. Vafeiadis. Modular fine-grained concurrency verification. PhD Thesis. University of Cambridge, 2008.
[29] V. Vafeiadis. Automatically proving linearizability. In CAV’10: Conference on Computer Aided Verification, volume 6174 of LNCS, pages 450–464. Springer, 2010.

Appendix A. Additional proofs
A.1. Proof of Proposition 7.7. We prove the required by induction on the length of S.
If S is empty, then so is S 0 and lc = δ(e). Assume the statement of the proposition is valid
for all histories S of length less than n > 0. Consider a history S = S0 ψ of length n and a
corresponding history S 0 satisfying the conditions of the proposition. We now make a case
split on the type of the action ψ.
• ψ is a call transferring σ0 that is not in S 0 . Then S0 and S 0 are identical except S0 may
have extra calls. Hence, by the induction hypothesis for S0 and S 0 , S 0 is balanced from
l1 , JS 0 K] l2  JS 0 K] l1 and
JSK] l1 = JS0 ψK] l1 = (JS0 K] l1 ) ◦ δ(σ0 ) = (JS 0 K] l1 ) ◦ (lc ◦ δ(σ0 )).

• ψ is a call transferring σ0 also present in S 0 . Then S 0 = S00 ψ, where S00 and S0 are identical
except S0 may have extra calls. Hence, by the induction hypothesis for S0 and S00 , we
have
JSK] l1 = JS0 ψK] l1 = (JS0 K] l1 ) ◦ δ(σ0 ) =

(JS00 K] l1 ) ◦ lc ◦ δ(σ0 ) = (JS00 ψK] l1 ) ◦ lc = (JS 0 K] l1 ) ◦ lc .

In particular, S 0 is balanced from l1 . By the induction hypothesis for S0 and S00 , we also
have JS00 K] l2  JS00 K] l1 . From this we get
JS 0 K] l2 = JS00 ψK] l2 = (JS00 K] l2 ) ◦ δ(σ0 )  (JS00 K] l1 ) ◦ δ(σ0 ) = JS00 ψK] l1 = JS 0 K] l1 .

• ψ is a return transferring σ0 . Then it is also present in S 0 , so that S 0 = S00 ψ, where S0
and S00 are identical except S0 may have extra calls. Then by the induction hypothesis
for S0 and S00 , we have:
JSK] l1 = JS0 ψK] l1 = (JS0 K] l1 ) \\ δ(σ0 ) = ((JS00 K] l1 ) ◦ lc ) \\ δ(σ0 ).

Since S 0 = S00 ψ is balanced from l2 , (JS00 K] l2 ) \\ δ(σ0 ) is defined. Furthermore, by the induction hypothesis for S0 and S00 , we also have JS00 K] l2  JS00 K] l1 . Hence, (JS00 K] l1 ) \\ δ(σ0 )
is defined as well. By Proposition 2.7, we then have:
JSK] l1 = ((JS00 K] l1 ) ◦ lc ) \\ δ(σ0 ) =

((JS00 K] l1 ) \\ δ(σ0 )) ◦ lc = (JS00 ψK] l1 ) ◦ lc = (JS 0 K] l1 ) ◦ lc .

In particular, S 0 is balanced from l1 . From JS00 K] l2  JS00 K] l1 , it also follows that

JS 0 K] l2 = JS00 ψK] l2 = (JS00 K] l2 ) \\ δ(σ0 )  (JS00 K] l1 ) \\ δ(σ0 ) = JS00 ψK] l1 = JS 0 K] l1 .

LINEARIZABILITY WITH OWNERSHIP TRANSFER

39

A.2. Proof of Lemma 5.6. Before delving into the proof of Lemma 5.6, we prove three
important lemmas about our semantics that justify its key steps. The first concerns the
evaluation of a call or a return action: intuitively, it says that the evaluation of such an
action by the client matches that by the library.
Lemma A.1 (Preservation). Let Γ be a method specification, σ0 , σ1 states, and ϕ an action
describing a call to or return from a method specified in Γ such that
Then for all

σ00 , σ10 , ϕ0 ,

JΓ ` ϕKσ0 6= > ∧ Jϕ : ΓKσ1 6= >.

((σ00 , ϕ0 ) ∈ JΓ ` ϕKσ0 ∧ (σ10 , ϕ0 ) ∈ Jϕ : ΓKσ1 ) =⇒ ((σ00 ∗ σ10 )↓ ⇐⇒ (σ0 ∗ σ1 )↓ ).

If furthermore σ0 ∗ σ1 is defined, then we have

{σ0 ∗ σ1 } = {σ00 ∗ σ10 | ∃ϕ0 . (σ00 , ϕ0 ) ∈ JΓ ` ϕKσ0 ∧ (σ10 , ϕ0 ) ∈ Jϕ : ΓKσ1 ∧ (σ00 ∗ σ10 )↓ }.

Proof. Consider Γ, σ0 , σ1 , ϕ satisfying the conditions in the lemma. We show the lemma
only for the case when ϕ is a call action: for some t, m, p, we have ϕ = (t, call m) and
{p} m { } ∈ Γ. The proof for the other case is symmetric.
To show the first claim of the lemma, consider σ00 , σ10 , ϕ0 such that
(σ00 , ϕ0 ) ∈ JΓ ` ϕKσ0 ∧ (σ10 , ϕ0 ) ∈ Jϕ : ΓKσ1 .

By the definition of the action evaluation, there exist σ2 , σ3 such that
ϕ0 = (t, call m(σ3 )) ∧ (σ2 ∗ σ3 )↓ ∧ (σ3 ∗ σ1 )↓ ∧ σ0 = σ2 ∗ σ3 ∧ σ00 = σ2 ∧ σ10 = σ3 ∗ σ1 .
Hence,
(σ00 ∗ σ10 )↓ ⇐⇒ (σ2 ∗ (σ3 ∗ σ1 ))↓ ⇐⇒ ((σ2 ∗ σ3 ) ∗ σ1 )↓ ⇐⇒ (σ0 ∗ σ1 )↓ .
Let us move on to the second claim of the lemma. Since JΓ ` (t, call m)Kσ0 6= >, pt is
precise and the ∗ operator is cancellative, there exists a unique splitting σ2 ∗ σ3 = σ0 of σ0
such that σ3 ∈ pt . Let ϕ0 = (t, call m(σ3 )). Then
({(σ2 , ϕ0 )} = JΓ ` (t, call m)Kσ0 ) ∧ (∀σ10 . (σ10 , ϕ0 ) ∈ J(t, call m) : ΓKσ1 ⇐⇒ σ10 = σ3 ∗ σ1 ).

Hence,

{σ00 ∗ σ10 | ∃ϕ0 . (σ00 , ϕ0 ) ∈ JΓ ` (t, call m)Kσ0 ∧ (σ10 , ϕ0 ) ∈ J(t, call m) : ΓKσ1 ∧ (σ00 ∗ σ10 )↓ }
= {σ2 ∗ (σ3 ∗ σ1 )} = {σ0 ∗ σ1 }.

The second lemma describes the decomposition and composition properties of trace evaluation.
Lemma A.2 (Trace Decomposition and Composition). Consider traces τ, κ, λ without interface actions such that cover(τ, κ, λ). For all states σ0 , σ1 , if
then
and

(σ0 ∗ σ1 )↓ ∧ JΓ ` κKσ0 6= > ∧ Jλ : ΓKσ1 6= >,

(A.1)

Jτ K(σ0 ∗ σ1 ) = {(σ 0 , τ ) ∈ JΓ ` κKσ0 ⊗ Jλ : ΓKσ1 }

(A.2)

∀σ00 , σ10 , κ0 , λ0 . (cover(τ, κ0 , λ0 ) ∧ (σ00 , κ0 ) ∈ JΓ ` κKσ0 ∧ (σ10 , λ0 ) ∈ Jλ : ΓKσ1 )

=⇒ (σ00 ∗ σ10 )↓ . (A.3)

40

A. GOTSMAN AND H. YANG

Proof. Consider τ, κ, λ, σ0 , σ1 , Γ satisfying the assumptions. We prove the lemma by induction on the length of τ . The base case of τ being the empty sequence is trivial.
Now suppose that τ = τ 0 ϕ for some τ 0 , ϕ. Then there exist κ0 and λ0 such that
cover(τ 0 , κ0 , λ0 ) ∧ ((κ = κ0 ϕ ∧ λ = λ0 ) ∨ (κ = κ0 ∧ λ = λ0 ϕ) ∨ (κ = κ0 ϕ ∧ λ = λ0 ϕ)).
By the assumption of the lemma, we have that
JΓ ` κ0 Kσ0 6= > ∧ Jλ0 : ΓKσ1 6= >.

(A.4)

Jτ 0 K(σ0 ∗ σ1 ) = {(σ 0 , τ 0 ) ∈ JΓ ` κ0 Kσ0 ⊗ Jλ0 : ΓKσ1 }

(A.5)

Hence, by the induction hypothesis, we have that
and

∀σ00 , σ10 , κ00 , λ00 . (cover(τ 0 , κ00 , λ00 ) ∧ (σ00 , κ00 ) ∈ JΓ ` κ0 Kσ0 ∧ (σ10 , λ00 ) ∈ Jλ0 : ΓKσ1 )

=⇒ (σ00 ∗ σ10 )↓ . (A.6)

From (A.5) it follows that:
Next, we prove that

Jτ 0 K(σ0 ∗ σ1 ) 6= >.

(A.7)

Jτ 0 ϕK(σ0 ∗ σ1 ) 6= >.
(A.8)
For the sake of contradiction, suppose this disequality does not hold. Because of (A.7),
there exists σ 00 such that
(σ 00 , ) ∈ Jτ 0 K(σ0 ∗ σ1 ) ∧ JϕKσ 00 = >.

(A.9)

By (A.5), this implies the existence of σ000 , σ100 such that

(σ000 , ) ∈ JΓ ` κ0 Kσ0 ∧ (σ100 , ) ∈ Jλ0 : ΓKσ1 ∧ σ 00 = σ000 ∗ σ100 .

We split cases based on the relationships among κ, κ0 , λ and λ0 .
(1) If κ = κ0 ϕ and λ = λ0 , then ϕ = (t, c) for some t, c. By (A.1), JΓ ` ϕKσ000 6= >, so that
fct (σ000 ) 6= >. Hence, by the Strong Locality of fct , fct (σ000 ∗ σ100 ) 6= >, so that JϕK(σ 00 ) 6= >.
But this contradicts (A.9).
(2) If κ = κ0 and λ = λ0 ϕ, then ϕ = (t, c) for some t, c. This case is symmetric to the
previous one.
(3) If κ = κ0 ϕ and λ = λ0 ϕ, then ϕ is a call or a return action. Then, by the definition of
evaluation, JϕKσ 00 = {(σ 00 , ϕ)} =
6 >. This gives the desired contradiction.
The remainder of the proof is again done by a case analysis on the relationships among κ,
κ0 , λ and λ0 . We consider three cases.
1. κ = κ0 ϕ and λ = λ0 . In this case, ϕ = (t, c) for some t, c. As shown in (A.8),
00
0 ∗ σ1 ) 6= >. Pick σ such that

Jτ 0 ϕK(σ

(σ 00 , τ 0 ϕ) ∈ Jτ 0 ϕK(σ0 ∗ σ1 ).

(A.10)

By the definition of the trace evaluation and the induction hypothesis in (A.5), there exist
σ000 , σ100 , κ00 and λ00 such that
(σ 00 , ϕ) ∈ JϕK(σ000 ∗ σ100 ) ∧ (σ000 , κ00 ) ∈ JΓ ` κ0 Kσ0 ∧ (σ100 , λ00 ) ∈ Jλ0 : ΓKσ1 ∧ cover(τ 0 , κ00 , λ00 ).
(A.11)
Then
cover(τ 0 (t, c), κ00 (t, c), λ00 ).

LINEARIZABILITY WITH OWNERSHIP TRANSFER

41

We have JΓ ` (t, c)Kσ000 6= >, because κ = κ0 (t, c) and JΓ ` κKσ0 6= >. Hence fct (σ000 ) 6= >
and, furthermore, σ 00 ∈ fct (σ000 ∗ σ100 ). Hence, by the Strong Locality of fct , there exists σ0000
such that
σ0000 ∈ fct (σ000 ) ∧ σ 00 = σ0000 ∗ σ100 .
This implies
(σ0000 , κ00 (t, c)) ∈ JΓ ` κ0 (t, c)Kσ0 = JΓ ` κKσ0 .
From what we have shown so far, it follows that
Thus,

(σ 00 , τ 0 (t, c)) = (σ0000 ∗ σ100 , τ 0 (t, c)) ∈ JΓ ` κKσ0 ⊗ Jλ : ΓKσ1 .

Jτ K(σ0 ∗ σ1 ) ⊆ {(σ 00 , τ ) ∈ JΓ ` κKσ0 ⊗ Jλ : ΓKσ1 }.
(A.12)
00
00
To show the other inclusion and the (A.3) part of the lemma, consider σ0 , σ1 , κ00 , λ00
such that
(σ000 , κ00 ) ∈ JΓ ` κ0 (t, c)Kσ0 ∧ (σ100 , λ00 ) ∈ Jλ0 : ΓKσ1 ∧ cover(τ 0 (t, c), κ00 , λ00 ).

Then for some κ000 we have

κ00 = κ000 (t, c) ∧ cover(τ 0 , κ000 , λ00 ).
By the definition of the evaluation function, there exists σ0000 such that
(σ0000 , κ000 ) ∈ JΓ ` κ0 Kσ0 ∧ (σ000 , (t, c)) ∈ JΓ ` (t, c)Kσ0000 .

By the induction hypothesis in (A.5) and (A.6),

(σ0000 ∗ σ100 )↓ ∧ (σ0000 ∗ σ100 , τ 0 ) ∈ Jτ 0 K(σ0 ∗ σ1 ).

Now by the Footprint Preservation property of fct , the first conjunct above implies that
(σ000 ∗ σ100 )↓, which proves (A.3). By the Strong Locality of fct ,
(σ000 ∗ σ100 , (t, c)) ∈ J(t, c)K(σ0000 ∗ σ100 ).

From what we have shown above it follows that
Hence,

(σ000 ∗ σ100 , τ 0 (t, c)) ∈ Jτ K(σ0 ∗ σ1 ).
Jτ K(σ0 ∗ σ1 ) ⊇ {(σ 00 , τ ) ∈ JΓ ` κKσ0 ⊗ Jλ : ΓKσ1 }.

(A.13)

2. κ = κ0 and λ = λ0 ϕ. This case is symmetric to the previous one.
3. κ = κ0 ϕ and λ = λ0 ϕ. In this case ϕ is a call to or a return from a method in Γ.
As shown in (A.8), Jτ 0 ϕK(σ0 ∗ σ1 ) 6= >. Pick σ 00 such that (A.10) holds. By the definition
of evaluation and the induction hypothesis in (A.5), there exist σ000 , σ100 , κ00 and λ00 such
that (A.11) holds. But
JΓ ` ϕKσ000 6= > ∧ Jϕ : ΓKσ100 6= >.
Furthermore, σ 00 = σ000 ∗ σ100 . Hence, by Lemma A.1 and the definition of the evaluation,
there exist σ0000 , σ1000 , ϕ0 such that
σ 00 = σ0000 ∗ σ1000 ∧ (σ0000 , ϕ0 ) ∈ JΓ ` ϕKσ000 ∧ (σ1000 , ϕ0 ) ∈ Jϕ : ΓKσ100

This in turn implies that

(σ0000 , κ00 ϕ0 ) ∈ JΓ ` κ0 ϕKσ0 ∧ (σ1000 , λ00 ϕ0 ) ∈ Jλ0 ϕ : ΓKσ1 .

From what we have shown so far, it follows that

(σ 00 , τ 0 ϕ) = (σ0000 ∗ σ1000 , τ 0 ϕ) ∈ JΓ ` κKσ0 ⊗ Jλ : ΓKσ1 .

42

A. GOTSMAN AND H. YANG

Thus, (A.12) holds.
To show the other inclusion and the (A.3) part of the lemma, consider
σ000 , σ100 , σ0000 , σ1000 , κ00 , λ00 , ϕ0
such that
(σ000 , κ00 ) ∈ JΓ ` κ0 Kσ0 ∧ (σ100 , λ00 ) ∈ Jλ0 : ΓKσ1 ∧ (σ0000 , ϕ0 ) ∈ JΓ ` ϕKσ000
∧ (σ1000 , ϕ0 ) ∈ Jϕ : ΓKσ100 ∧ cover(τ 0 ϕ, κ00 ϕ0 , λ00 ϕ0 ).

We need to show that

(σ0000 ∗ σ1000 )↓ ∧ (σ0000 ∗ σ1000 , τ 0 ϕ) ∈ Jτ 0 ϕK(σ0 ∗ σ1 ).

In particular, this establishes (A.13).
Since cover(τ 0 ϕ, κ00 ϕ0 , λ00 ϕ0 ) and ϕ0 is a call to or a return from a method in Γ,
cover(τ 0 , κ00 , λ00 ) ∧ ϕ = ground(ϕ0 ).
We now use the induction hypothesis in (A.5) and (A.6) and derive that
(σ000 ∗ σ100 )↓ ∧ (σ000 ∗ σ100 , τ 0 ) ∈ Jτ 0 K(σ0 ∗ σ1 ).

But JΓ ` ϕKσ000 6= > and Jϕ : ΓKσ100 6= >. Hence, by Lemma A.1,
(σ0000 ∗ σ1000 )↓ ∧ (σ000 ∗ σ100 = σ0000 ∗ σ1000 ).

By the definition of evaluation,
JϕK(σ000 ∗ σ100 ) = {(σ000 ∗ σ100 , ϕ)} = {(σ0000 ∗ σ1000 , ϕ)}.

From what we have shown, it follows that
as required.

(σ0000 ∗ σ1000 , τ 0 ϕ) ∈ Jτ 0 ϕK(σ0 ∗ σ1 ),

The following lemma shows that the trace-set generation of our semantics also satisfies
the decomposition and composition properties.
Lemma A.3. ∀τ. τ ∈ LC(L)M ⇐⇒ (∃κ, λ. κ ∈ LΓ ` C M ∧ λ ∈ LL : ΓM ∧ cover(τ, κ, λ)).

Proof. Let

C = let [−] in C1 k . . . k Cn ; L = {m = Cm | m ∈ {m1 , . . ., mj }}; Cmgc = (m1 + . . . + mj )∗ .
First, consider τ ∈ LC(L)M. By the definition of the semantics, for some trace τ 0 , τ is a
prefix of τ 0 ,
∀t ∈ {1, . . . , n}. τ 0 |t ∈ LCt Mt (λ(m, t). LCm Mt ( ))
0
and all actions in τ are done by some thread t ∈ {1, . . . , n}. Then
∀t ∈ {1, . . . , n}. client(τ 0 |t ) ∈ LCt Mt (λ(m, t). {ε}) ∧ lib(τ 0 |t ) ∈ LCmgc Mt (λ(m, t). LCm Mt ( )).

Since all actions in τ 0 are done by some thread t ∈ {1, . . . , n}, we have

client(τ 0 ) ∈ (client(τ 0 |1 ) k . . . k client(τ 0 |n )) ∧ lib(τ 0 ) ∈ (lib(τ 0 |1 ) k . . . k lib(τ 0 |n )).
Hence,

client(τ 0 ) ∈ LΓ ` C M ∧ lib(τ 0 ) ∈ LL : ΓM.
Since client(τ ) is a prefix of client(τ 0 ) and lib(τ ) is a prefix of lib(τ 0 ), this implies
client(τ ) ∈ LΓ ` C M ∧ lib(τ ) ∈ LL : ΓM.

LINEARIZABILITY WITH OWNERSHIP TRANSFER

43

Furthermore, cover(τ, client(τ ), lib(τ )), as desired.
Assume now that
Then for some traces

κ ∈ LΓ ` C M ∧ λ ∈ LL : ΓM ∧ cover(τ, κ, λ).

κ0

and λ0 , κ is a prefix of κ0 , λ is a prefix of λ0 , and

∀t ∈ {1, . . . , n}. κ0 |t ∈ LCt Mt (λ(m, t). {ε}) ∧ λ0 |t ∈ LCmgc Mt (λ(m, t). LCm Mt ( )).

The definition of our semantics in Figure 5 allows us to choose λ0 in such a way that for
some trace τ 0 , τ is a prefix of τ 0 and cover(τ 0 , κ0 , λ0 ). Then
∀t ∈ {1, . . . , n}. τ 0 |t ∈ LCt Mt (λ(m, t). LCm Mt ( ))

and τ 0 ∈ (τ 0 |1 k . . . k τ 0 |n ). Thus, τ 0 ∈ LC(L)M, which implies τ ∈ LC(L)M, as desired.
Proof of Lemma 5.6. We first show that C(L) is safe for I0 ∗ I1 . Pick states σ0 , σ1 , τ such
that
σ0 ∈ I0 ∧ σ1 ∈ I1 ∧ (σ0 ∗ σ1 )↓ ∧ τ ∈ LC(L)M.
By Lemma A.3, there exist traces κ, λ such that
κ ∈ LΓ ` C M ∧ λ ∈ LL : ΓM ∧ cover(τ, κ, λ).

(A.14)

By our assumptions, Γ ` C and L : Γ are safe for I0 and I1 , respectively. Hence, JΓ ` κKσ0 6=
> and Jλ : ΓKσ1 6= >. By Lemma A.2, these disequalities imply that Jτ K(σ0 ∗ σ1 ) 6= >. We
have just shown the safety of C(L) for I0 ∗ I1 .
Next, we show that
JC(L), I0 ∗ I1 K ⊆ JΓ ` C, I0 K ⊗ JL : Γ, I1 K.

Pick (σ, τ ) ∈ JC(L), I0 ∗ I1 K. Then for some σ0 , σ1 we have

σ0 ∈ I0 ∧ σ1 ∈ I1 ∧ σ = σ0 ∗ σ1 ∧ τ ∈ LC(L)M ∧ ( , τ 0 ) ∈ Jτ K(σ0 ∗ σ1 ).

By Lemma A.3, there are κ, λ such that (A.14) holds. We use Lemma A.2 and deduce that
for some κ0 , λ0 we have
( , κ0 ) ∈ JΓ ` κKσ0 ∧ ( , λ0 ) ∈ Jλ : ΓKσ1 ∧ cover(τ, κ0 , λ0 ).

Furthermore, σ0 ∈ I0 , σ1 ∈ I1 and (σ0 ∗ σ1 )↓. Hence,

(σ, τ ) = (σ0 ∗ σ1 , τ ) ∈ JΓ ` C, I0 K ⊗ JL : Γ, I1 K,

as desired.
Finally, we prove that

JC(L), I0 ∗ I1 K ⊇ JΓ ` C, I0 K ⊗ JL : Γ, I1 K.

Pick (σ, τ ) ∈ JΓ ` C, I0 K ⊗ JL : Γ, I1 K. By the definition of the ⊗ operator and our semantics,
there exist σ0 , σ1 , σ00 , σ10 , κ, λ, κ0 , λ0 such that
σ = σ0 ∗ σ1 ∧ σ0 ∈ I0 ∧ σ1 ∈ I1 ∧ κ ∈ LΓ ` C M ∧ λ ∈ LL : ΓM

∧ (σ00 , κ0 ) ∈ JΓ ` κKσ0 ∧ (σ10 , λ0 ) ∈ Jλ : ΓKσ1 ∧ cover(τ, κ0 , λ0 ).

By the definition of our semantics, κ = ground(κ0 ) and λ = ground(λ0 ). Because of this and
cover(τ, κ0 , λ0 ) we have cover(τ, κ, λ). By Lemma A.3, this implies τ ∈ LC(L)M. Also, by
Lemma A.2, we have that
(σ00 ∗ σ10 )↓ ∧ (σ00 ∗ σ10 , τ ) ∈ Jτ K(σ0 ∗ σ1 ).

44

A. GOTSMAN AND H. YANG

Hence,
as desired.

(σ, τ ) = (σ0 ∗ σ1 , τ ) ∈ JC(L), I0 ∗ I1 K,

A.3. Proof of Lemma 8.3. Consider λ ∈ JL : Γ0 K(σ0 ∗ σ00 ). Then there exist σ1 and
ζ ∈ LLM such that (σ1 , λ) ∈ Jζ : Γ0 K(σ0 ∗ σ00 ). We show that for some σ2 we have
((σ2 , TλUΓ ) ∈ Jζ : ΓKσ0 ) ∧ (σ1 = σ2 ∗ (hVhistory(λ)WΓ iσ00 )).

We proceed by induction on the length of ζ. The base case of ζ = ε is trivial. Assume
that the above holds for some λ, ζ, σ1 , σ2 and consider ϕ, ϕ0 , σ10 such that
ζϕ ∈ LLM ∧ (σ10 , ϕ0 ) ∈ Jϕ : Γ0 Kσ1 ∧ hVhistory(λϕ0 )WΓ iσ00 6= >.

We show that for some σ20 we have

((σ20 , Tλϕ0 UΓ ) ∈ Jζϕ : ΓKσ0 ) ∧ (σ10 = σ20 ∗ (hVhistory(λϕ0 )WΓ iσ00 )).

We consider three cases, depending on the type of the actions ϕ and ϕ0 .
• ϕ = ϕ0 = (t, c). Then history(λϕ0 ) = history(λ). Since L : Γ is safe at σ0 , fct (σ2 ) 6= >.
Hence, by the Strong Locality property, we have
σ10 ∈ fct (σ1 ) = fct (σ2 ∗ (hVhistory(λ)WΓ iσ00 )) =
fct (σ2 ) ∗ {hVhistory(λ)WΓ iσ00 } = fct (σ2 ) ∗ {hVhistory(λϕ0 )WΓ iσ00 }.
Then σ10 = σ20 ∗ (hVhistory(λϕ0 )WΓ iσ00 ) for some σ20 ∈ fct (σ2 ).
0
m
• ϕ = (t, call m) and ϕ0 = (t, call m(σp ∗ σp0 )), where σp ∈ pm
t and σp ∗ σp ∈ rt . Then
σ10 = σ1 ∗ σp ∗ σp0 = (σ2 ∗ σp ) ∗ ((hVhistory(λ)WΓ iσ00 ) ∗ σp0 ) = (σ2 ∗ σp ) ∗ (hVhistory(λϕ0 )WΓ iσ00 ).
Hence, the required holds for σ20 = σ2 ∗ σp .
• ϕ = (t, ret m) and ϕ0 = (t, ret m(σq ∗ σq0 )), where σq ∈ qtm and σq ∗ σq0 ∈ sm
t . Then
σ2 ∗ (hVhistory(λ)WΓ iσ00 ) = σ1 = σ10 ∗ σq ∗ σq0 .
Since L : Γ is safe at σ0 , σ2 = σ20 ∗ σq for some σ20 , so that
σ20 ∗ σq ∗ (hVhistory(λ)WΓ iσ00 ) = σ10 ∗ σq ∗ σq0 .
By the cancellativity of ∗, this entails
σ20 ∗ (hVhistory(λ)WΓ iσ00 ) = σ10 ∗ σq0 .
We also know that hVhistory(λϕ0 )WΓ iσ00 6= >, so that
hVhistory(λϕ0 )WΓ iσ00 = (hVhistory(λ)WΓ iσ00 ) \ σq0
is defined. Hence, σ10 = σ20 ∗ (hVhistory(λϕ0 )WΓ iσ00 ).

LINEARIZABILITY WITH OWNERSHIP TRANSFER

45

A.4. Proof of Lemma 8.4. In the following, we extend the T·UΓ operation to non-interface
actions by assuming that it does not change them.
Consider λ, σ0 , σ00 , σ000 satisfying the conditions of the lemma. Then history(λ) is balanced
from δ(σ000 ∗ σ00 ) for δ(σ0 )  δ(σ000 ), and there exist σ and ζ ∈ LLM such that (σ, TλUΓ ) ∈ Jζ :
ΓKσ0 . We show that
(σ ∗ (hVhistory(λ)WΓ iσ00 ), λ) ∈ Jζ : Γ0 K(σ0 ∗ σ00 )

by induction on the length of ζ. The base case of ζ = ε is trivial. Assume that the above
holds for some λ, σ0 , σ00 , σ000 , σ, ζ and consider ϕ, ϕ0 , σ 0 such that
(ζϕ ∈ LLM) ∧ ((σ 0 , Tϕ0 UΓ ) ∈ Jϕ : ΓKσ) ∧

(history(λϕ0 ) is balanced from δ(σ000 ∗ σ00 ) for δ(σ0 )  δ(σ000 )) ∧ (hVhistory(λϕ0 )WΓ iσ00 6= >).
We show that

(σ 0 ∗ (hVhistory(λϕ0 )WΓ iσ00 ), λϕ0 ) ∈ Jζϕ : Γ0 K(σ0 ∗ σ00 ).
We consider three cases, depending on the type of the actions ϕ and ϕ0 .
• ϕ = ϕ0 = (t, c). Then history(λ) = history(λϕ0 ) and σ 0 ∈ fct (σ). Since
(σ ∗ (hVhistory(λ)WΓ iσ00 ))↓ ,
by the Footprint Preservation property, (σ 0 ∗ (hVhistory(λ)WΓ iσ00 ))↓. Then by the Strong
Locality property,
σ 0 ∗ (hVhistory(λϕ0 )WΓ iσ00 ) = σ 0 ∗ (hVhistory(λ)WΓ iσ00 ) ∈
fct (σ) ∗ {hVhistory(λ)WΓ iσ00 } = fct (σ ∗ (hVhistory(λ)WΓ iσ00 )).
0
m
• ϕ = (t, call m) and ϕ0 = (t, call m(σp ∗ σp0 )), where σp ∈ pm
t and σp ∗ σp ∈ rt . In
0
0
00
0
this case we have σ = σ ∗ σp . Since history(λϕ ) is balanced from δ(σ0 ∗ σ0 ), we have
(σ ∗ (hVhistory(λ)WΓ iσ00 ) ∗ σp ∗ σp0 )↓. Then

σ ∗ (hVhistory(λ)WΓ iσ00 ) ∗ σp ∗ σp0 = σ 0 ∗ ((hVhistory(λ)WΓ iσ00 ) ∗ σp0 ) = σ 0 ∗ hVhistory(λϕ0 )WΓ iσ00 .
• ϕ = (t, ret m) and ϕ0 = (t, ret m(σq ∗σq0 )), where σq ∈ qtm and σq ∗σq0 ∈ sm
t . In this case we
have σ 0 = σ \ σq . We know hVhistory(λϕ0 )WΓ iσ00 6= >. Thus, ((hVhistory(λ)WΓ iσ00 ) \ σq0 )↓.
Since σ ∗ (hVhistory(λ)WΓ iσ00 ) is defined, so is
σ 0 ∗ (hVhistory(λϕ0 )WΓ iσ00 ) = σ 0 ∗ ((hVhistory(λ)WΓ iσ00 ) \ σq0 ) =
(σ \ σq ) ∗ ((hVhistory(λ)WΓ iσ00 ) \ σq0 ) = (σ ∗ (hVhistory(λ)WΓ iσ00 )) \(σq ∗ σq0 ).
Glossary
Symbol

Meaning and section

Σ
∗
e
σ, θ
p, q, r, s
g(x)↓
g(x)↑
g[x : y]

separation algebra, 2.1
operation accompanying a separation algebra, 2.1
unit of a separation algebra, 2.1
state, 2.1
predicate on states, 2.1; parameterised predicate, 4.1
function g is defined on x, 2.1
function g is undefined on x, 2.1
the function that has the same value as g everywhere,

46

A. GOTSMAN AND H. YANG

π
\
l
δ(σ)
F(Σ)
◦
\\

ψ
t
m
H, S
ε
τ (i)
τ k
|τ |
JHK]
H
v
ρ
c
C
L
S
C
P
Γ
>
fct
ϕ
τ
κ
λ, ζ, α, β
lib(τ )
client(τ )
history(τ )
η
L Γ ` P : Γ0 M
JΓ ` P : Γ0 K
JΓ ` τ : Γ0 K
JΓ ` ϕ : Γ0 K
I
JP, IK
ground(τ )
interf(L, I)
∼

except for x, where it has the value y, 2.1
permission, 2.1
subtraction: on states, 2.1; on a state and a predicate, 4.1
footprint, 2.2
footprint of a state σ, 2.2
the set of all footprints in a separation algebra Σ, 2.2
addition operation on footprints, 2.2
subtraction operation on footprints, 2.2
“smaller-than” relation on footprints, 2.2
interface action, 3
thread identifier, 3
library method, 3
history, 3
empty history or trace, 3
the i-th element of τ , 3
the prefix of τ of length k, 3
is the length of τ , 3
footprint tracking function, 3
interface set, 3
linearizability: on histories, 3; interface sets, 3; libraries, 6
bijection on history indices, 3
primitive command, 4
command, 4
library, 4
complete program, 4
open program with a client, 4
open or complete program, 4
method specification, 4.1
error state, 4.2
transformer for a primitive command c and thread identifier t, 4.2
action, 5.1
trace, 5.1
client trace, 5.1
library trace, 5.1
projection of τ to library actions, calls and returns, 5.1
projection of τ to client actions, calls and returns, 5.1
projection of τ to calls and returns, 5.1
mapping from methods to trace sets, 5.2
trace set, 5.2
denotation of a program P, 5.3
evaluation of a trace τ , 5.3
evalutation of an action ϕ, 5.3
set of initial states, 5.4
set of traces of P run from states in I, 5.4
erasure of state annotations from actions in τ , 5.4
interface set of L run from initial states in I, 6
equivalence of client traces, 6

LINEARIZABILITY WITH OWNERSHIP TRANSFER

TλU
VλW
hHi

47

selects state annotations corresponding to unextended specifications, 8
selects state annotations recording extra state, 8
evaluation of a history H recording extra state, 8

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view
a copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a
letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or
Eisenacher Strasse 2, 10777 Berlin, Germany

