11institutetext: IMDEA Software Institute 22institutetext: Microsoft Research
Cambridge

# A Generic Logic for Proving Linearizability
(Extended Version)

Artem Khyzha 11 Alexey Gotsman 11 Matthew Parkinson 22

###### Abstract

Linearizability is a commonly accepted notion of correctness for libraries of
concurrent algorithms, and recent years have seen a number of proposals of
program logics for proving it. Although these logics differ in technical
details, they embody similar reasoning principles. To explicate these
principles, we propose a logic for proving linearizability that is generic: it
can be instantiated with different means of compositional reasoning about
concurrency, such as separation logic or rely-guarantee. To this end, we
generalise the Views framework for reasoning about concurrency to handle
relations between programs, required for proving linearizability. We present
sample instantiations of our generic logic and show that it is powerful enough
to handle concurrent algorithms with challenging features, such as helping.

##  1 Introduction

To manage the complexity of constructing concurrent software, programmers
package often-used functionality into libraries of concurrent algorithms.
These encapsulate data structures, such as queues and lists, and provide
clients with a set of methods that can be called concurrently to operate on
these (e.g., java.util.concurrent). To maximise performance, concurrent
libraries may use sophisticated non-blocking techniques, allowing multiple
threads to operate on the data structure with minimum synchronisation. Despite
this, each library method is usually expected to behave as though it executes
atomically. This requirement is formalised by the standard notion of
correctness for concurrent libraries, linearizability [14], which establishes
a form of a simulation between the original concrete library and another
abstract library, where each method is implemented atomically.

A common approach to proving linearizability is to find a linearization point
for every method of the concrete library at which it can be thought of taking
effect. 111Some algorithms cannot be reasoned about using linearization
points, which we discuss in §7. Given an execution of a concrete library, the
matching execution of the abstract library, required to show the simulation,
is constructed by executing the atomic abstract method at the linearization
point of the concrete method. A difficulty in this approach is that
linearization points are often not determined by a statically chosen point in
the method code. For example, in concurrent algorithms with helping [13], a
method may execute an operation originally requested by another method, called
in a different thread; then the linearization point of the latter method is
determined by an action of the former.

Recent years have seen a number of program logics for proving linearizability
(see [6] for a survey). To avoid reasoning about the high number of possible
interleavings between concurrently executing threads, these logics often use
thread-modular reasoning. They establish protocols that threads should follow
when operating on the shared data structure and reason separately about every
thread, assuming that the rest follow the protocols. The logics for proving
linearizability, such as [26, 18], usually borrow thread-modular reasoning
rules from logics originally designed for proving non-relational properties of
concurrent programs, such as rely-guarantee [15], separation logic [21] or
combinations thereof [26, 7]. Although this leads the logics to differ in
technical details, they use similar methods for reasoning about
linearizability, usually based on linearization points. Despite this
similarity, designing a logic for proving linearizability that uses a
particular thread-modular reasoning method currently requires finding the
proof rules and proving their soundness afresh.

To consolidate this design space of linearization-point-based reasoning, we
propose a logic for linearizability that is generic, i.e., can be instantiated
with different means of thread-modular reasoning about concurrency, such as
separation logic [21] or rely-guarantee [15]. To this end, we build on the
recently-proposed Views framework [3], which unifies thread-modular logics for
concurrency, such as the above-mentioned ones. Our contribution is to
generalise the framework to reason about relations between programs, required
for proving linearizability. In more detail, assertions in our logic are
interpreted over a monoid of relational views, which describe relationships
between the states of the concrete and the abstract libraries and the protocol
that threads should follow in operating on these. The operation of the monoid,
similar to the separating conjunction in separation logic [21], combines the
assertions in different threads while ensuring that they agree on the
protocols of access to the state. The choice of a particular relational view
monoid thus determines the thread-modular reasoning method used by our logic.

To reason about linearization points, relational views additionally describe a
set of special tokens (as in [26, 18, 2]), each denoting a one-time permission
to execute a given atomic command on the state of the abstract library. The
place where this permission is used in the proof of a concrete library method
determines its linearization point, with the abstract command recorded by the
token giving its specification. Crucially, reasoning about the tokens is
subject to the protocols established by the underlying thread-modular
reasoning method; in particular, their _ownership_ can be transferred between
different threads, which allows us to deal with helping.

We prove the soundness of our generic logic under certain conditions on its
instantiations (Definition 2, §3). These conditions represent our key
technical contribution, as they capture the essential requirements for soundly
combining a given thread-modular method for reasoning about concurrency with
the linearization-point method for reasoning about linearizability.

To illustrate the use of our logic, we present its example instantiations
where thread-modular reasoning is done using disjoint concurrent separation
logic [20] and a combination of separation logic and rely-guarantee [26]. We
then apply the latter instantiation to prove the correctness of a sample
concurrent algorithm with helping. We expect that our results will make it
possible to systematically design logics using the plethora of other methods
for thread-modular reasoning that have been shown to be expressible in the
Views framework [20, 4, 1].

##  2 Methods Syntax and Sequential Semantics

We consider concurrent programs that consist of two components, which we call
libraries and clients. Libraries provide clients with a set of methods, and
clients call them concurrently. We distinguish concrete and abstract
libraries, as the latter serve as specification for the former due to its
methods being executed atomically.

Syntax. Concrete methods are implemented as sequential commands having the
syntax:

$C\in{\sf Com}::={\sf\alpha}\mid C\mathbin{\,;\,}C\mid
C\mathbin{+}C\mid{C}^{\star}\mid{\sf skip},\quad\mbox{where
}{\sf\alpha}\in{\sf PCom}$

The grammar includes primitive commands ${\sf\alpha}$ from a set ${\sf PCom}$,
sequential composition $C\mathbin{\,;\,}C$, non-deterministic choice
$C\mathbin{+}C$ and a finite iteration ${C}^{\star}$ (we are interested only
in terminating executions) and a termination marker ${\sf skip}$. We use
$\mathbin{+}$ and $(\cdot)^{\star}$ instead of conditionals and while loops
for theoretical simplicity: as we show at the end of this section, given
appropriate primitive commands the conditionals and loops can be encoded. We
also assume a set ${\sf APCom}$ of abstract primitive commands, ranged over by
${\rm A}$, with which we represent methods of an abstract library.

${\longrightarrow}\subseteq{\sf Com}\times{\sf PCom}\times{\sf Com}$

$\begin{array}[]{l@{\ }l@{\ }l}\genfrac{}{}{0.5pt}{}{\displaystyle
C_{1}\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}_{1}}{\displaystyle
C_{1}\mathbin{\,;\,}C_{2}\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}_{1}\mathbin{\,;\,}C_{2}}&\genfrac{}{}{0.5pt}{}{\displaystyle\,}{\displaystyle{C}^{\star}\mathrel{{\xlongrightarrow{{\sf
id}}}{}}C;{C}^{\star}}&\genfrac{}{}{0.5pt}{}{\displaystyle\,}{\displaystyle{\sf\alpha}\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}{\sf
skip}}\\\ \genfrac{}{}{0.5pt}{}{\displaystyle i\in\\{1,2\\}}{\displaystyle
C_{1}\mathbin{+}C_{2}\mathrel{{\xlongrightarrow{{\sf
id}}}{}}C_{i}}&\genfrac{}{}{0.5pt}{}{\displaystyle\,}{\displaystyle{\sf
skip}\mathbin{\,;\,}C\mathrel{{\xlongrightarrow{{\sf
id}}}{}}C}&\genfrac{}{}{0.5pt}{}{\displaystyle\,}{\displaystyle{C}^{\star}\mathrel{{\xlongrightarrow{{\sf
id}}}{}}{\sf skip}}\end{array}$

${\ext@arrow
05{40}0{\arrowfill@\relbar\relbar\twoheadrightarrow}{}{}}\subseteq({\sf
Com}\times{\sf State})\times({\sf ThreadID}\times{\sf PCom})\times({\sf
Com}\times{\sf State})$

$\genfrac{}{}{0.5pt}{}{\displaystyle\sigma^{\prime}\in\llbracket{\sf\alpha}\rrbracket_{t}(\sigma)\quad
C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}}{\displaystyle\langle
C,\sigma\rangle\mathrel{{\ext@arrow
05{40}0{\arrowfill@\relbar\relbar\twoheadrightarrow}{}{t,{\sf\alpha}}}{}}\langle
C^{\prime},\sigma^{\prime}\rangle}$

Figure 1: The operational semantics of sequential commands

Semantics. We assume a set ${\sf State}$ of concrete states of the memory,
ranged over by $\sigma$, and abstract states ${\sf AState}$, ranged over by
$\Sigma$. The memory is shared among $N$ threads with thread identifiers ${\sf
ThreadID}=\\{1,2,\dots,N\\}$, ranged over by $t$.

We assume that semantics of each primitive command ${\sf\alpha}$ is given by a
non-deterministic state transformer $\llbracket{\sf\alpha}\rrbracket_{t}:{\sf
State}\to\mathcal{P}({\sf State})$, where $t\in{\sf ThreadID}$. For a state
$\sigma$, the set of states $\llbracket{\sf\alpha}\rrbracket_{t}(\sigma)$ is
the set of possible resulting states for ${\sf\alpha}$ executed atomically in
a state $\sigma$ and a thread $t$. State transformers may have different
semantics depending on a thread identifier, which we use to introduce thread-
local memory cells later in the technical development. Analogously, we assume
semantics of abstract primitive commands with state transformers
$\llbracket{\rm A}\rrbracket_{t}:{\sf AState}\to\mathcal{P}({\sf AState})$,
all of which update abstract states atomically. We also assume a primitive
command ${\sf id}\in{\sf PCom}$ with the interpretation $\llbracket{\sf
id}\rrbracket_{t}(\sigma)\triangleq\\{\sigma\\}$, and its abstract counterpart
${\sf id}\in{\sf APCom}$.

The sets of primitive commands ${\sf PCom}$ and ${\sf APCom}$ as well as
corresponding state transformers are parameters of our framework. In Figure 1
we give rules of operational semantics of sequential commands, which are
parametrised by semantics of primitive commands. That is, we define a
transition relation ${\ext@arrow
05{40}0{\arrowfill@\relbar\relbar\twoheadrightarrow}{}{}}~{}\subseteq~{}({\sf
Com}\times{\sf State})\times({\sf ThreadID}\times{\sf PCom})\times({\sf
Com}\times{\sf State})$, so that $\langle C,\sigma\rangle\mathrel{{\ext@arrow
05{40}0{\arrowfill@\relbar\relbar\twoheadrightarrow}{}{t,{\sf\alpha}}}{}}\langle
C^{\prime},\sigma^{\prime}\rangle$ indicates a transition from $C$ to
$C^{\prime}$ updating the state from $\sigma$ to $\sigma^{\prime}$ with a
primitive command ${\sf\alpha}$ in a thread $t$. The rules of the operational
semantics are standard.

Let us show how to define traditional control flow primitives, such as an if-
statement and a while-loop, in our programming language. Assuming a language
for arithmetic expressions, ranged over by $E$, and a function $\llbracket
E\rrbracket_{\sigma}$ that evaluates expressions in a given state $\sigma$, we
define a primitive command ${\tt assume}(E)$ that acts as a filter on states,
choosing only those where $E$ evaluates to non-zero values.

$\llbracket{\tt assume}(E)\rrbracket_{t}(\sigma)\triangleq\mbox{ if
}\llbracket E\rrbracket_{\sigma}\not=0\mbox{ then }\\{\sigma\\}\mbox{ else
}\emptyset.$

Using ${\tt assume}(E)$ and the C-style negation $!E$ in expressions, a
conditional and a while-loop can be implemented as the following commands:

$\displaystyle{\tt if}\ E\ {\tt then}\ C_{1}\ {\tt else}\ C_{2}\triangleq({\tt
assume}(E);C_{1})\mathbin{+}({\tt assume}(!E);C_{2})$ $\displaystyle{\tt
while}\ E\ {\tt do}\ C\triangleq({\tt assume}(E);C)^{\star};{\tt assume}(!E)$

##  3 The generic logic

In this section, we present our framework for designing program logics for
linearizability proofs. Given a concrete method and a corresponding abstract
method, we aim to demonstrate that the former has a linearization point either
within its code or in the code of another thread. The idea behind such proofs
is to establish simulation between concrete and abstract methods using
linearization points to determine when the abstract method has to make a
transition to match a given execution of the concrete method. To facilitate
such simulation-based proofs, we design our relational logic so that formulas
in it denote relations between concrete states, abstract states and special
tokens.

Tokens are our tool for reasoning about linearization points. At the beginning
of its execution in a thread $t$, each concrete method $m$ is given a token
${\sf todo}({\rm A}_{m})$ of the corresponding abstract primitive command
${\rm A}_{m}$. The token represents a one-time permission for the method to
take effect, i.e. to perform a primitive command ${\rm A}_{m}$ on an abstract
machine. When the permission is used, a token ${\sf todo}({\rm A}_{m})$ in a
thread $t$ is irreversibly replaced with ${\sf done}({\rm A}_{m})$. Thus, by
requiring that a method start its execution in a thread $t$ with a token ${\sf
todo}({\rm A}_{m})$ and ends with ${\sf done}({\rm A}_{m})$, we ensure that it
has in its code a linearization point. The tokens of all threads are described
by $\Delta\in{\sf Tokens}$:

${\sf Tokens}={\sf ThreadID}\rightharpoonup(\\{{\sf todo}({\rm A})\mid{\rm
A}\in{\sf APCom}\\}\cup\\{{\sf done}({\rm A})\mid{\rm A}\in{\sf APCom}\\})$

Reasoning about states and tokens in the framework is done with the help of
relational views. We assume a set ${\sf Views}$, ranged over by $p$, $q$ and
$r$, as well as a reification function $\lfloor{\ }\rfloor:{\sf
Views}\to\mathcal{P}({\sf State}\times{\sf AState}\times{\sf Tokens})$ that
interprets views as ternary relations on concrete states, abstract states and
indexed sets of tokens.

###### Definition 1

A relational view monoid is a commutative monoid $({\sf
Views},\mathbin{*},u)$, where ${\sf Views}$ is an underlying set of relational
views, $\mathbin{*}$ is a monoid operation and $u$ is a unit.

The monoid structure of relational views allows treating them as restrictions
on the environment of threads. Intuitively, each thread uses views to declare
a protocol that other threads should follow while operating with concrete
states, abstract states and tokens. Similarly to the separating conjunction
from separation logic, the monoid operation $\mathbin{*}$ (view composition)
applied to a pair of views combines protocols of access to the state and
ensures that they do not contradict each other.

Disjoint Concurrent Separation logic. To give an example of a view monoid, we
demonstrate the structure inspired by Disjoint Concurrent Separation logic
(DCSL). A distinctive feature of DCSL is that its assertions enforce a
protocol, according to which threads operate on disjoint pieces of memory. We
assume a set of values ${\sf Val}$, of which a subset ${\sf Loc}\subseteq{\sf
Val}$ represents heap addresses. By letting ${\sf State}={\sf AState}=({\sf
Loc}\rightharpoonup_{\rm fin}{\sf Val})\cup\\{\lightning\\}$ we represent a
state as either a finite partial function from locations to values or an
exceptional faulting state $\lightning$, which denotes the result of an
invalid memory access. We define an operation $\bullet$ on states, which
results in $\lightning$ if either of the operands is $\lightning$, or the
union of partial functions if their domains are disjoint. Finally, we assume
that the set ${\sf PCom}$ consists of standard heap-manipulating commands with
usual semantics [21, 3].

We consider the view monoid $(\mathcal{P}(({\sf
State}\setminus\\{\lightning\\})\times({\sf
AState}\setminus\\{\lightning\\})\times{\sf Tokens}),\mathbin{*}_{\sf SL},([\
],[\ ],[\ ]))$: the unit is a triple of nowhere defined functions $[\ ]$, and
the view composition defined as follows:

$p\mathbin{*}_{\sf
SL}p^{\prime}\triangleq\\{(\sigma\bullet\sigma^{\prime},\Sigma\bullet\Sigma^{\prime},\Delta\uplus\Delta^{\prime})\mid(\sigma,\Sigma,\Delta)\in
p\land(\sigma^{\prime},\Sigma^{\prime},\Delta^{\prime})\in p^{\prime}\\}.$

In this monoid, the composition enforces a protocol of exclusive ownership of
parts of the heap: a pair of views can be composed only if they do not
simultaneously describe the content of the same heap cell or a token. Since
tokens are exclusively owned in DCSL, they cannot be accessed by other
threads, which makes it impossible to express a helping mechanism with the
DCSL views. In §5, we present another instance of our framework and reason
about helping in it.

Reasoning about linearization points. We now introduce action judgements,
which formalise linearization-points-based approach to proving linearizability
within our framework.

|
---|---
$\textstyle{\sigma\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\lfloor{p\mathbin{*}r}\rfloor}$$\scriptstyle{\llbracket{\sf\alpha}\rrbracket}$$\textstyle{\Sigma\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\llbracket{\rm
A}\rrbracket}$$\textstyle{\sigma^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\lfloor{q\mathbin{*}r}\rfloor}$$\textstyle{\Sigma^{\prime}}$

Let us assume that ${\sf\alpha}$ is executed in a concrete state $\sigma$ with
an abstract state $\Sigma$ and a set of tokens $\Delta$ satisfying a
precondition $p$. According to the action judgement
$\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{q\\}$, for every update
$\sigma^{\prime}\in\llbracket{\sf\alpha}\rrbracket_{t}(\sigma)$ of the
concrete state, the abstract state may be changed to
$\Sigma^{\prime}\in\llbracket{\rm A}\rrbracket_{t^{\prime}}(\Sigma)$ in order
to satisfy the postcondition $q$, provided that there is a token ${\sf
todo}({\rm A})$ in a thread $t^{\prime}$. When the abstract state $\Sigma$ is
changed and the token ${\sf todo}({\rm A})$ of a thread $t^{\prime}$ is used,
the concrete state update corresponds to a linearization point, or to a
regular transition otherwise.

###### Definition 2

The action judgement $\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{q\\}$ holds, iff the
following is true:

$\forall
r,\sigma,\sigma^{\prime},\Sigma,\Delta{.\,}(\sigma,\Sigma,\Delta)\in\lfloor{p\mathbin{*}r}\rfloor\land\sigma^{\prime}\in\llbracket{\sf\alpha}\rrbracket_{t}(\sigma)\implies{}\\\
\exists\Sigma^{\prime},\Delta^{\prime}{.\,}{\sf
LP}^{*}(\Sigma,\Delta,\Sigma^{\prime},\Delta^{\prime})\land(\sigma^{\prime},\Sigma^{\prime},\Delta^{\prime})\in\lfloor{q\mathbin{*}r}\rfloor,$

where ${\sf LP}^{*}$ is the transitive closure of the following relation:

${\sf LP}(\Sigma,\Delta,\Sigma^{\prime},\Delta^{\prime})\triangleq\exists
t^{\prime},{\rm A}\ldotp\Sigma^{\prime}\in\llbracket{\rm
A}\rrbracket_{t^{\prime}}(\Sigma)\land\Delta(t^{\prime})={\sf todo}({\rm
A})\land\Delta^{\prime}=\Delta[t^{\prime}:{\sf done}({\rm A})],$

and $f[x:a]$ denotes the function such that $f[x:a](x)=a$ and for any $y\neq
x$, $f[x:a](y)=f(y)$.

Note that depending on pre- and postconditions $p$ and $q$,
$\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{q\\}$ may encode a regular transition, a
conditional or a standard linearization point. It is easy to see that the
latter is the case only when in all sets of tokens $\Delta$ from
$\lfloor{p}\rfloor$ some thread $t^{\prime}$ has a todo-token, and in all
$\Delta^{\prime}$ from $\lfloor{q}\rfloor$ it has a done-token. Additionally,
the action judgement may represent a conditional linearization point of
another thread, as the ${\sf LP}$ relation allows using tokens of other
threads.

Action judgements have a closure property that is important for thread-modular
reasoning: when $\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{q\\}$ holds, so does
$\,{\sf\alpha}\Vdash_{t}\\{p*r\\}\\{q*r\\}$ for every view $r$. That is,
execution of ${\sf\alpha}$ and a corresponding linearization point preserves
every view $r$ that $p$ can be composed with. Consequently, when in every
thread action judgements hold of primitive commands and thread’s views, all
threads together mutually agree on each other’s protocols of the access to the
shared memory encoded in their views. This enables reasoning about every
thread in isolation with the assumption that its environment follows its
protocol. Thus, the action judgements formalise the requirements that
instances of our framework need to satisfy in order to be sound. In this
regard action judgements are inspired by semantic judgements of the Views
Framework [3]. Our technical contribution is in formulating the essential
requirements for thread-modular reasoning about linearizability of concurrent
libraries with the linearization-point method and in extending the semantic
judgement with them.

We let a repartitioning implication of views $p$ and $q$, written
$p\Rrightarrow q$, denote $\forall
r{.\,}\lfloor{p*r}\rfloor\subseteq\lfloor{q*r}\rfloor$. A repartitioning
implication $p\Rrightarrow q$ ensures that states satisfying $p$ also satisfy
$q$ and additionally requires this property to preserve any view $r$.

Program logic. We are now in a position to present our generic logic for
linearizability proofs via the linearization-point method. Assuming a view
monoid and reification function as parameters, we define a minimal language
${\sf Assn}$ for assertions $\mathcal{P}$ and $\mathcal{Q}$ denoting sets of
views:

$\displaystyle\mathcal{P},\mathcal{Q}\in{\sf
Assn}::=\rho\mid\mathcal{P}\mathbin{*}\mathcal{Q}\mid\mathcal{P}\lor\mathcal{Q}\mid\mathcal{P}\Rrightarrow\mathcal{Q}\mid\exists
X{.\,}\mathcal{P}\mid\dots$

The grammar includes view assertions $\rho$, a syntax ${\sf VAssn}$ of which
is a parameter of the framework. Formulas of ${\sf Assn}$ may contain the
standard connectives from separation logic, the repartitioning implication and
the existential quantification over logical variables $X$, ranging over a set
${\sf LVar}$.

$\begin{array}[]{l c
r}\llbracket\mathcal{P}\mathbin{*}\mathcal{Q}\rrbracket_{{\bf
i}}=\llbracket\mathcal{P}\rrbracket_{{\bf
i}}\mathbin{*}\llbracket\mathcal{Q}\rrbracket_{{\bf
i}}&&\llbracket\mathcal{P}\Rrightarrow\mathcal{Q}\rrbracket_{{\bf
i}}=\llbracket\mathcal{P}\rrbracket_{{\bf
i}}\Rrightarrow\llbracket\mathcal{Q}\rrbracket_{{\bf i}}\\\\[1.0pt]
\llbracket\mathcal{P}\lor\mathcal{Q}\rrbracket_{{\bf
i}}=\llbracket\mathcal{P}\rrbracket_{{\bf
i}}\lor\llbracket\mathcal{Q}\rrbracket_{{\bf i}}&\hfill\hfil&\llbracket\exists
X{.\,}\mathcal{P}\rrbracket_{{\bf i}}=\bigvee_{n\in{\sf
Val}}\llbracket\mathcal{P}\rrbracket_{{\bf i}[X:n]}\end{array}$

Figure 2: Satisfaction relation for the assertion language ${\sf Assn}$

Let us assume an interpretation of logical variables ${\bf i}\in{\sf Int}={\sf
LVar}\to{\sf Val}$ that maps logical variables from ${\sf LVar}$ to values
from a finite set ${\sf Val}$. In Figure 2, we define a function
$\llbracket\cdot\rrbracket_{\cdot}:{\sf Assn}\times{\sf Int}\to{\sf Views}$
that we use to interpret assertions. Interpretation of assertions is
parametrised by $\llbracket\cdot\rrbracket_{\cdot}:{\sf VAssn}\times{\sf
Int}\to{\sf Views}$. In order to interpret disjunction, we introduce a
corresponding operation on views and require the following properties from it:

$\begin{array}[]{l@{\hspace{7em}}l}\lfloor{p\lor
q}\rfloor=\lfloor{p}\rfloor\cup\lfloor{q}\rfloor\hfil\hskip 70.0001pt&(p\lor
q)*r=(p*r)\lor(q*r)\end{array}$ (1)

The judgements of the program logic take the form
$\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C\,\left\\{{\mathcal{Q}}\right\\}$.
In Figure 3, we present the proof rules, which are mostly standard. Among
them, the Prim rule is noteworthy, since it encorporates the simulation-based
approach to reasoning about linearization points introduced by action
judgements. The Frame rule applies the idea of local reasoning from separation
logic [21] to views. The Conseq enables weakening a precondition or a
postcondition in a proof judgement and uses repartitioning implications to
ensure the thread-modularity of the weakened proof judgement.

$\begin{array}[]{r@{\hspace{2pt}}c@{\hspace{2pt}}r@{\hspace{2pt}}c}\mbox{\footnotesize\sc(Prim)}\hskip
2.0&\dfrac{\forall{\bf
i}{.\,}\,{\sf\alpha}\Vdash_{t}\\{\llbracket\mathcal{P}\rrbracket_{{\bf
i}}\\}\\{\llbracket\mathcal{Q}\rrbracket_{{\bf
i}}\\}}{\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,{\sf\alpha}\,\left\\{{\mathcal{Q}}\right\\}}\hfil\hskip
2.0&\mbox{\footnotesize\sc(Seq)}\hskip
2.0&\dfrac{\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C_{1}\,\left\\{{\mathcal{P}^{\prime}}\right\\}\quad\vdash_{t}\left\\{{\mathcal{P}^{\prime}}\right\\}\,C_{2}\,\left\\{{\mathcal{Q}}\right\\}}{\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C_{1}\mathbin{\,;\,}C_{2}\,\left\\{{\mathcal{Q}}\right\\}}\\\\[9.0pt]
\mbox{\footnotesize\sc(Frame)}\hskip
2.0&\dfrac{\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C\,\left\\{{\mathcal{Q}}\right\\}}{\vdash_{t}\left\\{{\mathcal{P}\mathbin{*}\mathcal{R}}\right\\}\,C\,\left\\{{\mathcal{Q}\mathbin{*}\mathcal{R}}\right\\}}\hfil\hskip
2.0&\mbox{\footnotesize\sc(Disj)}\hskip
2.0&\dfrac{\vdash_{t}\left\\{{\mathcal{P}_{1}}\right\\}\,C\,\left\\{{\mathcal{Q}_{1}}\right\\}\quad\vdash_{t}\left\\{{\mathcal{P}_{2}}\right\\}\,C\,\left\\{{\mathcal{Q}_{2}}\right\\}}{\vdash_{t}\left\\{{\mathcal{P}_{1}\lor\mathcal{P}_{2}}\right\\}\,C\,\left\\{{\mathcal{Q}_{1}\lor\mathcal{Q}_{2}}\right\\}}\\\\[9.0pt]
\mbox{\footnotesize\sc(Ex)}\hskip
2.0&\dfrac{\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C\,\left\\{{\mathcal{Q}}\right\\}}{\vdash_{t}\left\\{{\exists
X{.\,}\mathcal{P}}\right\\}\,C\,\left\\{{\exists
X{.\,}\mathcal{Q}}\right\\}}\hfil\hskip
2.0&\mbox{\footnotesize\sc(Choice)}\hskip
2.0&\dfrac{\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C_{1}\,\left\\{{\mathcal{Q}}\right\\}\quad\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C_{2}\,\left\\{{\mathcal{Q}}\right\\}}{\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C_{1}\mathbin{+}C_{2}\,\left\\{{\mathcal{Q}}\right\\}}\\\\[9.0pt]
\mbox{\footnotesize\sc(Iter)}\hskip
2.0&\dfrac{\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C\,\left\\{{\mathcal{P}}\right\\}}{\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C^{\star}\,\left\\{{\mathcal{P}}\right\\}}\hfil\hskip
2.0&\mbox{\footnotesize\sc(Conseq)}\hskip
2.0&\dfrac{\mathcal{P}^{\prime}\Rrightarrow\mathcal{P}\quad\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C\,\left\\{{\mathcal{Q}}\right\\}\quad\mathcal{Q}\Rrightarrow\mathcal{Q}^{\prime}}{\vdash_{t}\left\\{{\mathcal{P}^{\prime}}\right\\}\,C\,\left\\{{\mathcal{Q}^{\prime}}\right\\}}\end{array}$

Figure 3: Proof rules

Semantics of proof judgements. We give semantics to judgements of the program
logic by lifting the requirements of action judgements to sequential commands.

######  Definition 3 (Safety Judgement)

We define ${\sf safe}_{t}$ as the greatest relation such that the following
holds whenever ${\sf safe}_{t}(p,C,q)$ does:

  * •

if $C\not={\sf skip}$, then $\forall
C^{\prime},{\sf\alpha}{.\,}C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}\implies\exists
p^{\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p^{\prime}\\}\land{\sf
safe}_{t}(p^{\prime},C^{\prime},q)$,

  * •

if $C={\sf skip}$, then $p\Rrightarrow q$.

###### Lemma 4

$\forall
t,\mathcal{P},C,\mathcal{Q}{.\,}\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C\,\left\\{{\mathcal{Q}}\right\\}\implies\forall{\bf
i}{.\,}{\sf safe}_{t}(\llbracket\mathcal{P}\rrbracket_{{\bf
i}},C,\llbracket\mathcal{Q}\rrbracket_{{\bf i}}).$

We can understand the safety judgement ${\sf
safe}_{t}(\llbracket\mathcal{P}\rrbracket_{{\bf
i}},C,\llbracket\mathcal{Q}\rrbracket_{{\bf i}})$ as an obligation to create a
sequence of views $\llbracket\mathcal{P}\rrbracket_{{\bf
i}}=p_{1},p_{2},\dots,p_{n+1}=\llbracket\mathcal{Q}\rrbracket_{{\bf i}}$ for
each finite trace ${\sf\alpha}_{1},{\sf\alpha}_{2},\dots,{\sf\alpha}_{n}$ of
$C$ to justify each transition with action judgements
$\,{\sf\alpha}_{1}\Vdash_{t}\\{p_{1}\\}\\{p_{2}\\}$, …,
$\,{\sf\alpha}_{n}\Vdash_{t}\\{p_{n}\\}\\{p_{n+1}\\}$. Thus, when ${\sf
safe}_{t}(\llbracket\mathcal{P}\rrbracket_{{\bf
i}},C,\llbracket\mathcal{Q}\rrbracket_{{\bf i}})$ holds, it ensures that every
step of the machine correctly preserves a correspondence between a concrete
and abstract execution. Intuitively, the safety judgement lifts the simulation
between concrete and abstract primitive commands established with action
judgements to the implementation and specification of a method.

In Lemma 4, we establish that the proof judgements of the logic imply the
safety judgements. As a part of the proof, we show that each of the proof
rules of the logic holds of safety judgements. Due to space constraints, this
and other proofs are given in the extended version of the paper [17].

##  4 Soundness

In this section, we formulate linearizability for libraries. We also formulate
the soundness theorem, in which we state proof obligations that are necessary
to conclude linearizability.

Libraries. We assume a set of method names ${\sf Method}$, ranged over by $m$,
and consider a concrete library $\mathrm{\ell}:{\sf
Method}\rightharpoonup(({\sf Val}\times{\sf Val})\to{\sf Com})$ that maps
method names to commands from ${\sf Com}$, which are parametrised by a pair of
values from ${\sf Val}$. For a given method name $m\in{\sf
dom}(\mathrm{\ell})$ and values $a,v\in{\sf Val}$, a command
$\mathrm{\ell}(m,a,v)$ is an implementation of $m$, which accepts $a$ as a
method argument and either returns $v$ or does not terminate. Such an unusual
way of specifying method’s arguments and return values significantly
simplifies further development, since it does not require modelling a call
stack.

Along with the library $\mathrm{\ell}$ we consider its specification in the
form of an abstract library $\mathcal{L}\in{\sf Method}\rightharpoonup(({\sf
Val}\times{\sf Val})\to{\sf APCom})$ implementing a set of methods ${\sf
dom}(\mathcal{L})$ atomically as abstract primitive commands
$\\{\mathcal{L}(m,a,v)\mid m\in{\sf dom}(\mathcal{L})\\}$ parametrised by an
argument $a$ and a return value $v$. Given a method $m\in{\sf Method}$, we
assume that a parametrised abstract primitive command $\mathcal{L}(m)$ is
intended as a specification for $\mathrm{\ell}(m)$.

Linearizability. The linearizability assumes a complete isolation between a
library and its client, with interactions limited to passing values of a given
data type as parameters or return values of library methods. Consequently, we
are not interested in internal steps recorded in library computations, but
only in the interactions of the library with its client. We record such
interactions using histories, which are traces including only events ${\sf
call}\ m(a)$ and ${\sf ret}\ m(v)$ that indicate an invocation of a method $m$
with a parameter $a$ and returning from $m$ with a return value $v$, or
formally:

$h::=\varepsilon\mid(t,{\sf call}\ m(a))\mathbin{{:}{:}}h\mid(t,{\sf ret}\
m(v))\mathbin{{:}{:}}h.$

Given a library $\mathrm{\ell}$, we generate all finite histories of
$\mathrm{\ell}$ by considering $N$ threads repeatedly invoking library methods
in any order and with any possible arguments. The execution of methods is
described by semantics of commands from § 2.

We define a thread pool $\tau:{\sf ThreadID}\to({\sf idle}\uplus({\sf
Com}\times{\sf Val}))$ to characterise progress of methods execution in each
thread. The case of $\tau(t)={\sf idle}$ corresponds to no method running in a
thread $t$. When $\tau(t)=(C,v)$, to finish some method returning $v$ it
remains to execute $C$.

###### Definition 5

We let $\mathcal{H}\llbracket\mathrm{\ell},\sigma\rrbracket=\bigcup_{n\geq
0}\mathcal{H}_{n}\llbracket\mathrm{\ell},(\lambda t\ldotp{\sf
idle}),\sigma\rrbracket$ denote the set of all possible histories of a library
$\mathrm{\ell}$ that start from a state $\sigma$, where for a given thread
pool $\tau$, $\mathcal{H}_{n}\llbracket\mathrm{\ell},\tau,\sigma\rrbracket$ is
defined as a set of histories such that
$\mathcal{H}_{0}\llbracket\mathrm{\ell},\tau,\sigma\rrbracket\triangleq\\{\varepsilon\\}$
and:

$\begin{array}[]{rcl}\mathcal{H}_{n}\llbracket\mathrm{\ell},\tau,\sigma\rrbracket&\triangleq&\\{((t,{\sf
call}\ m(a))::h)\mid a\in{\sf Val}\land m\in{\sf
dom}(\mathrm{\ell})\land\tau(t)={\sf idle}\land{}\\\ &&\hskip
92.50014pt\exists v\ldotp
h\in\mathcal{H}_{n-1}\llbracket\mathrm{\ell},\tau[t:(\mathrm{\ell}(m,a,v),v)],\sigma\rrbracket\\}\\\
&&{}\cup\\{h\mid\exists
t,{\sf\alpha},C,C^{\prime},\sigma^{\prime},v\ldotp\tau(t)=(C,v)\land\langle
C,\sigma\rangle\mathrel{{\ext@arrow
05{40}0{\arrowfill@\relbar\relbar\twoheadrightarrow}{}{t,{\sf\alpha}}}{}}\langle
C^{\prime},\sigma^{\prime}\rangle\land{}\\\ &&\hskip
92.50014pth\in\mathcal{H}_{n-1}\llbracket\mathrm{\ell},\tau[t:(C^{\prime},v)],\sigma^{\prime}\rrbracket\\}\\\
&&{}\cup\\{((t,{\sf ret}\ m(v))::h)\mid m\in{\sf
dom}(\mathrm{\ell})\land\tau(t)=({\sf skip},v)\land{}\\\ &&\hskip
92.50014pth\in\mathcal{H}_{n-1}\llbracket\mathrm{\ell},\tau[t:{\sf
idle}],\sigma\rrbracket\\}\end{array}$

Thus, we construct the set of all finite histories inductively with all
threads initially idling. At each step of generation, in any idling thread $t$
any method $m\in{\sf dom}(\mathrm{\ell})$ may be called with any argument $a$
and an expected return value $v$, which leads to adding a command
$\mathrm{\ell}(m,a,v)$ to the thread pool of a thread $t$. Also, any thread
$t$, in which $\tau(t)=(C,v)$, may do a transition $\langle
C,\sigma\rangle\mathrel{{\ext@arrow
05{40}0{\arrowfill@\relbar\relbar\twoheadrightarrow}{}{t,{\sf\alpha}}}{}}\langle
C^{\prime},\sigma^{\prime}\rangle$ changing a command in the thread pool and
the concrete state. Finally, any thread that has finished execution of a
method’s command ($\tau(t)=({\sf skip},v)$) may become idle by letting
$\tau(t)={\sf idle}$.

We define $\mathcal{H}_{n}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket$
analogously and let the set of all histories of an abstract library
$\mathcal{L}$ starting from the initial state $\Sigma$ be
$\mathcal{H}\llbracket\mathcal{L},\Sigma\rrbracket=\bigcup_{n\geq
0}\mathcal{H}_{n}\llbracket\mathcal{L},(\lambda t\ldotp{\sf
idle}),\Sigma\rrbracket$.

###### Definition 6

For libraries $\mathrm{\ell}$ and $\mathcal{L}$ such that ${\sf
dom}(\mathrm{\ell})={\sf dom}(\mathcal{L})$, we say that $\mathcal{L}$
linearizes $\mathrm{\ell}$ in the states $\sigma$ and $\Sigma$, written
$(\mathrm{\ell},\sigma)\sqsubseteq(\mathcal{L},\Sigma)$, if
$\mathcal{H}\llbracket\mathrm{\ell},\sigma\rrbracket\subseteq\mathcal{H}\llbracket\mathcal{L},\Sigma\rrbracket$.

That is, an abstract library $\mathcal{L}$ linearizes $\mathrm{\ell}$ in the
states $\sigma$ and $\Sigma$, if every history of $\mathrm{\ell}$ can be
reproduced by $\mathcal{L}$. The definition is different from the standard one
[14]: we use the result obtained by Gotsman and Yang [10] stating that the
plain subset inclusion on the sets of histories produced by concrete and
abstract libraries is equivalent to the original definition of
linearizability.

Soundness w.r.t. linearizability. We now explain proof obligations that we
need to show for every method $m$ of a concrete library $\mathrm{\ell}$ to
conclude its linearizability. Particularly, for every thread $t$, argument
$a$, return value $v$, and a command $\mathrm{\ell}(m,a,v)$ we require that
there exist assertions $\mathcal{P}(t,\mathcal{L}(m,a,v))$ and
$\mathcal{Q}(t,\mathcal{L}(m,a,v))$, for which the following Hoare-style
specification holds:

$\vdash_{t}\left\\{{\mathcal{P}(t,\mathcal{L}(m,a,v))}\right\\}\,\mathrm{\ell}(m,a,v)\,\left\\{{\mathcal{Q}(t,\mathcal{L}(m,a,v))}\right\\}$
(2)

In the specification of $\mathrm{\ell}(m,a,v)$,
$\mathcal{P}(t,\mathcal{L}(m,a,v))$ and $\mathcal{Q}(t,\mathcal{L}(m,a,v))$
are assertions parametrised by a thread $t$ and an abstract command
$\mathcal{L}(m,a,v)$. We require that in a thread $t$ of all states satisfying
$\mathcal{P}(t,\mathcal{L}(m,a,v))$ and $\mathcal{Q}(t,\mathcal{L}(m,a,v))$
there be only tokens ${\sf todo}(\mathcal{L}(m,a,v))$ and ${\sf
done}(\mathcal{L}(m,a,v))$ respectively:

$\forall{\bf i},t,\sigma,\Sigma,\Delta,r\ldotp{}\\\\[-4.0pt]
\begin{array}[]{@{}l@{}}((\sigma,\Sigma,\Delta)\in\lfloor{\llbracket\mathcal{P}(t,\mathcal{L}(m,a,v))\rrbracket_{{\bf
i}}\mathbin{*}r}\rfloor\implies\Delta(t)={\sf todo}(\mathcal{L}(m,a,v)))\\\
{}\land((\sigma,\Sigma,\Delta)\in\lfloor{\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,v))\rrbracket_{{\bf
i}}\mathbin{*}r}\rfloor\implies\Delta(t)={\sf
done}(\mathcal{L}(m,a,v)))\end{array}$ (3)

Together, (2) and (3) impose a requirement that a concrete and an abstract
method return the same return value $v$. We also require that the states
satisfying the assertions only differ by a token of a thread $t$:

$\forall{\bf i},t,{\rm A},{\rm
A}^{\prime},r,\Delta\ldotp(\sigma,\Sigma,\Delta[t:{\sf done}({\rm
A})])\in\lfloor{\llbracket\mathcal{Q}(t,{\rm A})\rrbracket_{{\bf
i}}\mathbin{*}r}\rfloor\iff{}\\\ (\sigma,\Sigma,\Delta[t:{\sf todo}({\rm
A}^{\prime})])\in\lfloor{\llbracket\mathcal{P}(t,{\rm
A}^{\prime})\rrbracket_{{\bf i}}\mathbin{*}r}\rfloor.$ (4)

###### Theorem 7

For given libraries $\mathrm{\ell}$ and $\mathcal{L}$ together with states
$\sigma$ and $\Sigma$, $(\mathrm{\ell},\sigma)\sqsubseteq(\mathcal{L},\Sigma)$
holds, if ${\sf dom}(\mathrm{\ell})={\sf dom}(\mathcal{L})$ and (2), (3) and
(4) hold for every method $m$, thread $t$ and values $a$ and $v$.

##  5 The RGSep-based Logic

In this section, we demonstrate an instance of the generic proof system that
is capable of handling algorithms with helping. This instance is based on
RGSep [26], which combines rely-guarantee reasoning [15] with separation logic
[21].

The main idea of the logic is to partition the state into several thread-local
parts (which can only be accessed by corresponding threads) and the shared
part (which can be accessed by all threads). The partitioning is defined by
proofs in the logic: an assertion in the code of a thread restricts its local
state and the shared state. In addition, the partitioning is dynamic, meaning
that resources, such as a part of a heap or a token, can be moved from the
local state of a thread into the shared state and vice versa. By transferring
a token to the shared state, a thread gives to its environment a permission to
change the abstract state. This allows us to reason about environment helping
that thread.

The RGSep-based view monoid. Similarly to DCSL, we assume that states
represent heaps, i.e. that ${\sf State}={\sf AState}={\sf
Loc}\rightharpoonup_{\rm fin}{\sf Val}\uplus\\{\lightning\\}$, and we denote
all states but a faulting one with ${\sf State}_{\sf H}={\sf AState}_{\sf
H}={\sf Loc}\rightharpoonup_{\rm fin}{\sf Val}$. We also assume a standard set
of heap-manipulating primitive commands with usual semantics.

We define views as triples consisting of three components: a predicate $P$ and
binary relations $R$ and $G$. A predicate $P\in\mathcal{P}(({\sf State}_{\sf
H}\times{\sf AState}_{\sf H}\times{\sf Tokens})^{2})$ is a set of pairs
$(l,s)$ of local and shared parts of the state, where each part consists of
concrete state, abstract state and tokens. Guarantee $G$ and rely $R$ are
relations from $\mathcal{P}(({\sf State}\times{\sf AState}\times{\sf
Tokens})^{2})$, which summarise how individual primitive commands executed by
the method’s thread (in case of $G$) and the environment (in case of $R$) may
change the shared state. Together guarantee and rely establish a protocol that
views of the method and its environment respectively must agree on each
other’s transitions, which allows us to reason about every thread separately
without considering local state of other threads, assuming that they follow
the protocol. The agreement is expressed with the help of a well-formedness
condition on views of the RGSep-based monoid that their predicates must be
stable under rely, meaning that their predicates take into account whatever
changes their environment can make:

${\sf stable}(P,R)\triangleq\forall l,s,s^{\prime}\ldotp(l,s)\in
P\land(s,s^{\prime})\in R\implies(l,s^{\prime})\in P.$

A predicate that is stable under rely cannot be invalidated by any state
transition from rely. Stable predicates with rely and guarantee relations form
the view monoid with the underlying set of views ${\sf Views}_{\sf
RGsep}=\\{(P,R,G)\mid{\sf stable}(P,R)\\}\cup\\{\bot\\},$ where $\bot$ denotes
a special inconsistent view with the empty reification. The reification of
other views simply joins shared and local parts of the state:

$\lfloor{(P,R,G)}\rfloor=\\{(\sigma_{l}\bullet\sigma_{s},\Sigma_{l}\bullet\Sigma_{s},\Delta_{l}\uplus\Delta_{s})\mid((\sigma_{l},\Sigma_{l},\Delta_{l}),(\sigma_{s},\Sigma_{s},\Delta_{s}))\in
P\\}.$

Let an operation $\cdot$ be defined on states analogously to DCSL. Given
predicates $P$ and $P^{\prime}$, we let $P\mathbin{*}P^{\prime}$ be a
predicate denoting the pairs of local and shared states in which the local
state can be divided into two substates such that one of them together with
the shared state satisfies $P$ and the other together with the shared state
satisfies $P^{\prime}$:

$P\mathbin{*}P^{\prime}\triangleq\\{((\sigma_{l}\bullet\sigma^{\prime}_{l},\Sigma_{l}\bullet\Sigma^{\prime}_{l},\Delta_{l}\uplus\Delta^{\prime}_{l}),s)\mid((\sigma_{l},\Sigma_{l},\Delta_{l}),s)\in
P\land((\sigma^{\prime}_{l},\Sigma^{\prime}_{l},\Delta^{\prime}_{l}),s)\in
P^{\prime}\\}$

We now define the monoid operation $\mathbin{*}$, which we use to compose
views of different threads. When composing views $(P,R,G)$ and
$(P^{\prime},R^{\prime},G^{\prime})$ of the parallel threads, we require
predicates of both to be immune to interference by all other threads and each
other. Otherwise, the result is inconsistent:

$(P,R,G)\mathbin{*}(P^{\prime},R^{\prime},G^{\prime})\triangleq\mbox{if
}G\subseteq R^{\prime}\land G^{\prime}\subseteq R\mbox{ then
}(P\mathbin{*}P^{\prime},R\cap R^{\prime},G\cup G^{\prime})\mbox{ else }\bot.$

That is, we let the composition of views be consistently defined when the
state transitions allowed in a guarantee of one thread are treated as
environment transitions in the other thread, i.e. $G\subseteq R^{\prime}$ and
$G^{\prime}\subseteq R$. The rely of the composition is $R\cap R^{\prime}$,
since the predicate $P*P^{\prime}$ is guaranteed to be stable only under
environment transitions described by both $R$ and $R^{\prime}$. The guarantee
of the composition is $G\cup G^{\prime}$, since other views need to take into
account all state transitions either from $G$ or from $G^{\prime}$.

$\vDash:({\sf State}\times{\sf AState}\times{\sf Tokens})\times({\sf
State}\times{\sf AState}\times{\sf Tokens})\times{\sf Int}\times{\sf Assn}$
$\begin{array}[]{l@{\ \
}l}((\sigma_{l},\Sigma_{l},\Delta_{l}),(\sigma_{s},\Sigma_{s},\Delta_{s}),{\bf
i})\models E\mathbin{\mapsto}F,&\mbox{iff }\sigma_{l}=[\llbracket
E\rrbracket_{\bf i}:\llbracket F\rrbracket_{\bf i}],\Sigma_{l}=[\ ],\mbox{ and
}\Delta_{l}=[\ ]\\\\[1.0pt]
((\sigma_{l},\Sigma_{l},\Delta_{l}),(\sigma_{s},\Sigma_{s},\Delta_{s}),{\bf
i})\models E\mathbin{\Mapsto}F,&\mbox{iff }\sigma_{l}=[\
],\Sigma_{l}=[\llbracket E\rrbracket_{\bf i}:\llbracket F\rrbracket_{\bf
i}],\mbox{ and }\Delta_{l}=[\ ]\\\\[1.0pt]
((\sigma_{l},\Sigma_{l},\Delta_{l}),(\sigma_{s},\Sigma_{s},\Delta_{s}),{\bf
i})\models\left[{\sf todo}({\rm A})\right]_{t},&\mbox{iff }\sigma_{l}=[\
],\Sigma_{l}=[\ ],\mbox{ and }\Delta_{l}=[t:{\sf todo}({\rm A})]\\\\[1.0pt]
((\sigma_{l},\Sigma_{l},\Delta_{l}),(\sigma_{s},\Sigma_{s},\Delta_{s}),{\bf
i})\models\left[{\sf done}({\rm A})\right]_{t},&\mbox{iff }\sigma_{l}=[\
],\Sigma_{l}=[\ ],\mbox{ and }\Delta_{l}=[t:{\sf done}({\rm A})]\\\\[1.0pt]
((\sigma_{l},\Sigma_{l},\Delta_{l}),(\sigma_{s},\Sigma_{s},\Delta_{s}),{\bf
i})\models\boxed{\pi},&\mbox{iff }\sigma_{l}=[\ ],\Sigma_{l}=[\
],\Delta_{l}=[\ ],\mbox{ and}\\\
&\hfill((\sigma_{s},\Sigma_{s},\Delta_{s}),([\ ],[\ ],[\ ]),{\bf
i})\models\pi\\\\[1.0pt]
((\sigma_{l},\Sigma_{l},\Delta_{l}),(\sigma_{s},\Sigma_{s},\Delta_{s}),{\bf
i})\models\pi*\pi^{\prime},&\mbox{iff there exist
}\sigma^{\prime}_{l},\sigma^{\prime\prime}_{l},\Sigma^{\prime}_{l},\Sigma^{\prime\prime}_{l},\Delta^{\prime}_{l},\Delta^{\prime\prime}_{l}\mbox{
such that}\\\
&\sigma_{l}=\sigma^{\prime}_{l}\bullet\sigma^{\prime\prime}_{l},\Sigma_{l}=\Sigma^{\prime}_{l}\bullet\Sigma^{\prime\prime}_{l},\Delta_{l}=\Delta^{\prime}_{l}\uplus\Delta^{\prime\prime}_{l},\\\
&((\sigma^{\prime}_{l},\Sigma^{\prime}_{l},\Delta^{\prime}_{l}),(\sigma_{s},\Sigma_{s},\Delta_{s}),{\bf
i})\models\pi,\mbox{ and }\\\
&((\sigma^{\prime\prime}_{l},\Sigma^{\prime\prime}_{l},\Delta^{\prime\prime}_{l}),(\sigma_{s},\Sigma_{s},\Delta_{s}),{\bf
i})\models\pi^{\prime}\end{array}$

Figure 4: Satisfaction relation for a fragment of the assertion language ${\sf
VAssn}$

The RGSep-based program logic. We define the view assertion language ${\sf
VAssn}$ that is a parameter of the proof system. Each view assertion $\rho$
takes form of a triple $(\pi,\mathcal{R},\mathcal{G})$, and the syntax for
$\pi$ is:

$\begin{array}[]{c c l}E&::=&a\mid X\mid E+E\mid\dots,\quad\mbox{where
}X\in{\sf LVar},a\in{\sf Val}\\\ \pi&::=&E=E\mid E\mathbin{\mapsto}E\mid
E\mathbin{\Mapsto}E\mid\left[{\sf todo}({\rm A})\right]_{t}\mid\left[{\sf
done}({\rm
A})\right]_{t}\mid\boxed{\pi}\mid\pi\mathbin{*}\pi\mid\neg\pi\mid\dots\\\
\end{array}$

Formula $\pi$ denotes a predicate of a view as defined by a satisfaction
relation $\models$ in Figure 4. There $E\mathbin{\mapsto}E$ and
$E\mathbin{\Mapsto}E$ denote a concrete and an abstract state describing
singleton heaps. A non-boxed formula $\pi$ denotes the view with the local
state satisfying $\pi$ and shared state unrestricted; $\boxed{\pi}$ denotes
the view with the empty local state and the shared state satisfying $\pi$;
$\pi\mathbin{*}\pi^{\prime}$ the composition of predicates corresponding to
$\pi$ and $\pi^{\prime}$. The semantics of the rest of connectives is
standard. Additionally, for simplicity of presentation of the syntax, we
require that boxed assertions $\boxed{\pi}$ be not nested (as opposed to
preventing that in the definition).

The other components $\mathcal{R}$ and $\mathcal{G}$ of a view assertion are
sets of rely/guarantee actions $\mathcal{A}$ with the syntax:
$\mathcal{A}::=\pi\leadsto\pi^{\prime}$. An action $\pi\leadsto\pi^{\prime}$
denotes a change of a part of the shared state that satisfies $\pi$ into one
that satisfies $\pi^{\prime}$, while leaving the rest of the shared state
unchanged. We associate with an action $\pi\leadsto\pi^{\prime}$ all state
transitions from the following set:

$\llbracket\pi\leadsto\pi^{\prime}\rrbracket=\\{((\sigma_{s}\bullet\sigma^{\prime\prime}_{s},\Sigma_{s}\bullet\Sigma^{\prime\prime}_{s},\Delta_{s}\uplus\Delta^{\prime\prime}_{s}),(\sigma^{\prime}_{s}\bullet\sigma^{\prime\prime}_{s},\Sigma^{\prime}_{s}\bullet\Sigma^{\prime\prime}_{s},\Delta^{\prime}_{s}\uplus\Delta^{\prime\prime}_{s}))\mid{}\\\
\exists{\bf i}\ldotp(([\ ],[\ ],[\ ]),(\sigma_{s},\Sigma_{s},\Delta_{s}),{\bf
i})\models\boxed{\pi}\land(([\ ],[\ ],[\
]),(\sigma^{\prime}_{s},\Sigma^{\prime}_{s},\Delta^{\prime}_{s}),{\bf
i})\models\boxed{\pi^{\prime}}\\}$

We give semantics to view assertions with the function
$\llbracket\cdot\rrbracket_{\cdot}$ that is defined as follows:

$\llbracket(\pi,\mathcal{R},\mathcal{G})\rrbracket_{{\bf
i}}\triangleq(\\{(l,s)\mid(l,s,{\bf
i})\models\pi\\},\bigcup\nolimits_{\mathcal{A}\in\mathcal{R}}\llbracket\mathcal{A}\rrbracket,\bigcup\nolimits_{\mathcal{A}\in\mathcal{G}}\llbracket\mathcal{A}\rrbracket).$

##  6 Example

⬇

1int L = 0, ${\tt k}$ = 0, ${\tt arg}$[N], ${\tt res}$[N]; \\\ initially all
${\tt res}[i]\neq{\tt nil}$

2

3$\mathrm{\ell}({\sf inc},a,r)$:

4 $\left\\{\begin{array}[]{l}{\sf global}*M(t)*\left[{\sf
todo}(\mathcal{L}({\sf inc},a,r))\right]_{t}\end{array}\right\\}$

5 ${\tt arg}$[mytid()] := $a$;

6 ${\tt res}$[mytid()] := ${\tt nil}$;

7 $\left\\{\begin{array}[]{l}{\sf global}*\boxed{{\sf true}*({\sf
task_{todo}}(t,a,r)\lor{\sf task_{done}}(t,a,r))}\end{array}\right\\}$

8 while (${\tt res}$[mytid()] = ${\tt nil}$):

9 if (CAS(&L, $0$, mytid())):

10 $\left\\{\begin{array}[]{l}\boxed{\&{{\tt
L}}\mathbin{\mapsto}t*\circledast_{j\in{\sf ThreadID}}\,{\sf
tinv}(j)}*\boxed{{\sf true}*({\sf task_{todo}}(t,a,r)\lor{\sf
task_{done}}(t,a,r))}*{\sf kinv}(\\_)\end{array}\right\\}$

11 for (i := 1; i $\leq$ N; ++i):

12 $\left\\{\begin{array}[]{l}\boxed{\&{{\tt
L}}\mathbin{\mapsto}t*\circledast_{j\in{\sf ThreadID}}\,{\sf tinv}(j)}*{\sf
kinv}(\\_)*{\sf LI}(i,t,a,r)\end{array}\right\\}$

13 if (${\tt res}$[i] = ${\tt nil}$):

14 $\left\\{\begin{array}[]{l}\exists V,A,R{.\,}{\sf kinv}(V)*{\sf
LI}(i,t,a,r)*{}\\\ \boxed{\&{{\tt L}}\mathbin{\mapsto}t*\circledast_{j\in{\sf
ThreadID}}\,{\sf tinv}(j)}*\boxed{{\sf true}*{\sf
task_{todo}}(i,A,R)}\end{array}\right\\}$

15 ${\tt k}$ := ${\tt k}$ + ${\tt arg}$[i];

16 $\left\\{\begin{array}[]{l}\exists V,A,R{.\,}\&{{\tt
k}}\mathbin{\mapsto}V+A*\&{{\tt K}}\mathbin{\Mapsto}V*{\sf LI}(i,t,a,r)*{}\\\
\boxed{\&{{\tt L}}\mathbin{\mapsto}t*\circledast_{j\in{\sf ThreadID}}\,{\sf
tinv}(j)}*\boxed{{\sf true}*{\sf task_{todo}}(i,A,R)}\end{array}\right\\}$

17 ${\tt res}$[i] := ${\tt k}$;

18 $\left\\{\begin{array}[]{l}\exists V,A,R{.\,}{\sf kinv}(V+A)*{\sf
LI}(i+1,t,a,r)*{}\\\ \boxed{\&{{\tt
L}}\mathbin{\mapsto}t*\circledast_{j\in{\sf ThreadID}}\,{\sf
tinv}(j)}*\boxed{{\sf true}*{\sf task_{done}}(i,A,R)}\end{array}\right\\}$

19 $\left\\{\begin{array}[]{l}\boxed{\&{{\tt
L}}\mathbin{\mapsto}t*\circledast_{j\in{\sf ThreadID}}\,{\sf
tinv}(j)}*\boxed{{\sf true}*{\sf task_{done}}(t,a,r)}*{\sf
kinv}(\\_)\end{array}\right\\}$

20 L = $0$;

21 assume(${\tt res}$[mytid()] = $r$);

22 $\left\\{\begin{array}[]{l}{\sf global}*M(t)*\left[{\sf
done}(\mathcal{L}({\sf inc},a,r))\right]_{t}\end{array}\right\\}$

Figure 5: Proof outline for a flat combiner of a concurrent increment.
Indentation is used for grouping commands.

In this section, we demonstrate how to reason about algorithms with helping
using relational views. We choose a simple library $\mathrm{\ell}$
implementing a concurrent increment and prove its linearizability with the
RGSep-based logic.

The concrete library $\mathrm{\ell}$ has one method ${\sf inc}$, which
increments the value of a shared counter ${\tt k}$ by the argument of the
method. The specification of $\mathrm{\ell}$ is given by an abstract library
$\mathcal{L}$. The abstract command, provided by $\mathcal{L}$ as an
implementation of ${\sf inc}$, operates with an abstract counter ${\tt K}$ as
follows (assuming that ${\tt K}$ is initialised by zero):

⬇

1$\mathcal{L}({\sf inc},a,r)$: < __kabs := __kabs + $a$; assume(__kabs ==
$r$); >

That is, $\mathcal{L}({\sf inc},a,r)$ atomically increments a counter and a
command ${\tt assume}({\tt K}==r)$, which terminates only if the return value
$r$ chosen at the invocation equals to the resulting value of ${\tt K}$. This
corresponds to how we specify methods’ return values in §4.

In Figure 5, we show the pseudo-code of the implementation of a method ${\sf
inc}$ in a C-style language along with a proof outline. The method
$\mathrm{\ell}({\sf inc},a,r)$ takes one argument, increments a shared counter
${\tt k}$ by it and returns the increased value of the counter. Since ${\tt
k}$ is shared among threads, they follow a protocol regulating the access to
the counter. This protocol is based on flat combining [11], which is a
synchronisation technique enabling a parallel execution of sequential
operations.

The protocol is the following. When a thread $t$ executes $\mathrm{\ell}({\sf
inc},a,r)$, it first makes the argument of the method visible to other threads
by storing it in an array ${\tt arg}$, and lets ${\tt res}[t]={\tt nil}$ to
signal to other threads its intention to execute an increment with that
argument. It then spins in the loop on line 8, trying to write its thread
identifier into a variable ${\tt L}$ with a compare-and-swap (CAS). Out of all
threads spinning in the loop, the one that succeeds in writing into ${\tt L}$
becomes a combiner: it performs the increments requested by all threads with
arguments stored in ${\tt arg}$ and writes the results into corresponding
cells of the array ${\tt res}$. The other threads keep spinning and
periodically checking the value of their cells in ${\tt res}$ until a
non-${\tt nil}$ value appears in it, meaning that a combiner has performed the
operation requested and marked it as finished. The protocol relies on the
assumption that ${\tt nil}$ is a value that is never returned by the method.
Similarly to the specification of the increment method, the implementation in
Figure 5 ends with a command ${\tt assume}({\tt res}[{\tt mytid}()]=r)$.

The proof outline features auxiliary assertions defined in Figure 6. In the
assertions we let $\\_$ denote a value or a logical variable whose name is
irrelevant. We assume that each program variable ${\tt var}$ has a unique
location in the heap and denote it with $\&{\tt var}$. Values $a$, $r$ and $t$
are used in the formulas and the code as constants.

We prove the following specification for $\mathrm{\ell}({\sf inc},a,r)$:

$\mathcal{R}_{t},\mathcal{G}_{t}\vdash_{t}\left\\{{\genfrac{}{}{0.0pt}{}{\displaystyle{\sf
global}*M(t)*}{\displaystyle\left[{\sf todo}(\mathcal{L}({\sf
inc},a,r))\right]_{t}}}\right\\}\,\mathrm{\ell}({\sf
inc},a,r)\,\left\\{{\genfrac{}{}{0.0pt}{}{\displaystyle{\sf
global}*M(t)*}{\displaystyle\left[{\sf done}(\mathcal{L}({\sf
inc},a,r))\right]_{t}}}\right\\}$

In the specification, $M(t)$ asserts the presence of ${\tt arg}[t]$ and ${\tt
res}[t]$ in the shared state, and ${\sf global}$ is an assertion describing
the shared state of all the threads. Thus, the pre- and postcondition of the
specification differ only by the kind of token given to $t$.

$\begin{array}[]{l c l}X\mathbin{\not\mapsto}Y&\triangleq&\exists
Y^{\prime}{.\,}X\mathbin{\mapsto}Y^{\prime}*Y\neq Y^{\prime}\\\\[1.0pt]
M(t)&\triangleq&\boxed{{\sf true}*(\&{{\tt
arg}[t]}\mathbin{\mapsto}\\_*\&{{\tt res}[t]}\mathbin{\not\mapsto}{\tt
nil})}\\\\[1.0pt] {\sf task_{todo}}(t,a,r)&\triangleq&\&{{\tt
arg}[t]}\mathbin{\mapsto}a*\&{{\tt res}[t]}\mathbin{\mapsto}{\tt
nil}*\left[{\sf todo}(\mathcal{L}({\sf inc},a,r))\right]_{t};\\\\[1.0pt] {\sf
task_{done}}(t,a,r)&\triangleq&\&{{\tt arg}[t]}\mathbin{\mapsto}a*\&{{\tt
res}[t]}\mathbin{\mapsto}r*r\not={\tt nil}*\left[{\sf done}(\mathcal{L}({\sf
inc},a,r))\right]_{t};\\\\[1.0pt] {\sf kinv}(V)&\triangleq&\&{{\tt
k}}\mathbin{\mapsto}V*\&{{\tt K}}\mathbin{\Mapsto}V\\\\[1.0pt] {\sf
LI}(i,t,a,r)&\triangleq&\boxed{\begin{array}[t]{l}{\sf true}*((t<i\land{\sf
task_{done}}(t,a,r))\lor{}\\\\[1.0pt] (t\geq i\land({\sf
task_{todo}}(t,a,r)\lor{\sf task_{done}}(t,a,r))))\end{array}}\\\\[1.0pt] {\sf
tinv}(i)&\triangleq&\&{{\tt arg}[i]}\mathbin{\mapsto}\\_*\&{{\tt
res}[i]}\mathbin{\Mapsto}\\_\lor{\sf task_{todo}}(i,\\_,\\_)\lor{\sf
task_{done}}(i,\\_,\\_)\\\\[1.0pt] {\sf global}&\triangleq&\boxed{(\&{{\tt
L}}\mathbin{\mapsto}0*{\sf kinv}(\\_)\lor\&{{\tt
L}}\mathbin{\not\mapsto}0)*\circledast_{j\in{\sf ThreadID}}\,{\sf
tinv}(j)},\end{array}$

Figure 6: Auxiliary predicates. $\circledast_{j\in{\sf ThreadID}}\,{\sf
tinv}(j)$ denotes ${\sf tinv}(1)\mathbin{*}{\sf
tinv}(2)\mathbin{*}\cdot\mathbin{*}{\sf tinv}(N)$

The main idea of the proof is in allowing a thread $t$ to share the ownership
of its token $\left[{\sf todo}(\mathcal{L}({\sf inc},a,r))\right]_{t}$ with
the other threads. This enables two possibilities for $t$. Firstly, $t$ may
become a combiner. Then $t$ has a linearization point on line 17 (when the
loop index $i$ equals to $t$). In this case $t$ also helps other concurrent
threads by performing their linearization points on line 17 (when $i\neq t$).
The alternative possibility is that some other thread becomes a combiner and
does a linearization point of $t$. Thus, the method has a non-fixed
linearization point, as it may occur in the code of a different thread.

We further explain how the tokens are transferred. On line 6 the method
performs the assignment res[mytid()] := nil, signalling to other threads about
a task this thread is performing. At this step, the method transfers its token
$\left[{\sf todo}(\mathcal{L}({\sf inc},a,r))\right]_{t}$ to the shared state,
as represented by the assertion $\boxed{{\sf true}*{\sf task_{todo}}(t,a,r)}$.
In order to take into consideration other threads interfering with $t$ and
possibly helping it, here and further we stabilise the assertion by adding a
disjunct ${\sf task_{done}}(t,a,r)$.

If a thread $t$ gets help from other threads, then ${\sf task_{done}}(t,a,r)$
holds, which implies that ${\tt res}[t]\neq{\tt nil}$ and $t$ cannot enter the
loop on line 8. Otherwise, if $t$ becomes a combiner, it transfers ${\sf
kinv}(\\_)$ from the shared state to the local state of $t$ to take over the
ownership of the counters ${\tt k}$ and ${\tt K}$ and thus ensure that the
access to the counter is governed by the mutual exclusion protocol. At each
iteration $i$ of the forall loop, res[i] = nil implies that ${\sf
task_{todo}}(i,\\_,\\_)$ holds, meaning that there is a token of a thread $i$
in the shared state. Consequently, on line 17 a thread $t$ may use it to
perform a linearization point of $i$.

The actions defining the guarantee relation $\mathcal{G}_{t}$ of a thread
$t^{\prime}$ are the following:

  1. 1.

$\&{{\tt arg}[t]}\mathbin{\mapsto}\\_*\&{{\tt
res}[t]}\mathbin{\not\mapsto}{\tt nil}\leadsto\&{{\tt
arg}[t]}\mathbin{\mapsto}a*\&{{\tt res}[t]}\mathbin{\not\mapsto}{\tt nil}$;

  2. 2.

$\&{{\tt arg}[t]}\mathbin{\mapsto}a*\&{{\tt res}[t]}\mathbin{\not\mapsto}{\tt
nil}\leadsto{\sf task_{todo}}(t,a,r)$;

  3. 3.

$\&{{\tt L}}\mathbin{\mapsto}0*{\sf kinv}(\\_)\leadsto\&{{\tt
L}}\mathbin{\mapsto}t$;

  4. 4.

$\&{{\tt L}}\mathbin{\mapsto}t*{\sf task_{todo}}(T,A,R)\leadsto\&{{\tt
L}}\mathbin{\mapsto}t*{\sf task_{done}}(T,A,R)$

  5. 5.

$\&{{\tt L}}\mathbin{\mapsto}t\leadsto\&{{\tt L}}\mathbin{\mapsto}0*{\sf
kinv}(\\_)$

  6. 6.

${\sf task_{done}}(t,a,r)\leadsto\&{{\tt arg}[t]}\mathbin{\mapsto}a*\&{{\tt
res}[t]}\mathbin{\mapsto}r$

Out of them, conditions 2 and 6 specify transfering the token of a thread $t$
to and from the shared state, and condition 4 describes using the shared token
of a thread $T$. The rely relation of a thread $t$ is then defined as the
union of all actions from guarantee relations of other threads and an
additional action for each thread $t^{\prime}\in{\sf
ThreadID}\setminus\\{t\\}$ allowing the client to prepare a thread
$t^{\prime}$ for a new method call by giving it a new token: $\left[{\sf
done}(\mathcal{L}({\sf inc},A,R))\right]_{t^{\prime}}\leadsto\left[{\sf
todo}(\mathcal{L}({\sf inc},A^{\prime},R^{\prime}))\right]_{t^{\prime}}$.

##  7 Related Work

There has been a significant amount of research on methods for proving
linearizability. Due to space constraints, we do not attempt a comprehensive
survey here (see [6]) and only describe the most closely related work.

The existing logics for linearizability that use linearization points differ
in the thread-modular reasoning method used and, hence, in the range of
concurrent algorithms that they can handle. Our goal in this paper was to
propose a uniform basis for designing such logics and to formalise the method
they use for reasoning about linearizability in a way independent of the
particular thread-modular reasoning method used. We have only shown
instantiations of our logic based on disjoint concurrent separation logic [20]
and RGSep [26]. However, we expect that our logic can also be instantiated
with more complex thread-modular reasoning methods, such as those based on
concurrent abstract predicates [4] or islands and protocols [25].

Our notion of tokens is based on the idea of treating method specifications as
resources when proving atomicity, which has appeared in various guises in
several logics [26, 18, 2]. Our contribution is to formalise this method of
handling linearization points independently from the underlying thread-modular
reasoning method and to formulate the conditions for soundly combining the two
(Definition 2, §3).

We have presented a logic that unifies the various logics based on
linearization points with helping. However, much work still remains as this
reasoning method cannot handle all algorithms. Some logics have introduced
speculative linearization points to increase their applicability [25, 18]; our
approach to helping is closely related to this, and we hope could be extended
to speculation. But there are still examples beyond this form of reasoning:
for instance there are no proofs of the Herlihy-Wing queue [14] using
linearization points (with helping and/or speculation). This algorithm can be
shown linearizable using forwards/backwards simulation [14] and more recently
has been shown to only require a backwards simulation [22]. But integrating
this form of simulation with the more intrincate notions of interference
expressible in the Views framework remains an open problem.

Another approach to proving linearizability is the aspect-oriented method.
This gives a series of properties of a queue [12] (or a stack [5])
implementation which imply that the implementation is linearizable. This
method been applied to algorithms that cannot be handled with standard
linearization-point-based methods. However, the aspect-oriented approach
requires a custom theorem per data structure, which limits its applicability.

In this paper we concentrated on linearizability in its original form [14],
which considers only finite computations and, hence, specifies only safety
properties of the library. Linearizability has since been generalised to also
specify liveness properties [9]. Another direction of future work is to
generalise our logic to handle liveness, possibly building on ideas from [19].

When a library is linearizable, one can use its atomic specification instead
of the actual implementation to reason about its clients [8]. Some logics
achieve the same effect without using linearizability, by expressing library
specifications as judgements in the logic rather than as the code of an
abstract library [16, 24, 23]. It is an interesting direction of future work
to determine a precise relationship between this method of specification and
linearizability, and to propose a generic logic unifying the two.

##  8 Conclusion

We have presented a logic for proving the linearizability of concurrent
libraries that can be instantiated with different methods for thread-modular
reasoning. To this end, we have extended the Views framework [3] to reason
about relations between programs. Our main technical contribution in this
regard was to propose the requirement for axiom soundness (Definition 2, §3)
that ensures a correct interaction between the treatment of linearization
points and the underlying thread-modular reasoning. We have shown that our
logic is powerful enough to handle concurrent algorithms with challenging
features, such as helping. More generally, our work marks the first step
towards unifying the logics for proving relational properties of concurrent
programs.

## References

  * [1] R. Bornat, C. Calcagno, P. W. O’Hearn, and M. J. Parkinson.  Permission accounting in separation logic.  In POPL, 2005.
  * [2] P. da Rocha Pinto, T. Dinsdale-Young, and P. Gardner.  TaDA: A logic for time and data abstraction.  In ECOOP, 2014.
  * [3] T. Dinsdale-Young, L. Birkedal, P. Gardner, M. J. Parkinson, and H. Yang.  Views: compositional reasoning for concurrent programs.  In POPL, 2013.
  * [4] T. Dinsdale-Young, M. Dodds, P. Gardner, M. J. Parkinson, and V. Vafeiadis.  Concurrent abstract predicates.  In ECOOP, 2010.
  * [5] M. Dodds, A. Haas, and C. M. Kirsch.  A scalable, correct time-stamped stack.  In POPL, New York, NY, USA, 2015.
  * [6] B. Dongol and J. Derrick.  Verifying linearizability: A comparative survey.  arXiv CoRR, 1410.6268, 2014.
  * [7] X. Feng.  Local rely-guarantee reasoning.  In POPL, 2009.
  * [8] I. Filipovic, P. W. O’Hearn, N. Rinetzky, and H. Yang.  Abstraction for concurrent objects.  Theoretical Computer Science, 2010.
  * [9] A. Gotsman and H. Yang.  Liveness-preserving atomicity abstraction.  In ICALP, 2011.
  * [10] A. Gotsman and H. Yang.  Linearizability with ownership transfer.  LMCS, 2013.
  * [11] D. Hendler, I. Incze, N. Shavit, and M. Tzafrir.  Flat combining and the synchronization-parallelism tradeoff.  In SPAA, 2010.
  * [12] T. A. Henzinger, A. Sezgin, and V. Vafeiadis.  Aspect-oriented linearizability proofs.  In CONCUR. 2013.
  * [13] M. Herlihy and N. Shavit.  The art of multiprocessor programming.  2008\.
  * [14] M. Herlihy and J. M. Wing.  Linearizability: A correctness condition for concurrent objects.  ACM TOPLAS, 1990.
  * [15] C. B. Jones.  Specification and design of (parallel) programs.  In IFIP Congress, 1983.
  * [16] R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal, and D. Dreyer.  Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning.  In POPL, 2015.
  * [17] A. Khyzha, A. Gotsman, and M. Parkinson.  A generic logic for proving linearizability (extended version).  Available from http://software.imdea.org/~artem/papers/rviews.pdf.
  * [18] H. Liang and X. Feng.  Modular verification of linearizability with non-fixed linearization points.  In PLDI, 2013.
  * [19] H. Liang, X. Feng, and Z. Shao.  Compositional verification of termination-preserving refinement of concurrent programs.  In LICS, 2014.
  * [20] P. W. O’Hearn.  Resources, concurrency, and local reasoning.  Theoretical Computer Science, 2007.
  * [21] P. W. O’Hearn, J. C. Reynolds, and H. Yang.  Local reasoning about programs that alter data structures.  In CSL, 2001.
  * [22] G. Schellhorn, H. Wehrheim, and J. Derrick.  How to prove algorithms linearisable.  In CAV. 2012.
  * [23] I. Sergey, A. Nanevski, and A. Banerjee.  Specifying and verifying concurrent algorithms with histories and subjectivity.  In ESOP, 2015.
  * [24] K. Svendsen and L. Birkedal.  Impredicative concurrent abstract predicates.  In ESOP, 2014.
  * [25] A. J. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, and D. Dreyer.  Logical relations for fine-grained concurrency.  In POPL, 2013.
  * [26] V. Vafeiadis.  Modular fine-grained concurrency verification.  PhD Thesis. Technical Report UCAM-CL-TR-726, University of Cambridge, 2008\.

##  Appendix 0.A Additional details of the RGSep-based logic

The unit $u_{\sf RGsep}$ does not restrict states and the allowed state
transitions of the environment, while disallowing any action in the current
thread:

$u_{\sf RGsep}=(\\{([\ ],[\ ],[\ ])\\}\times({\sf State}\times{\sf
AState}\times{\sf Tokens}),({\sf State}\times{\sf AState}\times{\sf
Tokens})^{2},\emptyset)$

Since action judgements are essential for reasoning about primitive commands
in our logic, we further refine conditions under which it holds of views from
the RGSep-based view monoid.

###### Proposition 8

The action judgement $\,{\sf\alpha}\Vdash_{t}\\{(P,R,G)\\}\\{(Q,R,G)\\}$
holds, if it is true that:

  * •

$\begin{multlined}\forall\sigma_{l},\sigma_{s},\sigma^{\prime}_{l},\sigma^{\prime}_{s},\Sigma_{l},\Sigma_{s},\Delta_{l},\Delta_{s}\ldotp((\sigma_{l},\Sigma_{l},\Delta_{l}),(\sigma_{s},\Sigma_{s},\Delta_{s}))\in
P\land{}\\\
\sigma^{\prime}_{l}\bullet\sigma^{\prime}_{s}\in\llbracket{\sf\alpha}\rrbracket_{t}(\sigma_{l}\bullet\sigma_{s})\implies\exists\Sigma^{\prime}_{l},\Sigma^{\prime}_{s},\Delta^{\prime}_{l},\Delta^{\prime}_{s}\ldotp((\sigma^{\prime}_{l},\Sigma^{\prime}_{l},\Delta^{\prime}_{l}),(\sigma^{\prime}_{s},\Sigma^{\prime}_{s},\Delta^{\prime}_{s}))\in
Q\land{}\\\
((\sigma_{s},\Sigma_{s},\Delta_{s}),(\sigma^{\prime}_{s},\Sigma^{\prime}_{s},\Delta^{\prime}_{s}))\in
G\land{\sf
LP}^{*}(\Sigma_{l}\bullet\Sigma_{s},\Delta_{l}\uplus\Delta_{s},\Sigma^{\prime}_{l}\bullet\Sigma^{\prime}_{s},\Delta^{\prime}_{l}\uplus\Delta^{\prime}_{s});\end{multlined}\forall\sigma_{l},\sigma_{s},\sigma^{\prime}_{l},\sigma^{\prime}_{s},\Sigma_{l},\Sigma_{s},\Delta_{l},\Delta_{s}\ldotp((\sigma_{l},\Sigma_{l},\Delta_{l}),(\sigma_{s},\Sigma_{s},\Delta_{s}))\in
P\land{}\\\
\sigma^{\prime}_{l}\bullet\sigma^{\prime}_{s}\in\llbracket{\sf\alpha}\rrbracket_{t}(\sigma_{l}\bullet\sigma_{s})\implies\exists\Sigma^{\prime}_{l},\Sigma^{\prime}_{s},\Delta^{\prime}_{l},\Delta^{\prime}_{s}\ldotp((\sigma^{\prime}_{l},\Sigma^{\prime}_{l},\Delta^{\prime}_{l}),(\sigma^{\prime}_{s},\Sigma^{\prime}_{s},\Delta^{\prime}_{s}))\in
Q\land{}\\\
((\sigma_{s},\Sigma_{s},\Delta_{s}),(\sigma^{\prime}_{s},\Sigma^{\prime}_{s},\Delta^{\prime}_{s}))\in
G\land{\sf
LP}^{*}(\Sigma_{l}\bullet\Sigma_{s},\Delta_{l}\uplus\Delta_{s},\Sigma^{\prime}_{l}\bullet\Sigma^{\prime}_{s},\Delta^{\prime}_{l}\uplus\Delta^{\prime}_{s});$

  * •

$\llbracket{\sf\alpha}\rrbracket_{t}(\sigma)\neq\lightning\implies\forall\sigma^{\prime}\ldotp\llbracket{\sf\alpha}\rrbracket_{t}(\sigma\bullet\sigma^{\prime})=\\{\sigma^{\prime\prime}\bullet\sigma^{\prime}\mid\sigma^{\prime\prime}\in\llbracket{\sf\alpha}\rrbracket_{t}(\sigma)\\}$.

The requirement to primitive commands in Proposition 8 is similar to that of
the action judgements. The difference is that in the RG-based proof system it
is not necessary to require ${\sf\alpha}$ to preserve any view $r$ of the
environment: since a predicate $P_{r}$ of any view $(P_{r},R_{r},G_{r})$ in
another thread is stable under $R_{r}$, it is also stable under $G\subseteq
R_{r}$ whenever $(P,R,G)\mathbin{*}(P_{r},R_{r},G_{r})$ is defined.
Consequently, views of the environment are never invalidated by local
transitions. Using the premise of Proposition 8 in Prim rule makes it closer
to the standard proof rule for the atomic step in Rely/Guarantee.

##  Appendix 0.B Compositionality properties of the safety relation

In this section, we formulate and prove compositionality properties of the
safety relation.

For further reference we restate the definition of a repartitioning
implication:

$p\Rrightarrow q\triangleq\forall
r{.\,}\lfloor{p*r}\rfloor\subseteq\lfloor{q*r}\rfloor.$ (5)

###### Lemma 9

The safety relation ${\sf safe}_{t}$ has the following closure properties:

  * •

Frame: $\forall t,C,p,q,r{.\,}{\sf safe}_{t}(p,C,q)\implies{\sf
safe}_{t}(p*r,C,q*r)$;

  * •

Choice: $\forall t,C_{1},C_{2},p,q{.\,}{\sf safe}_{t}(p,C_{1},q)\land{\sf
safe}_{t}(p,C_{2},q)\implies{\sf safe}_{t}(p,C_{1}\mathbin{+}C_{2},q)$;

  * •

Iter: $\forall t,C,p{.\,}{\sf safe}_{t}(p,C,p)\implies{\sf
safe}_{t}(p,{C}^{\star},p)$;

  * •

Seq: $\forall t,C_{1},C_{2},p,p^{\prime},q{.\,}{\sf
safe}_{t}(p,C_{1},p^{\prime})\land{\sf
safe}_{t}(p^{\prime},C_{2},q)\implies{\sf
safe}_{t}(p,C_{1}\mathbin{\,;\,}C_{2},q)$;

  * •

Conseq: $\forall t,C,p,p^{\prime},q,q^{\prime}{.\,}p^{\prime}\Rrightarrow
p\land{\sf safe}_{t}(p,C,q)\land q\Rrightarrow q^{\prime}\implies{\sf
safe}_{t}(p^{\prime},C,q^{\prime})$;

  * •

Disj: $\begin{multlined}\forall t,C,p_{1},p_{2},q_{1},q_{2}{.\,}{\sf
safe}_{t}(p_{1},C,q_{1})\land{\sf safe}_{t}(p_{2},C,q_{2})\implies{}\\\ {\sf
safe}_{t}(p_{1}\lor p_{2},C,q_{1}\lor q_{2}).\end{multlined}\forall
t,C,p_{1},p_{2},q_{1},q_{2}{.\,}{\sf safe}_{t}(p_{1},C,q_{1})\land{\sf
safe}_{t}(p_{2},C,q_{2})\implies{}\\\ {\sf safe}_{t}(p_{1}\lor
p_{2},C,q_{1}\lor q_{2}).$

We prove all of the properties by coinduction. To this end, we take the fixed-
point definition of ${\sf safe}_{t}$. We consider

$F_{t}:\mathcal{P}({\sf Views}\times{\sf Com}\times{\sf
Views})\to\mathcal{P}({\sf Views}\times{\sf Com}\times{\sf Views})$

defined as follows:

$\begin{array}[]{rcl}F_{t}(X)&\triangleq&\\{(p,C,q)\mid\forall
C^{\prime},{\sf\alpha}{.\,}C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}\implies\exists
p^{\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p^{\prime}\\}\land(p^{\prime},C^{\prime},q)\in
X\\}\\\ &&\hfill{}\cup\\{(p,{\sf skip},q)\mid p\Rrightarrow q\\}\end{array}$

Note that a powerset domain ordered by inclusion is a complete lattice and $F$
is a mapping on it, which means that $F$ is monotone. Consequently, by
Knaster-Tarski fixed-point theorem $F$ has the greatest fixed-point. It is
easy to see that ${\sf safe}_{t}\triangleq{\sf gfp}\,{F_{t}}$ in Definition 3.

In the proof of Lemma 9 we use the following properties of the action
judgement and the $\Rrightarrow$ relation.

######  Proposition 10 (Locality)

$\begin{array}[]{l}\forall p,q,r{.\,}p\Rrightarrow q\implies p*r\Rrightarrow
q*r;\\\ \forall
t,{\sf\alpha},p,q,r{.\,}\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{q\\}\implies\,{\sf\alpha}\Vdash_{t}\\{p*r\\}\\{q*r\\}.\end{array}$

######  Proposition 11 (Consequence)

$\forall t,{\sf\alpha},p,q,p^{\prime},q^{\prime}{.\,}p^{\prime}\Rrightarrow
p\land\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{q\\}\land q\Rrightarrow
q^{\prime}\implies\,{\sf\alpha}\Vdash_{t}\\{p^{\prime}\\}\\{q^{\prime}\\}.$

The proofs of Propositions 10 and 11 are straighforward: both properties can
be easily checked after unfolding definitions of action judgements.

######  Proposition 12 (Distributivity)

$\forall
t,{\sf\alpha},p_{1},p_{2},q_{1},q_{2}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p_{1}\\}\\{q_{1}\\}\land\,{\sf\alpha}\Vdash_{t}\\{p_{2}\\}\\{q_{2}\\}\implies\,{\sf\alpha}\Vdash_{t}\\{p_{1}\lor
p_{2}\\}\\{q_{1}\lor q_{2}\\}.$

###### Proof

According to the Definition 2 of the action judgement
$\,{\sf\alpha}\Vdash_{t}\\{p_{1}\lor p_{2}\\}\\{q_{1}\lor q_{2}\\}$, in order
to prove the latter we need to demonstrate the following:

$\forall
r,\sigma,\sigma^{\prime},\Sigma,\Delta{.\,}\sigma^{\prime}\in\llbracket{\sf\alpha}\rrbracket_{t}(\sigma)\land(\sigma,\Sigma,\Delta)\in\lfloor{(p_{1}\lor
p_{2})\mathbin{*}r}\rfloor\implies{}\\\
\exists\Sigma^{\prime},\Delta^{\prime}{.\,}{\sf
LP}^{*}(\Sigma,\Delta,\Sigma^{\prime},\Delta^{\prime})\land(\sigma^{\prime},\Sigma^{\prime},\Delta^{\prime})\in\lfloor{(q_{1}\lor
q_{2})\mathbin{*}r}\rfloor.$ (6)

Let us consider any view $r$, states $\sigma,\sigma^{\prime},\Sigma$ and
tokens $\Delta$ such that both
$\sigma^{\prime}\in\llbracket{\sf\alpha}\rrbracket_{t}(\sigma)$ and
$(\sigma,\Sigma,\Delta)\in\lfloor{(p_{1}\lor p_{2})\mathbin{*}r}\rfloor$ hold.
According to the properties of disjunction stated in equalities (1),

$\lfloor{(p_{1}\lor
p_{2})\mathbin{*}r}\rfloor=\lfloor{(p_{1}\mathbin{*}r)\lor(p_{2}\mathbin{*}r)}\rfloor=\lfloor{p_{1}\mathbin{*}r}\rfloor\cup\lfloor{p_{2}\mathbin{*}r}\rfloor.$

Consequently,
$(\sigma,\Sigma,\Delta)\in\lfloor{p_{1}\mathbin{*}r}\rfloor\cup\lfloor{p_{2}\mathbin{*}r}\rfloor$.

Let us assume that
$(\sigma,\Sigma,\Delta)\in\lfloor{p_{1}\mathbin{*}r}\rfloor$ (the other case
is analogous). Then according to the action judgement
$\,{\sf\alpha}\Vdash_{t}\\{p_{1}\\}\\{q_{1}\\}$, there exist $\Sigma^{\prime}$
and $\Delta^{\prime}$ such that:

${\sf
LP}^{*}(\Sigma,\Delta,\Sigma^{\prime},\Delta^{\prime})\land(\sigma^{\prime},\Sigma^{\prime},\Delta^{\prime})\in\lfloor{q_{1}\mathbin{*}r}\rfloor.$
(7)

Once again, according to the properties (1) of disjunction:

$\lfloor{q_{1}\mathbin{*}r}\rfloor\subseteq\lfloor{q_{1}\mathbin{*}r}\rfloor\cup\lfloor{q_{2}\mathbin{*}r}\rfloor=\lfloor{(q_{1}\mathbin{*}r)\lor(q_{2}\mathbin{*}r)}\rfloor=\lfloor{(q_{1}\lor
q_{2})\mathbin{*}r}\rfloor,$

which together with (7) means that
$(\sigma^{\prime},\Sigma^{\prime},\Delta^{\prime})\in\lfloor{(q_{1}\lor
q_{2})\mathbin{*}r}\rfloor$. Overall we have shown that there exist
$\Sigma^{\prime}$ and $\Delta^{\prime}$ such that ${\sf
LP}^{*}(\Sigma,\Delta,\Sigma^{\prime},\Delta^{\prime})$ and
$(\sigma^{\prime},\Sigma^{\prime},\Delta^{\prime})\in\lfloor{(q_{1}\lor
q_{2})\mathbin{*}r}\rfloor$, which concludes the proof of (6).

We now prove the closure properties from Lemma 9.

Proof of Frame. Let us define an auxiliary function:

$\phi(X,r)\triangleq\\{(p*r,C,q*r)\mid(p,C,q)\in X\\}.$

Then our goal is to prove that $\phi({\sf safe}_{t},r)\subseteq{\sf
safe}_{t}$. Since ${\sf safe}_{t}={\sf gfp}\,{F_{t}}$, we can do a proof by
coinduction: to conclude that $\phi({\sf safe}_{t},r)\subseteq{\sf safe}_{t}$
holds, we demonstrate $\phi({\sf safe}_{t},r)\subseteq F_{t}(\phi({\sf
safe}_{t},r))$.

Consider any $(p^{\prime},C,q^{\prime})\in\phi({\sf safe}_{t},r)$. There
necessarily are $p,q,r$ such that $p^{\prime}=p*r$, $q^{\prime}=q*r$ and
$(p,C,q)\in{\sf safe}_{t}$. Let us assume that $C={\sf skip}$. Then
$(p,C,q)\in{\sf safe}_{t}$ implies that $p\Rrightarrow q$. By Proposition 10,
$p*r\Rrightarrow q*r$, which implies $(p*r,{\sf skip},q*r)\in{\sf safe}_{t}$
to hold.

Now let $C\not={\sf skip}$. Since $(p,C,q)\in{\sf safe}_{t}$, by definition of
the safety relation the following holds of every ${\sf\alpha}$, $C^{\prime}$
and any transition $C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$:

$\exists
p^{\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p^{\prime}\\}\land(p^{\prime},C^{\prime},q)\in{\sf
safe}_{t}.$

By Proposition 10, $\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p^{\prime}\\}$ implies
$\,{\sf\alpha}\Vdash_{t}\\{p*r\\}\\{p^{\prime}*r\\}$. Also, when
$(p^{\prime},C^{\prime},q)\in{\sf safe}_{t}$, it is the case that
$(p^{\prime}*r,C^{\prime},q*r)\in\phi({\sf safe}_{t},r)$. Thus, we have shown
for every transition $C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$
that there exists $p^{\prime\prime}=p^{\prime}*r$ such that
$\,{\sf\alpha}\Vdash_{t}\\{p*r\\}\\{p^{\prime\prime}\\}$ and
$(p^{\prime\prime},C^{\prime},q*r)\in\phi({\sf safe}_{t},r)$:

$\forall{\sf\alpha},C{.\,}C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}\implies\exists
p^{\prime\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p*r\\}\\{p^{\prime\prime}\\}\land(p^{\prime\prime},C^{\prime},q*r)\in\phi({\sf
safe}_{t},r),$

which is sufficient to conclude that $(p*r,C,q*r)\in F_{t}(\phi({\sf
safe}_{t},r))$. ∎

Proof of Choice. Let us define an auxiliary function:

$\phi(X,Y)\triangleq\\{(p,C_{1}\mathbin{+}C_{2},q)\mid(p,C_{1},q)\in
X\land(p,C_{2},q)\in Y\\}.$

Then our goal is to prove that $\phi({\sf safe}_{t},{\sf
safe}_{t})\subseteq{\sf safe}_{t}$. For convenience, we prove an equivalent
inequality $\phi({\sf safe}_{t},{\sf safe}_{t})\cup{\sf safe}_{t}\subseteq{\sf
safe}_{t}$ instead.

Since ${\sf safe}_{t}={\sf gfp}\,{F_{t}}$, we can do a proof by coinduction:
to conclude that $\phi({\sf safe}_{t},{\sf safe}_{t})\cup{\sf
safe}_{t}\subseteq{\sf safe}_{t}$ holds, we demonstrate $\phi({\sf
safe}_{t},{\sf safe}_{t})\cup{\sf safe}_{t}\subseteq F_{t}(\phi({\sf
safe}_{t},{\sf safe}_{t})\cup{\sf safe}_{t})$.

Let us consider $(p,C,q)\in{\sf safe}_{t}$. Since ${\sf safe}_{t}={\sf
gfp}\,{F_{t}}$, we know that ${\sf safe}_{t}=F_{t}({\sf safe}_{t})$ holds.
Then by monotonicity of $F_{t}$, $(p,C,q)\in F_{t}({\sf safe}_{t})\subseteq
F_{t}(\phi({\sf safe}_{t},{\sf safe}_{t})\cup{\sf safe}_{t})$.

Now let us consider $(p,C,q)\in\phi({\sf safe}_{t},{\sf safe}_{t})$. There
necessarily are $C_{1}$ and $C_{2}$ such that $C=C_{1}\mathbin{+}C_{2}$,
$(p,C_{1},q)\in{\sf safe}_{t}$, and $(p,C_{2},q)\in{\sf safe}_{t}$. For
$(p,C_{1}\mathbin{+}C_{2},q)$ to belong to $F_{t}(\phi({\sf safe}_{t},{\sf
safe}_{t})\cup{\sf safe}_{t})$, the following has to be proven for every
transition
$C_{1}\mathbin{+}C_{2}\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$:

$\exists
p^{\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p^{\prime}\\}\land(p^{\prime},C^{\prime},q)\in\phi({\sf
safe}_{t},{\sf safe}_{t})\cup{\sf safe}_{t}.$ (8)

According to the rules of the operational semantics (Figure 1), whenever
$C_{1}\mathbin{+}C_{2}\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$,
necessarily ${\sf\alpha}={\sf id}$ and either $C^{\prime}=C_{1}$ or
$C^{\prime}=C_{2}$. Let us assume that $C^{\prime}=C_{1}$ (the other case is
analogous). The action judgement $\,{\sf id}\Vdash_{t}\\{p\\}\\{p\\}$ holds
trivially. Knowing that $(p,C_{1},q)\in{\sf safe}_{t}$, it is easy to see that
(8) can be satisfied by letting $p^{\prime}=p$. Consequently,
$(p,C_{1}\mathbin{+}C_{2},q)\in F_{t}(\phi({\sf safe}_{t},{\sf
safe}_{t})\cup{\sf safe}_{t})$, which concludes the proof. ∎

Proof of Disj. Let

$\phi(X)\triangleq\\{(p_{1}\lor p_{2},C,q_{1}\lor q_{2})\mid(p_{1},C,q_{1})\in
X\land(p_{2},C,q_{2})\in X\\}.$

Then our goal is to prove that $\phi({\sf safe}_{t})\subseteq{\sf safe}_{t}$.
Since ${\sf safe}_{t}={\sf gfp}\,{F_{t}}$, we can do a proof by coinduction:
to conclude that $\phi({\sf safe}_{t})\subseteq{\sf safe}_{t}$ holds, we
demonstrate $\phi({\sf safe}_{t})\subseteq F_{t}(\phi({\sf safe}_{t}))$.

Let us consider $(p,C,q)\in\phi({\sf safe}_{t})$. Then there necessarily are
$p_{1},q_{1},p_{2}$ and $q_{2}$ such that $p=p_{1}\lor p_{2}$, $q=q_{1}\lor
q_{2}$, and $(p_{1},C,q_{1}),(p_{2},C,q_{2})\in{\sf safe}_{t}$. From the
latter we get that for any ${\sf\alpha},C^{\prime}$ and a transition
$C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$ the following holds:

$\begin{array}[]{l}\exists
p^{\prime}_{1}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p_{1}\\}\\{p^{\prime}_{1}\\}\land(p^{\prime}_{1},C^{\prime},q_{1})\in{\sf
safe}_{t};\\\ \exists
p^{\prime}_{2}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p_{2}\\}\\{p^{\prime}_{2}\\}\land(p^{\prime}_{2},C^{\prime},q_{2})\in{\sf
safe}_{t}.\end{array}$

Then it is the case that $(p^{\prime}_{1}\lor
p^{\prime}_{2},C^{\prime},q_{1}\lor q_{2})\in\phi({\sf safe}_{t})$. Moreover,
$\,{\sf\alpha}\Vdash_{t}\\{p_{1}\lor p_{2}\\}\\{p^{\prime}_{1}\lor
p^{\prime}_{2}\\}$ holds by Proposition 12. Thus, we have shown for every
transition $C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$ that there
exists $p^{\prime}=p^{\prime}_{1}\lor p^{\prime}_{2}$ such that
$\,{\sf\alpha}\Vdash_{t}\\{p_{1}\lor p_{2}\\}\\{p^{\prime}\\}$ and
$(p^{\prime},C^{\prime},q_{1}\lor q_{2})\in\phi({\sf safe}_{t})$:

$\forall{\sf\alpha},C{.\,}C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}\implies\exists
p^{\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p_{1}\lor
p_{2}\\}\\{p^{\prime}\\}\land(p^{\prime},C^{\prime},q_{1}\lor
q_{2})\in\phi({\sf safe}_{t}).$

which is sufficient to conclude that $(p_{1}\lor p_{2},C,q_{1}\lor q_{2})\in
F_{t}(\phi({\sf safe}_{t}))$. ∎

Proof of Iter. To do a proof by coinduction, we strengthen Iter property as
follows:

$\forall p,C{.\,}((p,C,p)\in{\sf safe}_{t}\implies(p,{C}^{\star},p)\in{\sf
safe}_{t})\land{}\\\ (\forall p_{1},C_{1}{.\,}(p_{1},C_{1},p)\in{\sf
safe}_{t}\land(p,C,p)\in{\sf
safe}_{t}\implies(p_{1},C_{1}\mathbin{\,;\,}{C}^{\star},p)\in{\sf safe}_{t}).$
(9)

Let us define auxilliary functions:

$\displaystyle\phi(X)\triangleq\\{(p,{C}^{\star},p)\mid(p,C,p)\in X\\}$
$\displaystyle\psi(X)\triangleq\\{(p_{1},C_{1}\mathbin{\,;\,}{C}^{\star}_{2},p_{2})\mid(p_{1},C_{1},p_{2}),(p_{2},C_{2},p_{2})\in
X\\}.$

Using them, we rewrite (9) as $\phi({\sf safe}_{t})\cup\psi({\sf
safe}_{t})\subseteq{\sf safe}_{t}$. Let $\xi=\\{(p,{\sf skip},p)\\}$. It is
easy to see that $\phi({\sf safe}_{t})\cup\psi({\sf
safe}_{t})\cup\xi\subseteq{\sf safe}_{t}$ is also an equivalent reformulation
of (9), since $\xi\subseteq{\sf safe}_{t}$ always holds.

Since ${\sf safe}_{t}={\sf gfp}\,{F_{t}}$, we can do a proof by coinduction:
to conclude that $\phi({\sf safe}_{t})\cup\psi({\sf
safe}_{t})\cup\xi\subseteq{\sf safe}_{t}$, we demonstrate $\phi({\sf
safe}_{t})\cup\psi({\sf safe}_{t})\cup\xi\subseteq F_{t}(\phi({\sf
safe}_{t})\cup\psi({\sf safe}_{t})\cup\xi)$.

Consider any $(p,C,q)\in\xi$. Necessarily, $C={\sf skip}$ and $q=p$. Note that
$p\Rrightarrow p$ always holds, which by definition of $F_{t}$ is sufficient
for $(p,{\sf skip},p)\in F_{t}(\phi({\sf safe}_{t})\cup\psi({\sf
safe}_{t})\cup\xi)$. Thus, $(p,C,q)\in F_{t}(\phi({\sf safe}_{t})\cup\psi({\sf
safe}_{t})\cup\xi)$.

Consider any $(p,C^{\prime},q)\in\phi({\sf safe}_{t})$. Necessarily, $p=q$ and
there exists a sequential command $C$ such that $C^{\prime}={C}^{\star}$ and
$(p,C,p)\in{\sf safe}_{t}$. We need to show that $(p,{C}^{\star},p)\in
F_{t}(\phi({\sf safe}_{t})\cup\psi({\sf safe}_{t})\cup\xi)$. For the latter to
hold, by definition of $F_{t}$ it is sufficient that for every ${\sf\alpha}$,
$C^{\prime\prime}$ and a transition
$C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime\prime}$ the following
be true:

$\exists
p^{\prime\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p^{\prime\prime}\\}\land(p^{\prime\prime},C^{\prime\prime},p)\in\phi({\sf
safe}_{t})\cup\psi({\sf safe}_{t})\cup\xi.$ (10)

According to the operational semantics in Figure 1, when there is a transition
$C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime\prime}$, necessarily
${\sf\alpha}={\sf id}$ and either $C^{\prime\prime}={\sf skip}$ or
$C^{\prime\prime}=C\mathbin{\,;\,}{C}^{\star}$. Let us assume that
$C^{\prime\prime}={\sf skip}$. Since both $(p,{\sf skip},p)\in\xi$ and
$\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p\\}$ always hold, it is easy to see that
letting $p^{\prime\prime}=p$ satisfies (10). Now let us turn to the case when
$C^{\prime\prime}=C\mathbin{\,;\,}{C}^{\star}$. Note that
$(p,C\mathbin{\,;\,}{C}^{\star},p)\in\psi({\sf safe}_{t})$ holds by definition
of $\psi$. Thus, by letting $p^{\prime\prime}=p$ we satisfy (10).

Consider $(p_{1},C_{0},p_{2})\in\psi({\sf safe}_{t})$. Necessarily, there
exist $C_{1}$ and $C_{2}$ such that:

$C_{0}=C_{1}\mathbin{\,;\,}{C}^{\star}_{2}\land(p_{1},C_{1},p_{2})\in{\sf
safe}_{t}\land(p_{2},C_{2},p_{2})\in{\sf safe}_{t}.$ (11)

We need to show that $(p_{1},C_{1}\mathbin{\,;\,}{C}^{\star}_{2},p_{2})\in
F_{t}(\phi({\sf safe}_{t})\cup\psi({\sf safe}_{t})\cup\xi)$. For the latter to
hold, we need to prove the following for every ${\sf\alpha}$, $C^{\prime}$ and
a transition
$C_{1}\mathbin{\,;\,}{C}^{\star}_{2}\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$:

$\exists
p^{\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p_{1}\\}\\{p^{\prime}\\}\land(p^{\prime},C^{\prime},p_{2})\in\phi({\sf
safe}_{t})\cup\psi({\sf safe}_{t})\cup\xi.$ (12)

According to the operational semantics in Figure 1, when there is a transition
$C_{1}\mathbin{\,;\,}{C}^{\star}_{2}\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$,
either of the following is true:

  * •

there are $C^{\prime}_{1}$ and a transition
$C_{1}\mathrel{{\xlongrightarrow{C}}{}}C^{\prime}_{1}$ such that
$C^{\prime}=C^{\prime}_{1}\mathbin{\,;\,}{C}^{\star}_{2}$;

  * •

$C_{1}={\sf skip}$, $C^{\prime}=C_{2}$ and ${\sf\alpha}={\sf id}$.

Let us assume that the former is the case. From (11) we know that
$(p_{1},C_{1},p_{2})\in{\sf safe}_{t}$, so by definition of the safety
relation we get that:

$\exists
p^{\prime}_{1}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p_{1}\\}\\{p^{\prime}_{1}\\}\land(p^{\prime}_{1},C^{\prime}_{1},p_{2})\in{\sf
safe}_{t}.$

Consequently,
$(p^{\prime}_{1},C^{\prime}_{1}\mathbin{\,;\,}{C}^{\star}_{2},p_{2})\in\psi({\sf
safe}_{t})$. Thus, by letting $p^{\prime}=p^{\prime}_{1}$ we can satisfy (12).

Now let $C_{1}={\sf skip}$ and ${\sf\alpha}={\sf id}$. From (11) we know that
$(p_{1},{\sf skip},p_{2})\in{\sf safe}_{t}$, meaning that necessarily
$p_{1}\Rrightarrow p_{2}$. It is easy to see that $p_{1}\Rrightarrow p_{2}$
holds if and only if so does $\,{\sf id}\Vdash_{t}\\{p_{1}\\}\\{p_{2}\\}$.
Knowing that $(p_{2},C_{2},p_{2})\in{\sf safe}_{t}$, we can satisfy (12) by
letting $p^{\prime}=p_{2}$. ∎

Proof of Seq. Let

$\phi(X,q^{\prime})\triangleq\\{(p,C_{1}\mathbin{\,;\,}C_{2},q)\mid(p,C_{1},q^{\prime})\in
X\land(q^{\prime},C_{2},q)\in X\\}.$

Then our goal is to prove that $\phi({\sf safe}_{t},q^{\prime})\subseteq{\sf
safe}_{t}$. For convenience, we prove an equivalent inequality $\phi({\sf
safe}_{t},q^{\prime})\cup{\sf safe}_{t}\subseteq{\sf safe}_{t}$ instead.

Since ${\sf safe}_{t}={\sf gfp}\,{F_{t}}$, we can do a proof by coinduction:
to conclude that $\phi({\sf safe}_{t},q^{\prime})\cup{\sf
safe}_{t}\subseteq{\sf safe}_{t}$ holds, we demonstrate $\phi({\sf
safe}_{t},q^{\prime})\cup{\sf safe}_{t}\subseteq F_{t}(\phi({\sf
safe}_{t},q^{\prime})\cup{\sf safe}_{t})$.

Let us consider any $(p,C,q)\in{\sf safe}_{t}$. Since ${\sf safe}_{t}={\sf
gfp}\,{F_{t}}$, we know that ${\sf safe}_{t}=F_{t}({\sf safe}_{t})$ holds.
Then by monotonicity of $F_{t}$, $p,C,q)\in F_{t}({\sf safe}_{t})\subseteq
F_{t}(\phi({\sf safe}_{t},{\sf safe}_{t})\cup{\sf safe}_{t})$.

Now let us consider any $(p,C,q)\in\phi({\sf safe}_{t},q^{\prime})$. There
necessarily are $C_{1}$ and $C_{2}$ such that:

$C=C_{1}\mathbin{\,;\,}C_{2}\land(p,C_{1},q^{\prime})\in{\sf
safe}_{t}\land(q^{\prime},C_{2},q)\in{\sf safe}_{t}.$ (13)

For $(p,C_{1}\mathbin{\,;\,}C_{2},q)$ to belong to $F_{t}(\phi({\sf
safe}_{t},{\sf safe}_{t})\cup{\sf safe}_{t})$, the following has to be the
case for every transition
$C_{1}\mathbin{\,;\,}C_{2}\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$:

$\exists
p^{\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p^{\prime}\\}\land(p^{\prime},C^{\prime},q)\in\phi({\sf
safe}_{t},q^{\prime})\cup{\sf safe}_{t}.$ (14)

According to the rules of the operational semantics (Figure 1), when there is
a transition
$C_{1}\mathbin{\,;\,}C_{2}\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$,
either of the following is true:

  * •

there exists $C^{\prime}_{1}$ such that
$C^{\prime}=C^{\prime}_{1}\mathbin{\,;\,}C_{2}$ and
$C_{1}\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}_{1}$; or

  * •

$C_{1}={\sf skip}$, ${\sf\alpha}={\sf id}$ and $C^{\prime}=C_{2}$.

Let us assume that the former is the case. From (13) we know that
$(p,C_{1},q^{\prime})\in{\sf safe}_{t}$, which means that the following holds
of $C_{1}\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}_{1}$:

$\exists
p^{\prime\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p^{\prime\prime}\\}\land(p^{\prime\prime},{\sf\alpha}^{\prime}_{1},q^{\prime})\in{\sf
safe}_{t}.$

When $(p^{\prime\prime},{\sf\alpha}^{\prime}_{1},q^{\prime})\in{\sf safe}_{t}$
and $(q^{\prime},{\sf\alpha}_{2},q)\in{\sf safe}_{t}$, it is the case that
$(p^{\prime\prime},{\sf\alpha}^{\prime}_{1}\mathbin{\,;\,}{\sf\alpha}_{2},q)\in\phi({\sf
safe}_{t},q^{\prime})$. Thus, by letting $p^{\prime}=p^{\prime\prime}$ we
satisfy (14).

We now consider the case when $C_{1}={\sf skip}$, ${\sf\alpha}={\sf id}$ and
$C^{\prime}=C_{2}$. From (13) we know that $(p,{\sf skip},q^{\prime})\in{\sf
safe}_{t}$, meaning that $p\Rrightarrow q^{\prime}$, or equivalently $\,{\sf
id}\Vdash_{t}\\{p\\}\\{q^{\prime}\\}$. We also know from (13) that
$(q^{\prime},C_{2},q)\in{\sf safe}_{t}$. Thus, (14) can be satisfied by
letting $p^{\prime}=q^{\prime}$. ∎

Proof of Conseq. Let us first show that ${\sf safe}_{t}(p^{\prime},C,q)$
holds, when so do $p^{\prime}\Rrightarrow p$ and ${\sf safe}_{t}(p,C,q)$. When
$C={\sf skip}$, ${\sf safe}_{t}(p,C,q)$ gives us that $p\Rrightarrow q$. It is
easy to see that $p^{\prime}\Rrightarrow p$ and $p\Rrightarrow q$ together
imply $p^{\prime}\Rrightarrow q$, which is sufficient to conclude that ${\sf
safe}_{t}(p^{\prime},C,q)$ holds. Let us assume that $C\not={\sf skip}$. From
${\sf safe}_{t}(p,C,q)$ we get that the following holds of every transition
$C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$:

$\exists
p^{\prime\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p^{\prime\prime}\\}\land{\sf
safe}_{t}(p^{\prime\prime},C^{\prime},q)$

However, by applying Proposition 11 about Consequence property of axiom
judgements to $p^{\prime}\Rrightarrow p$ and
$\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p^{\prime\prime}\\}$ we get that
$\,{\sf\alpha}\Vdash_{t}\\{p^{\prime}\\}\\{p^{\prime\prime}\\}$. Together with
the formula above, it allows us to conclude that ${\sf
safe}_{t}(p^{\prime},C,q)$ holds.

Now let us prove that ${\sf safe}_{t}(p,C,q^{\prime})$ holds, when so do
$q\Rrightarrow q^{\prime}$ and ${\sf safe}_{t}(p,C,q)$. We define an
auxilliary function:

$\phi(X,q)\triangleq\\{(p,C,q^{\prime})\mid(p,C,q)\in X\land q\Rrightarrow
q^{\prime}\\}.$

Our goal is to prove that $\phi({\sf safe}_{t},q)\subseteq{\sf safe}_{t}$.
Since ${\sf safe}_{t}={\sf gfp}\,{F_{t}}$, we can do a proof by coinduction:
to conclude that $\phi({\sf safe}_{t},q)\subseteq{\sf safe}_{t}$ holds, we
demonstrate $\phi({\sf safe}_{t},q)\subseteq F_{t}(\phi({\sf safe}_{t},q))$.

Let us consider any $(p,C,q^{\prime})\in\phi({\sf safe}_{t},q)$. Necessarily,
$(p,C,q)\in{\sf safe}_{t}$ and $q\Rrightarrow q^{\prime}$. When $C={\sf
skip}$, we need to show that $p\Rrightarrow q^{\prime}$. Since $(p,{\sf
skip},q)\in{\sf safe}_{t}$, it is the case that $p\Rrightarrow q$. It is easy
to see that $p\Rrightarrow q$ and $q\Rrightarrow q^{\prime}$ together imply
$p\Rrightarrow q^{\prime}$, which is sufficient to conclude that
$(p,C,q^{\prime})\in F_{t}(\phi({\sf safe}_{t},q))$.

Now consider the case when $C\not={\sf skip}$. Since $(p,{\sf\alpha},q)\in{\sf
safe}_{t}$, by definition of the safety relation the following holds of every
${\sf\alpha}$, $C^{\prime}$ and a transition
$C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$:

$\exists
p^{\prime\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p^{\prime\prime}\\}\land(p^{\prime\prime},C^{\prime},q)\in{\sf
safe}_{t}$

Knowing that $q\Rrightarrow q^{\prime}$ and
$(p^{\prime\prime},C^{\prime},q)\in{\sf safe}_{t}$, it is easy to see that
$(p^{\prime\prime},C^{\prime},q^{\prime})\in\phi({\sf safe}_{t},q)$. Thus, we
have shown that:

$\forall{\sf\alpha},C^{\prime}{.\,}C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}\implies\exists
p^{\prime\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{p\\}\\{p^{\prime\prime}\\}\land(p^{\prime\prime},C^{\prime},q^{\prime})\in\phi({\sf
safe}_{t},q),$

which is sufficient for $(p,C,q^{\prime})\in F_{t}(\phi({\sf safe}_{t},q))$ to
hold. ∎

##  Appendix 0.C Proof of Lemma 4

Lemma. $\forall
t,\mathcal{P},C,\mathcal{Q}{.\,}\vdash_{t}\left\\{{\mathcal{P}}\right\\}\,C\,\left\\{{\mathcal{Q}}\right\\}\implies\forall{\bf
i}{.\,}{\sf safe}_{t}(\llbracket\mathcal{P}\rrbracket_{{\bf
i}},C,\llbracket\mathcal{Q}\rrbracket_{{\bf i}}).$

We prove Lemma 4 by rule induction. For that we choose arbitrary thread
identifier $t$ and demonstrate that $\forall{\bf i}{.\,}{\sf
safe}_{t}(\llbracket\mathcal{P}\rrbracket_{{\bf
i}},C,\llbracket\mathcal{Q}\rrbracket_{{\bf i}})$ is closed under the proof
rules from Figure 3. The cases of Choice, Iter, Seq, Conseq, Frame and Disj
rules are straightforward: they trivially follow from Lemma 9 after using the
properties of $\llbracket-\rrbracket_{{\bf i}}$ from Figure 2. The Ex rule
uses the fact that ${\sf Val}$, which is the range of $i$, is finite, which
makes possible proving it just like the Disj rule.

It remains to consider the Prim rule to conclude Lemma 4. Let us assume that
$\forall{\bf
i}^{\prime}{.\,}\,{\sf\alpha}\Vdash_{t}\\{\llbracket\mathcal{P}\rrbracket_{{\bf
i}^{\prime}}\\}\\{\llbracket\mathcal{Q}\rrbracket_{{\bf i}^{\prime}}\\}$
holds. We need to demonstrate that so does $\forall{\bf i}{.\,}{\sf
safe}_{t}(\llbracket\mathcal{P}\rrbracket_{{\bf
i}},{\sf\alpha},\llbracket\mathcal{Q}\rrbracket_{{\bf i}})$. To conclude that
the latter holds, according Definition 3 we need to prove the following for
every ${\bf i}$:

$\forall
C^{\prime},{\sf\alpha}^{\prime}{.\,}{\sf\alpha}\mathrel{{\xlongrightarrow{{\sf\alpha}^{\prime}}}{}}C^{\prime}\implies\exists
p^{\prime}{.\,}\,{\sf\alpha}^{\prime}\Vdash_{t}\\{\llbracket\mathcal{P}\rrbracket_{{\bf
i}}\\}\\{p^{\prime}\\}\land{\sf
safe}_{t}(p^{\prime},C^{\prime},\llbracket\mathcal{Q}\rrbracket_{{\bf i}})$
(15)

According to the operational semantics from Figure 1, the only transition from
a command ${\sf\alpha}$ is
${\sf\alpha}\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}{\sf skip}$. Thus, in
the formula above ${\sf\alpha}^{\prime}={\sf\alpha}$ and $C^{\prime}={\sf
skip}$. Note that ${\sf safe}_{t}(\llbracket\mathcal{Q}\rrbracket_{{\bf
i}},{\sf skip},\llbracket\mathcal{Q}\rrbracket_{{\bf i}})$ holds trivially.
Additionally, by our assumption,
$\,{\sf\alpha}\Vdash_{t}\\{\llbracket\mathcal{P}\rrbracket_{{\bf
i}^{\prime}}\\}\\{\llbracket\mathcal{Q}\rrbracket_{{\bf i}^{\prime}}\\}$ holds
for any ${\bf i}^{\prime}$. Consequently, it holds for ${\bf i}^{\prime}={\bf
i}$. We conclude that by letting
$p^{\prime}=\llbracket\mathcal{Q}\rrbracket_{{\bf i}}$ we satisfy (15).

∎

##  Appendix 0.D Proof of Theorem 7

We further refer to the assumptions of Theorem 7 as a relation ${\sf
safelib}(\mathrm{\ell},\mathcal{L},\mathcal{P},\mathcal{Q})$ defined as
follows.

###### Definition 13

Given a concrete library $\mathrm{\ell}$, an abstract library $\mathcal{L}$
and $\mathcal{P},\mathcal{Q}:{\sf ThreadID}\times{\sf APCom}\to{\sf VAssn}$,
we say that a relation ${\sf
safelib}(\mathrm{\ell},\mathcal{L},\mathcal{P},\mathcal{Q})$ holds if and only
if the following requirements are met:

  1. 1.

${\sf dom}(\mathrm{\ell})={\sf dom}(\mathcal{L})$;

  2. 2.

$\forall{\bf i},t,{\rm
A},\sigma,\Sigma,\Delta,r{.\,}(\sigma,\Sigma,\Delta)\in\lfloor{\llbracket\mathcal{P}(t,{\rm
A})\rrbracket_{{\bf i}}\mathbin{*}r}\rfloor\implies\Delta(t)={\sf todo}({\rm
A})$;

  3. 3.

$\forall{\bf i},t,{\rm
A},\sigma,\Sigma,\Delta,r{.\,}(\sigma,\Sigma,\Delta)\in\lfloor{\llbracket\mathcal{Q}(t,{\rm
A})\rrbracket_{{\bf i}}\mathbin{*}r}\rfloor\implies\Delta(t)={\sf done}({\rm
A})$;

  4. 4.

$\begin{multlined}\forall{\bf i},t,{\rm A},{\rm
A}^{\prime},r,\Delta{.\,}((\sigma,\Sigma,\Delta[t:{\sf todo}({\rm
A})])\in\lfloor{\llbracket\mathcal{P}(t,{\rm A})\rrbracket_{{\bf
i}}\mathbin{*}r}\rfloor\iff{}\\\ (\sigma,\Sigma,\Delta[t:{\sf done}({\rm
A}^{\prime})])\in\lfloor{\llbracket\mathcal{Q}(t,{\rm
A}^{\prime})\rrbracket_{{\bf
i}}\mathbin{*}r}\rfloor).\end{multlined}\forall{\bf i},t,{\rm A},{\rm
A}^{\prime},r,\Delta{.\,}((\sigma,\Sigma,\Delta[t:{\sf todo}({\rm
A})])\in\lfloor{\llbracket\mathcal{P}(t,{\rm A})\rrbracket_{{\bf
i}}\mathbin{*}r}\rfloor\iff{}\\\ (\sigma,\Sigma,\Delta[t:{\sf done}({\rm
A}^{\prime})])\in\lfloor{\llbracket\mathcal{Q}(t,{\rm
A}^{\prime})\rrbracket_{{\bf i}}\mathbin{*}r}\rfloor).$

  5. 5.

$\begin{multlined}\forall m,a,r,t{.\,}m\in{\sf dom}(\mathrm{\ell})\land
a,r\in{\sf Val}\land t\in{\sf ThreadID}\implies{}\\\
\vdash_{t}\left\\{{\mathcal{P}(t,\mathcal{L}(m,a,r))}\right\\}\,\mathrm{\ell}(m,a,r)\,\left\\{{\mathcal{Q}(t,\mathcal{L}(m,a,r))}\right\\};\end{multlined}\forall
m,a,r,t{.\,}m\in{\sf dom}(\mathrm{\ell})\land a,r\in{\sf Val}\land t\in{\sf
ThreadID}\implies{}\\\
\vdash_{t}\left\\{{\mathcal{P}(t,\mathcal{L}(m,a,r))}\right\\}\,\mathrm{\ell}(m,a,r)\,\left\\{{\mathcal{Q}(t,\mathcal{L}(m,a,r))}\right\\};$

To strengthen the statement of Theorem 7 as necessary for its proof, we define
an auxilliary relation, a thread pool invariant. With this relation we
establish a correspondence between the information about LP in a thread $t$
from a given view $v_{t}$ and sequential commands in a thread $t$ of a
concrete thread pool $\tau$ and abstract thread pool $\mathcal{T}$.

###### Definition 14

Given a concrete library $\mathrm{\ell}$, an abstract library $\mathcal{L}$,
predicates $\mathcal{P},\mathcal{Q}:{\sf ThreadID}\times{\sf APCom}\to{\sf
VAssn}$, a concrete thread pool $\tau$, an abstract thread pool $\mathcal{T}$,
a view $v_{t}$ and an interpretation of logical variables ${\bf i}$, we say
that a thread pool invariant ${\sf inv}_{t}({\bf
i},\tau,\mathcal{T},v_{t},\Delta)$ holds in a thread $t$ if and only if the
following requirements are met:

  * •

if $\tau(t)={\sf idle}$, then $\mathcal{T}(t)={\sf idle}$ and
$v_{t}\Rrightarrow\llbracket\mathcal{Q}(t,\\_)\rrbracket_{{\bf i}}$, or

  * •

there exist $C,r,m,a$ such that $\tau(t)=(C,r)$ and the following holds:

${\sf
safe}_{t}(v_{t},C,\mathcal{Q}(t,\mathcal{L}(m,a,r)))\land((\Delta(t)={\sf
todo}(\mathcal{L}(m,a,r))\land\mathcal{T}(t)=(\mathcal{L}(m,a,r),r))\lor{}\\\
(\Delta(t)={\sf done}(\mathcal{L}(m,a,r))\land\mathcal{T}(t)=({\sf
skip},r))).$

Finally, analogously to Definition 5, we write down formally a definition of
the set of histories of abstract libraries.

###### Definition 15

We define $\mathcal{H}_{n}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket$
as a set of histories such that
$\mathcal{H}_{0}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket\triangleq\\{\varepsilon\\}$
and:

$\begin{array}[]{rcl}\mathcal{H}_{n}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket&\triangleq&\\{((t,{\sf
call}\ m(a))::h)\mid m\in{\sf dom}(\mathcal{L})\land\mathcal{T}(t)={\sf
idle}\land{}\\\ &&\hfill\exists
r{.\,}h\in\mathcal{H}_{n-1}\llbracket\mathcal{L},\mathcal{T}[t:(\mathcal{L}(m,a,r),r)],\Sigma\rrbracket\\}\\\
&&{}\cup\\{h\mid\exists t,{\rm A},\Sigma^{\prime},r{.\,}\mathcal{T}(t)=({\rm
A},r)\land\Sigma^{\prime}\in\llbracket{\rm A}\rrbracket_{t}(\Sigma)\land{}\\\
&&\hfill h\in\mathcal{H}_{n-1}\llbracket\mathcal{L},\mathcal{T}[t:({\sf
skip},r)],\Sigma^{\prime}\rrbracket\\}\\\ &&{}\cup\\{((t,{\sf ret}\
m(r))::h)\mid m\in{\sf dom}(\mathcal{L})\land\mathcal{T}(t)=({\sf
skip},r)\land{}\\\ &&\hfill
h\in\mathcal{H}_{n-1}\llbracket\mathcal{L},\mathcal{T}[t:{\sf
idle}],\Sigma\rrbracket\\}\end{array}$

We let $\mathcal{H}\llbracket\mathrm{\ell},\sigma\rrbracket=\bigcup_{n\geq
0}\mathcal{H}_{n}\llbracket\mathcal{L},(\lambda t{.\,}{\sf
idle}),\Sigma\rrbracket$ denote the set of all possible histories of a library
$\mathcal{L}$ that start from a state $\Sigma$.

We are now ready to prove Theorem 7.

Proof. Let us consider any $\mathrm{\ell},\mathcal{L},\mathcal{P},\mathcal{Q}$
such that ${\sf safelib}(\mathrm{\ell},\mathcal{L},\mathcal{P},\mathcal{Q})$
holds. Let us explain how we strengthen the statement of the theorem in this
proof. We prove that $\forall n{.\,}\phi(n)$ holds with $\phi(n)$ formulated
as follows:

$\phi(n)=\forall{\bf i},\sigma,\Sigma,\Delta,\tau,\mathcal{T}{.\,}(\exists
v_{1},\dots,v_{N}{.\,}(\forall k{.\,}{\sf inv}_{k}({\bf
i},\tau,\mathcal{T},v_{k},\Delta))\land{}\\\
(\sigma,\Sigma,\Delta)\in\lfloor{\circledast_{t\in{\sf
ThreadID}}v_{t}}\rfloor)\implies\mathcal{H}_{n}\llbracket\mathrm{\ell},\tau,\sigma\rrbracket\subseteq\mathcal{H}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket.$
(16)

Note that according to the semantics of the assertion language ${\sf Assn}$
(Figure 2):

$\llbracket\circledast_{k\in{\sf ThreadID}}(\exists{\rm
A}{.\,}\mathcal{Q}(k,{\rm A}))\rrbracket_{{\bf i}}=\circledast_{k\in{\sf
ThreadID}}\llbracket(\exists{\rm A}{.\,}\mathcal{Q}(k,{\rm
A}))\rrbracket_{{\bf i}}.$

With that in mind, it is easy to see that letting
$v_{k}=\llbracket(\exists{\rm A}{.\,}\mathcal{Q}(k,{\rm A}))\rrbracket_{{\bf
i}}$ for all $k\in{\sf ThreadID}$, $\tau=(\lambda t{.\,}{\sf idle})$ and
$\mathcal{T}=(\lambda t{.\,}{\sf idle})$ in (16) yields the formula:

$(\forall{\bf
i},\sigma,\Sigma,\Delta{.\,}(\sigma,\Sigma,\Delta)\in\lfloor{\llbracket\circledast_{k\in{\sf
ThreadID}}(\exists{\rm A}{.\,}\mathcal{Q}(k,{\rm A}))\rrbracket_{{\bf
i}}}\rfloor\implies{}\\\ \bigcup_{n\geq
0}\mathcal{H}_{n}\llbracket\mathrm{\ell},\lambda t{.\,}{\sf
idle},\sigma\rrbracket\subseteq\mathcal{H}\llbracket\mathcal{L},\lambda
t{.\,}{\sf idle},\Sigma\rrbracket),$

which coincides with the statement of the theorem.

We prove $\forall n{.\,}\phi(n)$ by induction on $n$. Let us take any ${\bf
i},\sigma,\Sigma,\Delta,\tau$ and $\mathcal{T}$, and consider
$v_{1},\dots,v_{N}$ such that the premisses of $\phi(n)$ hold:

$(\forall k{.\,}{\sf inv}_{k}({\bf
i},\tau,\mathcal{T},v_{k},\Delta))\land(\sigma,\Sigma,\Delta)\in\lfloor{\circledast_{k\in{\sf
ThreadID}}v_{k}}\rfloor$ (17)

We need to demonstrate that every history $h$ of the concrete library
$\mathrm{\ell}$ from the set
$\mathcal{H}_{n}\llbracket\mathrm{\ell},\tau,\sigma\rrbracket$ is also a
history of the abstract library $\mathcal{L}$:
$h\in\mathcal{H}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket$.

By Definition 5 of
$\mathcal{H}_{n}\llbracket\mathrm{\ell},\tau,\sigma\rrbracket$, if $n=0$, then
$h$ is an empty history that is trivially present in
$\mathcal{H}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket$. Let us now
consider $n>0$ and assume that $\phi(n-1)$ holds. By definition of
$\mathcal{H}_{n}\llbracket\mathrm{\ell},\tau,\sigma\rrbracket$, $h$
corresponds to one of the three events in a thread $t$: a call of an arbitrary
method $m$ with an argument $a$ in a thread $t$, a return from a method $m$
with a return value $r$ or a transition in a thread $t$. We consider each case
separately.

Case #1. There is a history $h^{\prime}$, a thread $t$, a method $m\in{\sf
dom}(\mathrm{\ell})$, its argument $a$ and a return value $r$ such that
$h=(t,{\sf call}\ m(a))::h^{\prime}$, $\tau(t)={\sf idle}$ and
$h^{\prime}\in\mathcal{H}_{n-1}\llbracket\mathrm{\ell},\tau[t:(\mathrm{\ell}(m,a,r),r),\sigma]\rrbracket$.
By Definition 15, to conclude that $h=(t,{\sf call}\
m(a))::h^{\prime}\in\mathcal{H}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket$
it is necessary to show that $\mathcal{T}(t)={\sf idle}$ and
$h^{\prime}\in\mathcal{H}\llbracket\mathcal{L},\mathcal{T}[t:(\mathcal{L}(m,a,r),r)],\Sigma\rrbracket$,
which we further do in the proof of Case #1.

According to (17), ${\sf inv}_{t}({\bf i},\tau,\mathcal{T},v_{t},\Delta)$ and
$(\sigma,\Sigma,\Delta)\in\lfloor{\circledast_{k\in{\sf
ThreadID}}v_{k}}\rfloor$ hold. Then necessarily $\mathcal{T}(t)={\sf idle}$
and $v_{t}\Rrightarrow\llbracket\mathcal{Q}(t,\\_)\rrbracket_{{\bf i}}$, which
corresponds to the only case when $\tau(t)={\sf idle}$ in the thread pool
invariant. By Definition 5 of
$v_{t}\Rrightarrow\llbracket\mathcal{Q}(t,\\_)\rrbracket_{{\bf i}}$,
$(\sigma,\Sigma,\Delta)\in\lfloor{\circledast_{k\in{\sf
ThreadID}}v_{k}}\rfloor$ implies
$(\sigma,\Sigma,\Delta)\in\lfloor{\llbracket\mathcal{Q}(t,\\_)\rrbracket_{{\bf
i}}\mathbin{*}\circledast_{k\in{\sf ThreadID}\setminus\\{t\\}}v_{k}}\rfloor$.
From requirements to predicates $\mathcal{P}$ and $\mathcal{Q}$ in ${\sf
safelib}(\mathrm{\ell},\mathcal{L},\mathcal{P},\mathcal{Q})$ we obtain that
the following holds of $(\sigma,\Sigma,\Delta)$:

  * •

$\Delta(t)={\sf done}(\\_)$, and

  * •

$(\sigma,\Sigma,\Delta[t:{\sf
todo}(\mathcal{L}(m,a,r))])\in\lfloor{\llbracket\mathcal{P}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}}\mathbin{*}\circledast_{k\in{\sf ThreadID}\setminus\\{t\\}}v_{k}}\rfloor$.

Let
$v_{t}^{\prime}=\llbracket\mathcal{P}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}}$ and $v_{k}^{\prime}=v_{k}$ for all $k\not=t$. Obviously,
$(\sigma,\Sigma,\Delta[t:{\sf
todo}(\mathcal{L}(m,a,r))])\in\lfloor{\circledast_{k}v_{k}^{\prime}}\rfloor$.

Also, by Lemma 4, ${\sf
safe}_{t}(\llbracket\mathcal{P}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}},\mathrm{\ell}(m,a,r),\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}})$ holds. This allows us to conclude that in a thread $t$ a thread pool
invariant ${\sf inv}_{t}({\bf
i},\tau[t:(\mathrm{\ell}(m,a,r),r)],\mathcal{T}[t:(\mathcal{L}(m,a,r),r)],v_{t}^{\prime},\Delta[t:\mathcal{L}(m,a,r)])$
holds. Moreover, according to (17), thread pool invariants hold in all other
threads as well.

We have shown that there exist $v_{1}^{\prime},\dots,v_{N}^{\prime}$ such
that:

$(\forall k{.\,}{\sf inv}_{k}({\bf
i},\tau[t:(\mathrm{\ell}(m,a,r),r)],\mathcal{T}[t:(\mathcal{L}(m,a,r),r)],v_{k}^{\prime},\Delta[t:\mathcal{L}(m,a,r)]))\land{}\\\
(\sigma,\Sigma,\Delta[t:{\sf
todo}(\mathcal{L}(m,a,r))])\in\lfloor{\circledast_{k\in{\sf
ThreadID}}v_{k}^{\prime}}\rfloor,$

which by the induction hypothesis $\phi(n-1)$ implies that
$h^{\prime}\in\mathcal{H}_{n-1}\llbracket\mathrm{\ell},\tau[t:(\mathrm{\ell}(m,a,r),r)],\sigma\rrbracket\subseteq\mathcal{H}\llbracket\mathcal{L},\mathcal{T}[t:(\mathcal{L}(m,a,r),r)],\Sigma\rrbracket$.
We have also show that $\mathcal{T}(t)={\sf idle}$. By Definition 15,
$h=(t,{\sf call}\
m(a))::h^{\prime}\in\mathcal{H}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket$,
which concludes the proof of Case #1.

Case #2. There is a history $h^{\prime}$, a thread $t$, a method $m\in{\sf
dom}(\mathrm{\ell})$, its argument $a$ and a return value $r$ such that
$h=(t,{\sf ret}\ m(r))::h^{\prime}$, $\tau(t)=({\sf skip},r)$ and
$h^{\prime}\in\mathcal{H}_{n-1}\llbracket\mathrm{\ell},\tau[t:{\sf
idle}],\sigma\rrbracket$. By Definition 15, to conclude that $h=(t,{\sf ret}\
m(r))::h^{\prime}\in\mathcal{H}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket$
it is necessary to show that $\mathcal{T}(t)=({\sf skip},r)$ and
$h^{\prime}\in\mathcal{H}\llbracket\mathcal{L},\mathcal{T}[t:{\sf
idle}],\Sigma\rrbracket$, which we further do in this proof of Case #2.

According to (17), a thread invariant ${\sf inv}_{t}({\bf
i},\tau,\mathcal{T},v_{t},\Delta)$ holds. Then the following is true:

${\sf safe}_{t}(v_{t},{\sf
skip},\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}})\land((\Delta(t)={\sf
todo}(\mathcal{L}(m,a,r))\land\mathcal{T}(t)=(\mathcal{L}(m,a,r),r))\lor{}\\\
(\Delta(t)={\sf done}(\mathcal{L}(m,a,r))\land\mathcal{T}(t)=({\sf
skip},r))).$ (18)

By Definition 3 of ${\sf safe}_{t}(v_{t},{\sf
skip},\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf i}})$,
$v_{t}\Rrightarrow\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}}$ holds. Consequently, by Definition 5:

$(\sigma,\Sigma,\Delta)\in\lfloor{v_{t}\mathbin{*}\circledast_{k\in{\sf
ThreadID}\setminus\\{t\\}}v_{k}}\rfloor\subseteq\lfloor{\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}}\mathbin{*}\circledast_{k\in{\sf ThreadID}\setminus\\{t\\}}v_{k}}\rfloor.$

From the third requirement to $\mathcal{Q}$ in Definition 13:

$(\sigma,\Sigma,\Delta)\in\lfloor{\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}}\mathbin{*}\circledast_{k}v_{k}}\rfloor\implies\Delta(t)={\sf
done}(\mathcal{L}(m,a,r)).$

Consequently, from (18) we get that $\Delta(t)={\sf done}(\mathcal{L}(m,a,r))$
and $\mathcal{T}(t)=({\sf skip},r)$.

Let
$v_{t}^{\prime}=\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}}$ and $v_{k}^{\prime}=v_{k}$ for $k\not=t$. It is easy to see that ${\sf
inv}_{t}({\bf i},\tau[t:{\sf idle}],\mathcal{T}[t:{\sf
idle}],v_{t}^{\prime},\Delta)$ holds trivially by Definition 14. Moreover,
according to (17), thread pool invariants hold in other threads as well.

We have shown that there exist $v_{1}^{\prime},\dots,v_{N}^{\prime}$ such
that:

$(\forall k{.\,}{\sf inv}_{k}({\bf i},\tau[t:{\sf idle}],\mathcal{T}[t:{\sf
idle}],v_{k}^{\prime},\Delta))\land(\sigma,\Sigma,\Delta)\in\lfloor{\circledast_{k\in{\sf
ThreadID}}v_{k}^{\prime}}\rfloor,$

which by the induction hypothesis $\phi(n-1)$ implies that
$h^{\prime}\in\mathcal{H}_{n-1}\llbracket\mathrm{\ell},\tau[t:{\sf
idle}],\sigma\rrbracket\subseteq\mathcal{H}\llbracket\mathcal{L},\mathcal{T}[t:{\sf
idle}],\Sigma\rrbracket$. We have also show that $\mathcal{T}(t)=({\sf
skip},r)$. By Definition 15, $h=(t,{\sf ret}\
m(r))::h^{\prime}\in\mathcal{H}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket$,
which concludes the proof of Case #2.

Case #3. There is a thread $t$, sequential commands $C$ and $C^{\prime}$, a
primitive command ${\sf\alpha}$, concrete states $\sigma$ and
$\sigma^{\prime}$ and a return value $r$ such that $\tau(t)=(C,r)$, $\langle
C,\sigma\rangle\mathrel{{\ext@arrow
05{40}0{\arrowfill@\relbar\relbar\twoheadrightarrow}{}{t,{\sf\alpha}}}{}}\langle
C^{\prime},\sigma^{\prime}\rangle$ and
$h\in\mathcal{H}_{n-1}\llbracket\mathrm{\ell},\tau[t:(C^{\prime},r)],\sigma^{\prime}\rrbracket$.

According to (17), ${\sf inv}_{t}({\bf i},\tau,\mathcal{T},v_{t},\Delta)$
holds. Consequently, there exist a method $m$ with its argument $a$ such that
$C=\mathcal{L}(m,a,r)$ and:

${\sf
safe}_{t}(v_{t},C,\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}})\land{}\\\ ((\Delta(t)={\sf
todo}(\mathcal{L}(m,a,r))\land\mathcal{T}(t)=(\mathcal{L}(m,a,r),r))\lor{}\\\
(\Delta(t)={\sf done}(\mathcal{L}(m,a,r))\land\mathcal{T}(t)=({\sf
skip},r))).$ (19)

It is easy to see that whenever there is a transition $\langle
C,\sigma\rangle\mathrel{{\ext@arrow
05{40}0{\arrowfill@\relbar\relbar\twoheadrightarrow}{}{t,{\sf\alpha}}}{}}\langle
C^{\prime},\sigma^{\prime}\rangle$, there also is a stateless transition
$C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$. By Definition 3 of
${\sf
safe}_{t}(v_{t},C,\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}})$, if $C\mathrel{{\xlongrightarrow{{\sf\alpha}}}{}}C^{\prime}$, then there
exists a view $v_{t}^{\prime}$ such that
$\,{\sf\alpha}\Vdash_{t}\\{v_{t}\\}\\{v_{t}^{\prime}\\}$ and ${\sf
safe}_{t}(v_{t}^{\prime},C^{\prime},\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}})$.

Let $v_{k}^{\prime}=v_{k}$ for any $k\not=t$. By Definition 2 of the action
judgement $\,{\sf\alpha}\Vdash_{t}\\{v_{t}\\}\\{v_{t}^{\prime}\\}$, for
$(\sigma,\Sigma,\Delta)\in\lfloor{v_{t}\mathbin{*}\circledast_{k\not=t}v_{k}}\rfloor$
and any $\sigma^{\prime}\in\llbracket{\sf\alpha}\rrbracket_{t}(\sigma)$, there
exist $\Sigma^{\prime},\Delta^{\prime}$ such that:

${\sf
LP}^{*}(\Sigma,\Delta,\Sigma^{\prime},\Delta^{\prime})\land(\sigma^{\prime},\Sigma^{\prime},\Delta^{\prime})\in\lfloor{v_{t}^{\prime}\mathbin{*}\circledast_{k\not=t}v_{k}}\rfloor.$
(20)

Let us assume that $\Delta=\Delta^{\prime}$. Note that ${\sf
safe}_{t}(v_{t}^{\prime},C^{\prime},\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}})$ holds, and according to (19) the following holds too:

$(\Delta(t)={\sf
todo}(\mathcal{L}(m,a,r))\land\mathcal{T}(t)=(\mathcal{L}(m,a,r),r))\lor{}\\\
(\Delta(t)={\sf done}(\mathcal{L}(m,a,r))\land\mathcal{T}(t)=({\sf skip},r))$

Thus, it is easy to see that ${\sf inv}_{t}({\bf
i},\tau[t:(C^{\prime},r)],\mathcal{T},v_{t}^{\prime},\Delta)$ holds. Combining
this observation with (20), we conclude that we have demonstrated existance of
$v_{1}^{\prime},\dots,v_{N}^{\prime}$ such that:

$(\forall k{.\,}{\sf inv}_{k}({\bf
i},\tau[t:(C^{\prime},r)],\mathcal{T},v_{k}^{\prime},\Delta))\land(\sigma^{\prime},\Sigma^{\prime},\Delta)\in\lfloor{\circledast_{k\in{\sf
ThreadID}}v_{k}^{\prime}}\rfloor,$

which by the induction hypothesis $\phi(n-1)$ implies that
$h\in\mathcal{H}_{n-1}\llbracket\mathrm{\ell},\tau[t:(C^{\prime},r)],\sigma^{\prime}\rrbracket\subseteq\mathcal{H}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket$.
This concludes the proof of the case when $\Delta=\Delta^{\prime}$.

We now return to the case when $\Delta\not=\Delta^{\prime}$. According to
(20), ${\sf LP}^{*}(\Sigma,\Delta,\Sigma^{\prime},\Delta^{\prime})$ holds,
meaning that linearization points of one or more threads have been passed.
Without loss of generality, we assume the case of exactly one linearization
point, i.e. that ${\sf LP}(\Sigma,\Delta,\Sigma^{\prime},\Delta^{\prime})$
holds. Consequently, according to Definition 2 there exist $t^{\prime}$ and
${\rm A}^{\prime}$ such that:

$\Sigma^{\prime}\in\llbracket{\rm
A}^{\prime}\rrbracket_{t^{\prime}}(\Sigma)\land\Delta(t^{\prime})={\sf
todo}({\rm A}^{\prime})\land\Delta^{\prime}=\Delta[t^{\prime}:{\sf done}({\rm
A}^{\prime})$ (21)

Let us consider the thread pool invariant ${\sf inv}_{t^{\prime}}({\bf
i},\tau,\mathcal{T},v_{t^{\prime}},\Delta)$, which holds according to (17). We
show that $\tau(t^{\prime})\neq{\sf idle}$. From (21) we know that
$\Delta(t^{\prime})={\sf todo}({\rm A}^{\prime})$. Since the third requirement
to $\mathcal{Q}$ in Definition 13 requires that $\Delta(t)={\sf
done}(\mathcal{L}(m,a,r))$ hold, by Definition 14 it can only be the case that
there exist $C^{\prime\prime},m^{\prime},a^{\prime},r^{\prime}$ such that
$\tau(t^{\prime})=(C^{\prime\prime},r^{\prime})$ and the following is true:

${\sf
safe}_{t^{\prime}}(v_{t},C^{\prime\prime},\llbracket\mathcal{Q}(t^{\prime},\mathcal{L}(m^{\prime},a^{\prime},r^{\prime}))\rrbracket_{{\bf
i}})\land{}\\\ ((\Delta(t^{\prime})={\sf
todo}(\mathcal{L}(m^{\prime},a^{\prime},r^{\prime}))\land\mathcal{T}(t^{\prime})=(\mathcal{L}(m^{\prime},a^{\prime},r^{\prime}),r^{\prime}))\lor{}\\\
(\Delta(t^{\prime})={\sf
done}(\mathcal{L}(m^{\prime},a^{\prime},r^{\prime}))\land\mathcal{T}(t^{\prime})=({\sf
skip},r^{\prime}))).$ (22)

From formula (21) we know that ${\rm
A}^{\prime}=\mathcal{L}(m^{\prime},a^{\prime},r^{\prime})$. Consequently,
$\Delta^{\prime}(t^{\prime})={\sf
done}(\mathcal{L}(m^{\prime},a^{\prime},r^{\prime}))\land\mathcal{T}[t^{\prime}:({\sf
skip},r^{\prime})](t^{\prime})=({\sf skip},r^{\prime})$ holds, which allows us
to conclude the thread pool invariant ${\sf inv}_{t^{\prime}}({\bf
i},\tau[t:(C^{\prime},r)],\mathcal{T}[t^{\prime}:({\sf
skip},r^{\prime})],v_{t^{\prime}}^{\prime},\Delta^{\prime})$ in case of
$t^{\prime}\neq t$.

We now show that ${\sf inv}_{t}({\bf
i},\tau[t:(C^{\prime},r)],\mathcal{T}[t^{\prime}:({\sf
skip},r^{\prime})],v_{t}^{\prime},\Delta^{\prime})$ hold, both when
$t=t^{\prime}$ and $t\neq t^{\prime}$. Let us first assume $t=t^{\prime}$
($r=r^{\prime}$). Then from (19) we get that ${\rm A}=\mathcal{L}(m,a,r)$ and
$\Delta^{\prime}(t)={\sf done}(\mathcal{L}(m,a,r))$ hold. When $t\neq
t^{\prime}$, no abstract transition is made in $t$, so
$\Delta(t)=\Delta^{\prime}(t)$ and
$\mathcal{T}(t)=\mathcal{T}[t^{\prime}:({\sf skip},r^{\prime})](t)$.
Consequently, the following is true in both cases:

$((\Delta^{\prime}(t)={\sf
todo}(\mathcal{L}(m,a,r))\land\mathcal{T}[t^{\prime}:({\sf
skip},r^{\prime})](t)=(\mathcal{L}(m,a,r),r))\lor{}\\\
(\Delta^{\prime}(t)={\sf
done}(\mathcal{L}(m,a,r))\land\mathcal{T}[t^{\prime}:({\sf
skip},r^{\prime})](t)=({\sf skip},r^{\prime}))).$ (23)

Together with ${\sf
safe}_{t}(v_{t}^{\prime},C^{\prime},\llbracket\mathcal{Q}(t,\mathcal{L}(m,a,r))\rrbracket_{{\bf
i}})$ , those observations imply ${\sf inv}_{t}({\bf
i},\tau[t:(C^{\prime},r)],\mathcal{T}[t^{\prime}:({\sf
skip},r^{\prime})],v_{t}^{\prime},\Delta^{\prime})$.

Combining these observations with
$(\sigma^{\prime},\Sigma^{\prime},\Delta^{\prime})\in\lfloor{v_{t}^{\prime}\mathbin{*}\circledast_{k\not=t}v_{k}}\rfloor$
following from (20), we conclude that we have demonstrated existance of
$v_{1}^{\prime},\dots,v_{N}^{\prime}$ such that:

$(\forall k{.\,}{\sf inv}_{k}({\bf
i},\tau[t:(C^{\prime},r)],\mathcal{T}[t^{\prime}:({\sf
skip},r^{\prime})],v_{k}^{\prime},\Delta^{\prime}))\land(\sigma^{\prime},\Sigma^{\prime},\Delta^{\prime})\in\lfloor{\circledast_{k\in{\sf
ThreadID}}v_{k}^{\prime}}\rfloor,$

which by the induction hypothesis $\phi(n-1)$ implies that
$h\in\mathcal{H}_{n-1}\llbracket\mathrm{\ell},\tau[t:(C^{\prime},r)],\sigma^{\prime}\rrbracket\subseteq\mathcal{H}\llbracket\mathcal{L},\mathcal{T}[t:({\sf
skip},r^{\prime})],\Sigma^{\prime}\rrbracket$. Now that we demonstrated that
$\mathcal{T}(t^{\prime})=(\mathcal{L}(m^{\prime},a^{\prime},r^{\prime}),r^{\prime})$,
$\Sigma^{\prime}\in\llbracket\mathcal{L}(m^{\prime},a^{\prime},r^{\prime})\rrbracket_{t}(\Sigma)$
and $h\in\mathcal{H}\llbracket\mathcal{L},\mathcal{T}[t:({\sf
skip},r^{\prime})],\Sigma^{\prime}\rrbracket$ all hold, by Definition 15 we
can conclude that
$h\in\mathcal{H}\llbracket\mathcal{L},\mathcal{T},\Sigma\rrbracket$. ∎