Effect-Dependent Transformations for Concurrent Programs
Nick Benton

Martin Hofmann

Vivek Nigam

Microsoft Research, Cambridge, UK

LMU, Munich, Germany

UFPB, João Pessoa, Brazil

nick@microsoft.com

hofmann@ifi.lmu.de

vivek.nigam@gmail.com

of evaluating e will be of type τ with side-effects at most ε, under assumptions Γ (a ‘rely’ condition), on the behaviour of e’s
free variables. The possible interaction points between e and its
environment are restricted to initial states and parameter values,
and final states and results, of e itself and its explicitly-listed free
variables. Furthermore, all those interaction points are visible in
the term and are governed by specific annotations appearing in the
typing judgement.
For shared-variable concurrency, there are many more possible
interactions. An expression’s environment now also includes anything that may be running concurrently and, moreover, atomic steps
of e and its concurrent environment may be arbitrarily interleaved,
so it is no longer sufficient to just consider initial and final states. A
priori, this leads to far fewer equations between programs. For example, X++;X-- may be distinguished from skip by being run concurrently with a command that reads or writes X. But few programs
do anything useful in the presence of unconstrained interference,
so we need ways to describe and control it. Fine-grained, optimistic
algorithms, which rely on custom protocols being followed by multiple threads with concurrent access to a shared data structure, can
significantly outperform ones based on coarse-grained locking, but
are notoriously challenging to write and verify.
There is a huge literature on shared-variable concurrency, from
type systems ensuring race-freedom of programs with locks [1]
to sophisticated semantic models for reasoning about refinement
of fine-grained concurrent datastructures [27]. This paper explores
effect types as a straightforward, lightweight interface language for
modular reasoning about equivalence and refinement, e.g. for safely
transforming sequential composition into parallelism. We show
how the semantics of a simple effect system scales smoothly to the
concurrent setting, allowing us to control interference and prove
non-trivial equivalences, extending (somewhat to our surprise) to
the correctness of some fine-grained algorithms.
We build on a trace semantics for concurrent programs, due to
Brookes [13], which explicitly describes possible interference by
the environment. We extend Brookes’s semantics to a higher-order
language and then refine it by a semantically-formulated effect
system that separately tracks: (1) the store effects of an expression
during evaluation; (2) the assumed effects of transitions by the
environment; and (3) the overall end-to-end effect. Rather than
tracking effects at the level of individual concrete heap cells, we
view the heap as a set of abstract data structures, each of which
may span several locations, or parts of locations [6]. Each abstract
location has its own notion of equality, and its own notion of legal
mutation. Write effects, for example, need only be flagged when the
equivalence class of an abstract location may change. Both typing
and refinement judgements may be established by a combination of
generic type-based rules and semantic reasoning in the model.
We begin with some motivating examples.

arXiv:1510.02419v1 [] 8 Oct 2015

Abstract
We describe a denotational semantics for an abstract effect system for a higher-order, shared-variable concurrent programming
language. We prove the soundness of a number of general effectbased program equivalences, including a parallelization equation
that specifies sufficient conditions for replacing sequential composition with parallel composition. Effect annotations are relative to
abstract locations specified by contracts rather than physical footprints allowing us in particular to show the soundness of some
transformations involving fine-grained concurrent data structures,
such as Michael-Scott queues, that allow concurrent access to different parts of mutable data structures.
Our semantics is based on refining a trace-based semantics for
first-order programs due to Brookes. By moving from concrete to
abstract locations, and adding type refinements that capture the possible side-effects of both expressions and their concurrent environments, we are able to validate many equivalences that do not hold
in an unrefined model. The meanings of types are expressed using
a game-based logical relation over sets of traces. Two programs e1
and e2 are logically related if one is able to solve a two-player game:
for any trace with result value v1 in the semantics of e1 (challenge)
that the player presents, the opponent can present an (response)
equivalent trace in the semantics of e2 with a logically related result value v2 .

1.

Introduction

Type-and-effect systems refine conventional types with extra
static information capturing a safe upper bound on the possible
side-effects of expression evaluation. Since their introduction by
Gifford and Lucassen [16], effect systems have been used for many
purposes, including region-based memory management [11], tracking exceptions [21, 23], communication behaviour [5] and atomicity [15] for concurrent programs, and information flow [12].
A major reason for tracking effects is to justify program transformations, most obviously in optimizing compilation [9]. For example, one may remove computations whose results are unused,
provided that they are sufficiently pure, or commute two statemanipulating computations, provided that the locations they may
read and write are suitably disjoint. Several groups have recently
studied the semantics of effect systems, with a focus on formally
justifying such effect-dependent equational reasoning [6, 8, 10, 17,
25]. A common approach, which we follow here, is to interpret
effect-refined types using a logical relation over the (denotational or
operational) semantics of the unrefined (or untyped) language, simultaneously identifying both the subset of computations that have
a particular effect type and a coarser notion of equivalence (or approximation) on that subset. Such a semantic approach decouples
the meaning of effect-refined types from particular syntactic rules:
one may establish that a term has a type using various more or less
approximate inference systems, or by detailed semantic reasoning.
For sequential computations with global state, denotational
models already provide significant abstraction. For example, the
denotations of skip and X++;X-- are typically equal, so it is immediate that the second is semantically pure. More generally, the
meaning of a judgement Γ ` e : τ&ε guarantees that the result

Equivalence modulo non-interference: Our semantics justifies
the following equation at the effect type unit & {coX } | ε |
ε ∪ {rd X , wr X }:
(X := !X + 1; X := !X + 1) = (X := !X + 2)
1

2018/3/12

head

This says that the two commands are equivalent with return type
unit, exhibit the effect coX , signifying concurrent or ‘chaotic’
access to X along the way, and have an overall end-to-end effect
of ε plus reading and writing X, provided that the effect, ε, of the
concurrent environment does not involve X.

n−1

Overlapping References: Let p,p−1 implement a bijection Z →
Z × Z, and consider the following functions:

n−k

readFst () = p(!X).1
readSnd () = p(!X).2
wrtFst n = let rec try () = (let m =!X in let (x, y) = p(m) in
let m0 = p−1 (n, y) in if cas(X, m, m0 ) then () else try ())
in try ()
wrtSnd n = let rec try () = let m =!X in let (x, y) = p(m) in
let m0 = p−1 (x, n) in if cas(X, m, m0 ) then () else try ()
in try ()

head
n0

n1

nj

null

nj+1 null

Figure 1. Illustration of a Michael-Scott Queue. The list resulting
from the pointer to the element n0 (the head pointer with the
continuous arrow in black) contains the list of elements [n1 , . . . , n j ].
The enqueueing operation is illustrated by the dotted arrow and the
box with the element n j+1 (in blue), while the dequeueing operation
is illustrated by the dot dashed head pointer (in red).

which multiplex two abstract integer references onto a single concrete one. Note that the write functions, wrtFst and wrtSnd, use
compare-and-swap, cas, to atomically update the value of the reference.
Our generic rules then say that a program, e1 , that only reads
and/or writes one abstract reference can be commuted, or executed
in parallel, with another program, e2 , that only reads and/or writes
into a different reference. This lets one use types to, say, justify
parallelizing a call to wrtFst followed by one to wrtSnd, even
though they read and write the same concrete location, which looks
like a race.

dequeue () =

let rec try () =
let n0 =!head in if !n0 .next = null then null
else let n1 =!n0 .next in
if cas(!head, n0 , n1 ) then !n1 .ele else try ()
in try ()

enqueue(x) =

let rec try (p) =
if !p.next = null then
if atomic(if !p.next = null then
!p.next := ref(x, null); true else false)
then () else try (!p.next)
else try (!p.next)
in try (!head)

Figure 2. Enqueue and Dequeue programs for a Michael-Scott
Queue at location head.

Version numbers: One can isolate a transaction that reads and
then writes a piece of state simply by enclosing the whole thing in
atomic(·). A more concurrent alternative adds a monotonic version
number to the data. A transaction then works on a private copy, only
committing its changes back (and incrementing the version) if the
current version number is the same as that of the original copy. We
can define an abstract integer reference X in terms of two concrete
ones, Xver and Xval , governed by a specification that says !Xval may
only change when !Xver increases. We define

pointed by head. Consider the following functions:
map f =

map2Par f =

transact f = let rec try() = let (val, ver) = atomic((!Xval , !Xver ))

in let res = f (val) in if atomic(if !Xver = ver then
Xver := ver + 1; Xval := res; true else false)
then () else try()
in try()

Under the assumption that f is a pure function (has effect type
∅|ε

int −−→ int for any ε), we can show
ε

let rec applyf n =
n.ele := f (n.ele); if n.next = null then ()
else applyf (n.next)
in if !head = null then () else applyf (!head)
let rec applyf2 n =
n.ele := f (n.ele) k n.next.ele := f (n.next.ele);
if n.next.next = null then ()
else if n.next.next.next = null then
n.next.next.ele = f (n.next.next.ele)
else applyf2 (n.next.next)
in if !head = null then ()
else if !head.next = null then
!head.next.ele := f (!head.next.ele)
else applyf2 (!head)

The function map simply applies a pure function f to each element
of the list, each element per iteration. The function map2Par, on
the other hand, applies f to two consecutive elements of the list
in parallel, potentially allowing one to exploit multiple cores. Our
effect-based reasoning will soundly transform map into map2Par
(under the assumption that the environment does not interfere with
the list).

transact f = atomic(Xval := f (!Xval ); Xver :=!Xver + 1)

at type unit&{rdX , wrX } | ε | ε ∪ {rdX , wrX } for any ε not including chaotic access, coX , to X. The environment effect ε here may
include reading and writing X, so concurrent calls to transact are
linearizable.

Michael-Scott Queue: The Michael-Scott Queue [20] (MSQ) is
a fine grained concurrent data structure, allowing threads to access
and modify different parts of a queue safely and simultaneously. We
present a version like that of Turon et al [27], which is an idealized
version of the MSQ, without a tail pointer.

Loop Parallelization: Our next example is inspired by a loop
unrolling optimization [26]. Assume given a linked list of integers

2

2018/3/12

in which the only elimination for computations is let, though
we sometimes nest computations as shorthand for let-expanded
versions in examples.
The construct e1 ke2 is evaluated by arbitrarily interleaving evaluation steps of e1 and e2 until each has produced a value, say v1 and
v2 ; the result is then (v1 , v2 ). Assignment, dereferencing and allocation are atomic, but evaluation of nested expressions is generally
not. To enforce atomicity, atomic(e) evaluates an arbitrary e in one
step, without any environmental interference. One can then define
a (more realistic) compare-and-swap operation cas(X, v1 , v2 ):

An MSQ maintains a pointer head to a non-empty linked list
as depicted in Figure 1. The first node, the node containing the
element n0 in the figure, is not an element of the queue, but is a
“sentinel”. Hence the queue in the figure holds [n1 , . . . , n j ].
The enqueue and dequeue operations are defined in Figure 2 and
illustrated in Figure 1. Elements are dequeued from the beginning
of the linked list, and enqueued at the end, which involves a traversal that is done without locking. Once the end, p, of the linked list is
found, the program atomically attempts to insert the new element.
This is necessary because other programs may have enqueued elements to the end of the list, meaning that p is no longer the end of
the list.
The dequeue operation should move the head pointer from the
current sentinel, n0 , to the following element n1 . However, as other
programs may also be attempting to dequeue an element, we use
compare-and-swap to atomically update the head pointer if head
still points to the same sentinel. Notice that the dequeued elements
can still reach the sentinel of the queue. (In Figure 1, these are
the nodes containing n−k , . . . , n−1 .) This is necessary because there
might be other (slower) threads that want to enqueue an element
and are still searching for the end of the list by traversing the portion
of the queue that has already been dequeued.
We prove that the enqueue and dequeue of Figure 2 are equivalent to atomic(enqueue) and atomic(dequeue), their atomic
versions which perform all operations in a single step, at a type
that allows the environment to be concurrently reading and writing
the queue. So the fine-grained MSQ behaves like a synchronized
queue, as might also be implemented using locks.

2.

cas(X, v1 , v2 ) = atomic(if !X = v1 then X := v2 ; true else false)
this atomically both checks if location X contains v1 and, if so,
replaces it with v2 and returns true; otherwise the location is
unchanged and the returned value is false.
We define the free variables, FV(e), of a term, closed terms, and
the substitution e[v/x] of v for x in e, in the usual way. Locations
may occur in terms, but the type system will constrain their use.

3.

Denotational Model

We now sketch a denotational semantics for our metalanguage
based on Brookes’ trace semantics [13]. Fuller details can be found
in a technical report (attached), which in particular establishes
computational adequacy of the model with respect to a small-step
operational semantics using interleaving.
3.1

Preliminaries
A predomain is an ω-cpo, i.e., a partial order with suprema
of ascending chains. A domain is a predomain with a least element, ⊥. Recall that f : A → A0 is continuous if it is monotone
x ≤ y ⇒ f (x) ≤ f (y) and preserves suprema of chains, i.e.,
f (supi xi ) = supi f (xi ). Any set is a predomain with the discrete
order (flat predomain). If X is a set and A a predomain then any
f : X → A is continuous. We denote a partial (continuous) function from set (predomain) A to set (predomain) B by f : A + B.
If A, B are predomains the cartesian product A × B and the set of
continuous functions A→B form themselves predomains (with the
obvious componentwise and pointwise orders) and make the category of predomains cartesian closed. Likewise, the partial continuous functions A+B between predomains A, B form a domain.
If P ⊆ A and Q ⊆ B are subsets of predomains A and B we
define P × Q ⊆ A × B and P→Q ⊆ A→B in the usual way. We may
write f : P → Q for f ∈ P→Q.
A subset U ⊆ A is admissible if whenever (ai )i is an ascending
chain in A such that ai ∈ U for all i, then supi ai ∈ U, too. If
f : X × A → A is continuous and A is a domain then one defines
f ‡ (x) = supi f xi (⊥) with f x (a) = f (x, a). One has, f (x, f ‡ (x)) =
f ‡ (x) and if U ⊆ A is admissible and contains ⊥ and f : X ×U → U
then f ‡ : X → U, too. An element d of a predomain A is compact
if whenever d ≤ supi ai then d ≤ ai for some i. E.g. in the domain
of partial functions from N to N the compact elements are precisely
the finite ones. A continuous partial function f : A + A is a retract
if f (a) ≤ a and f ( f (a)) = f (a) hold for all a ∈ A. In short: f ≤ idA
and f ◦ f ≤ f . If, in addition, f has a finite image then f is called a
deflation [3]. Note that if f is a retract then dom( f ) = Img( f ) and
if a ∈ Img( f ) then a = f (a). We also note that if a is in the image
of a deflation then a is compact.
We define the usual state monad on predomains, by taking
S A = H + H × A.

Syntax

In this section we define the syntax of a metalanguage for concurrent, stateful computations and higher-order functions. Communication between parallel computations is via a shared heap mapping dynamically allocated locations to structured values, which
include pointers. To keep the model simple, we do not allow functions to be stored in the heap (no higher-order store).
Memory model We assume a countably infinite set L of physical locations X1 , . . . , Xn , . . . and a set VB of “R-values” that can be
stored in those references including integers, booleans, locations,
and tuples of R-values, written (v1 , . . . , vn ). We assume that it is
possible to tell of which form a value is and to retrieve its components in case it is a tuple. A heap h, then, is a finite map from
L to VB, written {(X1 , c1 ), (X2 , c2 ), . . . , (Xn , cn )}, specifying that the
value stored in location Xi is ci . We write dom(h) for the domain of
h and write h[X7→c] for the heap that agrees with h except that it
gives the variable X the value c. The set of heaps is denoted by H.
We also assume that new(h, v) yields a pair (X, h0 ) where X ∈ L is
a fresh location and h0 ∈ H is h[X7→v].
Syntax of expressions The syntax of untyped values and computations is:
v ::= x | (v1 , v2 ) | vr | c | rec f x = t
e ::= v | let x = e1 in e2 | v1 v2 | if v then e1 else e2
|!v | v1 := v2 | ref(v) | e1 ke2 | atomic(e)
Here, x ranges over variables, vr over R-values, and c over builtin functions, which include arithmetic, testing whether a value is
an integer, function, pair or reference, equality on simple values,
etc. Each c has a corresponding semantic partial function Fc , so for
example F+ (n, n0 ) = n + n0 for integers n, n0 .
The construct rec f x = e defines a recursive function with body
e and recursive calls made via f ; we use λx.e as syntactic sugar
in the case when f is not free in e. Next, !v (reading) returns the
contents of location v, v1 := v2 (writing) updates location v1 with
value v2 , and ref(v) (allocating) returns a fresh location initialized
with v. The metatheory is simplified by using “let-normal form”,

Definition 3.1. Let P be a subset of a predomain A. Then Adm(P)
is the least admissible superset of P. Concretely, a ∈ Adm(P) iff
there exists a chain (ai )i such that ai ∈ P for all i and a = supi ai .
Lemma 3.2. If f : A1 ×· · ·×An is continuous; Pi ⊆ Ai are arbitrary
subsets and Q ⊆ B is admissible then f : P1 × · · · × Pn → Q implies
f : Adm(P1 ) × · · · × Adm(Pn ) → Q.

3

2018/3/12

Lemma 3.3. Let A, B be predomains and let (pi )i be a chain of
retracts on B such that pi (b) is compact for each i and supi pi = idB
and b ∈ Q implies pi (b) ∈ Q for all i. Then P→Adm(Q) =
Adm(P → Q).

Note that it is not possible to tell from a trace whether an external update of X has happened before or after the reading of X.
Let us also illustrate how traces iron out some intensional differences that show up when concurrency is modelled using transition systems or resumptions. Consider the following two programs
where ? denotes a nondeterministically chosen boolean value.

3.2

Traces
A trace models a terminating run of a concurrent computation as
a sequence of pairs of heaps, each representing pre- and post-state
of one or more atomic actions. The semantics of a program then is
a (typically large) set of traces (and final values), accounting for all
possible environment interactions.

e1
e2

≡
≡

if ? then X := 0; true else X := 0; false
X := 0; ?

Both e1 and e2 admit the same traces, namely (([x], [0]), true)
and (([x], [0]), false) and stuttering variants thereof. In semantic
models based on transition systems or resumptions and bisimulation, these are distinguished, which necessitates the use of special
mechanisms such as history and prophecy variables [2], forwardbackward simulation [19], or speculation [27] in reasoning.
Axioms [Down] and [Sup] are known from the Hoare powerdomain [24]. Recall that the Hoare powerdomain PA contains
the subsets of A which are downclosed ([Down]) and closed under
suprema of chains ([Sup]). Such subsets are also known as Scottclosed sets. Thus, T A is the restriction of P(Tr×A) to the sets closed
under stuttering and mumbling. Axiom [Down] ensures that the ordering is indeed a partial order and not merely a preorder. Additional nondeterministic outcomes that are less defined than existing
ones are not recorded in the semantics.

Definition 3.4 (Traces). A trace is a finite sequence of the form
(h1 , k1 )(h2 , k2 ) · · · (hn , kn ) where for 1 ≤ j ≤ i ≤ n, we have
hi , ki ∈ H and dom(h j ) ⊆ dom(hi ), dom(h j ) ⊆ dom(ki ), dom(k j ) ⊆
dom(hi ), dom(k j ) ⊆ dom(ki ). We write Tr for the set of traces.
Let t be a trace. A trace of the form u (h, h) v where t = uv is
said to arise from t by stuttering. A trace of the form u(h, k)v where
t = u(h, q)(q, k)v is said to arise from t by mumbling. For example, if t = (h1 , k1 )(h2 , k2 )(h3 , k3 ) then (h1 , k1 )(h, h)(h2 , k2 )(h3 , k3 )
arises from t by stuttering. In the case where k1 = h2 the trace
(h1 , k2 )(h3 , k3 ) arises from t by mumbling. A set of traces U is
closed under stuttering and mumbling if whenever t0 arises from
t by stuttering or mumbling and t ∈ U then t0 ∈ U, too.
Brookes [13] gives a fully-abstract semantics for while-programs
with parallel composition using sets of traces closed under stuttering and mumbling. We here extend his semantics to higher-order
functions and general recursion.

Definition 3.7. If U ⊆ Tr × A then U † is the least subset of T A
containing U, i.e. U † is the closure of U under [S& M], [Down],
[Sup].
Definition 3.8. Let A, B be a predomains. We define the continuous
functions rtn : A → T A and bnd : (A→T B) × T A → T B by:

Definition 3.5 (Trace Monad). Let A be a predomain. Elements of
the domain T A are sets U of pairs (t, a) where t is a trace and a ∈ A
such that the following properties are satisfied:

rtn(a) := ({((h, h), a) | h ∈ H})†
bnd( f, g) := ({(uv, b) | (u, a) ∈ g ∧ (v, b) ∈ f (a)})†

• [S&M]: if t0 arises from t by stuttering or mumbling and (t, a) ∈

These endow T A with the structure of a strong monad. The continuous function fromstate : S A → T A is defined by:

U then (t0 , a) ∈ U.
• [Down]: if (t, a1 ) ∈ U and a2 ≤ a1 then (t, a2 ) ∈ U.
• [Sup]: if (ai )i is a chain in A and (t, ai ) ∈ U for all i then
(t, supi ai ) ∈ U.

fromstate(c) := {((h, k), a) | c(h) = (k, a)}†
If t1 , t2 , t3 are traces, we write inter(t1 , t2 , t3 ) to mean that t3 can be
obtained by interleaving t1 and t2 in some way, i.e., t3 is contained
in the shuffle of t1 and t2 . In order to model parallel composition
we introduce the following helper function

The elements of T A are partially ordered by inclusion.
Lemma 3.6. If A is a predomain then T A is a domain.

| : T A × T B → T (A × B)
U | V := {(t3 , (a, b)) | inter(t1 , t2 , t3 ), (t1 , a) ∈ U, (t2 , b) ∈ V}†

An element U of T A represents the possible outcomes of a
nondeterministic, interactive computation with final result in A.
Thus, if (t, a) ∈ U for t = (h1 , k1 ) . . . (hn , kn ) then there could be
n interactions with the environment with heaps h1 , . . . , hn being
“played” by the environment and “answered” with heaps k1 , . . . , kn
by the computation. After that, this particular computation ends and
a is the final result value.
For example, the semantics of X :=!X + 1; X :=!X + 1; !X
contains many traces, including the following, where we write [n]
for the heap in which X has value n:
(([10], [12]), 12),
(([10], [11])([15], [16]), 16),
(([10], [11])([15], [16])([17, 17]), 17),
(([10], [11])([15], [16])([17, 17]), 16),
(([10], [11])([17], [17])([15], [16]), 16), . . .
Axiom [S&M] is taken from Brookes. It ensures that the semantics does not distinguish between late and early choice [27]
and related phenomena which are reflected, e.g., in resumption semantics [24], but do not affect observational equivalence. Note that
non-termination is modelled by the empty set, so we are working
with an ‘angelic’ notion of equivalence (‘may semantics’ [22]). For
example, the semantics of X := 0; if X=0 then 0 else diverge
is the same as that of X := 0; 0 and contains, for example
(([10], [0]), 0) but also (stuttering) ((([10], [0]), ([34], [34])), 0).

The continuous map at : T A → T A is defined by:
at(U) := {((h, k), v) | ((h, k), v) ∈ U}†
Notice that due to mumbling ((h, k), v) ∈ U iff there exists an
element ((h1 , h2 )(h2 , h3 ) . . . (hn−2 , hn−1 )(hn−1 , hn ), v) ∈ U where h =
h1 and hn = k. The presence of such an element, however, models
an atomic execution of the computation represented by U.
3.3

Semantic values
The predomain V of untyped values is the least solution of the
following domain equation:
V ' VB + (V → T V) + V∗ .
That is, values are either R-values, continuous functions from values to computations (T V), or tuples of values. We tend to identify
the summands of the right hand side with subsets of V but may use
tags like fun( f ) ∈ V when f : V → T V to avoid ambiguity.
We have families of deflations pi : V + V and qi : T V → T V,
referred to as canonical deflations, so that (pi )i and (qi )i are ascending chains converging to the identity. The definition is entirely
standard and may be found in the accompanying material. It shows
in particular that V and T V are bifinite (equivalently SFP) (pre)domains [3] and as such also Scott (pre-) domains. The presence

4

2018/3/12

l

of these deflations allows us to apply Lemma 3.3 and simplifies
reasoning in general.
The semantics of values VvW ∈ V → V and terms ~t ∈ V →
T V are given by the recursive clauses in Figure 3. Environments, ρ,
are properly tuples of values; we abuse notation slightly by treating
them as maps from variables, x, to values, v, (and write ρ[x7→v] for
functional update) to avoid mentioning an explicit context in which
untyped terms are well-formed.

4.

l

If h →
− h1 and at the same time h = h1 , then we say that h1 arises
from h by a silent move in l. Our semantic framework will permit
silent moves at all times.
We now introduce some examples of abstract locations.
Single Integer For our simplest example, consider the following
abstract location parametric with respect to concrete location X as
follows:

Abstract Locations

int(X)

h ∼ h0

We build on the concept of abstract locations defined by Benton,
Hofmann, and Nigam [6]. These allow complicated data structures
that span several concrete locations, or only parts of them, to be
a regarded as a single “location” that can be written to and read
from. Essentially, an abstract location is given by a partial equivalence relation on heaps modelling well-formedness and equality
together with a transitive relation modelling allowed modifications
of the abstract location. Abstract locations then allow certain commands that modify the physical heap to be treated as read-only or
even pure if they respect the contracts. Abstract locations are related to islands [4] which also allow one to specify heap allocated
data structures and use transition systems for that purpose. An important difference is that abstract locations do not require physical
footprints in the form of sets of concrete locations.
Due to the absence of dynamic allocation at the level of abstract
locations in the present paper, we can slightly simplify the original
definition [6], dropping those axioms that involve the interaction
with dynamic allocation.1 On the other hand, in the presence of
concurrency, we need two partial equivalence relations: one that
models semantic equivalence and well-formedness and a finer one
that constrains the heap modifications that other concurrent computations that are independent of the given abstract locations are
allowed to do while an operation on the abstract location is ongoing, but temporarily preempted.

int(X)

h = h0

∃n.h(X) = int(n) ∧ h0 (X) = int(n)
int(X)
h ∼ h0

⇐⇒
⇐⇒

int(X)

h −−−−→ h1
⇐⇒
h : int(X), h1 : int(X) and ∀X 0 ∈ L.X 0 , X ⇒ h(X 0 ) = h1 (X)

Two heaps are semantically equivalent (w.r.t. int(X) that is) if the
values stored in X are integers and equal; the step relation requires
all other concrete locations to be unchanged.
We will sometimes abuse notation and write rd X , wr X , coX for
rdint(X) , wrint(X) , coint(X) .
Overlapping references Let X be a concrete location encoding
a pair of integer values using a bijection p. We define the abstract
location fst(X) as below. We omit snd(X) which is similar, but only
looks at the second projection, instead of the first.
fst(X)

h ∼ h0 ⇐⇒ ∃a1 a2 a01 a02 ∈ Z.h(X) = p−1 (a1 , a2 ) ∧
h0 (X) = p−1 (a01 , a02 ) ∧ a1 = a01
fst(X)

fst(X)

h = h0 ⇐⇒ h ∼ h0
fst(X)

h−
−−−→ h1 ⇐⇒ h : fst(X), h1 : fst(X) and
(∀X 0 , X.h(X 0 ) = h1 (X 0 )) ∧ (∀a1 a2 a01 a02 ∈ Z.h(X) = p−1 (a1 , a2 ) ∧
h1 (X) = p−1 (a01 , a02 ) ⇒ a2 = a02 )

The semantic (and strict) equivalence of fst(X) (respectively,
snd(X)) specifies that two heaps h and h0 are equivalent whenever they both store a pair of values in X and the first projections
(respectively, second projection) of these pairs are the same. The
step relation of fst(X) (respectively, snd(X)) specifies that it keeps
all other locations alone and does not change the second projection
(respectively, first projection) of the pair stored at location X.

Definition 4.1 (Concurrent Abstract Location). A concurrent abstract location l consists of the following data:
l
(1) a partial equivalence relation ∼ on H modeling the “semanl
tic equivalence” on the bits of the store that l uses. If h ∼ h0 then
0
the same computation started on h and h , respectively, will yield
related or even equal results.
l
l
(2) a partial equivalence relation = on H refining ∼ and modeling the “strict equivalence” on the bits of the store that l uses. If a
concurrent computation on l has reached h and is preempted, then
l
another computation may replace h with h0 where h = h0 and then
0
the original computation on l may resume on h without the final
result being compromised.
l
(3) a transitive (and reflexive on the support of ∼) relation
l
→
− modeling how exactly the heap may change upon writing the
abstract location and in particular what bits of the store such writes
l
leave intact. In other words, if h →
− h1 then h1 might arise by writing
l
l
to l in h and all possible writes are specified by →.
− We call →
− the
step relation of l.
In addition, we require the following conditions where h : l
l
stands for h ∼ h.

Version Numbers The abstract location X consists of two concrete locations XVal and XVer and its relations are specified as follows:
X

h ∼ h0 ⇐⇒
X

h = h ⇐⇒
X

0

h→
− h1 ⇐⇒

h(XVal ) = h0 (XVal )
X

h ∼ h0

∀X 0 < {XVer , XVal }.h(X 0 ) = h1 (X 0 ) ∧
h : X ∧ h1 : X ∧ h(XVer ) <= h1 (XVer ) ∧
[h(XVal ) , h1 (XVal ) ⇒ h(XVer ) < h1 (XVer )]

Two heaps are semantically equivalent if they have the same value
(independent of the version number). The step relation specifies
that the version number does not descrease and it increases if the
value changes.
Loop Parallelization For a concrete location X, we introduce
two concurrent abstract locations listeven(X) and listodd(X), which
only look, respectively, at the elements in the the even and odd
positions of the linked list pointed by X. Formally, let L(X, h)
denote that h(X) points to a well formed linked list of integers of
length L(X, h).len and locations L(X, h).locs and that L(X, h)[i] is
the ith node of the list for 1 ≤ i ≤ L(X, h).len. The relations for
listeven(X) are as below. We omit the relations for listodd(X), which

l

1. If h : l then h = h;
l

2. if h →
− h1 then h : l and h1 : l.
1 Though

our examples do all satisify these axioms, leaving the way open
to a future extension with dynamically allocation of abstract locations and
concurrency.

5

2018/3/12

= ρ(x)
= vr
= (Vv1 Wρ, Vv2 Wρ)
= di if i = 1, 2, VvWρ = (d1 , d2 )
= fun( f )
where f (v) = rtn(Fc (v)) if Fc (v) is defined
and f (v) = ∅, otherwise.
= fun(g‡ (ρ))
where g(ρ, u) = λd.VeWρ[ f 7→u, x7→d]
= 0, otherwise

VxWρ
Vvr Wρ
V(v1 , v2 )Wρ
Vv.iWρ
VcWρ
Vrec f x = eWρ
VvWρ

~vρ
~let x = e1 in e2 ρ
~v1 v2 ρ
~if v then e1 else e2 ρ
~if v then e1 else e2 ρ
~!vρ
~v1 := v2 ρ
~ref(v)ρ
~atomic(e)ρ
~e1 ke2 ρ
~eρ

=
=
=
=
=
=
=
=
=
=
=

rtn(VvWρ)
bnd(λd.~e2 ρ[x7→d], ~e1 ρ)
Vv1 Wρ(Vv2 Wρ)
~e1 ρ, if VvWρ = true
~e2 ρ, if VvWρ = false
fromstate(λh.(h, h(X))), when VvWρ = X
fromstate(λh.(h[X7→Vv2 Wρ], ())), if Vv1 Wρ = X
fromstate(λh.new(h, VvWρ))
at(~e)
~e1 ρ | ~e2 ρ
∅, otherwise

Figure 3. Denotational semantics
dom(h). We omit the obvious frame conditions. We now define

are similar.
h

h

listeven(X)

∼

listeven(X)

=

h0 ⇐⇒

listeven(X)

msq(X)

h ∼ h0

L(X, h) ∧ L(X, h0 ) ∧ L(X, h).len = L(X, h0 ).len ∧
L(X, h)[2i] = L(X, h0 )[2i]
for 0 ≤ i ≤ bL(X, h).len/2c
listeven(X)
h ∼ h0

h0 ⇐⇒

h −−−−−−−→ h1 ⇐⇒

msq(X)

h = h0
msq(X)

h−
−−−−→ h1
step(h, h1 )

h : listeven(X) ∧ h1 : listeven(X) ∧
L(X, h) ∧ L(X, h1 ) ∧ for 0 ≤ i ≤ bL(X, h).len/2c
L(X, h)[2i + 1] = L(X, h1 )[2i + 1] ∧
L(X, h)[2i].next = L(X, h1 )[2i].next ∧
∀X 0 < L(X, h).locs.h(X 0 ) = h1 (X)

⇐⇒
⇐⇒

h : msq(X) ∧ h1 : msq(X) ∧ step∗ (h, h1 )
∀X 0 , X.h(X 0 ) = h1 (X 0 ) ∧
[h1 (X) = h(X).next ∨ ∃v.snoc(h, h1 , X, v)]

msq(X)

Definition 4.2 (world). A world is a set of abstract locations.
The relation h |= w (heap h satisfies world w) is defined as the
largest relation such that h |= w implies
• h : l for all l ∈ w;
l

l0

• if l ∈ w and h →
− h1 then h = h1 holds for all l0 ∈ w with l0 , l

and h1 |= w.

The original account of abstract locations [6] also has a notion of independence of locations which facilitates reasoning in
the presence of dynamic allocation, and in particular permitted relocation of abstract locations. Since we are not currently treating
dynamic allocation of abstract locations, we can avoid this notion
here.
We remark that if our world w contains two obviously “dependent” abstract locations, e.g. has both an integer location and a
boolean location placed at the same physical location, then there
will be no heap h such that h |= w.
We assume a fixed current world w which may appear in definitions without being notationally reflected. See also Assumption 1.

X 0 can be reached from X in h
by following a chain of next pointers

We use List(X, h, (X0 , . . . , Xn ), (v1 . . . , vn )) to signal that h(X) points
to a linked list with nodes X0 , . . . , Xn and entries v1 , . . . vn . Note
that the first node X0 acts as a sentinel and its elem component is
ignored. Formally:
h(Xi ).elem = vi for i = 1, . . . , n
h(Xn ).next = null

5.

We define fp(X, h) as the set of locations reachable and co-reachable
from X via next, formally:
next

h ∼ h0 ∧ ∀X 0 ∈ fp(X, h).h(X 0 ) = h0 (X 0 )

Worlds
We will group the abstract locations used to describe a program
into a world. In this paper we do not model dynamic evolution
of worlds; all abstract locations ever used must be set up upfront.
While allocation of concrete locations may happen to increase a
data structure modelled by an abstract location, e.g. in the MichaelScott Queue example, no new such datastructures can appear. It is
possible, however, to extend our work in this direction by using
(proof-relevant) Kripke logical relations [4, 6].

msq(X)

h(X).head = X0
h(Xi ).next = Xi+1 for i = 0, . . . , n − 1

⇐⇒

4.1

The relation −−−−−→, finally, is defined as the transitive closure of
the actions of operations on the MSQ: adding nodes at the tail and
moving nodes from the head to the garbage tail.
We now give a formal definition. We represent pointers head,
next, elem using some layout convention, e.g. v.head = v.1, etc. We
then define
next

~ X~0 ∃~v.List(X, h, X,
~ ~v) ∧ List(X, h0 , X~0 , ~v)
∃X

In all of these examples, the only silent moves are identity
moves. This is not so in the examples from [6] which contained
data-structures that would reorganize during lookups and also patterns like late initialisation.

Michael-Scott queue For concrete location X we introduce a
concurrent abstract location msq(X) first informally as follows: we
msq(X)
have h ∼ h0 if both h and h0 contain a well-formed MSQ rooted
at X and these queues contain the same entries in the same order.
They may, however, use different locations for the nodes and also
have different garbage tails.
msq(X)
The relation h = h0 asserts that h and h0 are identical on
the part reachable and co-reachable from X via next pointers. This
means that while an MSQ operation is working on the queue no
concurrent operation working elsewhere is allowed to relocate the
queue or remove the garbage trail which would be the case if we
MS Q(X)
merely required that such operations do not change the ∼ -class.

h, X → X 0 ⇐⇒

⇐⇒

Effects

For each abstract location l we have three elementary effects rdl
(reading from l), wrl (writing to l), and col (chaotic or concurrent
access). The chaotic access is similar to writing, but allows writes
that are not in sync. For example, e1 = X := 1 and e2 = X := 2 both
have individually the wr X effect, but e1 and e2 are distinguishable
with a context that assumes the wr X -effect. Thus, e1 and e2 are
not equal “at type” wr X . At type coX they are, however, equal,
because a context that copes with this effect may not assume that
both produce equal results.

next

fp(X, h) = {X 0 | X → X 0 ∨ X 0 → X}
Finally, we define snoc(h, h0 , X, v) to mean that h0 arises from h by
attaching a new node containing v at the end of the list pointed
to by X in h. Thus, in particular, List(X, h, (X0 , . . . , Xn ), (v1 . . . , vn ))
implies List(X, h0 , (X0 , . . . , Xn , Xn+1 ), (v1 . . . , vn , v)) for some Xn+1 <
6

2018/3/12

6.

We use the col effect to tell the environment not to look at a
particular location during a concurrent computation. For example,
we will be able to show that X := !X + 1; X := !X + 1 is equivalent
to X := !X + 2 “at type” unit & coX | ε | ε ∪ {rd X , wr X }
whenever X < locs(ε). This means that the two computations
are indistinguishable by environments that do not read, let alone
modify X during the computation and assume regular read-write
access once it is completed. It would alternatively be possible to
replace the co-effect using a special set of private locations akin to
the private regions from [10].
We use the notation rds(ε), wrs(ε), cos(ε) to refer to the abstract
locations l for which ε contains rdl , wrl , and col , respectively. We
write locs(ε) := rds(ε) ∪ wrs(ε) ∪ cos(ε). We also write εC for ε
with all read effects removed and each wrl in ε replaced by col .

Typing and congruence rules
Types are given by the grammar
ε1 | ε3

τ ::= unit | int | bool | A | τ1 × τ2 | τ1 −−−−→ τ2
ε2

where A ranges over user-specified abstract types. They will typically include reference types such as intref and also types like
ε1 | ε3

lists, sets, and even objects. In τ1 −−−−→ τ2 the triple of effects
ε2

(ε1 , ε2 , ε3 ) must be an effect specification.
We use two judgments:
• Γ ` v ≤ v0 : τ specifying that values v and v0 have type τ and

that v approximates v0 ,

• Γ ` e ≤ e0 : τ & ε1 | ε2 | ε3 specifying that the programs

Definition 5.1. An effect ε is well-formed (with respect to the
current world) if locs(ε) ⊆ w and rds(ε) ∩ cos(ε) = ∅ and cos(ε) ⊆
wrs(ε). An effect specification is a triple (ε1 , ε2 , ε3 ) of well-formed
effects such that ε2 ⊆ ε3 .

e and e0 under the context Γ have type τ, with the effect specification (ε1 , ε2 , ε3 ) specifying, respectively, the effects during
execution, the effects of the interacting environment and the
start and completion effects. Moreover, e approximates e0 at this
specification.

An effect specification (ε1 , ε2 , ε3 ) approximates the behaviour
of a computation e in the following way: the effect ε1 summarizes
side effects that may occur during the execution of e (corresponding
to a guarantee condition in the rely-guarantee formalism [14]); the
effect ε2 summarizes effects of the interacting environment that e
can tolerate while still functioning as expected (corresponding to
a rely condition). Finally, ε3 summarizes the side effects that may
occur between start and completion of e. All the effects that the
environment might introduce must be recorded in ε3 because they
are not under “our” control and might happen at any time even as
the very last thing before the final result is returned. The effects
flagged in ε1 , on the other hand, do not necessarily show up in ε3 ,
for a computation might be able to clean up those effects prior to
returning the final result. The requirement that rds(ε) ∩ cos(ε) =
∅ is owed to the fact that all effects should preserve their own
precondition, however the precondition of rdl is agreement on l
which is not preserved by col . The requirement cos(ε) ⊆ wrsε
reflects the fact that cos(l) includes wrl as a special case.
Note that if εC ∪ ε1 is a (well-formed) effect, then it is the case
that rds(ε1 ) ∩ (wrs(ε) ∪ cos(ε)) = ∅. We will use this observation to
simplify some side conditions.
In our concrete examples, we abbreviate {col }∪{wrl } by just col ,
in other words, the chaotic effect silently implies the write effect.
Consider the computations e1 = X := !X + 1; X := !X + 1
and e2 = X := !X + 2. Let εX stand for {rd X , wr X } and analogously εY . Each of the two computations can be assigned the effect (εX , εY , εX ∪ εY ), but they are distinguishable at that effect typing. Under the looser specification ({coεX }, εY , εX ∪ εY ), however,
they are indistinguishable, and our semantics is able to validate this
equivalence, see Example 7.5.
Finally, consider the program e =!X that simply reads a location
storing an integer. We can show that this program has type Z & ∅ |
ε | ε, rd X , where the read effect on X is only in the global effects.

We assume an ambient set of axioms each having the form
(v, v0 , τ) where v, v0 are values in the metalanguage and τ is a
type meaning that v and v0 are claimed to be of type τ and that
v approximates v0 . This must then be proved “manually” using the
semantics rather than using the rules. The
We also define typing judgements Γ ` v : τ and Γ ` e : τ &
ε1 | ε2 | ε3 which denote the special case when Γ ` v ≤ v : τ and
Γ ` e ≤ e : τ & ε1 | ε2 | ε3 can be derived from the rules from
Figure 6. We do not formulate explicit typing rules to save space.
The plan is to justify all the rules semantically using a logical
relation (Section 7) and to then conclude their soundness w.r.t.
typed observational appoximation and equivalence (Section 8).
The parallel composition rule states that two programs e1 and
e2 can be composed when their internal effects are not conflicting
in the sense that the internal effects of one program appear as
environment interaction effects of the other program. Note the
relationship to the parallel composition rule of the rely-guarantee
formalism [14]. Also note that the effects of computations e1 and
e2 are not required to be independent from each other as we do in
the parallization rule further down.
The appearance of the t-operation deserves special mention. It
might be, for example, that e1 modifies X on the way, thus wr X ∈ ε1
but cleans up this modification by eventually restoring the old value
of X. This would be reflected by wr X < ε ∪ ε0 ∪ ε2 . In that case, we
would not expect to see wr X in the end-to-end effect of the parallel
composition and that is precisely what t achieves.
The rules labelled (Sem) make available all kinds of program
transformations that are valid on the level of the untyped denotational semantics, including commuting conversions for let and if,
fixpoint unrolling, and beta and eta equalities.
Finally, we have several effect-dependent (in)equalities: the parallelization rule generalises a similar rule from [10]. The other ones
are concurrent version of analogous rules for sequential computation that have been analysed in previous work [6–8, 25] and are
at the basis of all kinds of compiler optimizations. The side conditions on the effects are rather subtle and much less obvious than
those found in a sequential setting. The parallelization rule is similar to the parallel congruence rule in that it requires the participating
computations to mutually tolerate each other. This time, however,
since the two computations being compared will do rather different
things temporarily they must be oblivious against chaotic access,
hence the (−)C strengthenings in the premise.
The reason for the appearance of (−)C in the other rules is
similar. The rule for pure lambda hoist seems unusual and will
thus be explained in more detail. First, the computation e1 to be

Notations. For any well-formed effects ε, ε0 we use the notation
ε ⊥ ε0 to mean that rds(ε) ∩ wrs(ε0 ) = rds(ε0 ) ∩ wrs(ε) = wrs(ε) ∩
wrs(ε0 ) = ∅. Note that this implies in particular cos(ε)∩rds(ε0 ) = ∅,
etc. Intuitively, two programs exhibiting effects ε and ε0 , respecrds(ε)
tively, commute with each other. We write h ∼ h0 to mean
ε
l
h ∼ h0 for each l ∈ rds(ε). We write →
− for the transitive closure
S
S
l
l
ε
l
of l∈wrs(ε) →
− ∪ l∈w →
− ∩ =. Thus, →
− allows steps by locations
recorded as writing in ε and silent steps by all locations in the current world.
We define the notation ε1 t ε2 which appears in the parallel
congruence rule by
ε1 t ε2 = ε1 ∪ ε2 \ {wr` | wr` < ε1 ∩ ε2 } \ {co` | co` < ε1 ∩ ε2 }
7

2018/3/12

hoisted may indeed have side effects ε1 so long as they are cleaned
up by the time e1 completes and the intervening environment does
not notice (modelled by the conditions ε1 ⊥ ε and final effect
εC = εC ∪ ∅). In the conclusion the transient effect ε1 shows up
again, but (−)C -ed since it only appears in different sides. Also in
the other rules like commuting etc. it is the case that the familiar
side conditions on applicability only affect the end-to-end effects
whereas the transient effects are merely required not to interfere
with the environment.
The following definitions provide the semantics of our effect
annotations.

Definition 7.4. Let E ⊆ V × V be a value specification and
(ε1 , ε2 , ε3 ) an effect specification. We define the relations T 0 (E, ε1 , ε2 , ε3 )
and T (E, ε1 , ε2 , ε3 ) between sets of trace-value pairs, i.e. on
P(Tr × Values):
(U, U 0 ) ∈ T 0 (E, ε1 , ε2 , ε3 ) if and only if



 ∀((h1 , k1 ) . . . (hn , kn ), a) ∈ U.h1 |= w ⇒


rds(ε
)
3
0
0 0
|
=
w
⇒
h
.
h
∼
h
⇒
∀
h


1
1 1
1


0
0
0
0
0
0
∃k1 .[ε1 ](h1 , h1 , k1 , k1 ) ∧ ∀h2 .[ε2 ](k1 , k1 , h2 , h2 ) ⇒




∃k20 .[ε1 ](h2 , h02 , k2 , k20 ) ∧ ∀h03 .[ε2 ](k2 , k20 , h3 , h03 ) ⇒


···


0
0
0
0
0


∃
k
.[ε
](
h
,
k
,
h
,
k
)
∧
[ε
](
h
,
h
,
k
,
k
)∧
1
n n
3
1
n
n n
1 n n


∃a0 ∈ V.(a, a0 ) ∈ E ∧ ((h01 , k10 ) . . . (h0n , kn0 ), a0 ) ∈ U 0

Definition 6.1 (Tiling). Let w ` ε. We write [ε](h, h0 , h1 , h01 ) to
ε
ε
mean that (i) h |= w ⇒ h →
− h1 and (ii) h0 |= w ⇒ h0 →
− h01 and (iii)
l
l
rds(ε)
l
h ∼ h0 and l ∈ wrs(ε) \ cos(ε) imply (h = h1 ∧ h0 = h01 ) ∨ h1 ∼ h01 .

We define the relation T (E, ε1 , ε2 , ε3 ) ⊆ T V × T V as the admissible
closure of T 0 , i.e. Adm(T 0 (E, ε1 , ε2 , ε3 )).
The game-theoretic view of T 0 (E, ε1 , ε2 , ε3 ) may be understood
as follows. Given U, U 0 ∈ T V we can consider a game between
a proponent (who believes (U, U 0 ) ∈ T V) and an opponent who
believes otherwise. The game begins by the opponent selecting an
element ((h1 , k1 ) . . . (hn , kn ), a) ∈ U and h1 |= w, the pilot trace
rds(ε )
and a start heap h01 |= w such that h1 ∼ 3 h01 to begin a trace
0
in U . Then, the proponent answers with a matching heap k10 so

Thus, assuming semantic consistency of heaps, h and h0 evolve
to h1 and h01 according to the modifying (writing or chaotic) locations in ε, and if h, h0 agree on the reads of ε then written locations
will either be identicallly modified or left alone.
If the step relations of all abstract locations commute with each
other then tiling admits an alternative characterisation in terms of
preservation of binary relations [8]. The present more operational
version is inspired by the treatment of effects in [10].

rds(ε )

that [ε1 ](h1 , h01 , k1 , k10 ). If h1 ∼ 1 h01 does not hold, proponent
does not need to ensure that writes are in sync. The opponent then
plays a heap h02 so that [ε2 ](k1 , k10 , h2 , h02 ). At this point, it is in

Lemma 6.2. Suppose that w ` ε, w ` ε1 , w ` ε2 . The following
hold whenever well-formed.
1. If [ε](h, h0 , h1 , h01 ) and [ε](h1 , h01 , h2 , h02 ) then [ε](h, h0 , h2 , h02 );
2. [ε](h, h0 , h, h0 )
3. If ε1 ⊆ ε2 then [ε1 ](h, h0 , h1 , h01 ) ⇒ [ε2 ](h, h0 , h1 , h01 )
4. [ε](h, h0 , h1 , h01 ) ⇒ [εC ](h, h0 , h1 , h01 )
rds(ε)
rds(ε)
5. If [ε](h, h0 , k, k0 ) and h ∼ h0 then k ∼ k0 . (this relies on
rds(ε) ∩ cos(ε) = ∅.)
6. Suppose [ε](h, h0 , h1 , h01 ). If h |= w then h1 |= w; if h0 |= w then
h01 |= w.

7.

rds(ε )

the proponents interest to make sure that k1 ∼ 2 k10 for otherwise
opponent may make “funny” moves.
Then, again, proponent plays a heap k20 such that [ε1 ](h2 , h02 , k2 , k20 )
and so on until, proponent has played kn0 so that [ε1 ](hn , h0n , kn , kn0 ).
After that final heap has been played, it is checked that [ε3 ](h, h0 , kn , kn0 )
holds. If not, proponent loses. If yes, then proponent must also play
a value a0 and it is then checked whether or not ((h01 , k10 ) . . . (h0n , kn0 ), a0 ) ∈
U 0 and (a E a0 ). If this is the case or if at any one point in the game
the opponent was unable to move because there exists no appropriate heap then the proponent has won the game. Otherwise the
opponent wins and we have (U, U 0 ) ∈ T 0 (E, ε1 , ε2 , ε3 ) iff the proponent has a winning strategy for that game.
We notice that by Lemma 6.2(6) well-formedness of heaps w.r.t.
the ambient world is a global invariant which allows us to refrain
form explicitly assuming and asserting it in subsequent proofs and
statements.
We now illustrate the game with a few examples.

Logical Relation

Definition 7.1 (Specifications). A value specification is a relation
E ⊆ V × V such that
• if x1 ≤ x and y ≤ y1 and x E y then x1 E y1 ;
• if (xi )i and (yi )i are chains such that xi E yi then supi xi E supi yi ,

i.e., E is admissible qua relation;
• if x E y then pi (x) E pi (y) for each i, i.e. E is closed under the

canonical deflations.

Example 7.5. Consider the following programs: e1 = (X :=
!X + 1; X := !X + 1) and
e2 = (X := !X + 2).
Let l = int(X) be the abstract location for a single integer stored
at X (see Section 4). Let E = ~unit = {((), ())} be the value
specification for the unit type.
We show that (~e1 , ~e2 ) ∈ T (E, {col }, ε, ε ∪ {rdl , wrl }} under
the assumption that {col } ⊥ ε, that is, when the environment does
not read nor write X. This condition is clearly necessary, for e1 and
e2 can be distinguished by an environment allowed to read or write
X.
Let us now prove the claim when {col } ⊥ ε. The opponent picks
a pilot trace in the semantics of e1 , for example, ((h1 , k1 )(h2 , k2 ), ())
where h1 (X) = n and k1 (X) = n + 1 and h2 (X) = n0 and k2 (X) =
n0 + 1. The other possible traces are stuttering or mumbling variants
of this one and do not present additional difficulties. The opponent
l
also chooses a heap h01 such that h1 ∼ h01 , i.e., h01 (X) = n. Now
the proponent will choose to stutter for the time being and thus
selects k10 := h01 . Indeed, [col ](h1 , h01 , k1 , k10 ) holds, so this is legal.
The opponent now presents h02 such that [ε](k1 , k10 , h2 , h02 ). By the
assumption on ε we know that n0 = h2 (X) = k1 (X) = n + 1
and also h02 (X) = k10 (X) = n. The proponent now answers with

Similarly, a computation specification is a relation Q ⊆ T V × T V
such that ≤; Q; ≤ ⊆ Q and Q is admissible qua relation and Q is
closed under the canonical deflations qi .
The requirement ≤; E; ≤ ⊆ E ensures smooth interaction with
the down-closure built into our trace monad. Admissibility is
needed for the soundness of recursion and closure under the canonical deflations, finally is needed so that Lemma 3.3 can be applied.
Definition 7.2. If E ⊆ V × V and Q ⊆ T V × T V then the relation
E→Q ⊆ V × V is defined by
f E→Q f 0 ⇐⇒ ∀x x0 .(x E x0 ) ⇒ ( f (x) Q f 0 (x0 ))
In particular, for f E→Q f 0 to hold, both f, f 0 must be functions
(and not elements of base type or tuples).
Lemma 7.3. If E and Q are specifications so is E→Q.
The following is the crucial definition of this paper; it gives a
semantic counterpart to observational approximation and, due to
its game-theoretic flavour, allows for very intuitive proofs.

8

2018/3/12

Γ ` true ≤ true : bool

Γ ` false ≤ false : bool

Γ ` n ≤ n : int

Γ ` e1 ≤ e2 : τ & ε1 | ε2 | ε3 Γ ` e1 ≤ e2 : τ & ε1 | ε2 | ε3
Γ ` e1 ≤ e3 : τ & ε1 | ε2 | ε3
ε1 | ε3

Γ ` v1 ≤ v01 : τ1 −−−−→ τ2
ε2

Γ ` v ≤ v0 : τ1 × τ2
Γ ` v.i ≤ v0 .i : τi

Γ, x : τ ` x ≤ x : τ

Γ ` vi ≤ v0i : τ1 i = 1, 2
Γ ` (v1 , v2 ) ≤ (v01 , v02 ) : τ1 × τ2

Γ`v≤v :τ
Γ ` v ≤ v0 : τ & ε1 | ε2 | ε3
0

Γ ` v ≤ v0 : bool
Γ ` e1 ≤ e01 : τ & ε1 | ε2 | ε3 Γ ` e2 ≤ e02 : τ & ε1 | ε2 | ε3

Γ ` v2 ≤ v02 : τ1

Γ ` v1 v2 ≤ v01 v02 : τ2 & ε1 | ε2 | ε3

Γ ` if v then e1 else e2 ≤ if v0 then e01 else e02 : τ & ε1 | ε2 | ε3
ε1 | ε3

Γ ` e1 ≤ e01 : τ1 & ε1 | ε2 | ε3
Γ, x:τ1 ` e2 ≤ e02 : τ2 & ε1 | ε2 | ε3

Γ, f :τ1 −−−−→ τ2 , x:τ1 ` e ≤ e0 : τ2 & ε1 | ε2 | ε3

Γ ` let x = e1 in e2 ≤ let x = e01 in e02 : τ2 & ε1 | ε2 | ε3

Γ ` rec f x = e ≤ rec f x = e0 : τ1 −−−−→ τ2

ε2

ε1 | ε3
ε2

Γ ` e1 ≤ e01 : τ1 & ε1 | ε ∪ ε2 | ε ∪ ε2 ∪ ε0 Γ ` e2 ≤ e02 : τ2 & ε2 | ε ∪ ε1 | ε ∪ ε1 ∪ ε0
Γ ` e1 ke2 ≤ e01 ke02 : τ1 × τ2 & ε1 ∪ ε2 | ε | ε ∪ ε0 ∪ (ε1 t ε2 )
Γ ` e ≤ e : τ & ε1 | ε2 | ε3 ~e = ~e0 
Sem1
Γ ` e0 ≤ e0 : τ & ε1 | ε2 | ε3
Γ ` e ≤ e0 : τ & ε1 | ε2 | ε3 ε1 ⊆ ε01 ε02 ⊆ ε2
Γ ` e ≤ e0 : τ & ε01 | ε02 | ε03

Γ ` e ≤ e : τ & ε1 | ε2 | ε3 ~e = ~e0 
Sem2
Γ ` e ≤ e0 : τ & ε1 | ε2 | ε3

ε3 ⊆ ε03

(v, v0 , τ) an axiom
Ax1
Γ`v≤v:τ

Γ ` e ≤ e0 : τ & ε1 | ∅ | ε3
Atom
Γ ` atomic(e) ≤ atomic(e0 ) : τ & ε3 | ε2 | ε2 ∪ ε3

(v, v0 , τ) an axiom
Ax2
Γ ` v0 ≤ v0 : τ

Figure 4. Typing and congruence rules
Γ ` e1 : τ1 & ε1 | εC ∪ εC2 | εC ∪ εC2 ∪ ε01

Γ ` e2 : τ2 & ε2 | εC ∪ εC1 | εC ∪ εC1 ∪ ε02

ε1 ⊥ ε2

ε1 ⊥ ε

ε2 ⊥ ε

Γ ` e1 ke2 ≤ (let x = e1 in let y = e2 in (x, y)) : τ1 × τ2 & εC1 ∪ εC2 | ε | ε ∪ ε01 ∪ ε02
Γ ` e1 : τ1 & ε1 | εC | εC ∪ ε01

Γ ` e2 : τ2 & ε2 | εC | εC ∪ ε02

ε01 ⊥ ε02

Γ ` (let x = e1 in let y = e2 in (x, y)) = (let y = e2 in let x = e1 in (x, y)) : τ1 × τ2 &
Γ ` e : τ & ε1 | εC2 | εC2 ∪ ε0

ε1 ⊥ ε
εC1

∪

εC2

ε2 ⊥ ε

| ε | ε ∪ ε01 ∪ ε02

rds(ε0 ) ∩ wrs(ε0 ) = ∅ ε2 ⊥ ε1

Γ ` (let x = e in (x, x)) ≤ (let x = e in let y = e in (x, y))) : τ × τ & εC1 | ε2 | ε2 ∪ ε0
(v, v0 , τ) an axiom
Ax
Γ ` v ≤ v0 : τ

Γ ` e1 : τ1 & ε1 | εC | εC

Γ, x : τ3 , y : τ1 ` e2 : τ2 & ε2 | ε | ε ∪ ε2
εC
∪ε2 | ε∪ε3
1

Parallelization

Commuting

Duplicated
ε ⊥ ε1

Lambda Hoist

Γ ` let y = e1 in λx.e2 ≤ λx.let y = e1 in e2 : τ3 −−−−−−−−−→ τ2 & εC1 | ε | ε
ε

Γ ` e1 : τ1 & ε1 | ε | ε ∪
C

C

ε01

Γ ` e2 : τ2 & ε2 | ε |

ε02

ε1 ⊥ ε

Γ ` e2 ≤ (let x = e1 in e2 ) : τ2 & εC1 ∪ ε2 | ε | ε ∪ ε02

wrs(ε01 ) = ∅

Deadcode

Figure 5. Effect-dependent transformations.
k20 := h02 [X7→n + 2]. It follows that [col ](h2 , h02 , k2 , k20 ) and also
[rdl , wrl ](h1 , h01 , k2 , k20 ). Finally, by stuttering (h01 , h01 )(h02 , h02 [X7→n +
2]) ∈ ~e2  so that proponent wins the game.

h01 that agrees with the initial heap [n1 |n2 ] on the reads of ε ∪
{rd X , rdY , wr X , wrY }. Thus, h01 should be of the form [n1 |n2 ].
We now play the move ([n1 |n2 ], [n1 + 1|n2 ]). This is a valid move
in the game as [coX , coY ]([n1 |n2 ], [n1 |n2 ], [n1 |n2 + 1], [n1 + 1|n2 ]).
The environment moves returning [n1 + 1|n2 ] as it does not read
nor modify X and Y. We can now match the trace above by playing
([n1 +1|n2 ], [n1 +1|n2 +1]) and returning ((), ()), winnning the game.

Example 7.6. Consider the following programs e1 and e2 :
(X := !X + 1kY := !Y + 1) and (X := !X + 1; Y := !Y + 1).
We show (~e1 , ~e2 ) ∈ T (E, {coX , coY }, ε, ε ∪ {rd X , rdY , wr X , wrY }),
provided ε does not read nor modify X and Y. This equivalence
could be deduced syntactically using our parallelization equation
shown in Figure 5. For illustrative purpose, however, we describe
its semantic proof using a game.
The opponent picks a pilot trace in ~e1 , for example, the trace
([n1 |n2 ], [n1 |n2 + 1])([n1 |n2 + 1], [n1 + 1|n2 + 1])((), ()), where [nX |nY ]
denotes a heap where X and Y store nX and nY , respectively. Notice
that in this trace, Y is incremented before X and since ε does
not read nor modify X and Y, the environment move does not
change the values in X nor Y. We are also given an initial heap

The following is one of the main technical result of our paper and shows that the computation specifications T (. . . ) can indeed serve as the basis for a logical relation. We just show here
the soundness proof for the parallel congruence rule. The missing
proofs appear in the attached Appendix.
Theorem 7.7. The following hold whenever well-formed.
1. If (U, U 0 ) ∈ T (E, ε1 , ε2 , ε3 ) then (qi (U), qi (U 0 )) ∈ T (E, ε1 , ε2 ).
2. T (E, ε1 , ε2 , ε3 ) is a computation specification.
3. If (U, U 0 ) ∈ T (E, ε1 , ε2 , ε3 ) then (U † , U 0 † ) ∈ T (E, ε1 , ε2 , ε3 ).

9

2018/3/12

Theorem 7.8. Suppose that Γ ` v : τ and Γ ` e : τ & ε1 | ε2 | ε3 .
Then (η, η0 ) ∈ ~Γ (interpreting a context as a cartesian product)
implies (VvWη, VvWη0 ) ∈ ~τ and (~eη, ~eη0 ) ∈ T (~τ, ε1 , ε2 , ε3 ).

4. If (a, a0 ) ∈ E then (rtn(a), rtn(a0 )) is in T (E, ε1 , ε2 , ε3 ).
5. Suppose that (ε1 , ε2 , ε3 ) is an effect specification where ε1 ∪
rds(ε )
ε2 ⊆ ε3 . Suppose that whenever h ∼ 1 h0 and c(h) =
0
0
(h1 , a) then there exist (h1 , a ) such that c0 (h0 ) = (h01 , a0 )
and [ε1 ](h, h0 , h1 , h01 ) and aEa0 . We then have for any ε2 ,
(fromstate(c), fromstate(c0 )) ∈ T (E, ε1 , ε2 , ε3 ).
6. If ( f, f 0 ) ∈ E1 →T (E2 , ε1 , ε2 , ε3 ) and (U, U 0 ) ∈ T (E1 , ε1 , ε2 , ε3 )
then (bnd( f, U), bnd( f 0 , U 0 )) ∈ T (E2 , ε1 , ε2 , ε3 ).
7. If (U1 , U10 ) ∈ T (E1 , ε1 , ε ∪ ε2 , ε ∪ ε2 ∪ ε0 ) and (U2 , U20 ) ∈
T (E2 , ε2 , ε ∪ ε1 , ε ∪ ε1 ∪ ε0 ) then (U1 | U10 , U2 | U20 ) ∈ T (E1 ×
E2 , ε1 ∪ ε2 , ε, ε ∪ ε0 ∪ (ε1 t ε2 )).
8. (U, U 0 ) ∈ T (E, ε1 , ∅, ε3 ) ⇒ (at(U), at(U 0 )) ∈ T (ε3 , ε2 , ε2 ∪ ε3 ).

Proof. By induction on derivations. Most cases are already subsumed by Theorem 7.7. The typing rules regarding functions and
recursion follow from the definitions and from the fact that all specifications are admissible.


8.

ε1 | ε3

approximates v0 at type τ if for all f such that ` f : τ −−−−→ int
ε
(“observations”) it is the case that if ((hinit , k), n) ∈ ~ f v for
0
0
v ∈ Z and starting from hinit then ((hinit , k ), n) ∈ ~ f v  for some
k0 . We write ` v ≤obs v0 in this case. We say that v and v0 are
observationally equivalent at type τ, written ` v =obs v0 if both
` v ≤obs v0 : τ and ` v0 ≤obs v : τ.

Proof. Ad 7. Suppose that (U1 , U10 ) ∈ T (E1 , ε1 , ε∪ε2 , ε∪ε2 ∪ε0 ) and
(U2 , U20 ) ∈ T (E2 , ε2 , ε ∪ ε1 , ε ∪ ε1 ∪ ε0 ) and let (t, (a, b)) ∈ U1 | U2 ,
thus inter(t1 , t2 , t) (ignoring † by item 3) where (t1 , a) ∈ U1 and
(t2 , b) ∈ U2 . Let S 1 , S 2 be corresponding winning strategies. The
idea is to use S 1 when we are in t1 and to use S 2 when we are in
t2 . Supposing that t starts with a t1 fragment we begin by playing
according to S 1 . Let t be of the form:
t=

This means that for every test harness f we build around v and
v0 , no matter how complicated it is and whatever environments
it sets up to run concurrently with v and v0 it is the case that
each terminating computation of v (in the environment installed by
f ) can be matched by a terminating computation with the same
result by v0 in the same environment. It is important, however,
that the environment be well typed, thus will respect the contracts
set up by the type τ. E.g. if τ is a functional type expecting,
say, a pure function as argument then, by the typing restriction,
the environment f cannot suddenly feed v and v0 a side-effecting
function as input.
We remark that observational approximation extends canonically to open terms by lambda abstracting free variables (and
adding a dummy abstraction in the case of closed terms) [6].
As usual, the logical relation is sound with respect to typed observational approximation and thus can be used to deduce nontrivial observational approximation relations. We state and prove the
precise formulation of this result.

(h1 , k1 ) · · · (hn , kn )(hn+1 , kn+1 ) · · · (hn+m , kn+m )
(hn+m+1 , kn+m+1 ) · · · (hn+m+k , kn+m+k ) · · · (h p , k p )

composed of pieces of the traces t1 and t2 . Assume w.l.o.g. that
the first piece (h1 , k1 ) · · · (hn , kn ) is a part of t1 . We are given a
rds(ε∪ε0 ∪(ε1 tε2 )) 0
initial heap h01 such that h
∼
h . Since rds(ε1 t ε2 ) =
rds(ε1 ) ∪ rds(ε2 ), we can apply strategy S 1 to guide us through the
first part of the game, obtaining:
(h01 , k10 ) · · · (h0n , kn0 )
Moreover, we have an environment move which forms the tile
[ε](kn , kn0 , hn+1 , hn0 +1 ). Thus, we have the tile [ε∪ε1 ](h1 , h01 , hn+1 , h0n+1 )
which can be seen as an environment move for t2 . Therefore, we
can use strategy S 2 for the U 0 and continue the game, obtaining the
trace piece:
0
0
(h0n+1 , kn+1
) · · · (h0n+m , kn+m
)
Now, we can return to the S 1 game as the trace above is seen as
an environment move for U. Alternating these strategies, we get a
trace t which is in (U | U 0 ). Let (a0 , b0 ) be the final values reached
at the end. It is clear that [ε ∪ ε0 ∪ ε1 ∪ ε2 ](h, h0 , h p , h0p ) and also
aE1 a0 and bE2 b0 .
It remains to assert the stronger statement [ε ∪ ε0 ∪ (ε1 t
ε2 )](h, h0 , h p , h0p ). To see this suppose that wrl ∈ ε1 \ ε2 \ ε \ ε0 .
Since the entire game can be viewed as an instance of the game
U1 vs U10 with interventions by U2 vs. U20 regarded as environment interactions we have [ε ∪ ε2 ∪ ε0 ](h, h0 , h p , h0p ) so that in fact
l

Theorem 8.2. Let v, v0 be closed values and suppose that (~v, ~v0 ) ∈
~τ. Then ` v ≤obs v0 : τ.
ε1 | ε3

Proof. If ` f : τ −−−−→ int then by Thm 7.8 we have (~ f , ~ f ) ∈
ε1 | ε3
ε2

Let ((hinit , k), v) ∈ ~ f v. We have hinit |= w and thus in particular
rds(ε3 )∪rds(ε1 )
∼
hinit . There must therefore exist a matching heap k0
hinit
and a value v0 such that ((hinit , k0 ), v0 ) ∈ ~ f v0  and v = v0 ∈ Z. 

l



This means that the examples from earlier on give rise to valid
transformations in the sense of observational approximation. For
instance, for e1 and e2 form Example 7.5 we find that λ .e1 =obs

We assign a value specification ~τ to each refined type by
•

~int = {(v, v0 ) | v = v0 ∈ Z}

•

~τ1 −−−−→ τ2  = ~τ1 →T (~τ2 , ε1 , ε2 , ε3 )

ε1 | ε3

ε2

~τ −−−−→ int, so (~ f v, ~ f v0 ) ∈ T (~int, ε1 , ε2 , ε3 )+ .

h = h p and h0 = h0p . The case of col and ε1 ,ε2 interchanged is

analogous.

Typed observational approximation

Definition 8.1 (Observational approximation). Let v, v0 be value
expressions where ` v : τ and ` v0 : τ. We say that v observationally

• ~τ1 × τ2  = ~τ1  × ~τ2 

{col } | ε∪{rdl ,wrl

λ .e2 at type unit −−−−−−−−−−−→ unit whenever X does not appear
ε
in ε.

ε2

We omit the obvious definition of the other basic types and assume
value specifications for user-specified types as given.

9.

Effect-dependent transformations

We will now establish the semantic soundness of the inequational theory of effect-dependent program transformations given in
Figure 5. It includes concurrent versions of the effect-dependent
equations from [8, 25], but the side conditions on the environmental interaction are by no means obvious. We also note that some
equations now only hold in one direction thus become inequations.
This is in particular the case for duplicated computations. Suppose
that ? is a computation that nondeterministically chooses a boolean
value and let e := let x = ? in (x, x). Then, even though ? does

Assumption 1. We henceforth adopt the following soundness assumption which must be established concretely for every concrete
instance of our framework.
• The initial heap satisfies the current world: hinit |= w.
• Each axiom is type sound: whenever (v, v0 , τ) is an axiom then

(v, v) ∈ ~τ and (v0 , v0 ) ∈ ~τ.
• Each axiom is inequationally sound: whenever (v, v0 , τ) is an
axiom then (v, v0 ) ∈ ~τ.

10

2018/3/12

context as a cartesian product) implies (VvWη, Vv0 Wη0 ) ∈ ~τ+ and
(~eη, ~e0 η0 ) ∈ T (~τ, ε1 , ε2 , ε3 )+ .

not read nor write any location we only have e ≤ (?, ?), but not
(?, ?) ≤ e for (?, ?) admits the result (true, false) but e does not.
Furthermore, due to presence of nontermination the equations for
dead code elimination and pure lambda hoist also hold in one direction only. It might be possible to restore both directions of said
equations by introducing special effects for nondeterminism and
nontermination; we have not explored this avenue. We concentrate
the individual effect-dependent transformations before summarising the foregoing results in the general soundness Theorem 9.2.
In many of the equations, co-effects play an important role. For
example, in the commuting and parallelization equations, the internal effects ε1 and ε2 in the premises are replaced by εC1 and εC2 in
the internal effects of the conclusion. This makes sense intuitively
because the computations are run in a different order, so for the
internal moves, the locations in ε1 and ε2 can be modified in any
way (see Example 7.6). However, in the global effect, we can still
guarantee the effects ε01 and ε02 because of the ⊥-conditions. This
intuition appears directly in the soundness proofs.
The following thus constitutes the second main technical result
of our paper. We sketch the soundness proof for parallelization. The
detailed proofs appear in the attached Appendix.

Sketch. In essence the proof is by induction on derivations of inequalities. However, we need to slightly strengthen the induction
hypothesis as follows:
Define
~Γ ` τ = {( f, f 0 ) | ∀(η, η0 ) ∈ ~Γ.( f (η), f 0 (η0 )) ∈ ~τ}
~Γ ` τ&(ε1 , ε2 , ε3 ) = {( f, f 0 ) | ∀(η, η0 ) ∈ ~Γ.
( f (η), f 0 (η0 )) ∈ T (~τ, ε1 , ε2 , ε3 )}
We now show by induction on derivations that Γ ` v ≤ v0 : τ
implies (~v, ~v0 ) ∈ ~Γ ` τ+ and that Γ ` e ≤ e0 : τ & ε1 | ε2 | ε3
implies (~e, ~e0 ) ∈ ~Γ ` τ&(ε1 , ε2 , ε3 )+ .
The various cases now follow from earlier results in a straightforward manner. Namely, we use Theorem 7.7 for the congruence
rules and Theorem 9.1 for the effect-dependent transformations.
As a representative case we show the case where e ≡ let x =
e1 ine2 and e0 ≡ letx = e01 ine02 . Inductively, we know (~e1 , ~e01 ) ∈
~Γ ` τ1 &(ε1 , ε2 , ε3 )n1 and (~e1 , ~e01 ) ∈ ~Γ, x:τ1 ` τ&(ε1 , ε2 , ε3 )n2
for some n1 , n2 > 0. By Theorem 7.8, we also have (~e1 , ~e1 ) ∈
~Γ ` τ1 &(ε1 , ε2 , ε3 ) and analogous statements for e01 , e2 , e02 . We
can, therefore, assume, w.l.o.g. that n1 = n2 and then use Theorem 7.7 (6) repeatedly (n1 times) so as to conclude (~e, ~e) ∈
~Γ ` τ&(ε1 , ε2 , ε3 )n1 .
The rules for dead code and pure lambda hoist rely on the cases
“Dead” and “Pure” of Thm 9.1 in a slightly indirect way. We sketch
the argument for pure lambda hoist. The pilot trace begins with a
trace belonging to e1 and yielding a value v for x. We can then
invoke case “Pure” on subsequent occurrences of e1 in the right
hand side.


Theorem 9.1. The following hold whenever well-formed.
• Commuting If (U1 , U10 ) ∈ T (E1 , ε1 , εC , εC ∪ ε01 ) and (U2 , U20 ) ∈

T (E2 , ε2 , εC , εC ∪ ε02 ) and ε1 ⊥ ε and ε2 ⊥ ε and ε01 ⊥ ε02 then
({(t1 t2 , (v1 , v2 )) | (t1 , v1 ) ∈ U1 , (t2 , v2 ) ∈ U2 }† ,
{(t20 t10 , (v01 , v02 )) | (t10 , v01 ) ∈ U10 , (t20 , v02 ) ∈ U20 }† )
∈ T (E1 × E2 , (ε1 ∪ ε2 )C , ε, ε ∪ ε01 ∪ ε02 )

• Duplicated If (U, U 0 ) ∈ T (E, ε1 , εC2 , εC2 ∪ ε0 ) and rds(ε0 ) ∩

wrs(ε0 ) = ∅ and ε2 ⊥ ε1 , then

Theorem 9.3. Suppose that ` v : τ and ` v0 : τ and that
(~v, ~v0 ) ∈ ~τ+ where (−)+ denotes transitive closure. Then
` v ≤obs v0 : τ.

({(t, (v, v)) | (t, v) ∈ U}† , {(t10 t20 , (v01 , v02 )) | (t10 , v01 ) ∈ U 0 ,
(t20 , v02 ) ∈ U 0 }† ) ∈ T (E, ε1 , ε2 , ε2 ∪ ε0 )
• Pure Let (U, U 0 ) ∈ T (E, ε1 , εC2 , εC2 ), such that ε1

⊥ ε2 .
If ((q1 , k1 ) . . . (qn , kn ), v) ∈ U for some arbitrary trace t =
(q1 , k1 ) . . . (qn , kn ) (with q1 |= w) and value v, then (rtn(v), U 0 ) ∈
T (E, εC1 , ε2 , ε2 );
• Dead Suppose that (U, U 0 ) ∈ T (unit, ε1 , ε2 , ε2 ∪ ε01 ), where
wrs(ε01 ) = ∅ and ε1 ⊥ ε2 . Then (U, rtn(())) ∈ T (unit, εC1 , ε2 , ε2 ∪
ε01 ).
• Parallelization If (U1 , U10 ) ∈ T (E1 , ε1 , εC ∪ εC2 , εC ∪ εC2 ∪ ε01 )
and (U2 , U20 ) ∈ T (E2 , ε2 , εC ∪ εC1 , εC ∪ εC1 ∪ ε02 ) and ε1 ⊥ ε2 and
ε1 ⊥ ε and ε2 ⊥ ε, then

ε1 | ε3

Proof. If ` f : τ1 −−−−→ int then by Thm 7.8 we have (~ f , ~ f ) ∈
ε1 | ε3

ε2

~τ −−−−→ int, so (~ f v, ~ f v0 ) ∈ T (~int, ε1 , ε2 , ε3 )+ .
ε2

Let ((hinit , k), v) ∈ ~ f v. We have hinit |= w and thus in particular
rds(ε3 )∪rds(ε1 )
hinit
∼
hinit . There must therefore exist a matching heap k0
0
and a value v such that ((hinit , k0 ), v0 ) ∈ ~ f v0  and v = v0 ∈ Z. 
We now return to the examples that we discussed in Section 1
and demonstrate how to prove using our denotational semantics the
properties that have been discussed informally.

(U1 kU2 , {(t10 t20 (v01 , v02 )) | (t10 , v01 ) ∈ U10 , (t20 , v02 ) ∈ U20 }† ) ∈
T (E1 × E2 , εC1 ∪ εC2 , ε, ε ∪ ε01 ∪ ε02 )

Overlapping References With this example, we illustrate the parallelization rule. In particular, the functions declared in Section 1
have the following type, where ε does not read nor write X:

Proof. (Sketch) Parallelization.
Assume w.l.o.g. that the pilot trace takes the form (t, (v1 , v2 ))
where inter(t1 , t2 , t) and (ti , vi ) ∈ Ui . Just as in the commuting case
we set up two side games Ui vs. Ui0 on ti , vi . Unlike, in that case,
however, these games are running simultaneously and along with
the main game. Moves by the environment in the main game are
forwarded to the side game we are currently in, i.e., the one to
which the current portion of t being played on belongs. At each
change of control, we switch between the two side games making
last sequence of moves of the other game into a single environment
move. It is here that the resilience against chaotic modification is
needed. Once the play is over we then assert the claims about the
end-to-end effect ε∪ε01 ∪ε02 location by location using the definition
of tiling.


∅ | εC ,cosnd(X) ,rdfst(X)

readFst : unit −−−−−−−−−−−−−−−−→ int
εC ,cosnd(X)

wrfst(X) | εC ,cosnd(X) ,wrfst(X)

writeFst : int −−−−−−−−−−−−−−−−−−−−−→ unit
εC ,cosnd(X)

The obvious and analogous typings for readSnd and writeSnd
are elided. We justify this typing semantically as described in
Theorem 7.7. To illustrate how this is done, consider the function
(writeSnd 17). We show how the game is played against itself
using the typing shown above. We start with a “pilot trace”, say:
([2|3], [2|3]), ([2|17], [2|17]), (())
where [x|y] denotes a store with X = p(x, y) and other components
left out for simplicity. The first step corresponds to our reading
of X and in the second step – since there was no environment
intervention – we write 17 into the first component.
We now start to play: Say that we start at the heap [13|12].
We answer [13|12]. If the environment does not change X, then

Theorem 9.2. Suppose that Γ ` v ≤ v0 : τ and Γ ` e ≤
e0 : τ & ε1 | ε2 | ε3 and assume that for each axiom (v, v0 , τ)
it holds that (v, v0 ) ∈ ~τ+ . Then (η, η0 ) ∈ ~Γ+ (interpreting a
11

2018/3/12

we write 17 to its first component resulting in the following trace,
which is possible for writeFst(17).
([13|12], [13|12]), ([13|12], [17|12]), (())
If, however, the environment plays [18|21] (a modification of both
components of X has occurred), then we answer [17|21]. Again,
([13|12], [13|12]), ([18|21], [17|21]), (())
is a possible trace for writeFst(17). It is easy to check that there is
a strategy that justifies the typing given above.
Now, consider a program, e1 , that only calls readFst, writeFst,
and another program, e2 , that only calls readSnd, writeSnd. Since
the former functions have disjoint effects to the latter ones, e1
and e2 will have effect specifications, respectively, of the form
(ε1 , εC ∪ εC2 , εC ∪ εC2 ∪ ε1 ) and (ε2 , εC ∪ εC1 , εC ∪ εC1 ∪ ε2 ), where
ε1 ∩ ε2 = ε1 ∩ ε = ε2 ∩ ε = ∅. Thus we can use the parallelization
rule shown in Figure 5 to conclude that the behavior of e1 ke2 is the
same as executing these programs sequentially, although they read
and write to the same concrete location.

Notice that the congruence rules now allow us to deduce
the equivalence of op1 k · · · k opn and atomic(op1 ) k · · · k
atomic(opn ) for opi being enqueues or dequeues, which effectively
amounts to linearizability.

10.

Discussion

We have shown how a simple effect system for stateful computation and its relational semantics, combined with the notion
of abstract locations, scales to a concurrent setting. The resulting
type system provides a natural and useful degree of control over
the otherwise anarchic possibilities for interference in shared variable languages, as demonstrated by the fact that we can delineate
and prove the conditions for non-trivial contextual equivalences,
including fine-grained data structures.
The primary goal of this line of work is not so much to find
reasoning principles that support the most subtle equivalence arguments for particular programs, but rather to capture more generic
properties of modules, expressed in terms of abstract locations and
relatively simple effect annotations, that can be exploited by clients
(including optimizing compilers) in external reasoning and transformations. But there are of course, particularly in view of the fact
that we allow deeper reasoning to be used to establish that expressions can be assigned particular effect-refined types, very close connections with other work on richer program logics and models.
Rely-guarantee reasoning is widely used in program logics for
concurrency, including relational ones [18], whilst our abstract locations are very like the islands of Ahmed et al [4]. Recent work of
Turon et al [27] on relational models for fine-grained concurrency
introduces richer abstractions, notably state transition systems expressing inter-thread protocols that can involve ownership transfer.
These certainly allow the verification of more complex fine-grained
algorithms than can be dealt with in our setting, and it would be natural to try defining an effect semantics over such a model. Indeed,
one might reasonably hope that effects could provide something of
a ‘simplifying lens’, with refined types capturing things that would
otherwise be extra model structure or more complex invariants,
such that the combination does not lead to further complexity. The
use of Brookes’s trace model (also used by, for example, Turon and
Wand [28]) already seems to bring some simplification compared
to transition systems or resumptions.
Birkedal et al [10] have also studied relational semantics for effects in a concurrent language. The language considered there has
dynamic allocation via regions and higher-order store, neither of
which we have here. On the other hand, their invariants are based on
simply-typed concrete locations and thus do not allow to capture effects at the level of whole datastructures as abstract locations do. As
a result, the examples in [10] are of a simpler nature than ours. Furthermore, we offer a subtler parallelization rule, distinguish transient and end-to-end effects, and validate other effect-dependent
equivalences like commuting, lambda hoist, deadcode and duplication. Our use of denotational methods and in particular the extension of Brookes’ trace semantics to higher-order functions does
result in a rather simpler and more intuitive definition of the logical
relation by comparison with [10]. While some of the complications
are due to the dynamic allocation and typed locations, others like
the explicit step counting, the need for effect-instrumented operational semantics, and the separation of branches in the definition
of safety are not. We thus see our work also as a proof-of-concept
for denotational semantics in the realm of higher-order concurrent
programming.
The ‘RGSim’ relation proposed by Liang et al. for proving concurrent refinements under contextual assumptions also has many
similarities with our logical relation [18, Def.4]. The focus of
that work is on proving particular equivalences and refinements,
whereas we encapsulate general patterns of behaviour in a refined

Loop Parallelization We show that the function map is equivalent to map2Par. It is easy to see that the function map is equivalent to the program map2Seq, which is the program obtained
from map2Par by replacing the underlined parallel operator ‘k’ in
map2Par by a sequential operator ‘;’. The proof goes simply by
unfolding map.
We then proceed by showing map2Seq and map2Par are
equivalent using our equations and the abstract locations listodd(X)
and listodd(X) defined above. The piece of code that applies f
first, namely e1 = n.ele := f (n.ele), has global effects ε01 =
rdlistodd(X) , wrlistodd(X) , while the second application, namely, e2 =
n.next.ele := f (n.next.ele), has effects ε02 = rdlisteven(X) , wrlisteven(X) .
Notice that ε01 ⊥ ε02 . Therefore, provided that the environment does
not read nor modify the list, we can apply the parallelization equation to justify running e1 and e2 parallel is equivalent to running
them in sequence.
Michael-Scott Queue We now show that the enqueue and
dequeue functions described in Section 1 for the Michael-Scott
Queue have the same behavior as their atomic versions. We only
show the case for dequeue, as the case for enqueue is similar.
More precisely, we now justify the axiom
MSQ | MSQ

(dequeue, atomic(dequeue), unit −−−−−−−→ int)
MSQ

where MSQ = {rdmsq(X) , wrmsq(X) }. That is, they approximate each
other at a type where the environment is allowed to operate on the
queue as well. We also note that the converse of the axiom is obvious by stuttering and mumbling. After consuming a dummy argument () let the resulting pilot trace be (h1 , k1 ) . . . (hi , ki ) . . . (hn , kn )a
and h01 be the start heap to match. We can now assume that the pasmsq(X)

sages from ki to hi+1 are according to the protocol, i.e. ki −−−−−→
hi+1 . Namely, should this not be the case we are free to make arbitrary moves and still win the game by default of the environment
player. Therefore, there must exist i such that in the move (hi , ki )
the element a is dequeued and h j = k j holds for j , i. We can thus
match this trace by a trace in the semantics of atomic(dequeue ())
by stuttering until i:
(h01 , h01 ) . . . (h0i , . . .
where h j and h0j have the same content, but not necessarily the exact
same layout. Given the environment’s allowed effects it is then clear
that also hi and h0i have the same content, but not necessarily the
same as h1 and h01 because in the meantime other operations on the
queue might have succeeded. We then dequeue the corresponding
element from h0i leading to ki0 and continue by stuttering.
. . . , ki0 )(h0i+1 , h0i+1 ) . . . (h0n , h0n )a0
It is now clear that this is a matching trace and that a = a0 so we
are done.

12

2018/3/12

References

type system and can show the soundness of generic program transformations relying only on effect types (which combine smoothly
with hand proofs of particular equivalences).
There are many directions for further work. Most importantly,
we would like to add dynamic allocation of abstract locations
following [6]. In addition to relieving us from having to set up
all data structures in the initial heap this would, as we believe,
also allow us to model and reason about lock-based protocols in
an elegant way. Other possible extension include higher-order store
and weak concurrency models.

[1] M. Abadi, C. Flanagan, and S. N. Freund. Types for safe locking:
Static race detection for java. ACM Trans. Program. Lang. Syst.,
28(2):207–255, 2006.
[2] M. Abadi and L. Lamport. The existence of refinement mappings.
Theor. Comput. Sci., 82(2):253–284, 1991.
[3] S. Abramsky and A. Jung. Domain theory, 1994. Online Lecture
Notes, avaliable from CiteSeerX.
[4] A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In POPL, 2009.
[5] T. Amtoft, F. Nielson, and H. R. Nielson. Type and Effect Systems:
Behaviours for Concurrency. World Scientific, 1999.
[6] N. Benton, M. Hofmann, and V. Nigam. Abstract effects and proofrelevant logical relations. In POPL, pages 619–632, 2014.
[7] N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Relational
semantics for effect-based program transformations with dynamic allocation. In PPDP, 2007.
[8] N. Benton, A. Kennedy, M. Hofmann, and L. Beringer. Reading, writing and relations: Towards extensional semantics for effect analyses.
In APLAS, volume 4279 of LNCS, 2006.
[9] N. Benton, A. Kennedy, and G. Russell. Compiling Standard ML to
Java bytecodes. In ICFP, 1998.
[10] L. Birkedal, F. Sieczkowski, and J. Thamsborg. A concurrent logical
relation. In P. Cégielski and A. Durand, editors, CSL, volume 16
of LIPIcs, pages 107–121. Schloss Dagstuhl - Leibniz-Zentrum fuer
Informatik, 2012.
[11] L. Birkedal, M. Tofte, and M. Vejlstrup. From region inference to von
Neumann machines via region representation inference. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages (POPL ’96), 1996.
[12] N. Broberg and D. Sands. Flow locks: Towards a core calculus for
dynamic flow policies. In 15th European Symposium on Programming
(ESOP ’06), volume 3924 of LNCS. Springer, 2006.
[13] S. D. Brookes. Full abstraction for a shared-variable parallel language.
Inf. Comput., 127(2):145–163, 1996.
[14] J. W. Coleman and C. B. Jones. A structural proof of the soundness of
rely/guarantee rules. J. Log. Comput., 17(4):807–841, 2007.
[15] C. Flanagan and S. Qadeer. A type and effect system for atomicity.
In Proceedings of the ACM SIGPLAN Conference on Programming
Language Design and Implementation (PLDI ’03), 2003.
[16] D. K. Gifford and J. M. Lucassen. Integrating functional and imperative programming. In LISP and Functional Programming, 1986.
[17] O. Kammar and G. D. Plotkin. Algebraic foundations for effectdependent optimisations. In POPL, 2012.
[18] H. Liang, X. Feng, and M. Fu. A rely-guarantee-based simulation
for verifying concurrent program transformations. In J. Field and
M. Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2012,
Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 455–
468. ACM, 2012.
[19] N. A. Lynch and F. W. Vaandrager. Forward and backward simulations, ii: Timing-based systems. Inf. Comput., pages 1–25, 1996.
[20] M. M. Michael and M. L. Scott. Nonblocking algorithms and
preemption-safe locking on multiprogrammed shared memory multiprocessors. J. Parallel Distrib. Comput., 51(1):1–26, May 1998.
[21] N.Benton and P. Buchlovsky. Semantics of an effect analysis for
exceptions. In 3rd ACM Workshop on Types in Language Design and
Implementation (TLDI ’07), 2007.
[22] R. D. Nicola and M. Hennessy. Testing equivalence for processes. In
ICALP, pages 548–560, 1983.
[23] F. Pessaux and X. Leroy. Type-based analysis of uncaught exceptions.
In Proceedings of the 26 ACM Symposium on Principles of Programming Languages (POPL ’99), 1999.
[24] G. D. Plotkin. A powerdomain construction. SIAM J. Comput.,
5(3):452–487, 1976.

13

2018/3/12

A.

[25] J. Thamsborg and L. Birkedal. A Kripke logical relation for effectbased program transformations. In ICFP, 2011.

Proof of Theorem 7.7

Proof. In each case, using Corollary 3.2 and Lemma 3.3 (for case
6), we can in fact assume w.l.o.g. that the assumed pairs are in
T 0 (. . . ) rather than T (. . . ).

[26] J.-B. Tristan and X. Leroy. A simple, verified validator for software
pipelining. In POPL, 2010.
[27] A. J. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, and D. Dreyer.
Logical relations for fine-grained concurrency. In R. Giacobazzi and
R. Cousot, editors, POPL, pages 343–356. ACM, 2013.
[28] A. J. Turon and M. Wand. A separation logic for refining concurrent
objects. In T. Ball and M. Sagiv, editors, Proceedings of the 38th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages
247–258. ACM, 2011.

Ad 1. Let (t, a) ∈ qi (U), i.e. a = pi (a0 ) where (t, a0 ) ∈ U. By
down-closure ([Down]) we also have (t, a) ∈ U. We can now play
the strategy guaranteed by the assumption (U, U 0 ) ∈ T (E, ε1 , ε2 , ε3 )
which will yield (depending on the opponent’s moves) a trace t0
and a value a0 such that (t0 , a0 ) ∈ U 0 and (pi (a), a0 ) ∈ E. Now,
since E is a specification we get (pi (a), pi (a0 )) ∈ E noting that pi is
idempotent. So, we modify the strategy so as to return pi (a0 ) rather
than a0 and thus obtain a winning strategy asserting the desired
conclusion.
Ad 2 This is an easy consequence from 1.
Ad 3 Pick (U, U 0 ) ∈ T 0 (E, ε1 , ε2 , ε3 ). Since T (E, ε1 , ε2 , ε3 ) is
closed under suprema it suffices to show that (q j (U † ), q j (U 0 † )) ∈
T (E, ε1 , ε2 , ε3 ) for each j. Fix such j and pick (t, p j (a)) ∈ q j (U † ),
thus (t, a) ∈ U † .
By induction on the closure process we can assume w.l.o.g. that
(t, a) arises from (t1 , a) ∈ U by a single mumbling or stuttering step
or that (t, a1 ) ∈ U for some a1 ≥ a or else that (t, ai ) ∈ U where
supi ai = a.
In the former two cases fix a strategy for the original element of
U. We will use this strategy to build a new one demonstrating that
(t, a) ∈ U 0 , hence (t, p j (a)) ∈ q j (U 0 ) as required.
If (t, a) arises by stuttering, so t = u(h, h)v and t1 = uv we play
the strategy until u is worked off. If the opponent then produces a
heap h0 to match h we answer h0 .
Now [ε1 ](h, h0 , h, h0 ) is always true (Lemma 6.2) so this is
a legal move. Thereafter, we continue just as in the original
strategy. In the special case where v is empty, we must also
show that [ε3 ](h1 , h01 , h, h0 ) knowing [ε3 ](h1 , h01 , kn , kn0 ) where u =
(h1 , k1 ) . . . (hn , kn ) and u0 = (h01 , k10 ) . . . (h0n , kn0 ) is the matching
trace. We have [ε2 ](kn , kn0 , h, h0 ) for otherwise opponent’s playing h0 would have been illegal. Since, by assumption ε2 ⊆ ε3 ,
we can conclude [ε3 ](kn , kn0 , h, h0 ) and then [ε3 ](h1 , h01 , h, h0 ) by
Lemma 6.2(3&1).
If (t, a) arises by mumbling then we must have t = u(h1 , h3 )v and
t1 = u(h1 , h2 )(h2 , h3 )v. We play until the strategy has produced a
match h02 for h2 . So far, the play has produced a trace u0 matching u,
and a state h01 so that [ε1 ](h1 , h01 , h2 , h02 ). Now, we can ask what the
original strategy would produce if we gave it (temporarily assuming
opponent’s role) the state h02 as a match for h2 . Note that this is
legal because [ε2 ](h2 , h02 , h2 , h02 ). The strategy will then produce
h03 such that [ε1 ](h2 , h02 , h3 , h03 ) and our answer in the play on the
new trace against the challenge h01 will be this very h03 . Indeed,
by composing tiles (Lemma 6.2) we have [ε1 ](h1 , h01 , h3 , h03 ) as
required. Thereafter, the play continues according to the original
strategy.
For down-closure, we play the strategy against (t, a1 ) yielding
a match (t0 , a01 ) ∈ U 0 where a1 Ea01 . That same strategy also wins
against (t, a) because aEa01 since E is a value specification.
For closure under [Sup], finally, pick i so that ai ≥ p j (a) recalling that a = supi ai . Since we have a winning strategy for (t, ai ),
we also have one (by down-closure which was already proved) for
(t, p j (a)) as required.
Ad 4. Suppose aEa0 . By 3 which we have just proved we only
need to match elements of the form ((h, h)a). The opponent plays
rds(ε )
h0 where h ∼ 3 h0 and we answer with h0 itself and a0 . This is
always a legal move (Lemma 6.2) and aEa0 , so we win the game.
Ad 5. Again, we only need to match traces of the form ((h, h1 ), a)
where c(h) = (h1 , a). In this case, suppose that the opponent
14

2018/3/12

ε

plays h0 where h ∼3 h0 . The assumption gives (h01 , a0 ) such that
c0 (h0 ) = (h01 , a0 ) and [ε1 ](h, h0 , h1 , h01 ) and aEa0 . We thus play h01
and a0 and indeed [ε1/3 ](h, h0 , h1 , h01 ) and aEa0 hold so this is a
winning move.
Ad 6. Suppose ( f, f 0 ) ∈ E1 →T (E2 , ε1 , ε2 , ε3 ) and (U, U 0 ) ∈
T (E1 , ε1 , ε2 , ε3 ). Suppose that (uv, b) ∈ ap(f, U) where (u, a) ∈ U
and (v, b) in f (a) (note that we can ignore the †-closure). We need
to produce a trace (u0 v0 , b0 ) ∈ ap(f’, U 0 ) such that (u0 , a0 ) ∈ U 0 and
(v0 , b0 ) in f 0 (a0 ) and bE2 b0 . Assume that:

B.

(h1 , k1 )(h2 , k2 ) · · · (hn , kn )

(hn+1 , kn+1 ) · · · (hn+m , kn+m ) (a, b)

where
t1 = (h1 , k1 )(h2 , k2 ) · · · (hn , kn ) v1 ∈ U1
t2 = (hn+1 , kn+1 ) · · · (hn+m , kn+m ) v2 ∈ U2
We make similar use of Theorem 7.7(3) in the subsequent cases
without explicit mention.

u = (h1 , k1 ) · · · (hn , kn ) and v = (hn+1 , kn+1 ) · · · (hn+m , kn+m )

rds(ε∪ε0 ∪ε0 )

rds(ε )

We are also given a heap h01 such that h1
∼1 2 h01 . Because
0
0
0
ε1 ⊥ ε2 , h1 and hn+1 agree on the reads of ε2 . Thus we can start
a game U2 vs. U20 using h01 and t2 . We forward all environment’s
moves from the main game to the side game and use the responses
from the side game to answer in the main game. Suppose that the
side game leads to the valid U2 -trace

We are given a heap h01 , such that h1 ∼ 3 h01 . We can use the
strategy S 1 from (U, U 0 ) ∈ T (E1 , ε1 , ε2 , ε3 ) for (u, a). We play
according to S 1 to work off the u-part. This results in a matching
trace u0 ∈ U 0 :
u0 = (h01 , k10 ) · · · (h0n , kn0 )
where [ε3 ](h1 , h01 , kn , kn0 ) and (a, a0 ) ∈ E2 . We get ( f (a), f (a0 )) ∈
T (E2 , ε1 , ε2 , ε3 ). Now, we are given a heap h0n+1 that is an environment move forming the tile [ε2 ](kn , kn0 , hn+1 h0n+1 ). From the fact that
rds(ε )
ε2 ⊆ ε3 and Lemma 6.2(5) we can conclude hn+1 ∼ 3 h0n+1 .
Thus we can continue our play by using the strategy S 2 from
( f (a), f (a0 )) ∈ T (E2 , ε1 , ε2 , ε3 ) which yields a continuation v0 of
0
0 0 0

(h01 , k10 )(h02 , k20 ) · · · (h0m , km0 ) v02
where v2 E2 v02 and (1) [εC ∪ ε02 ](hn+1 , h01 , kn+m , km0 ). Notice that in the
global game these are legal responses as [εC1 ∪ εC2 ](hi , h0i , ki , ki0 ) for
1 ≤ i ≤ m.
We now have an environment move [ε](km , km0 , hm+1 , h0m+1 ).
Since ε01 ⊥ ε and ε02 ⊥ ε01 , the heaps h01 and h0m+1 agree in the
reads of ε01 . Therefore, we can run a game U1 vs. U10 using h0m+1
and t1 , obtaining the trace:

our trace and a final answer b . It is then clear that (u v , b ) ∈
bnd( f 0 , U 0 ) so this combination of strategies does indeed win.

Ad 7. Suppose that (U1 , U10 ) ∈ T (E1 , ε1 , ε ∪ ε2 , ε ∪ ε2 ∪ ε0 ) and
(U2 , U20 ) ∈ T (E2 , ε2 , ε ∪ ε1 , ε ∪ ε1 ∪ ε0 ) and let (t, (a, b)) ∈ U1 | U2 ,
thus inter(t1 , t2 , t) (ignoring † by item 3) where (t1 , a) ∈ U1 and
(t2 , b) ∈ U2 . Let S 1 , S 2 be corresponding winning strategies. The
idea is to use S 1 when we are in t1 and to use S 2 when we are in
t2 . Supposing that t starts with a t1 fragment we begin by playing
according to S 1 . Let t be of the form:
t=

Proof of Theorem 9.1

Proof. Commuting. By Theorem 7.7(3) we can assume our pilot
trace t to be of the form:

0
0
0
(h0m+1 , km+1
)(h0m+2 , km+2
) · · · (h0m+n , km+n
) v01
0
where v1 E1 v01 and (2) [εC ∪ ε01 ](h1 , h0m+1 , kn , km+n
). The reasoning is
similar to the use of the previous game.
Thus we have that (v1 , v2 )(E1 × E2 )(v01 , v02 ).
0
Now, we need to conclude that [εC ∪ ε01 ∪ ε02 ](h1 , h01 , kn+m , km+n
).
This follows from the fact that ε01 ⊥ ε02 and (1) and (2). In particular,
0
from (1) and ε01 ⊥ ε02 , we get that km+n and km+n
agree on the
0
locations in ε02 , while from (2), we get that km+n and km+n
agree
0
on the locations in ε1 . This finishes the proof.
Duplicated. Assume given a trace in U:

(h1 , k1 ) · · · (hn , kn )(hn+1 , kn+1 ) · · · (hn+m , kn+m )
(hn+m+1 , kn+m+1 ) · · · (hn+m+k , kn+m+k ) · · · (h p , k p )

composed of pieces of the traces t1 and t2 . Assume w.l.o.g. that
the first piece (h1 , k1 ) · · · (hn , kn ) is a part of t1 . We are given a
rds(ε∪ε0 ∪(ε1 tε2 )) 0
initial heap h01 such that h
∼
h . Since rds(ε1 t ε2 ) =
rds(ε1 ) ∪ rds(ε2 ), we can apply strategy S 1 to guide us through the
first part of the game, obtaining:

t = (h1 , k1 ) · · · (hn , kn ) v
rds(ε ∪ε0 )

and a heap h01 such that h1
∼2
h01 . Since ε2 ⊥ ε1 and rds(ε0 ) ∩
wrs(ε0 ) = ∅, we have that h1 and kn agree on the reads of ε0 .
We start by simply stuttering:

(h01 , k10 ) · · · (h0n , kn0 )

t0 = (h01 , h01 )(h02 , h02 ) · · · (h0n , ??)

Moreover, we have an environment move which forms the tile
[ε](kn , kn0 , hn+1 , hn0 +1 ). Thus, we have the tile [ε∪ε1 ](h1 , h01 , hn+1 , h0n+1 )
which can be seen as an environment move for t2 . Therefore, we
can use strategy S 2 for the U 0 and continue the game, obtaining the
trace piece:

where [ε](ki , hi+1 , ki0 , h0i+1 ) for 1 ≤ i ≤ n + m. Notice that for
1 ≤ i ≤ n − 1, we have [εC1 ](hi , h0i , hi+1 , h0i ). So the stuttering moves
are valid responses.
We will now play U1 vs. U10 to construct the missing heap “??”.
We first run a game using h0n and t, where the environment moves
are simply stutter moves:

0
0
(h0n+1 , kn+1
) · · · (h0n+m , kn+m
)

(h0n , q1 )(q1 , q2 ) · · · (qn−1 , qn ) v01

Now, we can return to the S 1 game as the trace above is seen as
an environment move for U. Alternating these strategies, we get a
trace t which is in (U | U 0 ). Let (a0 , b0 ) be the final values reached
at the end. It is clear that [ε ∪ ε0 ∪ ε1 ∪ ε2 ](h, h0 , h p , h0p ) and also
aE1 a0 and bE2 b0 .
It remains to assert the stronger statement [ε ∪ ε0 ∪ (ε1 t
ε2 )](h, h0 , h p , h0p ). To see this suppose that wrl ∈ ε1 \ ε2 \ ε \ ε0 .
Since the entire game can be viewed as an instance of the game
U1 vs U10 with interventions by U2 vs. U20 regarded as environment
l
interactions we have [ε ∪ ε2 ∪ ε0 ](h, h0 , h p , h0p ) so that in fact h = h p

such that vEv01 and [εC ∪ ε0 ](h1 , h0n , kn , qn ). Notice that using stuttering environment moves are valid as [εC ](ki , qi , hi+1 , qi ) for 1 ≤
i ≤ n − 1.
Since h1 and kn agree on the reads of ε0 and qn and kn agree on
rds(ε0 ) from [εC ∪ ε0 ](h1 , h0n , kn , qn ), we can run the game U1 vs. U10
again on qn and t with stutter environment moves:
(qn , qn+1 )(qn+1 , qn+2 ) · · · (qn+m−1 , qn+m ) v02
where vEv02 and [εC ∪ε0 ](h1 , qn , kn , qn+m ). Thus, (v, v)(E×E)(v01 , v02 ).
We now put ?? := qm+n which leads to a valid trace due to
repeated mumbling. Finally, [ε ∪ ε02 ](h1 , h01 , kn , qn+m ) follows from
[εC ∪ ε0 ](h1 , qn , kn , qn+m ) and ε ⊥ ε0 .

l

and h0 = h0p . The case of col and ε1 ,ε2 interchanged is analogous.
Ad 8. This is direct from the definition of atomic and appealing
on the fact that (U, U 0 ) ∈ T (E, ε1 , ∅, ε3 ).


15

2018/3/12

Pure. We start with a trace from rtn(v), for example (h1 , h1 ), v
and an arbitrary heap h01 . We now consider the game involving U
vs. U 0 on t, v and h01 :
t = (q1 , k1 )(q2 , k2 ) · · · (qn , kn ), v
0
t0 = (h01 , k10 )(k10 , k20 ) · · · (kn−1
, kn0 ), v0
We have that vEv0 and [ε3 ](q1 , h01 , kn , kn0 ). By mumbling, (h01 , kn0 ) ∈
U 0 . We can reply with kn0 in the main game.
Dead. Assume given a trace of the form:
(h1 , k1 ) · · · (hn , kn ) v
rds(ε3 )

and h01 such that h1 ∼ h01 . We now initiate a side game U
vs. U 0 on this trace and respond in the main game by stuttering.
Thus, we obtain traces (h01 , h01 ) · · · (h0n , h0n ) () in the main game and
(h01 , k10 ) · · · (h0n , kn0 ) v0 in the side game.
The main trace is in rtn(()). The side game tells us that v = ()
ε1
and that hi −→ ki and therefore [εC1 ](hi , h0i , ki , h0i ). It remains to show
0
that [ε ∪ ε1 ∪ ε02 ](h1 , h01 , kn , kn0 ). This follows from the fact that ε1
has only reads as hi and ki agree on all locations.
Parallelization. We start with a trace in U1 kU2 . Assume that the
trace is of the following form:
t1,1 t2,1 t1,2 t2,2 . . . t1,n t2,n (v1 , v2 )
where each ti, j is a possibly empty sequence of moves of the form
m
m
(h1i, j , ki,1 j ) · · · (hi, ji, j , ki, ji, j ) and
t1 = t1,1 · · · t1,n v1 ∈ U1
t2 = t2,1 · · · t2,n v2 ∈ U2
are traces from U1 and U2 , respectively. We are also given a heap
rds(εC ∪εC ∪ε01 )

rds(ε∪ε01 ∪ε02 )

∼
h01 . We also have h11,1
∼2
run a side game U1 vs. U10 using h01 and t1 , yielding:
h01 such that h11,1

h01 . We

0
0
t1,1
· · · t1,n
v01

Assume that (h01 , k10 ) and (h0o , ko0 ) are, respectively, the first and
last moves of this trace. We have v1 E1 v01 and (1) [εC ∪ εC2 ∪
m
ε01 ](h11,1 , h01 , k1,n
, ko0 ). Notice that these are legal moves in the global
game as we have [εC1 ∪ εC2 ] tiles for the player moves and [ε] times
for the environment moves.
Now, assume there is an environment move (ko , h0o+1 ). Since
ε1 ⊥ ε2 and ε ⊥ ε2 , the heaps h11,1 and h12,1 agree on the reads
of ε02 and h01 and h0o+1 also agree on the reads of ε02 . (Notice as well
that wrs(ε1 )∩rds(ε02 ) = ∅ as εC ∪εC1 ∪ε2 is a valid effect.) Therefore,
we can invoke an U2 game using h0o+1 and t2 , obtaining the trace:
0
0
t2,1
· · · t2,n
v02
0
0
Assume that (h0o+1 , ko+1
) and (h0o+p , ko+p
) are, respectively, the first
and last moves of this trace. We have v2 E2 v02 and (2) [εC ∪ εC1 ∪
m
0
ε02 ](h12,1 , h0o+1 , k2,n
, ko+p
). For the same reasons as above, these are
legal moves in the global game.
Therefore (v1 , v2 )(E1 × E2 )(v01 , v02 ).
m
We need now to prove that [ε ∪ ε01 ∪ ε02 ](h11,1 , h01 , k2,n
, ko+p ). From
m
(1) and ε1 ⊥ ε2 and ε ⊥ ε1 , we have that k2,n
and ko+p agree on the
m
locations of ε1 . Similarly, k2,n
and ko+p agree on the locations of ε2 .
m
Since there are only ε tiles and ε ⊥ ε1 and ε ⊥ ε2 , k2,n
and ko+p
agree on the locations of ε. This finishes the proof.


16

2018/3/12

