Higher-Order Linearisability
Andrzej S. Murawski1 and Nikos Tzevelekos2

arXiv:1610.07965v1 [cs.PL] 25 Oct 2016

1

University of Warwick

2

Queen Mary University of London

Abstract. Linearisability is a central notion for verifying concurrent libraries: a
given library is proven safe if its operational history can be rearranged into a new
sequential one which, in addition, satisfies a given specification. Linearisability
has been examined for libraries in which method arguments and method results
are of ground type, including libraries parameterised with such methods. In this
paper we extend linearisability to the general higher-order setting: methods can
be passed as arguments and returned as values. A library may also depend on
abstract methods of any order. We use this generalised notion to show correctness
of several higher-order example libraries.

1

Introduction

Computer programs often take advantage of libraries, which are collections of routines,
often of specialised nature, implemented to facilitate software development and, among
others, code reuse and modularity. To support the latter, libraries should follow their specifications, which describe the range of expected behaviours the library should conform
to for safe and correct deployment. Adherence to given specifications can be formalised
using the classic notion of contextual approximation (refinement), which scrutinises
the behaviour of code in any possible context. Unfortunately, the quantification makes
it difficult to prove contextual approximations directly, which motivates research into
sound techniques for establishing it.
In the concurrent setting, a notion that has been particularly influential is that of
linearisability [12]. Linearisability requires that, for each history generated by a library,
one should be able to find another history from the specification (its linearisation), which
matches the former up to certain rearrangements of events. In the original formulation by
Herlihy and Wang [12], these permutations were not allowed to disturb the order between
library returns and client calls. Moreover, linearisations were required to be sequential
traces, that is, sequences of method calls immediately followed by their returns. This
notion of linearisability only applies to closed, i.e. fully implemented, libraries in which
both method arguments and results are of ground types. The closedness limitation was
lifted by Cerone, Gotsman and Yang [3], who extended the techniques to parametric
libraries, whereby methods were divided into available routines (public methods) and
unimplemented ones (abstract methods). However, both public and abstract methods
were still restricted to first-order functions of type int → int. In this paper, we make
a further step forward and present linearisability for general higher-order concurrent
libraries, where methods can be of arbitrary higher-order types. In doing so, we also
propose a corresponding notion of sequential history for higher-order histories.
We examine libraries L that can interact with their environments by means of public
and abstract methods: a library L with abstract methods of types Θ = θ1 , ⋯, θn and

public methods Θ′ = θ1′ , ⋯, θn′ ′ is written as L ∶ Θ → Θ′ . We shall work with arbitrary
higher-order types generated from the ground types unit and int. Types in Θ, Θ′ must
always be function types, i.e. their order is at least 1.
A library L may be used in
K
L
L'
computations by placing it in a
PL
context that will keep on calling
Θ
Θ' M1
Θ' PK
Θ
OL
OK
its public methods (via a client
K) as well as providing impleΘ'' MN
Θ''
mentations for the abstract ones
(via a parameter library L′ ). The
′
comprising
setting is depicted in Figure 1. Fig. 1. A library L ∶ Θ′ → Θ in environment
′′
a
parameter
library
L
∶
∅
→
Θ,
Θ
and
a
client
K of the
Note that, as the library L inform Θ′ , Θ′′ ⊢ M1 ∥⋯∥MN .
′
teracts with K and L , they exchange functions between each other. Consequently, in addition to K making calls to
public methods of L and L making calls to its abstract methods, K and L′ may also issue
calls to functions that were passed to them as arguments during higher-order interactions.
Analogously, L may call functions that were communicated to it via library calls.
Our framework is operational in flavour and draws upon concurrent [15,7] and
operational game semantics [13,16,8]. We shall model library use as a game between two
participants: Player (P), corresponding to the library L, and Opponent (O), representing
the environment (L′ , K) in which the library was deployed. Each call will be of the form
call m(v) with the corresponding return of the shape ret m(v), where v is a value. As
we work in a higher-order framework, v may contain functions, which can participate in
subsequent calls and returns. Histories will be sequences of moves, which are calls and
returns paired with thread identifiers. A history is sequential just if every move produced
by O is immediately followed by a move by P in the same thread. In other words, the
library immediately responds to each call or return delivered by the environment. In
contrast to classical linearisability, the move by O and its response by P need not be
a call/return pair, as the higher-order setting provides more possibilities (in particular,
the P response may well be a call). Accordingly, linearisable higher-order histories can
be seen as sequences of atomic segments (linearisation points), starting at environment
moves and ending with corresponding library moves.
In the spirit of [3], we are going to consider two scenarios: one in which K and
L′ share an explicit communication channel (the general case) as well as a situation in
which they can only communicate through the library (the encapsulated case). Further,
in the encapsulated case, we will handle the case in which extra closure assumptions can
be made about the parameter library (the relational case). The restrictions can deal with
a variety of assumptions on the use of parameter libraries that may arise in practice.
In each of the three cases, we shall present a candidate definition of linearisability
and illustrate it with tailored examples. The suitability of each kind of linearisability will
be demonstrated by showing that it implies the relevant form of contextual approximation
(refinement). We shall also examine compositionality of the proposed concepts. One of
our examples will discuss the correctness of an implementation of the flat-combining
approach [11,3], adapted to higher-order types.

2

2

Higher-order linearisability

As mentioned above, we examine libraries interacting with their context by means of
abstract and public methods. In particular, we consider higher-order types given by the
grammar on the left below, and let Meths be a set of method names.
θ ∶∶= unit ∣ int ∣ θ × θ ∣ θ → θ

Meths = ⊎θ,θ′ Methsθ,θ′

v ∶∶= () ∣ i ∣ m ∣ (v, v)

Methods are ranged over my m (and variants), and each set Methsθ,θ′ contains names
for methods of type θ → θ′ . Finally, we let v range over computational values, which
include a unit value, integers, methods, and pairs of values.
The framework of a higher-order library and its environment is depicted in Figure 1.
Given Θ, Θ′ ⊆ Meths, a library L is said to have type Θ → Θ′ if it defines public
methods with names (and types) as in Θ′ , using abstract methods Θ. The environment
of L consists of a client K (which invokes the public methods of Θ′ ), and a parameter
library L′ (which provides the code for the abstract methods Θ). In general, K and L′
may be able to interact via a disjoint set of methods Θ′′ ⊆ Meths, to which L has no
access.
In the rest of this paper we will be implicitly assuming that we work with a library L
operating in an environment presented in Figure 1. The client K will consist of a fixed
number N of concurrent threads. Next we introduce a notion of history tailored to the
setting and define how histories can be linearised. In Section 3 we present the syntax for
libraries and clients; and in Section 4 we define their semantics in terms of histories (and
co-histories).
2.1

Higher-order histories

The operational semantics of libraries will be given in terms of histories, which are
sequences of method calls and returns each decorated with a thread identifier and a
polarity index XY , where X ∈ {O, P } and Y ∈ {L, K}:
(t, call m(v))XY

(t, ret m(v))XY

We refer to decorated calls and returns like above as moves. Here, m is a method name
and v is a value of matching type. The index XY is specifying which of the three entities
(L, L′ , K) produces the move, and towards whom it is addressed.
– If X = P then the move is issued by L. Moreover, if Y = L then it is addressed to
L′ ; otherwise, if Y = K then it is addressed to K.
– If XY = OL then the move is issued by L′ , and is addressed to L.
– If XY = OK then the move is issued by K, and is addressed to L.
We can justify the choice of indices: the moves can be seen as defining a 2-player game
between the library (L), which represents the Proponent player in the game, and its
enviroment (L′ , K) that represents the Opponent. Moves played between L and L′ are
moreover decorated with L; whereas those between L and K have K. Note that the
possible interaction between L′ and K is invisible to L and is therefore not accounted
for in the game (but we will later see how it can affect it). We use O to refer to either
OK or OL, and P to refer to either P K or P L.
3

Definition 1. [Prehistories] We define prehistories as sequences of moves derived by
one of the following grammars,
P
′
O
HO
pre ∶∶=  ∣ call m(v)OY Hpre ret m(v )P Y Hpre
P
O
′
Hpre ∶∶=  ∣ call m(v)P Y Hpre ret m(v )OY HP
pre

where, in each line, the two occurrences of Y ∈ {K, L} and m ∈ Meths must each match.
Moreover, if m ∈ Methsθ,θ′ , the types of v, v ′ must match θ, θ′ respectively.
The elements of HO
pre are patterns of actions starting with an O-move, while those in
start with a P -move. Note that, in each case, the polarities alternate and the polarities
of calls and matching returns always match the pattern (XY, X ′ Y ) for X =/ X ′ .
Histories will be interleavings of prehistories tagged with thread identifiers (natural
O/P
numbers) that satisfy a number of technical conditions. Given h ∈ Hpre and t ∈ N, we
write t × h for h in which each call or return is decorated with t. We refer to such moves
with (t, call m(v))XY or (t, ret m(v))XY respectively. If we only want to stress the X
or Y membership, we shall drop Y or X respectively. Moreover, when no confusion
arises, we may sometimes drop a move’s polarity altogether.
HP
pre

Definition 2. [Histories] Given Θ, Θ′ , the set of histories over Θ → Θ′ is defined by:
HΘ,Θ′ = ⋃N >0 ⋃h1 ,⋯,hN ∈HO (1 × h1 ) ∣ ⋯ ∣ (N × hN )
pre
where (1 × h1 ) ∣ ⋯ ∣ (N × hN ) is the set of all interleavings of (1 × h1 ), ⋯, (N × hN ),
satisfying the following conditions.
1. For any s1 (t, call m(v))XY s2 ∈ HΘ,Θ′ :
– either m ∈ Θ′ and XY = OK, or m ∈ Θ and XY = P L,
– or there is a move (t′ , x′ )X ′ Y in s1 with X ≠ X ′ , such that x′ ∈ {call m′ (v), ret m′ (v)}
and v contains m.
2. For any s1 (t, x)XY s2 ∈ HΘ,Θ′ , where x ∈ {call m(v), ret m(v)} and v includes
some m′ ∈ Meths, m′ must not occur in s1 .
Condition 1 in the definition above requires that any call must refer to Θ or Θ′ , or be
introduced earlier as a higher-order argument or result. If the method is from Θ′ , the call
must be tagged with OK (i.e. issued by K). Dual constraints apply to Θ. If a method
name does not come from Θ or Θ′ , in order for the call (t, call m(v))XY to be valid, m
must be introduced in an earlier action with the same tag Y but with the opposite tag X.
Moreover, as specified by Condition 2, any action involving a higher-order value (i.e.
a method name) in its argument or result must label it with a fresh name, one that has
not been used earlier. This is done to enable the history to refer unambiguously to each
method name encountered during the interaction.
We shall range over HΘ,Θ′ using h, s. The subscripts Θ, Θ′ will often be omitted.
Remark 3. Histories will be used to define the semantics JLK of libraries (cf. Section 4).
In particular, for each library L ∶ Θ → Θ′ , we shall have JLK ⊆ HΘ,Θ′ .

4

1

public count, update;

2
3
4

Lock lock;
F := λx.0;

11
12

5
6

13

count = λi. (! F)i

14

7
8

9
10

15

update = λ(i, g ). upd r( i , g ,(! F)i )

16

upd r = λ(i, g, j ).
let y = | gj | in
lock . acquire ();
let f = !F in
if ( j==fi ) then {
F := λx. if (x==i) then y else fx ;
lock . release (); y }
else { lock. release (); upd r( i ,g, fi ) }

Fig. 2. Multiset library Lmset . [count ∶ int → int, update ∶ int × (int → int) → int]

Example 4. Let Θ = {m ∶ int → int} and Θ′ = {m′ ∶ int → int}. Note that singlethreaded library histories from H∅,Θ′ must have the shape (1, call m′ (i1 ))OK (1, ret m′ (j1 ))P K
⋯ (1, call m′ (ik ))OK (1, ret m′ (jk ))P K . In this case, the definition coincides with [3].
However, in general, our notion of histories is more liberal. For example, the sequence
(1, call m′ (1))OK (1, call m(2))P L (1, call m′ (3))OK (1, ret m′ (4))P K (1, ret m(5))OL
(1, ret m′ (6))P K is in HΘ,Θ′ , even though it is not allowed by Definition 1 of [3]. The
sequence represents a scenario in which the public method m′ is called for the second
time before the first call is answered. In our higher-order setting, this scenario may arise
if the parameter library communicates with the client and the communication includes a
function that can issue a call to the public method m′ .1
Finally, we present a notion of sequential history, which generalises that of [12].
Definition 5. We call a history h ∈ HΘ,Θ′ sequential if it is of the form
h = (t1 , x1 )OY1 (t1 , x′1 )P Y1′ ⋯ (tk , xk )OYk (tk , x′k )P Yk′
seq
for some ti , xi , x′i , Yi , Yi′ . We let HΘ,Θ
′ contain all sequential histories of HΘ,Θ ′ .

Next we consider our first example.
Example 6 (Multiset). Consider a concurrent multiset library Lmset that uses a private
reference for storing the multiset’s characteristic function. The implementation is given
in Figure 2. This is a simplified version of the optimistic set algorithm of [10,19], albeit
extended with a higher-order update method. The method computes the new value for
element i without acquiring a lock on the characteristic function in the hope that when
the lock is acquired the value at i will still be the same and the update can proceed
(otherwise another attempt to update the value has to be made). The use of a single
reference instead of a linked list means that memory safety is no longer problematic, so
we focus on linearisability instead. Note we write ∣j∣ for the absolute value of j.
Our verification goal will be to prove linearisability of Lmset to a specification
seq
Amset ⊆ H∅,Θ
, where Θ = {count, update} (the method upd r is private). Amset certifies
that Lmset correctly implements some integer multiset I whose elements change over
time according to the moves in h. That is, for each history h ∈ Amset there is a multiset I
that is empty at the start of h (i.e. I(i) = 0 for all i) and:2
1
2

By comparison, in [3], each (1, call m(v))P L must be followed by some (1, ret m(v ′ ))OL .
For a multiset I and a natural number i, we write I(i) for the multiplicity of i in I; moreover,
we set I[i ↦ j] to be I with its multiplicity of i set to j.

5

– If I changes value between two consecutive moves in h then the second move is a
P -move. In other words, the client cannot update the elements of I.
– Each call to count on argument i must be immediately followed by a return with
value I(i), and with I remaining unchanged.
– Each call to update on (i, m) must be followed by a call to m on i, with I unchanged.
Then, m must later return with some value j. Assuming at that point the multiset will
have value I ′ , if I(i) = I ′ (i) then the next move is a return of the original update
call, with value j; otherwise, a new call to m on i is produced, and so on.
We formally define the specification next.
○
Let H∅,Θ
contain extended histories over ∅ → Θ, which are histories where each
move is accompanied by a multiset (i.e. the sequence consists of elements of the form
○
(t, x, I)XY ). For each s ∈ H∅,Θ
, we let π1 (s) be the history extracted by projection, i.e.
π1 (s) ∈ H∅,Θ . For each t, we let s ↾ t be the subsequence of s of elements with first
component t. Writing ⊑ for the prefix relation, and dropping the Y index from moves (Y
is always K here), we define Amset = {π1 (s) ∣ s ∈ A○mset } where:
seq
○
A○mset = {s ∈ H∅,Θ
∣ π1 (s) ∈ H∅,Θ
∧ (∀s′ ( , I)P ( , J)O ⊑ s. I = J) ∧ ∀t. s ↾ t ∈ S}

and, for each t, the set of t-indexed histories S is given by the following grammar.
S → 

∣

(t, call cnt(i), I)O (t, ret cnt(I(i)), I)P S

∣

(t, call upd(i, m), I)O Mi,j
I,J (t, ret upd(∣j∣), J[i ↦ ∣j∣])P S

Mi,j
I,J → (t, call m(I(i)), I)P S (t, ret m(j), J)O

(if I(i) = J(i))

i,j
′
′
Mi,j
I,J → (t, call m(I(i)), I)P S (t, ret m(j ), J )O MJ ′ ,J

(if I(i) =/ J ′ (i))

By definition, the histories in Amset are all sequential. The elements of A○mset carry along
the multiset I that is being represented. The conditions on A○mset stipulate that O cannot
change the value of I, while the rest of the conditions above are imposed by the grammar
for S. With the notion of linearisability to be introduced next, it will be possible to show
that JLmset K indeed linearises to Amset (see Section 5.1).
2.2

General linearisability

We begin with a definition of reorderings on histories.
Definition 7. Suppose X, X ′ ∈ {O, P } and X ≠ X ′ . Let ◁XX ′ ⊆ HΘ,Θ′ × HΘ,Θ′ be
the smallest binary relation over HΘ,Θ′ satisfying
s1 (t′ , x′ )X ′ (t, x)s2 ◁XX ′ s1 (t, x)(t′ , x′ )X ′ s2
s1 (t′ , x′ )(t, x)X s2 ◁XX ′ s1 (t, x)X (t′ , x′ )s2
where t ≠ t′ .
Intuitively, two histories h1 , h2 are related by ◁XX ′ if the latter can be obtained from
the former by swapping two adjacent moves from different threads in such a way that,
after the swap, an X-move will occur earlier or an X ′ -move will occur later. Note that,
because of X ≠ X ′ , the relation always applies to pairs of moves of the same polarity.
On the other hand, we cannot have s1 (t, x)X (t′ , x′ )X ′ s2 ◁XX ′ s1 (t′ , x′ )X ′ (t, x)X s2 .
6

Definition 8. [General Linearisability] Given h1 , h2 ∈ HΘ,Θ′ , we say that h1 is linearised by h2 , written h1 ⊑ h2 , if h1 ◁∗P O h2 .
Given libraries L, L′ ∶ Θ → Θ′ and set of sequential histories A ⊆ HΘ,Θ′ we write
L ⊑ A, and say that L can be linearised to A, if for any h ∈ JLK there exists h′ ∈ A such
seq
that h ⊑ h′ . Moreover, we write L ⊑ L′ if L ⊑ JL′ K ∩ HΘ,Θ
′.
Remark 9. The definition above follows the classic definition from [12] and allows us to
(first) express linearisability in terms of a given library L and a sequential specification
A. The definition given in [3], on the other hand, expresses linearisability as a relation
between two libraries. This is catered for at the end of Definition 8. Explicitly, we have
that L ⊑ L′ if for all h ∈ JLK there is some sequential h′ ∈ JL′ K such that h ⊑ h′ .

Example 10. Let Θ = {m ∶ int → int} and Θ′ = {m′ ∶ int → int}. First, consider
h, h1 , h2 ∈ H∅,Θ′ given by:
h = (1, call m(1))OK (1, ret m(2))P K (2, call m(3))OK (2, ret m(4))P K
h1 = (1, call m(1))OK (2, call m(3))OK (1, ret m(2))P K (2, ret m(4))P K
h2 = (2, call m(3))OK (1, call m(1))OK (2, ret m(4))P K (1, ret m(2))P K

The histories are related in the following ways: for any i = 1, 2, we have h ◁∗OP hi and
hi ◁∗P O h. Moreover, h1 ◁∗XX ′ h2 and h2 ◁∗XX ′ h1 for any X ≠ X ′ . Note that we do
not have h ◁∗P O hi or hi ◁∗OP h.
Consider now h3 , h4 ∈ HΘ,Θ′ given respectively by:
h3 = (1, call m(1))OK (1, call m′ (2))P L (1, ret m′ (3))OL (1, ret m(4))P K
(2, call m(5))OK (2, call m′ (6))P L (2, ret m′ (7))OL (2, ret m(8))P K
h4 = (1, call m(1))OK (2, call m(5))OK (1, call m′ (2))P L (1, ret m′ (3))OL
(2, call m′ (6))P L (2, ret m′ (7))OL (2, ret m(8))P K (1, ret m(4))P K
Observe that h3 ◁∗OP h4 (and, thus, h4 ◁∗P O h3 ). However, we do not have h4 ◁∗OP h3
or h3 ◁∗P O h4 .
Regarding linearisability, we can make the following remarks.
– Observe that in histories from H∅,Θ′ , we shall have the following actions: call m′ (i)O
and ret m′ (j)P . Thus, ◁∗P O cannot swap (t, ret m′ (j)) with (t′ , call m′ (i)), as in
the standard definition of linearisability [12].
– When HΘ,Θ′ is considered, the available actions are call m′ (i)O , ret m(j)O and
call m(i)P , ret m′ (j)P . Then ◁∗P O coincides with Definition 2 of [3] for secondorder libraries.
2.3

Encapsulated linearisability

A different notion of linearisability will be applicable in cases where the parameter
library L′ of Figure 1 is encapsulated, that is, the client K can have no direct access to it
(i.e. Θ′′ = ∅). In particular, we shall impose an extra condition on histories in order to
reflect the more restrictive nature of interaction. Specifically, in addition to sequentiality
in every thread, we shall disallow switches between L and K components by O.
7

Definition 11. We call a history h ∈ HΘ,Θ′ encapsulated if, for each thread t, if h =
s1 (t, x)P Y s2 (t, x′ )OY ′ s3 and moves from t are absent from s2 then Y = Y ′ . Moroever,
enc
enc
′
we set HΘ,Θ
′ = {h ∈ HΘ,Θ ′ ∣ h encapsulated} and JLKenc = JLK ∩ HΘ,Θ ′ (if L ∶ Θ → Θ ).
We define the corresponding linearisability notion as follows.

Definition 12. [Enc-linearisability] Let ◇ ⊆ HΘ,Θ′ × HΘ,Θ′ be the smallest binary
relation on HΘ,Θ′ such that
s1 (t, m)Y (t′ , m′ )Y ′ s2

◇

s1 (t′ , m′ )Y ′ (t, m)Y s2

for any Y, Y ′ ∈ {K, L} such that Y ≠ Y ′ and t ≠ t′ .
enc
Given h1 , h2 ∈ HΘ,Θ
′ , we say that h1 is enc-linearised by h2 , and write h1 ⊑enc h2 ,
∗
if h1 (◁P O ∪ ◇) h2 and h2 is sequential.
seq
A library L ∶ Θ → Θ′ can be enc-linearised to A, written L ⊑enc A, if A ⊆ HΘ,Θ
′ ∩
enc
′
′
HΘ,Θ′ and for any h ∈ JLKenc there exists h ∈ A such that h ⊑enc h . Moreover, we write
seq
L ⊑enc L′ if L ⊑enc JL′ Kenc ∩ HΘ,Θ
′.
Remark 13. Recall Θ, Θ′ from Example 10. Note that histories may contain the following actions only: call m′ (i)OK , ret m(i)OL , call m(i)P L , ret m′ (i)P K . Then (◁P O ∪
◇)∗ preserves the order between call m(i)P L and ret m(i)OL as well as that between
ret m′ (i)P K and call m′ (i)OK , i.e. it coincides with Definition 3 of [3].
Example 14 (Parameterised multiset). We revisit the multiset library of Example 6
and extend it with an abstract method foo and a corresponding update method update enc
which performs updates using foo as the value-updating function. In contrast to the update
method of Lmset , the method update enc is not optimistic: it retrieves the lock upon its
call, and only releases it before return. In particular, the method calls foo while it retains
the lock. We call this library Lmult2 ∶ ∅ → Θ′ , with Θ′ = {count, update, update enc}.
Observe that, were foo able to externally call update, we would reach a deadlock: foo
would be keeping the lock while waiting for the return of a method that requires the lock.
On the other hand, if the library is encapsulated then the latter scenario is not plausible.
In such a case, Lmult2 linearises to the specification Amult2 which is defined as follows
(cf. Example 6). Let Amset2 = {π1 (s) ∣ s ∈ A○mset2 } where:
seq
○
′
A○mset2 = {s ∈ H∅,Θ
′ ∣ π1 (s) ∈ H
∅,Θ ′ ∧ (∀s ( , I)P ( , J)O ⊑ s. I = J) ∧ ∀t. s ↾ t ∈ S}

and the set S is now given by the grammar of Example 6 extended with the rule:
S → (t, call upd enc(i), I)OK (t, call foo(i), I)P L (t, ret foo(j), I)OL (t, ret upd enc(∣j∣), I ′ )P K S
with I ′ = I[i ↦ ∣j∣]. Linearisability is shown in Section 5.1.
2.4

Relational linearisability

Finally, we consider a special subcase of the encapsulated case, in which parameter
libraries must satisfy additional constraints, specified through relational closure. This
notion is desirable in cases when unconditional encapsulated linearisability does not hold,
yet one may want to show that it would hold conditionally on the parameter library. The
condition on the parameter library L′ ∶ ∅ → Θ is termed as a relation R ⊆ H∅,Θ × H∅,Θ .
8

1
2
3
4

public count, update, update enc;
abstract foo;
Lock lock;
F := λx.0;

5
6

20
21
22

count = λi. (! F)i

23

update = λ(i, g ). upd r( i , g ,(! F)i )

25

7
8

9
10

24

upd r = λ(i, g, j ).
...
update enc = λi.
lock . acquire ();
let y = | foo ((! F)i )| in
let f = !F in
F := λx. if (x==i) then y else fx ;
lock . release (); y

Fig. 3. Parameterised multiset library Lmset2 . [foo , update enc∶ int → int, lines 10-16 as in Fig. 2]

Definition 15. Given a history h ∈ HΘ,Θ′ and X ∈ {K, L}, we write h ↾ X for the
subsequence of h with moves whose second index is X.
Given a sequence of moves s, we write s for the sequence obtained from s by simply
swapping the O/P indexes in its moves (e.g. xOL yP K zP K = xP L yOK zOK ).
Definition 16. [Relational linearisability] Let R ⊆ H∅,Θ × H∅,Θ be a set closed under
enc
permutations of names in Meths ∖ Θ. Given h1 , h2 ∈ HΘ,Θ
′ , we say that h1 is Rlinearised by h2 , written h1 ⊑R h2 , if h2 is sequential and (h1 ↾K) ◁∗P O (h2 ↾K) and
(h1 ↾ L) R (h2 ↾ L).
seq
enc
Given L ∶ Θ → Θ′ and A ⊆ H∅,Θ
∩ H∅,Θ
, we write L ⊑R A if for any h ∈ JLKenc
seq
′
′
there exists h ∈ A such that h ⊑R h . Moreover, L ⊑R L′ if L ⊑ JL′ Kenc ∩ HΘ,Θ
′.
Note the above permutation-closure requirement: if h R h′ and π is a (type-preserving)
permutation on Meths ∖ Θ then π(h) R π(h′ ). The requirement adheres to the fact that,
apart from the method names from a library interface, the other method names in its
semantics are arbitrary and can be freely permuted without any observable effect. Thus,
R in particular should not be distinguishing between such names.
Our third example extends the flat-combining case study from [3] by lifting it to
higher-order types.
Example 17. Flat combining [11] is a synchronisation paradigm that advocates the use
of single thread holding a global lock to process requests of all other threads. To facilitate
this, threads share an array to which they write the details of their requests and wait either
until they acquire a lock or their request has been processed by another thread. Once a
thread acquires a lock, it executes all requests stored in the array and the outcomes are
written to the shared array for access by the requesting threads.
The authors of [3] analysed a parameterised library that reacts to concurrent requests
by calling the corresponding abstract methods subject to mutual exclusion. In Figure 4,
we present the code adapted to arbitrary higher-order types, which is possible thanks to
the presence of higher-order references in our framework. We assume:
Θ = {mi ∈ Methsθi ,θi′ ∣ 1 ≤ i ≤ k}

Θ′ = {m′i ∈ Methsθi ,θi′ ∣ 1 ≤ i ≤ k}

Thus the setup of [3] corresponds to θi = θi′ = int. The library Lfc is built following
the flat combining approach and, on acquisition of a lock, the winning thread acts as a
combiner of all registered requests. Note that the requests will be attended to one after
9

1
2
3
4

abstract mi ; public m′i ; . . . ;
Lock lock;
struct {op, parm, wait , retv }
requests [N];

7
8
9

12
13
14

5
6

10
11

m′i = λz.
requests [tid ].op := i;
requests [tid ].parm := z;
requests [tid ].wait := 1;

15
16
17
18

while ( requests [tid ].wait)
if ( lock . tryacquire ()) {
for ( t=0; t<N; t++)
if ( requests [ t ]. wait) {
let j = requests [ t ]. op in
requests [ t ]. retv := mj (requests[t].parm);
requests [ t ]. wait := 0
}; lock . release () };
requests [tid ].retv;

Fig. 4. Flat combination library Lfc .

another (thus guaranteeing mutual exclusion) and only one lock acquisition will suffice
to process one array of requests.
In Section 5.2, we shall show that Lfc can be R-linearised to the specification given
by the sequential histories of the library Lspec that implements m′i as follows:
6

m′i = λz. ( lock.acquire(); let result = mi (z) in lock.release(); result )
Thus, each abstract call in Lspec is protected by a lock.

3

Library syntax

We now look at the concrete syntax of libraries and clients. Libraries comprise collections
of typed methods. The order3 of their argument and result types is unrestricted and will
adhere to the grammar: θ ∶∶= unit ∣ int ∣ θ → θ ∣ θ × θ.
We shall use three disjoint enumerable sets of names, referred to as Vars, Meths and
Refs, to name respectively variables, methods and references. x, f (and their decorated
variants) will be used to range over Vars; m will range over Meths and r over Refs.
Methods and references are implicitly typed, that is, we assume
Meths = ⊎θ,θ′ Methsθ,θ′

Refs = Refsint ⊎ ⊎θ,θ′ Refsθ,θ′

where Methsθ,θ′ contains names for methods of type θ → θ′ , Refsint contains names of
integer references and Refsθ,θ′ contains names for references to methods of type θ → θ′ .
We write ⊎ to stress the disjointness of sets in their union.
The syntax for building libraries is defined in Figure 5. Thus, each library L begins
with a series of method declarations (public or abstract) followed by a block B consisting
of method implementations (m = λx.M ) and reference initialisations (r ∶= i or r ∶=
λx.M ). Our typing rules will ensure that each public method must be implemented
within the block, in contrast to abstract methods. On the other hand, a client K consists
of a parallel composition of closed terms.
Terms M specify the shape of allowable method bodies. () is the skip command,
i ranges over integers, tid is the current thread identifier and ⊕ represents standard
arithmetic operations. Thanks to higher-order references, we can simulate divergence
3

Type order is defined by ord(unit) = ord(int) = 0, ord(θ1 × θ2 ) = max(ord(θ1 ), ord(θ2 )),
ord(θ1 → θ2 ) = max(ord(θ1 ) + 1, ord(θ2 )).

10

L ∶∶= B ∣ abstract m; L ∣ public m; L

Libraries

Clients

K ∶∶= M ∥⋯∥ M

Blocks

B ∶∶=  ∣ m = λx.M ; B ∣ r ∶= λx.M ; B ∣ r ∶= i; B

Terms

M ∶∶= () ∣ i ∣ tid ∣ x ∣ m ∣ M ⊕ M ∣ if M then M else M ∣ ⟨M, M ⟩ ∣ π1 M ∣ π2 M
∣ λxθ.M ∣ xM ∣ mM ∣ let x = M in M ∣ r ∶= M ∣ !r

Γ ⊢ () ∶ unit

Γ ⊢ i ∶ int

Γ ⊢ tid ∶ int

Γ ⊢ M ∶ int Γ ⊢ M0 , M1 ∶ θ
Γ ⊢ if M then M1 else M0 ∶ θ

Γ ⊢ !r ∶ θ → θ′

Γ ⊢ M ∶ θ Γ, x ∶ θ ⊢ N ∶ θ′
Γ ⊢ let x = M in N ∶ θ′
m ∈ Methsθ,θ′
⊢B  ∶ ∅

′

Γ ⊢ xM ∶ θ

′

⊢B B ∶ Θ

⊢B B ∶ Θ
Meths(B) ⊢L B ∶ ∅ → Θ
′

m ∉ Θ′′

Θ ⊢L abstract m; L ∶ Θ ⊎ {m} → Θ′′

Γ ⊢ M1 , M2 ∶ int
Γ ⊢ M1 ⊕ M2 ∶ int

Γ ⊢ ⟨M1 , M2 ⟩ ∶ θ1 × θ2
Γ ⊢ πi M ∶ θi (i = 1, 2)

Γ ⊢M ∶θ

⊢B m = λx.M ; B ∶ Θ ⊎ {m}

Θ ⊎ {m} ⊢L L ∶ Θ′ → Θ′′

Γ ⊢ m ∶ θ → θ′

r ∈ Refsθ,θ′ Γ ⊢ M ∶ θ → θ′
Γ ⊢ r ∶= M ∶ unit

Γ (x) = θ → θ

x ∶ θ ⊢ M ∶ θ′

r ∈ Refsint ⊢B B ∶ Θ
⊢B r ∶= i; B ∶ Θ

m ∈ Methsθ,θ′

Γ ⊢ Mi ∶ θi (i = 1, 2)
Γ ⊢ ⟨M1 , M2 ⟩ ∶ θ1 × θ2

r ∈ Refsθ,θ′

r ∈ Refsint Γ ⊢ M ∶ int
Γ ⊢ r ∶= M ∶ unit

Γ (x) = θ
Γ ⊢x∶θ

m ∈ Methsθ,θ′

r ∈ Refsint
Γ ⊢ !r ∶ int

Γ, x ∶ θ ⊢ M ∶ θ′
Γ ⊢ λxθ.M ∶ θ → θ′
Γ ⊢M ∶θ

Γ ⊢ mM ∶ θ′
r ∈ Refsθ,θ′ x ∶ θ ⊢ M ∶ θ′ ⊢B B ∶ Θ
⊢B r ∶= λx.M ; B ∶ Θ
Θ ⊎ {m} ⊢L L ∶ Θ′ → Θ′′

m ∈ Θ′′

′

Θ ⊢L public m; L ∶ Θ → Θ′′

Meths(Mj ) ⊆ Θ ⊢ Mj ∶ unit (j = 1, ⋯, N )
Θ ⊢K M1 ∥⋯∥MN ∶ unit

Fig. 5. Library syntax and typing rules for terms (⊢), blocks (⊢B ), libraries (⊢L ), clients (⊢K ).

by (!r)(), where r ∈ Refsunit,unit is initialised with λxunit .(!r)(). Similarly, after r ∶=
λxunit .let y = M in (if y then (N ; (!r)()) else ()), while M N can be simulated by
(!r)(). We shall also use the standard derived syntax for sequential composition, i.e.
M ; N stands for let x = N in M , where x does not occur in M .
Remark 18. In Section 2 we used lock-related operations in our example libraries
(acquire, tryacquire, release), on the understanding that they can be coded using shared
memory. Similarly, the array of Example 17 can be constructed using references.
For each term M , we write Meths(M ) for the set of method names occurring in
M . We also use the same notation for method names in blocks and libraries. Terms are
typed in environments Γ = {x1 ∶ θ1 , ⋯, xn ∶ θn } assigning types to their free variables.
Method blocks are typed through judgements ⊢B B ∶ Θ, where Θ ⊆ Meths. The
judgments collect the names of methods defined in a block as well as making sure that
the definitions respect types and are not duplicated. Also, any initialisation statements
will be scrutinised for type compliance.
Finally, we type libraries using statements of the form Θ ⊢L L ∶ Θ′ → Θ′′ , where
Θ, Θ′ , Θ′′ ⊆ Meths and Θ′ ∩ Θ′′ = ∅. The judgment ∅ ⊢L L ∶ Θ′ → Θ′′ guarantees that
any method occurring in L is present either in Θ′ or Θ′′ , that all methods in Θ′ have been
declared as abstract and not implemented, while all methods in Θ′′ have been declared
11

as public and defined. Thus, ∅ ⊢L L ∶ Θ → Θ′ stands for a library in which Θ, Θ′ are the
abstract and public methods respectively. In this case, we also write L ∶ Θ → Θ′ .
Remark 19. For simplicity, we do not include private methods but the same effect could
be achieved by storing them in higher-order references. As we explain in the next section,
references present in library definitions are de facto private to the library.
Note also that, according to our definition, sets of abstract and public methods are
disjoint. However, given m, m′ ∈ Refsθ,θ′ , one can define a “public abstract” method
with: public m; abstract m′ ; m = λxθ .m′ x .

4

Semantics

The semantics of our system will be given in several stages. First, we define an operational semantics for sequential and concurrent terms that may draw methods from a
function repository. We then adapt it to capture interactions of concurrent clients with
libraries that do not feature abstract methods. The extended notion is then used to define
contextual approximation (refinement) for arbitrary libraries. Subsequently, we introduce
a trace semantics of arbitrary libraries that will be used to define higher-order notions of
linearisability and, ultimately, to relate them to contextual refinement.
4.1

Library-client evaluation

Libraries, terms and clients are evaluated in environments comprising:
– A method environment R, called own-method repository, which is a finite partial
map on Meths assigning to each m in its domain, with m ∈ Methsθ,θ′ , a term of the
form λy.M (we omit type-superscripts from bound variables for economy).
– A finite partial map S ∶ Refs ⇀ (Z ∪ Meths), called store, which assigns to each r in
its domain an integer (if r ∈ Refsint ) or name from Methsθ,θ′ (if r ∈ Refsθ,θ′ ).
The evaluation rules are presented in Figure 6.
Remark 20. We shall assume that reference names used in libraries are library-private,
i.e. sets of reference names used in different libraries are assumed to be disjoint. Similarly,
when libraries are being used by client code, this is done on the understanding that the
references available to that code do not overlap with those used by libraries. Still, for
simplicity, we shall rely on a single set Refs of references in our operational rules.
First we evaluate the library to create an initial repository and store. This is achieved
by the first set of rules in Figure 6, where we assume that Sinit is empty. Note that m in
the last rule is any fresh method name of the appropriate type. Thus, library evaluation
produces a tuple (, R0 , S0 ) including a method repository and a store, which can
be used as the initial repository and store for evaluating M1 ∥⋯∥MN using the (KN )
rule. We shall call the latter evaluation semantics for clients (denoted by Ô
Ô⇒) the
multi-threaded operational semantics.
Reduction rules rely on evaluation contexts E, defined along with values v in the
third group in Figure 6. Finally, rules for closed-term reduction (Ð
→t ) are given in the last
group, where t is the current thread index. Note that the rule for E[λx.M ] involves the
creation of a new method name m, which is used to put the function in the repository R.
We define termination for clients linked with libraries that have no abstract methods.
12

(L) Ð→lib (L, ∅, Sinit )

(r ∶= i; B, R, S) Ð→lib (B, R, S[r ↦ i])

(abstract m; L, R, S) Ð→lib (L, R, S)

(m = λx.M ; B , R, S) Ð→lib (B, R ⊎ (m ↦ λx.M ), S)

(public m; L, R, S) Ð→lib (L, R, S)

(r ∶= λx.M ; B, R, S) Ð→lib (B, R ⊎ (m ↦ λx.M ), S∗ )

(M, R, S) Ð
→t (M ′ , R′ , S ′ )
(M1 ∥⋯∥Mt−1 ∥M ∥Mt+1 ∥⋯∥MN , R, S) Ô
Ô⇒ (M1 ∥⋯∥Mt−1 ∥M ′ ∥Mt+1 ∥⋯∥MN , R′ , S ′ )

(KN )

E ∶∶= ● ∣ E ⊕ M ∣ i ⊕ E ∣ if E then M else M ∣ πj E ∣ ⟨E, M ⟩ ∣ ⟨v, E⟩ ∣ mE ∣ let x = E in M ∣ r ∶= E
v ∶∶= () ∣ i ∣ m ∣ ⟨v, v⟩

(Evaluation Contexts and Values)

(E[tid ], R, S) Ð
→t (E[t], R, S)

(E[i1 ⊕ i2 ], R, S) Ð
→t (E[i], R, S)

(E[!r], R, S) Ð
→t (E[S(r)], R, S)

(E[if 0 then M1 else M0 ], R, S) Ð
→t (E[M0 ], R, S)

(i = i1 ⊕ i2 )

(E[r ∶= v], R, S) Ð
→t (E[()], R, S∗∗ )

(E[if i∗ then M1 else M0 ], R, S) Ð
→t (E[M1 ], R, S)

(E[λx.M ], R, S) Ð
→t (E[m], R∗ , S)

(E[mv], R∗∗ , S) Ð
→t (E[M {v/x}], R∗∗ , S)

(E[πj ⟨v1 ,v2 ⟩], R, S) Ð
→t (E[vj ], R, S)

(E[let x = v in M ], R, S) Ð
→t (E[M {v/x}], R, S)

Fig. 6. Evaluation rules for libraries (Ð→lib ), clients (Ô
Ô⇒), and terms (Ð
→t ). Here, S∗ = S[r ↦ m],
S∗∗ = S[r ↦ v], R∗ = R ⊎ (m ↦ λx.M ); and i∗ ≠ 0, R∗∗ (m) = λx.M .

Definition 21. Let L ∶ ∅ → Θ′ and Θ′ ⊢K M1 ∥⋯∥MN ∶ unit.4 We say that M1 ∥⋯∥MN
terminates with linked library L if
(M1 ∥⋯∥MN , R0 , S0 ) Ô
Ô⇒∗ (()∥⋯∥(), R, S)
for some R, S, where (L) Ð→∗lib (, R0 , S0 ). Then we write link L in (M1 ∥⋯∥MN ) ⇓.
We shall build a notion of contextual approximation of libraries on top of termination:
one library will be said to approximate another if, whenever the former terminates when
composed with any parameter library and client, so does the latter.
There are several ways of composing libraries. Here we will be considering the
notions of union and sequencing. The latter is derived from the former with the aid of
a third construct, called hiding. Below, we denote a library L as L = D; B, where D
contains all the (public/abstract) method declarations of L, and B is its method block.
Definition 22. [Library union, hiding, sequencing] Let L1 ∶ Θ1 → Θ2 be a library of
the form D1 ; B1 .
– Given library L2 ∶ Θ1′ → Θ2′ (= D2 ; B2 ) which accesses disjoint parts of the store
from L1 and such that Θ2 ∩ Θ2′ = ∅, we define the union of L1 and L2 as:
L1 ∪L2 ∶ (Θ1 ∪Θ1′ )∖(Θ2 ∪Θ2′ ) → Θ2 ∪Θ2′ = (D1 ; B1 )∪(D2 ; B2 ) = D1′ ; D2′ ; B1 ; B2
where D1′ is D1 with any “abstract m” declaration removed for m ∈ Θ2′ ; dually for D2′ .
4

Recall our convention (Remark 20) that L and M1 , ⋯, MN must access disjoint parts of the
store. Terms M1 , ⋯, MN can share reference names, though.

13

– Given some Θ = {m1 , ⋯, mn } ⊆ Θ2 , we define the Θ-hiding of L1 as:
L1 ∖ Θ ∶ Θ1 → (Θ2 ∖ Θ) = (D1 ; B1 ) ∖ Θ = D1′ ; B1′ {!r1 /m1 }⋯{!rn /mn }
where D1′ is D1 without public m declarations for m ∈ Θ and, for each i, ri is a
fresh reference matching the type of mi , and B1′ is obtained from B1 by replacing
each definition mi = λx.M by ri ∶= λx.M .
The sequencing of L′ ∶ ∅ → Θ1 , Θ′ with L1 is: L′ ; L1 ∶ ∅ → Θ2 , Θ′ = (L′ ∪ L1 ) ∖ Θ1 .
Thus, the union of two libraries L1 and L2 as above corresponds to merging their
code and removing any abstract method declarations for methods defined in the union.
On the other hand, the hiding of a public method simply renders it private via the use of
references. These notions are used in defining contextual notions for libraries, that is,
notions that require quantification over all possible contexts.
Definition 23. Given L1 , L2 ∶ Θ → Θ′ , we say that L1 contextually approximates
L2 , written L1 ⊏∼ L2 , if for all L′ ∶ ∅ → Θ, Θ′′ and Θ′ , Θ′′ ⊢K M1 ∥⋯∥MN ∶ unit, if
link L′ ; L1 in (M1 ∥⋯∥MN ) ⇓ then link L′ ; L2 in (M1 ∥⋯∥MN ) ⇓. In this case, we also
say that L2 contextually refines L1 .
Note that, according to this definition, the parameter library L′ may communicate
directly with the client terms through a common interface Θ′′ . We shall refer to this case
as the general case. Later on, we shall also consider more restrictive testing scenarios
in which this possibility of explicit communication is removed. Moreover, from the
disjointness conditions in the definitions of sequencing and linking we have that Li , L′
and M1 ∥⋯∥MN access pairwise disjoint parts of the store.
Remark 24. Our definition of contextual approximation models communication between
the client and the parameter library explicitly through the shared interface Θ′′ . This is
different in style (but not in substance) from [3], where the presence of public abstract
methods inside the tested library provides such a communication channel.
4.2

Trace semantics

Building on the earlier operational semantics, we next introduce a trace semantics of
libraries, in the spirit of game semantics [1]. As mentioned in Section 2, the behaviour
of a library will be represented as an exchange of moves between two players called O
and P , representing the library (P ) and the corresponding context (O) respectively. The
context consists of the client of the library as well as the parameter library, with an index
on each move specifying which of them is involved in the move (K or L respectively).
In contrast to the semantics of the previous section, we will handle scenarios in
which methods need not be present in the repository R. Calls to such undefined methods
will be represented by labelled transitions – calls to the context made on behalf of the
library (P ). The calls can later be responded to with labelled transitions corresponding
to returns, made by the context (O). On the other hand, O will be able to invoke methods
in R, which will also be represented through suitable labels. Because we work in a
higher-order setting, calls and returns made by both players may involve methods as
arguments or results. Such methods also become available for future calls: function
14

arguments/results supplied by P are added to the repository and can later be invoked by
O, while function arguments/results provided by O can be queried in the same way as
abstract methods.
After giving semantics to libraries, we shall also define a semantics for contexts, i.e.
clients paired with parameter libraries where the main library is missing. More precisely,
given a parameter library L′ ∶ ∅ → Θ, Θ′ and client Θ′ , Θ′′ ⊢K M1 ∥⋯∥MN ∶ unit, we
will define the semantics of M1 ∥⋯∥MN when paired with L′ . In such a scenario, the
roles of O and P will be reversed: P K will own moves played by the client, P L will be
the parameter library, while O will correspond to the missing main library (OK when
interacting with the client, and OL when talking to the parameter library).
Recall the notions of history (Def. 2) and history complementation (Def. 15). We
next define a dual notion of history that is used for assigning semantics to contexts.
co
Definition 25. The set of co-histories over Θ → Θ′ is: HΘ,Θ
′ = {h ∣ h ∈ HΘ,Θ ′ }.
co
We shall range over HΘ,Θ
′ again using variables h, s. We can show the following.
co
Lemma 26. – For all h ∈ HΘ,Θ′ we have h ↾ L ∈ H∅,Θ
and h ↾ K ∈ H∅,Θ′ .
co
co
– For all h ∈ HΘ,Θ′ we have h ↾ L ∈ H∅,Θ and h ↾ K ∈ H∅,Θ
′.

The trace semantics will utilise configurations that carry more components than the
previous semantics, in order to compensate for the fact that we need to keep track of the
evaluation history that is currently processed, as well as the method names that have
been passed between O and P . We define two kinds of configurations:
O-configurations (E, −, R, P, A, S) and P-configurations (E, M, R, P, A, S) ,
where the component E is an evaluation stack, that is, a stack of the form [X1 , X2 , ⋯, Xn ]
with each Xi being either an evaluation context or a method name. On the other
hand, P = (PL , PK ) with PL , PK ⊆ dom(R) being sets of public method names,
and A = (AL , AK ) is a pair of sets of abstract method names. P will be used to record
all the method names produced by P and passed to O: those passed to OK are stored
in PK , while those leaked to OL are kept in PL . Inside A, the story is the opposite
one: AK (AL ) stores the method names produced by OK (resp. OL) and passed to P .
Consequently, the sets of names stored in PL , Pk , AL , Ak will always be disjoint.
Given a pair P as above and a set Z ⊆ Meths, we write P ∪K Z for the pair
(PL , PK ∪ Z). We define ∪L in a similar manner, and extend it to pairs A as well.
Moreover, given P and A, we let φ(P, A) be the set of fresh method names for P, A:
φ(P, A) = Meths ∖ (PL ∪ PK ∪ AL ∪ AK ).
We next give the rules generating the trace semantics. Note that the rules are parameterised by Y ∈ {K, L}. This parameter will play a role in our treatment of the
encapsulated case, as it allows us to track the labels related to interactions with the client
and the parameter library respectively. In all of the rules below, whenever we write m(v)
or m(v ′ ), we assume that the type of v matches the argument type of m.
Internal rule First we embed the internal rules, introduced earlier: if (M, R, S) Ð
→t
(M ′ , R′ , S ′ ) and dom(R′ ∖ R) consists of names that do not occur in E, A, we have:
(E, M, R, P, A, S) Ð
→t (E, M ′ , R′ , P, A, S ′ )

(I NT)

This includes internal method calls (i.e. (E[mv], R, S) Ð
→t ⋯ with m ∈ dom(R) ).
15

P calls In the next family of rules, the library (P ) calls one of its abstract methods
(either the original ones or those acquired via interaction). Thus, the rule applies to m ∈ AY .
call m(v ′ )P Y

(E, E[mv], R, P, A, S) ÐÐÐÐÐÐÐ→t (m ∶∶ E ∶∶ E, −, R′ , P ′ , A, S)

(PQ Y)

If v does not contain any method names then v ′ = v, R′ = R, P ′ = P. Otherwise, if v
contains the (pairwise distinct) names m1 , ⋯, mk , a fresh name m′i ∈ φ(P, A) is created
for each method name mi (for future reference to the method), and replaced for mi in v.
That is, v ′ = v{m′i /mi ∣ 1 ≤ i ≤ k}. We must also have that the m′i ’s are pairwise distinct
(the rule fires for any such m′i ’s), and also R′ = R ⊎ {m′i ↦ λx.mi x ∣ 1 ≤ i ≤ k} and
P ′ = P ∪Y {m′1 , ⋯, m′k }.
P returns Analogously, the library (P ) may return a result to an earlier call made
by the context. This rule is applicable provided m ∈ PY .
ret m(v ′ )P Y

(m ∶∶ E, v, R, P, A, S) ÐÐÐÐÐÐ→t (E, −, R′ , P ′ , A, S)

(PAY)

v ′ , R′ , P ′ are subject to the same constraints as in (PQ Y ).
O calls The remaining rules are dual and represent actions of the context. Here the
context calls a public method: either an original one or one that has been made public
later (by virtue of having been passed to the context by the library). Here we require
m ∈ PY and R(m) = λx.M .
call m(v)OY

(E, −, R, P, A, S) ÐÐÐÐÐÐ→t (m ∶∶ E, M {v/x}, R, P, A′ , S)

(OQ Y)

If v contains the names m1 , ⋯, mk ∈ Meths, it must be the case that mi ∈ φ(P, A), for
each i, and A′ = A ∪Y {m1 , ⋯, mk }.
O returns Finally, we have rules corresponding to values being returned by the
context in response to calls made by the library. In this case we insist on m ∈ AY .
ret m(v)OY

(m ∶∶ E ∶∶ E, −, R, P, A, S) ÐÐÐÐÐÐ→t (E, E[v], R, P, A′ , S)

(OAY)

As in the previous case, if m ∈ Meths is present in v then we need m ∈ φ(P, A) and A′
is calculated in the same way.
Finally, we extend the trace semantics to a concurrent setting where a fixed number
of N -many threads run in parallel. Each thread has separate evaluation stack and term
components, which we write as C = (E, X) (where X is a term or “−”). Thus, a
configuration now is of the following form, and we call it an N -configuration:
(C1 ∥⋯∥CN , R, P, A, S)
where, for each i, Ci = (Ei , Xi ) and (Ei , Xi , R, P, A, S) is a sequential configuration.
We shall abuse notation a little and write (Ci , R, P, A, S) for (Ei , Xi , R, P, A, S). Also,
⃗ ↦ C ′ ] = C1 ∥⋯∥Ci−1 ∥C ′ ∥Ci+1 ∥⋯∥CN .
below we write C⃗ for C1 ∥⋯∥CN and C[i

16

The concurrent traces are produced by the following two rules with the proviso that
⃗
the names freshly produced internally in (PI NT ) are fresh for the whole of C.
(Ci , R, P, A, S) Ð
→i (C ′ , R′ , P, A, S ′ )
(PI NT)
⃗ R, P, A, S) Ô
⃗ ↦ C ′ ], R′ , P, A, S ′ )
(C,
Ô⇒ (C[i
xXY

(Ci , R, P, A, S) ÐÐ→i (C ′ , R′ , P ′ , A′ , S ′ )
(i,x)XY
⃗ ↦ C ′ ], R′ , P ′ , A′ , S ′ )
⃗ R, P, A, S) ÔÔÔ⇒
(C[i
(C,

(PE XT)

We can now define the trace semantics of a library L. We call a configuration component
Ci final if it is in one of the following forms:
Ci = ([], −) or Ci = ([], ())
⃗ R, P, A, S) final just if C⃗ =
for O- and P -configurations respectively. We call (C,
C1 ∥⋯∥CN and each Ci is final.
Definition 27. For each L ∶ Θ → Θ′ , we define the N -trace semantics of L to be:
JLKN = { s ∣ (C⃗0 , R0 , (∅, Θ′ ), (Θ, ∅), S0 ) Ô
Ô⇒∗ ρ ∧ ρ final }
s

where C⃗0 = ([], −)∥⋯∥([], −) and (L) Ð→∗lib (, R0 , S0 ).

For economy, in the sequel we might be dropping the index N from JLKN .
We conclude this section by providing a semantics for library contexts. Recall that
in the definition of contextual approximation the library L ∶ Θ → Θ′ is deployed in a
context consisting of a parameter library L′ ∶ ∅ → Θ, Θ′′ and a concurrent composition
of client threads Θ′ , Θ′′ ⊢ Mi ∶ unit (i = 1, ⋯, N ). This context makes internal use of
methods defined in the parameter library, while it recurs to the trace system for the
methods in Θ′ . At the same time, the context provides the methods in Θ in the trace
system. We shall write link L′ ; − in (M1 ∥⋯∥MN ), or simply C, to refer to such contexts.
We give the following semantics to contexts.
Definition 28. Let Θ′ , Θ′′ ⊢K M1 ∥⋯∥MN ∶ unit and L′ ∶ ∅ → Θ, Θ′′ . We define the
semantics of the context formed by L′ and M1 , ⋯, MN to be:
Jlink L′ ; − in (M1 ∥⋯∥MN )K = { s ∣ (C⃗0 , R0 , (Θ, ∅), (∅, Θ′ ), S0 ) Ô
Ô⇒∗ ρ ∧ ρ final }
s

where (L′ ) Ð→∗lib (, R0 , S0 ) and C⃗0 = ([], M1 )∥⋯∥([], MN ).

Lemma 29. For any L ∶ Θ → Θ′ , L′ ∶ ∅ → Θ, Θ′′ and Θ′ , Θ′′ ⊢K M1 ∥⋯∥MN ∶ unit
co
we have JLKN ⊆ HΘ,Θ′ and Jlink L′ ; − in (M1 ∥⋯∥MN )K ⊆ HΘ,Θ
′.
Proof. The relevant sequences of moves are clearly alternating and well-bracketed, when
projected on single threads, because the LTS is bipartite (O- and P -configurations) and
separate evaluation stacks control the evolution in each thread. Other conditions for histories follow from the partitioning of names into AK , AL , PK , PL and suitable initialisation: Θ, Θ′ are inserted into AL , PK respectively (for JLK) and into PL , AK for JCK.
17

5

Examples

We now revisit the example libraries from Section 2 and show they each linearise to their
respective specification, according to the relevant notion of linearisability (general/encapsulated/relational).
5.1

Multiset examples

Recall the multiset library Lmset and the specification Amset of Example 6 and Figure 2.
We show that Lmset ⊑ Amset . More precisely, taking an arbitrary history h ∈ JLmset K we
show that h can be rearranged using ◁∗P O to match an element of Amset . We achieve
this by identifying, for each O-move (t, x)O and its following P -move (t, x′ )P in h, a
linearisation point between them, i.e. a place in h to which (t, x)O can moved right and
to which (t, x′ )P can be moved left so that they become consecutive and, moreover, the
resulting history is still produced by Lmset . After all these rearrangements, we obtain a
sequential history ĥ such that h ⊑ ĥ and ĥ is also produced by Lmset . It then suffices to
show that ĥ ∈ Amset .
Lemma 30 (Multiset). Lmset linearises to Amset .
Proof. Taking an arbitrary h ∈ JLmset K, we demonstrate the linearisation points for
pairs of (O, P ) moves in h, by case analysis on the moves (we drop K indices from
moves as they are ubiquitous). Let us assume that h has been generated by a sequence
ρ1 ⇒ ρ2 ⇒ ⋯ ⇒ ρk of atomic transitions and that the variable F of Lmset is instantiated
with the reference rF . Line numbers used below will refer to Figure 2.
1. h = ⋯ (t, call cnt(i))O s (t, ret cnt(j))P ⋯ . Here the linearisation point is the configuration ρi that dereferences rF as per line 6 in Lmset (the !F expression).
2. h = ⋯ (t, call upd(i, m))O s (t, call m(j))P ⋯ . The linearisation point is the dereferencing of rF in line 8.
3. h = ⋯ (t, ret m(j ′ ))O s (t, ret upd(∣j ′ ∣))P ⋯ . The linearisation point is the update
to rF in line 14.
4. h = ⋯ (t, ret m(j ′ ))O s (t, call m(j ′′ ))P ⋯ . The linearisation point is the dereferencing of rF in line 12.
Each of the linearisation points above specifies a P O-rearrangement of moves. For
instance, for h = s0 (t, call cnt(i))O s (t, ret cnt(j))P s′ , let s = s1 s2 where s0 s1 is the
prefix of h produced by ρ1 ⇒ ρ2 ⇒ ⋯ ⇒ ρi . The rearrangement of h is then the history
ĥ = s0 s1 (t, call upd(i, m))O (t, call m(j))P s2 s′ . We thus obtain h ◁∗P O ĥ.
The selection of linearisation points is such that it guarantees that ĥ ∈ JLmset K. E.g.
in case 1, the transitions occurring in thread t between the configuration that follows
(t, call cnt(i))O and ρi do not access rF . Hence, we can postpone them and fire them in
sequence just ρi . After ρi+1 and until (t, ret cnt(j))P there is again no access of rF in
t and we can thus bring forward the corresponding transitions just after ρi+1 . Similar
reasoning applies to case 2. In case 4, we reason similarly but also take into account that
rendering the acquisition of the lock by t atomic is sound (i.e. the semantics can produce
the rearranged history). Case 3 is similar, but we also use the fact that the access to rF in
lines 11-16 is inside the lock, and hence postponing dereferencing (line 12) to occur in
sequence before update (line 14) is sound.

18

Now, any transition sequence α which produces ĥ (in JLmult K) can be used to derive
an extended history h○ ∈ A○mult , by attaching to each move in ĥ the multiset represented
x
in the configuration that produces the move (ρ produces the move x if ρ Ô
Ô⇒ ρ′ in α).
By projection we then obtain ĥ ∈ Amult .
On the other hand, the multiset library of Example 14 and Figure 3 requires encapsulation in order to linearise (cf. Example 14).
Lemma 31 (Parameterised multiset). Lmset2 enc-linearises to Amset2 .
Proof. Again, we identify linearisation points, this time for given h ∈ JLmult2 Kenc . For
cases 1-4 as above we reason as in Lemma 30. For upd enc we have the following case.
h = s (t, call upd enc(i))OK s1 (t, call foo(j))P L s2 (t, ret foo(j ′ ))OL s3 (t, ret upd enc(∣j ′ ∣))P K ⋯
Here, we need a linearisation point for all four moves above. We pick this to be the point
corresponding to the update of the multiset reference F on line 24 (Figure 3). We now
transform h to ĥ so that the four moves become consecutive, in two steps:
– Let us write s3 as s3 = s13 s23 , where the split is at the linearisation point. Since the lock
is constantly held by thread t in s2 s13 , there can be no calls or returns to foo in s2 s13 .
Hence, all moves in s2 s13 are in component K and can be transposed with the L-moves
above, using ◇∗ , to obtain h′ = s (t, call upd enc(i))OK s1 s2 s13 (t, call foo(j))P L
(t, ret foo(j ′ ))OL s23 (t, ret upd enc(∣j ′ ∣))P K ⋯
– Next, by P O-rearrangement we obtain ĥ = s s1 s2 s13 (t, call upd enc(i))OK (t, call foo(j))P L
(t, ret foo(j ′ ))OL (t, ret upd enc(∣j ′ ∣))P K s23 ⋯ . Thus, h(◁P O ∪ ◇)∗ ĥ.
To prove that ĥ ∈ Amult2 we work as in Lemma 30, i.e. via showing that ĥ ∈ JLmult2 Kenc .
For the latter, we rely on the fact that the linearisation point was taken at the reference
update point (so that any dereferencings from other threads are preserved), and that the
dereferences of lines 22 and 23 are within the same lock as the update.
5.2

Flat combining

Recall the libraries Lfc and Lspec from Example 17 and Figure 4. We shall investigate
the impact of introducing higher-order types to the flat combining algorithm, which will
lead to several surprising discoveries. First of all, let us observe that, even if θi = θi′ = int,
higher-order interactions of both Lspec and Lfc with a client and parameter library
according to Definition 23 (general case) may lead to deadlock. In this case, a client can
communicate with the parameter library (via Θ′′ ) and, for example, he could supply it
with a function that calls a public method of the library, say, m′i . That function could
then be used to implement mi and, consequently, a client call to m′i would result in lock
acquisition, then a call to mi , which would trigger another call to m′i and an attempt to
acquire the same lock, while mi cannot return (cf. Example 4).
Deadlock can also arise in the encapsulated case (Definition 37) if the library contains
a public method, say m′i , with functional arguments. Then the client can pass a function
that calls m′i as an argument to m′i and, if the abstract method mi subsequently calls the
argument, deadlock would follow in the same way as before. Correspondingly, in these
cases there exist sequences of transitions induced by our transition system that cannot

19

be extended to a history, e.g. for θi = unit → unit this happens after (1, call m′ (v))OK
(1, call m(v ′ )P L ) (1, call v ′ ())OL (1, call v())P K (1, call m′ (v ′′ ))OK . Consequently,
the protocol should not really be used in an unrestricted higher-order setting.
However, the phenomenon described above cannot be replicated in the encapsulated
case provided the argument types are ground (θi = unit, int). In this case, without
imposing any restrictions on the result types θi′ , we shall show that Lfc ⊑R Lspec , where
R stands for thread-name invariance. Note that this is a proper extension of the result
in [3], where θi′ had to be equal to unit or int. It is really necessary to use the finer
notion of ⊑R here, as we do not have Lfc ⊑enc Lspec (a parameter library that is sensitive
to thread identifiers may return results that allow one to detect that a request has been
handled by a combiner thread which is different from the original one).
Lemma 32 (Flat combining). Let Θ = {mi ∈ Methsint,θi′ ∣ 1 ≤ i ≤ k} and Θ′ = {m′i ∈
Methsint,θi′ ∣ 1 ≤ i ≤ k} be such that Θ ∩ Θ′ = ∅. Let R consist of pairs (h1 , h2 ) ∈
H∅,Θ × H∅,Θ that are identical once thread identifiers are ignored. Then Lfc ⊑R Lspec .
Proof. Observe that histories from JLspec Kenc feature threads built from segments of one
of the three forms (we suppress integer arguments for economy):
– (t, call m′i )OK (t, call mi )P L (t, ret mi (v))OL (t, ret m′i (v ′ ))P K , or
– (t′ , call w(v))OY (t′ , call w′ (v ′ ))P Y ′ for Y ≠ Y ′ , where w is a name introduced in
an earlier move (t′′ , x)P Y and w′ is a corresponding name introduced by the move
preceding (t′′ , x)P Y , or
– (t′ , ret w′ (v ′′ ))OY ′ (t′ , ret w(v ′′′ ))P Y such that a segment (t′ , call w(v))OY (t′ , call w′ (v ′ ))P Y ′
already occurred earlier.
We shall refer to moves in the second and third kind of segments as inspection moves
and write φ to refer to sequences built exclusively from such sequences (we will use φK
and φL if we want to stress that the moves are exclusively tagged with K or L). Let us
write X for the subset of JLspec Kenc containing plays of the form:
(t0 , call m′i0 )(t0 , call mi0 )(t0 , ret mi0 (v0 ))(t0 , ret m′i0 (v0′ )) φ0

(t1 , call m′i1 )(t1 , call mi1 ) φ1 (t1 , ret mi1 (v1 ))(t1 , ret m′i1 (v1′ )) φ2
⋯ (tk , call m′ik )(tk , call mik ) φ2k−1 (tk , ret mik (vk ))(tk , ret m′ik (vk )) φ2k
where each φi contains moves alternating between O and P .
Let h1 ∈ JLfc Kenc . Threads in h1 are built from blocks of the shapes:
(t, call m′i )OK ((t, call mj )P L (t, ret mj (v)OL ))∗ (t, ret m′i (v ′ ))P K

or (t′ , call w(v))OY (t′ , call w′ (v ′ ))P Y ′ or (t′ , ret w′ (v ′′ ))OY (t′ , ret w(v ′′′ ))P Y ′ .
In the first case, the j’s and v’s are meant to represent different values in each iteration.
In the second kind of block, w needs to be introduced earlier by some (t′′ , x)P Y move
and w′ is then a name introduced by the preceding move. For the third kind, an earlier
calling sequence of the second kind must exist in the same thread.
Note that, due to locking and sequentiality of loops, h1 ↾ L takes the shape:
L
L
(t0 , call mi0 )P (t0 , ret mi0 (v0 ))O φL
0 (t1 , call mi1 )P φ1 (t1 , ret mi1 (v1 ))O φ2
L
L
⋯ (tk , call mik )P φ2k−1 (tk , ret mik (vk ))O φ2k

20

Each segment Sj = (tj , call mij ) φL
2j−1 (tj , ret mij (vj )) in h1 ↾ L must be preceded
(in h1 ) by a corresponding public call (t′j , call m′j )OK and followed by a matching return
(t′j , ret m′j (wj ))P K , where t′j need not be equal to tj . Note that there can be no other
moves from t′j separating the two moves in h1 ↾ K.
Let h′1 be obtained from h1 via the following operations around each segment Sj :
– move (t′j , call m′ij ) right to precede (tj , call mij ),
– move (t′j , ret m′ij (vj′ )) left to follow (tj , ret mi (vj )),
– rename (tj , call mi )P L (tj , ret mij (vj ))OL to (t′j , call mij )P L (t′j , ret mij (vj ))OL .
We stress that the changes are to be performed simultaneously for each segment Sj .
The rearrangements result in a library history, because they bring forward the points at
which various vj , vj′ have been introduced and, thus, inspection moves are legal. Then
we have h1 ⊑R h′1 , i.e. (h1 ↾ L)R(h′1 ↾ L) and (h1 ↾ K) ◁∗P O (h′1 ↾ K). The former
follows from the multiple renaming of the moves originally tagged with tj to t′j and the
fact that their order in h1 ↾ L is unaffected. The latter holds, because O-moves move
right and P -moves move left past other moves in h1 ↾ K that are not from the same
thread. To conclude, we show that there exists h2 ∈ X such that (h′1 ↾ L) = (h2 ↾ L) and
(h′1 ↾ K) ◁∗P O (h2 ↾ K). We can obtain h2 by rearranging inspection moves in different
threads of h′1 so that they alternate between O and P . Since the inspection moves come
in pairs this can simply be done by bringing the paired moves next to each other. Because
one of them is always from K and the other from L, this can be achieved by rearranging
moves in h′1 ↾ K only: if the O-move is from K it can be moved to the right, otherwise the
P -move from K can be moved left. Then we have h2 ∈ X ⊆ JLspec Kenc with h1 ⊑R h2 ,
as required.

6

Correctness

In this section we prove that the linearisability notions we introduce are correct: linearisability implies contextual approximation. The approach is based on showing that, in
each case, the semantics of contexts is saturated relatively to conditions that are dual to
linearisability. Hence, linearising histories does not alter the observable behaviour of a
library. We start by presenting two compositionality theorems on the trace semantics,
which will be used for relating library and context semantics.
6.1

Compositionality

The semantics we defined is compositional in the following ways:
– To compute the semantics of a library L inside a context C, it suffices to compose the
semantics of C with that of L, for a suitable notion of context-library composition
(JCK ⊘ JLK).
– To compute the semantics of a union library L1 ∪ L2 , we can compose the semantics
of L1 and L2 , for a suitable notion of library-library composition (JL1 K ⊗ JL2 K).
The above are proven using bisimulation techniques for connecting syntactic and semantic compositions, and are presented in Appendices C and D respectively.
The latter correspondence is used in Appendix E for proving that linearisability is
a congruence for library composition. From the former correspondence we obtain the
following result, which we shall use for showing correctness.

21

Theorem 33. Let L ∶ Θ → Θ′ , L′ ∶ ∅ → Θ, Θ′′ and Θ′ , Θ′′ ⊢K M1 ∥⋯∥MN ∶ unit, with
L, L′ and M1 ; ⋯; MN accessing pairwise disjoint parts of the store. Then:
link L′ ; L in (M1 ∥⋯∥MN ) ⇓ ⇐⇒ ∃h ∈ JLKN . h̄ ∈ Jlink L′ ; − in (M1 ∥⋯∥MN )K
6.2

General linearisability

Recall the general notion of linearisability defined in Section 2.2, which is based on
move-reorderings inside histories.
In Def.s 27 and 28 we have defined the trace semantics of libraries and contexts. The
semantics turns out to be closed under ◁∗OP .
Lemma 34 (Saturation). Let X = JLK (Def. 27) or X = Jlink L′ ; − in (M1 ∥⋯∥MN )K
(Def. 28). Then if h ∈ X and h ◁∗OP h′ then h′ ∈ X.
Proof. Recall that the same labelled transition system underpins the definition of X in
either case. We make several observations about the single-threaded part of that system.
– The store is examined and modified only during -transitions.
– The only transition possible after a P -move is an O-move. In particular, it is never
the case that a P -move is separated from the following O-move by an -transition.
Let us now consider the multi-threaded system and t ≠ t′ .
(t′ ,m′ )P

∗

(t,m)

– Suppose ρ ÔÔÔÔ⇒ ρ1 Ô
Ô⇒ ρ2 ÔÔ⇒ ρ3 . Then the (t′ , m′ )P -transition can be
∗

(t,m)

(t′ ,m′ )P

delayed inside t′ until after (t, m), i.e. ρ Ô
Ô⇒ ρ′1 ÔÔ⇒ ρ′2 ÔÔÔÔ⇒ ρ3 for some
′
′
′
ρ1 , ρ2 . This is possible because the ((t , m′ )P -labelled) transition does not access
or modify the store, and none of the -transitions distinguished above can be in t′ ,
thanks to our earlier observations about the behaviour of the single-threaded system.
(t′ ,m′ )

∗

(t,m)O

– Analogously, suppose ρ ÔÔÔ⇒ ρ1 Ô
Ô⇒ ρ2 ÔÔÔ⇒ ρ3 . Then the (t, m)O -transition
(t′ ,m′ )

(t,m)O

∗

can be brought forward, i.e. ρ ÔÔÔ⇒ ρ′1 ÔÔÔ⇒ ρ′2 Ô
Ô⇒ ρ3 , because it does not
access or modify the store and the preceding -transitions cannot be from t.
This, along with the fact that h1 ◁XX ′ h2 ⇐⇒ h2 ◁X ′ X h1 ⇐⇒ h1 ◁X ′ X h2 .
lead us to the notion of linearisability defined in Def. 8.
Theorem 35. L1 ⊑ L2 implies L1 ⊏∼ L2 .
Proof. Consider C such that C[L1 ] ⇓. We need to show C[L2 ] ⇓. Because C[L1 ] ⇓,
Theorem 33 implies that there exists h1 ∈ JL1 K such that h1 ∈ JCK. Because L1 ⊑ L2 ,
there exists h2 ∈ JL2 K with h1 ◁∗P O h2 . Note that h1 ◁∗OP h2 . By Lem. 34, h2 ∈ JCK.
Because h2 ∈ JL2 K and h2 ∈ JCK, using Theorem 33 we can conclude C[L2 ] ⇓.
Theorem 36. If L1 ⊑ L2 then, for suitably typed L accessing disjoint part of the store
than L1 and L2 , we have L ∪ L1 ⊑ L ∪ L2 .

22

6.3

Encapsulated linearisability

In this case libraries are being tested by clients that do not communicate with the
parameter library explicitly.
Definition 37. [Encapsulated ⊏∼ ] Given libraries L1 , L2 ∶ Θ → Θ′ , we write L1 ⊏∼ enc L2
when, for all L′ ∶ ∅ → Θ and Θ′ ⊢K M1 ∥⋯∥MN ∶ unit, if link L′ ; L1 in (M1 ∥⋯∥MN ) ⇓
then link L′ ; L2 in (M1 ∥⋯∥MN ) ⇓.
We shall call contexts of the above kind encapsulated, because the parameter library
L′ can no longer communicate directly with the client, unlike in Def. 23, where they
shared methods in Θ′′ . Consequently, Jlink L′ ; − in (M1 ∥⋯∥MN )K can be decomposed
via parallel composition into two components, whose labels correspond to L (parameter
library) and K (client) respectively.
Lemma 38 (Decomposition). Suppose L′ ∶ ∅ → Θ and Θ′ ⊢K M1 ∥⋯∥MN ∶ unit,
where Θ ∩ Θ′ = ∅. Then, setting C ′ ≡ link ∅ ; − in (M1 ∥⋯∥MN ), we have:
co
′
′
Jlink L′ ; − in (M1 ∥⋯∥MN )K = { h ∈ HΘ,Θ
′ ∣ (h ↾ L) ∈ JL K, (h ↾ K) ∈ JC K } .

Remark 39. Consider parameter library L′ ∶ ∅ → {m} and client {m′ } ⊢K M ∶ unit
with m, m′ ∈ Methsunit→(unit→unit) , and suppose we insert in their context a “copycat”
library L which implements m′ as m′ = λx.mx . Then the following scenario may seem
to contradict encapsulation: – M calls m′ (); – L calls m(); – L′ returns with m(m′′ ) to
L; – and finally L copycats this return to M . However, by definition the latter copycat is
done by L returning m′ (m′′′ ) to M , for some fresh name m′′′ , and recording internally
that m′′′ ↦ λx.m′′ x. Hence, no methods of L′ can leak to M and encapsulation holds.
Because of the above decomposition, the context semantics satisfies a stronger
closure property than that already specified in Lem. 34, which in turn leads to the notion
of encapsulated linearisability of Def. 12. The latter is defined in term of the symmetric
reordering relation ◇, which allows for swaps (in either direction) between moves from
different threads if they are tagged with K and L respectively.
Moreover, we can show the following.
Lemma 40 (Encapsulated saturation). Consider X = Jlink L′ ; − in (M1 ∥⋯∥MN )K
(Definition 28). Then:
– If h ∈ X and h (◁OP ∪ ◇)∗ h′ then h′ ∈ X.
– Let s1 (t, x)OY s2 (t, x′ )P Y ′ s3 ∈ X be such that no move in s2 comes from thread t.
Then Y = Y ′ , i.e. inside a thread only O can switch between K and L.
Due to Theorem 33, the above property of contexts means that, in order to study
termination in the encapsulated case, one can safely restrict attention to library traces
satisfying a dual property to the one above, i.e. to elements of JLKenc . Note that JLKenc can
be obtained directly from our labelled transition system by restricting its single-threaded
part to reflect the switching condition. Observe that Theorem 33 will still hold for JLKenc
(instead of JLK), because we have preserved all the histories that are compatible with
context histories. We are ready to prove correctness of encapsulated linearisability.

23

Theorem 41. L1 ⊑enc L2 implies L1 ⊏∼ enc L2 .
Proof. Similarly to Theorem 35, except we invoke Lemma 40 instead of Lemma 34.
We next examine the behaviour of ⊑enc with respect to library composition. In contrast
to Section 6.2, we need to restrict composition for it to be compatible with encapsulation.
Remark 42. The general case of union does not conform with encapsulation in the sense
that encapsulated testing of L ∪ Li (i = 1, 2) according to Def. 37 may subject Li to
unencapsulated testing. For example, because method names of L and Li are allowed to
overlap, methods in L may call public methods from Li as well as implementing abstract
methods from Li . This amounts to L playing the role of both K and L, which in addition
can communicate with each other, as both are inside L.
Even if we make L and Li non-interacting (i.e. without common abstract/public
methods), if higher-order parameters are still involved, the encapsulated tests of L ∪ Li
can violate the encapsulation hypothesis for Li . For instance, consider the methods
m2 , m′1 , m′2 ∈ Methsunit,unit and m1 ∈ Meths(unit→unit),unit , and libraries L1 , L2 ∶
{m1 } → {m2 } and L ∶ {m′1 } → {m′2 }, as well as the unions L ∪ Li ∶ {m1 , m2 } →
{m′1 , m′2 }. A possible trace in JL ∪ Li Kenc is this one:
hi = (1, call m2 ())OK (1, call m1 (v))P L (1, ret m1 ())OL

(1, ret m2 ())P K (1, call m′2 ())OK (1, call m′1 ())P L (1, call v())OL
which decomposes as hi = h′ ⩕σΠ,∅ h′i , with Π = {m1 , m2 , m′1 , m′2 }, σ = 2222112,
h′ = (1, call m′2 ())OK (1, call m′1 ())P L and:
h′i = (1, call m2 ())OK (1, call m1 (v))P L (1, ret m1 ())OL (1, ret m2 ())P K (1, call v())OL
We now see that h′i ∉ JLi Kenc as in the last move O is changing component from K to L.
We therefore look at compositionality for two specific cases: encapsulated sequencing
(e.g. of L∶ Θ → Θ′ with L′ ∶ Θ′ → Θ′′ ) and disjoint union for first-order methods. Given
L ∶ Θ1 → Θ2 and L′ ∶ Θ1′ → Θ2′ , we define their disjoint union L ⊎ L′ = L ∪ L′ ∶
(Θ1 ∪ Θ1′ ) → (Θ2 ∪ Θ2′ ) under the assumption that (Θ1 ∪ Θ2 ) ∩ (Θ1′ ∪ Θ2′ ) = ∅.
Theorem 43. Let L1 , L2 ∶ Θ1 → Θ2 and L ∶ Θ1′ → Θ2′ . If L1 ⊑enc L2 then:
– assuming Θ2′ = Θ1 , we have L ; L1 ⊑enc L ; L2 and L1 ; L ⊑enc L2 ; L;
– if Θ1 , Θ2 , Θ1′ , Θ2′ are first-order then L ⊎ L1 ⊑enc L ⊎ L2 .
6.4

Relational linearisability

Finally, we examine relational linearisability (Def. 16). We begin with a suitable notion
of relation R. We next restrict encapsulated contextual testing to R-closed contexts.
Definition 44. Let R ⊆ H∅,Θ × H∅,Θ be a set closed under permutation of names in
Meths ∖ Θ. We say that L ∶ ∅ → Θ is R-closed if, for any h, h′ such that h R h′ , if
h ∈ JLK then h′ ∈ JLK.

Definition 45. [R-closed encapsulated ⊏∼ ] Given L1 , L2 ∶ Θ → Θ′ , we write L1 ⊏∼ R L2
if, for all R-closed L′ ∶ ∅ → Θ and for all Θ′ ⊢K M1 ∥⋯∥MN ∶ unit, whenever
link L′ ; L1 in (M1 ∥⋯∥MN ) ⇓ then we also have link L′ ; L2 in (M1 ∥⋯∥MN ) ⇓.
24

Theorem 46. L1 ⊑R L2 implies L1 ⊏∼ R L2 .
We conclude by showing that ⊑R is also compositional in the sense proposed in [3].
)-closed if, for all k ∈ H and h′ ∈ JLKenc , (h′ ↾
Given R, G ⊆ H × H, we say that L is (R
G
K) R k implies that there is h′′ ∈ JLKenc with (h′′ ↾ K) = k and (h′ ↾ L) G (h′′ ↾ L).
Theorem 47. Let R, G ⊆ H × H, L1 , L2 ∶ Θ1 → Θ2 and L ∶ Θ1′ → Θ2′ , such that
L1 ⊑R L2 . If L is suitably typed:
)-closed, we have L ; L1 ⊑G L ; L2 ; – L1 ; L ⊑R L2 ; L;
– if L is (R
G
– if Θ1 , Θ2 , Θ1′ , Θ2′ are first-order then L ⊎ L1 ⊑R+ L ⊎ L2 , where R+ = {(s, s′ ) ∈
H∅,Θ1 ∪Θ1′ × H∅,Θ1 ∪Θ1′ ∣ (s↾Θ1 )R(s′ ↾Θ1 ), (s↾Θ1′ ) = (s′ ↾Θ1′ )}and s ↾ Θ is the
largest subsequence of s belonging to H∅,Θ1 .

7

Related and future work

Since the work of Herlihy and Wing [12], linearisability has been consistently used as a
correctness criterion for concurrent algorithms on a variety of data structures [18], and
has yielded a variety of proof methods [5]. As mentioned in the Introduction, the field
has focussed on libraries with methods of base-type inputs and outputs, with Cerone
et al. recently catering for the presence of abstract as well as public methods [3]. An
explicit connection between linearisability and refinement was made by Filipovic et
al. in [6], where it was shown that, in base-type settings, linearisability and refinement
coincide. Similar results have been proved in [4,9,17,3]. Our contributions herein are
notions of linearisability that can serve as correctness criteria for libraries with methods
of arbitrary higher-order types. Moreover, we relate them to refinement, thus establishing
the soundness of linearisability, and demonstrate they are well-behaved with respect to
library composition.
Verification of concurrent higher-order programs has been extensively studied outside of linearisability; we next mention works most closely related to linearisability
reasoning. At the conceptual level, [6] proposed that the verification goal behind linearisability is observational refinement. In the same vein, [24] utilised logical relations as a
direct method for proving refinement in a higher-order concurrent setting, while [23]
introduced a program logic that builds on logical relations. On the other hand, proving
conformance to a history specification has been addressed in [20] by supplying historyaware interpretations to off-the-shelf Hoare logics for concurrency. Other logic-based
approaches for concurrent higher-order libraries, which do not use linearisability or any
other notion of logical atomicity, include Higher-Order and Impredicative Concurrent
Abstract Predicates [21,22].
One possible avenue for expansion of this work, following the example of [6], would
be to identify language fragments where higher-order linearisability coincides with observational refinement. Based on the game semantic results of [7], such a correspondence
may be possible to demonstrate already in the language examined herein.
The higher-order language we examined used memory in the form of references,
which were global and moreover followed the standard memory model (sequential consistency). Therefore, future research also includes enriching the setting with dynamically
allocated memory and expanding its reach to weak memory models. In the latter direction, our traces could need to be strengthened towards truly-concurrent structures, such
as event-structures, following the recent examples of [2,14].
25

References
1. S. Abramsky and G. McCusker. Game semantics. In H. Schwichtenberg and U. Berger, editors,
Logic and Computation. Springer-Verlag, 1998. Proceedings of the 1997 Marktoberdorf
Summer School.
2. S. Castellan. Weak memory models using event structures. In JFLA, 2016.
3. A. Cerone, A. Gotsman, and H. Yang. Parameterised linearisability. In Proceedings of
ICALP’14, volume 8573 of Lecture Notes in Computer Science, pages 98–109. Springer,
2014.
4. J. Derrick, G. Schellhorn, and H. Wehrheim. Mechanically verified proof obligations for
linearizability. ACM Trans. Program. Lang. Syst., 33(1):4, 2011.
5. B. Dongol and J. Derrick. Verifying linearisability: A comparative survey. ACM Comput.
Surv., 48(2):19, 2015.
6. I. Filipovic, P. W. O’Hearn, N. Rinetzky, and H. Yang. Abstraction for concurrent objects.
Theor. Comput. Sci., 411(51-52):4379–4398, 2010.
7. D. R. Ghica and A. S. Murawski. Angelic semantics of fine-grained concurrency. In
Proceedings of FOSSACS, volume 2987 of Lecture Notes in Computer Science, pages 211–
225. Springer-Verlag, 2004.
8. D. R. Ghica and N. Tzevelekos. A system-level game semantics. Electr. Notes Theor. Comput.
Sci., 286:191–211, 2012.
9. A. Gotsman and H. Yang. Liveness-preserving atomicity abstraction. In Automata, Languages
and Programming - 38th International Colloquium, ICALP 2011. Proceedings, Part II, pages
453–465, 2011.
10. S. Heller, M. Herlihy, V. Luchangco, M. Moir, W. N. S. III, and N. Shavit. A lazy concurrent
list-based set algorithm. In OPODIS, pages 3–16, 2005.
11. D. Hendler, I. Incze, N. Shavit, and M. Tzafrir. Flat combining and the synchronizationparallelism tradeoff. In Proceedings of SPAA 2010, pages 355–364, 2010.
12. M. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects.
ACM Trans. Program. Lang. Syst., 12(3):463–492, 1990.
13. A. Jeffrey and J. Rathke. A fully abstract may testing semantics for concurrent objects. Theor.
Comput. Sci., 338(1-3):17–63, 2005.
14. A. S. A. Jeffrey and J. Riely. On thin air reads: Towards an event structures model of relaxed
memory. In Proceedings of LICS, 2016.
15. J. Laird. A game semantics of Idealized CSP. In Proceedings of MFPS’01, pages 1–26.
Elsevier, 2001. ENTCS, Vol. 45.
16. J. Laird. A fully abstract trace semantics for general references. In Proceedings of ICALP,
volume 4596 of Lecture Notes in Computer Science, pages 667–679. Springer, 2007.
17. H. Liang and X. Feng. Modular verification of linearizability with non-fixed linearization
points. In ACM SIGPLAN Conference on Programming Language Design and Implementation,
PLDI ’13. Proceedings, pages 459–470, 2013.
18. M. Moir and N. Shavit. Concurrent data structures. In Handbook of Data Structures and
Applications. Chapman and Hall/CRC, 2004.
19. P. W. O’Hearn, N. Rinetzky, M. T. Vechev, E. Yahav, and G. Yorsh. Verifying linearizability
with hindsight. In PODC, pages 85–94, 2010.
20. I. Sergey, A. Nanevski, and A. Banerjee. Specifying and verifying concurrent algorithms
with histories and subjectivity. In Programming Languages and Systems - 24th European
Symposium on Programming, ESOP 2015. Proceedings, pages 333–358, 2015.
21. K. Svendsen and L. Birkedal. Impredicative concurrent abstract predicates. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014.
Proceedings, pages 149–168, 2014.

26

22. K. Svendsen, L. Birkedal, and M. J. Parkinson. Joins: A case study in modular specification of
a concurrent reentrant higher-order library. In ECOOP 2013 - Object-Oriented Programming
- 27th European Conference. Proceedings, pages 327–351, 2013.
23. A. Turon, D. Dreyer, and L. Birkedal. Unifying refinement and hoare-style reasoning in a logic
for higher-order concurrency. In ACM SIGPLAN International Conference on Functional
Programming, ICFP’13, pages 377–390, 2013.
24. A. J. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, and D. Dreyer. Logical relations for finegrained concurrency. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, POPL ’13, pages 343–356, 2013.

27

A

Big-step vs small-step reorderings

[3] defines linearisation in the general case using a “big-step” relation that applies a
single permutation to the whole sequence. This contrasts with our definition as ◁∗P O ,
in which we combine multiple adjacent swaps. We show that the two definitions are
equivalent.
Definition 48. [[3]] Let h1 , h2 ∈ HΘ,Θ′ of equal length. We write h1 ◁big
P O h2 if there
is a permutation π ∶ {1, ⋯, ∣h1 ∣} → {1, ⋯, ∣h2 ∣} such that, writing hi (j) for the j-th
element of hi : for all j, we have h1 (j) = h2 (π(j)) and, for all i < j:
((∃t. h1 (i) = (t, −) ∧ h1 (j) = (t, −))
∨(∃t1 , t2 . h1 (i) = (t1 , −)P ∧ h1 (j) = (t2 , −)O )) Ô⇒ h2 (i) < h2 (j)
In other words, h2 is obtained from h1 by permuting moves in such a way that their
order in threads is preserved and whenever a O-move occurred after an P -move in h1 ,
the same must apply to their permuted copies in h2 .
∗
Lemma 49. ◁big
P O = ◁P O .

Proof. It is obvious that ◁∗P O ⊆ ◁big
P O , so it suffices to show the converse.
Suppose h1 ◁big
h
.
Consider
the set Xh1 ,h2 = {h ∣ h1 ◁∗P O h, h ◁big
PO 2
P O h2 }. Note
that Xh1 ,h2 is not empty, because h1 ∈ Xh1 ,h2 .
For two histories h′ , h′′ , define δ(h′ , h′′ ) to be the length of the longest common
prefix of h′ and h′′ . Let N = max{δ(h, h2 ) ∣ h ∈ Xh1 ,h2 }. Note that N ≤ ∣h1 ∣ = ∣h2 ∣.
h

– If N = ∣h2 ∣ then we are done, because N = ∣h2 ∣ implies h2 ∈ Xh1 ,h2 and, thus,
h1 ◁∗P O h2 .
– Suppose N < ∣h2 ∣ and consider h such that N = δ(h, h2 ). We are going to arrive at a
contradiction by exhibiting h′ ∈ Xh1 ,h2 such that δ(h′ , h2 ) > N .
Because N = δ(h, h2 ) and N < ∣h2 ∣, we have
h2 = a1 ⋯aN (t, m)u
h = a1 ⋯aN (t1 , m1 )⋯(tk , mk )(t, m)u′ ,
where ti ≠ t, because order in threads must be preserved. Consider
h′ = a1 ⋯aN (t, m)(t1 , m1 )⋯(tk , mk )u′ .
Clearly δ(h′ , h2 ) > N so, for a contradiction, it suffices to show that h′ ∈ Xh1 ,h2 .
big
′
Note that because h ◁big
P O h2 , we must also have h ◁P O h2 , because the new P O
′
dependencies in h (wrt h) caused by moving (t, m) forward are consistent with h2 .
Hence, we only need to show that h ◁∗P O h′ . Let us distinguish two cases.
● If (t, m) is a P -move then, clearly, h ◁∗P O h′ (P -move moves forward).
● If (t, m) is an O-move then, because h ◁big
P O h2 , all of the (ti , mi ) actions must
be O-moves (otherwise their position wrt (t, m) would have to be preserved in
h2 and it isn’t). Hence, h ◁∗P O h′ , as required.

28

B

Proofs from Section 6

Proof of Lemma 40. For the first claim, closure under ◁OP (resp. ◇) follows from
Lemma 34. (resp. Lemma 38).
Suppose h = s1 (t, x)OY s2 (t, x′ )P Y ′ s3 violates the second claim and (t, x), (t, x′ )
is the earliest such violation in h, i.e. no violations occur in s1 . Observe that then h
restricted to moves of the form (t, z)XY ′ would not be alternating, which contradicts
the fact that h ↾ Y ′ is a history (Lemma 38).
Proof of Theorem 46. Consider C such that C[L1 ] ⇓. We need to show C[L2 ] ⇓. Since
C[L1 ] ⇓, by Theorem 33 there exists h1 ∈ JL1 Kenc such that h1 ∈ JCKenc . Also, by
Lemma 38, (h1 ↾ K) ∈ JC ′ Kenc and (h1 ↾ L) ∈ JL′ Kenc for C ′ , L′ specified in that lemma.
Because L1 ⊑R L2 , there exists h2 ∈ JL2 Kenc such that (h1 ↾ K) ◁∗P O (h2 ↾ K) and
(h1 ↾ L) R (h2 ↾ L). Note that the former implies (h1 ↾ K) ◁∗OP (h2 ↾ K). Because
(h1 ↾ L) ∈ JL′ Kenc , (h1 ↾ L) R (h2 ↾ L) and L′ is R-closed, we have (h2 ↾ L) ∈ JL′ Kenc .
On the other hand, because (h1 ↾ K) ∈ JC ′ Kenc and (h1 ↾ K) ◁∗OP (h2 ↾ K) Lemma 40
implies (h2 ↾ K) ∈ JC ′ Kenc . Consequently, (h2 ↾ K) ∈ JC ′ Kenc and (h2 ↾ L) ∈ JL′ Kenc ,
so Lemma 38 entails h2 ∈ JCKenc . Hence, since h2 ∈ JL2 K and h2 ∈ JCKenc , we can
conclude C[L2 ] ⇓ by Theorem 33.

C

Trace compositionality

In this section we demonstrate how the semantics of a library inside a context can be
drawn by composing the semantics of the library and that of the context. The result
played a crucial role in our arguments about linearisability and contextual refinement in
Section 6.
Let us divide (reachable) evaluation stacks into two classes: L-stacks, which can be
produced in the trace semantics of a library; and C-stacks, which appear in traces of a
context.
EL ∶∶= [] ∣ m ∶∶ E ∶∶ EL′

EC ∶∶= [] ∣ m ∶∶ EC′

EL′

EC′ ∶∶= m ∶∶ E ∶∶ EC

∶∶= m ∶∶ EL

From the trace semantics definition we have that N -configurations in the semantics
of a library feature evaluation stacks of the forms EL (in O-configurations) and EL′ (in
P -configurations): these we will call L-stacks. On the other hand, those produced from
a context utilise C-stacks which are of the forms EC (in P -configurations) and EC′ (in
O-configurations).
From here on, when we write E we will mean an L-stack or a C-stack. Moreover, we
⃗ ⋯)
will call an N -configuration ρ an L-configuration (or a C-configuration), if ρ = (C,
and, for each i, Ci = (Ei , ⋯) with Ei an L-stack (resp. a C-stack).
⃗ R, P, A, S) is a C-configuration
Let ρ, ρ′ be N -configurations and suppose ρ = (C,
′
′
′
′
′
′
⃗
and ρ = (C , R , P , A , S ) an L-configuration. We say that ρ and ρ′ are compatible,
written ρ ≍ ρ′ , if S and S ′ have disjoint domains and, for each i:
– Ci = (EC , M ) and Ci′ = (EL , −), or Ci = (EC′ , −) and Ci′ = (EL′ , M ).
– If the public and abstract names of Ci are (PL , PK ) and (AL , AK ) respectively, and
′
those of Ci′ are (PL′ , PK
) and (A′L , A′K ), then PL = A′L , PK = A′K , AL = PL′ and
′
AK = PK
.
29

– The private names of ρ (i.e. those in dom(R) ∖ PL ∖ PK ) do not appear in ρ′ , and
dually for the private names of ρ′ .
– If Ci = (E, ⋯) and Ci′ = (E ′ , ⋯) then E and E ′ are in turn compatible, that is:
● either E = m ∶∶ E ∶∶ E1 , E ′ = m ∶∶ E1′ and E1 , E1′ are compatible,
● or E = m ∶∶ E1 , E ′ = m ∶∶ E ∶∶ E1′ and E1 , E1′ are compatible,
or E = E ′ = [].
Note, in particular, that if ρ ≍ ρ′ then ρ must be a context configuration, and ρ′ a library
configuration.
We next define a trace semantics on compositions of compatible such N -configurations.
We use the symbol ⊘ for configuration composition: we call this external composition,
to distinguish it from the composition of ρ and ρ′ we can obtain by merging their
components, which we will examine later.
ρ1 Ô
Ô⇒ ρ′1
I NT1
ρ1 ⊘ ρ2 Ð→ ρ′1 ⊘ ρ2

ρ2 Ô
Ô⇒ ρ′2
I NT2
ρ1 ⊘ ρ2 Ð→ ρ1 ⊘ ρ′2

(t,call m(v))

(t,call m(v))

(t,ret m(v))

(t,ret m(v))

ρ1 ÔÔÔÔÔ⇒ ρ′1 ρ2 ÔÔÔÔÔ⇒ ρ′2
C ALL
ρ1 ⊘ ρ2 Ð→ ρ′1 ⊘ ρ′2
ρ1 ÔÔÔÔÔ⇒ ρ′1 ρ2 ÔÔÔÔÔ⇒ ρ′2
R ETN
ρ1 ⊘ ρ2 Ð→ ρ′1 ⊘ ρ′2
The I NT rules above have side-conditions imposing that the resulting pairs of configurations are still compatible. Concretely, this means that the names created fresh in internal
transitions do not match the names already present in the configurations of the other
component. Note that external composition is not symmetric, due to the context/library
distinction we mentioned.
Our next target is to show a correspondence between the above-defined semantic
composition and the semantics obtained by (syntactically) merging compatible configurations. This will demonstrate that composing the semantics of two components
is equivalent to first syntactically composing them and then evaluating the result. In
order to obtain this correspondence, we need to make the semantics of syntactically
composed configurations more verbose: in external composition methods belong either
to the context or the library, and when e.g. the client wants to evaluate mm′ , with m a
library method, the call is made explicit and, more importantly, m′ is replaced by a fresh
method name. On the other hand, when we compose syntactically such a call will be
done internally, and without refreshing m′ .
To counter-balance the above mismatch, we extend the syntax of terms and evaluation
contexts, and the operational semantics of closed terms as follows. The semantics will
now involve quadruples of the form:
⃗ S)
(E[M ], R1 , R2 , S) written also (E[M ], R,
where the two repositories correspond to context and library methods respectively, so
in particular dom(R1 ) ∩ dom(R2 ) = ∅. Moreover, inside E[M ] we tag method names
and lambda-abstractions with indices 1 and 2 to record which of the two components
(context or library) is enclosing them: the tag 1 is used for the context, and 2 for the
30

library. Thus e.g. a name m1 signals an occurrence of method m inside the context.
Tagged methods are passed around and stored as ordinary methods, but their behaviour
changes when they are applied. Moreover, we extend (tagged) evaluation contexts by
explicitly marking return points of methods:
E ∶∶= ● ∣ ⋯ ∣ let x = E in M ∣ mE ∣ r ∶= E ∣ ⟨mi ⟩ E
In particular, E[M ] may not necessarily be a (tagged) term, due to the return annotations.
The new reduction rules are as follows (we omit indices when they are not used in the
rules).
⃗ S) Ð
⃗ S′)
(E[i1 ⊕ i2 ], R,
→′t (E[i], R,
⃗ S) Ð
⃗ S′)
(E[tid ], R,
→′ (E[t], R,

(i = i1 ⊕ i2 )

t

⃗ S) Ð
⃗ S′)
(E[πj ⟨v1 , v2 ⟩], R,
→′t (E[vj ], R,
⃗ S) Ð
⃗ S) (j = (i > 0))
(E[if i then M0 else M1 ], R,
→′t (E[Mj ], R,
⃗ S) Ð
⃗ ⊎i (m ↦ λx.M ), S)
(E[λi x.M ], R,
→′ (E[mi ], R
t

⃗ S) Ð
⃗ S) if Ri (m) = λx.M
(E[mi v], R,
→′t (E[M {v/x}i ], R,
i
′
i
′
⃗ S) Ð
⃗ ′ , S) if R3−i (m) = λx.M with
(E[m v], R,
→t (E[⟨m ⟩ M {v /x}3−i ], R
⃗′ = R
⃗ ⊎i {m′ ↦ λy.mj y ∣ 1 ≤ j ≤ k}
Meths(v) = {m1 , ⋯, mk }, v ′ = v{ m′j /mj ∣ 1 ≤ j ≤ k}, R
j
i
′
′i
′
′
⃗
⃗
(E[⟨m ⟩ v], R, S) Ð
→ (E[v ], R ⊎3−i {m ↦ λy.mj y}, S) with mj , m and v ′ as above
t

j

j

⃗ S) Ð
⃗ S)
(E[let x = v in M ], R,
→′t (E[M {v/x}], R,
′
⃗ S) Ð
⃗ S)
(E[!r], R,
→ (E[S(r)], R,
t

⃗ S) Ð
⃗ S[r ↦ i])
(E[r ∶= i], R,
→′t (E, R,
⃗ S) Ð
⃗ S[r ↦ mi ])
(E[r ∶= mi ], R,
→′ (E, R,
t

Above we write M i for the term M with all its methods and lambdas tagged (or re⃗ ⊎1 (m ↦ λx.M ) = (R1 ⊎ (m ↦
tagged) with i. Moreover, we use the convention e.g. R
λx.M ), R2 ). Note that the repositories need not contain tags as, whenever a method is
looked up, we subsequently tag its body explicitly.
Thus, the computationally observable difference of the new semantics is in the rule
for reducing E[mi v] when m is not in the domain of Ri : this corresponds precisely to
the case where e.g. a library method is called by the context with another method as
argument. A similar behaviour is exposed when such a method is returning. However,
this novelty merely adds fresh method names by η-expansions and does not affect the
termination of the reduction.
Defining parallel reduction Ô
Ô⇒′ in an analogous way to Ô
Ô⇒, we can show the
following. We let a quadruple (M1 ∥⋯∥MN , R, S) be final if Mi = () for all i, and we
write (M1 ∥⋯∥MN , R, S) ⇓ if (M1 ∥⋯∥MN , R, S) can reduce to some final quadruple;
these notions are defined for (M1 ∥⋯∥MN , R1 , R2 , S) in the same manner.
Lemma 50. For any legal (M1 ∥⋯∥MN , R1 , R2 , S), we have that (M1 ∥⋯∥MN , R1 , R2 , S) ⇓
iff (M1 ∥⋯∥MN , R1 ∪ R2 , S) ⇓.
31

We now proceed to syntactic composition of N -configurations. Given a pair ρ1 ≍ ρ2 ,
we define a single quadruple corresponding to their syntactic composition, called their in⃗ R1 , P1 , A1 , S1 ) and ρ2 = (C⃗′ , R2 , P2 , A2 , S2 )
ternal composition, as follows. Let ρ1 = (C,
′
and, for each i, Ci = (Ei , Xi ) and Ci = (Ei′ , Xi′ ), with {Xi , Xi′ } = {Mi , −}, and we let
ki = 1 just if Xi = Mi . We let the internal composition of ρ1 and ρ2 be the quadruple:
kN
′
ρ1 ⩕ ρ2 = ((E1 ⩕ E1′ )[M1k1 ]∥⋯∥(EN ⩕ EN
)[MN
], R1 , R2 , S1 ⊎ S2 )

where compatible evaluation stacks E, E ′ are composed into a single evaluation context
E ⩕ E ′ , as follows.
(m ∶∶ E ∶∶ E) ⩕ (m ∶∶ E ′ ) = (E ⩕ E ′ )[E[⟨m⟩ ●]1 ]
(m ∶∶ E ′ ) ⩕ (m ∶∶ E ∶∶ E) = (E ⩕ E ′ )[E[⟨m⟩ ●]2 ]
and [] ⩕ [] = ●. Unfolding the above, we have that, for example:
[mk , Ek , mk−1 , mk−2 , Ek−2 , ⋯, m1 , E1 ]
′

′

⩕ [mk , mk−1 , Ek−1 , mk−2 , ⋯, m1 ] = E11 [⟨m11 ⟩ E22 [⋯Ekk [⟨mkk ⟩ ●]⋯]]
where k ′ = 2 − (k mod 2).
We proceed to fleshing out the correspondence. We observe that an L-configuration
ρ can be the final configuration of a trace just if all its components are O-configurations
with empty evaluation stacks. On the other hand, for C-configurations, we need to
reach P -configurations with terms (). Thus, we call an N -configuration ρ final if ρ =
⃗ R, P, A, S) and either Ci = ([], −) for all i, or Ci = ([], ()) for all i.
(C,
Let us write (S1 , ↪1 , F1 ) for the transition system induced from external composition, and (S2 , ↪2 , F2 ) be the transition system derived from internal composition:
– S1 = {ρ ⊘ ρ′ ∣ ρ ≍ ρ′ }, F1 = {ρ ⊘ ρ′ ∈ S1 ∣ ρ, ρ′ final}, and ↪1 the transition relation
Ð→ defined previously.
⃗ S) ∣ (M1 ∥⋯∥MN , R1 ⊎ R2 , S) valid}, F2 = {x ∈ S2 ∣
– S2 = {(M1 ∥⋯∥MN , R,
x final}, and ↪2 the transition relation Ô
Ô⇒′ defined above.
A relation R ⊆ S1 × S2 is called a bisimulation if, for all (x1 , x2 ) ∈R:
– x1 ∈ F1 iff x2 ∈ F2 ,
– if x1 ↪1 x′1 then x2 ↪2 x′2 and (x′1 , x′2 ) ∈ R,
– if x2 ↪2 x′2 then x1 ↪1 x′1 and (x′1 , x′2 ) ∈ R.
Given (x1 , x2 ) ∈ S1 × S2 , we say that x1 and x2 are bisimilar, written x1 ∼ x2 , if
(x1 , x2 ) ∈ R for some bisimulation R.
Lemma 51. Let ρ ≍ ρ′ be compatible N -configurations. Then, (ρ ⊘ ρ′ ) ∼ (ρ ⩕ ρ′ ).
Recall we write h̄ for the O/P complement of the history h. We can now prove
Theorem 33, which states that the behaviour of a library L inside a context C can be
deduced by composing the semantics of L and C.

32

Theorem 33 Let L ∶ Θ → Θ′ , L′ ∶ 1 → Θ, Θ1 and Θ′ , Θ1 ⊢ M1 , ⋯, MN ∶ unit, with L, L′
and M1 ; ⋯; MN accessing pairwise disjoint parts of the store. Then, link L′ ; L in (M1 ∥⋯∥MN ) ⇓
iff there is h ∈ JLKN such that h̄ ∈ Jlink L′ ; − in (M1 ∥⋯∥MN )K.

Proof. Let C be the context link L′ ; − in (M1 ∥⋯∥MN ), and suppose (L) Ð→∗lib
(, R0 , S0 ) and (L′ ) Ð→∗lib (, R′0 , S0′ ) with dom(R0 ) ∩ dom(R′0 ) = dom(S0 ) ∩
dom(S0′ ) = ∅. We set:
ρ0 = (([], −)∥⋯∥([], −), R0 , (∅, Θ′ ), (Θ, ∅), S0 )
ρ′0 = (([], M1 )∥⋯∥([], MN ), R′0 , (Θ, ∅), (∅, Θ′ ), S0′ )

We pick these as the initial N -configurations for JLKN and JCK respectively. Moreover,
⃗ ∣
we have that (L′ ; L) Ð→∗lib (, R′′0 , S0′′ ) where R′′0 = {(m, (R0 ⊎ R′0 )(m){!⃗
r/m})
⃗ ⊎s {(ri , mi ) ∣ i = 1, ⋯, n}, assuming
m ∈ dom(R0 ⊎ R′0 )} and S0′′ = (S0 ⊎ S0′ ){!⃗
r/m}
Θ = {m1 , ⋯, mn } and r1 , ⋯, rn are fresh references of corresponding types. Hence,
the initial triple for JC[L]K is taken to be φ0 = (([], M1 )∥⋯∥([], MN ), R′′0 , S0′′ ). On
the other hand, ρ′0 ⩕ ρ0 = (([], M1 )∥⋯∥([], MN ), R′0 , R0 , S0 ⊎ S0′ ) and, using also
Lemma 50, we have that φ0 ⇓ iff ρ′0 ⩕ ρ0 ⇓.
Then, for the forward direction of the claim, from φ0 ⇓ we obtain that ρ′0 ⩕ρ0 ⇓. From
the previous lemma, we have that so does ρ′0 ⊘ρ0 . From the latter reduction we obtain the
required common history. Conversely, suppose h ∈ JLKN and h̄ ∈ JCK. WLOG, assume
that Meths(h) ∩ (dom(R0 ) ∪ dom(R′0 )) ⊆ Θ ∪ Θ1 ∪ Θ′ (we can appropriately alphacovert R0 and R′0 for this). Then, ρ0 and ρ′0 both produce h, with opposite polarities.
By definition of the external composite reduction, we then have that ρ′0 ⊘ ρ0 reduces to
some final state. By the previous lemma, we have that ρ′0 ⩕ ρ0 reduces to some final
quadruple, which in turn implies that φ0 ⇓, i.e. link L′ ; L in (M1 ∥⋯∥MN ) ⇓.
C.1

Lemma 50

We purpose to show that, for any legal (M1 ∥⋯∥MN , R1 , R2 , S), (M1 ∥⋯∥MN , R1 , R2 , S) ⇓
iff (M1 ∥⋯∥MN , R1 ∪ R2 , S) ⇓.
We prove something stronger. For any repository R whose entries are of the form
(m, λx.m′ x), we define a directed graph G(R) where vertices are all methods appearing
in R, and (m, m′ ) is a (directed) edge just if R(m) = λx.m′ x. In such a case, we call R
an expansion class if G(R) is acyclic and all its vertices have at most one outgoing edge.
Moreover, given an expansion class R, we define the method-for-method substitution
{R} that assigns to each vertex m of G(R) the (unique) leaf m′ such that there is
a directed path from m to m′ in G(R). Let us write L(R) for the set of leaves of
G(R). For any quadruple φ = (E1 [M1 ]∥⋯∥EN [MN ], R1 , R2 , S) and expansion class
R ⊆ R1 ∪ R2 , we define the triple:
φ#R = (E1 [M1 ]∥⋯∥EN [MN ], R1 ∪ R2 , S){R}
= (E1 [M1 ]{R}∥⋯∥EN [MN ]{R}, (R1 ∪ R2 ){R}, S{R})
where R′ {R} = {(m, R′ (m){R}) ∣ m ∈ dom(R′ ∖ R) ∪ L(R)}, S{R} = (S ↾
Refsint ) ∪ {(r, S(r){R}) ∣ r ∈ dom(S) ∖ Refsint }, and E[M ] is the term obtained from
E[M ] by removing all tagging.
33

We next define a notion of indexed bisimulation between the transition systems
produced from quadruples and triples respectively. Given an expansion class R, a
relation RR between quadruples and triples is called an R-bisimulation if, whenever
φ1 R R φ2 :
–
–
–
–

φ1 final implies φ2 final
φ2 final implies φ2 ⇓
φ1 Ô
Ô⇒′ φ′1 implies φ2 Ô
Ô⇒= φ′2 and φ′1 RR′ φ′2 for some expansion class R′ ⊇ R
′
φ2 Ô
Ô⇒ φ2 implies φ1 Ô
Ô⇒′∗ φ′1 and φ′1 RR′ φ′2 for some expansion class R′ ⊇ R.

Thus, Lemma 50 directly follows from the next result.
Lemma 52. For all expansion classes R, the relation RR =
⃗ S) legal ∧ R ⊆ R1 ∪ R2 }
{(φ, φ#R) ∣ φ = (E1 [M1 ]∥⋯∥EN [MN ], R,
is a bisimulation.
Proof. Suppose φRR φ#R . We note that finality conditions are satisfied: if φ is final
then so is φ#R ; while if φ#R is final then all its contexts are from the grammar:
E ′ ∶∶= ● ∣ ⟨mi ⟩ E ′
so φ ⇓ by acyclicity of G(R).
Suppose now φ Ô
Ô⇒ φ′ , say due to (E1 [M1 ], R1 , R2 , S) Ð
→′1 (E1′ [M1′ ], R′1 , R′2 , S ′ ).
In case the reduction is not a function call or return, then it can be clearly simulated by
φ#R . Otherwise, suppose:
⃗ S) Ð
⃗ S). If m ∉ dom(R) then, writing R12 for
– (E1 [mi v], R,
→′1 (E1 [M {v/x}i ], R,
R1 ∪R2 , the above can be simulated by (E1 [mv], R12 , S){R} Ð
→1 (E1 [M {v/x}], R12 , S){R}.
If, on the other hand, m ∈ dom(R), suppose Ri (m) = λx.m′ x, then M = m′ x and
m{R} = m′ {R} so we have:
E1 [M {v/x}i ]{R} = E1 [(m′ v)i ]{R} = E1 [(mv)i ]{R}
and E1 [(mv)i ] = E1 [mi v] by the way the semantics was defined, so φ′#R = φ#R .
⃗ S) Ð
⃗ ′ , S), with R3−i (m) = λx.M ,
– (E1 [mi v], R,
→′1 (E1 [⟨mi ⟩ M {v ′ /x}3−i ], R
′
′
′
⃗ = R⊎
⃗ i {m′ ↦ λx.mj x ∣ 1 ≤ j ≤ k}.
⃗ /m}
⃗ and R
Meths(v) = {m1 , ⋯, mk }, v = {m
j
′
′
Let R = R ⊎ {mj ↦ λx.mj x ∣ 1 ≤ j ≤ k} ⊆ R′1 ∪ R′2 . If m ∉ dom(R) then
(E1 [mv], R12 , S){R} Ð
→1 (E1 [M {v/x}], R12 , S){R}, and we have:
E1 [⟨mi ⟩ M {v ′ /x}3−i ]{R′ } = E1 [M {v ′ /x}]{R′ }
= E1 [M {v/x}]{R}
Moreover, R12 {R} = (R′1 ∪R′2 ){R′ } and S{R} = S{R′ }, so φ′#R = (E1 [M {v/x}], R12 , S){R}.
On the other hand, if R(m) = λx.m′′ x then:
E[⟨mi ⟩ M {v ′ /x}3−i ]{R′ } = E[m′′ v ′ ]{R′ }
= E[m′′ v]{R} = E[mv]{R}
so φ#R = φ′#R .
′

34

– Finally, the cases for method-return reductions are treated similarly as above.
⃗ S).
Suppose now φ#R Ô
Ô⇒ φ′ , where recall that we write φ as (E1 [M1 ]∥⋯∥EN [MN ], R,
We show by induction on sizeR (E1 [M1 ], ⋯, EN [MN ]) that φ Ô
Ô⇒′ φ′′ and φ′ RR′ φ′′
for some R′ ⊇ R. The size-function we use measures the length of G(R)-paths that
appear inside its arguments:
sizeR (E1 [M1 ], ⋯, EN [MN ]) = sizeR (E1 [M1 ]) + ⋯ + sizeR (EN [MN ])
sizeR (E[M ]) = ∑ 2∣m∣R + ∑ 1
m∈X1

m∈X2

where X1 is the multiset containing all occurrences of methods m ∈ dom(R) inside
E[M ] in call position (e.g. mM ′ ), and X2 contains all occurrences of methods m ∈
dom(R) inside E[M ] in return position (i.e. ⟨mi ⟩ ⋯). We write ∣m∣R for the length of
the unique directed path from m to a leaf in G(R). The fact that X1 , X2 are multisets
reflects that we count all occurrences of m in call/return positions. Suppose WLOG
that the reduction to φ′ is due to some (E1 [M1 ], R12 , S){R} Ð
→1 (E ′ [M ′ ], R′ , S ′ ).
If the reduction happens inside M1 {R} (this case also encompasses the base case of
the induction) then the only case we need to examine is that of the reduction being a
method call. In such a case, suppose we have E1 [M1 ]{R} = E[mv], E ′ = E, M ′ =
M {v/x} and R12 {R}(m) = λx.M . Then, E1 [M1 ] = Ẽ[m̃i ṽ] for some Ẽ, m̃, ṽ such
that m̃{R} = m, ṽ{R} = v and Ẽ{R} = E. If m =/ m̃ then, supposing R(m̃) = λx.m̃′ x
we have the following cases:
⃗ S) Ð
⃗ S) = φ′′
– (Ẽ[m̃i ṽ], R,
→′1 (Ẽ[m̃′i ṽ], R,
1
i
′
i
⃗
⃗ ′ , S) = φ′′ , with R
⃗′ = R
⃗ ⊎3−i {m′ ↦
– (Ẽ[m̃ ṽ], R, S) Ð
→1 (Ẽ[⟨m̃ ⟩(m̃′ v ′ )3−i ], R
1
j
λx.mj x ∣ 1 ≤ j ≤ k}, etc.
Let φ′′ be the extension of φ′′1 to an N -quadruple by using the remaining Ei [Mi ]’s of φ,
so that φ Ô
Ô⇒′ φ′′ . In the first case above we have that φ′′#R = φ, and in the latter that
′
φ′′#R = φ (with R′ = R ⊎ {m′j ↦ λx.mj x ∣ 1 ≤ j ≤ k}), and we appeal to the IH.
Suppose now that m̃ = m and R12 (m) = λx.M̃ . Then, one of the following is the case:
⃗ S), R,
⃗ S) Ð
⃗ S) = φ′′
– (Ẽ[m̃i ṽ], R,
→′1 (Ẽ[M̃ {ṽ/x}i ], R,
1
i
′
i
′
3−i
⃗
⃗ ′ = R⊎
⃗ 3−i {m′ ↦
⃗ ′ , S) = φ′′ , with R
– (Ẽ[m̃ ṽ], R, S) Ð
→1 (Ẽ[⟨m̃ ⟩ M̃ {v /x} ], R
1
j
λx.mj x ∣ 1 ≤ j ≤ k}, etc.
Extending φ′′1 to φ′′ as above, in the former case we then have that φ′′#R = φ′ , and in
′
the latter that φ′′#R = φ′ , as required.
Finally, let us suppose that M1 is some value v. Then, we can write E1 as E1 =
E2 [E ′ ], with E ′ coming from the grammar E ′ ∶∶= ● ∣ ⟨mi ⟩ E ′ and E2 not being of
the form E ′′ [⟨mi ⟩ ●]. Observe that E1 = E2 . If E ′ = ● then by a case analysis on E1
⃗ S) Ð
we can see that φ#R can simulate the reduction. Otherwise, (E2 [E ′ [v]], R,
→′1
′′ ′i
′
′
′′
i
′
′
⃗
⃗
⃗
(E2 [E [v ]], R , S) whereby E = E [⟨m ⟩ ●] and R = R ⊎3−i {mj ↦ λx.mj x ∣ 1 ≤
j ≤ k}, etc. We have that
⃗ ′ , S){R′ } = (E2 [E ′ [v]], R,
⃗ S){R}
φ′′1 = (E2 [E ′′ [v ′i ]], R
and hence, extending φ′′1 to φ′′ , we have φ′′#R = φ#R . We can now appeal to the
IH.
′

35

C.2

Lemma 51

Let ρ ≍ ρ′ be compatible N -configurations. Then, (ρ ⊘ ρ′ ) ∼ (ρ ⩕ ρ′ ).
We prove that the relation R = {(ρ1 ⊘ ρ2 , ρ1 ⩕ ρ2 ) ∣ ρ1 ≍ ρ2 } is a bisimulation. Let us
suppose that (ρ1 ⊘ ρ2 , ρ1 ⩕ ρ2 ) ∈ R.
– Suppose ρ1 ⊘ρ2 ↪1 ρ′1 ⊘ρ′2 . If the transition is due to (I NT 1) then ρ2 = ρ′2 and we can
see that ρ1 ⩕ ρ2 Ô
Ô⇒′ ρ′1 ⩕ ρ2 . Similarly if the transition is due to (I NT 2). Suppose
(1,call m(v))

(1,call m(v))

now we used instead (C ALL), e.g. ρ1 ÔÔÔÔÔ⇒ ρ′1 and ρ2 ÔÔÔÔÔ⇒ ρ′2 , and
let us consider the case where v ∈ Meths (the other case is simpler). Then, assuming
ρ1 = (C11 ∥⋯, R1 , P1 , A1 , S1 ) and ρ2 = (C12 ∥⋯, R2 , P2 , A2 , S2 ), we have that either
of the following scenarios holds, for some x ∈ {K, L}: C11 = (E1 , E[mm′ ]), C12 =
(E2 , −) and
call m(v)

(E1 , E[mm′ ], R1 , P1 , A1 , S1 ) ÐÐÐÐÐ→1
(m ∶∶ E ∶∶ E1 , R1 ⊎ (v ↦ λx.m′ x), P1 ∪x {v}, A1 , S1 )
call m(v)

(E2 , −, R2 , P2 , A2 , S2 ) ÐÐÐÐÐ→1
(m ∶∶ E2 , M {v/x}, R2 , P1 , A1 ∪x {v}, S2 )
or its dual, where ρ2 contains the code initiating the call. Focusing WLOG in the
former case and setting S = S1 ⊎ S2 :
ρ1 ⩕ ρ2 = ((E1 ⩕ E2 )[E[m1 m′ ]]∥⋯, R1 , R2 , S)
↪2 ((E1 ⩕ E2 )[E[⟨m1 ⟩ M {v/x}2 ]]∥⋯, R′1 , R2 , S)
= ρ′1 ⩕ ρ′2

(R′1 = R1 ⊎ (v ↦ λx.m′ x))

The case for (R ETN) is treated similarly.
⃗ S) ↪2 (E[M ′ ]∥ M2 ∥⋯∥MN , R
⃗ ′, S′)
– Suppose ρ1 ⩕ ρ2 = (E[M1 ]∥M2 ∥⋯∥MN , R,
1
′′
and let ρ1 = ((E1 , M1 )∥⋯, R1 , P1 , A1 , S1 ) and ρ2 = ((E2 , −)∥⋯, R2 , P2 , A2 , S2 ),
where (E1 ⩕ E2 )[M1′′ ] = E[M1 ]. If the redex M1 is not of the forms M1 = m1 v
or M1 = ⟨m1 ⟩ v, with m ∈ dom(R2 ), then the reduction can clearly be simulated
by ρ1 ⊘ ρ2 (internally, by ρ1 ). Otherwise, similarly as above, the reduction can be
simulated by a mutual call/return of m.
Finally, it is clear that ρ1 ⊘ ρ2 is final iff ρ1 ⩕ ρ2 is final.

D

General compositionality

This compositionality result will allow us to compose histories of component libraries in
order to obtain those of their composite library. Let L1 ∶ Θ1 → Θ2 and L2 ∶ Θ1′ → Θ2′ .
The semantic composition will be guided by two sets of names Π, P. Π contains
method names that are shared between by the respective libraries and their context.
Thus Π ⊇ Θ1 ∪ Θ1′ ∪ Θ2 ∪ Θ2′ . The names in P, on the other hand, will be used for
private communication between L1 and L2 . Consequently, Π ∩ P consists of names that
can be used both for internal communication between L1 and L2 , and for contextual
interactions, i.e. Π ∩ P = (Θ1 ∪ Θ1′ ) ∩ (Θ2 ∪ Θ2′ ).
36

Given hi ∈ JLi K(i = 1, 2), we define the composition of h1 and h2 , written h1 ⩕σΠ,P
h2 , as a partial operation depending on Π, P and an additional parameter σ ∈ {0, 1, 2}∗
which we call a scheduler. It is given inductively as follows. We let  ⩕Π,P  =  and:
σ
(t, call m(v))s1 ⩕0σ
Π,P (t, call m(v))s2 = s1 ⩕Π,P′ s2
σ
(t, ret m(v))s1 ⩕0σ
Π,P (t, ret m(v))s2 = s1 ⩕Π,P′ s2
σ
(t, call m(v))P Y s1 ⩕1σ
Π,P s2 = (t, call m(v))P Y (s1 ⩕Π ′ ,P s2 )
σ
(t, ret m(v))P Y s1 ⩕1σ
Π,P s2 = (t, ret m(v))P Y (s1 ⩕Π ′ ,P s2 )
σ
(t, call m(v))OY s1 ⩕1σ
Π,P s2 = (t, call m(v))OY (s1 ⩕Π ′ ,P s2 )
σ
(t, ret m(v))OY s1 ⩕1σ
Π,P s2 = (t, ret m(v))OY (s1 ⩕Π ′ ,P s2 )

along with the dual rules for the last four cases (i.e. where we schedule 2 in each case).
Note that the definition uses sequences of moves that are suffixes of histories (such as
si ). The above equations are subject to the following side conditions:
– Meths(v) ∩ (Π ∪ P) = ∅, Π ′ = Π ⊎ Meths(v) and P′ = P ⊎ Meths(v);
– m ∈ P in the 0-scheduling cases;
– m ∈ Π in the 1-scheduling cases and, also, m ∈ Π ∖ P in the third case (the P -call);
– in the 1-scheduling cases, we also require that the leftmost move with thread index t
in s2 is not a P -move.
History composition is a partial function: if the conditions above are not met, or h1 , h2 , σ
are not of the appropriate form, then the composition is undefined. The above conditions
ensure that the composed histories are indeed compatible and can be produced by
composing actual libraries. For instance, the last condition corresponds to determinacy
of threads: there can only be at most one component starting with a P -move in each
thread t. We then have the following correspondence.
Theorem 53. If L1 ∶ Θ1 → Θ2 and L2 ∶ Θ1′ → Θ2′ access disjoint parts of the store then
JL1 ∪ L2 KN = { h ∈ H ∣ ∃σ, h1 ∈JL1 KN, h2 ∈JL2 KN. h = h1 ⩕σΠ0 ,P0 h2 }
with Π0 = Θ1 ∪ Θ2 ∪ Θ1′ ∪ Θ2′ and P0 = (Θ1 ∪ Θ1′ ) ∩ (Θ2 ∪ Θ2′ ).
The rest of this section is devoted in proving the Theorem.
Recall that we examine library composition in the sense of union of libraries. This
scenario is more general than the one of Appendix C as, during composition via union,
the calls and returns of each of the component libraries may be caught by the other library
or passed as a call/return to the outer context. Thus, the setting of this section comprises
given libraries L1 ∶ Θ1 → Θ2 and L2 ∶ Θ1′ → Θ2′ , such that Θ2 ∩ Θ2′ = ∅, and relating
their semantics to that of their union L1 ∪ L2 ∶ (Θ1 ∪ Θ1′ ) ∖ (Θ2 ∪ Θ2′ ) → Θ2 ∪ Θ2′ .
Given configurations for L1 and L2 , in order to be able to reduce them together we
need to determine which of their methods can be used for communication between them,
and which for interacting with the external context, which represents player O in the
game. We will therefore employ a set of method names, denoted by Π and variants, to
register those methods used for interaction with the external context. Another piece of
37

information we need to know is in which component in the composition was the last
call played, or whether it was an internal call instead. This is important so that, when O
(or P ) has the choice to return to both components, in the same thread, we know which
one was last to call and therefore has precedence. We use for this purpose sequences
w = (w1 , ⋯, wN ) where, for each i, wi ∈ {0, 1, 2}∗ . Thus, if e.g. w1 = 2w1′ , this would
mean that, in thread 1, the last call to O, was done from the second component; if, on the
other hand, w1 = 0w1′ then the last call in thread 1 was an internal one between the two
components. Given such a w and some j ∈ {0, 1, 2}, for each index t, we write j +t w
for w[t ↦ (jwt )].
Let us fix libraries L1 ∶ Θ1 → Θ2 and L2 ∶ Θ1′ → Θ2′ . Let ρ1 , ρ2 be N -configurations,
⃗ R, P, A, S) and ρ2 =
and in particular L-configurations, and suppose that ρ1 = (C,
′
′
′
′
′
′
′
⃗
(C , R , P , A , S ). Moreover, let Θ1 ∪ Θ2 ∪ Θ1 ∪ Θ2 ⊆ Π. We say that ρ1 and ρ2 are
′
(w, Π)-compatible, written ρ1 ≍w
Π ρ2 , if S, S have disjoint domains and, for each i;
– Ci = (EL′ , M ) and Ci′ = (EL , −), or Ci = (EL , −) and Ci′ = (EL′ , M ), or Ci = (EL1 , −)
and Ci′ = (EL2 , −).
′
– We have Θ1 ⊆ Al , Θ2 ⊆ PK , Θ1′ ⊆ A′L , Θ2′ ⊆ PK
and, setting
′
P = (PK ∩ A′L ) ⊎ (PL ∩ A′K ) ⊎ (PK
∩ AL ) ⊎ (Pl′ ∩ AK )

we also have:
′
● (PL ⊎ PK ⊎ Al ⊎ AK ) ∩ (PL′ ⊎ PK
⊎ A′l ⊎ A′K ) = P ⊎ (Θ1 ∩ Θ1′ ),
′
′
● Π ∩ P = (Θ2 ∪ Θ2 ) ∩ (Θ1 ∪ Θ1 ),
′
● Π ∪ P = PL ∪ PK ∪ Pl′ ∪ PK
∪ AL ∪ AK ∪ A′L ∪ A′K .
– The private names of R do not appear in ρ2 , and dually for the private names of R′ .
– If Ci = (E, ⋯) and Ci′ = (E ′ , ⋯) then E and E ′ are wi -compatible, that is, either
E = E ′ = [] or:
● E = m ∶∶ E1 and E ′ ∈ EL , with m ∈ Π, wi = 1u and E1 , E ′ are u-compatible,
● or E = m ∶∶ E1 and E ′ = m ∶∶ E ∶∶ E2 , with m ∈ P, wi = 0u and E1 , E2 are
u-compatible,
● or E = m ∶∶ E ∶∶ E1 and E ′ ∈ EL , with m ∈ Π ∖ P, wi = 1u and E1 , E ′ are
u-compatible,
or the dual of one of the three conditions above holds.
w
Given ρ1 ≍w
Π ρ2 , we let their external composition be denoted as ρ1 ⊗Π ρ2 (and note
that now the notation is symmetric for ρ1 and ρ2 ) and define the semantics for external

38

composition by these rules:
ρ1 Ô
Ô⇒ ρ′1
I NT1
′
w
ρ1 ⊗ w
Π ρ2 Ð→ ρ1 ⊗Π ρ2
(t,call m(v))

ρ1 ÔÔÔÔÔ⇒ ρ′1

(t,call m(v))

ρ2 ÔÔÔÔÔ⇒ ρ′2

0+t w ′
′
ρ 1 ⊗w
ρ2
Π ρ2 Ð→ ρ1 ⊗Π
(t,ret m(v))

ρ1 ÔÔÔÔÔ⇒ ρ′1

C ALL (m ∈ P)

(t,ret m(v))

ρ2 ÔÔÔÔÔ⇒ ρ′2

′
tw
ρ1 ⊗0+
ρ2 Ð→ ρ′1 ⊗w
Π ρ2
Π

R ETN (m ∈ P)

(t,call m(v))P Y

ρ1 ÔÔÔÔÔÔÔ⇒ ρ′1
ρ 1 ⊗w
Π

(t,call m(v))P Y

ρ2 ÐÐÐÐÐÐÐÐ→

ρ′1

tw
⊗1+
Π′

PC ALL1 (m ∈ Π ∖ P)
ρ2

(t,ret m(v))P Y

ρ1 ÔÔÔÔÔÔ⇒ ρ′1
(t,ret m(v))P Y

tw
ρ1 ⊗1+
ρ2 ÐÐÐÐÐÐÐÐ→ ρ′1 ⊗w
Π ′ ρ2
Π

PR ETN1 (m ∈ Π)

(t,call m(v))OY

ρ1 ÔÔÔÔÔÔÔ⇒ ρ′1
(t,call m(v))OY

1+t w
′
ρ 1 ⊗w
ρ2
Π ρ2 ÐÐÐÐÐÐÐÐ→ ρ1 ⊗Π ′

OC ALL1 (m ∈ Π)

(t,ret m(v))OY

ρ1 ÔÔÔÔÔÔÔ⇒ ρ′1
(t,ret m(v))OY

tw
ρ1 ⊗1+
ρ2 ÐÐÐÐÐÐÐÐ→ ρ′1 ⊗w
Π ′ ρ2
Π

OR ETN1 (m ∈ Π ∖ P)

along with their dual counterparts (I NT2 , XC ALL2 , XR ETN2 ). The internal rules above
have the same side-conditions on name privacy as before. Moreover, in (XR ETNi) and
(XC ALLi), for X=O,P, we let Π ′ = Π ⊎t Meths(v) and impose that the t-th component
of ρ3−i be an O-configuration and Meths(v) ∩ Meths(ρ3−i ) = ∅.
We can now show the following.
s

w
′
Lemma 54. Let ρ1 ≍w
Ð→∗ ρ′1 ⊗w
Π ρ2 and suppose ρ1 ⊗Π ρ2 Ð
Π ′ ρ2 for some sequence s
′ w′ ′
of moves. Then, ρ1 ≍Π ′ ρ2 .
′

We next juxtapose the semantics of external composition to that obtained by internally composing the libraries and then deriving the multi-threaded semantics of the
result. As before, we call the latter form internal composition. The traces we obtain
are produced from a transition relation, written Ô
Ô⇒′ , between configurations of the
⃗ R,
⃗ P, A, S). In particular, in each
form (C1 ∥⋯∥CN , R1 , R2 , P, A, S), also written (C,
Ci = (Ei , Xi ) with Xi = Ei [Mi ] or Xi = −, Ei is selected from the extended evaluation
contexts and Ei is an extended L-stack, that is, of either of the following two forms:
′
Eext ∶∶= [] ∣ mi ∶∶ E ∶∶ Eext

′
Eext
∶∶= m ∶∶ Eext

where E is again from the extended evaluation contexts.
First, given u-compatible evaluation stacks E, E ′ , we construct a pair E ⩕u E ′ consisting of an extended evaluation context and an extended L-stack, as follows. Given
39

E ⩕u E ′ = (E ′ , E ′′ ):
(m ∶∶ E ∶∶ E) ⩕0u (m ∶∶ E ′ ) = (E ′ [E[⟨m⟩ ●]1 ], E ′′ )
(m ∶∶ E) ⩕0u (m ∶∶ E ∶∶ E ′ ) = (E ′ [E[⟨m⟩ ●]2 ], E ′′ )
(m ∶∶ E) ⩕1u E ′ = E ⩕2u (m ∶∶ E ′ ) = (●, m ∶∶ E ′ ∶∶ E ′′ )
(m ∶∶ E ∶∶ E) ⩕1u E ′ = E ⩕2u (m ∶∶ E ∶∶ E ′ )
= (●, m ∶∶ E ′ [E] ∶∶ E ′′ ) if E ′ ∈ EL
and [] ⩕ [] = (●, []).
For each pair ρ1 ≍w
Π ρ2 , we define a configuration corresponding to their syntactic
′
composition as follows. Let ρ1 = (C1 ∥⋯∥CN , R1 , P1 , A1 , S1 ) and ρ2 = (C1′ ∥⋯∥CN
, R2 , P2 , A2 , S2 )
′
′
′
u ′
′′
and, for each i, Ci = (Ei , Xi ) and Ci = (Ei , Xi ). If Ei ⩕ Ei = (Ei , Ei ), we set:
Ci ⩕

u

Ci′

⎧
(Ei′′ , Ei [M 1 ])
⎪
⎪
⎪
⎪ ′′
= ⎨(Ei , Ei [M 2 ])
⎪
⎪
′′
⎪
⎪
⎩(Ei , −)

if Xi = M and Xi′ = −
if Xi = − and Xi′ = M
if Xi = Xi′ = −

We then let the internal composition of ρ1 and ρ2 be:
w1 ′
wN ′
ρ1 ⩕w
CN , R1 , R2 , P ′ , A′ , S1 ⊎ S2 )
Π ρ2 = (C1 ⩕ C1 ∥⋯∥CN ⩕

where we set P ′ = ((P1L ⊎ P2L ) ∩ Π, (P1K ⊎ P2K ) ∩ Π) and A′ = ((A1L ∪ A2L ) ∩
(Π ∖ P), (A1K ⊎ A2K ) ∩ Π).
Now, as expected, the definition of Ô
Ô⇒′ builds upon Ð
→′t . The definition of the latter
is given by the following rules.
⃗ S) Ð
⃗ ′, S′)
(E[M ], R,
→′t (E ′ [M ′ ], R
(I NT′ )
⃗ P, A, S) Ð
⃗ ′ , P, A, S ′ )
(E, E[M ], R,
→′ (E, E ′ [M ′ ], R
t

⃗ P, A, S)
(E, E[m v], R,
i

call m(v ′ )P Y
ÐÐÐÐÐÐÐ→t′

⃗ ′ , P ′ , A, S)
(mi ∶∶E ∶∶ E, −, R

(PQ Y′ )

′

ret m(v )P Y ′
⃗ P, A, S) ÐÐÐÐÐÐ→
⃗′ ′
(m ∶∶ E, v, R,
t (E, −, R , P , A, S)

(PAY′ )

call m(v)OY ′
i ⃗
′
⃗ P, A, S) ÐÐÐÐÐÐ→
(E, −, R,
t (m ∶∶ E, M {v/x} , R, P, A , S)

(OQ Y′ )

⃗ P, A, S) ÐÐÐÐÐÐ→t′ (E, E[v i ], R,
⃗ P, A′ , S)
(mi ∶∶E ∶∶ E, −, R,

(OAY′ )

ret m(v)OY

The side-conditions are similar to those for the relation Ð
→t between ordinary configurations, with the following exceptions: in (PQ Y′ ), if Meths(v) = {m1 , ⋯, mk } then
⃗′ = R
⃗ ⊎i {m′ ↦ λx.mj x}; and in
v ′ = v{m′j /mj ∣ 1 ≤ j ≤ k}, for fresh m′j ’s, and R
j
′
′
′
⃗
⃗
(PAY ), if m ∈ dom(Ri ) then R = R ⊎i {mj ↦ λx.mj x}, etc. Moreover, in (OQ Y′ )
we have that m ∈ dom(Ri ). Finally, we let
(t,x)XY ′
⃗ R,
⃗ P, A, S) ÔÔÔ⇒
⃗ ↦ C ′ ], R
⃗ ′ , P ′ , A′ , S ′ )
(C,
(C[t

⃗ P, A, S) ÐÐÐ→t′ (C ′ , R
⃗ ′ , P ′ , A′ , S ′ ).
just if (Ct , R,
xXY

40

We next relate the transition systems induced by external (via ⊗) and internal composition (via ⩕). Let us write (S1 , ↪1 , F1 ) for the transition system induced by external
composition of compatible N -configurations (so ↪1 is Ð→), and (S2 , ↪2 , F2 ) be the
one for internal composition (so ↪2 is Ô
Ô⇒′ ). Finality of extended N -configurations
⃗ ⋯) is defined as expected: all Ci ’s must be ([], −). A relation R ⊆ S1 ×S2
(C1 ∥⋯∥CN , R,
is called a bisimulation if, for all (x1 , x2 ) ∈ R:
– x1 ∈ F1 iff x2 ∈ F2 ,
– if x1 ↪1 x′1 then x2 ↪2 x′2 and (x′1 , x′2 ) ∈ R,
(t,x)XY

(t,x)XY

(t,x)XY

(t,x)XY

– if x1 ,ÐÐÐÐ→1 x′1 then x2 ,ÐÐÐÐ→2 x′2 and (x′1 , x′2 ) ∈ R,
– if x2 ↪2 x′2 then x1 ↪1 x′1 and (x′1 , x′2 ) ∈ R,
– if x2 ,ÐÐÐÐ→2 x′2 then x1 ,ÐÐÐÐ→1 x′1 and (x′1 , x′2 ) ∈ R.
Again, we say that x1 and x2 are bisimilar, and write x1 ∼ x2 , if there exists a bisimulation R such that (x1 , x2 ) ∈ R.
′
w ′
w ′
Lemma 55. Let ρ ≍w
Π ρ be compatible N -configurations. Then, (ρ ⊗Π ρ ) ∼ (ρ ⩕Π ρ ).
w
w
Proof. We prove that the relation R = {(ρ1 ⊗w
Π ρ2 , ρ1 ⩕Π ρ2 ) ∣ ρ1 ≍Π ρ2 } is a bisimuw
w
lation. Let us suppose that (ρ1 ⊗Π ρ2 , ρ1 ⩕Π ρ2 ) ∈ R.
(t,x)

′
ÐÐ→ ρ′1 ⊗w
– Let ρ1 ⊗w
Π ρ2 Ð
Π ′ ρ2 with the transition being due to (XC ALL 1 ), e.g.
′

(1,call m(v))

ρ1 ÔÔÔÔÔ⇒ ρ′1 and ρ′2 = ρ2 , w′ = 1 +1 w and Π ′ = Π ⊎1 Meths(v), Meths(v) =
{m′1 , ⋯, m′j }, and recall that Meths(v) ∩ Meths(ρ2 ) = ∅. Then, assuming ρ1 =
(C11 ∥⋯, R1 , P1 , A1 , S1 ), we have that one of the following holds, for some x ∈
{K, L}:
call m(v)

C11 = (E1 , E[mv ′ ]) and (C11 , R1 , P1 , A1 , S1 ) ÐÐÐÐÐ→1
(m ∶∶ E ∶∶ E1 , −, R1 ⊎ {m′j ↦ λx.mj x ∣ 1 ≤ j ≤ k}, P1 ∪x Meths(v), A1 , S1 )
call m(v)

C11 = (E1 , −) and (C11 , R1 , P1 , A1 , S1 ) ÐÐÐÐÐ→1
(m1 ∶∶ E1 , mv, R1 , P1 , A1 ∪x Meths(v), S1 )
In the former case, if ρ2 = ((E2 , −)∥⋯, R2 , P2 , A2 , S2 ) with E1 ⩕w1 E2 = (E ′ , E),
we get:
′
′ 1
ρ1 ⩕w
Π ρ2 = ((E, E [E[mv ] ])∥⋯, R1 , R2 , P, A, S)
(1,call m(v))

ÔÔÔÔÔ⇒′
(m1 ∶∶ E ′ [E 1 ] ∶∶ E, −)∥⋯, R1 ⊎ {m′j ↦ λx.mj x ∣ 1 ≤ j ≤ k}, R2 , P ′, A, S)
with P, A as in the definition of composition and P ′ = P ∪x Meths(v), and the latter
′
N -configuration equals ρ′1 ⩕w
Π ′ ρ2 . The other case is treated in the same manner, and
we work similarly for (R ETN1 ).
– On the other hand, if the transition is due to (C ALL) or (R ETN) then we work as in
the proof of Lemma 51.
41

(1,call m(v))
′
′
⃗
⃗′ ′ ′
– Suppose ρ1 ⩕w
Π ρ2 = (C1 ∥⋯, R, P, A, S) ÔÔÔÔÔ⇒ (C1 ∥⋯, R , P , A , S). Then,
assuming WLOG that v ∈ Meths, one of the following must be the case, for some
x ∈ {K, L} and i ∈ {1, 2}:
call m(v) ′
⃗ P, A, S) Ð
C1 = (E, E[mi v ′ ]) and (C1 , R,
ÐÐÐÐ→1
i
′
⃗
(m ∶∶ E ∶∶ E, R ⊎i {mj ↦ λx.mj x ∣ 1 ≤ j ≤ k}, P ∪x Meths(v), A, S)

⃗ P, A, S) ÐÐÐÐÐ→1′
C1 (E, −) and (C1 , R,
call m(v)

⃗ P, A ∪x Meths(v), S)
(m ∶∶ E, M {v/x}i , R,
We only examine the former case, as the latter one is similar, and suppose that
i = 1. Taking ρj = (C1j ∥⋯, Rj , Pj , Aj , Si ), for j = 1, 2, we have that (C11 , C12 ) =
((E1 , E ′ [mv ′ ], (E2 , −)), for some E, E1 , E2 such that E1 ⩕w1 E2 = (E ′′ , E) and E =
E ′′ [E ′1 ]. Moreover, taking R′1 = R1 ⊎{m′j ↦ λx.mj x ∣ 1 ≤ j ≤ k}, P1′ = P1 ⊎x {v},
w′ = 1 +1 w and Π ′ = Π ⊎ Meths(v) (note Meths(v) = {m′1 , ⋯, m′k }),
(1,call m(v))

′

′

′
′
′
w
′
w
ρ1 ⊗ w
Π ρ2 ÐÐÐÐÐÐÐ→ ((m ∶∶ E ∶∶ E1 , −)∥⋯, R1 , P1 , A1 , S1 ) ⊗Π ′ ρ2 = ρ1 ⊗Π ′ ρ2
′
′
⃗′ ′ ′
and ρ′1 ⩕w
Π ′ ρ2 = (C1 ∥⋯, R , P , A , S) as required. The case for return transitions is
similar.
– On the other hand, if the transition out of ρ1 ⩕w
Π ρ2 does not have a label then we
work as in the proof of Lemma 51.

w
Moreover, by definition of syntactic composition, ρ1 ⊗w
Π ρ2 is final iff ρ1 ⩕Π ρ2 is.
h

Given an N -configuration ρ and a history h, let us write ρ ⇓ h if ρ Ô
Ô⇒ ρ′ for
′
⃗
⃗
some final configuration ρ . Similarly if ρ is of the form (C, R, P, A, S). We have the
following connections in history productions. The next lemma is proven in a similar
fashion as Lemma 50.
Lemma 56. For any legal (M1 ∥⋯∥MN , R1 , R2 , P, A, S) and history h, we have that
(M1 ∥⋯∥MN , R1 , R2 , P, A, S) ⇓ h iff (M1 ∥⋯∥MN , R1 ∪ R2 , P, A, S) ⇓ h.
w
Lemma 57. For any compatible N -configurations ρ1 ≍w
Π ρ2 and history h, (ρ1 ⊗Π ρ2 ) ⇓
h iff:
∃h1 , h2 , σ. ρ1 ⇓ h1 ∧ ρ2 ⇓ h2 ∧ h = h1 ⩕σΠ,P h2

where P is computed from ρ1 , ρ2 and Π as before.
Proof. We show that, for any compatible N -configurations ρ1 ≍w
Π ρ2 and history suffix
s, (ρ1 ⊗w
Π ρ2 ) ⇓ s iff:
∃s1 , s2 , σ. ρ1 ⇓ s1 ∧ ρ2 ⇓ s2 ∧ s = s1 ⩕σΠ,P s2
where P is computed from ρ1 , ρ2 and Π as in the beginning of this section.
The left-to-right direction follows from straightforward induction on the length of
the reduction that produces s. For the right-to-left direction, we do induction on the
42

length of σ. If σ =  then s1 = s2 = s = . Otherwise, we do a case analysis on the first
element of σ. We only look at the most interesting subcase, namely of σ = 0σ ′ . Then,
for some m ∈ P:
s1 = (t, call m(v))s′1

s2 = (t, call m(v))s′2

w
′
w
′
By ρi ⇓ si and ρ1 ≍w
Π ρ2 we have that ρ1 ⊗Π ρ2 Ð→ ρ1 ⊗Π ρ2 , where w = 0 +t w and
′ w′ ′
′
′
′
σ′
′
′
w′ ′
ρ1 ≍Π ρ2 . Also, ρi ⇓ si and s = s1 ⩕Π,P′ s2 so, by IH, (ρ1 ⊗Π ρ2 ) ⇓ s.
′

We can now prove the correspondence between the traces of component libraries
and those of their union.
Theorem 53 Let L1 ∶ Θ1 → Θ2 and L2 ∶ Θ1′ → Θ2′ be libraries accessing disjoint parts
of the store. Then,
JL1 ∪ L2 KN = {h ∈ HL ∣ ∃σ, h1 ∈JL1 KN, h2 ∈JL2 KN. h = h1 ⩕σΠ0 ,P0 h2 }
with Π0 = Θ1 ∪ Θ2 ∪ Θ1′ ∪ Θ2′ and P0 = (Θ1 ∪ Θ1′ ) ∩ (Θ2 ∪ Θ2′ ).
Proof. Let us suppose (Li ) Ð→∗lib (, Ri , Si ), for i = 1, 2, with dom(R1 ) ∩ dom(R2 ) =
dom(S1 ) ∩ dom(S2 ) = ∅. We set:
ρ1 = (([], −)∥⋯∥([], −), R1 , (∅, Θ2 ), (Θ1 , ∅), S1 )
ρ2 = (([], −)∥⋯∥([], −), R2 , (∅, Θ2′ ), (Θ1′ , ∅), S2 )
We pick these as the initial configurations for JL1 KN and JL2 KN respectively. Then,
(L1 ∪ L2 ) Ð→∗lib (, R0 , S0 ) where R0 = R1 ⊎ R2 and S0 = S1 ⊎ S2 , and we take
ρ0 = (([], −)∥⋯∥([], −), R0 , (∅, Θ2 ∪ Θ2′ ), ((Θ1 ∪ Θ1′ ) ∖ P0 , ∅), S0 )
as the initial N -configuration for JL1 ∪ L2 KN . On the other hand, we have ρ1 ⩕Π0 ρ2 =
(([], −)∥⋯∥([], −), R1 , R2 , (∅, Θ2 ∪ Θ2′ ), ((Θ1 ∪ Θ1′ ) ∖ P0 , S0 ). From Lemma 56, we
have that ρ0 ⇓ h iff ρ1 ⩕Π0 ρ2 ⇓ h, for all h.
Pick a history h. For the forward direction of the claim, ρ0 ⇓ h implies ρ1 ⩕Π0 ρ2 ⇓ h
which, from Lemma 55, implies ρ1 ⊗Π0 ρ2 ⇓ h. We now use Lemma 57 to obtain
h1 , h2 , σ such that ρi ⇓ hi and h = h1 ⩕σΠ0 ,P0 h2 . Conversely, suppose that hi ∈ JLi KN
and h = h1 ⩕σΠ0 ,P0 h2 . WLOG assume that (Meths(h1 ) ∪ Meths(h2 )) ∩ (dom(R1 ) ∪
dom(R2 )) ⊆ Π0 (or we appropriately alpha-covert R1 and R2 ). Then, ρi ⇓ hi , for
i = 1, 2, and therefore ρ1 ⊗Π0 ρ2 ⇓ h by Lemma 57. By Lemma 55 we have that
ρ1 ⩕Π0 ρ2 ⇓ h, which in turn implies that ρ0 ⇓ h, i.e. h ∈ JL1 ∪ L2 KN .

E
E.1

Composition congruence
Proof of Theorem 36

Proof. Assume L1 ⊑ L2 and suppose h1 ∈ JL ∪ L1 K. By Theorem 53, h1 = h′ ⩕σΠ,P h′1 ,
where h′ ∈ JLK and h′1 ∈ JL1 K. Because L1 ⊑ L2 , there exists h′2 ∈ JL2 K such that
h′1 ⊑ h′2 , i.e. h′1 ◁∗P O h′2 . Note that some of the rearrangements necessary to transform h′1
into h′2 may concern actions shared by h′1 and h′ ; their polarity will then be different in
h′ . Let h′′ be obtained by applying such rearrangements to h′ . We claim that h′ ◁∗OP h′′ .
43

Indeed, suppose that (t′ , x′ )(t, x)P are consecutive in h′1 , but swapped in order to obtain
h′2 , and (t, x)P appears in h′ as (t, x)O . Now, the move (t′ , x′ ) either appears in h1 , or
it appears in h′ and gets hidden in h1 . In every case, let s contain the moves of h′ that
are after (t′ , x′ ) in the composition to h1 , and before (t, x)O . We have that s(t, x)O is
a subsequence of h′ and h′ ◁∗OP h′′ holds just if s contains no moves from t. But, if s
contained moves from t then the rightmost one such would be some (t, y)P . Moreover, in
the composition towards h1 , the move would be scheduled with 1. The latter would break
the conditions for trace composition as, at that point, the corresponding subsequence of
h′1 has as leftmost move in t the P-move (t, x)P . We can show similarly that h′ ◁∗OP h′′
holds in the case that the permutation in h′1 is on consecutive moves (t, x)O (t′ , x′ ).
Finally, the rearrangements in h′1 that do not affect moves shared with h′ can be treated
in a simpler way: e.g. in the case of (t′ , x′ )(t, x)P consecutive in h′1 and swapped in h′2 ,
if (t, x)P does not appear in h′ then we can check that h′ cannot contain any t-moves
between (t′ , x′ ) and (t, x) as the conditions for trace composition impose that only O is
expected to play in that part of h′ (and any t-move would swap this polarity).
′
Now, since h′ ∈ JLK, Lemma 34 implies h′′ ∈ JLK. Take h2 to be h′′ ⩕σΠ,P h′2 , where σ ′
is obtained from σ following these move rearrangements. We then have h2 ∈ JL ∪ L2 K.
Moreover, h1 ⊑ h2 thanks to h′1 ⊑ h′2 . Hence, h2 ∈ JL ∪ L2 K and h1 ⊑ h2 . Thus,
L ∪ L1 ⊑ L ∪ L2 .
E.2

Proof of Theorem 43

Proof. Let us consider the first sequencing case (the second one is dual), and assume
that L1 , L2 ∶ Θ → Θ′ and L ∶ Θ′′ → Θ. Assume L1 ⊑enc L2 and suppose h1 ∈ JL ; L1 Kenc .
By Theorem 53, h1 = h′ ⩕σΠ,P h′1 , where h′ ∈ JLK, h′1 ∈ JL1 K and method calls from Θ
are always scheduled with 0. The fact that O cannot switch between L/K components in
(threads of) h1 implies that the same holds for h′ , h′1 , hence h′ ∈ JLKenc and h′1 ∈ JL1 Kenc .
Because L1 ⊑enc L2 , there exists h′2 ∈ JL2 Kenc such that h′1 ⊑ h′2 , i.e. h′1 (◁P O ∪
◇)∗ h′2 . As before, some of the rearrangements necessary to transform h′1 into h′2 may
concern actions shared by h′1 and h′ ; we need to check that these can lead to compatible
h′′ ∈ JLKenc . Let h′′ be obtained by applying such rearrangements to h′ . We claim that
h′ ◁∗OP h′′ . The transpositions covered by ◁P O are treated as in Lemma 36. Suppose
now that (t′ , x′ )P K (t, x)OL are consecutive in h′1 but swapped in order to obtain h′2 ,
and (t, x)OL appears in h′ as (t, x)P K . Now, the move (t′ , x′ ) cannot appear in h′
as it is in L1 ’s K-component (L is the L-component of L1 ). Let s contain the moves
of h′ that are after (t′ , x′ ) in the composition to h1 , and before (t, x)P K . We claim
that s contains no moves from t, so h′ can be directly composed with h′2 as far as this
transposition is concerned. Indeed, if s contained moves from t then, taking into account
the encapsulation conditions, the leftmost one such would be some (t, y)OK . But the
K-component of L is L1 , which contradicts the fact that the moves we consider are
′
consecutive in h′1 . Hence, taking h2 to be h′′ ⩕σΠ,P h′2 , where σ ′ is obtained from σ
following the ◁P O move rearrangements, we have h2 ∈ JL ; L2 Kenc and h1 ⊑enc h2 . Thus,
L ; L1 ⊑enc L ; L2 .
The case of L ⊎ L1 ⊑enc L ⊎ L2 is treated in a similar fashion. In this case, because
of disjointness, the moves transposed in h′1 do not have any counterparts in h′ . Again,
we consider consecutive moves (t′ , x′ )P K (t, x)OL in h′1 that are swapped in order to

44

obtain h′2 . Let s contain the moves of h′ that are after (t′ , x′ ) in the composition to
h1 , and before (t, x). As Θ1 , Θ1′ is first-order, (t, x)OL must be a return move and the
t-move preceding it in h1 must be the corresponding call. The latter is a move in h′1 ,
which therefore implies that there can be no moves from t in s. Similarly for the other
transposition case.
E.3

Proof of Theorem 47

)-closed and L1 ⊑R L2 . Consider h1 ∈
Proof. For the first claim, suppose L is (R
G
JL ; L1 Kenc . By Theorem 53, h1 = h′ ⩕σΠ,P h′1 , where h′ ∈ JLKenc and h′1 ∈ JL1 Kenc .
Since L1 ⊑R L2 , there exists h′2 ∈ JL2 Kenc such that (h′1 ↾ K) ⊑ (h′2 ↾ K) and (h′1 ↾
L) R (h′2 ↾ L). By the permutation-closure of R, we can pick h′2 not to contain any
common names with h′ apart from those in the common moves of h′1 and h′ . Because
)-closed, h′ ∈ JLKenc and (h′ ↾ L) = (h′1 ↾ L) and (h′1 ↾ L) R (h′2 ↾ L),
L is (R
G
we can conclude that there exists h′′ ∈ JLKenc such that (h′′ ↾ K) = (h′2 ↾ L) and
(h′ ↾ L) G (h′′ ↾ L). Applying the corresponding rearrangements to σ, we have that h′′
′
′
and h′2 are compatible, i.e. (h′′ ⩕σΠ,P h′2 ) ∈ JL ; L2 Kenc . Let h2 = h′′ ⩕σΠ,P h′2 . We want
to show h1 ⊑R h2 . To that end, it suffices to make the following observations.
– We have (h1 ↾ K) ⊑ (h2 ↾ K) because (h1 ↾ K) = (h′1 ↾ K), (h′1 ↾ K) ⊑ (h′2 ↾ K)
and (h′2 ↾ K) = (h2 ↾ K).
– We have (h1 ↾ L) G (h2 ↾ L) because (h1 ↾ L) = (h′ ↾ L), (h′ ↾ L) G (h′′ ↾ L)
and (h′′ ↾ L) = (h2 ↾ L).
Consequently L ; L1 ⊑G L ; L2 .
Suppose now L1 ⊑R L2 . Consider h1 ∈ JL1 ; LKenc , i.e. h1 = h′1 ⩕σΠ,P h′ , where
h′1 ∈ JL1 Kenc and h′ ∈ JLKenc . Because L1 ⊑R L2 , there exists h′2 ∈ JL2 Kenc such that
h′1 ⊑R h′2 , i.e. (h′1 ↾ K) ⊑ (h′2 ↾ K) and (h′1 ↾ L)R(h′2 ↾ L). Define h′′ to be h′
in which (h′ ↾ L) = (h′1 ↾ K) was modified by applying the same rearrangements
as those witnessing (h′1 ↾ K) ⊑ (h′2 ↾ K). Consequently h′ ◁∗P O h′′ . By Lemma 40,
h′′ ∈ JLKenc . Moreover, (h′′ ↾ L) = (h′2 ↾ K). Consequently, h′2 and h′′ are compatible
′
for the corresponding σ ′ . Let h2 = h′2 ⩕σΠ,P h′′ ∈ JL2 ; LK. Then we get:
– (h1 ↾ K) = (h′ ↾ K) = (h′′ ↾ K) = (h2 ↾ K);
– (h1 ↾ L) = (h′1 ↾ L), (h′1 ↾ L)R(h′2 ↾ L), (h′2 ↾ L) = (h2 ↾ L).
Consequently h1 ⊑R h2 and, hence, L1 ; L ⊑R L2 ; L.
For the last claim, we observe that because of the type-restrictions, the elements of
JL ⊎ Li Kenc are interleavings of histories from JLKenc and JLi Kenc . Consider now h1 ∈
JL ⊎ L1 Kenc , i.e. h1 = h′ ⩕σΠ,P h′1 , where h′1 ∈ JL1 Kenc and h′ ∈ JLKenc , and let h′2 ∈
JL2 Kenc be such that h′1 ⊑R h′2 . From our previous observation, we have that h′ can
′
still be composed with h′2 , for appropriate σ ′ . Thus, taking h2 = h′ ⩕σΠ,P h′2 , we have
′
′
h2 ∈ JL ⊎ L2 Kenc and, moreover, h1 ⊑R h2 implies h1 ⊑R+ h2 .

45

