has to occur

Verifying C11-Style Weak Memory Libraries via Refinement]Verifying C11-Style Weak Memory Libraries via Refinement

S. Dalvandi]Sadegh Dalvandi
University of Surrey, Guildford, Surrey, United Kingdom
Supported by EPSRC Grant EP/R032556/1.

B. Dongol]Brijesh Dongol
University of Surrey, Guildford, Surrey, United Kingdom

morekeywords=if, then, else, let, in ,keywordstyle=,
literate=   1

Deductive verification of concurrent programs under weak memory
has thus far been limited to simple programs over a monolithic
state space.
For scalability, we also require
modular techniques with verifiable library abstractions. This
paper addresses this challenge in the context of RC11 RAR, a
subset of the C11 memory model that admits relaxed and
release-acquire accesses, but disallows, so-called, load-buffering
cycles. We develop a simple  framework for specifying
abstract objects that precisely characterises the observability
guarantees of abstract method calls. We show how this framework
can be integrated with an operational semantics that enables
verification of client programs that execute abstract method calls
from a library they use. Finally, we show how implementations of
such abstractions in RC11 RAR can be verified by developing a
(contextual) refinement framework for abstract objects. Our
framework, including the operational semantics, verification
technique for client-library programs, and simulation between
abstract libraries and their implementations, has been mechanised
in Isabelle/HOL.

§ INTRODUCTION

The formal verification of concurrent programs in a weak memory setting
is challenging since various writes to the memory locations
may be reordered arbitrarily and therefore seen by other threads
in an order different from the program order. In order to reason
about such programs, the
observations that a thread can make of the writes within
the system should be taken into consideration.

In recent work, reasoning about per-thread observations has led to operational
characterisations of the memory model, where high-level predicates for
reasoning about per-thread observations have been developed, and deductive verification
techniques applied to standard litmus tests and non-trivial synchronisation
algorithms [9].

Current operational verification techniques for weak memory are however, focussed on (closed)
programs, and hence

do not provide straightforward mechanisms for (de)composing clients
and libraries. This problem requires special consideration under weak
memory since the execution of a library
may induce synchronisation. That is, a thread's observations of a system
(including of client variables) can change

when executing
library methods.

This paper addresses several questions surrounding client-library
composition in a weak memory context. Like prior works
[9, 12, 25],
we focus on RC11-RAR, a fragment of C11 memory model, which is one of
the most interesting and challenging fragments for
verification.[The memory model can be extended, but since
this paper focusses on verification and refinement we keep the
memory fragment small to simplify the presentation. ]

(1) How can a client use a weak memory library,
i.e., what abstract guarantees can a library provide a client program?
Prior works [14, 4] describe
techniques for specifying the behaviour of abstract objects,
which are in turn related to their implementations using causal
relaxations of linearizability.

However, these works do not provide a mechanism for reasoning about
the behaviour of client programs that use abstract libraries. In
this paper, we address this gap by presenting a modular operational
that combines weak
memory states of clients and libraries.

This is our first

(2) What does it mean to implement an abstract
library?  To ensure that behaviours of client programs using an
abstract library are preserved, we require contextual
refinement between a library implementation and its abstract
specification. This guarantees that no new client behaviours are
introduced when a client uses a (concrete) library implementation in
place of its (abstract) library specification. Under sequential
consistency (SC), it is well known that linearizable libraries
guarantee (contextual)
refinement [13, 21, 20]. However,
under weak memory, a generic notion of linearizability is difficult to
pin down [14, 11]. We therefore present a direct
technique for establishing contextual refinement under weak memory. A
key innovation is the development of context-sensitive simulation
rules that ensure that each client thread that uses the
implementation observes a subset of the values seen by the
abstraction. This is our second contribution.

(3) Can the same abstract library specify multiple
implementations?  A key benefit of refinement is the ability to use
the same abstract specification for multiple implementations, e.g., to
fine-tune clients for different concurrent workload scenarios. To
demonstrate the applicability of our framework, we provide a
proof-of-concept example for an abstract lock and show that the same
lock specification can be implemented by a sequence lock and ticket
lock. The theory itself is generic and can be applied to concurrent
objects in general; we prove correctness of the Treiber
Stack for RC11-RAR. The original Treiber stack assumes SC memory. We prove correctness under relaxed and release-acquire accesses, thereby showing where additional synchronisation is required under weak memory. This is our third contribution.

(4) How can we support operational verification? Can the
verification techniques be mechanised?
Assuming the existence of an operational semantics for the underlying
memory model, we aim for deductive verification of both
client-library composition and contextual refinement. We show that
this can be supported
by prototyping the full verification stack in the Isabelle/HOL theorem
prover.[Our Isabelle theories may be accessed via [7]. Note that the theories require Isabelle 2020.] All of the programs, theorems and proof rules in this paper are fully verified. Our Isabelle development is around 25 KLOC (thousand lines of code), where around 2.5 KLOC is taken from [10].
This is our fourth contribution.

Closely related to our work is that of Raad et al. [37],
who have tackled the
problem of client-library programs in a declarative
framework. Their framework provides support for axiomatic
specifications of weak memory concurrent libraries and verification of
library implementations against these specifications. Although this work addresses a similar set of questions to ours, there are several key differences in our approach.

We move from a declarative to an operational semantics, which provides
a significant step-change as it allows integration with
well-understood reasoning techniques of Owicki-Gries
(cf. sec:hoare-logic-c11) and refinement
(cf. sec:cont-refin), as well as the possibility of
rely-guarantee in future work. Raad et al
[37] also describe a notion of
refinement, but their definition is not based on trace
refinement. Moreover, our operational semantics enables a new approach
to library specifications than Raad et
al. [37]. In particular, we follow
an approach in which library operations interact with weak memory in a
manner that is similar to the interaction between standard reads and
writes within C11 (see sec:specifying-c11-style). This paves
the way for implementations that take further advantage of weak
memory, since our specifications allow new operations to be introduced
in the “middle” of an existing abstract history. This is akin to
checking multiple complete executions in a declarative approach for each legal position of the operation.

The strength of Raad et al.'s declarative approach
[37] is that it considers more than
one memory model and handles so-called “towers of abstraction”,
where a library implementation can in turn use other library
specifications. The former is more complex in an operational setting
since the operational rules are fine-tuned to a particular memory
model, but the latter can be handled via straightforward extensions to
the semantics (see Aside <ref>).[We have not done
this here to simplify the presentation.] On the other hand, our approach
is in a stronger position w.r.t mechanised verification. While  our
development (including all examples and case studeis) is fully mechanised,
[37] has only achieved a partial
mechanisation over a small parts of their contribution.

Overally, the contributions of our work  can be seen as follows.
First, it presents an
approach for specifying abstract libraries and the associated view-based
assertions that allows verification of client programs that use the
abstract library in an Owicki-Gries setting. Second, it introduces
a generalised  operational semantics for C11 weak memory that allows
implementation of C11-style libraries and also provides an assertion
language that allows for verification of libraries at the implementation
level. Third, it provides a refinement
framework that allows one to prove that an implementation correctly
refines the abstract specification. The first two, can be used independently
and offers enough support (in varying levels of abstraction) to verifying
client-library programs. The third contribution, allows for establishing
a formal link between the high level abstract specification of a library
and its implemenation.

The general workflow of our approach is as follows:

* Defining the abstract operational specification of a library.

* Verifying client programs that uses the library operations using Hoare logic
and Owicki-Gries.

* Implementing the library using the generalised operational
semantics of C11.

* Proving that the implementation is a contextual refinement of the
abstract specification and therefore it can safely replace the abstract
specification in the client programs.

In sec:message-passing-via we motivate the main ideas and
illustrate the basic principle of message-passing synchronisation, but
for programs comprising a program executing with an abstract
library. sec:gener-weak-memory presents a modular programming language
and operational semantics for reads/write accesses within this
language. A method for encoding the operational semantics of abstract
objects is given in sec:abstr-object-semant. In
sec:example-verification, we describe verification of client
programs that use abstract libraries, and in sec:cont-refin
we present our refinement theory. We use an abstract lock and two
different implementations of this lock as running examples.

Finally, in sec:view-based-relax, we discuss the
specification of generic concurrent objects that exploit view-based
relaxations, making use of the framework developed in
sec:abstr-object-semant. Here, we also describe the
verification of the Treiber Stack adapted for C11.

§ MESSAGE PASSING VIA LIBRARY OBJECTS

We first illustrate the basic principles of client-object synchronisation in weak memory.

Init:  $d:=0;$ $s.init();$

$\begin{array}{@{}l@{\ }||@{\ }l}
\text{\bf Thread } 1
& \text{\bf Thread } 2\\
d := 5; \qquad &
\text{\bf do } r_1 := s.pop() \\

s.push(1); & \text{\bf until}\ r_1 = 1;  \\
& r_2 \gets d; \\
\end{array}$

$\{r_2 = 0 \lor r_2=5\}$

Unsynchronised message passing

Init: $d:=0;$ $s.init();$

$\begin{array}{@{}l@{\ }||@{\ }l}
\text{\bf Thread } 1
& \text{\bf Thread } 2\\
% {\color{blue} \{ f \not \approx_2 1 \wedge d =_1 0\}} & {\color{blue} \{ \CObs{f}{1}{t}{d}{5} \}} \\
d := 5; \qquad &
\text{\bf do } r_1 := s.pop^{\sf A}() \\
s.push^{\sf R}(1);               & \text{\bf until}\ r_1 = 1;  \\
% {\color{blue} \{ f \not \approx_2 1 \wedge d =_1 5\}} & {\color{blue} \{ d =_2 5\}} \\

& r_2 \gets d; \\
% {\color{blue} \{ true\}} & {\color{blue} \{r_2 = 5\} }

\end{array}$

$\{ r_2=5\}$

Publication via a synchronising

Client-object message passing.

Under SC all threads have a single common view of the shared
state. When a new write is executed, the “views” of all threads are
updated so that they are guaranteed to only see this new latest write. In
contrast, each thread in a C11 program has its own view of each
variable. Views may not be updated when a write occurs, allowing
threads to read stale writes. To enforce view updates, additional
synchronisation (e.g., release-acquire) must be introduced [5, 25, 32].

Now consider a generalisation of this idea to (client) programs that use
The essence of the problem is illustrated by the message-passing programs in Figures <ref> and <ref>.

Under SC, when the program in
fig:po-message-bad terminates, the value of $r_2$ is
guaranteed to be $5$.

However, this is not necessarily true in a weak memory setting. Even
if $pop$ operation in thread 2 returns 1, it may be possible for
thread 2 to observe a stale value 0 for $d$. Therefore the program only
guarantees the weaker postcondition $r_2 = 0 \lor r_2 = 5$.

To address this problem, the library operations in
fig:publication are annotated with release-acquire
annotations. In particular, the client assumes the availability of a
“releasing push” ($push^{\sf R}(1)$), which is to be used for
message passing. Thread 2 pops from $s$ using an “acquiring pop”
($pop^{\sf A}()$). If this pop returns 1, the stack operations induce
a happens-before synchronisation in the client, which in turn means
that it is now impossible for thread 2 to read the stale initial
write for $d$.

Verification strategy.

Our aim is to enable deductive verification of such programs by
leveraging recently developed operational semantics, assertion
language and Owicki-Gries style proof strategy for RC11
RAR [9]. We show that these existing concepts generalise
naturally to client-object, and in a manner that enables modular

The assertion language of [9] enables reasoning about a
thread's views, e.g., in fig:mp-proof, after initialisation,
thread $t \in \{1,2\}$ has definite value $0$ for $d$
(denoted $[d = 0]_t$).
In this paper, we extend such assertions to capture thread views over
library objects. E.g., after initialisation, the only value a pop by
thread $t$ can return is $empty$, and this is captured by the
assertion $[s.pop({empty})]_t$.

The precondition of $d := 5$ states that thread 2 cannot pop value
$1$ from $s$ (as captured by the assertion $\neg \langle

The precondition of the $\kwuntil$ loop in thread 2 contains a conditional observation assertion (i.e.,
$\langle s.pop(1) \rangle [d = 5]_2$), which states that if thread 2
pops value 1 from $s$ then it will subsequently be in a state where it
will definitely read $5$ for $d$.

A key benefit of the logic in [9] is that it enables the use of
standard Owicki-Gries reasoning and straightforward
mechanisation [8]. As we shall see (sec:example-client-lbjec), we maintain these benefits in
the context of client-object programs.

Init:  $d:=0;$ $s.init();$

$\{[d = 0]_1 \wedge [d = 0]_2 \wedge [s.pop({empty})]_1 \wedge [s.pop({empty})]_2\}$

$\begin{array}{l@{\quad}||@{\quad }l}
\text{\bf Thread } 1
& \text{\bf Thread } 2\\
\begin{array}[t]{@{}l@{}}
{\color{blue} \{ \neg \langle s.pop(1) \rangle_2 \wedge [d = 0]_1\}} \\
1: d := 5; \\
{\color{blue} \{ \neg \langle s.pop(1) \rangle_2 \wedge [d = 5]_1\}} \\
2: s.push^{\sf R}(1); \\
{\color{blue} \{ true\}}
\end{array}
\begin{array}[t]{@{}l@{}}
{\color{blue} \{ \langle s.pop(1) \rangle [d= 5]_2 \}} \\
3: \text{\bf do } r_1 := s.pop^{\sf A}()\
\text{\bf   until}\ r_1 = 1; \\
{\color{blue} \{ [d = 5]_2\}} \\
4: r_2 \gets d; \\
{\color{blue} \{r_2 = 5\} }
\end{array}
\end{array}

$\{ r_2=5\}$

A proof outline for message passing

Contextual refinement.

Contextual refinement relates a client using an abstract object with a
client that uses a concurrent implementation of the object. More precisely, we say
that a concrete object $CO$ is a contextual refinement of an
abstract object $AO$ iff for any client $C$, every behaviour of $C$
when it uses $CO$ is a possible behaviour of $C$ when it uses
$AO$. Thus, there is no observable difference to any client when it
uses $CO$ in place of $AO$.

In a weak memory setting, to enable a client to use an object,
one must specify how synchronisation between object method
calls affects the client state. To implement such a
specification, we must describe how the abstract synchronisation
are represented in the implementation. Prior works have appealed to
extensions of notions such as linearizability to ensure contextual
[14, 19, 37]. In
this paper, we aim for a more direct approach and consider contextual

§ GENERALISED
OPERATIONAL SEMANTICS

We now present a simple program syntax

that allows one to write open programs
that can be filled by an abstract method or concrete implementation of
a method.

§.§ Program Syntax

We start by defining a syntax of concurrent programs, starting with
the structure of sequential programs (single threads).  A thread may
use global shared variables (from $\GVar$) and local registers
(from $\LVar$).  We let $\Var = \GVar \cup \LVar$ and assume
$\GVar \cap \LVar = \emptyset$. For client-library programs, we
partition $\GVar$ into $\GVar_C$ (the global client variables) and
$\GVar_L$ (the global library variables) and similarly $\LVar$ into
$\LVar_C$ and $\LVar_L$. In an implementation, global variables can be
accessed in three different synchronisation modes: acquire (A, for reads), release (R, for writes) and relaxed (no
annotation).  The annotation RA is employed for update
operations, which read and write to a shared variable in a single
atomic step.

We let $\Obj$ and $\Meth$ be the set of all objects and method calls,

We assume that
$\ominus$ is a unary operator (e.g., $\neg$), $\oplus$ is a binary
operator (e.g., $\land$, $+$, $=$) and $n$ is a value (of type
$\Val$). Expressions must only involve local

The syntax of sequential programs, $\Comm$, is given by the following
grammar with $r \in \LVar, x \in \GVar, o \in \Obj, m \in \Meth, u, v \in \Val$:

t]r@ ll
$\Exp_L$   ::=     $\Val \mid \LVar  \mid \ominus \Exp_L \mid \Exp_L \oplus Exp_L$

$\CExp_L$   ::=     $\bullet \mid \Exp_L$

$\bullet$ ::=     $\Val \mid o.m([u]) \mid \Comm $, where $\Comm$ contains no holes

$\AComm$ ::=     $ \bullet \mid \kwskip \mid % x.\kwswap(v)^{\sf RA} \mid
r \gets \kwcas^{\sf [R] [A]}(x, u, v)
\mid$

$r \gets \kwfai^{\sf [R] [A]}(x)
% \mid x := \Exp_L \mid
\mid r := \CExp_L
\mid {} $
$x :=^{\sf [R]} \Exp_L \mid  r \gets^{\sf [A]} x$

$\Comm$ ::=     $\AComm \mid \Comm ; \Comm \mid \kwif~B\ \kwthen\ \Comm\ \kwelse\ \Comm \mid
\kwwhile\ B\ \kwdo\ \Comm$

where we assume $B$ to be an expression of type $\CExp_L$
that evaluates to a boolean.

We allow programs with holes, denoted
$\bullet$, which may be filled by an abstract or concrete method
call. During a program's execution, the hole may also be filled by
the null value $\bot \notin
\Val$, or the return value of the method call.
The notation ${\sf [X]}$ denotes that the annotation ${\sf X}$ is
optional, where ${\sf X} \in \{{\sf A}, {\sf R}\}$, enabling one to
distinguish relaxed, acquiring and releasing accesses. Within a method
call, the argument $u$ is optional. Later, we will also use
$\kwdo$-$\kwuntil$ loops, which is straightforward to define in terms
of the  syntax above.

§.§ Program Semantics

For simplicity, we assume concurrency at the top level only. We let
$\Tid$ be the set of all thread identifiers and use a function
$\Prog: \Tid \to \Comm$ to model a program comprising multiple
threads. In examples, we typically write concurrent programs as
$C_1 || \ldots || C_n$, where $C_i \in \Comm$.  We further assume some
initialisation of variables.  The structure of our programs
thus is $\Init; \big( C_1 || \ldots || C_n \big) $.

The operational semantics for this language is defined in three parts.
The program semantics fixes the steps that the concurrent
program can take.  This gives rise to transitions
$(P,\lstate) \trans {a}_t (P',\lstate')$ of a thread $t$ where $P$ and
$P'$ are programs, $\lstate$ and $\lstate'$ is the state of local
variables and $a$ is an action (possibly the silent action $\epsilon$,
see below).  The program semantics is combined with a memory
semantics reflecting the C11 state, and in particular the writes from which a read action can
Finally, there is the object semantics, which defines the
abstract semantics of the object at hand.

We assume that the set of actions is given by $\Act$. We let
$\epsilon \notin \Act$ be a silent action and let
$\Act_\epsilon = \Act \cup \{\epsilon\}$.
For an
expression $E$ over local variables, we write $\llbr{E}_{\ls}$ for the
value of $E$ in local state $\ls$; we write $\ls[r := v]$ to state
that $\ls$ remains unchanged except for the value of local variable
$r$ which becomes $v$. We use $C[D]$ to denote the program $C$ with the
hole filled by $D$. If $D = \bot$, we proceed with the execution of
$C$, otherwise we execute $D$. Note that if $D$ terminates with a
value (due to a method call that returns a value), then the hole
contains a value and execution may proceed by either using the rule
for $r \asgn v$ or the rule for $v ; C_2$, both of which are present
in fig:comm-sem. The last two rules, Cli and Lib,
lift the transitions of threads to a transition of a client and
library program, respectively. These are distinguished by the
subscript $L$, which only appears in transitions corresponding to the

$\inference{r \in \LVar \quad v = \llbr{E}_{{\it ls}}}{(r := E,{\it ls}) \trans{\epsilon} (\kwskip,\ls[r := v]) }\hfill
\inference{x \in \GVar \quad a = wr^{\sf [R]}(x, \llbr{E}_{{\it ls}}) }{(x :=^{\sf [R]} E,ls) \trans{a} (\kwskip,\ls) }\hfill \inference{a = rd^{\sf [A]}(x,v) \quad v \in \Val}{ (r \gets^{\sf [A]} x, \ls) \trans a (\kwskip,\ls[r := v]) }
\inference{(C_1,\ls) \trans{a} (C_1',ls')}{(C_1 ; C_2,\ls) \trans{a}
(C_1' ; C_2,\ls')}\hfill
\inference{v \in \Val \cup \{\bot\}}{(v ; C_2,\ls) \trans{\epsilon}
\inference
{({\it IF}, \ls) \trans{\epsilon} (C_1,\ls)}
\hfill\inference
{\neg \llbr{B}_{\ls}}
{({\it IF}, \ls) \trans{\epsilon} (C_2,\ls) }

\inference{\llbr{B}_{\ls}}{
\begin{array}[t]{@{}l@{}}
({\it WHILE}, \ls)
\trans{\epsilon}  (C; {\it WHILE}, \ls)
\end{array}
}     \qquad
\inference{\neg \llbr{B}_{\ls}}
\begin{array}[t]{@{}l@{}}
({\it WHILE}, \ls)  \trans{\epsilon}  (\kwskip, \ls)
\end{array}
}    \qquad
\inference{}{ (\COSem{C}{\kwskip}, \ls) \trans \epsilon (C,\ls) }$

$  \inference{(D, ls) \trans a (D', ls')}{ (\COSem{C}{D}, \ls) \trans{a}_L (\COSem{C}{D'},\ls') }
\qquad
\inference{a = rd(x,v') \quad v'\neq u \quad u,v,v' \in \Val}{ (r \gets \kwcas^{\sf [R] [A]}(x, u, v), \ls) \trans a (\kwskip,\ls[r := \False]) }

\inference{a = upd^{\sf X}(x,u,v) \quad u,v \in \Val}{ (r \gets \kwcas^{\sf X}(x, u, v), \ls) \trans a (\kwskip,\ls[r := \True]) }
\qquad
\inference{a = upd^{\sf X}(x,u,u+1) \quad u \in \Val}{ (r \gets \kwfai^{\sf X}(x), \ls) \trans a (\kwskip,\ls[r := u]) }

\inference[\sc
Cli]{(P(t), \ls) \trans{a} (C,\ls') \quad a \in \Act_\epsilon}
{(P,\lstate) \trans{a}_t (P[t := C], \ls')}
\qquad
\inference[\sc
Lib]{(P(t),\lstate) \trans{a}_L (C,\ls') \quad a \in \Act_\epsilon}
{(P,\lstate) \trans{a}_{L, t} (P[t := C], \ls')}

Program semantics, where ${\it IF} = \kwif \ B\ \kwthen\
C_1\ \kwelse\ C_2$ and ${\it WHILE} = \kwwhile\ B\ \kwdo\ C$

The rules in fig:comm-sem allow for all possible values
for any read. We constrain these values

with respect to a memory semantics (formalised by
$\strans{a}_t$), which is described for reads, writes and updates in
sec:memory-semantics and for abstract objects in

The combined semantics brings together a client state $\gamma$ and library
state $\beta$ as follows.

\begin{gather*} \small
\inference{(P,\lstate) \trans {\epsilon }_t (P',\lstate')}
{(P,\lstate,\gamma, \beta) \ltsArrow{% \beta
} (P', \lstate',\gamma, \beta)}  \small
\qquad
\inference{(P,\lstate) \trans {\epsilon }_{L,t} (P',\lstate')}
{(P,\lstate,\gamma, \beta) \ltsArrow{% \beta
(P', \lstate',\gamma, \beta)}
\\[1mm] \small
\inference{(P,\lstate) \trans {a}_t (P',\lstate') \qquad  \gamma,
\beta \strans{a}_{t} \gamma', \beta'} {(P,\lstate,\gamma, \beta)
\ltsArrow{% a
} (P', \lstate',\gamma', \beta')} % \label{sem-comb}
\qquad
\inference{(P,\lstate) \trans {a}_{L,t} (P',\lstate') \qquad
\beta, \gamma \strans{a}_{t} \beta', \gamma'}
{(P,\lstate,\gamma, \beta)
\ltsArrow{% a
} (P', \lstate',\gamma', \beta')}
\end{gather*}

These rules ensure, for example, that a read only returns a value
allowed by the underlying memory model. In
sec:abstr-object-semant, we introduce additional rules so
that the memory model also contains actions corresponding to method
calls on an abstract object.

Note that the memory semantics (see sec:memory-semantics and sec:abstr-object-semant) defined
by $\gamma, \beta \strans{a}_t \gamma', \beta'$ assumes that $\gamma$ is
the state of the component being executed and $\beta$ is the state of
the context. For a client step, we have that $\gamma$ is the
executing component state and $\beta$ is the context state, whereas
for a library step, these parameters are swapped.

§.§ Memory Semantics

Next, we detail the modularised memory semantics, which builds on an
earlier monolithic semantics [9], which is a
timestamp-based revision of an earlier operational
semantics [12]. Our present extension
is a semantics that copes with client-library interactions in weak
memory. Namely, it describes how synchronisation (in our example
release-acquire synchronisation) in one component affects thread views
in another component. The semantics
accommodates both client synchronisation affecting a library, and vice

Component State.

We assume $\Act$ denotes the set of actions. Following [9],
each global write is represented by a pair
$(a, q) \in \Act \times \rat$, where $a$ is a write action, and $q$ is
a rational number that we use as a timestamp corresponding to
modification order (cf.
[25, 16, 36]).
The set of modifying operations within a component that have occurred
so far is recorded in $\writes \subseteq \Act \times \rat$. Unlike
prior works, to accommodate (abstract) method
calls of a data structure, we record abstract operations in general,
as opposed to writes only.

Each state must record the operations that are observable to each
thread. To achieve this, we use two families of functions from global
variables to writes (cf.
[36, 27]).

* A thread view function $\tview_t \in \GVar \rightarrow \writes$ that returns the
viewfront of thread $t$. The thread $t$ can read from any
write to variable $x$ whose timestamp is not earlier than
$\tview_t(x)$. Accordingly, we define, for each state $\gamma$,
thread $t$ and global variable $x$, the set of observable
writes, where $\tst(w) = q$ denotes $w$'s timestamp:

\gamma.\OW(t, x) =  \{(a, q) \in \gamma.\writes  \mid
\begin{array}[t]{@{}l@{}}
\mathit{var}(a) = x    {}\wedge \tst(\gamma.\tview_t(x)) \leq q\}
\end{array}

* A modification view function $\mview_w \in  \GVar \rightarrow \Act \times \rat$ that records the
viewfront of write $w$, i.e., the viewfront of the thread
that executed $w$ immediately after $w$'s execution. We use
$\mview_w$ to compute a new value for $\tview_t$ if a thread $t$
synchronizes with $w$, i.e., if $w \in \WR$ and another
thread executes an $e \in \RA$ that reads from $w$.

The client cannot directly access writes in the library, therefore the thread
view function must map to writes within the same component. On the other
hand, synchronisation in a component can affect thread views in
another (as discussed in sec:message-passing-via), thus the
modification view function may map to operations across the system.

Finally, our semantics maintains a set $\covered \subseteq
\writes$. In C11 RAR, each update action occurs in modification order
immediately after the write that it reads from
[12]. This property ensures the
atomicity of updates.
We disallow

any newer modifying operation (write or update) from intervening
between any update and the write or update that it reads from.  As we
explain below, covered writes are those that are immediately prior to
an update in modification order, and new write actions never interact
with a covered write (i.e. do not write immediately after them in the modification order).

$\GVar_C = \{x_1, ... , x_n\}$, $\GVar_L = \{y_1, ..., y_{n'}\}$,
$\LVar = \{r_1, ... , r_m\}$,
$k_i, k_i', l_i \in \Val$, and
$\Init = x_1:=k_1; \ldots, x_n:=k_n ; [r_1 := l_1 ;] \dots [r_m :=
l_m;]$, where we use the notation $[r_i := l_i;]$ to mean that the
assignment $r_i := l_i$ may optionally appear in $\Init$. Thus each
shared variable is initialised exactly once and each local variable is
initialised at most once. The initial values of the state components
are then as follows, where we assume $0$ is the initial
timestamp, $t$ is a thread, $x_i \in \GVar_C$ and $y_i \in \GVar_L$

\begin{align*}
& \gamma_\Init.\writes  = \bigcup_{1 \leq i \leq n }\{(wr(x_i,k_i),0)\}
& \beta_\Init.\writes  = \bigcup_{1 \leq i \leq n' }\{(wr(y_i,k_i'),0)\} \\
& \gamma_\Init.\tview_t(x_i) =  (wr(x_i,k_i),0)
& &
\beta_\Init.\tview_t(y_i) =  (wr(y_i,k_i'),0) \\
& \gamma_\Init.\covered  = \beta_\Init.\covered= \emptyset & &
\gamma_\Init.\mview_{x_i} =
\begin{array}[t]{@{}l@{}}
\beta_\Init.\mview_{y_i}= \\\gamma_\Init.\tview_t \!\cup\! \beta_\Init.\tview_t
\end{array}
\end{align*}

The local state component of each thread must also be compatible with
$\Init$, i.e., for each $t$ if $r_i \in \dom(lst(t))$ we have that
$({\it lst}(t))(r_i) = l_i$ provided $r_i := l_i$ appears in $\Init$.
We let ${\it lst}_\Init$ be the local state compatible with $\Init$
and let $\Gamma_\Init = ({\it lst}_\Init,\gamma_\Init, \beta_\Init)$.

$\inference[{\sc Read}] {a \in \{rd(x, n), rd^\mathsf{A}(x, n) \}
\qquad (w, q) \in \gamma.\OW(t, x) \qquad
\wrval(w) = n \\
\tview' = \ensuremath{%\mbox{$$
\begin{cases}
\gamma.\tview_t\otimes\gamma.\mview_{(w,q)}&\mbox{if
$(w, a) \in \WR \times \RA$ % synchronise
% in $\gamma$
\gamma.\tview_t[x := (w, q)]&\mbox{otherwise}
\end{cases}} %$$
\\    \ctview' = \ensuremath{%\mbox{$$
\begin{cases}
\beta.\tview_t\otimes\gamma.\mview_{(w,q)}&\mbox{if
$(w, a) \in \WR \times \RA$ % synchronise
% in $\gamma$
\beta.\tview_t &\mbox{otherwise}
\end{cases}} %$$
{\gamma, \beta\  \strans{a}_{t}\  \gamma[\tview_t \asgn \tview'], \beta[\tview_t \asgn \ctview'] }$
$ \inference[{\sc Write}] {
a \in \{ wr(x,n), wr^{\sf R}(x,n)\} \qquad (w, q) \in \gamma.\OW(t, x) \setminus \gamma.\covered \qquad \fresh_\gamma(q,q') \\
\writes' = \gamma.\writes \cup \{(a, q')\} \qquad
\tview' = \gamma.\tview_t[x := (a, q')] \qquad \mview' = \tview' \cup \beta.\tview_t
{\gamma, \beta\  \strans{a}_{t}\  \gamma[\tview_t \asgn \tview', \mview_{(a,q')} \asgn \mview', \writes \asgn \writes'], \beta }$
\inference[{\sc Update-RA}] {
a = upd^{\sf
\qquad (w, q) \in \gamma.\OW(t, x) \setminus \gamma.\covered
\qquad
\wrval(w) = m
\qquad
\fresh_\gamma(q,q') \\ \writes' = \gamma.\writes \cup \{(a, q')\} \qquad
\covered' = \gamma.\covered \cup \{(w, q)\} \qquad \mview' = \tview' \cup \ctview'
\\
\tview' = \ensuremath{%\mbox{$$
\begin{cases}
\gamma.\tview_t[x \asgn (a,
q')]\otimes\gamma.\mview_{(w,q)}&\mbox{if $w \in
\WR$ % if $w$, $a$ synchronise in $\gamma$
\gamma.\tview_t[x \asgn (a, q')]&\mbox{otherwise}
\end{cases}}%$$}
\\
\ctview' = \ensuremath{%\mbox{$$
\begin{cases}
\beta.\tview_t \otimes\gamma.\mview_{(w,q)}&\mbox{if $w \in
\WR$ % if $w$, $a$ synchronise in $\gamma$
\beta.\tview_t &\mbox{otherwise}
\end{cases}}
{\gamma, \beta\ \strans{a}_{t}\  \gamma\left[
\begin{array}[c]{@{}l@{}}
\tview_t \asgn \tview', \mview_{(a,q')} \asgn \mview', \\
\writes \asgn \writes',
\covered \asgn \covered'
\end{array}\right], \beta[\tview_t\asgn \ctview']}$

\inference[{\sc Update-Rel}] {
a = upd^{\sf R}(x,m,n)
\qquad (w, q) \in \gamma.\OW(t, x) \setminus \gamma.\covered
\qquad
\wrval(w) = m
\\
\fresh_\gamma(q,q') \qquad \writes' = \gamma.\writes \cup \{(a, q')\} \qquad
\covered' = \gamma.\covered \cup \{(w, q)\}
\\
\tview' = \gamma.\tview_t[x \asgn (a, q')] \qquad \mview' = \tview' \cup \beta.\tview_t
{\gamma, \beta\ \strans{a}_{t}\  \gamma\left[
\begin{array}[c]{@{}l@{}}
\tview_t \asgn \tview', \mview_{(a,q')} \asgn \mview',
\writes \asgn \writes',
\covered \asgn \covered'
\end{array}\right], \beta}$

Transition relation for reads, writes and updates of the
memory semantics

Transition semantics.
The transition relation of our semantics for global reads and writes
is given in fig:surrey-opsem and builds on an earlier
semantics that does not distinguish the state of the
context [9]. Each transition
$\gamma, \beta \strans{a}_{t} \gamma', \beta'$ is labelled by an action
$a$ and thread $t$ and updates the target state $\gamma$ (the state of
component being executed) and the context

Read transition by thread $t$. Assume that $a$ is
either a relaxed or acquiring read to variable $x$, $w$ is a write to
$x$ that $t$ can observe (i.e., $(w, q) \in \gamma.\OW(t,x)$), and the
value read by $a$ is the value written by

Each read causes the viewfront of $t$ to be updated. For an
unsynchronised read, $\tview_t$ is simply updated to include the new
write. A synchronised read causes the executing thread's view of the
executing component and context to be updated. In particular, for each
variable $x$, the new view of $x$ will be the later (in timestamp
order) of either $\tview_t(x)$ or $\mview_w(x)$. To express this, we
use an operation that combines two views $V_1$ and $V_2$, by
constructing a new view from $V_1$ by taking the later view of each
\begin{align*}
V_1 \otimes V_2  = \lambda x \in \dom(V_1).\ &
\textbf{if}~\tst(V_2(x)) \leq \tst(V_1(x))\  \textbf{then}\ V_1(x)\ \textbf{else}\  V_2(x)
\end{align*}

Write transition by thread $t$. A write
transition must identify the write $(w,q)$ after which $a$
occurs. This $w$ must be observable and must not be covered —
the second condition preserves the atomicity of read-modify-write (RMW)
updates. We must choose a fresh timestamp $q' \in \rat$ for $a$, which
for a C11 state $\gamma$ is formalised by $\fresh_\gamma(q, q') = q < q' \wedge \forall w' \in \gamma.\writes.\ q < \tst(w') \Rightarrow q' < \tst(w')$.

That is, $q'$ is a new timestamp for variable $x$ and that
$(a,q')$ occurs immediately after $(w,q)$. The new write is added to
the set $\writes$.

We update $\gamma.\tview_t$ to include the new
write, which ensures that $t$ can no longer observe any writes prior to
$(a, q')$. Moreover, we set the viewfront of $(a, q')$ to be the new
viewfront of $t$ in $\gamma$ together with the thread viewfront of the
environment state $\beta$. If some other thread synchronises with this
new write in some later transition, that thread's view will become at
least as recent as $t$'s view at this transition. Since $\mview$ keeps
track of the executing thread's view of both the component being
executed and its context, any synchronisation through this new write
will update views across components.

Update (aka RMW) transition by thread $t$. These
transitions are best understood as a combination of the read and write
transitions. As with a write transition, we must choose a valid fresh
timestamp $q'$, and the state component $\writes$ is updated in the
same way. State component $\mview$ includes information from the new
view of the executing thread $t$.  As discussed earlier, in Update transitions it is necessary to record that the write that
the update interacts with is now covered, which is achieved by adding
that write to $\covered$. Finally, we must compute a new thread view,
which is similar to a Read transition, except that the thread's
new view always includes the new write introduced by the

[Generalisation to multiple components]

The semantics can be extended to handle multiple environment
components, e.g., if a single client is interacting with multiple
libraries. Here, the context $\beta$ in fig:surrey-opsem
would be generalised to a set of states $S$. Release-acquire
synchronisation in the component $\gamma$, would lead to an updates in
the thread views for each of the context states in $S$. This would
lead to generalisation of the assertions in
sec:example-verification and the refinement rules in

§ ABSTRACT OBJECT SEMANTICS

The rules in fig:surrey-opsem provide a semantics for read,
write and update operations for component programs within an executing
context and can be used to model clients and libraries under RC11
RAR. These rules do not cover the behaviour of abstract objects, which
we now consider.

There have been many different proposals for specifying and verifying
concurrent objects
memory [28, 4, 19, 26, 37, 11, 14],
since there are several different objectives that must be addressed.
These objectives are delicately balanced in
linearizability [23], the most well-used consistency
condition for concurrent objects. Namely, linearizability ensures:

* The abstract specification is explainable with respect to a
sequential specification.

* Correctness is compositional, i.e., any concrete
execution of a system  comprising two linearizable objects is
itself linearizable.

* Correctness ensures contextual (aka observational)
refinement, i.e., the use of a linearizable implementation within
a client program in place of its abstract specification does not
induce any new behaviours in the client program.

There is however an inherent cost to linearizability stemming from the
fact that the effect of each method call must take place before
the method call returns. In the context of weak memory, this
restriction induces additional synchronisation that may not
necessarily be required for
correctness [41]. Therefore, over
the years, several types of relaxations to the above requirements have
been proposed
[28, 4, 19, 26, 37, 11, 14].

General data structures present many different design choices at the
abstract level [37], but discussing these now detracts from our main
contribution, i.e., the integration and verification of clients and
libraries in a weak memory model.

Therefore, we restrict our attention to an abstract lock object, which
is sufficient to highlight the main ideas. Locks have a clear ordering
semantics (each new lock $\acquire$ and lock $\release$ operation must
have a larger timestamp than all other existing operations) and
synchronisation requirements (there must be a release-acquire
synchronisation from the lock  to the lock

To enable proofs of contextual refinement (see
sec:cont-refin), we must ensure corresponding method calls
return the same value at the abstract and concrete levels. To this
end, we introduce a special variable $rval$ to each local state that
stores the value that each method call returns.
[Abstract lock]

Consider the specification of a lock with methods
Acquire and Release.

Each method call of the lock is indexed by a subscript to uniquely
identify the method call.  For the lock, the subscript is a counter
indicating how many lock operations have been executed and is used
in the example proof in sec:example-verification.

\[
\inference[{\sc Acq}] {a = l.\acquire_n \quad ls' = ls[rval := \True]
{({\tt l.Acquire()}, ls) \trans a (\True, ls')}
\quad \ \ \inference[{\sc Rel}]
{a = l.\release_n \quad ls' = ls[rval := \bot]}
{({\tt l.Release()}, ls) \trans a (\bot, ls')}
\]

Locks, by default are synchronising, i.e., in the memory
semantics, a (successful)  requires the operation to
synchronise with the most recent lock  (in a manner
consistent with release-acquire semantics), so that any writes that
are happens-before ordered before the  are visible to
the thread that acquires the lock. The initial state of an abstract
lock $l$, $\gamma_\Init$, is given by:

\begin{align*}
\gamma_\Init.\writes & = \{(l.init_0,0)\}
\alpha_\Init.\tview_t(l) & =  (l.init_0,0)
\alpha_\Init.\covered & =  \emptyset
\end{align*}

We also obtain the rules below, where  $\alpha$ is the state of
the lock and $\gamma$ is the state of the client.

To record the thread that currently owns the lock, we derive a new
action, $b$, from the action $a$ of the program
semantics. Action $(w, q)$ represents the method that is observed by
the $\acquire$ method, which must be an operation in
$\alpha.\writes$ such that $q$ has the maximum timestamp for $l$
(i.e., $q = \maxTS(\alpha.\writes_{|l})$). The new timestamp $q'$ must be larger
than $q$. We create a new component state $\alpha'$ from $\alpha$ by (1) inserting $(b, q')$ into $\alpha.\writes$; (2) updating $\tview_t$ to $\tview'$, where $\tview'$
synchronises with the previous thread view in $\alpha$ to include
information from the modification view of $(w, q)$, and updates $t$'s view of $l$ to include the new operation $(b, q')$;  (3)  updating the contextual thread view for $t$ to $\ctview'$,
where $\ctview'$ synchronises with the previous thread view in the
context state $\gamma$ to include information from the modification
view of $(w, q)$; and (4) updating the modification view for the new operation $(b, q')$
to $\mview'$, where $\mview'$ contains the view of $t$.
Finally, the context state $\gamma'$ updates the thread view of $t$ to
$\ctview'$ since synchronisation with a release may cause the view
to be updated.

A lock release, simply introduces a new operation with a maximal
timestamp, provided that the thread executing the release currently holds
the lock.

$    \inference[{\sc Acquire}] {
a = l.\acquire_n  \qquad b = l.\acquire_n(t) \qquad (w, q) \in \alpha.\writes \qquad  w \in \{l.init_0, l.\release_{n-1}\} \\
q = \maxTS(\alpha.\writes_{|l}) \qquad q < q' \\ \writes' = \alpha.\writes
\cup \{(b, q')\}
\qquad \mview' = \tview' \cup \ctview' \qquad \covered' = \sigma.\covered \cup \{(w,q)\} \\
\tview' = \alpha.\tview_t[l \asgn (b,
q')]\otimes\alpha.\mview_{(w,q)} \quad \ctview' = \gamma.\tview_t
\otimes\alpha.\mview_{(w,q)} \\
} {\alpha, \gamma\ \strans{a}_{t}\
\alpha\left[
\begin{array}[c]{@{}l@{}}
\writes := \writes', \tview_t := \tview',
\\
\mview_{(b, q')} := \mview', \covered := \covered'
\end{array}\right]
, \gamma[\tview_t \asgn \ctview']}

\inference[{\sc Release}] {
a = l.\release_n \quad w = l.\acquire_{n-1}(t) \quad
(w, q) \in \alpha.\writes \quad
q = \maxTS(\alpha.\writes_{|l}) \quad q < q'  \\
\writes' = \alpha.\writes \cup \{(a, q')\} \qquad
\tview' = \alpha.\tview_t[x \asgn (a, q')]
\\
\mview' = \tview' \cup \gamma.\tview_t
{\alpha, \gamma\  \strans{a}_{t}\  \alpha\left[
\begin{array}[c]{@{}l@{}}
\writes := \writes', \tview_t := \tview',
\mview_{(a, q')} := \mview'
\end{array}\right]
, \gamma}

Operational semantics for lock acquire and release

§ CLIENT-LIBRARY VERIFICATION

Having formalised the semantics of clients and libraries in a weak
memory setting, we now work towards verification of (client) programs
that use such libraries.  We develop an assertion language for
specifying client-library states in sec:assertion-language, a
Hoare logic for reasoning about client-library programs in
sec:hoare-logic-c11 and an example verification of a client
program using a lock library in sec:example-client-lbjec.

§.§ Assertion language

In our proof, we use observability assertions, which describe
conditions for a thread to observe a specific value for a given
variable. Unlike earlier works, our operational semantics covers
clients and their libraries, and hence operates over pairs of

Possible observation, denoted $\langle x = u\rangle_t$, means
that thread $t$ may observe value $u$ for
$x$ [9]. We extend this concept to cope with abstract
method calls as follows. In particular, for an object $o$ and method
$m$, we use $\langle o.m \rangle_t$ to denote that thread $t$ can observe

\begin{align*}
\langle x = n \rangle_t (\sigma)  & \ \  \equiv \ \ \exists w\in
\sigma.\OW(t,x).\ \wrval(w) = n\\
\langle o.m \rangle_t (\sigma) & \ \  \equiv \ \ \exists q.\ (o.m, q) \in
\sigma.\writes \wedge q \geq \sigma.\tview_t(o)
\end{align*}

To distinguish possible observation in clients and libraries, we introduce the following notation,
where $\gamma$ and $\beta$ are the client and library states,
respectively, and $p$ is either a valuation (i.e., $x = n$) or an
abstract method call (i.e., $o.m$):

\begin{align*}
\langle p \rangle_t^C (\gamma, \beta) & \ \ \equiv \ \ \langle p \rangle_t (\gamma)  &
\langle p \rangle_t^L (\gamma, \beta) & \ \ \equiv \ \ \langle p \rangle_t(\beta)
\end{align*}

Definite observation, denoted $[x = u]_t$, means that
thread $t$ can only see the last write to $x$, and that this write has
written value $u$. Recall that each write is a pair containing a write
event and a timestamp. Let $W$ be a set of writes with a unique
timestamp for each $x$, i.e., $(W_{|x})^{-1}$ is a function.  We
define the last write to $x$ in a set of writes $W$ as:

\begin{align*}
\last(W, x) \ \  \equiv \ \  & (W_{|x})^{-1}(\maxTS(W_{|x}))
% \begin{array}[t]{@{}l@{}}
%   w \in \{w \in W \mid \var(w) = x \} \wedge {}
%                                            (\forall w' \in W_{|x}.\ \tst(w') \leq \tst(w))
% \end{array}
\end{align*}

We define the definite observation of a view function, $view$ with
respect to a set of writes as follows:

\begin{align*}
\begin{array}[t]{@{}r@{}l@{}}
\dview (view, W, x) = n
\ \   \equiv\ \  &  view(x) = \last(W, x) \wedge
\wrval(\last(W, x)) = n
\end{array}
\end{align*}

The first conjunct ensures that the viewfront of $view$ for $x$ is the
last write to $x$ in $W$, and the second conjunct ensures that the
value written by the last write to $x$ in $W$ is $n$.  For a variable
$x$, thread $t$ and value $n$, we define:

\begin{align*}
[x = n]_t (\sigma) \ \ & \equiv \ \ \dview(\sigma.\tview_t, \sigma.\writes \cap \W, x) =n
\end{align*}

The extension of definite observation assertions to abstract method
calls is straightforward to define. Namely we have:

\begin{align*}
[o.m]_t (\sigma) \ \ & \equiv \ \
\begin{array}[t]{@{}l@{}}
\sigma.\tview_t(o) =  \maxTS(\sigma.\writes_{|o}) \wedge {}
(o.m, \maxTS(\sigma.\writes_{|o})) \in \sigma.\writes
\end{array}
\end{align*}

As with possible observations, we lift definite observation
predicates to state spaces featuring clients and libraries:

\begin{align*}
[p]^C_t (\gamma, \beta) & \ \ \equiv \ \ [p]_t(\gamma) &
[p]^L_t (\gamma, \beta) & \ \ \equiv \ \ [p]_t(\beta)
\end{align*}

Conditional observation, denoted
$\CObs{x}{u}{t}{y}{v}$, means that if thread $t$ synchronises with a
write to variable $x$ with value $u$, it must subsequently
observe value $v$ for $y$.  For variables $x$ and $y$, thread $t$ and
values $u$ and $v$, we define:

\begin{align*}
\begin{array}[t]{@{}r@{~}l@{}}
& \CObs{x}{u}{t}{y}{v} (\sigma) \\
\ \ \equiv \ \ &
\forall w \in \sigma.\OW(t,x) .\
\wrval(w) = u \imp  \act(w) \in \WR \wedge \dview(\sigma.\mview_w, \sigma.\writes, y) = v
\end{array}
\end{align*}

This is a key
assertion used in message passing proofs
[9, 25] since it guarantees an
observation property on a variable, $y$, via a synchronising read of
another variable, $x$.

As with possible and definite assertions, conditional assertions can be
generalised to objects and extended to pairs of states describing a
client and its library. However, unlike possible and definition
observations assertions, conditional observation enables one to
describe view synchronisation across different states. For example,
consider the following, which enables conditional observation of an
abstract method to establish a definite observation assertion for the
thread view of the client.  We assume a set $Sync \subseteq \Act$ that
identifies a set of synchronising abstract actions.

\begin{align*}
\begin{array}[t]{@{}r@{~}l@{}}
\langle o.m \rangle^L[y = v]_t^C (\gamma, \beta)  \ \ \equiv \ \  &
\forall q.\ (o.m, q) \in \beta.\writes \wedge q \geq \beta.\tview_t(o) \imp \\
&       {} \qquad\qquad o.m \in Sync \wedge \dview(\beta.\mview_{(o.m, q)}, \gamma.\writes, y) = v
\end{array}
\end{align*}

It is possible to define other variations, e.g., conditional observation
synchronisation from clients to libraries, but we leave out the
details of these since they are straightforward to construct.

Covered operations, denoted $\cvd{o.m}{}$, holds iff
all but the last operation $m$ of the object $o$ is covered.

Recall from
the Acquire rule that

a new acquire operation causes the immediately prior (release)
operation $l.release_{n-1}$ to be covered so that no later acquire can
be inserted between $l.release_{n-1}$ and the new acquire.

To reason about this phenomenon over states, we use:

\begin{align*}
\cvd{o.m}{} (\sigma) &\ \  \equiv\ \
\begin{array}[t]{@{}l@{}}
\forall (w, q) \in \sigma.\writes_{|o} \setminus \sigma.\covered.\   w = o.m \wedge q = \maxTS(\sigma.\writes_{|o})
\end{array}
\end{align*}

where $\sigma.\writes_{|o}$ is the set of operations over object

Hidden value, denoted $\cvv{o.m}{}$, states that
the operation $o.m$ exists, but all of these are hidden from

In proofs, such assertions limit the values that
can be returned.

\begin{align*}
% \cvv{x}{u}
% &\ \  =\ \  \lambda \sigma.\
%   \begin{array}[t]{@{}l@{}}
%     (\exists (w, q) \in \sigma.\writes.\ \var(w) = x \wedge \wrval(w) = u) \wedge {}\\
%   (\forall (w, q) \in \sigma.\writes.\ \wrval(w) = u \imp (w, q)
%   \in \sigma.\covered)
% \end{array} \\
\cvv{o.m}{}(\sigma)
&\ \  \equiv\ \
\begin{array}[t]{@{}l@{}}
(\exists q.\ (o.m, q) \in \sigma.\writes) \wedge {}  (\forall q.\ (o.m, q) \in \sigma.\writes  \imp (o.m, q) \in \sigma.\covered)
\end{array}
\end{align*}

Both covered and hidden-value assertions can be lifted to pairs of
states and can be used to reason about standard writes, as opposed to
method calls (details omitted). For instance, we can define
$\cvd{x}{C}(\gamma, \beta) \ \equiv\ \cvd{x}{}(\gamma)$ and
$\cvd{x}{L}(\gamma, \beta) \ \equiv\ \cvd{x}{}(\beta)$.

§.§ Hoare Logic and Owicki-Gries for C11 and Abstract Objects

Since we have an operational semantics, the assertions in sec:assertion-language can be
integrated into standard Hoare-style proof calculus in a
manner [9, 8]. The only
differences are the state model (which is a weak memory state, as
opposed to mappings from variables to values) and the atomic
components (which may include reads of global variables, and, in this
paper, abstract method calls).

Following [9, 8], we let
$\Sigma_C$ and $\Sigma_{L}$ to be the set of all possible global
state configurations of the client and library, respectively and let
$\Sigma_{C11} = (\LVar \to \Val) \times \Sigma_C \times \Sigma_{L}$
be the set of all possible client-library C11 states. Predicates over
$\Sigma_{C11}$ are therefore of

type $\Sigma_{C11} \to \mathbb{B}$.  This leads to the following
definition of a Hoare triple, which we note is the same as the
standard definition — the only difference is that the state
component is of type $\Sigma_{C11}$.

$p, q \in \Sigma_{C11} \to \mathbb{B}$, $P \in {\it Prog}$ and
$\textsf{\textbf{E}} = \lambda t : \Tid.\ \kwskip$.  The semantics
of a Hoare triple under partial correctness is given by: $\begin{array}{r@{~}l}
\{p\} \Init \{q\} & =  q(\Gamma_\Init)
\\[2pt]
\{p\}
\Init ; P \{q\} & =  \exists r.\,\{p\}
\Init \{r\} \wedge \{r\} P \{q\}

\\[2pt]
\{p\}P \{q\} & = \begin{array}[t]{@{}l@{}}
\forall \lstate,\gamma, \beta ,\lstate',\gamma', \beta'.\ \\
\qquad p(\lstate,
\gamma, \beta) \wedge     ((P, \lstate, \gamma, \beta) \ltsArrow{}^* (\textsf{\textbf{E}},
\lstate', \gamma', \beta')) \	\imp \	 q(\lstate',\gamma', \beta')
\end{array}
\\
\end{array}$

This definition (in the context of RC11
[32]) allows all standard Hoare logic
rules for compound statements to be reused [9].  Due to
concurrency, following Owicki and Gries, one must prove local
correctness and interference freedom (or
stability) [34, 9, 8, 31]. This
is also defined in the standard manner.

Namely, a statement $R \in \AComm$ with precondition $pre(R)$ (in the
standard proof outline) does not interfere with an assertion $p$
iff $\{ p \wedge pre(R)\} \ R \ \{ p\}.$ Proof outlines of concurrent
programs are interference free if no statement in one thread
interferes with an assertion in another thread.

The only additional properties that one must define are on the
interaction between atomic commands and predicates over assertions
defined in sec:assertion-language. A collection of rules for
reads, writes and updates have been given in prior
work [8, 9]. Here, we
present rules for method calls of the abstract lock object defined in

In proofs, it is often necessary to reason about particular versions
of the lock (i.e., the lock counter). Therefore, we use ${\tt l.Acquire(\mbox{$v$})}$
and ${\tt l.Release(\mbox{$v$})}$ to denote the transitions that set the lock version to
$v$. Also note that in our example proof, it is clear from context
whether an assertion refers to the client or library state, and hence,
for clarity, we drop the superscripts $C$ and $L$ as used in

The lemma below has been verified in Isabelle/HOL.

Each of the following holds,
where the statements are
decorated with the  identifier of the executing thread, assuming ${\tt m} \in \{{\tt Acquire}, {\tt Release}\}$ and $t \neq t'$

\begin{align}
& \{\cvv{l.\release_u}{}\}\ {\tt
l.Acquire(\mbox{$v$})_t} \ \{ v > u + 1 \} %\tag{\sc AcqVer}
\\
& \{\cvv{l.\release_u}{}\}\ {\tt l.m(\mbox{$v$})_t}\
\{\cvv{l.\release_u}{}\}
%\tag{\sc H-Sta}
\\
& \{[l.\release_u]_t\}
\ {\tt
l.Acquire(\mbox{$v$})_t}\ \{[l.\acquire_{u+1}]_t\}\\
% \tag{\sc Acq-DO} \\
& \{[x = u]_t\}\ {\tt l.m(\mbox{$v$})_{t'}}\
\{[x = u]_t\} \\
%\tag{\sc DO-Other}\\
& \{
\langle l.\release_u \rangle [x = n]_t \}\
{\tt l.Acquire(\mbox{$v$})_t}\ \{v = u + 1 \imp [x = n]_t\} %\tag{\sc CO-Use}
\\
&  \left\{
\begin{array}[c]{@{}l@{}}
\neg \langle l.\release_u \rangle_{t'}
{}\wedge{} {[}x = v]_t
\end{array}
\right\}\ {\tt l.Release(\mbox{$u$})_{t}}\
\{\langle \release_u \rangle [x = v]_{t'}\} %\tag{\sc CO-Intro}
\label{co-intro}
\end{align}

§.§ Example Client-Library Verification

To demonstrate use of our logic in verification, consider the simple
program in fig:lockmp-proof, which comprises a lock object
$l$ and shared client variables $d_1$ and $d_2$ (both initially $0$).
Thread 1 writes 5 to both $d_1$ and $d_2$ after acquiring the lock
while thread 2 reads $d_1$ and $d_2$ (into local registers $r_1$ and
$r_2$) also after acquiring the lock.

Under SC, it is a standard exercise to show that
the program terminates with $r_1 = r_2$ and $r_i = 0$ or $r_i =

We show that the lock specification in
sec:abstr-object-semant together with the assertion language
from sec:assertion-language and Owicki-Gries logic from
sec:hoare-logic-c11 is sufficient to prove this property. In
particular, the specification guarantees adequate synchronisation so
that if the Thread 2's lock acquire sees the lock release in Thread 1,
it also sees the writes to $d_1$ and $d_2$. The proof

relies on two distinct types of properties:

* Mutual exclusion: As in SC, no
two threads should execute their critical sections at the same

* Write visibility: If thread 1 enters its critical section
first, its writes to both $d_1$ and $d_2$ must be visible to thread
2 after thread 2 acquires the lock. Note that this property is not
necessarily guaranteed in a weak memory setting since all reads/writes
to $d_1$ and $d_2$ in fig:lockmp-proof are relaxed.

Init:  $d_1:=0;$ $d_2:=0;$ ${\tt l.init()};$

$\{Inv \wedge [d_1 = 0]_1 \wedge [d_2 = 0]_1 \wedge [d_1 = 0]_2 \wedge [d_2 = 0]_2\}$

$\begin{array}{l@{\quad}||@{\quad }l}
\text{\bf Thread } 1
& \text{\bf Thread } 2\\

\begin{array}[t]{@{}l@{}}
1: \{Inv \wedge \mathbf{P_1}\}\ {\bf if}\ {\tt l.Acquire()} \\
2: \{Inv \wedge \mathbf{P_2}\}\ \quad d_1 := 5 ; \\
3: \{Inv \wedge \mathbf{P_3}\}\  \quad d_2 := 5 ; \\
4: \{Inv \wedge \mathbf{P_4}\}\ \quad {\tt l.Release()}
\end{array}
\begin{array}[t]{@{}l@{}}
1: \{Inv \wedge \mathbf{Q_1}\}\ {\bf if}\ {\tt l.Acquire(\mbox{$rl$})} \\
2: \{Inv \wedge \mathbf{Q_2}\}\ \quad r_1 \gets d_1 ; \\
3: \{Inv \wedge \mathbf{Q_3}\}\ \quad r_2 \gets d_2 ; \\
4: \{Inv \wedge \mathbf{Q_4}\}\ \quad{\tt l.Release()}
\end{array}
\end{array}$

$5: \{(r_1=0 \wedge r_2=0) \vee (r_1=5 \wedge r_2=5)\}$

where assuming $P_{po}  =  (pc_2 = 1 \imp  \neg \langle l.\release_2 \rangle_2)\wedge \cvv{l.\init_0}{}$, we have

\begin{array}[t]{@{}l@{\quad}l@{}}
\begin{array}[t]{@{}r@{}l@{}}
P_1 =  &   [d_1 = 0]_1
\wedge [d_2 = 0]_1
\wedge  \\
& (pc_2 = 1 \imp [l.init_0]_{1} \wedge [l.init_0]_{2})\\
&  \wedge  (pc_2 \in \{2,3,4\} \imp \cvd{l.\acquire_1}{}) \\
P_2 =   & [d_1 = 0]_1 \wedge [d_2 = 0]_1
\wedge P_{po}
\\
P_3 =  & [d_1 = 5]_1 \wedge [d_2 = 0]_1
\wedge P_{po}
\\
P_4  =  & [d_1 = 5]_1 \wedge [d_2 = 5]_1
\wedge
\\
\end{array}
\begin{array}[t]{@{}r@{}l@{}}
& Q_1' = pc_1 = 5 \wedge \langle l.\release_2 \rangle [d_1 = 5]_2 {} \wedge \langle l.\release_2\rangle [d_2 = 5]_2 \\
& Q_1  =  \begin{array}[t]{@{}l@{}}
\left(
\begin{array}[c]{@{}l@{}l@{}}
pc_1 \notin \{2,3,4\} \imp \\
\qquad ([l.init_0]_2 \wedge [d_1 = 0]_2 \wedge  {[}d_2 = 0]_2)   {} \lor  Q_1' {} \\
% & (pc_1 = 5 \wedge \langle l.\release_2 \rangle [d_1 = 5]_2
% {} \wedge \langle l.\release_2\rangle [d_2 = 5]_2)
\end{array}\right)
\\
{} \wedge (pc_1 = 1 \imp [l.init_0]_1)
\wedge (pc_1 = 5 \imp \cvv{l.\init_0}{})
\end{array}
\\
& Q_2  =  (rl = 1 \imp [d_1 = 0]_2 \wedge [d_2 = 0]_2)
\\
& \qquad\ \  {} \wedge (rl = 3 \imp [d_1 = 5]_2 \wedge [d_2 = 5]_2)
\\
& Q_3  =
\begin{array}[t]{@{}l@{}}
(rl = 1 \imp r_1 = 0 \wedge [d_2 = 0]_2)  \\
{} \wedge (rl = 3 \imp r_1 = 5 \wedge [d_2 = 5]_2)
\end{array}
\\
& Q_4  =
\begin{array}[t]{@{}l@{}}
(rl = 1 \imp r_1 = 0 \wedge r_2 = 0) \\
{} \wedge (rl = 3 \imp r_1 = 5 \wedge r_2 = 5)
\end{array}

\end{array}
\end{array}

Proof outline for lock-synchronisation

Our proof is supported by the following global invariant:

\begin{align*}
Inv \ \ \equiv{}\ \  & \neg (pc_1 \in \{2,3,4\} \wedge pc_2 \in \{2,3,4\}) \wedge (rl \in \{1, 3\})
\end{align*}

The first conjunct establishes mutual exclusion, while the second
ensures that the lock version written by the acquire in thread 2 is
either 1 or 3, depending on which thread enters its critical section
The main purpose of the
definite and possible observation assertions is to establish

$Q_1'$ (which appears in $Q_1$) using rule co-intro.

This predicate helps establish $[d_1 = 5]_2$ and
$[d_2 = 5]_2$ in thread 2 whenever thread 2 acquires the lock after
thread 1. The most critical of these assertions is $Q_1$, which states that if
thread 1 is not executing its critical section then we either have

* $[l.init_0]_2 \wedge [d_1 = 0]_2 \wedge [d_2 = 0]_2$, i.e.,
thread 2 can definitely see the lock initialisation and definitely
observe both $d_1$ and $d_2$ to have value $0$, or

* $Q_1'$ holds,

i.e., thread 1 has
released the lock and has established a state whereby if thread 2
acquires the lock, it will be able to establish the definite value
assertions $[d_1 = 5]_2$ and $[d_2 = 5]_2$.

Note that $Q_1$ also includes a conjunct
$pc_1 = 5 \imp \cvv{l.\init_0}{}$, which ensures that if thread 2 enters
its critical section after thread 1 has terminated, then it does so
because it sees $l.\release_2$ (as opposed to $l.\init_0$). This means
that we can establish $rl = 1 \imp [d_1 = 0]_2 \wedge [d_2 = 0]_2$
(i.e., thread 2 has acquired the lock first) and
$rl = 3 \imp [d_1 = 5]_2 \wedge [d_2 = 5]_2$ (i.e., thread 2 has
acquired the lock second) in $Q_2$. Using these definite value
assertions, we can easily establish that the particular values that
are loaded into registers $r_1$ and $r_2$. The lemma has been verified
in Isabelle/HOL.

The proof outline in fig:lockmp-proof is valid.

§ CONTEXTUAL REFINEMENT

We now describe what it
means to implement a specification so that any client
property that was preserved by the specification is not invalidated by the
We define
and prove contextual refinement directly, i.e., without appealing to
external correctness conditions over libraries, cf.
linearizability [23, 11, 21, 14, 20].
We present our refinement theory in sec:refin-simul-weak,
including a proof technique based on forward simulation.
In Sections
<ref> and <ref>, we provide two
examples of contextual refinement of the abstract lock object
introduced in sec:abstr-object-semant.

§.§ Refinement and Simulation for Weak Memory

Since we have an operational semantics with an interleaving semantics
over weak memory states, the development of our refinement theory
closely follows the standard approach under
SC [15].

Suppose $P$ is a program with initialisation $\Init$. An
execution of $P$ is defined by a possibly infinite sequence
$\Pi_0\, \Pi_1\, \Pi_2\,\dots$ such that

* each $\Pi_i$ is a 4-tuple $(P_i, ls_i, \gamma_i, \beta_i)$
comprising a program, local state, global client state and global library state, and

* $(ls_0, \gamma_0, \sigma_0) = (\ls_\Init, \gamma_\Init,
\sigma_\Init)$, and

* for each $i$, we have $\Pi_i \Longrightarrow \Pi_{i+1}$ as
defined in sec:program-semantics.

A client trace corresponding to an execution
$\Pi_0\,\Pi_1\,\Pi_2\dots$ is a sequence $\ct \in \Sigma_C^*$
such that $\ct_i = (\pi_{2}(\Pi_i)_{|C}, \pi_{3}(\Pi_i))$, where
$\pi_n$ is a projection function that extracts the $n$th component of
a given tuple and $ls_{|C}$ restricts the given local state $ls$ to
the variables in $\LVar_C$.  Thus each $\ct_i$ is the global client
state component of $\Pi_i$.

After a projection, the concrete implementation may contain (finite or
infinite) stuttering [15], i.e.,
consecutive states in which the client state is unchanged. We let
${\it rem\_stut}(\ct)$ be the function that removes all stuttering
from the trace $\ct$, i.e., each consecutively repeating state is
replaced by a single instance of that state. We let $\Tr(P)$ denote
the set of stutter-free traces of a program $P$, i.e., the
stutter-free traces generated from the set of all executions of $P$.

Below we refer to the client that uses the abstract object as the
abstract client and the client that uses the object's
implementation as the concrete client. The notion of contextual
refinement that we develop ensures that a client is not able to distinguish
the use of a concrete implementation in place of an abstract
specification. In other words, each thread of the concrete client
should only be able to observe the writes (and updates) in the client
state (i.e., $\gamma$ component) that the thread could already observe
in a corresponding of the client state of the abstract client.
First we define trace refinement for weak memory states.

We say a concrete state $\gamma_C$ is a refinement of an
abstract state $\gamma_A$, denoted
$(ls_A, \gamma_A) \sqsubseteq (ls_C, \gamma_C)$ iff $ls_A = ls_C$,
$\gamma_A.\covered = \gamma_C.\covered$ and for all threads $t$ and
$x \in \GVar$, we have
$\gamma_C.\OW(t, x) \subseteq \gamma_A.\OW(t, x)$.
We say a concrete
trace $\ct$ is a refinement of an abstract trace $\at$,
denoted $\at \refby \ct$, iff $\ct_i \sqsubseteq \at_i$ for all $i$.

This now leads to a natural trace-baseed definition of contextual refinement.

A concrete program $P_C$ is a refinement of an abstract
program $P_A$, denoted $P_A \refby P_C$, iff for any (stutter-free)
trace $\ct \in \Tr(P_C)$ there exists a (stutter-free) trace
$\at \in \Tr(P_A)$ such that $\at \refby \ct$.

Finally, we obtain a notion of contextual refinement for abstract
objects. Suppose $P$ is a program with holes. We let $P[O]$ be the
program in which the holes are filled with the operations from object
$O$. Note that $O$ may be an abstract object, in which case execution
of each method call follows the abstract object semantics
(sec:abstr-object-semant), or a concrete implementation, in
which case execution of each method call follows the semantics of
reads, writes and updates (sec:program-semantics).

We say a concrete object $CO$ is a contextual refinement of
an abstract object $AO$

iff for any client
program $C$, we have $C[AO] \refby C[CO]$.

To verify contextual refinement, we use a notion of simulation,
which once again is a standard technique from the literature. The
difference in a weak memory setting is the fact that the refinement
rules must relate more complex configurations, i.e., tuples of the
form $(P, {\it lst}, \gamma, \alpha)$.

The simulation relation, $R$, relates triples
$(als, \gamma_A, \alpha)$, comprising an abstract local state $als$,
client state $\gamma_A$ and library state $\alpha$, with triples
$(cls, \gamma_C, \beta)$ comprising a concrete local state $cls$, a
client state $\gamma_C$ and concrete library state $\beta$. The
simulation condition must ultimately ensure
$(als_{|C}, \gamma_A) \refby (cls_{|C}, \gamma_C)$ at each step as
defined in def:cont-refin-1. However, since client
synchronisation can affect the library state, a generic forward
simulation rule is non-trivial to define since it requires one to
describe how clients steps affect the simulation relation. We
therefore present a simpler use case for libraries that are used by
clients that do not perform any synchronisation outside the library
itself (e.g., the client in fig:lockmp-proof). If
$\Pi = (P, lst, \gamma, \alpha)$, we let
$\state(\Pi) = (lst, \gamma, \alpha)$ be the state corresponding to

For an abstract object $AO$ and a concrete object $CO$ and
a client $C$ that only synchronises through $AO$ (and $CO$),
$C[AO] \refby C[CO]$ holds if there exists a relation $R$ such that

* $R((als, \gamma_A, \alpha), (cls, \gamma_C, \beta)) \imp $

\begin{array}[c]{l}
als_{|C} = cls_{|C} % \wedge \gamma_A.\covered = \gamma_C.\covered
\wedge {} \\
\forall t, x.\
\begin{array}[t]{@{}l@{}}
\gamma_C.\OW(t, x) \subseteq \gamma_A.\OW(t, x) \wedge
als(t)(rval) = cls(t)(rval)
\end{array}
\end{array}
(client observation)

* $R(\state(\Omega_\Init), \state(\Pi_\Init))$ (initialisation)

* For any concrete configurations $\Pi$, $\Pi'$ and abstract
configuration $\Omega$, if $\Pi \Longrightarrow \Pi'$ via a step
corresponding to $CO$, and $R(\state(\Omega), \state(\Pi))$, then either

* $R(\state(\Omega), \state(\Pi))$, or (stuttering step)

* there exists an abstract configuration $\Omega'$ such that
$\Omega \Longrightarrow \Omega'$ and $R(\state(\Omega'),
\state(\Pi'))$.

(non-stuttering step)

If $R$ is a forward simulation between $AO$ and $CO$,
then for any client that only synchronises through $AO$ (and $CO$)
we have $C[AO] \refby C[CO]$.

§ CONCURRENT DATA STRUCTURES

The modelling approach in sec:abstr-object-semant provides a
flexible framework for specifying abstract objects and enables
specification of synchronised and unsynchronised method calls (as
detailed in fig:publication). We now show that the framework
also provides a mechanism for specifying concurrent objects whose
linearisation order is different from real-time order (cf.
[37, 14, 26, 19]).

Such specifications are a natural fit with the weak memory operational
semantics where new writes may be introduced in the “middle” of
order [12, 16, 27].

§.§ Specifying C11-Style Concurrent Data Structures

As with ordinary read, write and RMW operations, there
are two separate aspects to consider.

* The introduction of operations into modification order. As with
the operational C11
semantics [9, 12], we allow
operations to be introduced into the middle of modification order
(under some restrictions on thread views).

* The release-acquire synchronisation guarantees induced by the
operations. Concurrent data structures are to be implemented as
concurrent libraries, and hence induce inter-thread synchronisation
across both the library and the client.

As with writes, timestamps may be used to define a linear order of the
method calls of the object in question. However, different
threads may have different views of the object being
implemented, and this phenomenon must be supported by the
object specification.
To exemplify our approach,  a queue and a stack specification are.
given below

[Queue specification]

Consider a timeline corresponding to the state of a shared queue
as depicted below:

[thick,->] (-1,0) – (7,0);

(init) at (-1,0);
(enq1) at (1,0);
(enq2) at (3.5,0);
(deq2) at (6,0);

(init) [fill] circle (4pt)
node[below]  $\initq()$;

(enq1) [fill] circle (4pt)
node[below]  $\enq(1)$
node[above]  $t_1$;

[black] (enq2) [fill] circle (4pt)
node[below]  $\enq(2)$;

[black] (deq2) [fill] circle (4pt)
node[below]  $\deq(v)$
node[above]  $t_2$;

where the viewfront of threads $t_1$ and $t_2$
are depicted above the timeline and the abstract operations executed
below the timeline. The state can be generated by executing
the operations in the following temporal order:

* Thread $t_2$ executes $\enq(2)$, and hence $t_2$'s view of the
queue is that of $\enq(2)$.

* Thread $t_1$ executes $\enq(1)$, but since it has not yet
“seen” $\enq(2)$, it may choose a timestamp that is smaller than
the timestamp of $\enq(2)$ for $enq(1)$.

* Thread $t_2$ executes a dequeue, $\deq(v)$, for some yet to be
determined value $v$. Since $t_2$ also executed $\enq(2)$, the
timestamp of the $\deq(v)$ must be larger than that of

One option for the execution to continue in a sensible manner is to
ensure that the effect of the dequeue is communicated to all other
threads so that their views of the object are updated. Thus, if $t_1$
were to perform a new method call, this method call would appear after
$\deq(v)$ (with $v = 1$). However, imposing such a communication
requirement in the abstract specification induces additional (and
potentially unnecessary) synchronisation in an implementation. For
instance, a sensible continuation of the timeline in above would be
for thread $t_1$ to introduce additional enqueue operations between
$\enq(1)$ and $\deq(v)$ (with $v = 1$). In fact, the only
continuations that are disallowed is the introduction of new dequeue
operations between $\enq(1)$ and $\deq(v)$ (with $v = 1$) and new enqueue operations
before $\enq(1)$.

Our formal specification builds on this idea. We assume a predicate,
$\matchedTS$, that stores pairs of timestamps corresponding to
enqueues and dequeues. For any $(ts, ts') \in \matchedTS$, the
timestamp $ts$ corresponds to an enqueue that is removed from the
queue by the dequeue with timestamp $ts'$. To ensure
first-in-first-out behaviours, for any pair
$(ts, ts') \in \matchedTS$, it is illegal for a dequeue to be
introduced between $ts$ and $ts'$. Moreover, when a dequeue matches an
operation, it must match with the first unmatched enqueue that has a
smaller timestamp than the dequeue (or empty if no such enqueue
exists).  Below, we present a specification of enqueue and dequeue

We let
$\supp(R) = \dom(R) \cup \ran(R)$ for a relation $R$.

$\small \inference[{\sc Enq-Base}] {
\tst(\alpha.\tview_t(q)) < \ts' \qquad     \writes' = \alpha.\writes \cup \{(a, \ts')\} \\
(\forall (\mathit{ww}, \mathit{tt}) \in \alpha.\writes.\
\ww \in Enq \wedge \tts > \ts'  \imp \mathit{tt} \notin \dom(\alpha.\matchedTS))
\\
(\forall (\ww, \tts) \in \alpha.\writes.\ \tts > \ts' \imp ww \noteq q.deq_{\it empty}) \qquad
\tview' = \alpha.\tview_t[q := (a, \ts')]
{\alpha\ \Strans{a, \ts'}_{t}\  \alpha[\writes \asgn \writes', \tview_t \asgn \tview'] }

$\small \inference[{\sc Enq-Rlx}] {
a = q.enq_u % \qquad (w, \ts) \in \alpha.\OW(t, x) % \setminus \alpha.\covered
\qquad
\alpha\ \Strans{a, \ts'}_{t}\  \alpha'
{\alpha, \gamma\  \strans{a}_{t}\  \alpha', \gamma }
\qquad  \inference[{\sc Enq-Sync}] {
a =q.enq_u^{\sf R} \qquad
\alpha\  \Strans{a, \ts'}_{t}\  \alpha' \\
\mview' = \alpha'.\tview_t \cup \gamma.\tview_t
{\alpha, \gamma\  \strans{a}_{t}\  \alpha'[\mview_{(a,\ts')} \asgn \mview'], \gamma }
$ $\small  \inference[{\sc Deq-Base}] {
\max(\tst(\alpha.\tview_t(q)), \ts) < \ts' \\ \writes' = \alpha.\writes \cup \{(a, \ts')\}\qquad
(w, \ts) \in \alpha.\writes \qquad \ts \notin \dom(\alpha.\matchedTS)
\\
(\forall (\ww, \tts) \in \alpha.\writes.\ ww \in Enq \wedge \tts < \ts \imp \tts \in \dom(\alpha.\matchedTS)) \\
(\forall \tts' \in \ran(\alpha.\matchedTS).\ ts' > \tts')
\qquad
\tview' = \alpha.\tview_t[q := (a, \ts')]
{\alpha\  \Strans{a, \ts', w, ts}_{t}\
\alpha [\writes \asgn \writes', \tview_t \asgn \tview', \matchedTS := \matchedTS \cup \{(\ts, \ts')\}]}\\

$ \small \inference[{\sc Deq-NE-Rlx}] {
a = q.deq^{\sf [A]}_u \quad u \neq {\it empty} \qquad
\alpha\  \Strans{a, \ts', w, ts}_{t}\
\alpha' \qquad w = q.\enq^{\sf [R]}_u \quad (w, a) \notin {\sf R} \times {\sf A}
{\alpha, \gamma\  \strans{a}_{t}\  \alpha', \gamma}

$ \small \inference[{\sc Deq-NE-Sync}] {
a = q.deq^{\sf A}_u \qquad u \neq {\it empty} \qquad \alpha\  \Strans{a, \ts', w, ts}_{t}\
\alpha' \qquad w = q.enq^{\sf R}_u  \\
\tview' = \alpha'.\tview_t  \otimes \alpha.\mview_{(w,\ts)}
\qquad
\ctview' = \gamma.\tview_t  \otimes \alpha.\mview_{(w,\ts)}
{\alpha, \gamma\  \strans{a}_{t}\  \alpha'[\tview_t \asgn \tview'
], \gamma[\tview_t := \ctview']}\\

$ \small \inference[{\sc Deq-Emp}] {
a = q.deq_{\it empty} \qquad \tst(\alpha.\tview_t(q)) < \ts' \qquad \writes' = \alpha.\writes \cup \{(a, \ts')\}\\
(\forall (\ww, \tts) \in \alpha.\writes.\ \tts < \ts'
\imp  \tts \in \supp(\sigma.\matchedTS) \lor \ww = q.deq_{\it empty})
\\
\tview' = \alpha.\tview_t[q := (a, \ts')] %   \otimes \alpha.\mview_{(w,q)}
{\alpha, \gamma\  \strans{a}_{t}\  \alpha[\writes \asgn \writes',
\tview_t \asgn \tview'], \gamma }

Rules Enq-Base and Deq-Base define the basic rules for
enqueues and dequeues, factoring out the common aspects of relaxed and
synchronising operations. Enq-Base helps determine an
appropriate timestamp for a new (enqueue) operation and advances the
thread view of the executing thread to this timestamp. For a relaxed enqueue,
Enq-Rlx, no other state changes are necessary. However, for an acquiring enqueue, the modification view of the new operation must be updated as defined by Enq-Sync.

Deq-Base is similar to Enq-Base, but it also makes the
enqueue that the dequeue matches with explicit. This is used in rule
Deq-NE-Sync to update thread views of both the library and the
client to be consistent with the corresponding (releasing) enqueue operation.

[Stack specification]

The specification of a stack is designed
to ensure last-in-first-out order. We motivate the main ideas of the
specification below. Consider the following timeline corresponding to the state
of a shared stack:

[thick,->] (-1,0) – (5,0);

(init) at (-1,0);
(enq1) at (1,0);
(enq2) at (3.5,0);
(deq2) at (6,0);

(init) [fill] circle (4pt)
node[below]  $\inits()$
node[above]  $t_3$;

(enq1) [fill] circle (4pt)
node[below]  $\push(2)$
node[above]  $t_2$;

[black] (enq2) [fill] circle (4pt)
node[above] $t_1$
node[below]  $\push(1)$;

In this state,
thread $t_1$'s viewfront is at $\push(1)$, thread $t_2$'s viewfront is
at $\push(2)$ and thread $t_3$'s viewfront is at $\inits()$. Consider
a $\pop$ operation performed by each of the threads — these
operations must be consistent with their viewfronts. For the state
above, a pop executed by $t_3$ may return either empty, $1$ or $2$, a
pop executed by thread $t_2$ may return either $2$ or $1$, and a pop
executed by thread $t_1$ must return $1$.

Suppose $t_3$ performs a $pop$, and that the pop returns the value $2$. In this case, the state would be updated as follows:

[thick,->] (-1,0) – (7,0);

(init) at (-1,0);
(enq1) at (1,0);
(deq2) at (3.5,0);
(enq2) at (6,0);

(init) [fill] circle (4pt)
node[below]  $\inits()$;

(enq1) [fill] circle (4pt)
node[below]  $\push(2)$
node[above]  $t_2$;

[black] (enq2) [fill] circle (4pt)
node[above] $t_1$
node[below]  $\push(1)$;

[black] (deq2) [fill] circle (4pt)
node[below]  $\pop(2)$
node[above]  $t_3$;

Note that $t_3$'s viewfront must include $push(2)$, so $pop(2)$ must
occur after $push(2)$. However, $pop(2)$ must not occur after
$push(1)$; otherwise the popped value would be inconsistent with the
history of a sequential stack since the history
$\push(2)\, \push(1)\, \pop(2)$ is invalid.

Now consider an alternative execution starting from the first state
shown above, where thread $t_1$ performs a pop. The post state following this execution is given below:

[thick,->] (-1,0) – (7,0);

(init) at (-1,0);
(enq1) at (1,0);
(deq2) at (3.5,0);
(enq2) at (6,0);

(init) [fill] circle (4pt)
node[below]  $\inits()$
node[above]  $t_3$;

(enq1) [fill] circle (4pt)
node[below]  $\push(2)$
node[above]  $t_2$;

[black] (deq2) [fill] circle (4pt)
node[below]  $\push(1)$;

[black] (enq2) [fill] circle (4pt)
node[below]  $\pop(1)$
node[above]  $t_1$;

Now suppose $t_2$ performs a $pop$. This pop must return the value $2$
since $\push(1)$ has already been popped and $t_2$'s viewfront
includes $\push(2)$. Moreover, since $\push(1)$ and $\pop(1)$ are
already matched, it would be illegal for the pop by $t_2$ to be
introduced between $\push(1)$ and $\pop(1)$. However, it is acceptable
to introduce the pop before $\push(1)$ or after $\pop(1)$ since this
histories $\push(2)\, \pop(2)\, \push(1)\, \pop(1)$ and
$\push(2)\, \push(1)\, \pop(1)\, \pop(2)$ are both valid.

These ideas are captured by the semantics below. Rules Push-Base and Pop-Base capture the basic ordering
requirements and thread view updates. Rules Push-Rlx and Push-Sync define relaxed and (releasing) pushes, respectively,
while rules Pop-Rlx and Pop-Sync define unsynchronised and
synchronised pops, respectively.

$\small \inference[{\sc Push-Base}] {
\tst(\alpha.\tview_t(q)) < \ts' \qquad     \writes' = \alpha.\writes \cup \{(a, \ts')\} \\
(tt, tt') \in \alpha.\matchedTS.\ \ts' < tt \lor ts' > tt')
\qquad
\tview' = \alpha.\tview_t[q := (a, \ts')]
{\alpha\  \Strans{a, \ts'}_{t}\  \alpha[\writes \asgn \writes', \tview_t \asgn \tview']}
$ $\small \inference[{\sc Push-Rlx}] {
a =  q.push(u) \qquad \alpha\  \Strans{a, \ts'}_{t}\  \alpha'
{\alpha, \gamma\  \strans{a}_{t}\  \alpha', \gamma }
\quad \inference[{\sc Push-Sync}] {
a =  q.push(u)^{\sf R} \qquad \alpha\  \Strans{a, \ts'}_{t}\  \alpha' \\
\mview' = \tview' \cup \gamma.\tview_t
{\alpha, \gamma\  \strans{a}_{t}\  \alpha'[\mview_{(a,\ts')} \asgn \mview'], \gamma }
$$\small \inference[{\sc Pop-Base}] {
\alpha\  \Strans{a, \ts'}_{t}\  \alpha' \qquad
(w, \ts) \in \alpha.\writes \qquad \ts \notin \dom(\alpha.\matchedTS)
\qquad \ts < \ts' \\
(\forall (ww, \ts'') \in \alpha.\writes.\ ww \in Push \wedge \ts < \ts'' < \ts'
\imp \ts'' \in \dom(\alpha.\matchedTS))
{\alpha\  \Strans{a, \ts', w, \ts}_{t}\  \alpha'[\matchedTS := \matchedTS \cup \{(\ts, \ts')\}]}
$\small  \inference[{\sc Pop-NE-Rlx}] {
a = q.pop^{\sf [R]}_u \quad u \neq {\it empty} \quad \alpha\  \Strans{a, \ts', w, \ts}_{t}\  \alpha' \quad w = q.push^{\sf [A]}_u \quad (w, a) \notin {\sf R} \times {\sf A} \\
{\alpha, \gamma\  \strans{a}_{t}\  \alpha', \gamma}

$\small  \inference[{\sc Pop-NE-Sync}] {
a = q.pop(u)^{\sf A} \qquad u \neq {\it empty} \qquad \alpha\  \Strans{a, \ts', w, \ts}_{t}\  \alpha' \qquad w = q.push(u)^{\sf R}
\\
\tview' = \alpha'.\tview_t  \otimes \alpha.\mview_{(w,\ts)}
\qquad
\ctview' = \gamma.\tview_t  \otimes \alpha.\mview_{(w,\ts)}
{\alpha, \gamma\  \strans{a}_{t}\  \alpha'\left[
\begin{array}[c]{@{}l@{}}
\tview_t \asgn \tview'
\end{array}
\right], \gamma[\tview_t := \ctview']}

$\small \inference[{\sc Pop-Emp}] {
a = q.pop^{[{\sf A}]}_{\it empty} \qquad \tst(\alpha.\tview_t(q)) < \ts' \qquad \writes' = \alpha.\writes \cup \{(a, \ts')\}\\
(\forall (\ww, \tts) \in \alpha.\writes.\ \tts < \ts'
\imp  \tts \in \sup(\sigma.\matchedTS) \lor \ww = q.pop^{[{\sf A}]}_{\it empty})
\\
\tview' = \alpha.\tview_t[q := (a, \ts')] %   \otimes \alpha.\mview_{(w,q)}
{\alpha, \gamma\  \strans{a}_{t}\  \alpha[\writes \asgn \writes',
\tview_t \asgn \tview'], \gamma }

We contrast this specification with the prior declarative semantics of
Raad et al. [37], which defines
semantics for complete executions.  Note that Raad et
al. [37] also describe weak stack
specifications; but their notion of weakness relaxes the total order
of operations into a partial order. In our model, the operations are
still totally ordered, but this total order may be different from the
real-time order of operations, thus represents a relaxation of
abstract specifications as used in proofs of
linearizability [23, 6].

With this specification, it becomes possible to make the proof outline
described in fig:mp-proof more precise. In particular, we can
prove the following property, which we have verified using our
Isabelle/HOL mechanisation.

The proof outline in fig:mp-proof is

Note that the variable $d$ in fig:mp-proof is a client
variable, whereas the stack operations are part of an abstract
library. The synchronisation guarantees provided by the stack library
are sufficient to guarantee message passing in the client. Next, in
sec:treiber-stack, we show that such a specification can
indeed be implemented. In particular, we show that the Treiber stack
adapted for C11, as described by Doherty et al [11] satisfies
the stack specification from ex:stack, i.e., the
implementations of the push and pop operations in alg:treiber
provide sufficient synchronisation to provide client-side message

§.§ C11 Treiber Stack

Treiber stack with relaxed and release-acquire memory accesses

[1]
Top := null;

[1]
tml-ctr Push$^{\sf R}$v
n := (node);
n.val := v ;
top $\gets^{\sf A}$ Top ;
n.nxt := top  ;
$\kwcas^{\sf R}$(& Top, top, n)

[1]
Pop$^{\sf A}$

top $\gets ^{\sf A}$ Top ;
top $\neq$ null ;
nTop $\gets$ top.nxt ;
$\kwcas^{\sf R}$(& Top, top, nTop)
top.val ;

The example we consider (see alg:treiber) is the Treiber
Stack [43] (well-studied in a SC setting, but not in a weak
memory one), executing in the RC11 [32] memory model.

Due to weak memory effects, the events under consideration, including
method invocation and response events are partially ordered
[3, 30, 17, 32, 4].

In alg:treiber, all accesses to
Top occur in weak memory. In particular, any read of Top (lines
<ref>, <ref>) reading from a write to Top
(lines ) induces
happens-before order from the write to the read. Any read of
Top via a failed CAS is relaxed (see fig:comm-sem).

For simplicity, like Doherty et al [11] we assume that the
Pop operation blocks by spinning instead of returning
empty. Doherty et al show that the Treiber Stack in
alg:treiber satisfies a property known as causal
linearizability, which in turn guarantees compositionality:
any history containing executions of two causally linearizable objects
will itself be causally linearizable. However, nothing is known about
the client-side guarantees of the algorithm (namely, whether what
client-side synchronisation guarantees are available).

In this section, we address this shortcoming by proving refinement
between the implementation (alg:treiber) and the stack
specification described in ex:stack. In particular, we show
that the Push$^{\sf R}$(v) and Pop$^{\sf A}$ operations
respectively implement the synchronising push and pop operations in

Translated model and proof outline

[1]
Push$^{\sf R}$v
\{I \wedge \forall a \notin \usedAddr.\ [a = 0]_t^L\}$
${\bf choose}\  a\ {\bf where}\ a, a+1 \notin \usedAddr:$
$\nVal_t, \nNxt_t, \usedAddr :=$
$a, a + 1, \usedAddr \cup \{a, a+1\}$;
\{I \wedge [\nVal_t = 0]_t^L \wedge [\nNxt_t = 0]_t^L\}$
$\nVal_t := v$ ;
\{I \wedge [\nVal_t = v]_t^L \wedge [\nNxt_t = 0]_t^L\}$

\{I \wedge [\nVal_t = v]_t^L \wedge \exists v. [\nNxt_t = v]_t^L\}$
$top_t \gets^{\sf A} \Top$ ;
\{I \wedge [\nVal_t = v]_t^L \wedge \exists v. [\nNxt_t = v]_t^L\}$
$\nNxt_t := top_t$  ;
\{I \wedge [\nVal_t = v]_t^L \wedge [\nNxt_t = top_t]_t^L\}$
$\kwcas^{\sf R}(\Top, top_t, \nVal_t)$

[t]0.5 [1]
Pop$^{\sf A}$

\{I \wedge CO_{pop}\}$
$top_t \gets ^{\sf A} Top$ ;
\{I \wedge CO_{pop} \wedge DO_{pop}\}$
$top_t \neq null$ ;
\{I \wedge CO_{pop} \wedge DO_{pop}\}$
$\nTop_t \gets (top_t + 1)$ ;
\{I \wedge CO_{pop} \wedge DO_{pop}\}$
$\kwcas^{\sf R}(\Top, top_t, \nTop_t)$
\{I \wedge \exists v . [top_t = v]_t^L\}$
$rval_t \gets top_t$ ;

where ${\it TopVals}$ is the set of all values for all writes to
$\Top$ in the given weak memory state, and

\begin{align*} \small
I & \small= \refeq{inv-1} \wedge \refeq{inv-2} \wedge \refeq{inv-3} \wedge \refeq{inv-4}
\wedge \refeq{inv-5} \wedge \refeq{inv-6}
\\\small
CO_{pop} & =
\begin{array}[t]{@{}l@{}}
(\exists v. [Top = v]^L_t) \\
\wedge (\forall a \in {\it TopVals}.\  (\exists v . \langle \Top = a\rangle^L[a = v]_t^L) \wedge (\exists v . \langle \Top = a\rangle^L[(a + 1) = v]_t^L))
\end{array}
\\
\small DO_{pop} & = (\exists v .\ [top_t = v]_t^L) \wedge (\exists v .\ [(top_t + 1) = v]_t^L)
\end{align*}

Modelling the Treiber Stack. We track a set
of used addresses, $\usedAddr$. Specifically, each address in $\usedAddr$ is an
address containing the value ($n.\fval$) and next field ($n.\fnxt$) of
the node that a thread is trying to push, or has already been pushed
onto the stack. The variable $\Top$ is a (relaxed) pointer — the
value of each write to $\Top$ is an address from $\usedAddr$ or null. The $\fval$
and $\fnxt$ fields of each node are modelled by (relaxed) writes to
addresses in $\usedAddr$.

For the push, at line 4, two previously unused addresses are selected
and inserted into $\usedAddr$; these addresses is recorded in local
variable $\nVal_t$ and $\nNxt_t$ for thread $t$. We assume that the
new node constructor allocates two consecutive addresses, and hence
assume $\nNxt_t = \nVal_t + 1$. We also assume that both variables are
initialised with value $0$. In our development, $\Top$ will point to
an address holding the value, say $\nVal$, and the next node is
defined as the value of the last write to address $\nVal + 1$.  For
line 5, we introduce a relaxed write to the address corresponding to
$\nVal_t$ with value $v$. Line 7 corresponds to an acquiring read of
$\Top$, line 8 updates the $\fnxt$ field, and line 10 executes a
releasing $\kwcas$ on $\Top$. Similarly, for the pop, at line 13, we
introduce an acquiring read of $\Top$ into local variable $top_t$. At
line 15, we generate a read of the address $top_t + 1$ (which, as
describe above, dereferences the next field), and store the value of
this address in local variable $\nTop_t$. At line 16, we perform a
releasing $\kwcas$ on $\Top$.

Treiber Stack invariants. We use an
auxiliary variable $\pushedAddr$ to keep track of the addresses that
have been pushed on to the stack. We set $\pushedAddr$ to
$\pushedAddr \cup \{\nVal_t\}$ at line 9 and to
$\pushedAddr \setminus \{top_t\}$ at line 16 whenever the
corresponding $\kwcas$ operations succeed.  Given a library state
$\beta$, the addresses that have been pushed onto the stack (in order)
are thus given by $\nxtRel_\beta$ (defined below), recalling that we
use address $a+1$ to store writes to the next field. Thus:

\begin{align*}
\lastVal_\beta(x) & = \wrval(\last(\beta.\writes, x))
\\
\nxtRel_{\mem, \beta} & = \{(a,b) \mid  a \in \mem.\pushedAddr \wedge
b = \lastVal_\beta(a + 1) \}^+
\end{align*}

Thus, $\nxtRel_{\mem, \beta}$ is the transitive closure of the set
that maps each pushed address (as recorded in $\mem$) to the
address of the next node. The first component of our global invariant
ensures that $nxtRel_\beta$ is a total order with $\Top$ as the
minimal element ($\inf$) and $null$ as the maximal element ($\sup$).

\begin{align}
\label{inv-1}
& totalOrder(nxtRel_\beta) \wedge \inf(nxtRel_\beta) = {\it lastVal}_\beta(Top) \wedge \sup(nxtRel_\beta) = null
\end{align}

The next two components of the invariant state properties about
$\Top$, and links these values to the auxiliary state components
$\usedAddr$ and $pushedAddr$.

\begin{align}
\label{inv-2}
& \forall  w \in \beta.\writes_{| \Top}.\ w \in \W_{\sf R} \wedge (\wrval(w)  \neq  null  \imp   \wrval(w)  \in  \mem.\usedAddr)
\\
\label{inv-3}
& {\it lastVal}_\beta(Top)  \neq  null  \imp   {\it lastVal}_\beta(Top)  \in  \mem.\pushedAddr
\end{align}

Invariant inv-2 states writes to $\Top$ are releasing and
non-null writes are recorded in $\mem.\usedAddr$, while inv-3
states that whenever the last value of $\Top$ is non-null, this value
is a currently pushed address.[Invariant inv-3 could
be strengthened so that we have
${\it lastVal}_\beta(a) \in \mem.\pushedAddr$ for all
$a \in \dom(\nxtRel_{\mem, \beta})$, but is not needed for our
verification. ]
Finally, we have a set of simple invariants over $\usedAddr$ and

\begin{align}
\label{inv-4}
& \mem.\pushedAddr  \subseteq \mem.\usedAddr
\\
\label{inv-5}
& \forall a_1, a_2 \in \mem.\pushedAddr.\  a_1 \neq a_2  \imp  \lastVal_\beta(a_1 + 1)  \neq  \lastVal_\beta(a_2 + 1)
\\
\label{inv-6}
& \forall  a \in \mem.\pushedAddr.\  \lastVal_\beta(a + 1)  \neq  null  \imp  \lastVal_\beta(a + 1) \in \mem.\pushedAddr
\end{align}

Invariant inv-4 states that all pushed addresses are used
addresses, inv-5 states that the next pointers of different
pushed addresses are different and inv-6 states that if the
value of the next pointer of a pushed address is non-null, then the
node corresponding to the next pointer is a pushed address.

Simulation relation. We now describe the
simulation relation used to prove refinement between the Treiber Stack
and the stack specification in ex:stack.  A key component of
the relation is an injective function, $f$, mapping nodes
corresponding to pushed addresses to unmatched push operations of the
abstract specification. Recall from ex:stack that pushes are
matched if they have been subsequently popped. The refinement relation
$R_{\it TS}((als, \gamma_A, \alpha), (ls, \gamma_C, \beta)) = \exists f.\
\refeq{ref-2} \wedge \refeq{ref-3a} \wedge \refeq{ref-3} \wedge
\refeq{ref-3b} \wedge \refeq{ref-5} \wedge \refeq{ref-6} \wedge
\refeq{ref-7}$.

The first component ensures injectivity of $f$

and that
the corresponding operation is a pop that
returns empty.

\begin{align}
% \label{ref-1}
% & (\forall a_1, a_2 \in \mem.\pushedAddr.\ f(a_1) = f(a_2) \imp  a_1 = a_2)  \\
\label{ref-2}
& \injective(f) % \wedge \unmatchedPush_\alpha = \{f(a) \mid a \in \mem.\pushedAddr\}
\wedge \exists ts.\ f(null) = (pop(empty), ts)
\end{align}

We assume $\unmatchedPush_\alpha$ denotes the set of unmatched push
operations in the abstract state $\alpha$. The next two conditions
describe the relationship between pushed addresses in the concrete
state to the unmatched pushes:

\begin{align}
\label{ref-3a}
\begin{array}[c]{@{}l@{}l@{}}
\forall  a \in \mem.\pushedAddr .\ \ & f(a) \in  \unmatchedPush_\alpha   \wedge val_\alpha (f(a)) = {\it lastVal}_\beta(a)  \\
& {} \wedge \tst(f(a)) > \tst(f (\lastVal_\beta(a+1)))
\end{array}
\\
\label{ref-3}
& \begin{array}[c]{@{}l@{}}
% \qquad {} f(a) \in  \unmatchedPush_\alpha   \wedge \tst(f(a)) > \tst(f (\mem.nxt(a))
%  \\
\forall  a \in \mem.\pushedAddr,  op \in \unmatchedPush_\alpha.\ \\
\qquad op \neq f(a) \wedge op \neq f (\lastVal_\beta(a+1)) \imp   \\
\qquad  \tst(op) < \tst(f (\lastVal_\beta(a+1)) \lor \tst(op) > \tst(f(a))
\end{array}
\end{align}

Condition ref-3a states that for each pushed address, $f(a)$
is indeed an unmatched push with the same values. Moreover, the
timestamp of the push corresponding $f(a)$ is larger than the
timestamp of the push corresponding to the next node of $a$. Condition

ensures that the timestamp of $op$ is not in between that of $f(a)$
and the immediately next node of $f(a)$.

Suppose $\lastPush_\alpha$ returns the push in $\alpha$ with the
largest timestamp. The next condition ensures that when the stack is
non-empty, the node corresponding to the last write to $\Top$ is the
push with the largest timestamp, i.e.,

\begin{align}
\label{ref-3b}
\begin{array}[c]{@{}l@{}l@{}}
{\it lastVal}_\beta(Top) \neq null \imp{} & \lastPush_\beta \in \unmatchedPush_\alpha  \wedge f ({\it lastVal}_\beta(Top)) = \lastPush_\alpha
\end{array}
\end{align}

Finally, we have a set of conditions describing the views of threads
over client variables. Together these assertions ensures the client
observation property in def:fsim.

\begin{align}
\label{ref-5}
& \forall a\in \mem.\pushedAddr, x \in \GVar_C .\   \tst (\beta.\mview_{f(a)}(x))
\le \tst (\gamma_C.\tview_t(x))
\\
\label{ref-6}
\begin{array}[c]{@{}l@{}}
\forall a\in \mem.\pushedAddr, w \in \beta.\writes.\  var(w) = Top \wedge val(w) = a  \imp  \\
\qquad
\forall x \in \GVar_C.\ \tst (\alpha.\mview_{f(a)}(x)) \le \tst(\beta.\mview_w(x))
\end{array}
\\
\label{ref-7}
& \forall x \in \GVar_C .\ \tst (\gamma_A.\tview_t(x)) \le \tst(\gamma_C.\tview_t(x))
\end{align}

We then obtain the following proposition.

For synchronisation-free clients, $R_{\it TS}$ is a forward simulation
between the abstract stack object and the Treiber stack.

The simulation proof is similar to linearizability proofs in the
classical (sequentially consistent) setting [6]. All
steps except for a successful $\kwcas$ at lines 9 and 16 are
stuttering steps and are not matched with any abstract step. The
successful $\kwcas$ operations corresponds to the a releasing push or
an acquiring pop as allowed by the specification in ex:stack.

§.§ Mechanisation

Our deductive proof of the Treiber stack for the RC11-RAR within
Isabelle/HOL has been a significant undertaking. Many properties that
one would take for granted in a sequentially consistent setting are no
longer valid under weak memory. For instance, to guarantee that the
writes to the fields at lines 5 and 8 are seen by the reads in lines
15 and 17, respectively, one must ensure a happens-before relationship
through the releasing $\kwcas$ at line 9 and the acquiring read at
line 13. Moreover, client-side synchronisation guarantees defined by
the specification must also shown to be satisfied.
This verification has been made possible by the proof infrastructure
developed in earlier work [9], which considered much
simpler examples. Here, we have shown that the proof principles carry
over to pointer-based programs. Additionally, the specifications that
we have developed in sec:specifying-c11-style (and
sec:abstr-object-semant) are appropriate for guaranteeing
client synchronisation through a library object, and our refinement
theory can be used to show that these client-library synchronisation
requirements are also guaranteed by the Treiber stack.

The full development and verification of the Treiber stack is around 12 KLOC
in Isabelle accross 9 different theories. The proof is heavily dependent on
the general proof rules developed for the generalised C11 operational semantics.
A considerable effort was put to identify and prove the local and global
invariants of the stack's push and pop operations. Each of these invariants
was then proved correct locally and globally (interference freedom) in
the usual Owicki-Gries manner.

§.§ Discussion

The message passing idiom has manifested in our case study in two
different ways. In fig:mp-proof and the corresponding proof
of prop:stack-mp involves message passing through the stack
specification. In the Treiber stack implementation, threads use
message-passing to ensure that the relaxed writes to the “val” and
“nxt” fields of a node within a push are viewed by the pop via
release-acquire synchronisation on the $\Top$ pointer. In both cases,
message passing is succinctly characterised by conditional
observation assertion, suggesting that it is a key operator for
reasoning about such behaviours.
Conditional observation assertions capture the idea behind message
passing via “ownership transfer” as used in many separation
logics [42, 18, 25, 39, 38],
a “communication specification” [2] and
“protocols” [44], which have been used
to ensure happens-before knowledge is passed from one thread to
another. These techniques are however focussed on message passing via
reads and writes within a single object and cannot handle
message passing on client threads using library

An interesting observation that has been elucidated by our refinement
proof is the fact that the Treiber stack does not need to linearize
its operation in the middle of the abstract operation order as defined
by their timestamps. I.e., each new push / pop operation thereby is
not required to take advantage of the relaxation provided by the
specification in ex:stack. This is however not surprising —
the concrete implementation synchronises all pushes and pops through a
single $\Top$ pointer that is only modified using an RMW
generated by a $\kwcas$.  We conjecture this relaxation would be
required by, for example, a weak memory implementation of the
elimination stack [22], which augments a
standard stack with a disjoint elimination mechanism. Operations that
synchronise using the elimination mechanism do not interact with the
main stack data structure, and hence are not guaranteed to advance
thread views. We therefore conjecture that a C11-style relaxed-memory
version of the elimination stack would be an implementation of our
specification, where the stack can be weakly synchronised, allowing it
to take advantage of our relaxed specification.

§ RELATED WORK

The speed of development in the area has meant that it has become
almost impossible to cover all related works. Below, we provide a
brief overview of different approaches. There are now several
different approaches to program verification that support different
aspects of weak memory using pen-and-paper proofs
(e.g., [31, 44, 2, 18]),
model checking
(e.g., [28, 1]),
specialised tools
(e.g., [42, 26, 40, 38]),
and generalist theorem provers (e.g., [9]). These cover a
variety of (fragments of) memory models and proceed via exhaustive
checking, separation logics, or Hoare-style calculi.

Library abstractions in weak memory have been considered in earlier
works (e.g., [4]), but these were not accompanied
by an associated program logic or verification technique. The use of
abstract methods can be used to ensure weak-memory synchronisation
guarantees has been established in earlier
work [11, 14], where it has been shown to be necessary
for contextual refinement [14] and
compositionality [11].

Krishna et al. [26] have developed an
approach to verifying implementations of weakly consistent
libraries [19]. Their techniques are
mechanised using the CIVL verification tool and account for weak
memory relaxations by transitioning over a generic happens-before
relation encoded within a transition system. On the one hand, this
means that their techniques apply to any memory model, but on the
other hand, such a happens-before relation must ultimately be
supplied. Their methods currently cover refinement of libraries, but
do not cover clients that use library specifications. Nevertheless
given that CIVL is aimed at automation, it would be interesting to see
whether the assertion language from earlier works [9] (also
see sec:example-verification) can have a role in further
improving these verification methods.

More recent works include that on robustness of C11-style
programs, which aims to show “adequate synchronisation” so that the
weak memory executions reduce to executions under stronger memory
models [33]. Such reductions, although automatic,
are limited to finite state systems, and a small number of
threads. Furthermore, it is currently unclear how they would handle
client-library synchronisation or relaxed non sequentially consistent
specifications. Verification tools for deductive verification of C11-style programs
have been based on separation
logic [38, 39, 25]
and Owicki-Gries
reasoning [8, 9]. Those
based on separation logic offer a degree of automation but, as far as
the authors are aware, have not been applied to verification of data
structures. None of these works cover refinement.

Orthogonal to our paper is a series of works that address more relaxed
memory semantics that allow causality
cycles [35, 27, 29, 24],
e.g., the load-buffering litmus test, which our semantics
(like [32]) disallows. Although an
important problem, we eschew proofs of correctness in this weaker
memory model since the precise weak memory semantics that
appropriately handles load-buffering, yet rules out thin-air reads is
still a topic of ongoing research. Moreover, we note that many
concurrent object implementations naturally induce intra-thread
dependencies, whereby the relaxed model and the strict model we use
coincide without requiring introduction of any additional
synchronisation. Thus, although weak memory models with causality
cycles are a real phenomenon, there is more work to be done before
they relaxations they offer can be exploited. We consider the problem
of deductive verification under such memory models to be an important
problem for future work.

§ CONCLUSIONS

In this paper, we have presented a new approach to specifying and
verifying abstract objects over weak memory by extending an existing
operational semantics for RC11 RAR (a fragment of the C11 memory
model). This operational semantics allows one to execute programs in
thread order and accommodates weak memory behaviours via a special
encoding of the state. Moreover, unlike prior works [9], it
describes how (release-acquire) synchronisation within a library
affects a client state, and vice versa, supporting modular program

Operational semantics are widely acknowledged as being a prerequisite
to developing program logics, complementing declarative approaches
(e.g., [3, 37]), since a
meaning for stepwise program execution is needed to establish meaning
for pre/postconditions. We have demonstrated this by developing an
Owicki-Gries logic for client-library programs, extending prior
work [31, 9], which did not facilitate
proof modularisation of this nature.

We have also developed a novel operational technique for specifying weak memory concurrent objects, and shown that the
specification allows proofs of client-library synchronisation across
abstract library method calls.
This has been accompanied by a
refinement theory, that extends standard notions of refinement under
sequential consistency [15].  To exploit
these operational descriptions, we have developed an assertion
language that describes a thread's observations of client-library
states, which is in turn used to verify program invariants and proofs
of refinement.
We have shown that our methodology supports two types of
verification: (1) proofs of correctness of client programs that
use abstract libraries and (2) refinement proofs between
abstract libraries and their implementations.

We present the verification of two lock implementations as well as the
Treiber stack adapted for C11.

This amounts to one of the more sophisticated proofs performed using a
deductive verification approach.

[1]
P. A. Abdulla, J. Arora, M. F. Atig, and S. N. Krishna.
Verification of programs under the release-acquire semantics.
In K. S. McKinley and K. Fisher, editors, PLDI, pages
1117–1132. ACM, 2019.

[2]
J. Alglave and P. Cousot.
Ogre and Pythia: an invariance proof method for weak consistency
In G. Castagna and A. D. Gordon, editors, POPL, pages 3–18.
ACM, 2017.

[3]
J. Alglave, L. Maranget, and M. Tautschnig.
Herding cats: Modelling, simulation, testing, and data mining for
weak memory.
ACM Trans. Program. Lang. Syst., 36(2):7:1–7:74, 2014.

[4]
M. Batty, M. Dodds, and A. Gotsman.
Library abstraction for C/C++ concurrency.
In R. Giacobazzi and R. Cousot, editors, POPL, pages 235–248.
ACM, 2013.

[5]
M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber.
Mathematizing C++ concurrency.
In T. Ball and M. Sagiv, editors, POPL, pages 55–66. ACM,

[6]
B. Dongol and J. Derrick.
Verifying linearisability: A comparative survey.
ACM Comput. Surv., 48(2):19:1–19:43, 2015.

[7]
Sadegh Dalvandi and Brijesh Dongol.
Isabelle files for “Operationally Verifying C11-style Weak Memory
Libraries”, 2021.

[8]
S. Dalvandi, B. Dongol, and S. Doherty.
Integrating Owicki-Gries for C11-style memory models into
CoRR, abs/2004.02983, 2020.

[9]
S. Dalvandi, S. Doherty, B. Dongol, and H. Wehrheim.
Owicki-gries reasoning for C11 RAR.
In R. Hirschfeld and T. Pape, editors, ECOOP, volume 166 of
LIPIcs, pages 11:1–11:26. Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2020.

[10]
Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim.
Owicki-gries reasoning for C11 RAR (artifact).
Dagstuhl Artifacts Ser., 6(2):15:1–15:2, 2020.

[11]
S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick.
Making linearizability compositional for partially ordered
In C. A. Furia and K. Winter, editors, iFM, volume 11023 of
LNCS, pages 110–129. Springer, 2018.

[12]
S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick.
Verifying C11 programs operationally.
In Jeffrey K. Hollingsworth and Idit Keidar, editors, PPoPP,
pages 355–365. ACM, 2019.

[13]
B. Dongol and L. Groves.
Contextual trace refinement for concurrent objects: Safety and
In ICFEM, volume 10009 of LNCS, pages 261–278, 2016.

[14]
B. Dongol, R. Jagadeesan, J. Riely, and A. Armstrong.
On abstraction and compositionality for weak-memory linearisability.
In VMCAI, volume 10747 of LNCS, pages 183–204.
Springer, 2018.

[15]
W. P. de Roever and K. Engelhardt.
Data Refinement: Model-oriented Proof Theories and their
Comparison, volume 46 of Cambridge Tracts in Theoretical Computer
Cambridge University Press, 1998.

[16]
S. Dolan, KC Sivaramakrishnan, and A. Madhavapeddy.
Bounding data races in space and time.
In PLDI, PLDI 2018, pages 242–255, New York, NY, USA, 2018.

[17]
M. Doko and V. Vafeiadis.
A program logic for C11 memory fences.
In VMCAI, volume 9583 of LNCS, pages 413–430.
Springer, 2016.

[18]
M. Doko and V. Vafeiadis.
Tackling real-life relaxed concurrency with FSL++.
In ESOP, pages 448–475, 2017.

[19]
M. Emmi and C. Enea.
Weak-consistency specification via visibility relaxation.
Proc. ACM Program. Lang., 3(POPL):60:1–60:28, 2019.

[20]
I. Filipovic, P. W. O'Hearn, N. Rinetzky, and H. Yang.
Abstraction for concurrent objects.
Theor. Comput. Sci., 411(51-52):4379–4398, 2010.

[21]
A. Gotsman and H. Yang.
Liveness-preserving atomicity abstraction.
In ICALP (2), volume 6756 of LNCS, pages 453–465.
Springer, 2011.

[22]
D. Hendler, N. Shavit, and L. Yerushalmi.
A scalable lock-free stack algorithm.
In P. B. Gibbons and M. Adler, editors, SPAA, pages 206–215.
ACM, 2004.

[23]
M. Herlihy and J. M. Wing.
Linearizability: A correctness condition for concurrent objects.
ACM TOPLAS, 12(3):463–492, 1990.

[24]
R. Jagadeesan, A. Jeffrey, and J. Riely.
Pomsets with preconditions: a simple model of relaxed memory.
Proc. ACM Program. Lang., 4(OOPSLA):194:1–194:30, 2020.

[25]
J.-O. Kaiser, H.-H. Dang, D. D., O. Lahav, and V. Vafeiadis.
Strong logic for weak memory: Reasoning about release-acquire
consistency in Iris.
In Peter Müller, editor, ECOOP, volume 74 of LIPIcs, pages 17:1–17:29. Schloss Dagstuhl - Leibniz-Zentrum fuer
Informatik, 2017.

[26]
S. Krishna, M. Emmi, C. Enea, and D. Jovanovic.
Verifying visibility-based weak consistency.
In P. Müller, editor, ESOP, volume 12075 of Lecture
Notes in Computer Science, pages 280–307. Springer, 2020.

[27]
J. Kang, C.-K. Hur, O. Lahav, V. Vafeiadis, and D. Dreyer.
A promising semantics for relaxed-memory concurrency.
In POPL, pages 175–189. ACM, 2017.

[28]
M. Kokologiannakis, A. Raad, and V. Vafeiadis.
Model checking for weakly consistent libraries.
In K. S. McKinley and K. Fisher, editors, PLDI, pages 96–110.
ACM, 2019.

[29]
S.-H. Lee, M. Cho, A. Podkopaev, S. Chakraborty, C.-K. Hur, O. Lahav, and
V. Vafeiadis.
Promising 2.0: global optimizations in relaxed memory concurrency.
In A. F. Donaldson and E. Torlak, editors, PLDI, pages
362–376. ACM, 2020.

[30]
O. Lahav, N. Giannarakis, and V. Vafeiadis.
Taming release-acquire consistency.
In R. Bodík and R. Majumdar, editors, POPL, pages
649–662. ACM, 2016.

[31]
O. Lahav and V. Vafeiadis.
Owicki-Gries reasoning for weak memory models.
In M. M. Halldórsson, K. Iwama, N. Kobayashi, and B. Speckmann,
editors, ICALP, volume 9135 of LNCS, pages 311–323. Springer,

[32]
O. Lahav, V. Vafeiadis, J. Kang, C.-K. Hur, and D. Dreyer.
Repairing sequential consistency in C/C++11.
In PLDI, pages 618–632. ACM, 2017.

[33]
R. Margalit and O. Lahav.
Verifying observational robustness against a c11-style memory model.
Proc. ACM Program. Lang., 5(POPL), January 2021.

[34]
S. S. Owicki and D. Gries.
An axiomatic proof technique for parallel programs I.
Acta Inf., 6:319–340, 1976.

[35]
M. Paviotti, S. Cooksey, A. Paradis, D. Wright, S. Owens, and M. Batty.
Modular relaxed dependencies in weak memory concurrency.
In P. Müller, editor, ESOP, volume 12075 of Lecture
Notes in Computer Science, pages 599–625. Springer, 2020.

[36]
A. Podkopaev, I. Sergey, and A. Nanevski.
Operational aspects of C/C++ concurrency.
CoRR, abs/1606.01400, 2016.

[37]
A. Raad, M. Doko, L. Rozic, O. Lahav, and V. Vafeiadis.
On library correctness under weak memory consistency: specifying and
verifying concurrent libraries under declarative consistency models.
Proc. ACM Program. Lang., 3(POPL):68:1–68:31, 2019.

[38]
A. J. Summers and P. Müller.
Automating deductive verification for weak-memory programs.
In D. Beyer and M. Huisman, editors, TACAS, volume 10805 of
LNCS, pages 190–209. Springer, 2018.

[39]
A. J. Summers and P. Müller.
Automating deductive verification for weak-memory programs (extended
Int. J. Softw. Tools Technol. Transf., 22(6):709–728, 2020.

[40]
K. Svendsen, J. Pichon-Pharabod, M. Doko, O. Lahav, and V. Vafeiadis.
A separation logic for a promising semantics.
In A. Ahmed, editor, ESOP, volume 10801 of LNCS, pages
357–384. Springer, 2018.

[41]
P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen.
x86-tso: a rigorous and usable programmer's model for x86
Commun. ACM, 53(7):89–97, 2010.

[42]
J. Tassarotti, D. Dreyer, and V. Vafeiadis.
Verifying read-copy-update in a logic for weak memory.
In D. Grove and S. Blackburn, editors, PLDI, pages 110–120.
ACM, 2015.

[43]
R. K. Treiber.
Systems programming: Coping with parallelism.
Technical Report RJ 5118, IBM Almaden Res. Ctr., 1986.

[44]
A. Turon, V. Vafeiadis, and D. Dreyer.
GPS: navigating weak memory with ghosts, protocols, and separation.
In A. P. Black and T. D. Millstein, editors, OOPSLA, pages
691–707. ACM, 2014.

Here we give an additional data structure specification.

[Queue specification]

Consider a timeline corresponding to the state of a shared queue
as depicted below:

[thick,->] (-1,0) – (7,0);

(init) at (-1,0);
(enq1) at (1,0);
(enq2) at (3.5,0);
(deq2) at (6,0);

(init) [fill] circle (4pt)
node[below]  $\initq()$;

(enq1) [fill] circle (4pt)
node[below]  $\enq(1)$
node[above]  $t_1$;

[black] (enq2) [fill] circle (4pt)
node[below]  $\enq(2)$;

[black] (deq2) [fill] circle (4pt)
node[below]  $\deq(v)$
node[above]  $t_2$;

where the viewfront of threads $t_1$ and $t_2$
are depicted above the timeline and the abstract operations executed
below the timeline. The state can be generated by executing
the operations in the following temporal order:

* Thread $t_2$ executes $\enq(2)$, and hence $t_2$'s view of the
queue is that of $\enq(2)$.

* Thread $t_1$ executes $\enq(1)$, but since it has not yet
“seen” $\enq(2)$, it may choose a timestamp that is smaller than
the timestamp of $\enq(2)$ for $enq(1)$.

* Thread $t_2$ executes a dequeue, $\deq(v)$, for some yet to be
determined value $v$. Since $t_2$ also executed $\enq(2)$, the
timestamp of the $\deq(v)$ must be larger than that of

One option for the execution to continue in a sensible manner is to
ensure that the effect of the dequeue is communicated to all other
threads so that their views of the object are updated. Thus, if $t_1$
were to perform a new method call, this method call would appear after
$\deq(v)$ (with $v = 1$). However, imposing such a communication
requirement in the abstract specification induces additional (and
potentially unnecessary) synchronisation in an implementation. For
instance, a sensible continuation of the timeline in above would be
for thread $t_1$ to introduce additional enqueue operations between
$\enq(1)$ and $\deq(v)$ (with $v = 1$). In fact, the only
continuations that are disallowed is the introduction of new dequeue
operations between $\enq(1)$ and $\deq(v)$ (with $v = 1$) and new enqueue operations
before $\enq(1)$.

Our formal specification builds on this idea. We assume a predicate,
$\matchedTS$, that stores pairs of timestamps corresponding to
enqueues and dequeues. For any $(ts, ts') \in \matchedTS$, the
timestamp $ts$ corresponds to an enqueue that is removed from the
queue by the dequeue with timestamp $ts'$. To ensure
first-in-first-out behaviours, for any pair
$(ts, ts') \in \matchedTS$, it is illegal for a dequeue to be
introduced between $ts$ and $ts'$. Moreover, when a dequeue matches an
operation, it must match with the first unmatched enqueue that has a
smaller timestamp than the dequeue (or empty if no such enqueue
exists).  Below, we present a specification of enqueue and dequeue

We let
$\supp(R) = \dom(R) \cup \ran(R)$ for a relation $R$.

$\small \inference[{\sc Enq-Base}] {
\tst(\alpha.\tview_t(q)) < \ts' \qquad     \writes' = \alpha.\writes \cup \{(a, \ts')\} \\
(\forall (\mathit{ww}, \mathit{tt}) \in \alpha.\writes.\
\ww \in Enq \wedge \tts > \ts'  \imp \mathit{tt} \notin \dom(\alpha.\matchedTS))
\\
(\forall (\ww, \tts) \in \alpha.\writes.\ \tts > \ts' \imp ww \noteq q.deq_{\it empty}) \qquad
\tview' = \alpha.\tview_t[q := (a, \ts')]
{\alpha\ \Strans{a, \ts'}_{t}\  \alpha[\writes \asgn \writes', \tview_t \asgn \tview'] }

$\small \inference[{\sc Enq-Rlx}] {
a = q.enq_u % \qquad (w, \ts) \in \alpha.\OW(t, x) % \setminus \alpha.\covered
\qquad
\alpha\ \Strans{a, \ts'}_{t}\  \alpha'
{\alpha, \gamma\  \strans{a}_{t}\  \alpha', \gamma }
\qquad  \inference[{\sc Enq-Sync}] {
a =q.enq_u^{\sf R} \qquad
\alpha\  \Strans{a, \ts'}_{t}\  \alpha' \\
\mview' = \alpha'.\tview_t \cup \gamma.\tview_t
{\alpha, \gamma\  \strans{a}_{t}\  \alpha'[\mview_{(a,\ts')} \asgn \mview'], \gamma }
$ $\small  \inference[{\sc Deq-Base}] {
\max(\tst(\alpha.\tview_t(q)), \ts) < \ts' \\ \writes' = \alpha.\writes \cup \{(a, \ts')\}\qquad
(w, \ts) \in \alpha.\writes \qquad \ts \notin \dom(\alpha.\matchedTS)
\\
(\forall (\ww, \tts) \in \alpha.\writes.\ ww \in Enq \wedge \tts < \ts \imp \tts \in \dom(\alpha.\matchedTS)) \\
(\forall \tts' \in \ran(\alpha.\matchedTS).\ ts' > \tts')
\qquad
\tview' = \alpha.\tview_t[q := (a, \ts')]
{\alpha\  \Strans{a, \ts', w, ts}_{t}\
\alpha [\writes \asgn \writes', \tview_t \asgn \tview', \matchedTS := \matchedTS \cup \{(\ts, \ts')\}]}\\

$ \small \inference[{\sc Deq-NE-Rlx}] {
a = q.deq^{\sf [A]}_u \quad u \neq {\it empty} \qquad
\alpha\  \Strans{a, \ts', w, ts}_{t}\
\alpha' \qquad w = q.\enq^{\sf [R]}_u \quad (w, a) \notin {\sf R} \times {\sf A}
{\alpha, \gamma\  \strans{a}_{t}\  \alpha', \gamma}

$ \small \inference[{\sc Deq-NE-Sync}] {
a = q.deq^{\sf A}_u \qquad u \neq {\it empty} \qquad \alpha\  \Strans{a, \ts', w, ts}_{t}\
\alpha' \qquad w = q.enq^{\sf R}_u  \\
\tview' = \alpha'.\tview_t  \otimes \alpha.\mview_{(w,\ts)}
\qquad
\ctview' = \gamma.\tview_t  \otimes \alpha.\mview_{(w,\ts)}
{\alpha, \gamma\  \strans{a}_{t}\  \alpha'[\tview_t \asgn \tview'
], \gamma[\tview_t := \ctview']}\\

$ \small \inference[{\sc Deq-Emp}] {
a = q.deq_{\it empty} \qquad \tst(\alpha.\tview_t(q)) < \ts' \qquad \writes' = \alpha.\writes \cup \{(a, \ts')\}\\
(\forall (\ww, \tts) \in \alpha.\writes.\ \tts < \ts'
\imp  \tts \in \supp(\sigma.\matchedTS) \lor \ww = q.deq_{\it empty})
\\
\tview' = \alpha.\tview_t[q := (a, \ts')] %   \otimes \alpha.\mview_{(w,q)}
{\alpha, \gamma\  \strans{a}_{t}\  \alpha[\writes \asgn \writes',
\tview_t \asgn \tview'], \gamma }

Rules Enq-Base and Deq-Base define the basic rules for
enqueues and dequeues, factoring out the common aspects of relaxed and
synchronising operations. Enq-Base helps determine an
appropriate timestamp for a new (enqueue) operation and advances the
thread view of the executing thread to this timestamp. For a relaxed enqueue,
Enq-Rlx, no other state changes are necessary. However, for an acquiring enqueue, the modification view of the new operation must be updated as defined by Enq-Sync.

Deq-Base is similar to Enq-Base, but it also makes the
enqueue that the dequeue matches with explicit. This is used in rule
Deq-NE-Sync to update thread views of both the library and the
client to be consistent with the corresponding (releasing) enqueue operation.

§ PROOF RULES FOR CLIENTS AND LIBRARIES

Here, we give a set of rules from our Isabelle/HOL development
[7] that we use in the verification of client-library

We use $[S]_t^X$, where $S$ is a statement, $t$ is a thread and
$X \in \{L, C\}$ to denote that $S$ is statement of either the library
($L$) or client ($C$) action that is executed by thread $t$. E.g.,
$[x ~ := ~ v]^L_t$ denotes that $x := v$ is a write statement of the
library being executed thread $t$.

We specialise the notion of a covered operation from
sec:assertion-language and define covered writes over shared
locations as follows:

\begin{align*}
CW[x, u](\sigma) \equiv \forall w .\  w \in \sigma.(W_{|x})^{-1} \land w \not\in \sigma.cvd \imp w = \sigma.\last(W,x) \land \wrval(w) = u
\end{align*}

The assertion $CW[x, u]$ assumes a variable (or location) $x$ and
value $u$, and holds iff all but the last write to $x$ are covered,
and that the value of the last write is $u$.

* $\inference[{}]{ X \in \{L, C\}
}{\{[x ~ = ~ u]^X_t \} [x ~ := ~ v]^X_t \{[x ~ = ~ u]^X_t\}}$

* $\inference[{}]{ ~ X \in \{L, C\}
\{\exists ~ u ~ . ~ CW[x, u]\}\  [\kwcas^{\sf R}(x, v, ~ v')]^X_t
\{\exists ~ v ~ . ~ CW[x, v] \}}$

* $\inference[{}]{ ~ X \in \{L, C\}
}{ \{CW[x, ~ v]^X \}
~~ [r \gets \kwcas^{\sf R}(x, ~ u, ~ u')]_t^X~ \{r \imp [x ~ = ~ u']_t^X\}}$

* $\inference[{}]{
X \in \{L, C\}
}{ \{\langle x ~ = ~ a\rangle^{L}[y ~ = ~ b]_t^{X} \}~~[a ~ \leftarrow^A ~ x]_t^L~ \{[y ~ = ~ b]_t^X\} ~
~  ~ }$

* $\inference[{}]{ ~ X, X' \in \{L, C\} }{ \{[x ~ =_t ~ m]^X\}
~~ [r \gets \kwcas^{\sf R}(x, ~ u, ~ u')]_t^{X'}~ \{\neg r \imp [x ~ = ~ m]_t^X\}}$

* $\inference[{}]{X\in\{L, C\} \qquad t ~ \neq ~  ~ t'
\qquad x ~ \neq ~  ~ y
}{ ~ \{\neg ~ [x~ \approx ~ u]_{t'}^X
~~\land~~[y ~ = ~ v]_t^X\} [r \gets \kwcas^{\sf R}(x, ~ l, ~ u)]_t^X \{r \imp \langle x ~ = ~ u \rangle^{X} [y ~ = ~ v]_{t'}^{X}\}
~  ~ }$

* $\inference[{}]{
X\in\{L, C\} \qquad k ~ \neq ~  ~ u
\qquad t ~ \neq ~  ~ t' \qquad x ~ \neq ~  ~ y
}{ ~\{\langle x ~ = ~ u \rangle^{X} [y ~ = ~ v]_{t'}^{X}\} [r \gets \kwcas^{\sf R}(x, ~ l, ~ k)]_t^{X} \{r \imp \langle x ~ = ~ u \rangle^{X} [y ~ = ~ v]_{t'}^{X}\}
~  ~ }$

* $\inference[{}]{X\in\{L, C\} \qquad  x\neq  y }{\{[y ~ = ~ v]_t^{X} ~ ~~\land~~ ~ CW[x, ~ m]^{X}\} [r \gets \kwcas^{\sf R}(x, ~ m, ~ u)]_t^{X} \{r \imp \langle x ~ = ~ u\rangle^{X}[y ~ = ~ v ~]_t^{X}\}}$

* $\inference[{}]{X \in \{L, C\}~~
}{\{true\} [v ~ \leftarrow^{[A]} ~ x]_t^{X} \{[x ~ \approx ~ v]_t^{X}\} ~
~  ~ }$

* $\inference[{}]{
X \in \{L, C\}
}{ ~\{CW[x, ~ v]^{X}\}~~ [r \gets \kwcas^{\sf R}(x, ~ v, ~ v')]_t^{X} ~~ \{r \imp CW[x, ~ v']^{X}\} ~
~  ~ }$

* $\inference[{}]{
X \in \{L, C\}
}{\{CW[x, ~ v]^{X}\} [r \gets \kwfai(x)]^{X}_t~ \{CW[x, ~ (v+1)]^{X}\} ~
~  ~ }$

* $\inference[{}]{
X \in \{L, C\}
}{ \{True\}~~ [r \gets \kwcas^{\sf R}(x, ~ v, ~ v')]_t^{X}~ \{r \imp [x ~ \approx ~ v']_t^{X}\} ~
~  ~ }$

* $\inference[{}]{
X \in \{L, C\}
~~\land~~x ~ \neq ~  ~ y
}{\{\neg ~ [x ~ \approx ~ u]_t^{X}\} ~ [r \gets \kwcas^{\sf R}(y, ~ v, ~ v')]_{t'}^{X} ~ \{\neg ~ [x ~ \approx ~ u]_t^{X}\}}$

* $\inference[{}]{
X \in \{L, C\}
}{\{\neg ~ [x ~ \approx ~ u]_t^{X}\} ~[v ~ \leftarrow ~ y]_{t'}^{X} ~ \{\neg ~ [x ~ \approx ~ u]_t^{X}\}}$

* $\inference[{}]{
X \in \{L, C\} \qquad y ~ \neq ~  ~ x
}{\{\langle x ~ = ~ v \rangle^{X}[x ~ = ~ v]^{X}_t \} ~[v \gets \kwfai(y)]_{t'}^{X}~ \{\langle x ~ = ~ v \rangle^{X}[x ~ = ~ v]^{X}_t\}}$

* $\inference[{}]{X \in \{L, C\}
}{ ~\{\langle x ~ = ~ v \rangle^{X}[x ~ = ~ v]^{X}_t\} ~~ [v ~ \leftarrow^A ~ x]_t^{X} ~~ \{[x ~ = ~ v]_t^{X}\} ~
~  ~ }$

* $\inference[{}]{
X \in \{L, C\} \qquad t ~ \neq ~  ~ t'
}{\{\neg ~ [x ~ \approx ~ u]_t^{X} ~
~~\land~~[x ~ = ~ v]_{t'}^{X}\} ~[x ~ :=^{\sf R}~ u]_{t'}^{X}~ \{\langle x ~ = ~ u\rangle^{X}[x ~ = ~ u]_t^{X}\} ~
~  ~ }$

* $\inference[{}]{
X \in \{L, C\}
\qquad x ~ \neq ~  ~ y
}{\{\langle x ~ = ~ u\rangle^{X}[x ~ = ~ u]_t^{X}\} ~[y ~ := ~ v]_{t'}^{X}~ \{\langle x ~ = ~ u\rangle^{X}[x ~ = ~ u]_t^{X}\} ~
~  ~ }$

§ HOARE LOGIC RULES FOR THE ABSTRACT STACK OBJECT

In this section we provide a set of Hoare logic proof rules that we
used in our Isabelle/HOL development to prove programs that use the
abstract specification of the stack object. The rules relate
observation assertions for abstract method calls.

Here we assume that the
pop operations are part of the library, thus we omit the superscript
$L$ on the assertions and operations related to the stack. Recall that
$m^{[\sf Z]}(v)_t$ denotes that the annotation
${\sf Z} \in \{{\sf R}, {\sf A}\}$ is optional for the method $m$.

* $\inference[{}]{}{\{[pop(u)]_t\}~~ push^{[\sf R]}(v)_t  ~~\{[pop(v)]_t\} ~
~  ~ }$

* $\inference[{}]{}{\{[pop(u)]_t\}~~ push^{[\sf R]}(v)_t  ~~\{[pop(v)]_t\} ~
~  ~ }$

* $\inference[{}]{
}{\{[pop(u)]_t\} pop^{[\sf A]}(v)_t \{v ~ = ~ u\}
~  ~ }$

* $\inference[{}]{u \neq empty}{
\{\neg ~ \langle pop(u) \rangle_{t'}\wedge [y ~ =_t ~ v]^C\}\ push^{\sf R}(u)_t\
\{ \langle pop(u) \rangle [y ~ = ~ v]_{t'}\}}$

* $\inference[{}]
u \neq empty}{\{\langle pop(u)\rangle [y ~ = ~ v]_t^C\} pop^{\sf A}(u)_t \{[y ~ = ~ v]_t\}}$

* $\inference[{}]{
}{\{[x ~ = ~ v]_t^C\}\ push^{\sf [R]}(u)_{t'} \ \{[x ~ = ~ v]_t^C\}}$

* $\inference[{}]{
}{\{[x ~ = ~ v]_{t'}^C \}\ pop^{[\sf A]}(u)_t \ \{[x ~ = ~ v]_{t'}^C\}}$

* $\inference[{}]{
}{\{\neg ~ \langle pop(u)\rangle_{t'}\}\ [x := v]_t^C\ \{\neg ~ \langle pop(u)\rangle_{t'}\}
~  ~ }$

* $\inference[{}]{
}{\{\neg ~ \langle pop(u)\rangle_{t'}\}\ [v ~ \leftarrow ~ x]_t^C\ \{\neg ~ \langle pop(u)\rangle_{t'}\}}$

* $\inference[{}]{u \neq  empty}{\{\neg ~ \langle pop(u)\rangle_{t'}\} \ pop^{[A]}(v)_t \ \{\neg ~ \langle pop(u)\rangle_{t'}\}}$

* $\inference[{}]{
u \neq z
\qquad u \neq empty
\qquad z \neq empty
}{\{\langle pop(u)\rangle [y ~ = ~ v]_t^C\}\ pop^{[A]}(z)_t \ \{\langle pop(u)\rangle [y ~ = ~ v]_t^C\}}$

* $\inference[{}]{u\neq  z
~~ \qquad u \neq empty
}{\{\langle pop(u)\rangle [y ~ = ~ v]_t^C\}\ pop^{[A]}(z)_t \ \{\langle pop(u)\rangle [y ~ = ~ v]_t^C\}}$

* $\inference[{}]{}{\{\neg ~ \langle pop(u)\rangle_{t}\}\ [x ~ := ~ z]_{t'}^C \ \{\langle pop(u)\rangle [x ~ = ~ v]_t^C\}}$