††thanks: Derrick and Doherty are supported by EPSRC project EP/R032351/1.
Dongol is supported by EPSRC Grant EP/R032556/1. Bila and Dongol are supported
by VeTSS project “Persistent Safety and Security”. Wehrheim is partially
supported by DFG grant WE2290/12-1

# Modularising Verification of Durable Opacity

Eleni Bila  University of Surrey<EMAIL_ADDRESS>John Derrick
University of Sheffield<EMAIL_ADDRESS>Simon Doherty  University
of Sheffield<EMAIL_ADDRESS>Brijesh Dongol  University of Surrey
<EMAIL_ADDRESS>Gerhard Schellhorn  University of Augsburg
<EMAIL_ADDRESS>Heike Wehrheim  Paderborn University
<EMAIL_ADDRESS>
###### Abstract

Non-volatile memory (NVM), also known as persistent memory, is an emerging
paradigm for memory that preserves its contents even after power loss. NVM is
widely expected to become ubiquitous, and hardware architectures are already
providing support for NVM programming. This has stimulated interest in the
design of novel concepts ensuring correctness of concurrent programming
abstractions in the face of persistency and in the development of associated
verification approaches.

Software transactional memory (STM) is a key programming abstraction that
supports concurrent access to shared state. In a fashion similar to
linearizability as the correctness condition for concurrent data structures,
there is an established notion of correctness for STMs known as opacity. We
have recently proposed durable opacity as the natural extension of opacity to
a setting with non-volatile memory. Together with this novel correctness
condition, we designed a verification technique based on refinement. In this
paper, we extend this work in two directions.

First, we develop a durably opaque version of NOrec (no ownership records), an
existing STM algorithm proven to be opaque. Second, we modularize our existing
verification approach by separating the proof of durability of memory accesses
from the proof of opacity. For NOrec, this allows us to re-use an existing
opacity proof and complement it with a proof of the durability of accesses to
shared state.

###### keywords:

Nonvolatile memory, software transactional memory, opacity, formal
verification

##  1 Introduction

Non-volatile memories (NVM) promises the combination of the density and non-
volatility of NAND Flash-based solid-state disks (SSDs) with the performance
of volatile memory (RAM). The term persistent memory is used to describe an
NVM technology that presents two characteristics: directly byte-addressable
access from the user space by using byte-addressable operations and
preservation of its content even after system crashes and power failures. NVM
is intended to be used as an intermediate layer between traditional volatile
memory (VM) and secondary storage, and has the potential to vastly improve
system speed and stability. Speed-ups of 2-3 orders of magnitude are likely to
be feasible over and above hard disks. Furthermore, software that uses NVM has
the potential to be more robust; in case of a crash, a system state before the
crash may be recovered using contents from NVM, as opposed to being restarted
from secondary storage. For these reasons alone, NVM is widely expected to
become ubiquitous, and hardware architectures are already providing support
for NVM programming.

However, writing correct NVM programs is extremely difficult, as the semantics
of persistency can be unclear. Furthermore, because the same data is stored in
both a volatile and non-volatile manner, and because NVM is updated at a
slower rate than VM, recovery to a consistent state may not always be
possible. This is particularly true for concurrent systems, where coping with
NVM requires introduction of additional synchronisation instructions into a
program. Such instructions are already supported by Intel-x86 and ARMv8.

This has led to work on the design of the first persistent concurrent
programming abstractions, so far mainly concurrent data structures [ZFS+19,
FHMP18]. To support the reasoning of correctness for these abstractions
working over NVM, a coherent notion of correctness is needed. Such a notion
for concurrent data structures has been defined by Izraelevitz et al. [IMS16]
(known as durable linearizability) which naturally generalizes the standard
linearizability correctness condition [HW90]. A first proof technique for
showing durable linearizability has been proposed by Derrick et al. in
[DDD+19].

In this paper we investigate another key programming abstraction known as
Software Transactional Memory (STM) that supports concurrent access to shared
state. STM is a mechanism that provides an illusion of atomicity in concurrent
programs and aims to reduce the burden on programmers of implementing
complicated synchronization mechanisms. The analogy of STM is with database
transactions, which perform a series of accesses/updates to shared data (via
read and write operations) atomically in an all-or-nothing manner. Similarly
with an STM, if a transaction commits, all its operations succeed, and in the
aborting case, all its operations fail. STMs are now part of mainstream
programming, e.g., the ScalaSTM library, a new language feature in Clojure
that uses an STM implementation internally for all data manipulation and the
G++ 4.7 compiler (which supports STM features directly in the compiler).

In a fashion similar to linearizability as the correctness condition for
concurrent data structures, there is an established notion of correctness for
STMs known as opacity [GK08]. Overall, opacity guarantees that committed
transactions should appear as if they are executed atomically, at some unique
point in time, and aborted transactions, as if they did not execute at all.
Amongst other things, opacity also guarantees that all reads that a
transaction performs are valid with respect to a single memory snapshot.

A fundamental challenge when using persistent memory is to ensure a correct
recovery after a crash. This requires the persistent program state to be
consistent, at any point of execution. The consistency of persistent memory is
mainly depending on the order in which the write-backs to persistent memory
occur. Such write-backs are inevitable as cache lines should at some point be
evicted from the cache, to make space for new data. The order in which cache
lines are evicted is predominantly determined by the cache coherence protocol.
Various mechanisms are introduced in order to guarantee that the order in
which the processor issues writes coincide with the order that they propagate
to persistent memory. Conventional architectures (e.g. Intel, ARMv8), provide
explicit write-back instructions that flush the cache-line which contains the
address to be placed in the persistent memory.

One requirement of transactional memory is that the operations (reads/writes)
of each transaction should be atomic – performed as if they are a single
operation. Persistent transactional memory algorithms typically use (undo or
redo) logs to provide atomic writes of multiple cache lines to NVM. In our
case, we use a global persistent undo log that records the values of the
addresses that a writing transaction is about to update. When a transaction
commits it erases the values of the undo log. This is because after a
successful commit the writes of the committed transaction never need to be
undone. In case that a crash occurs before a writing transaction commits, the
undo log enables us to roll-back the state of the persistent memory, to a
consistent state. Specifically, the undo log allows the state of the
persistent memory to return to the state that it was immediately after the
last successful commit of a transaction. This is performed in two steps.
Firstly, after a crash, the content of the persistent is implicitly copied by
the system to the volatile memory. Afterward, a recovery operation checks for
a non-empty log and transfers the logged value to persistent memory. In this
way, the recovery undo the effects of the uncommitted writes. In the end of
the recovery procedure, the log is emptied.

In this paper, we investigate STMs and their correctness via opacity on non-
volatile memory architectures.

Doing this entails a number of steps. First, the correctness criterion of
opacity has to be adapted to cope with crashes in system executions. Second,
STM algorithms have to be extended to deal with the coexistence of volatile
and non-volatile memory during execution and need to be equipped with recovery
operations. Third, proof techniques for opacity need to be re-investigated to
make them usable for durable opacity. In this paper, we provide contributions
to all three steps.

  * •

For the first step, we define durable opacity as a generalisation of opacity
in the same way that durable linearizability has been defined as a
generalization of linearizability for NVM architectures. As we define it
below, durable opacity will require the executions of STMs to be opaque even
if they are interspersed with crashes. This guarantees that the shared state
remains consistent.

  * •

In the second step we show how to define correct STMs for NVM. This is
illustrated by extending the No-Ownership-Records (NOrec) STM of Dalessandro
et al. [DSS10] to create a durable NOrec. To this end, NOrec needs to be
equipped with a recovery operation and special statements to guarantee
consistency in case of crashes. We do so by extending it with a logging
mechanism which allows to flush written, but volatile values to NVM during
recovery.

  * •

For the third step, we introduce a novel modular approach for verification of
durable opacity which has been inspired by the modularised verification in the
context of flash memory filesystem [PEB+17, BSR20]. This approach separates
the proof of durability (correct handling of non-volatile memory) from the
proof of opacity (seeming atomicity of memory access). It can hence re-use
existing opacity proofs.

Finally, we bring all three steps together and apply our proof technique to
show that durable NOrec is indeed durably opaque. Using the modular approach,
we here leverage the opacity proof for NOrec given by Lesani et al. [LLM12a].

This article is an extension of our prior work [BDD+20]. Besides the
definition of opacity in [BDD+20], we here in addition introduce the durable
version of NOrec (durable NOrec), present a novel modular approach to the
verification of durable opacity and illustrate it on durable NOrec. The work
in [BDD+20] contains a durable version of another STM (the Transactional Mutex
Lock of Dalessandro et al. [DDS+10]) and a non-modular proof of its durable
opacity.

##  2 Concurrent Correctness and Durability

We start by defining the correctness conditions relevant for our approach.
These correctness conditions are linearizability and opacity. Linearizability
[HW90] is the standard correctness condition for concurrent data structures;
opacity [GK08] is typically employed for software transactional memory
algorithms. Both formalize some form of atomicity in which a block of code
seemingly atomic executes in an all-or-nothing manner. The difference lays in
the level of atomicity: for linearizability blocks of code describe one
operation of a concurrent data structure; for opacity we also have blocks of
code for specific operations, and in addition group such operations into
transactions.

###  2.1 Histories

Both correctness conditions are formalized on the basis of histories. A
history is a sequence of events. An event is either (1) an invocation (inv) or
(2) a response (res) of an operation $op$ out of a set of operations
$\mathit{\Sigma}$ or (3) a system wide crash event $\mathit{c}$. Invocation
and response events of the same operation are said to match. Events are
furthermore parameterized by thread or transaction identifiers from a set $T$.
For simplicity, we do not distinguish between threads and transactions here.
Invocation events might have input parameters and response events output
parameters. We use the following notation on histories: for a history $h$,
$h\zproject t$ is the projection onto the events of transaction or thread $t$
only, and $h[i..j]$ the subsequence of $h$ from $h(i)$ to $h(j)$ inclusive. We
say that two histories $h$ and $h^{\prime}$ are equivalent if $h\zproject
t=h^{\prime}\zproject t$ for all $t\in T$. For a response event $e$, we let
$rval(e)$ denote the value returned by $e$. If $e$ is not a response event,
then we let $rval(ev)=\bot$. We furthermore let $Res$ be the set of all
response and $Inv$ the set of all invocation events.

We consider two types of histories, transactional and non-transactional
histories. A transactional history only contains the invocation and response
events of Table 1. Software transactional memory algorithms allow for a
concurrent access to shared memory (a set of locations $Loc$). Every
transaction consists of an operation TMBegin followed by a number of
operations TMWr or TMRd and finally an operation TMCommit. All of these
operations might also return with an abort meaning that the operation has not
succeeded. We say that a transaction $t$ is committed in a history $h$ if
$res_{t}(\texttt{TMCommit}({\tt ok}))$ is contained in $h$. In non-
transactional histories we just have a set of operations on a data structure
and no grouping of operations into transactions.

invocations | possible matching responses
---|---
$inv_{t}(\texttt{TMBegin})$ |  $res_{t}(\texttt{TMBegin}({\tt ok}))$, $res_{t}(\texttt{TMBegin}({\tt abort}))$
$inv_{t}(\texttt{TMCommit})$ |  $res_{t}(\texttt{TMCommit}({\tt ok}))$, $res_{t}(\texttt{TMCommit}({\tt abort}))$
$inv_{t}(\texttt{TMRd}(x))$ |  $res_{t}(\texttt{TMRd}(v))$, $res_{t}(\texttt{TMRd}({\tt abort}))$
$inv_{t}(\texttt{TMWr}(x,v))$ |  $res_{t}(\texttt{TMWr}({\tt ok}))$, $res_{t}(\texttt{TMWr}({\tt abort}))$
Table 1: Events appearing in transactional histories, where $t\in T$ is a
transaction identifier, $x\in\mathit{Loc}$ is a location, and
$v\in\mathit{Val}$ a value

A (non-transactional) history is sequential if every invocation event (except
for possibly the last event) is directly followed by its matching response. A
transactional history is transaction sequential if it is sequential and there
are no overlapping transactions. A history is complete if there are no pending
operations, i.e., no invocations without a matching return. The function
$complete$ removes all pending operations from a history. A history is well-
formed if $h\zproject t$ is sequential for every $t\in T$. A well-formed
transactional history is furthermore transaction well-formed if for every $t$,
$h\zproject t=\lseq\mathit{ev}_{0},\ldots,\mathit{ev}_{m}\rseq$ is a
sequential history such that $\mathit{ev}_{0}=inv_{t}(\texttt{TMBegin})$, and
for all $0<i<m$, event $\mathit{ev}_{i}\neq inv_{t}(\texttt{TMBegin})$ and
$rval(\mathit{ev}_{i})\notin\\{\texttt{commit},\texttt{abort}\\}$. This in
particular implies that transaction identifiers cannot be re-used.

For a history $h$ and events $e_{1},e_{2}$, we write (1) $e_{1}<_{h}e_{2}$
whenever $h=h_{0}e_{1}h_{1}e_{2}h_{2}$, and (2) $e_{1}\ll_{h}e_{2}$ if
$e_{1}<_{h}e_{2}$ and $e_{1}\in Res,e_{2}\in Inv$ (real-time order of
operations). In a transactional history $h$, we furthermore write
$t_{1}\prec_{h}t_{2}$ if the commit operation of transaction $t_{1}$ completes
before transaction $t_{2}$ starts (real-time order of transactions).

###  2.2 Linearizability and Durable Linearizability

Linearizability of concurrent data structures is defined by comparing the
(possibly concurrent) histories arising in usages of the data structure to
sequential legal histories. Legality is defined by specifying sequential
objects $\mathbb{S}$, i.e., sequential versions of a data structure (see
Definition 3.2). These sequential versions define the ”correct” behaviour,
like, e.g. a queue data structure adhering to a FIFO protocol or not losing
elements. For the formal definition of linearizability here, we simply assume
that we have the set of sequential legal histories $H_{\mathbb{S}}$ (as
generated by sequential objects) given. Later, we will give an abstract data
type in the form of an IOA [LT87] as a specification of a sequential object.

A concurrent data structure is linearizable if all of its histories arising in
usages of the data structure are linearizable.

######  Definition .

A (concurrent) history $h$ is linearizable (wrt. some set of sequential
histories $H_{\mathbb{S}}$) if there exists some $h_{0}\in Res^{*}$
(completing some of the pending operations) such that for
$h^{\prime}=complete(hh_{0})$ there exists some $h_{s}\in H_{\mathbb{S}}$ such
that

L1

$h^{\prime}\equiv h_{s}$ and

L2

$e\ll_{h^{\prime}}e^{\prime}$ implies $e\ll_{h_{s}}e^{\prime}$.

For this definition, we assume the history does not contain any crash events.
Linearizability only considers executions of data structures without
intervening system crashes, basically because linearizability assumes data
structures to not survive crashes.

For durable linearizability, designed for hardware architectures with non-
volatile memory where data of main memory might survive system crashes, we
need to look at histories with crash events. Given a history $h$, we let ${\it
ops}(h)$ denote $h$ restricted to non-crash events. The crash events partition
a history into
$h=h_{0}\mathit{c}_{1}h_{1}\mathit{c}_{2}...h_{n-1}\mathit{c}_{n}h_{n}$, such
that $n$ is the number of crash events in $h$, $\mathit{c}_{i}$ is the $i$th
crash event and $ops(h_{i})=h_{i}$ (i.e., $h_{i}$ contains no crash events).
We call the subhistory $h_{i}$ the $i$-th era of $h$. For well-formedness of
histories we now also require every thread/transaction identifier to appear in
at most one era.

These definitions allow us to lift linearizability to durable linearizability.

######  Definition  (Durable Linearizability [IMS16]).

A history $h$ is durably linearizable if it is well formed and ${\it ops}(h)$
is linearizable.

###  2.3 Opacity and Durable Opacity

Opacity [GK10, GK08] compares concurrent histories generated by an STM
implementation to sequential histories. The difference to linearizability is
that we (a) need to consider entire transactions and (b) have to deal with
aborted transactions. The correctness criterion opacity guarantees that values
written by aborted transactions (i.e., transactions with events with abort as
response value) cannot be read by other transactions.

For opacity, we again compare concurrent histories against a set of legal
sequential ones, but now we employ transaction sequential histories. Again, we
assume the set of legal sequential transactional histories $TH_{\mathbb{S}}$
to be given, and out of these define the valid ones.

######  Definition .

Let $hs$ be a sequential history and $i$ an index of $hs$. Let $hs^{\prime}$
be the projection of $hs[0..(i-1)]$ onto all events of committed transactions
plus the events of the transaction to which $hs(i)$ belongs. Then we say _$hs$
is valid at $i$_ whenever $hs^{\prime}$ is legal. We say _$hs$ is valid_ iff
it is valid at each index $i$.

We let $VH_{\mathbb{S}}$ be the set of transaction sequential valid histories.
With this at hand, we can define opacity similar to linearizability.

######  Definition .

A (concurrent) history $h$ is end-to-end opaque iff there exists some
$h_{0}\in Res^{*}$ (completing some of the pending operations) such that for
$h^{\prime}=complete(hh_{0})$ there exists some $h_{s}\in VH_{\mathbb{S}}$
such that

O1

$h^{\prime}\equiv h_{s}$, and

O2

$t_{1}\prec_{h}t_{2}$ implies $t_{1}\prec_{h_{s}}t_{2}$.

A history $h$ is opaque iff each prefix $h^{\prime}$ of $h$ is end-to-end
opaque.

An STM algorithm itself is _opaque_ iff its set of histories occuring during
executions of the STM is opaque. For durable opacity, we simply lift this
definition to histories with crashes.

######  Definition  (Durably Opacity [BDD+20]).

A history $h$ is durably opaque iff it is transaction well-formed and $ops(h)$
is opaque.

In this paper, we aim at proving durable opacity of STM algorithms. For the
proof, we employ a modular proof technique which requires showing durable
linearizability of some library data structure providing access to shared
memory.

##  3 Using IOA to Prove Durable Opacity

Previous works [ADD17, DDD+16, DD15, AD17] have considered proofs of opacity
using the operational TMS2 specification [DGLM13], which has been shown to
guarantee opacity [LLM12b]. The proofs show refinement of the implementation
against the TMS2 specification using either forward or backward simulation. In
this, both implementation and specification are given as IOA as to be able to
employ standard simulation concepts. For durable opacity, we follow a similar
strategy. We develop the dTMS2 operational specification, a durable version of
the TMS2 specification, that we prove satisfies durable opacity. By proving a
simulation relation to hold between a (durable) STM implementation and dTMS2
we can establish durable opacity of an STM.

In the following, we will first of all shortly explain IOA and simulations in
general and thereafter develop dTMS2.

###  3.1 IOA, Refinement and Simulation

We use Input/Output Automata (IOA) [LT87] to model both STM implementations
and the specification, dTMS2.

######  Definition .

An _Input/Output Automaton (IOA)_ is a labeled transition system $A$ with a
set of _states_ $states(A)$, a set of _actions_ $acts(A)$, a set of _start
states_ $start(A)\subseteq states(A)$, and a _transition relation_
$trans(A)\subseteq states(A)\times acts(A)\times states(A)$ (so that the
actions label the transitions).

The set $acts(A)$ is partitioned into input actions $input(A)$, output actions
$output(A)$ and internal actions $internal(A)$. The internal actions represent
events of the system that are not visible to the external environment. The
input and output actions are externally visible, representing the automaton’s
interactions with its environment. Thus, we define the set of external
actions, $external(A)=input(A)\cup output(A)$. We write
$s\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{A}s^{\prime}$ iff
$(s,a,s^{\prime})\in trans(A)$.

An execution of an IOA $A$ is a sequence
$\sigma=s_{0}a_{0}s_{1}a_{1}s_{2}\dots s_{n}a_{n}s_{n+1}$ of alternating
states and actions, such that $s_{0}\in start(A)$ and for all states $s_{i}$,
$s_{i}\stackrel{{\scriptstyle a_{i}}}{{\longrightarrow}}_{A}s_{i+1}$. A
reachable state of $A$ is a state appearing in an execution of $A$. We let
$reach(A)$ denote the set of all reachable states of $A$. An invariant of $A$
is any superset of the reachable states of $A$ (equivalently, any predicate
satisfied by all reachable states of $A$). A trace of $A$ is any sequence of
(external) actions obtained by projecting the external actions of any
execution of $A$. The set of traces of $A$, denoted $traces(A)$, represents
$A$’s externally visible behaviour.

For automata $C$ and $A$, we say that $C$ is a refinement of $A$, denoted
$C\leq A$, iff $traces(C)\subseteq traces(A)$. We show that $C$ is a
refinement of $A$ by proving the existence of a forward simulation, which
enables one to check step correspondence between the transitions of $C$ and
those of $A$. The definition of forward simulation we use is adapted from that
of Lynch and Vaandrager [LV95].

######  Definition .

A _forward simulation_ from a concrete IOA $C$ to an abstract IOA $A$ is a
relation $R\subseteq states(C)\times states(A)$ such that each of the
following holds.

_Initialisation_. $\forall cs\in start(C).\ \exists as\in start(A).\ R(cs,as)$

_External step correspondence_.

$\begin{array}[t]{@{}l@{}}\forall cs\in reach(C),as\in reach(A),a\in
external(C),cs^{\prime}\in states(C).\\\ \qquad R(cs,as)\wedge
cs\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{C}cs^{\prime}\imp\exists
as^{\prime}\in states(A).\ R(cs^{\prime},as^{\prime})\wedge
as\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{A}as^{\prime}\end{array}$

_Internal step correspondence_.

$\begin{array}[t]{@{}l@{}}\forall cs\in reach(C),as\in reach(A),a\in
internal(C),cs^{\prime}\in states(C).\\\ \qquad R(cs,as)\wedge
cs\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{C}cs^{\prime}\imp\\\
\qquad\begin{array}[t]{@{}l@{}}R(cs^{\prime},as)\lor\exists a^{\prime}\in
internal(A),as^{\prime}\in states(A).\ R(cs^{\prime},as^{\prime})\wedge
as\stackrel{{\scriptstyle
a^{\prime}}}{{\longrightarrow}}_{A}as^{\prime}\end{array}\end{array}$

Forward simulation is sound in the sense that if there is a forward simulation
between $A$ and $C$, then $C$ refines $A$ [LV95, Mül98].

###  3.2 Canonical IOA for (durable) linearizability

To prove linearizability the relevant set of sequential histories
$H_{\mathbb{S}}$ are given as the histories of a sequential object
$\mathbb{S}$, that defines a set atomic operations $op_{i}$ that receive
input, modify a state and return output.

######  Definition  (Sequential Object).

A _sequential object_ $\mathbb{S}$ is a 5-tuple $(\Sigma,Val,State,Init)$
where

  * •

$State$ is a set of states, $Init\subseteq State$ is a set of initial states,

  * •

$Val$ is a set of values used as input and output,

  * •

$\Sigma$ is a set of atomic operations $op_{i}$ for some $i\in I$.
Each operation is specified as a relation $op_{i}\subseteq Val\times
State\times State\times Val$.

Some operations may have no or several inputs/outputs, which can be
accomodated by including tuples including the empty tuple $\epsilon$ in $Val$.
We drop an empty input or output when writing an event. A sequential history
of $\mathbb{S}$ has the form

$\displaystyle
inv(op_{k_{1}}(in_{1})),res(op_{k_{1}}(out_{1})),\ldots,inv(op_{k_{n}}(in_{n})),res(op_{k_{n}}(out_{n}))$
(1)

The history is a legal sequential history in $H_{S}$, iff there is a sequence
$s_{0}\ldots s_{n}$ of states, such that $s_{0}\in Init$ and
$(in_{m},s_{m},s_{m+1},out_{m})\in op_{k_{m}}$ for all $m<n$.

To prove durable linearizability of a concurrent implementation we will
specify the concurrent program as an IOA $C$ that generates a set of
concurrent histories. To prove that $C$ is durable linearizable to
$H_{\mathbb{S}}$ it is then sufficient to prove that $C$ refines the canonical
durable automaton $\textsc{DurAut}(\mathbb{S})$ shown in Fig. 1 (see
[DDD+19]). The state of this automaton incorporates the state $s$ of the
sequential object $\mathbb{S}$ and adds a program counter $pc_{t}$ for every
transaction $t\in T$. The possible values of this program counter include
notStarted, ready and crashed to indicate that the transaction has not started
(its initial value), is running but not currently executing an operation, or
has crashed. The execution of an operation $op$ is split into three steps: an
invocation and a response of the operation plus a do-step (where the actual
effect of the operation takes place).

  * •

First, when $pc_{t}$ = ready an invoke step with action $inv_{t}(op(in))$ is
executed. The input value of this step is arbitrary and gets stored in
$pc_{t}$ by setting it to $doOp(in)$.

  * •

Second, a step with internal action $do_{t}(op)$ is executed. This step will
correspond to the linearization point of an implementation. The step modifies
the state of $op$ by choosing a new state and an output according to the
specification of $op$ (the step is not possible if there is no
$s^{\prime},out^{\prime}$ with $op(in,s,s^{\prime},out^{\prime})$). The
computed output is again stored in $pc_{t}$ by setting it to $resOp(out)$.

  * •

Finally, a response step, that returns the $out$ value that was stored in
$pc_{t}$ by emitting an action $resOp(out)$. This step finishes the execution
of $op$ by setting $pc_{t}$ to ready.

The durable canonical automaton (more details are in [DDD+19]) is an extension
of the canonical automaton from [Lyn96] for linearizability to accommodate
durable linearizability. It is the most general specification of concurrent
runs that still allows to construct an equivalent sequential history: the
sequential history can be constructed as a sequence of invoke-response pairs
from the sequence of executed $do_{t}(op)$ steps. The automaton guarantees
that this sequential history is obviously in $H_{\mathbb{S}}$.

$\begin{array}[t]{ll}\lx@intercol inv_{t}(op(in))\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=ready\\\ \textsf{Eff: }&pc_{t}:=doOp(in)\end{array}$ | $\begin{array}[t]{ll}\lx@intercol do_{t}(op)\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=doOp(in)\\\ \textsf{Eff: }&(s,out):=SOME(s^{\prime},out^{\prime}).\\\ &\qquad\quad\qquad\quad op(in,s,s^{\prime},out^{\prime})\\\ &pc_{t}:=resOp(out)\end{array}$ | $\begin{array}[t]{ll}\lx@intercol\mathit{res}_{t}(op(out))\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=resOp(out)\\\ \textsf{Eff: }&pc_{t}:=ready\end{array}$
---|---|---
$\begin{array}[t]{ll}\lx@intercol run_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=notStarted\\\ \textsf{Eff: }&pc_{t}:=ready\end{array}$ | $\begin{array}[t]{ll}\lx@intercol crashRecovery\hfil\lx@intercol\\\ \textsf{Pre: }&true\\\ \textsf{Eff: }&pc:=\lambda t:T.\\\ &\quad\textbf{if\ }pc_{t}\neq idle\textbf{\ then\ }crashed\\\ &\qquad\qquad\quad\qquad\textbf{else\ }pc_{t}\end{array}$ |
Figure 1: Durable automaton $\textsc{DurAut}(\mathbb{S})$

###  3.3 Refinement in context

For our modular proof technique, we will let an STM algorithm call a library
in order to manage access to shared state. As both STM and library will be
given by IOA, we need some notion of a context automaton using a library
automaton. To this end, we employ the following definition of product
automaton [Lyn96] which requires synchronisation of two IOA on shared external
actions.

######  Definition .

Let A, B be two IOA with no shared internal actions. Then the product
automaton $A\times B$ is defined to have

  * •

states($A\times B$) = $states(A)\times states(B)$,

  * •

start($A\times B$) = $start(A)\times start(B)$,

  * •

acts($A\times B$) = $acts(A)\union acts(B)$,

  * •

$(as,bs)\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{A\times
B}(as^{\prime},bs^{\prime})$ iff the following two properties hold:
if $a\in actions(A)$, then $as\stackrel{{\scriptstyle
a}}{{\longrightarrow}}_{A}as^{\prime}$, else $as^{\prime}=as$;
if $a\in actions(B)$, then $bs\stackrel{{\scriptstyle
a}}{{\longrightarrow}}_{B}bs^{\prime}$, else $bs^{\prime}=bs$.

In the following we will use this product construction in an asymmetric way:
the only shared external actions of $A$ (the library) and $B$ (the STM
algorithm) are the invocations and responses of library calls, and the library
is furthermore required to have no further external actions. In such a
setting, we write $B[A]$ for the product of $A$ and $B$ (IOA $B$ is using
library automaton $A$).

Later we will develop two versions of the library which provides access to
shared memory: one with and one without volatile memory. These two versions
are shown to be a refinement of each other (more precisely, one version is
shown to be durable linearizability wrt. the other), and we need to lift this
result to STMs using the libraries. It is folklore knowledge that refinement
of an abstract object by a concrete object implies refinement between an
algorithm (a context) using the abstract object and the same algorithm using
the concrete one. Theorems stating such a property have been proven in many
settings, e.g. for data refinement in [dRE98]. The fundamental paper on
linearizability [HW90] implicitly uses such a result when it assumes that the
individual steps of algorithms are linearizable operations as well. We could
however not find a formal proof for IOA and thus state and show it in this
setting.

######  Theorem .

If $C\leq A$, then $B[C]\leq B[A]$.

Proof sketch. To prove refinement, we need to construct an execution of $B[A]$
with the same trace (i.e. the same external events), when given an execution
of $B[C]$. The execution of $B[C]$ contains an execution of $C$ by projecting
to the states of $C$ and removing all steps where $C$ is not involved. This
execution can be split into finite segments of internal $C$-steps that each
end with an external shared action (with possibly a final sequence of internal
$C$-steps, that is not used). By refinement there exists an execution of A
with the same external actions. This execution can be split in the same way.
Now delete the internal $C$-steps from the combined execution of $B[C]$, and
replace the $C$-step in each combined step of $C$ and $B$ with the
corresponding $A$-step from the abstract execution. Add the sequence of
internal $A$-steps that leads to this step right before the combined step in
the combined execution. The result is an execution of $B[A]$ which has the
same trace as the original execution. $\Box$

###  3.4 IOA for dTMS2

In this section, we describe the dTMS2 specification, an operational model
that ensures durable opacity, which is based on TMS2 [DGLM13]. TMS2 itself has
been shown to strictly imply opacity [LLM12b], and hence has been widely used
as an intermediate specification in the verification of transactional memory
implementations [ADD17, DDS+15, AD17, DDD+16].

In the following, we let $f\oplus g$ denote functional override of $f$ by $g$,
e.g., $f\oplus\\{x\mapsto u,y\mapsto v\\}=\lambda k.\ {\bf if}\ k=x\ {\bf
then}\ u\ {\bf elseif}\ k=y\ {\bf then}\ v\ {\bf else}\ f(k)$. Note that the
transition relation in IOA is typically defined by giving the actions in a
precondition-effect style fixing an enabling condition for an action and its
state changes.

State variables:
$mems:seq(L\to V)$, initially satisfying $\dom mems=\\{0\\}$
$pc_{t}:PCVal$, for each $t\in T$, initially $pc_{t}=\text{notStarted}$ for
all $t\in T$
$beginIdx_{t}:{\rm Nature}$ for each $t\in T$, unconstrained initially
$rdSet_{t}:L\pfun V$, initially empty for all $t\in T$
$wrSet_{t}:L\pfun V$, initially empty for all $t\in T$
Transition relation:
$\begin{array}[t]{ll}\lx@intercol
inv_{t}(\texttt{TMBegin})\hfil\lx@intercol\\\ \textsf{Pre:
}&pc_{t}=\text{notStarted}\\\ \textsf{Eff: }&pc_{t}:=\text{beginPending}\\\
&beginIdx_{t}:=len(mems)-1\end{array}$ $\begin{array}[t]{ll}\lx@intercol
res_{t}(\texttt{TMBegin})\hfil\lx@intercol\\\ \textsf{Pre:
}&pc_{t}=\text{beginPending}\\\ \textsf{Eff:
}&pc_{t}:=\text{ready}\end{array}$ $\begin{array}[t]{ll}\lx@intercol
inv_{t}(\texttt{TMRd}(l))\hfil\lx@intercol\\\ \textsf{Pre:
}&pc_{t}=\text{ready}\\\ \textsf{Eff: }&pc_{t}:=\text{doRead}(l)\end{array}$
$\begin{array}[t]{ll}\lx@intercol
res_{t}(\texttt{TMRd}(v))\hfil\lx@intercol\\\ \textsf{Pre:
}&pc_{t}=\text{resRead}(v)\\\ \textsf{Eff: }&pc_{t}:=\text{ready}\end{array}$
$\begin{array}[t]{ll}\lx@intercol
inv_{t}(\texttt{TMWr}(l,v))\hfil\lx@intercol\\\ \textsf{Pre:
}&pc_{t}=\text{ready}\\\ \textsf{Eff:
}&pc_{t}:=\text{doWrite}(l,v)\end{array}$ $\begin{array}[t]{ll}\lx@intercol
res_{t}(\texttt{TMWr})\hfil\lx@intercol\\\ \textsf{Pre:
}&pc_{t}=\text{resWrite}\\\ \textsf{Eff: }&pc_{t}:=\text{ready}\end{array}$
$\begin{array}[t]{ll}\lx@intercol
inv_{t}(\texttt{TMCommit})\hfil\lx@intercol\\\ \textsf{Pre:
}&pc_{t}=\text{ready}\\\ \textsf{Eff: }&pc_{t}:=\text{doCommit}\end{array}$
$\begin{array}[t]{ll}\lx@intercol
res_{t}(\texttt{TMCommit})\hfil\lx@intercol\\\ \textsf{Pre:
}&pc_{t}=\text{resCommit}\\\ \textsf{Eff:
}&pc_{t}:=\text{committed}\end{array}$ $\begin{array}[t]{ll}\lx@intercol
res_{t}(op(\texttt{abort}))\hfil\lx@intercol\\\ \textsf{Pre:
}&pc_{t}\notin\\{\text{notStarted},\text{ready},\\\
&\text{resCommit},\text{committed},\text{aborted}\\}\\\ \textsf{Eff:
}&pc_{t}:=\text{aborted}\end{array}$
$\begin{array}[t]{ll}\lx@intercol\texttt{DoWrite}_{t}(l,v)\hfil\lx@intercol\\\
\textsf{Pre: }&pc_{t}=\text{doWrite}(l,v)\\\ \textsf{Eff:
}&pc_{t}:=\text{resWrite}\\\ &wrSet_{t}:=wrSet_{t}\oplus\\{l\to
v\\}\end{array}$
$\begin{array}[t]{ll}\lx@intercol\texttt{DoCommitReadOnly}_{t}(n)\hfil\lx@intercol\\\
\textsf{Pre: }&pc_{t}=\text{doCommit}\\\ &\dom(wrSet_{t})=\emptyset\\\
&validIdx(t,n)\\\ \textsf{Eff: }&pc_{t}:=\text{resCommit}\end{array}$
$\begin{array}[t]{ll}\lx@intercol\texttt{DoCommitWriter}_{t}\hfil\lx@intercol\\\
\textsf{Pre: }&pc_{t}=\text{doCommit}\\\ &rdSet_{t}\subseteq last(mems)\\\
\textsf{Eff: }&pc_{t}:=\text{resCommit}\\\ &mems:=mems\cat(last(mems)\oplus
wrSet_{t})\end{array}$
$\begin{array}[t]{ll}\lx@intercol\texttt{DoRead}_{t}(l,n)\hfil\lx@intercol\\\
\textsf{Pre: }&pc_{t}=\text{doRead}(l)\\\ &l\in\dom(wrSet_{t})\vee
validIdx(t,n)\\\ \textsf{Eff: }&\texttt{if}\ l\in\dom(wrSet_{t})\
\texttt{then}\\\ &\ \ \ pc_{t}:=\text{resRead}(wrSet_{t}(l))\\\
&\texttt{else}\ v:=mems(n)(l)\\\ &\ \ \ \ \ \ \ \ pc_{t}:=\text{resRead}(v)\\\
&\ \ \ \ \ \ \ \ rdSet_{t}:=rdSet_{t}\oplus\\{l\to v\\}\end{array}$
$\begin{array}[t]{ll}\lx@intercol crashRecovery\hfil\lx@intercol\\\
\textsf{Pre: }&true\\\ \textsf{Eff: }&pc:=\lambda t:T.\\\ &\qquad\texttt{if}\
pc_{t}\notin\\{notStarted,committed\\}\\\ &\qquad\texttt{then}\ aborted\\\
&\qquad\texttt{else}\ pc_{t}\\\ &mems:=\langle last(mems)\rangle\end{array}$

where
$\begin{array}[t]{r@{~~}c@{~~}l}PCExternal~{}~{}&\sdef\hfil~{}~{}&\\{\text{notStarted},\text{ready},\text{resCommit},\text{resWrite},\text{committed},\text{aborted}\\}\cup{}\\\
~{}~{}&\hfil~{}~{}&\\{\text{resRead}(v)\mid v\in V\\}\\\
PCVal~{}~{}&\sdef\hfil~{}~{}&PCExternal\cup\\{\text{beginPending},\text{doCommit},\text{cancelPending}\\}\\\
~{}~{}&\hfil~{}~{}&{}\cup\\{\text{doRead}(l)\mid l\in
L\\}\cup\\{\text{doWrite}(l,v)\mid l\in L,v\in V\\}\\\\[2.84526pt]
validIdx(t,n)~{}~{}&\sdef\hfil~{}~{}&beginIdx_{t}\leq n<len(mems)\wedge
rdSet_{t}\subseteq mems(n)\\\ op~{}~{}&\in\hfil~{}~{}&\\{{\tt TMBegin},{\tt
TMRd},{\tt TMWr},{\tt TMCommit}\\}\end{array}$

Figure 2: The state space and transition relation of dTMS2, which extends TMS2
with a crash-recovery event

Formally, dTMS2 is specified by the IOA in Fig. 2, which describes the
required ordering constraints, memory semantics and prefix properties. We
assume a set $L$ of locations and a set $V$ of values. Thus, a memory is
modelled by a function of type $L\to V$. A key feature of dTMS2 (like TMS2) is
that it keeps track of a sequence of memory states, one for each committed
writing transaction. This makes it simpler to determine whether reads are
consistent with previously committed write operations. Each committing
transaction containing at least one write adds a new memory version to the end
of the memory sequence. However, unlike TMS2, following [DDD+19], the memory
state is considered to be the persistent memory state. Interestingly, the
volatile memory state need not be modelled.

The state space of dTMS2 has several components. The first, $mems$ is the
sequence of memory states. The original specification of TMS2 is parameterized
by some initialization predicate for $mem$ which we elide here for simplicity
(and simply assume the implementation to employ the same initialization). For
each transaction $t$ there is a program counter variable $pc_{t}$, which
ranges over a set of program counter values, which are used to ensure that
each transaction is well-formed, and to ensure that each transactional
operation takes effect between its invocation and response. There is also a
begin index variable $beginIdx_{t}$, that is set to the index of the most
recent memory version when the transaction begins. This variable is critical
to ensuring the real-time ordering property between transactions. Finally,
there is a read set, $rdSet_{t}$, and a write set, $wrSet_{t}$, which record
the values that the transaction has read and written during its execution,
respectively.

The read set is used to determine whether the values that have been read by
the transaction are consistent with the same version of memory (using
$validIdx$). The write set, on the other hand, is required because writes in
dTMS2 are modelled using deferred update semantics: writes are recorded in the
transaction’s write set, but are not published to any shared state until the
transaction commits.

The $crashRecovery$ action models the effect of crashes and consecutive
recoveries. It sets the program counter of every in-flight transaction to
$aborted$, which prevents these transactions from performing any further
actions in the era following the crash (for the generated history). Note that
since transaction identifiers are not reused, the program counters of
completed transactions need not be set to any special value (e.g., $crashed$)
as with durable linearizability [DDD+19]. Moreover, after restarting, it must
not be possible for any new transaction to interact with memory states prior
to the crash. We therefore reset the memory sequence to be a singleton
sequence containing the last memory state prior to the crash.

The external actions of dTMS2 are all invocation and response actions
($inv_{t}$ and $res_{t}$) plus the new $crashRecovery$ action. The latter is
the crash action $c$ of histories. Note that the traces of dTMS2 hence take
the form of histories.

The following theorem ensures that dTMS2 can be used as an intermediate
specification in our proof method.

######  Theorem .

Each trace of dTMS2 is durably opaque.

The proof of this theorem can be found in the appendix of [BDD+20].

##  4 A Modular Proof Technique

In this section, we present a new approach to verifying durable opacity that
allows one to leverage existing simulation-based proofs of opacity (see
Section 4.1). An overview of the proof steps are described in Fig. 3. Given an
existing opacity proof (step (1)) that uses simulation against TMS2, the
majority of the effort in the modularised proof method is the development of
libraries $AM$ and $CM$ that handle memory operations and a proof of durable
linearizability between the two. We exemplify this proof technique on a
durable version of the STM algorithm NOrec which we newly develop below.

TMS2$\mathcal{S}$$\geq$1(prove)dTMS2$\mathcal{T}$$\geq$3(check)\+
crash2$\mathcal{T}[AM]$$AM$modularise4$\mathcal{T}[CM]$$CM$$\geq$
(prove)5replaceTheorem 3.3 Figure 3: Overview of proof steps

###  4.1 Overview of proof technique

  1. 1.

Our modular proof method starts with an existing simulation-based proof
between an STM implementation, $\mathcal{S}$, and TMS2, which establishes
opacity of $\mathcal{S}$. In our example case study, we consider NOrec, which
has already been proven correct with respect to TMS2. Our primary motivation
for the new approach is to develop a durable version of an already opaque
algorithm and avoid full re-verification of the durable version (against
dTMS2).

  2. 2.

To make sense of the adaptation of $\mathcal{S}$ to persistent memory, we
start by assuming $\mathcal{S}$ runs directly on persistent memory, i.e., all
memory accesses are persistent, and there is no notion of volatile memory.
Hence, there are no flush operations that transfer memory contents from
volatile to persistent memory. Of course, $\mathcal{S}$ also does not contain
a notion of a crash-recovery operation since it has been designed to be opaque
as opposed to durably opaque.

This step of the transformation therefore is to define a new version of
$\mathcal{S}$, say $\mathcal{T}$, that extends $\mathcal{S}$ with a “crash-
recovery” operation. The purpose of this operation is to crash any live
transactions so that they are no longer able to execute and to reset the state
into a state consistent with initialisation. We will require that the crash-
recovery introduced into $\mathcal{T}$ is a refinement of the $crashRecovery$
operation of dTMS2 from Fig. 2. Note that the only difference between TMS2 and
dTMS2 is the $crashRecovery$ operation. We will therefore require that the
crash-recovery operation introduced to transform $\mathcal{S}$ to
$\mathcal{T}$ is compatible with $crashRecovery$.

  3. 3.

The next step is to verify that the transformed algorithm $\mathcal{T}$ is
durably opaque. To do this, we must adapt the existing simulation proof
between $\mathcal{S}$ and TMS2 to prove simulation between $\mathcal{T}$ and
dTMS2. Recall that the transformation from both $\mathcal{S}$ to $\mathcal{T}$
and TMS2 to dTMS2 involves the introduction of a crash-recovery operation.
Also recall that we assume both algorithms run directly on persistent memory,
and no volatile memory is assumed in either case. Therefore, the effect of
this crash-recovery operation in both cases is straightforward, and the
adaptation of the proof is therefore straightforward too.

  4. 4.

A key insight in our proof technique is the use of an external library that
handles such memory operations. We therefore in the next step adapt
$\mathcal{T}$ so that it relegates all memory operations (read, write, and
commit write-back) to an external library. We call this adapted algorithm
$\mathcal{T}[~{}]$, which is $\mathcal{T}$ but with calls to external
operations that manage memory interactions. We must additionally develop a
data type (library automaton), $AM$, that handles these memory events. This
enables one to define a composition $\mathcal{T}[AM]$ (via a product of two
IOA), where the library used by $\mathcal{T}[~{}]$ is $AM$.

There are two requirements for the library $AM$.

    1. (a)

We must be able to show that the traces of $\mathcal{T}[AM]$ are a subset of
the traces of $\mathcal{T}$, i.e., $\mathcal{T}[AM]$ is a trace refinement of
$\mathcal{T}$. Note that by transitivity of refinement this means that the
composition $\mathcal{T}[AM]$ will be durably opaque.

    2. (b)

We must allow $AM$ to be implemented by a concrete memory library that uses
both a volatile and persistent memory so that the algorithm can ultimately be
implemented in a non-volatile memory architecture.

To satisfy both criteria while keeping the proof burden light, we make $AM$ an
atomic object, i.e., reads, writes, and write-backs are coarse-grained atomic
operations. Moreover $AM$ operates directly on persistent memory, i.e., it
does not use volatile memory. With these restrictions in place, it becomes
straightforward to show trace refinement between the traces of $\mathcal{T}$
and $\mathcal{T}[AM]$.

  5. 5.

In this step, we develop $CM$, a durably linearizable implementation of $AM$,
comprising a fine-grained concurrent memory library that operates over both
volatile memory and persistent memory. The library $CM$ manages (persistent)
logging to undo partially completed operations (in case of a crash and
recovery) and flushing to ensure operations on volatile memory are made
persistent.

More importantly, as a consequence of Theorem 3.3 we obtain a trace refinement
property: the traces of $\mathcal{T}[CM]$ projected onto the operations of
$\mathcal{T}$ only (i.e., ignoring the library calls) are a subset of the
traces of $\mathcal{T}[AM]$ projected onto the operations of $\mathcal{T}$.

In the sequel we illustrate all these steps on the software transactional
memory algorithm NOrec (no ownership records [DSS10]).

###  4.2 Step 1: NOrec

As a starting point, we have NOrec which resembles $\mathcal{S}$ in the
following. NOrec (given in Figure 4 as an algorithm) employs a deferred update
strategy: writes to shared state are first of all stored in a write set and at
commit time written to main memory – if there are no conflicts with other
transactions. For conflict detection, NOrec uses value-based validation (see
the operation `TMValidate`).

More detailedly, for synchronisation NOrec uses a global counter glb
(initially $0$) and a local variable loc, which is used to store a copy of
glb. Each transaction obtains a local write set wrSet and a local read set
rdSet. Inside its wrSet a transaction records all the addresses that it
attempts to update and their values. The actual update of the memory takes
place inside the commit operation. An odd glb indicates that a live writing
transaction attempts to commit. After a successful commit glb is incremented
by two. glb being not equal to the loc value of a living transaction indicates
that a writing transaction committed. Inside its rdSet, a transaction records
the addresses that it reads and their corresponding values. Every time that a
transaction attempts to read an address which is not inside its wrSet, and loc
$\neq$ glb, the validation method is called. The validation method waits until
the global lock is not held and uses the rdSet to check whether or not the
transaction is still valid. In the case of writing transactions, the
consistency of the rdSet is also checked at the commit stage. Since NOrec
obtains a lazy version management, writes are not visible to the other
transactions, until the writing transaction commits.

Operation `TMBegin` copies the value of glb into its local variable loc and
checks whether glb is even. If this is so, the transaction is started.
Otherwise, a writing transaction is in progress and obtains the lock, so the
process attempts to start again by rereading loc. The operation `TMValidate`
checks if the transaction’s rdSet is consistent with the current state of
memory111Here, we have modified the original NOrec algorithm and also check
$time_{t}=glb$ at V5. This ensures that aborts only occur when the value in
the read set is inconsistent with shared memory while there is no concurrent
writer. This is necessary for our modular proof technique, but does not affect
opacity of NOrec.. If so, it updates its local variable’s value, time, by
assigning to it the current value of glb. `TMRead` firstly checks if the
transaction has written the address that attempt to read, and in case that
this is true, it returns the address’ value by reading it from its wrSet. Then
it checks if loc is up to date, i.e. equal to glb. If it is not up to date, it
means that another transaction has updated the memory and rdSet should be
checked to ensure that its values are consistent with the current state of the
memory. The check is performed by calling the operation `TMValidate`. If the
rdSet is found consistent, the loc is updated with the value of time that
`TMValidate` returns (R4).The (address, value) pair is then added in rdSet for
future validation (R6). Finally, the value of the read address is returned. If
the rdSet is not found consistent, the transaction aborts. `TMWrite` adds the
(address, value) pair that is to be written at the wrSet of the transaction.
The memory is updated at the commit stage. The operation `TMCommit` first
checks if the transaction is a read-only transaction. If it is, then no
further checking is required and the transaction commits at E1 (linearization
point for read-only transactions). If it is not, E2 checks whether a
concurrent writing transaction has been committed. If no such commit has
occured, the CAS at E2 succeeds loc = glb, so glb becomes odd (meaning that
the writing transaction obtains the lock). The memory is then updated at E6.
If the CAS does not succeed it means that a concurrent writing transaction has
been committed and rdSet needs further validation. E3 validates `rdSet` and
updates the value of loc. By this, it prepares the transaction for another
commit attempt. At E5 the memory is updated. At E6 the transaction stops to
obtain the lock by making the glb value even again (linearization point for
writing transactions).

⬇

Init:

I1 glb := 0

TMBegint:

B1 do $loc_{t}$ $\leftarrow$ glb;

B2 until even($loc_{t}$)

return ok;

TMReadt(addr):

R1 if addr $\in$ dom($wrSet_{t}$) then

return $wrSet_{t}(addr)$

R2 $v_{t}$ := *addr

R3 while $loc_{t}$ $\neq$ glb

R4 $loc_{t}$ := TMValidatet

R5 $v_{t}$ := *addr

R6 $rdSet_{t}$.insert(addr,$v_{t}$);

return $v_{t}$

TMWritet(addr,val):

W1 $wrSet_{t}$.insert(addr,val)

return ok;

⬇

TMCommitt:

E1 if $\neg$ $wrSet_{t}$.isEmpty()

then return;

E2 while !cas(glb, $loc_{t}$, $loc_{t}$ + 1)

E3 $loc_{t}$ := TMValidatet

E4 for $\all$ addr. (addr,val) $\in$ $wrSet_{t}$

E5 *addr := val

E6 glb := $loc_{t}$ + 2;

return ok;

TMValidatet:

V1 while true

V2 $time_{t}$ := glb

V3 if odd($time_{t}$) then goto V2

V4 for $\all$ (addr,val) $\in$ $rdSet_{t}$ do

V5 if *addr $\neq$ val $\wedge$ $time_{t}$ = glb

then abort

V6 if $time_{t}$ = glb

then return $time_{t}$

Figure 4: The NOrec algorithm. Line numbers for return statements are omitted.

Correctness of NOrec has been verified by Lesani et al. [LLM12a] using the
theorem prover PVS. The proof proceeds via showing a refinement relationship
(simulation relation) between NOrec and TMS2 [DGLM13]. For the proof, NOrec is
first of all transformed into an IOA. Here, we only exemplify this on one
operation, TMWrite with one statement W1. The operation is split into three
actions, an invocation and a response action (both external) plus a do action
(internal).

$\begin{array}[t]{ll}\lx@intercol
inv_{t}(\texttt{TMWr}(l,v))\hfil\lx@intercol\\\ \textsf{Pre:
}&pc_{t}=\text{ready}\\\ \textsf{Eff:
}&pc_{t}:=\text{doWrite}(l,v)\end{array}\begin{array}[t]{ll}\lx@intercol{\tt
DoWrite}_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{doWrite}(l,v)\\\
\textsf{Eff: }&pc_{t}:=\text{resWrite}\\\
&wrSet_{t}:=wrSet_{t}\oplus\\{l\rightarrow
v\\}\end{array}\begin{array}[t]{ll}\lx@intercol
res_{t}(\texttt{TMWr})\hfil\lx@intercol\\\ \textsf{Pre:
}&pc_{t}=\text{resWrite}\\\ \textsf{Eff: }&pc_{t}:=\text{ready}\end{array}$

The proof of refinement between NOrec and TMS2 is carried out via the
construction of a sequence of IOA in between TMS2 and NOrec, and a sequence of
simulation proofs from one to the next automaton on this sequence. We will not
give all the details of this proof here, rather concentrate on the key
concepts.

Overall, the proof uses the property that synchronisation via `glb` achieves
mutual exclusion between writing transactions:

$\displaystyle\forall t:T.\ $ $\displaystyle pc(t)\in\\{E4,E5,E6\\}$
$\displaystyle\implies glb=loc_{t}+1$ (2) $\displaystyle\quad{}\wedge\forall
t^{\prime}:T.\ t=t^{\prime}\vee pc(t^{\prime})\notin\\{E4,E5,E6\\}$

Here, $pc(t)$ refers to the program counter of transaction $t$ (pointing to
some program location in the algorithmic representation of NOrec, like E1) and
$loc_{t}$ to $t$’s local version of $loc$. The invariant states that we cannot
have two transactions doing their write backs at the same time. This is
basically the invariant snapshotWhenWritingBack of the addendum to
[LLM12a]222PVS file NOrecPaperPseudocode.pvs at
https://www.cs.ucr.edu/~lesani/companion/concur12/index.html.

The (main) relation $R\subseteq states(\text{\sc TMS2})\times states(\text{\sc
NOrec})$ used to show the simulation between TMS2 and NOrec takes the
following form333PVS file NOrecAtomicCommitValidateToTMS2.pvs:

”PCs match” (3) $\displaystyle{}\wedge as.last(mem)=cs.currMem$ (4)
$\displaystyle{}\wedge as.wrSet=cs.wrSet$ (5) $\displaystyle{}\wedge
as.rdSet=cs.rdSet$ (6)

Here, $as$ is the abstract state of TMS2 and $cs$ the concrete state of NOrec,
both seen as IOA, and $currMem$ refers to the current memory state of NOrec,
i.e., the contents of memory locations which are accessed via addresses.
Condition (3) says that in abstract (TMS2) and concrete (NOrec) states related
via $R$, the program counters have to match (e.g., when a transaction $t$ in
TMS2 has $pc_{t}=doCommit$, $pc(t)$ in NOrec is in $\\{E1,\ldots,E6\\}$). As
we do not give a full IOA version of NOrec here, we do not detail the exact
relation between the program counters of TMS2 and NOrec. Condition (4) states
that the last element in the sequence of memory functions $mem$ coincides with
the actual memory of NOrec. Finally, conditions (5) and (6) require write and
read sets of the threads to coincide in TMS2 and NOrec.

###  4.3 Step 2: Defining NOrec with crash and recovery

Next, we introduce an additional action to NOrec which abstractly models the
occurrence of a crash and the following recovery operation. As we still assume
that there is only persistent memory, the recovery part is almost empty. This
operation has two tasks: (1) to ensure that no transaction ”survives” crashes,
i.e., the currently running transactions cannot continue their operations, and
(2) to bring the meta data (i.e., glb) back to the initial state. Task (1)
simulates crashes and (2) the following recovery operation. We directly give
the additional operation in an IOA style, i.e., again with precondition and
effect.

$\begin{array}[t]{ll}\lx@intercol crashRecovery\hfil\lx@intercol\\\
\textsf{Pre: }&true\\\ \textsf{Eff: }&pc:=\lambda t\in T.\ \texttt{if}\
pc_{t}\notin\\{notStarted,committed\\}\ \texttt{then}\ aborted\ \texttt{else}\
pc_{t}\\\ &glb:=0\end{array}$

We call this enhanced NOrec algorithm cNOrec (i.e., NOrec with crash-
recovery). It resembles $\mathcal{T}$ in the description of our approach of
Fig. 3.

###  4.4 Step 3: Checking cNOrec refines dTMS2

Before we look at cNOrec and its relation to dTMS2, we first need to show that
bNOrec is a refinement of dTMS2, thereby establishing its durable opacity.
This is straightforward to check since the only new operation is the crash-
recovery, which preserves the original simulation relation used in the
original proof.

######  Lemma .

$\text{\sc cNOrec}\leq\text{\sc dTMS2}$.

For this, we can re-use the existing simulation between NOrec and TMS2. First,
we see that the additional operation in cNOrec does not invalidate the
invariant: after operation $crashRecovery$, the program counters of all
threads are either $aborted$ or in $\\{notStarted,committed\\}$. Thus the
invariant is trivially fulfilled.

Second, we check whether the relation $R$ is still a valid simulation
relation. To this end, we check the external step correspondence condition for
the newly introduced operation $crashRecovery$. Conditions $(\ref{R3})$ and
$(\ref{R4})$ are satisfied since read and write sets of abstract and concrete
state are not modified by the abstract and concrete $crashRecovery$ action.
Condition $(\ref{R2})$ is fulfilled because $crashRecovery$ in dTMS2 sets
$mems$ to $\langle last(mems)\rangle$, hence leaves $last(mems)$ untouched.
Finally, condition $(\ref{R1})$ in the relation $R$ is preserved because the
program counters of threads are either preserved (and hence still match) or –
for the in-flight transactions – are set to $aborted$ in both concrete and
abstract automaton. So, we can use exactly the same relation $R$ for proving
refinement between dTMS2 and bNOrec as we have used before.

###  4.5 Step 4: Modularising cNOrec and defining $AM$

⬇

TMBegint:

B1 do $loc_{t}$ $\leftarrow$ glb;

B2 until even($loc_{t}$)

return ok;

TMReadt(addr):

R1 if addr $\in$ dom($wrSet_{t}$) then

return $wrSet_{t}(addr)$

R2 $v_{t}$ = LibReadt(addr)

R3 while $loc_{t}$ $\neq$ glb

R4 $loc_{t}$ := TMValidatet

R5 $v_{t}$ := LibReadt(addr)

R6 $rdSet_{t}$.insert(addr,$v_{t}$);

return $v_{t}$

CrashRecovery:

R1 atomic {

LibRecovery;

glb := 0; }

TMWritet(addr,val):

W1 $wrSet_{t}$.insert(addr,val);

return ok;

⬇

TMCommitt:

E1 if $\neg$ $wrSet_{t}$.isEmpty()

then return;

E2 while !cas(glb, $loc_{t}$, $loc_{t}$ + 1)

E3 $loc_{t}$ := TMValidatet

E4 LibAcquiret

E5 LibCommitt($wrSet_{t}$)

E6 LibReleaset

E7 glb := $loc_{t}$ + 2;

return ok;

TMValidatet:

V1 while true

V2 $time_{t}$ := glb

V3 if odd($time_{t}$) then goto V2

V4 for $\all$ (addr,val) $\in$ $rdSet_{t}$ do

V5 if LibReadt(addr) $\neq$ val

$\wedge$ $time_{t}$ = glb

then abort

V6 if $time_{t}$ = glb

then return $time_{t}$

Figure 5: The $\text{\sc cNOrec}[~{}]$ algorithm with library calls that
relegate memory operations to a library

Next, we modularise cNOrec by calling a library instead of directly accessing
shared memory. The modularised algorithm cNOrec is given in Fig. 5, where
reads from memory in lines R2, R5 and V5 are processed through LibRead
operations that return the value of the given address from memory. When this
library is abstract (see Fig. 6), the reads are from persistent memory,
whereas in the concrete implementation (see Fig. 7), the reads will return
values from volatile memory. The write-back loop in lines E4 and E5 of Fig. 4
is replaced by a call to a write-back operation LibCommitt($wrSet_{t}$), which
commits the writes in the given write set, $wrSet_{t}$, to memory.

The crash-recovery operation makes a call to the recovery operation of the
library, LibRecovery. The LibRecovery operation at the abstract level (Fig. 6)
is a skip (or no-op) since $AM$ executes directly over NVM (and there is
nothing to recover). At the concrete level (Fig. 7), we introduce an atomic
recovery operation that resets the volatile memory to the persistent memory,
then persistently undoes any incomplete write-backs. For simplicity, we keep
the recovery operation atomic; following a system crash, we assume all
transactional operations will wait until recovery is completed. It is possible
to separately refine the atomic recovery process (in a manner that is immune
to crashes during recovery) in a separate step, but we do not discuss such a
recovery operation in detail in this paper.444In the KIV formalisation the
recovery operation is already defined by an atomic program that resets the
volatile memory and undoes any logged writes.

We also note that the TMCommit operation in Fig. 5 contains two operations
LibAcquiret and LibReleaset. These operations enforce an ownership-based
discipline that ensures the library never has to deal with concurrent commits,
which is essential to enable development of a durably linearizable concrete
memory library (see Section 4.6). Their introduction makes no difference to
the behaviour of the NOrec (and hence the cNOrec) algorithm since the write-
back with in the commit operation takes place under the mutual-exclusion
invariant (2). Thus, the use of LibAcquiret and LibReleaset is purely
auxiliary.

Since LibAcquiret and LibReleaset occur before and after a write-back, they
are also used to ensure that reads return a legitimate value. As we shall see
below, the abstract LibReadt operation only returns the value from memory if
no write-back operation is in progress. If there is a write-back in progress,
since the read operation will need to be re-validated, the read operation can
simply return a random value.

We now define the library corresponding to the abstract memory $AM$, as given
in Fig. 6. The library describes models of operations LibAcquire and
LibRelease, which guarantee exclusive access to the write-back, as described
above. In particular, we use a shared variable $owns$555Actually, the same
technique has been used in Lesani et al.’s opacity proof for NOrec: In the
abstract model of NOrec (file NOrec.pvs) the state contains a variable
commitLock which is set before writing back values and later released. This
model of NOrec has been shown to be a refinement of the pseudocode for NOrec
(file NOrecPaperPseudocodeToNOrec.pvs)., whose value is either the identifier
of the transaction that owns the lock, or $\bot$ to indicate that no thread
owns the lock. A read simply returns the value of the given address from
(persistent) memory, $mem$, provided no writing transaction is performing a
write-back. If the read detects that a write-back is executing it returns a
random value; in the context of NOrec, this does not introduce new behaviours
since the read that occurs during the write-back in another transaction causes
the read to be re-validated. The write-back overwrites the values in $mem$ by
the write set of the transaction in a single atomic step. The idea of using
ownership in an interface to enforce atomicity has been explored in prior work
[SBPR20].

Using the notation from Section 3.3, $\text{\sc cNOrec}[AM]$ denotes the
program in Fig. 5 using the abstract memory in Fig. 6. The traces of the
composition $\mathcal{T}[~{}]$ include, as external actions, the external
actions of both $\mathcal{T}$ and those of the library $L$, and let
$traces(\mathcal{T}[L])_{|\mathcal{T}}$ denote the traces restricted to just
$\mathcal{T}$. The next lemma (corollary of Theorem 3.3) establishes durable
opacity of $\text{\sc cNOrec}[AM]$.

######  Lemma .

$traces(\text{\sc cNOrec}[AM])_{|\text{\sc cNOrec}}\subseteq traces(\text{\sc
cNOrec})$

This lemma is straightforward to check since the abstract library $AM$ largely
replicates the behaviour of cNOrec. The only exceptions are the following.

  * •

We have used LibAcquire and LibRelease to make it explicit when write-back is
being executed. As explained, above the property being explicitly modelled is
implicitly present in cNOrec, as confirmed by the mutual exclusion property in
the NOrec invariant (2).

  * •

The read operation makes an accommodation to return a random value when there
is a write-back in progress. This is to allow a later refinement of the
library $AM$ by a concrete implementation $CM$ that uses the volatile memory.
This change however does not introduce new behaviours. For LibRead calls at
lines R2 and R5, the presence of another write-back will cause the reader to
re-validate its read set in both $\text{\sc cNOrec}[AM]$ and $\text{\sc
cNOrec}[~{}]$. Similarly, for the LibRead call at line V5 if a write-back is
in progress, then both cNOrec and $\text{\sc cNOrec}[AM]$ will retry the
validation since $time_{t}\neq{\tt glb}$.666Note that without the change to
NOrec introduced in Section 4.2, there would be slight differences in the way
in which validations return with abort. Namely, a validation may fail when
using a library even if the read set being validated is disjoint from the
write set of the write-back operation in another transaction due to the
randomisation introduced in the LibRead operation.

$\begin{array}[t]{ll}\lx@intercol inv_{t}(\texttt{LibAcquire})\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{idle}\\\ \textsf{Eff: }&pc_{t}:=\text{doAcquire}\end{array}$ | $\begin{array}[t]{ll}\lx@intercol res_{t}(\texttt{LibAcquire})\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{resAcquire}\\\ \textsf{Eff: }&pc_{t}:=\text{idle}\end{array}$
---|---
$\begin{array}[t]{ll}\lx@intercol inv_{t}(\texttt{LibRelease})\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{idle}\\\ \textsf{Eff: }&pc_{t}:=\text{doRelease}\end{array}$ | $\begin{array}[t]{ll}\lx@intercol res_{t}(\texttt{LibRelease})\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{resRelease}\\\ \textsf{Eff: }&pc_{t}:=\text{idle}\end{array}$
$\begin{array}[t]{ll}\lx@intercol inv_{t}(\texttt{LibRead}(addr))\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{idle}\\\ \textsf{Eff: }&pc_{t}:=\text{doRead}(addr)\end{array}$ | $\begin{array}[t]{ll}\lx@intercol res_{t}(\texttt{LibRead}(v))\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{resRead}(v)\\\ \textsf{Eff: }&pc_{t}:=\text{idle}\end{array}$
$\begin{array}[t]{ll}\lx@intercol inv_{t}(\texttt{LibCommit}(wrSet_{t}))\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{idle}\\\ &owns=t\\\ \textsf{Eff: }&pc_{t}:=\text{doCommit}(wrSet_{t})\end{array}$ | $\begin{array}[t]{ll}\lx@intercol res_{t}(\texttt{LibCommit}())\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{resCommit}\\\ \textsf{Eff: }&pc_{t}:=\text{idle}\end{array}$
$\begin{array}[t]{ll}\lx@intercol\texttt{DoAcquire}_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{doAcquire}\\\ &owns=\bot\\\ \textsf{Eff: }&pc_{t}:=\text{resAcquire}\\\ &owns:=t\end{array}$ | $\begin{array}[t]{ll}\lx@intercol\texttt{DoRelease}_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{doRelease}\\\ &owns=t\\\ \textsf{Eff: }&pc_{t}:=\text{resRelease}\\\ &owns:=\bot\end{array}$
$\begin{array}[t]{ll}\lx@intercol\texttt{DoRead}_{t}(addr)\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{doRead}(addr)\\\ \textsf{Eff: }&\texttt{if}\ owns=\bot\ \texttt{then}\\\ &\ \ \ v:=mem(addr)\\\ &\texttt{else}\ v:=?\\\ &pc_{t}:=\text{resRead}(v)\end{array}$ | $\begin{array}[t]{ll}\lx@intercol\texttt{DoCommitWrSet}_{t}(wrSet_{t})\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{doCommit}(wrSet_{t})\\\ &owns=t\\\ \textsf{Eff: }&pc_{t}:=\text{resCommit}\\\ &mem:=mem\oplus wrSet_{t}\end{array}$
Figure 6: Transition relation for $AM$ as an input/output automaton; the
LibRecovery operation, which resets $owns$ to $\bot$ is omitted

###  4.6 Step 5: Defining $CM$ and proving durable linearizability

$CM$ shown in Fig. 7 implements $AM$ on an architecture with persistent and
volatile memory: instead of reading and writing directly to a (persistent)
memory $mem$, it first of all writes to some an intermediate volatile cache
$vmem$. Functional correctness is not affected, when all transactions read and
write to the volatile cache $vmem$. However, on a crash the data in the cache
is lost, and computation can only resume from the state of the persistent
memory $pmem$. To ensure opacity, $pmem$ therefore has to be updated at least
in commit, to make sure that the new memory snapshot that results from the
successful commit is available even after a crash.

For a lazy STM implementation like NOrec committing the write set is the only
place in the code which writes to memory, so the implementation changes
updating $mem$ to updating both $vmem$ and $pmem$. Committing part of the
write set followed by a crash is the only place in the code where a crash
would result in a memory state, which is not a snapshot of the successfully
completed transactions. Since a crash during the commit implies that the
transaction is considered to be aborted, the memory updates that have been
done by partially committing the write set must be reverted. To make this
possible, we keep a persistent $log$ that stores old values for those
locations of the write set that have already been committed. On a crash, the
log is used to undo the partial commit777In the automaton, the recovery
executes $vmem:=pmem\oplus log$, the KIV specification uses a recovery program
that writes each log entry separately in a loop.. When the write set has been
fully committed, the log is cleared, and clearing the log becomes the
linearization point of the implementation of commit. After this point the
transaction has successfully committed.

We prove that $CM$ is durable linearizable to $AM$ via showing that $CM$
refines the canonical automaton of $AM$ (see Section 3.2 for canonical
automata and linearizability). Formally, both the IO Automata for $AM$ and for
$CM$ are specified in KIV [EPS+15] by giving labelled programs which generate
a predicate logic specification of the transition relation. Specifications and
proofs are online at [Sch20].

The refinement from $AM$ to $CM$ is proven in two steps. First an invariant
for $CM$ is proven which overapproximates the set of reachable states. The
invariant is then used in place of $reach(C)$ in the proof of a forward
simulation according to Def. 3.1.

The invariant of $CM$ consists of a global invariant and local assertions. The
global invariant

${\bf if}\ owns=\bot\ {\bf then}\ vmem=pmem\land log=\emptyset\ {\bf else}\
vmem\oplus log=pmem\oplus log$

states that as long as there is no writer that commits a write set, volatile
and persistent memory agree, and the log is empty. Otherwise adding the log to
volatile and persistent memory gives the same result: both result in the
memory snapshot at the start of the commit.

The local assertions give formulas that hold when a transaction $t$ is at a
specific $pc_{t}$. As an example, while $t$ is executing the write operation
($pc_{t}$ is one of $W1$ to $W8$) it has write ownership ($owns=t$). The KIV
specification specifies this implication (and many more) as pairs of a label
range and a formula. The full invariant is generated as a conjunction of all
local assertions, that is universally quantified over all $t$, together with
the global invariant. To have a thread-modular proof of the assertions, a rely
predicate $rely(t,s,s^{\prime})$ is specified that the steps of all other
transactions $t^{\prime}\neq t$ (from state $s$ to $s^{\prime}$) must satisfy.
Assertions for thread $t$ and the global invariant are shown to be stable with
respect to this predicate. In our case the rely predicate consists of two
formulas.

$owns=t\rightarrow vmem=vmem^{\prime}\land pmem=pmem^{\prime}\land
owns=owns^{\prime}\land log=log^{\prime})\\\ owns\neq t\rightarrow
owns^{\prime}\neq t$

The first ensures that while a transaction $t$ is writing other transactions
will leave $vmem$, $pmem$, $owns$ and $log$ unchanged. The second guarantees
that steps of other threads cannot make $t$ the writer.

The specification of $CM$ in KIV also fixes the linearization points of $CM$,
by defining non-$\tau$ actions for such steps. Reading linearizes at $R1$,
when the value is read from volatile memory. Committing linearizes at $W8$,
when the log is set to empty.

The forward simulation between $CM$ and $AM$ consists of a global part and a
local part for every transaction $t$ too. The global part simply states that
$owns$ of $AM$ and $CM$ are identical and that the abstract memory $mem$ of
$AM$ is always equal to $vmem\oplus log$ (the invariant implies that it is
then equal to $pmem\oplus log$ as well).

The local part of the simulation for thread $t$ gives a mapping between pc-
values of $CM$ and $AM$ in the obvious way. As an example, since the
linearization point of commit is at $W9$, all $pc_{t}$ values from $W1$ to
$W8$ are mapped to $doCommit(wrSet_{t})$, while $pc_{t}=resCommit$ is mapped
to $resCommit$. The local part of the simulation also ensures that input
received by an operation of $CM$ that is stored in a local variable is equal
to the corresponding input of $AM$, and similar for the outputs.

With this forward simulation, the proof has to show a commuting diagram for
every step of $CM$ according to Definition 3.1. The proofs of this refinement
in KIV are simple. Three days of work were required to set up the
specifications and to do the proofs, which have ca. 300 interactive steps.

$\begin{array}[t]{ll}\lx@intercol\texttt{DoAcquire}_{t}(owns)\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{doAcquire}(owns)\\\ &owns=\bot\\\ \textsf{Eff: }&pc_{t}:=\text{resAcquire}\\\ &owns:=t\end{array}$ | $\begin{array}[t]{ll}\lx@intercol\texttt{DoRelease}_{t}(owns)\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{doRelease}(owns)\\\ &owns=t\\\ \textsf{Eff: }&pc_{t}:=\text{resRelease}\\\ &owns:=\bot\end{array}$
---|---
$\begin{array}[t]{ll}\lx@intercol\texttt{W1}_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{W1}(wrSet)\\\ \textsf{Eff: }&\texttt{if}\ (wrSet\neq\,\emptyset)\,\texttt{then}\\\ &\ \ \ pc_{t}:=\text{W2}(wrSet)\\\ &\texttt{else}\ pc_{t}=\text{W8}\end{array}$ | $\begin{array}[t]{ll}\lx@intercol\texttt{W2}_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{W2}(wrSet)\\\ &SOME\ l.\ l\in dom(wrSet)\\\ \textsf{Eff: }&pc_{t}:=\text{W3}(wrSet,l)\end{array}$
$\begin{array}[t]{ll}\lx@intercol\texttt{W3}_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{W3}(wrSet,l)\\\ \textsf{Eff: }&pc_{t}:=\text{W4}(wrSet,l)\\\ &oldv_{t}:=vmem(l)\end{array}$ | $\begin{array}[t]{ll}\lx@intercol\texttt{W4}_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{W4}(wrSet,l)\\\ \textsf{Eff: }&pc_{t}:=\text{W5}(wrSet,l)\\\ &log:=log\oplus\\{l\to oldv_{t}\\}\end{array}$
$\begin{array}[t]{ll}\lx@intercol\texttt{W5}_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{W5}(wrSet,l)\\\ \textsf{Eff: }&pc_{t}:=\text{W6}(wrSet,l)\\\ &vmem(l):=wrSet(l)\end{array}$ | $\begin{array}[t]{ll}\lx@intercol\texttt{W6}_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{W6}(wrSet,l)\\\ \textsf{Eff: }&pc_{t}:=\text{W7}(wrSet,l)\\\ &pmem(l):=vmem(l)\end{array}$
$\begin{array}[t]{ll}\lx@intercol\texttt{W7}_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{W7}(wrSet,l)\\\ \textsf{Eff: }&pc_{t}:=\text{W1}(wrSet\backslash\\{(l,wrSet(l))\\})\end{array}$ | $\begin{array}[t]{ll}\lx@intercol\texttt{W8}_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{W8}\\\ \textsf{Eff: }&pc_{t}:=\text{resCommit}\\\ &log:=\emptyset\end{array}$
$\begin{array}[t]{ll}\lx@intercol\texttt{R1}_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{R1}(l)\\\ \textsf{Eff: }&\texttt{if}\ (owns=\,t)\,\texttt{then}\ v:=mems(l)\\\ &\texttt{else}\ v:=?\\\ &pc_{t}:=\text{resRead}(v)\end{array}$ | $\begin{array}[t]{ll}\lx@intercol run_{t}\hfil\lx@intercol\\\ \textsf{Pre: }&pc_{t}=\text{notStarted}\\\ \textsf{Eff: }&pc_{t}:=\text{ready}\end{array}$
$\begin{array}[t]{ll}\lx@intercol crashRecovery\hfil\lx@intercol\\\
\textsf{Pre: }&true\\\ \textsf{Eff: }&pc:=\lambda t:T.\texttt{if}\ pc_{t}\neq
ready\texttt{then}\ crashed\ \texttt{else}\ pc_{t}\\\ &vmem:=pmem\oplus log\\\
&log:=\emptyset\\\ &owns:=\bot\end{array}$
Figure 7: Transition relation of internal actions and external actions $run$
and $crashRecovery$ of $CM$

###  4.7 Step 6: Combining Durable Linearizability and Durable Opacity

We now have to combine durable linearizability of the library and durable
opacity of NOrec into a combined result. Since both notions map to IO automata
refinement, the result follows from the general result of nested refinement in
a context.

######  Theorem .

If $CM$ is durably linearizable to $AM$ and $\mathcal{T}[AM]$ can be proved
durably opaque by showing that it is a refinement of dTMS2, then
$\mathcal{T}[CM]$ is durably opaque.

Proof. The proof is by applying Theorem 3.3. Durable linearizability of $CM$
to $AM$ is equivalent to $CM$ being a refinement of the canonical automaton of
$AM$. $\mathcal{T}[CM]$ and $\mathcal{T}[AM]$ can be constructed as the
product automaton of $\mathcal{T}$ and $CM/AM$, since the state of
$\mathcal{T}$ and the state of the library are disjoint. The shared external
actions and steps between both automata are the invokes and responses of
library operations, together with the crash. The theorem implies that
$\mathcal{T}[CM]$ is a refinement of $\mathcal{T}[AM]$. Since
$\mathcal{T}[AM]$ refines dTMS2, and by transitivity of refinement we get that
$\mathcal{T}[CM]$ refines dTMS2, implying durable opacity. $\Box$

Note, that in the implementation $CM$ the $owns$ variable is an auxiliary
variable, that has no effect on computations. Therefore the final program code
equivalent to the automaton $\mathcal{T}[CM]$ can omit the variable together
with the calls to Acquire and Release.

##  5 Related Work

Constructing robust shared objects for NVRAM requires the development of
criteria that provide meaningful guarantees in the presence of crashes.
Linearizability [HW90], is one of the most well-known, broadly used,
correctness condition of concurrent objects. Several correctness conditions
attempt to adapt linearizability to histories that include crash events. As
mentioned before, durable linearizability [IMS16] extends the events that can
appear in an abstract concurrent history with crash events. Crashes are
considered global events. Durable linearizability expects that no thread
survives after a crash, thus a thread can operate only in one crash-free
region. On the contrary, strict linearizability [AF03], consider crashes to be
local to the threads that they occur. Under this condition, operations that
are not subjected to a failure can take effect between their invocation and
response. In the case that a thread crashes while executing an operation, it
requires this operation to take effect between its invocation and the crash,
but not after the crash. Operations that are disrupted from a crash are
behaving as aborted operations – they return the value $\bot$, which indicates
that they might have taken effect or not. In this way, a history that includes
crashes can be replaced with a history where the crashes are considered not
observable events from the system, and the crashed operations are replaced
with aborted operations. A disadvantage of this model is that it is proven to
exclude some wait-free implementations.

Guerraoui and Levy [GL04] have defined two more correctness conditions that
extend linearizability, persistent atomicity, and transient atomicity.
Persistent atomicity implies that, in the event of a crash, every pending
operation on the crashed thread is executed before subsequent to the crash
operations of the same thread are invoked. Transient atomicity relaxed this
condition further, by allowing a not complete operation due to a crash, to
take effect before the subsequent write response of the same thread. In the
context of NVRAM, these correctness criteria are suitable particularly to
wait-free implementations that use helping mechanisms in which invoked
operation by a thread may take effect by the action of another thread after
the first one crashes. Their main disadvantage is that they do not provide
composability. Berryhill et al. [BGT16] have proposed recoverable
linearizability, which requires every pending operation to happen before its
thread invokes anything on the same object post-crash. Although this condition
provides composability, it doesn’t provide consistency around the crash - a
thread can perform an operation on some other object before coming back to the
pending operation.

On the concrete level, several models both hardware and software specific, aim
to define the correctness of the order in which writes are persisted in NVM.
Pelley et al. [PCW14] describe various such low-level models including strict
persistency and relaxed persistency models such as epoch persistency and
strand persistency. Those models, consider hardware to be able to track
persist dependences and perform flushes implicitly. Izraelevitz et al.
[IMS16], give formal semantics to epoch persistency which corresponds to real-
world explicit ISAs, where flushes are issued explicitly with dedicated
instructions by the respective application. Raad et al. [RWV19] develop
declarative semantics that formalize the persistency semantics of ARMv8
architecture. On the language level, Kolli et al. [KGS+17] proposed an acquire
and release persistency model based on the acquire-release consistency of
C++11.

Regarding transactional memory [HLR10], not many correctness conditions have
been adapted to the persistent memory setting. Raad et al [RWV19] base their
framework for formalizing ARMV8 to a persistent variant of serializability
(PSER) under relaxed memory. Even though serializability provides simple
intuitive semantics it does not handle aborted transactions. TimeStone
[KKM+20] and Pisces [GYW+19] are persistent transnational memories that
guarantee Snapshot Isolation [BBG+95].

One concern regarding persistent memory is providing generic methods for
automatically adapting algorithms to the persistent memory setting. One
direction for solving this problem is persistent transactional memory. Even
though many hardware and software persistent TMs have been developed that
guarantee durability semantics, to our knowledge, no mechanisms have been
developed for automatically adapting well-known STMs to the use of persistent
memory.

Apart from PTMs, other frameworks are also trying to tackle this problem.
Indicatively, Naama Ben-David et al. [BDBFW19] developed a system that can
transform programs that consist of read, write and CAS operations in shared
memory, to persistent. The system aims to create concurrent algorithms that
guarantee consistency after a fault. This is done by introducing persist
checkpoints, which record the current state of the execution and from which
the execution can continue after a fault. Two consecutive checkpoints form a
capsule. When a fault occurs inside a capsule the program execution is
continued from the previous capsule boundary. It is ensured that every capsule
is correct (can be repeated safely). The authors assume the Parallel
Persistent Model (PPM) which consists of P processors, each with a local
ephemeral memory of limited and sharing persistent memory. Two persistent
write buffers are kept along with a persistent bit in order to solve crash
write-after-read conflicts. A copy of the ephemeral variables or the valid
write buffer is kept in persistent memory at the end of each capsule. Those
values are restored after a crash. CAS operations are replaced with
recoverable CAS operations [ABBH18] that are wrapped with a mechanism which
guarantees that CAS executions are not repeated after a successful execution.
The modified algorithm has constant computational and recovery delay, both of
which can decrease by applying several optimizations.

Izraelevitz et al. [IKK16] develop and implement a logging mechanism based on
undo and redo log properties named JUSTDO logging and introduce the concept of
FASE (failure-atomic sections). This mechanism aims to reduce the memory size
of log entries while preserving data integrity after crash occurrences. Unlike
optimistic transactions [CBB14], JUSTDO logging resumes the execution of
interrupted FASEs to their last store instruction, and then executes them
until completion. One disadvantage of this strategy is that the FASEs cannot
be rolled back after a system failure. As a consequence, there is no tolerance
of bugs inside the FASEs. In this system, it is assumed that the cache memory
is persistent, and the system also requires that all load/store instructions
access persistent data. A small log is maintained for each thread, that
records its most recent store within a FASE. The small per thread logs
simplify the log management and reduce the memory requirements.

##  6 Conclusion

In this paper, we use durable opacity as a correctness condition for software
transactional memory running on non-volatile hardware architectures. We have
proposed an abstract specification dTMS2 which is durably opaque and have
shown how this can be employed in refinement-based proofs of durable opacity.
We have furthermore developed a modular proof technique for such refinement
proofs, separating out the proof of durability from that of opacity. We have
exemplified this proof technique on the STM NOrec for which we have – to this
end – developed a version adequate for non-volatile memory.

Regarding verification methods for proving correctness, in this work, we
introduce a new proof technique that is inspired by work on the verification
of a Flash file system. Although this work does not target NVM or STMs,
Schellhorn et al. [SBPR20] also use ownership as a method to restrict
concurrency at the interface of a library. The development, which refines an
abstract POSIX-compatible file system specification in several steps to the
Linux interface MTD for flash hardware, also uses intermediate layers (similar
to the library AM used here) to introduce caches for flash pages [PEB+17] and
for file-content [BSR20], though the correctness criteria defined in these
papers are strictly weaker than durable linearizability.

Our new proof technique (outlined in Fig. 3) describes a similar technique in
the setting of STMs. In particular, we provide an abstract library that
operates directly on persistent memory and a concrete implementation that uses
both volatile and persistent memory. The original STM is placed in an
execution context that could have system crashes and uses the abstract and
concrete library to perform memory operations. Given an STM that already
refines TMS2 (and hence is opaque), the bulk of the verification effort using
our method is focused on verifying durable linearizability between the
abstract and concrete libraries.

#### Future work.

We conjecture that the libraries $AM$ and $CM$ that we have defined could be
used to transform other opaque algorithms into durably opaque algorithms when
the STMs use a lazy write-back commit with mutual exclusion between the write-
back operations. Other types of STMs, e.g., TL2 [DSS06] (which uses a per-
location lock to allow concurrent write-backs) and TML [DDS+10] (which uses an
eager write-back mechanism) cannot use the libraries $AM$ and $CM$ that we
have developed directly. Whether the modular library based approach presented
in this paper applies to these other algorithms as well remains a future
research topic.

## References

  * [ABBH18] H. Attiya, O. Ben-Baruch, and D. Hendler.  Nesting-safe recoverable linearizability: Modular constructions for non-volatile memory.  In Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing, pages 7–16, 2018.
  * [AD17] A. Armstrong and B. Dongol.  Modularising opacity verification for hybrid transactional memory.  In A. Bouajjani and A. Silva, editors, FORTE, volume 10321 of LNCS, pages 33–49. Springer, 2017.
  * [ADD17] A. Armstrong, B. Dongol, and S. Doherty.  Proving opacity via linearizability: A sound and complete method.  In A. Bouajjani and A. Silva, editors, FORTE, volume 10321 of LNCS, pages 50–66. Springer, 2017.
  * [AF03] M. K. Aguilera and S. Frølund.  Strict linearizability and the power of aborting.  Technical Report HPL-2003-241, 2003.
  * [BBG+95] H. Berenson, P. Bernstein, J. Gray, J. Melton, E. O’Neil, and P. O’Neil.  A critique of ansi sql isolation levels.  ACM SIGMOD Record, 24(2):1–10, 1995.
  * [BDBFW19] N. Ben-David, G. E Blelloch, M. Friedman, and Y. Wei.  Delay-free concurrency on faulty persistent memory.  In The 31st ACM Symposium on Parallelism in Algorithms and Architectures, pages 253–264, 2019.
  * [BDD+20] E. Bila, S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, and H. Wehrheim.  Defining and verifying durable opacity: Correctness for persistent software transactional memory.  In A. Gotsman and A. Sokolova, editors, FORTE 2020, volume 12136 of Lecture Notes in Computer Science, pages 39–58. Springer, 2020\.
  * [BGT16] R. Berryhill, W. Golab, and M. Tripunitara.  Robust shared objects for non-volatile main memory.  In 19th International Conference on Principles of Distributed Systems (OPODIS 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016\.
  * [BSR20] S. Bodenmüller, G. Schellhorn, and W. Reif.  Modular integration of crashsafe caching into a verified virtual file system switch.  In B. Dongol and E. Troubitsyna, editors, iFM, volume 12546 of Lecture Notes in Computer Science, pages 218–236. Springer, 2020.
  * [CBB14] D. R. Chakrabarti, H.-J. Boehm, and K. Bhandari.  Atlas: Leveraging locks for non-volatile memory consistency.  ACM SIGPLAN Notices, 49(10):433–452, 2014.
  * [DD15] B. Dongol and J. Derrick.  Verifying linearisability: A comparative survey.  ACM Comput. Surv., 48(2):19:1–19:43, 2015.
  * [DDD+16] S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, and H. Wehrheim.  Proving opacity of a pessimistic STM.  In P. Fatourou, E. Jiménez, and F. Pedone, editors, OPODIS, volume 70 of LIPIcs, pages 35:1–35:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
  * [DDD+19] J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, and H. Wehrheim.  Verifying correctness of persistent concurrent data structures.  In FM, volume 11800 of Lecture Notes in Computer Science, pages 179–195. Springer, 2019.
  * [DDS+10] L. Dalessandro, D. Dice, M. L. Scott, N. Shavit, and M. F. Spear.  Transactional mutex locks.  In P. D’Ambra, M. R. Guarracino, and D. Talia, editors, Euro-Par (2), volume 6272 of LNCS, pages 2–13. Springer, 2010.
  * [DDS+15] J. Derrick, B. Dongol, G. Schellhorn, O. Travkin, and H. Wehrheim.  Verifying opacity of a transactional mutex lock.  In FM, volume 9109 of LNCS, pages 161–177. Springer, 2015\.
  * [DGLM13] S. Doherty, L. Groves, V. Luchangco, and M. Moir.  Towards formally specifying and verifying transactional memory.  Formal Asp. Comput., 25(5):769–799, 2013.
  * [dRE98] W. P. de Roever and K. Engelhardt.  Data Refinement: Model-oriented Proof Theories and their Comparison, volume 46 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, 1998.
  * [DSS06] D. Dice, O. Shalev, and N. Shavit.  Transactional locking II.  In S. Dolev, editor, DISC, volume 4167 of LNCS, pages 194–208. Springer, 2006.
  * [DSS10] L. Dalessandro, M. F. Spear, and M. L. Scott.  Norec: streamlining STM by abolishing ownership records.  In R. Govindarajan, D. A. Padua, and M. W. Hall, editors, PPoPP, pages 67–78. ACM, 2010.
  * [EPS+15] G. Ernst, J. Pfähler, G. Schellhorn, D. Haneberg, and W. Reif.  KIV—Overview and VerifyThis competition.  Software Tools for Technology Transfer (STTT), 17(6):677–694, 2015\.
  * [FHMP18] M. Friedman, M. Herlihy, V. J. Marathe, and E. Petrank.  A persistent lock-free queue for non-volatile memory.  In A. Krall and T. R. Gross, editors, ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP, pages 28–40. ACM, 2018.
  * [GK08] R. Guerraoui and M. Kapalka.  On the correctness of transactional memory.  In S. Chatterjee and M. L. Scott, editors, PPOPP, pages 175–184. ACM, 2008.
  * [GK10] R. Guerraoui and M. Kapalka.  Principles of Transactional Memory.  Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2010.
  * [GL04] R. Guerraoui and R. Levy.  Robust emulations of shared memory in a crash-recovery model.  In 24th International Conference on Distributed Computing Systems, 2004. Proceedings., pages 400–407. IEEE, 2004.
  * [GYW+19] J. Gu, Q. Yu, X. Wang, Z. Wang, B. Zang, H. Guan, and H. Chen.  Pisces: a scalable and efficient persistent transactional memory.  In USENIX Annual Technical Conference, pages 913–928, 2019.
  * [HLR10] T. Harris, J. Larus, and R. Rajwar.  Transactional memory.  Synthesis Lectures on Computer Architecture, 5(1):1–263, 2010.
  * [HW90] M. Herlihy and J. M. Wing.  Linearizability: A correctness condition for concurrent objects.  ACM TOPLAS, 12(3):463–492, 1990.
  * [IKK16] Joseph Izraelevitz, Terence Kelly, and Aasheesh Kolli.  Failure-atomic persistent memory updates via justdo logging.  ACM SIGARCH Computer Architecture News, 44(2):427–442, 2016.
  * [IMS16] J. Izraelevitz, H. Mendes, and M. L. Scott.  Linearizability of persistent memory objects under a full-system-crash failure model.  In C. Gavoille and D. Ilcinkas, editors, DISC, volume 9888 of LNCS, pages 313–327. Springer, 2016.
  * [KGS+17] A. Kolli, V. Gogte, A. Saidi, S. Diestelhorst, P. M. Chen, S. Narayanasamy, and T. F. Wenisch.  Language-level persistency.  In 2017 ACM/IEEE 44th Annual International Symposium on Computer Architecture (ISCA), pages 481–493. IEEE, 2017.
  * [KKM+20] M. R. Krishnan, J. Kim, A. Mathew, X. Fu, A. Demeri, C. Min, and S. Kannan.  Durable transactional memory can scale with timestone.  In ASPLOS, pages 335–349, 2020.
  * [LLM12a] M. Lesani, V. Luchangco, and M. Moir.  A framework for formally verifying software transactional memory algorithms.  In M. Koutny and I. Ulidowski, editors, CONCUR 2012, pages 516–530, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.
  * [LLM12b] M. Lesani, V. Luchangco, and M. Moir.  Putting opacity in its place.  In Workshop on the Theory of Transactional Memory, 2012.
  * [LT87] N. A. Lynch and M. R. Tuttle.  Hierarchical correctness proofs for distributed algorithms.  In PODC, pages 137–151, New York, NY, USA, 1987. ACM.
  * [LV95] N. Lynch and F. Vaandrager.  Forward and backward simulations.  Information and Computation, 121(2):214 – 233, 1995.
  * [Lyn96] N. A. Lynch.  Distributed Algorithms.  Morgan Kaufmann, 1996.
  * [Mül98] O. Müller.  I/O Automata and beyond: Temporal logic and abstraction in Isabelle.  In J. Grundy and M. Newey, editors, TPHOLs, pages 331–348, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg.
  * [PCW14] S. Pelley, P. M. Chen, and T. F. Wenisch.  Memory persistency.  In 2014 ACM/IEEE 41st International Symposium on Computer Architecture (ISCA), pages 265–276. IEEE, 2014.
  * [PEB+17] J. Pfähler, G. Ernst, S. Bodenmüller, G. Schellhorn, and W. Reif.  Modular verification of order-preserving write-back caches.  In N. Polikarpova and S. A. Schneider, editors, iFM, volume 10510 of Lecture Notes in Computer Science, pages 375–390. Springer, 2017\.
  * [RWV19] A. Raad, J. Wickerson, and V. Vafeiadis.  Weak persistency semantics from the ground up: Formalising the persistency semantics of armv8 and transactional models.  Proceedings of the ACM on Programming Languages, 3(OOPSLA):1–27, 2019.
  * [SBPR20] G. Schellhorn, S. Bodenmüller, J. Pfähler, and W. Reif.  Adding concurrency to a sequential refinement tower.  In International Conference on Rigorous State-Based Methods, pages 6–23. Springer, 2020.
  * [Sch20] G. Schellhorn.  Verification of Durable Linearizability of a Memory Cache with KIV, 2020\.  URL: http://www.informatik.uni-augsburg.de/swt/projects/AM-CM.html.
  * [ZFS+19] Y. Zuriel, M. Friedman, G. Sheffi, N. Cohen, and E. Petrank.  Efficient lock-free durable sets.  PACMPL, 3(OOPSLA):128:1–128:26, 2019.