1

# Implementing and Verifying Release-Acquire Transactional Memory (Extended
Version)

Sadegh Dalvandi<EMAIL_ADDRESS>0000-0001-8813-780X University of
SurreyGuildfordUK and  Brijesh Dongol<EMAIL_ADDRESS>0000-0003-0446-3507 University of SurreyGuildfordUK

###### Abstract.

Transactional memory (TM) is an intensively studied synchronisation paradigm
with many proposed implementations in software and hardware, and combinations
thereof. However, TM under relaxed memory, e.g., C11 (the 2011 C/C++ standard)
is still poorly understood, lacking rigorous foundations that support
verifiable implementations. This paper addresses this gap by developing
TMS2-ra, a relaxed operational TM specification. We integrate TMS2-ra with
RC11 (the repaired C11 memory model that disallows load-buffering) to provide
a formal semantics for TM libraries and their clients. We develop a logic,
TARO, for verifying client programs that use TMS2-ra for synchronisation. We
also show how TMS2-ra can be implemented by a C11 library, TML-ra, that uses
relaxed and release-acquire atomics, yet guarantees the synchronisation
properties required by TMS2-ra. We benchmark TML-ra and show that it
outperforms its sequentially consistent counterpart in the STAMP benchmarks.
Finally, we use a simulation-based verification technique to prove correctness
of TML-ra. Our entire development is supported by the Isabelle/HOL proof
assistant.

Weak Memory, Transactional Memory, C11, Verification, Refinement

††journal: PACMPL††journalvolume: 1††journalnumber: OOPSLA††article:
1††journalyear: 2022††publicationmonth: 12††copyright: none††ccs: Software and
its engineering General programming languages††ccs: Social and professional
topics History of programming languages

##  1\. Introduction

The advent and proliferation of architectures implementing relaxed memory
models has resulted in many new challenges in the development of concurrent
programs. In the context of the C/C++ relaxed memory model defined by
C11111C11 refers to the 2011 ISO specification of C/C++. , over a decade’s
worth of research has resulted in rigorous semantic foundations (Batty et al.,
2016, 2011; Lee et al., 2020; Kang et al., 2017; Lahav et al., 2017; Paviotti
et al., 2020), and more recently, logics for reasoning about the correctness
of concurrent programs (Wright et al., 2021; Dalvandi et al., 2022; Doherty et
al., 2019; Dalvandi et al., 2020a; Kaiser et al., 2017; Kang et al., 2017;
Doko and Vafeiadis, 2017; He et al., 2016; Lahav and Vafeiadis, 2015;
Vafeiadis and Narayan, 2013). These works have provided the background
necessary to develop high-level abstractions and concurrency libraries over
relaxed-memory architectures. Recent works have included reimplementations of
concurrent data structures (Dalvandi and Dongol, 2021; Raad et al., 2019a;
Krishna et al., 2020; Emmi and Enea, 2019; Dongol et al., 2018b), including
those with relaxed specifications that aim to exploit the additional
behaviours allowed by relaxed memory.

Our aim for this paper is to implement and verify synchronisation
abstractions, fine-tuned for C11, in the form of transactional memory (TM)
libraries, which provide reusable foundations for high-performance, yet easy
to manage concurrency control (Herlihy and Moss, 1993; Shavit and Touitou,
1997; Guerraoui and Kapalka, 2010). Implementations include those in software
(as STM libraries) and hardware (Intel-RTM and Armv9). Other variations
include hybrid TM that combine software and hardware TMs and implementations
that are natively supported by the compiler (e.g., the continued C++ TM Lite
development). In addition to supporting general-purpose concurrency, TM has
also been used to develop transactional concurrent objects and data structures
(Assa et al., 2021, 2020; Bronson et al., 2010; Lesani et al., 2022). Intel’s
persistent memory development kit (PMDK) (Scargall, 2020) extensively promotes
the transactional paradigm (though multi-threaded transactions are not
directly supported by PMDK’s transactions). These prior works have assumed SC
transactions, i.e., that transactional access provide the same guarantees as
sequentially consistent memory. Our focus is the verification of STMs
implemented as a programming language library with _relaxed_ , _release_ ,
_acquire_ and _release-acquire_ accesses providing a pathway towards
simplified development of transactional objects (including concurrent data
structures) for relaxed memory.

TM implementations provide fine-grained interleaving (for efficiency) that
execute with an illusion of atomicity (for correctness). A completed
transaction may be committed or aborted so that all or none of its effects are
externally visible. TM implementations are designed to satisfy a variety of
correctness conditions such as (strict) serialisability, opacity, and snapshot
isolation, which restrict ordering possibilities of completed transactions. TM
has been extensively studied for sequentially consistent (SC) architectures
(Lamport, 1979), but implementations over relaxed memory are limited.

Prior works on relaxed memory transactions (e.g., (Chong et al., 2018; Dongol
et al., 2018a)) have focussed on foundations of hardware transactions and
their interaction with relaxed memory models, e.g., the expected isolation
guarantees, reordering possibilities etc. The work of Chong et al (Chong et
al., 2018) also provides for semantics of native C++ transactions. However,
native TM support in C++ is still in a state of flux (Zardoshti et al., 2019;
Spear et al., 2020) and the underlying designs have changed since the original
works by Chong et al (Chong et al., 2018). Moreover, these semantics are
presented in an axiomatic (aka declarative) style, which cannot be used to
verify TM implementations, where we require operational descriptions of
correctness. Therefore, our point of departure is a separate set of works on
TM specifications, in particular the TMS2 specification (Doherty et al.,
2013), which has been used extensively as a TM specification for standard
(i.e., SC) architectures.

More recent works have taken steps towards C++ implementations, including
native support of TM within C++ (Zardoshti et al., 2019) and STMs implemented
using C++ relaxed memory (Rodriguez and Spear, 2020). However, Zardoshti et
al. (2019) do not describe interactions with the C11 relaxed memory model,
while Rodriguez and Spear (Rodriguez and Spear, 2020) focus on data race
freedom and privatisation guarantees. Neither of these works have a formal
semantics, nor are they supported by a verification methodology. (See §7 for a
more comprehensive survey of related works.)

Our work addresses several gaps in the current state-of-the-art of
transactions for C/C++. We work with RC11, i.e., the repaired C11 memory model
(Lahav et al., 2017). The RC11 memory model disallows program-order and reads-
from cycles, and hence disallows load-buffering behaviour. This restriction
greatly simplifies reasoning and variants of RC11 are supported by a number of
different logics (Lahav and Vafeiadis, 2015; Dalvandi et al., 2022; Dalvandi
and Dongol, 2021; Dalvandi et al., 2020a; Kaiser et al., 2017; Dang et al.,
2022). Logics that address the full C11 memory model (allowing load buffering)
have also been developed, but proofs in these logics are limited to small
litmus tests (Wright et al., 2021; Svendsen et al., 2018).

We develop:  (i) a reusable specification of TM that provides well-defined
guarantees to those developing client programs;  (ii) techniques for verifying
client programs in C11 that use such TM abstractions;  (iii) implementationsof
TM in C11, including their rigorous verification; and  (iv) mechanisationof
the verification described above in the theorem prover Isabelle/HOL.  We
discuss these contributions in more detail below.

##### Correctness specifications.

To enable verification, we start with the _TMS2_ specification (Doherty et
al., 2013). TMS2 implies the TMS1 specification, which is known to be both
necessary and sufficient for observational refinement (of client programs)
(Attiya et al., 2018). The main difference between TMS1 and TMS2 is that TMS1
allows aborted transactions to observe different serialization orders (Lesani
et al., 2012). In contrast, TMS2, like _opacity_ (Guerraoui and Kapalka,
2010), ensures strict serializability of the committed transactions and
furthermore that aborted transactions are consistent with the serialisation
order. Although more restrictive than TMS1, TMS2 has been shown to be a robust
correctness condition that is useful in practice, providing a specification
for a number of TM implementations under SC (Derrick et al., 2018; Doherty et
al., 2016; Armstrong et al., 2017; Armstrong and Dongol, 2017).

Under relaxed memory, the TMS2 specification is inadequate since it does not
provide any of the client-side guarantees required by relaxed memory libraries
(Raad et al., 2018, 2019a; Dalvandi and Dongol, 2021; Dongol et al., 2018b).
Such client-side guarantees are required under relaxed memory since writes in
one thread are not guaranteed to be propagated to other threads unless the
library is properly synchronised (cf. the message passing litmus tests
(Alglave et al., 2014)).

Our first contribution is the adaptation of TMS2 to address this issue. In
particular, our specification, TMS2-ra, provides a flexible meaning of
correctness, allowing a client to specify relaxed, releasing, acquiring and
release-acquiring transactions (see §3), mimicking the memory annotations of
C11 atomics (Batty et al., 2011). This provides greater flexibility in TM
design; we develop a model in which these different types of transactions co-
exist within the same TM system.

##### Client verification.

Our second contribution (see §5) is a verification technique for relaxed-
memory client programs that use TMS2-ra. In particular, we prove correctness
of several variations of the message passing litmus test, synchronised through
TMS2-ra transactions, to show that TMS2-ra behaves as expected. In particular,
we show how different client-side guarantees are achieved depending on the
type of synchronisation guarantee (relaxed, releasing or acquiring) guaranteed
by the transaction in question.

Our verification framework includes a new logic, TARO, capable of efficiently
reasoning about the views of a client programs (Dalvandi et al., 2022; Kaiser
et al., 2017). This means that the correctness of programs can be established
using a standard Owicki-Gries reasoning framework (Dalvandi et al., 2020a;
Owicki and Gries, 1976; Dalvandi and Dongol, 2021).

##### Implementation, benchmarking and verification.

Our third contribution is the implementation and full verification of an STM
algorithm that uses C11 relaxed/release-acquire atomics and implements
TMS2-ra. Our implementation is an adaptation of Dalessandro et al’s
Transactional Mutex Lock (TML) (Dalessandro et al., 2010), which presents a
simple mechanism for synchronising transactions optimised for read-heavy
workloads. TML is synchronised using a single global lock, and allows multiple
concurrent read-only transactions, but at most one writing transaction, i.e.,
a writing transaction causes all other concurrent transactions to abort.

Interestingly, our adapted algorithm, which we call TML-ra, allows more
concurrency than TML by exploiting the parallelism afforded by relaxed and
release-acquire C11 atomics. Moreover, a writing transaction does not force
other read-only transactions to abort, allowing greater read/write parallelism
(see §4). We show that this theoretical speedup manifests in real
implementations and TML-ra outperforms its SC counterpart in all STAMP
benchmarks (see §4.3).

We use a simulation-based verification method for the C11 memory model
(Dalvandi and Dongol, 2021) to prove correctness of TML-ra. This proof
establishes a refinement between TML-ra and TMS2-ra, which ensures that all
observable behaviours of TML-ra are observable behaviours of TMS2-ra. Thus, if
a client program $C$ is proved correct when it uses TMS2-ra, then $C$ will
also be correct if we replace calls to TMS2-ra in $C$ by calls to TML-ra.

##### Mechanisation.

Our fourth contribution is the mechanisation of all proofs presented in the
paper in the Isabelle/HOL proof assistant (available as supplementary
material). This includes the operational semantics of C11 integrated with
TMS2-ra, soundness of all TARO rules, the use of TARO to prove several client
programs that use TMS2-ra, and finally the proof of simulation between TMS2-ra
and TML-ra.222Our development may be found in (Dalvandi and Dongol, 2022).

##### Overview.

This paper is structured as follows. We describe our requirements for relaxed
and release-acquire transactions in §2. We formalise this semantics in §3 via
the TMS2-ra specification, and describe its integration with a view-based
semantics for RC11 with release-acquire atomics (Dalvandi et al., 2020a). In
§4, we provide an examplar implementation and benchmarking results for TML-ra.
In §5, we present our logic for reasoning about release-acquire transactional
memory, which provides a method of reasoning about client programs that use
the TMS2-ra specification. Finally, in §6, we present a proof of correctness
of TML-ra via refinement w.r.t. TMS2-ra.

##  2\. Transactional guarantees in C11

A TM specification in a relaxed memory setting has two distinct sets of goals.
The first set must guarantee the expected behaviours of transactions, e.g.,
serializability, opacity etc. The second must provide client-side guarantees,
e.g., release-acquire synchronisation, observational refinement etc. We
consider both in our TMS2-ra specification (see Fig. 4).

###  2.1. Release-acquire synchronisation

$\begin{array}[]{@{}l@{~}||@{~}l}{\bf Thread}\
\tau{1}\hfil~{}\vrule\vrule~{}&{\bf Thread}\ \tau{2}\\\
1\\!:d:=5;\hfil~{}\vrule\vrule~{}&3\\!:\textsf{{do}}\ r_{1}\leftarrow f\\\
2\\!:f:=1;\hfil~{}\vrule\vrule~{}&\ \ \ \ \textsf{{until}}\ r_{1}=1;\\\
\hfil~{}\vrule\vrule~{}&4\\!:r_{2}\leftarrow d;\\\ \end{array}$

$\\{r_{2}=0\lor r_{2}=5\\}$

(a) Unsynchronised MP

$\begin{array}[]{l@{~}||@{~}l}\begin{array}[t]{@{}l@{}}{\bf Thread}\
\tau{1}\\\ 1\\!:d:=5;\\\ 2\\!:\hbox{\pagecolor{blue!15}$f:=^{\sf R}1$};\\\
\end{array}\hfil~{}\vrule\vrule~{}&\begin{array}[t]{@{}l@{}}{\bf Thread}\
\tau{2}\\\ 3\\!:\textsf{{do}}\ \hbox{\pagecolor{blue!15}$r_{1}\leftarrow^{\sf
A}f$}\\\ \ \ \ \ \textsf{{until}}\ r_{1}=1;\\\ 4\\!:r_{2}\leftarrow d;\\\
\end{array}\end{array}$

$\\{r_{2}=5\\}$

(b) Synchronised MP

Figure 1. Message passing (MP) in C11

Message passing (MP) in C11

Prior to detailing the design choices of TMS2-ra, we recap the basics of
release-acquire synchronisation in C11, including a recently developed
timestamp-based operational semantics, which is the semantics assumed by
TMS2-ra.

The fragment of C11 we focus on is the RC11-RAR fragment. The first “R”
denotes the _repairing model_ (Lahav et al., 2017), which precludes ‘thin-air’
behaviour by disallowing memory operations within a thread to be reordered.
The “RAR” refers to the fact that the model includes _release-acquire_ as well
as _relaxed_ atomics (Dalvandi et al., 2020b; Doherty et al., 2019). 333Note
that extending this model to include other types of C11 synchronisation (e.g.,
SC fences) and relaxations that allow intra-thread ordering is possible
(Wright et al., 2021), but these extended models are not so interesting for
the purposes of this paper, and the additional complexity that they induce
detracts from our main contributions.  For the remainder of this paper, we
simply write C11 to refer to RC11-RAR.

We explain the main ideas behind release-acquire synchronisation using the
message passing (MP) litmus test in Figs. 1 and 1. It comprises two shared
variables: $d$ (for data) and $f$ (for a flag), both of which are initially
$0$. Under SC, the postcondition of the program is $r_{2}=5$ because the loop
in thread $\tau{2}$ only terminates after $f$ has been updated to $1$ in
thread $\tau{1}$, which in turn happens after $d$ is set to $5$. Therefore,
the only possible value of $d$ that thread $\tau{2}$ can read is $5$.

However, in Fig. 1, all read/write accesses of $d$ and $f$ are relaxed, and
hence the program can only establish the weaker postcondition $r_{2}=0\lor
r_{2}=5$ since it is possible for thread $\tau{2}$ to read $0$ for d at line
4. In particular, reading $1$ for $f$ does not guarantee that thread $\tau{2}$
will read $5$ for $d$.

This anomaly is corrected in Fig. 1 where the highlighted code depicts the
necessary changes. In particular, we introduce a release annotation (line 2)
as well as an acquire annotation (line 3), which together induces a _happens-
before_ relation if the read of $f$ at line 3 reads from the write at line 2
(see (Batty et al., 2011)). This in turn ensures that thread $\tau{2}$ sees
the most recent write to $d$ at line 1. We explain how relaxed accesses and
release-acquire synchronisation is formalised by the operational semantics in
§3.1.

###  2.2. Transactional message passing

$\begin{array}[]{l@{\quad}||@{\quad}l}\begin{array}[t]{@{}l@{}}{\bf Thread}\
\tau{1}\\\ 1\\!:d:=5;\\\ 2\\!:\hbox{\pagecolor{black!8}${\tt TxBegin}(\sf
R)$}\\\ 3\\!:\hbox{\pagecolor{black!8}${\tt TxWrite}(f,1)$};\\\
4\\!:\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
\end{array}&\begin{array}[t]{@{}r@{~}l@{}}\lx@intercol{\bf Thread}\
\tau{2}\hfil\lx@intercol\\\ 5\\!:~{}&\textsf{{do}}\\\
6\\!:~{}&\quad\hbox{\pagecolor{black!8}${\tt TxBegin}(\sf A,\\{r_{1}\\})$}\\\
7\\!:~{}&\quad\hbox{\pagecolor{black!8}${\tt TxRead}(f,r_{1})$};\\\
8\\!:~{}&\quad\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
9\\!:~{}&\textsf{{until}}\ r_{1}=1\\\ 10\\!:~{}&r_{2}\leftarrow d\\\
\end{array}\end{array}$

$\\{r_{2}=5\\}$

(a) Transactional MP

$\begin{array}[]{@{}l@{~~~~}||@{~~~~}l@{}}\begin{array}[t]{@{}l@{}}{\bf
Thread}\ \tau{1}\\\ 1\\!:d_{1}:=5;\\\ 2\\!:\hbox{\pagecolor{black!8}${\tt
TxBegin}(\sf RX,\emptyset)$};\\\ 3\\!:\hbox{\pagecolor{black!8}${\tt
TxWrite}(d_{2},10)$};\\\ 4\\!:\hbox{\pagecolor{black!8}${\tt
TxWrite}(f,1)$};\\\ 5\\!:\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
\end{array}\hfil~{}~{}~{}~{}\vrule\vrule~{}~{}~{}~{}&\begin{array}[t]{@{}r@{~}l@{}}\lx@intercol{\bf
Thread}\ \tau{2}\hfil\lx@intercol\\\ 6\\!:~{}&\hbox{\pagecolor{black!8}${\tt
TxBegin}(\sf RX,\\{r_{1},r_{2}\\})$}\\\
7\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxRead}(f,r_{1})$};\\\
8\\!:~{}&\hbox{\pagecolor{black!8}{{if}}\ $r_{1}=1$\ {{then}}\ }\\\
9\\!:~{}&\hbox{\pagecolor{black!8}\quad${\tt TxRead}(d_{2},r_{2})$};\\\
10\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
11\\!:~{}&r_{3}\leftarrow d_{1};\end{array}\end{array}$

$\\{r_{1}=1\Rightarrow r_{2}=10\wedge r_{3}\in\\{0,5\\}\\}$

(b) Relaxed transactions

$\begin{array}[]{@{}l@{~~~~}||@{~~~~}l@{~~~~}||@{~~~~}l}\begin{array}[t]{@{}l@{}}{\bf
Thread}\ \tau{1}\\\ 1\\!:d_{1}:=5;\\\ 2\\!:\hbox{\pagecolor{black!8}${\tt
TxBegin}(\sf R,\emptyset)$}\\\ 3\\!:\hbox{\pagecolor{black!8}${\tt
TxWrite}(f,1)$};\\\ 4\\!:\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
\end{array}\hfil~{}~{}~{}~{}\vrule\vrule~{}~{}~{}~{}&\begin{array}[t]{@{}r@{~}l@{}}\lx@intercol{\bf
Thread}\ \tau{2}\hfil\lx@intercol\\\ 5\\!:~{}&d_{2}:=10;\\\
6\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxBegin}(\sf RA,\\{r_{2}\\})$}\\\
7\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxRead}(f,r_{2})$};\\\
8\\!:~{}&\hbox{\pagecolor{black!8}$\textsf{{if}}\ r_{2}=1\
\textsf{{then}}$}\\\ 9\\!:~{}&\hbox{\pagecolor{black!8}$\quad{\tt
TxWrite}(f,2)$}\\\ 10\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
\end{array}\hfil~{}~{}~{}~{}\vrule\vrule~{}~{}~{}~{}&\begin{array}[t]{@{}r@{~}l@{}}\lx@intercol{\bf
Thread}\ \tau{3}\hfil\lx@intercol\\\ 11\\!:~{}&\hbox{\pagecolor{black!8}${\tt
TxBegin}(\sf A,\\{r_{3}\\})$}\\\ 12\\!:~{}&\hbox{\pagecolor{black!8}${\tt
TxRead}(f,r_{3})$};\\\ 13\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
14\\!:~{}&\textsf{{if}}\ r_{3}=2\ \textsf{{then}}\\\ 15\\!:~{}&\ \ \ \
s_{1}\leftarrow d_{1}\\\ 16\\!:~{}&\ \ \ \ s_{2}\leftarrow d_{2}\\\
\end{array}\end{array}$

$\\{r_{3}=2\Rightarrow s_{1}=5\wedge s_{2}=10\\}$

(c) Extended transactional MP

Figure 2. Transactional memory client interactions

Transactional memory client interactions

We now describe the guarantees provided by our transactional model in the
context of a client program. Like standard reads and writes in C11, we allow
transactions to be combined with a synchronising annotation, which may be one
of relaxed (RX), releasing (R), acquiring (A), or release-acquiring (RA).
These annotations dictate whether or not transaction induces a client-side
happens before. In particular, client-side happens-before is induced from
thread $\tau{1}$ to thread $\tau{2}$ if  (i) a read in transaction $t_{2}$
executed by $\tau{2}$ reads-from a write in transaction $t_{1}$ executed by
$\tau{1}$,  (ii) $t_{1}$contains a release annotation (either R or RA), and
(iii) $t_{2}$contains an acquire annotation (either A or RA).  We illustrate
the implications of these annotations via the examples in Fig. 2, where the
highlights are used to identify the transactions. We assume that a client
provides a transaction with a set of registers that it may use when the
transaction begins (see §3).

Fig. 2 describes a transactional variation of MP. Thread $\tau{1}$ comprises a
(non-transactional) relaxed write on $d$ followed by a transactional write of
the flag, $f$. Thread $\tau{2}$ contains a transactional read of $f$ within a
loop that terminates if $\tau{2}$ reads $1$ for $f$. After the loop
terminates, $\tau{2}$ performs a (non-transactional) relaxed read of $d$. In
this example, like Fig. 1, the release and acquire annotations induce a
happens-before relation from $\tau{1}$ to $\tau{2}$ and hence ensure that the
read of $d$ in $\tau{2}$ does not return the stale value, $0$.

Fig. 2 describes a program that uses a relaxed transaction. The postcondition
of the program considers the case where the transaction in $\tau{1}$ occurs
before the transaction in $\tau{2}$ since the antecedent assumes that
$r_{1}=1$, i.e., the read of $f$ at line 7 reads the write of $f$ at line 4.
In this example, both transactions are relaxed, and hence, the ordering of
transactions above does not induce a happens before from $\tau{1}$ to
$\tau{2}$. Thus, the read of $d_{1}$ at line 11 is not guaranteed to see the
write of $d_{1}$ at line 1, i.e., the final value of $r_{3}$ is either $0$ or
$5$. However, since the write and read of $d_{2}$ occurs within the
transactions of $\tau{1}$ and $\tau{2}$, respectively, if $r_{1}=1$, then
$\tau{2}$ is guaranteed to read $10$ for $d_{2}$.

Finally, Fig. 2 demonstrates a program with an RA transaction. The antecedent
of the program’s postcondition implies that the transaction in $\tau{3}$
occurs after the transaction in $\tau{2}$, which in turn occurs after the
transaction in $\tau{1}$. Here, the transaction annotations ensure that the
writes to $d_{1}$ and $d_{2}$ (at lines 1 and 5) performed by the client are
seen by the client reads at lines 15 and 16. This is because the transaction
in $\tau{2}$ (annotated by RA) is guaranteed to synchronise with the
transaction in $\tau{1}$ (annotated by R), and similarly, the transaction in
$\tau{2}$ (annotated by A) is guaranteed to synchronise with the transaction
in $\tau{2}$ (annotated by RA). Note that if the transaction in $\tau{2}$ was
only releasing, then $\tau{1}$ and $\tau{2}$ would not synchronise, and the
read at line 15 may return either $0$ or $5$. Yet, the read at line 16 would
still be guaranteed to return $10$ for $d_{2}$ since $\tau{2}$ and $\tau{3}$
synchronise. If the transaction in $\tau{2}$ was only acquiring, then
$\tau{2}$ and $\tau{3}$ would not synchronise. In this case, although
$\tau{1}$ and $\tau{2}$ have synchronised, neither of the reads at lines 15
and 16 are guaranteed to return the new writes at lines 1 and 5.

Deciding a transaction’s synchronisation flag ultimately comes down to the
needs of a client program, much like memory_order parameters on
atomic_compare_exchange instructions in C11 (cppreference.com, 2022). Client
programs that require message passing through transactions would use release-
acquire, while others may only require relaxed annotations.

##  3\. Release-acquire TM specification

With the basic requirements for release-acquire and transactional
synchronisation in place, we work towards a formal TM specification. Our
specification will be closely tied to an operational semantics for C11 with
timestamped writes and per-thread views (Podkopaev et al., 2016; Dolan et al.,
2018; Kaiser et al., 2017; Kang et al., 2017; Dalvandi et al., 2020a) (see
§3.1). We integrate this model with a TM specification in §3.3.

###  3.1. View-based operational semantics

As discussed above, in our model, the C11 relaxed memory state is formalised
by _timestamped writes_. Instead of mapping each location to a value, the
state contains a set of writes $\mathtt{writes}\subseteq{\it Write}$, where
${\it Write}={\it Loc}\times\mathit{Val}\times{\it TS}$ represents a write to
a location ${\it Loc}$ with value $\mathit{Val}$ and
$TS\mathrel{\hat{=}}\mathbb{Q}$ is the set of possible timestamps. If
$w\in{\it Write}$ and $w=(x,v,{\it q})$, then we let ${\sf
loc}(w)\mathrel{\hat{=}}x$, ${\sf val}(w)\mathrel{\hat{=}}v$, ${\sf
tst}(w)\mathrel{\hat{=}}{\it q}$, be the functions that extract the location,
value and timestamp of $w$, respectively.

A view is a mapping from a location to a write of that location, i.e., ${\it
View}\mathrel{\hat{=}}{\it Loc}\to{\it Write}$. To define the allowable reads
by each thread to each location, the state also records a thread view for each
thread define by a function

${\tt tview}:{\it TId}\to{\it View}$

where ${\it TId}\mathrel{\hat{=}}\mathbb{N}$ is the set of thread identifiers.
A thread may read from _any_ write whose timestamp is no smaller than the
thread’s current view. Thus, the observable values (${\it OV}$), i.e., the set
of values that thread $\tau$ can read for location $x$ is

$\displaystyle{\it OW}_{\tau}(x)$ $\displaystyle\mathrel{\hat{=}}\left\\{{\it
w}\in\mathtt{writes}\begin{array}[]{@{~}|l@{}}{}\vrule\lx@intercol{\sf
loc}({\it w})=x\wedge{}{\sf tst}({\it w})\geq{\sf tst}({\tt
tview}_{\tau}(x))\end{array}\right\\}$ $\displaystyle{\it OV}_{\tau}(x)$
$\displaystyle\mathrel{\hat{=}}\\{{\sf val}({\it w})\mid{\it w}\in{\it
OW}_{\tau}(x)\\}$

A write may be introduced at any timestamp greater than the thread’s current
view (with a caveat that ensures atomicity of read-modify-writes, see (Doherty
et al., 2019; Dalvandi et al., 2020a) for details).

Finally, to formalise release-acquire synchronisation, a state in the
timestamp model also includes a notion of a modification view,

${\tt mview}:{\it Write}\to{\it View}$

which is a function that records the thread view of the executing thread when
a new write is introduced to $\mathtt{writes}$. In particular, if thread
$\tau$ introduces a new write ${\it w}$ to $\mathtt{writes}$ and ${\tt
tview}_{\tau}$ is updated to $view$ in this new state, then ${\tt mview}$ is
also updated so that ${\tt mview}_{\it w}=view$ in the new state. This
information is used to update thread views in case release-acquire
synchronisation occurs.

Formally, when threads synchronise, a new view is calculated using $\otimes$,
which is defined as follows. Given $V_{1},V_{2}\in{\it View}$, we have

$V_{1}\otimes V_{2}\mathrel{\hat{=}}\lambda x.\
\begin{array}[t]{@{}l@{}}\textbf{if}~{}{\sf tst}(V_{2}(x))\leq{\sf
tst}(V_{1}(x))\ \textbf{then}\ V_{1}(x)\ \textbf{else}\ V_{2}(x)\end{array}$

which constructs a new view by taking the write with the larger timestamp for
each location $x$.

$\sigma_{0}$$d$$f$$\tau{2}$$\tau{1}$$0,0$$0,0$

$\sigma_{1}$$d$$f$$\tau{2}$$\tau{1}$$0,0$$0,0$$5,1$

$\sigma_{2}$$d$$f$$\tau{2}$$\tau{1}$$0,0$$0,0$$5,1$$1^{\sf R}$,1

$\sigma_{3}$$d$$f$$\tau{2}$$\tau{1}$$0,0$$0,0$$5,1$$1^{\sf R}$,1

Figure 3. Synchronised message passing views

Synchronised message passing views

###### Example 0 (Synchronised MP).

Consider Fig. 3, which depicts a possible execution of the program in Fig. 1.
Each “$v,i$” represents a “value, timestamp” pair for the location in
question. The initial state is $\sigma_{0}$, where the views of threads
$\tau{1}$ and $\tau{2}$ are both the initial writes. State $\sigma_{1}$ occurs
after executing line 1, where the view of $\tau{1}$ is updated to the new
write on $d$. Similarly, $\sigma_{2}$ occurs after executing line 2. Note that
the new write is tagged with a release annotation. Moreover, the operational
semantics guarantees that in $\sigma_{2}$, we have $\sigma_{2}.{\tt
mview}_{(f,1,1)}(d)=(d,5,1)$, i.e., the modification view of the write
$(f,1,1)$ returns $(d,5,1)$ for $d$ (since this was the thread view of
$\tau{1}$ for $d$ when the write at line 2 occurred).

Finally, $\sigma_{3}$ depicts the state after execution of line $3$, where the
read returns the value $1$ for $f$. In this case, the thread view of $\tau{2}$
for $f$ is updated to the new read. More importantly, due to release-acquire
annotations the semantics enforces that the thread view of $\tau{2}$ for $d$
in $\sigma_{3}$ is also updated to the new modification view, i.e.,
$\sigma_{2}.{\tt mview}_{(f,1,1)}(d)$. Thus, after state $\sigma_{3}$,
$\tau{2}$ will no longer be able to return the stale value $0$ for $d$.

The key difference in execution of the unsynchronised example (Fig. 1) is that
the read at line 3 does not update ${\tt tview}_{\tau{2}}(d)$. Hence, for the
state of Fig. 1 analogous to $\sigma_{3}$, the view of $\tau{2}$ for $d$ will
remain at the initial write, allowing it to return a stale value.

###  3.2. TMS2

First, we consider the TMS2 specification, which is our TMS2-ra specification
without any client-side release-acquire guarantees. This is given by the
unhighlighted components of Fig. 4, which correspond precisely to the internal
actions of TMS2 (Doherty et al., 2013).444TMS2-ra, like TMS2 is presented as
an I/O automaton (Lynch, 1996). For simplicity, we eschew the external
actions, but they can easily be included to formalise the TM interface.  Note
that each action of Fig. 4 is atomic and guarded by the conditions defined in
pre. If all the conditions in pre hold the transition is enabled, and the
corresponding action atomically updates the state according to the assignments
and functions in eff. If some condition in pre does not hold then the
transition is blocked. We use $\sqcap$ to denote a non-deterministic choice
(see (Lynch, 1996) for details).

TMS2 is a close operational approximation of opacity (Guerraoui and Kapalka,
2010). The differences between TMS2 and opacity are minor (Lesani et al.,
2012), and much of the discussion below applies equally to opacity. TMS2 (and
opacity) distinguishes between completed and live transactions, where
completed transaction may either be committed or aborted. TMS2 guarantees the
existence of a total order $\prec$ over all transactions such that:

  1. (1)

if transaction $t_{1}$ executes TxEnd before $t_{2}$ executes TxBegin, then
$t_{1}\prec t_{2}$;

  2. (2)

for any transaction $t$, if $\prec_{\downarrow t}$ is the strict downclosure
of $t$ w.r.t. $\prec$ and $m$ is the memory obtained by applying the committed
transactions in $\prec_{\downarrow t}$ in order, then

     * •

all internal reads in $t$ for a variable $x$ are consistent with the last
write to $x$ in $t$, and

     * •

all external reads of $t$ are consistent with $m$.

Note that conditions (1) and (2) together imply strict serialisability of the
transactions. Condition (2) additionally ensures that no transaction reads
from an aborted or live transaction since all external writes can be explained
by the prior writes of committed transactions only. Moreover, reads of all
transactions (including aborted and live transactions) never return a spurious
value, i.e., each non-aborting read can be explained by prior committed
transactions.

The existence of the total order mentioned above is guaranteed by the TMS2
specification as follows. Each transaction $t$ comprises a local read set,
rdSett, local write set, wrSett, and variable, statust that is used to model
control flow within a transaction. If the status of $t$ is NOTSTARTED, $t$ may
transition to status READY if a thread $\tau$ executes TxBeginτ. Once ready,
$\tau$ may execute some number of TxRead and TxWrite operations, or TxEnd,
which sets the status of $t$ (the transaction that $\tau$ is executing) to
COMMITTED. Note that if transaction $t$ is READY, it may transition to status
ABORT at any time. Moreover, in some circumstances, $t$ may be forced to abort
because all other transitions of $t$ are blocked. For example, if $t$ is a
writing transaction and $t$’s read set is not a subset of $\mathit{last}(M)$,
then $t$ must abort.

To ensure read/write consistency, TMS2 uses a sequence of memories $M$, where
a memory is a mapping from locations to values. A transaction $t$ records the
earliest memory it can read from by setting beginIdxt to the last index of $M$
when $t$ executed TxBeginτ. Moreover, each committing writing transaction $t$
constructs a new memory $N=\mathit{last}(M)\oplus{}$wrSett which is the memory
$\mathit{last}(M)$ overwritten with the write set of $t$. It then appends $N$
to the end of $M$ (see TxEndWR).

We differentiate between internal reads TxReadInt and external reads
TxReadExt, by whether the read location $x$ is in the write set of the
executing transaction, $t$. An internal read of $x$ simply returns the value
of $x$ in the write set of $t$. An external read of $x$ non-deterministically
picks a memory index $i$. This read is enabled iff $i$ is a valid index (i.e.,
is between beginIdxt and the last memory index, $|M|-1$) and the read set of
$t$ is consistent with $M_{i}$ (i.e., the memory at index $i$). In case an
external read occurs, the read set is updated and the value read is returned.
This means that all external reads in $t$ are validated with respect to some
memory snapshot between beginIdxt and the maximum memory index. Note that it
is possible for two different reads to validate w.r.t. different memory
snapshots.

TMS2 prescribes a lazy write-back strategy via TxWrite, where writes are
cached in a local write set until the commit occurs (as described above).
However, as we shall see, this does not preclude implementations that use
eager write-backs, where writes occur in memory at the time of writing (see
(Derrick et al., 2018)). In fact, the TML-ra algorithm, our main case study in
this paper, is such an eager algorithm (see §4).

We split the commit phase into two cases: read-only (modelled by TxEndRO) and
writing (modelled by TxEndWR). Since all reads are validated at the time of
reading, a read-only transaction can simply commit the transaction. On the
other hand, the writing transaction must ensure its reads are valid w.r.t. the
last memory snapshot. The effect of this transition is to install a new memory
snapshot as described above.

The final component of $t$ is a local set regst that is used to keep track of
the set of registers that the transaction has written to. A client provides
the set of registers to be used by each transaction when the transaction
begins. These registers are set to a special value $\bot$ when a transaction
aborts to ensure that no value read by $t$ is seen outside $t$.

|  TxBeginV${}_{\tau}(\hbox{\pagecolor{black!8}${\it
sflag}$},\hbox{\pagecolor{black!8}$m$},$regSet$)$
---
| pre |  statust = NOTSTARTED
---|---
|  txnτ = $\bot$
| $m$ $\in$ $\mathit{OM}_{\tau}$
eff |  wrSett:=$\emptyset$
|  rdSett:=$\emptyset$
| beginIdxt:= $m$
| seenIdxst:=$\emptyset$
| synctypet:=${\it sflag}$
|  regst:=${\it regSet}$
|  txnτ:=$t$
|  statust:=READY
TxWriteτ($x,v$)
| pre |  statust = READY
---|---
|  txnτ = $t$
eff |  wrSett:=wrSett$\cup\\{x\mapsto v\\}$
TxReadIntτ($x,r$)
| pre |  statust = READY
---|---
|  $x\mapsto v\in$ wrSett
|  $r\in{}$regst
|  txnτ = $t$
eff |  $r$:=$v$
|  TxReadExtτ($x,i,r$)
---
| pre |  statust = READY
---|---
|  $x\notin\operatorname{\mathbf{dom}}$(wrSett)
|  beginIdx${}_{t}\leq i<|M|$
|  rdSet${}_{t}\subseteq M_{i}$
|  txnτ = $t$
eff |  rdSett:=rdSet${}_{t}\cup\\{x\mapsto M_{i}(x)\\}$
| if $S_{i}\in\\{{\sf R},{\sf RA}\\}$
| then seenIdxst:= seenIdxs${}_{t}\cup\\{i\\}$
|  $r$:=$M_{i}(x)$
TxRead${}_{\tau}(x,r)$ =
|  TxReadInt${}_{\tau}(x)\sqcap{}$ $\bigsqcap_{i}$TxReadExt${}_{\tau}(x,i,r)$
---
|  TxEndROτ
---
| pre |  statust = READY
---|---
|  wrSet${}_{t}=\emptyset$
|  txnτ = $t$
eff |  statust:=COMMIT
| if synctype${}_{t}\in\\{{\sf A},{\sf
RA}\\}\wedge{}$seenIdxs${}_{t}\neq\emptyset$
| then
|  let nv${}={\it view}$(seenIdxst,V) in
|  ${\tt tview}_{\tau}$:= ${\tt tview}_{\tau}\otimes{}$nv
|  txnτ:=$\bot$
| ${\tt txview}_{\tau}$:= $\max$(seenIdxst)
TxEndWRτ
| pre |  statust = READY
---|---
|  wrSet${}_{t}\neq\emptyset$
|  rdSet${}_{t}\subseteq\mathit{last}(M)$
|  txnτ = $t$
eff |  $M$:= $M\cdot(\mathit{last}(M)\oplus{}$wrSet${}_{t})$
|  statust:=COMMIT
| if synctype${}_{t}\in\\{{\sf A},{\sf
RA}\\}\wedge{}$seenIdxs${}_{t}\neq\emptyset$
| then
|  let nv${}={\it view}$(seenIdxst,V) in
|  $V$:= $V\cdot{}({\tt tview}_{\tau}\otimes{}$nv)
|  ${\tt tview}_{\tau}$:= ${\tt tview}_{\tau}\otimes{}$nv
| else $V$:= $V\cdot{}{\tt tview}_{\tau}$
| $S$:= $S\cdot{}$synctypet
|  txnτ:=$\bot$
| ${\tt txview}_{\tau}$:= $\max$(seenIdxst)
Abortτ
| pre |  statust = READY
---|---
|  txnτ = $t$
eff |  $\forall s\in{}$regst. $s$:=$\bot$
|  txnt:=$\bot$
|  statust:=ABORT
TXBegin${}_{\tau}({\it sflag},{\it regSet})$ = $\bigsqcap_{m}$
TXBeginV${}_{\tau}({\it sflag},m,{\it regSet})$
TxEndτ =  |  TxEndRO${}_{\tau}\sqcap{}$TxEndWRτ
---

where |
---|---
$M:{\it seq}({\it Loc}\to\mathit{Val})$, initially $M=\langle(\lambda v\in{\it Loc}.0)\rangle$ | $S:{\it seq}\\{\sf RX,R,A,RA\\}$, initially $S=\langle\sf RX\rangle$
$V:{\it seq}({\it Loc}\to{\it TS})$, initially $V=\langle(\lambda v\in{\it Loc}.0)\rangle$ | ${\it view}({\it Idxs},{\it Vf})=\lambda l\in{\it Loc}.\ {\it maxWr}\\{{\it Vf}_{i}(l)\mid i\in{\it Idxs}\\}$
$\mathit{OM}_{\tau}=\\{n~{}|~{}n\geq{\tt txview}_{\tau}\land n\leq|M|-1\\}$ |

Figure 4. TMS2-ra specification: highlighted components are extensions
necessary for client synchronisation for C11 transactions. We assume that the
transactions are executed by thread $\tau$. Moreover, let $Q\cdot a$ be the
sequence $Q$ appended with element $a$ and $f\oplus g$ be the function $f$
overridden by function $g$. Finally, let ${\it maxWr}$ be a function that
returns the write with the largest timestamp in the given set of writes.

WTMS specification

###  3.3. TMS2-ra

$d$$M$$\tau{2}$$\tau{1}$$0,0$$5,1$$\\{f\mapsto 0\\}^{\sf RX}$$\\{f\mapsto
1\\}^{\sf R}$

$\sigma_{2}$ (after executing line 4)

$d$$M$$\tau{2}$$\tau{1}$$0,0$$5,1$$\\{f\mapsto 0\\}^{\sf RX}$$\\{f\mapsto
1\\}^{\sf R}$

$\sigma_{3}$ (after executing line 8)

(a) Views for transactional MP (Fig. 2)

$d_{1}$$M$$\tau{2}$$\tau{1}$$0,0$$5,1$$\left\\{\begin{array}[]{@{}l@{}}f\mapsto
0,\\\ d_{2}\mapsto 0\end{array}\right\\}^{\sf
RX}$$\left\\{\begin{array}[]{@{}l@{}}f\mapsto 1,\\\ d_{2}\mapsto
10\end{array}\right\\}^{\sf RX}$

$\sigma_{2}$ (after executing line 5)

$d_{1}$$M$$\tau{2}$$\tau{1}$$0,0$$5,1$$\left\\{\begin{array}[]{@{}l@{}}f\mapsto
0,\\\ d_{2}\mapsto 0\end{array}\right\\}^{\sf
RX}$$\left\\{\begin{array}[]{@{}l@{}}f\mapsto 1,\\\ d_{2}\mapsto
10\end{array}\right\\}^{\sf RX}$

$\sigma_{3}$ (after executing line 10)

(b) Views for relaxed transactions (Fig. 2)

$M$$d_{1}$$d_{2}$$\tau{3}$$\tau{2}$$\tau{1}$$0,0$$5,1$$0,0$$\left\\{\begin{array}[]{@{}l@{}}f\mapsto
0\end{array}\right\\}^{\sf RX}$$\left\\{\begin{array}[]{@{}l@{}}f\mapsto
1\end{array}\right\\}^{\sf R}$

$\sigma_{2}$ (after executing line 4)

$M$$d_{1}$$d_{2}$$\tau{3}$$\tau{2}$$\tau{1}$$0,0$$5,1$$0,0$$10,1$$\left\\{\begin{array}[]{@{}l@{}}f\mapsto
0\end{array}\right\\}^{\sf RX}$$\left\\{\begin{array}[]{@{}l@{}}f\mapsto
1\end{array}\right\\}^{\sf R}$$\left\\{\begin{array}[]{@{}l@{}}f\mapsto
2\end{array}\right\\}^{\sf RA}$

$\sigma_{4}$ (after executing line 10)

$M$$d_{1}$$d_{2}$$\tau{3}$$\tau{2}$$\tau{1}$$0,0$$5,1$$0,0$$10,1$$\left\\{\begin{array}[]{@{}l@{}}f\mapsto
0\end{array}\right\\}^{\sf RX}$$\left\\{\begin{array}[]{@{}l@{}}f\mapsto
1\end{array}\right\\}^{\sf R}$$\left\\{\begin{array}[]{@{}l@{}}f\mapsto
2\end{array}\right\\}^{\sf RA}$

$\sigma_{5}$ (after executing line 13)

(c) Views for release-acquire transaction chain (Fig. 2)

Figure 5. Views for the transaction-based client program from Fig. 2

Views for the transaction-based client program from Fig. 2

We now discuss the release-acquire extensions of TMS2-ra, as defined by the
I/O automata algorithm in Fig. 4, including the highlighted components. The
key extension of TMS2-ra is its ability to synchronise client threads, thus
allowing it to cope with the examples in Fig. 2. Formally, this is achieved by
ensuring TMS2-ra synchronises the thread view of the client whenever
transactional release-acquire synchronisation occurs.

We introduce two new local variables in transaction $t$. Namely, synctypet,
which records the type of synchronisation of $t$, and seenIdxst, which records
the set of all memory indices seen by $t$ that are either releasing or
release-acquiring. We also introduce a new thread local variable ${\tt
txview}$, which records the transaction thread view of $\tau$. The transaction
thread view is similar to thread view introduced in §3.1. The difference here
is in the definition of ${\it View}$. In this context the ${\it View}$ is a
function that maps the threads to memory indexes of $M$. The transaction view
of $\tau$ is the smallest memory in $M$ that can be read by any transaction
$t$ that was begun by thread $\tau$. We also introduce two global variables.
Namely $S$, which is a sequence recording the type of each committed writing
transaction that installs each new memory in $M$, and $V$ which is a sequence
of modification views for each new memory in $M$. Thus, in TMS2-ra, memory
$M_{i}$ has synchronisation type $S_{i}$, and modification view $V_{i}$.

The transactional operations of TMS2 are modified as follows. In TxBegint, we
take as input the type of synchronisation transaction $t$ is to perform, and
store this value in synctypet. Another input to TxBegint is $m$, an index to a
visible memory $M$. We also initialise seenIdxst to the empty set. In
TxReadExt${}_{t}(x,i)$, i.e., a transition for external read of $x$ from
memory index $i$, we record the index $i$ in seenIdxst if the memory $M_{i}$
is releasing or release-acquiring.

When a transaction ends (for both read-only and writing transactions), if the
transaction is acquiring or release-acquiring and seenIdxst is non-empty, we
construct a new view nv to be the maximum modification view for each
transaction in seenIdxst using the function ${\it view}$. We use this to
synchronise the client thread’s view by updating ${\tt tview}_{\tau}$ to ${\tt
tview}_{\tau}\otimes{}$nv. For a writing transaction, we record this new view
of the client in $V$ so that any future transactions that synchronise with
this new transaction does so with respect to this view. Finally, once a
transaction ends, it updates ${\tt txview}$ to the largest index in
$\mathtt{seenIdxs}$.

We demonstrate the interaction of TMS2-ra and a client program by considering
the views of three possible executions of the programs in Fig. 5. Unlike the
trace considered in Fig. 3, we only show the most critical transitions. The
memory sequence $M$ of TMS2-ra is clear from the figures. We represent $S$ by
the superscripts on each state of $M$, and the modification views $V$ by the
dotted arrows () from each state of $M$.

Fig. 5 represents part of an execution of the program in Fig. 2. In the
execution depicted, we assume that all of thread $\tau{1}$ executes before
$\tau{2}$. Here, $\sigma_{2}$ is the state after executing line $4$, where
$\tau{1}$ has introduced a new write to $d$ and then executed its (releasing)
transaction, introducing a new memory snapshot whose modification view becomes
the new write of $d$ (since $\tau{1}$’s thread view is at this new write).
Then, when $\tau{2}$ executes its (acquiring) transaction that reads $1$ from
$f$, it synchronises with the latest memory snapshot, causing $\tau{2}$’s
thread view to be the new write of $d$ as well. This is analogous, as
required, to the way in which views are updated in C11 (see Fig. 3).

Fig. 5 represents a part execution of the program in Fig. 2. Again, we assume
a complete execution of thread $\tau{1}$ followed by $\tau{2}$. State
$\sigma_{2}$ is the state after executing line 5, where $\tau{1}$ has
introduced a new write to $d_{1}$. Now consider the state $\sigma_{3}$ (the
state after execution of line $10$), where $\tau{1}$ introduces a new memory
snapshot in $M$ with annotation RX and modification view pointing to the new
write on $d_{1}$. When $\tau{2}$ continues execution, its transaction must be
ordered after the latest memory snapshot, but this will not induce a release-
acquire synchronisation. This means that $\tau{2}$’s view of $d_{2}$ will not
be updated. However, since $\tau{2}$’s transaction occurs after $\tau{1}$’s
transaction, $\tau{2}$ is guaranteed to read $10$ for $d_{2}$. Note that the
transaction executed by $\tau{2}$ is a read-only relaxed transaction, the view
of $\tau{2}$ of the client variable ($d_{1}$) is unchanged. However,
$\tau{2}$’s view of the transactional memory (not shown in the diagrams) will
be updated to the new memory state $\\{f\mapsto 1,d_{2}\mapsto 10\\}$.

Finally, Fig. 5 represents part of an execution of Fig. 2 comprising the
complete execution of $\tau{1}$, $\tau{2}$ then $\tau{3}$ in order. State
$\sigma_{2}$ represents the state after executing line 4, where the
modification view of the newly installed memory is consistent with the view of
the executing thread $\tau{1}$. Then, in $\sigma_{4}$ (the state after
execution of line 10), we have a new write on $d_{2}$ with value 10 and a
further new snapshot that synchronises with the snapshot $\\{f\mapsto
1\\}^{\sf R}$ causing the thread view of $\tau{2}$ and the modification view
of the new snapshot to be updated to the last writes of $d_{1}$ and $d_{2}$.
Next, in $\sigma_{5}$, when $\tau{3}$ executes its transaction, this
transaction is guaranteed to synchronise with $\\{f\mapsto 2\\}^{\sf RA}$,
causing $\tau{3}$’s view to be updated to the latest writes of $d_{1}$ and
$d_{2}$, which is inherited from the modification view of $\\{f\mapsto
2\\}^{\sf RA}$.

###  3.4. Modular operational semantics

$\inference[{\sc TxBegin}$_τ(sflag, m,
regSet)$]{\gamma.\mathtt{status}_{t}={\tt
NOTSTARTED}\qquad\gamma.\mathtt{txn}_{\tau}=\bot\qquad m\in
vmems_{\tau}}{\mathit{lst},\gamma,\beta\ \mathrel{\raisebox{0.90005pt}{
\\!\\!\\!\\! \leavevmode\hbox to52.19pt{\vbox
to5.17pt{\pgfpicture\makeatletter\hbox{\hskip 26.09544pt\lower-3.19313pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.60231pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\scriptstyle~{}~{}~{}~{}~{}~{}~{}~{}~{}\
~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.71132pt}\pgfsys@invoke{ }{}{{
{\pgfsys@beginscope\pgfsys@setlinewidth{0.56906pt}\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{}
{}{}{} {}{}{}
\pgfsys@moveto{-1.48018pt}{1.97357pt}\pgfsys@curveto{-1.35683pt}{1.23347pt}{0.0pt}{0.12334pt}{0.37004pt}{0.0pt}\pgfsys@curveto{0.0pt}{-0.12334pt}{-1.35683pt}{-1.23347pt}{-1.48018pt}{-1.97357pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{25.08522pt}{-2.13748pt}\pgfsys@lineto{21.73979pt}{-2.13748pt}\pgfsys@lineto{20.88622pt}{-2.83748pt}\pgfsys@lineto{19.17905pt}{-1.43748pt}\pgfsys@lineto{17.47188pt}{-2.83748pt}\pgfsys@lineto{15.76471pt}{-1.43748pt}\pgfsys@lineto{14.05754pt}{-2.83748pt}\pgfsys@lineto{12.35037pt}{-1.43748pt}\pgfsys@lineto{10.6432pt}{-2.83748pt}\pgfsys@lineto{8.93604pt}{-1.43748pt}\pgfsys@lineto{7.22887pt}{-2.83748pt}\pgfsys@lineto{5.5217pt}{-1.43748pt}\pgfsys@lineto{3.81453pt}{-2.83748pt}\pgfsys@lineto{2.10736pt}{-1.43748pt}\pgfsys@lineto{0.40019pt}{-2.83748pt}\pgfsys@lineto{-1.30698pt}{-1.43748pt}\pgfsys@lineto{-3.01414pt}{-2.83748pt}\pgfsys@lineto{-4.72131pt}{-1.43748pt}\pgfsys@lineto{-6.42848pt}{-2.83748pt}\pgfsys@lineto{-8.13565pt}{-1.43748pt}\pgfsys@lineto{-9.84282pt}{-2.83748pt}\pgfsys@lineto{-11.54999pt}{-1.43748pt}\pgfsys@lineto{-13.25716pt}{-2.83748pt}\pgfsys@lineto{-14.96432pt}{-1.43748pt}\pgfsys@lineto{-16.6715pt}{-2.83748pt}\pgfsys@lineto{-18.37866pt}{-1.43748pt}\pgfsys@lineto{-20.08583pt}{-2.83748pt}\pgfsys@lineto{-21.793pt}{-1.43748pt}\pgfsys@lineto{-23.50017pt}{-2.83748pt}\pgfsys@lineto{-25.73979pt}{-2.13748pt}\pgfsys@lineto{-25.73979pt}{-2.13748pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.08522pt}{-2.13748pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}_{\tau}\
\mathit{lst},\gamma\left[\begin{array}[c]{@{}l@{}}\mathtt{beginIdx}_{t}:=m,\mathtt{seenIdxs}_{t}:=\emptyset,\mathtt{rdSet}_{t}:=\emptyset,\\\
\mathtt{wrSet}_{t}:=\emptyset,\mathtt{synctype}_{t}:={\it
sflag},\mathtt{regs}_{t}:={\it regSet},\\\ \mathtt{status}_{t}={\tt
READY},\mathtt{txn}_{\tau}:=t\par\end{array}\right],\beta}$

$\inference[{\sc TxWrite}$_τ(l, v)$]{\gamma.\mathtt{status}_{t}={\tt
READY}\qquad\gamma.\mathtt{txn}_{\tau}=t}{\mathit{lst},\gamma,\beta\
\mathrel{\raisebox{0.90005pt}{ \\!\\!\\!\\! \leavevmode\hbox to52.19pt{\vbox
to5.13pt{\pgfpicture\makeatletter\hbox{\hskip 26.09544pt\lower-3.19313pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.60231pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\scriptstyle~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}\
~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.71132pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{25.08522pt}{-2.13748pt}\pgfsys@lineto{21.73979pt}{-2.13748pt}\pgfsys@lineto{20.88622pt}{-2.83748pt}\pgfsys@lineto{19.17905pt}{-1.43748pt}\pgfsys@lineto{17.47188pt}{-2.83748pt}\pgfsys@lineto{15.76471pt}{-1.43748pt}\pgfsys@lineto{14.05754pt}{-2.83748pt}\pgfsys@lineto{12.35037pt}{-1.43748pt}\pgfsys@lineto{10.6432pt}{-2.83748pt}\pgfsys@lineto{8.93604pt}{-1.43748pt}\pgfsys@lineto{7.22887pt}{-2.83748pt}\pgfsys@lineto{5.5217pt}{-1.43748pt}\pgfsys@lineto{3.81453pt}{-2.83748pt}\pgfsys@lineto{2.10736pt}{-1.43748pt}\pgfsys@lineto{0.40019pt}{-2.83748pt}\pgfsys@lineto{-1.30698pt}{-1.43748pt}\pgfsys@lineto{-3.01414pt}{-2.83748pt}\pgfsys@lineto{-4.72131pt}{-1.43748pt}\pgfsys@lineto{-6.42848pt}{-2.83748pt}\pgfsys@lineto{-8.13565pt}{-1.43748pt}\pgfsys@lineto{-9.84282pt}{-2.83748pt}\pgfsys@lineto{-11.54999pt}{-1.43748pt}\pgfsys@lineto{-13.25716pt}{-2.83748pt}\pgfsys@lineto{-14.96432pt}{-1.43748pt}\pgfsys@lineto{-16.6715pt}{-2.83748pt}\pgfsys@lineto{-18.37866pt}{-1.43748pt}\pgfsys@lineto{-20.08583pt}{-2.83748pt}\pgfsys@lineto{-21.793pt}{-1.43748pt}\pgfsys@lineto{-23.50017pt}{-2.83748pt}\pgfsys@lineto{-25.73979pt}{-2.13748pt}\pgfsys@lineto{-25.73979pt}{-2.13748pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.08522pt}{-2.13748pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}_{\tau}\
\mathit{lst},\gamma\left[\begin{array}[c]{@{}l@{}}\mathtt{wrSet}_{t}:=\gamma.\mathtt{wrSet}_{t}\cup\\{l\mapsto
v\\}\end{array}\right],\beta}$

$\inference[{\sc TxRead}$_τ(l, r)$]{\gamma.\mathtt{status}_{t}={\tt
READY}\qquad\gamma.\mathtt{txn}_{\tau}=t\qquad r\in\gamma.\mathtt{regs}_{t}\\\
(l\in\operatorname{\mathbf{dom}}(\gamma.\mathtt{wrSet}_{t})\lor(\gamma.\mathtt{beginIdx}_{t}\leq
i~{}\land\gamma.\mathtt{rdSet}_{t}\subseteq\gamma.\mathit{M}_{i}))\\\
\begin{array}[t]{@{}r@{~}l}v=~{}&\textsf{{if}}\
l\notin\operatorname{\mathbf{dom}}(\gamma.\mathtt{wrSet}_{t})~{}\textsf{{then}}~{}\gamma.\mathit{M}_{i}(l)~{}\textsf{{else}}~{}\gamma.\mathtt{wrSet}_{t}(l)\\\\[2.0pt]
\mathtt{seenIdxs}^{\prime}=~{}&\textsf{{if}}\
l\notin\operatorname{\mathbf{dom}}(\gamma.\mathtt{wrSet}_{t})\wedge\gamma.S_{i}\in\\{\mathsf{R},\mathsf{R}\mathsf{A}\\}\\\
~{}&\textsf{{then}}~{}\gamma.\mathtt{seenIdxs}_{t}\cup\\{i\\}~{}\textsf{{else}}~{}\gamma.\mathtt{seenIdxs}_{t}\\\\[2.0pt]
\mathtt{rdSet}^{\prime}=~{}&\textsf{{if}}\
l\notin\operatorname{\mathbf{dom}}(\gamma.\mathtt{wrSet}_{t})~{}\textsf{{then}}~{}\gamma.\mathtt{rdSet}_{t}\cup\\{l\mapsto
v\\}~{}\textsf{{else}}~{}\gamma.\mathtt{rdSet}_{t}\end{array}}{\mathit{lst},\gamma,\beta\
\mathrel{\raisebox{0.90005pt}{ \\!\\!\\!\\! \leavevmode\hbox to52.19pt{\vbox
to5.13pt{\pgfpicture\makeatletter\hbox{\hskip 26.09544pt\lower-3.19313pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.60231pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\scriptstyle~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}\
~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.71132pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{25.08522pt}{-2.13748pt}\pgfsys@lineto{21.73979pt}{-2.13748pt}\pgfsys@lineto{20.88622pt}{-2.83748pt}\pgfsys@lineto{19.17905pt}{-1.43748pt}\pgfsys@lineto{17.47188pt}{-2.83748pt}\pgfsys@lineto{15.76471pt}{-1.43748pt}\pgfsys@lineto{14.05754pt}{-2.83748pt}\pgfsys@lineto{12.35037pt}{-1.43748pt}\pgfsys@lineto{10.6432pt}{-2.83748pt}\pgfsys@lineto{8.93604pt}{-1.43748pt}\pgfsys@lineto{7.22887pt}{-2.83748pt}\pgfsys@lineto{5.5217pt}{-1.43748pt}\pgfsys@lineto{3.81453pt}{-2.83748pt}\pgfsys@lineto{2.10736pt}{-1.43748pt}\pgfsys@lineto{0.40019pt}{-2.83748pt}\pgfsys@lineto{-1.30698pt}{-1.43748pt}\pgfsys@lineto{-3.01414pt}{-2.83748pt}\pgfsys@lineto{-4.72131pt}{-1.43748pt}\pgfsys@lineto{-6.42848pt}{-2.83748pt}\pgfsys@lineto{-8.13565pt}{-1.43748pt}\pgfsys@lineto{-9.84282pt}{-2.83748pt}\pgfsys@lineto{-11.54999pt}{-1.43748pt}\pgfsys@lineto{-13.25716pt}{-2.83748pt}\pgfsys@lineto{-14.96432pt}{-1.43748pt}\pgfsys@lineto{-16.6715pt}{-2.83748pt}\pgfsys@lineto{-18.37866pt}{-1.43748pt}\pgfsys@lineto{-20.08583pt}{-2.83748pt}\pgfsys@lineto{-21.793pt}{-1.43748pt}\pgfsys@lineto{-23.50017pt}{-2.83748pt}\pgfsys@lineto{-25.73979pt}{-2.13748pt}\pgfsys@lineto{-25.73979pt}{-2.13748pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.08522pt}{-2.13748pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}_{\tau}\
\mathit{lst}[r:=v],\gamma\left[\begin{array}[c]{@{}l@{}}\mathtt{rdSet}_{t}:=\mathtt{rdSet}^{\prime},\mathtt{seenIdxs}_{t}:=\mathtt{seenIdxs}^{\prime}\end{array}\right],\beta}$

$\inference[{\sc TxEndRO}$_τ$]{\gamma.\mathtt{status}_{t}={\tt
READY}\qquad\gamma.\mathtt{txn}_{\tau}=t\qquad\gamma.\mathtt{wrSet}_{t}=\emptyset\\\
{\tt
tview}^{\prime}=\begin{array}[t]{@{}l}\textsf{{if}}~{}\gamma.\mathtt{rdSet}_{t}\neq\emptyset\land\gamma.\mathtt{synctype}_{t}\in\\{\mathsf{A},\mathsf{R}\mathsf{A}\\}\wedge\gamma.\mathtt{seenIdxs}_{t}\neq\emptyset\\\
\textsf{{then}}~{}\beta.{\tt tview}_{\tau}\otimes{\it
view}(\gamma.\mathtt{seenIdxs}_{t},\gamma.V)~{}\textsf{{else}}~{}\beta.{\tt
tview}_{\tau}\end{array}}{\mathit{lst},\gamma,\beta\
\mathrel{\raisebox{0.90005pt}{ \\!\\!\\!\\! \leavevmode\hbox to52.19pt{\vbox
to5.13pt{\pgfpicture\makeatletter\hbox{\hskip 26.09544pt\lower-3.19313pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.60231pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\scriptstyle~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}\
~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.71132pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{25.08522pt}{-2.13748pt}\pgfsys@lineto{21.73979pt}{-2.13748pt}\pgfsys@lineto{20.88622pt}{-2.83748pt}\pgfsys@lineto{19.17905pt}{-1.43748pt}\pgfsys@lineto{17.47188pt}{-2.83748pt}\pgfsys@lineto{15.76471pt}{-1.43748pt}\pgfsys@lineto{14.05754pt}{-2.83748pt}\pgfsys@lineto{12.35037pt}{-1.43748pt}\pgfsys@lineto{10.6432pt}{-2.83748pt}\pgfsys@lineto{8.93604pt}{-1.43748pt}\pgfsys@lineto{7.22887pt}{-2.83748pt}\pgfsys@lineto{5.5217pt}{-1.43748pt}\pgfsys@lineto{3.81453pt}{-2.83748pt}\pgfsys@lineto{2.10736pt}{-1.43748pt}\pgfsys@lineto{0.40019pt}{-2.83748pt}\pgfsys@lineto{-1.30698pt}{-1.43748pt}\pgfsys@lineto{-3.01414pt}{-2.83748pt}\pgfsys@lineto{-4.72131pt}{-1.43748pt}\pgfsys@lineto{-6.42848pt}{-2.83748pt}\pgfsys@lineto{-8.13565pt}{-1.43748pt}\pgfsys@lineto{-9.84282pt}{-2.83748pt}\pgfsys@lineto{-11.54999pt}{-1.43748pt}\pgfsys@lineto{-13.25716pt}{-2.83748pt}\pgfsys@lineto{-14.96432pt}{-1.43748pt}\pgfsys@lineto{-16.6715pt}{-2.83748pt}\pgfsys@lineto{-18.37866pt}{-1.43748pt}\pgfsys@lineto{-20.08583pt}{-2.83748pt}\pgfsys@lineto{-21.793pt}{-1.43748pt}\pgfsys@lineto{-23.50017pt}{-2.83748pt}\pgfsys@lineto{-25.73979pt}{-2.13748pt}\pgfsys@lineto{-25.73979pt}{-2.13748pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.08522pt}{-2.13748pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}_{\tau}\
\mathit{lst},\gamma\left[\begin{array}[c]{@{}l@{}}\mathtt{status}_{t}:={\tt
COMMITTED},\\\ {\tt
txview}_{\tau}:=\max(\gamma.\mathtt{seenIdxs}_{t})\end{array}\right],\beta[{\tt
tview}_{\tau}:={\tt tview}^{\prime}]}$

$\inference[{\sc TxEndWR}$_τ$]{\gamma.\mathtt{status}_{t}={\tt
READY}\qquad\gamma.\mathtt{txn}_{\tau}=t\qquad\gamma.\mathtt{wrSet}_{t}\neq\emptyset\qquad
i=|\gamma.\mathit{M}|\\\
\mathit{S}^{\prime}=\gamma.\mathtt{synctype}_{t}\qquad
mem^{\prime}=(\mathit{last}(\gamma.\mathit{M})\oplus\gamma.\mathtt{wrSet}_{\tau})\\\
{\tt
tview}^{\prime}=\begin{array}[t]{@{}l}\textsf{{if}}~{}\gamma.\mathtt{rdSet}_{t}\neq\emptyset\land\gamma.\mathtt{synctype}_{t}\in\\{\mathsf{A},\mathsf{R}\mathsf{A}\\}\wedge\gamma.\mathtt{seenIdxs}_{t}\neq\emptyset\\\
\textsf{{then}}~{}\beta.{\tt tview}_{\tau}\otimes{\it
view}(\gamma.\mathtt{seenIdxs}_{t},\gamma.V)~{}\textsf{{else}}~{}\beta.{\tt
tview}_{\tau}\end{array}}{\mathit{lst},\gamma,\beta\
\mathrel{\raisebox{0.90005pt}{ \\!\\!\\!\\! \leavevmode\hbox to52.19pt{\vbox
to5.13pt{\pgfpicture\makeatletter\hbox{\hskip 26.09544pt\lower-3.19313pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.60231pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\scriptstyle~{}~{}~{}~{}~{}~{}\
~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}}{}{{}}{}{{}} {}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.71132pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{25.08522pt}{-2.13748pt}\pgfsys@lineto{21.73979pt}{-2.13748pt}\pgfsys@lineto{20.88622pt}{-2.83748pt}\pgfsys@lineto{19.17905pt}{-1.43748pt}\pgfsys@lineto{17.47188pt}{-2.83748pt}\pgfsys@lineto{15.76471pt}{-1.43748pt}\pgfsys@lineto{14.05754pt}{-2.83748pt}\pgfsys@lineto{12.35037pt}{-1.43748pt}\pgfsys@lineto{10.6432pt}{-2.83748pt}\pgfsys@lineto{8.93604pt}{-1.43748pt}\pgfsys@lineto{7.22887pt}{-2.83748pt}\pgfsys@lineto{5.5217pt}{-1.43748pt}\pgfsys@lineto{3.81453pt}{-2.83748pt}\pgfsys@lineto{2.10736pt}{-1.43748pt}\pgfsys@lineto{0.40019pt}{-2.83748pt}\pgfsys@lineto{-1.30698pt}{-1.43748pt}\pgfsys@lineto{-3.01414pt}{-2.83748pt}\pgfsys@lineto{-4.72131pt}{-1.43748pt}\pgfsys@lineto{-6.42848pt}{-2.83748pt}\pgfsys@lineto{-8.13565pt}{-1.43748pt}\pgfsys@lineto{-9.84282pt}{-2.83748pt}\pgfsys@lineto{-11.54999pt}{-1.43748pt}\pgfsys@lineto{-13.25716pt}{-2.83748pt}\pgfsys@lineto{-14.96432pt}{-1.43748pt}\pgfsys@lineto{-16.6715pt}{-2.83748pt}\pgfsys@lineto{-18.37866pt}{-1.43748pt}\pgfsys@lineto{-20.08583pt}{-2.83748pt}\pgfsys@lineto{-21.793pt}{-1.43748pt}\pgfsys@lineto{-23.50017pt}{-2.83748pt}\pgfsys@lineto{-25.73979pt}{-2.13748pt}\pgfsys@lineto{-25.73979pt}{-2.13748pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.08522pt}{-2.13748pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}_{\tau}\
\mathit{lst},\gamma\left[\begin{array}[c]{@{}l@{}}\mathtt{status}_{t}:={\tt
COMMITTED},\mathit{M}_{i}:=mem^{\prime}\\\
\mathit{S}_{i}:=\mathit{S}^{\prime},\mathtt{V}_{i}:={\tt tview}^{\prime}\\\
{\tt
txview}_{\tau}:=\max(\gamma.\mathtt{seenIdxs}_{t})\end{array}\right],\beta[{\tt
tview}_{\tau}:={\tt tview}^{\prime}]}$

$\inference[{\sc TxAbort}$_τ$]{\gamma.\mathtt{status}_{t}={\tt
READY}\qquad\gamma.\mathtt{txn}_{\tau}=t\qquad\mathit{lst}^{\prime}=\lambda
r\in\mathit{Reg}.\ \textsf{{if}}\ r\in\gamma.\mathtt{regs}_{t}\
\textsf{{then}}\ \bot\ \textsf{{else}}\
\mathit{lst}(r)}{\mathit{lst},\gamma,\beta\ \mathrel{\raisebox{0.90005pt}{
\\!\\!\\!\\! \leavevmode\hbox to52.19pt{\vbox
to5.13pt{\pgfpicture\makeatletter\hbox{\hskip 26.09544pt\lower-3.19313pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.60231pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\scriptstyle~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}\
~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.71132pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{25.08522pt}{-2.13748pt}\pgfsys@lineto{21.73979pt}{-2.13748pt}\pgfsys@lineto{20.88622pt}{-2.83748pt}\pgfsys@lineto{19.17905pt}{-1.43748pt}\pgfsys@lineto{17.47188pt}{-2.83748pt}\pgfsys@lineto{15.76471pt}{-1.43748pt}\pgfsys@lineto{14.05754pt}{-2.83748pt}\pgfsys@lineto{12.35037pt}{-1.43748pt}\pgfsys@lineto{10.6432pt}{-2.83748pt}\pgfsys@lineto{8.93604pt}{-1.43748pt}\pgfsys@lineto{7.22887pt}{-2.83748pt}\pgfsys@lineto{5.5217pt}{-1.43748pt}\pgfsys@lineto{3.81453pt}{-2.83748pt}\pgfsys@lineto{2.10736pt}{-1.43748pt}\pgfsys@lineto{0.40019pt}{-2.83748pt}\pgfsys@lineto{-1.30698pt}{-1.43748pt}\pgfsys@lineto{-3.01414pt}{-2.83748pt}\pgfsys@lineto{-4.72131pt}{-1.43748pt}\pgfsys@lineto{-6.42848pt}{-2.83748pt}\pgfsys@lineto{-8.13565pt}{-1.43748pt}\pgfsys@lineto{-9.84282pt}{-2.83748pt}\pgfsys@lineto{-11.54999pt}{-1.43748pt}\pgfsys@lineto{-13.25716pt}{-2.83748pt}\pgfsys@lineto{-14.96432pt}{-1.43748pt}\pgfsys@lineto{-16.6715pt}{-2.83748pt}\pgfsys@lineto{-18.37866pt}{-1.43748pt}\pgfsys@lineto{-20.08583pt}{-2.83748pt}\pgfsys@lineto{-21.793pt}{-1.43748pt}\pgfsys@lineto{-23.50017pt}{-2.83748pt}\pgfsys@lineto{-25.73979pt}{-2.13748pt}\pgfsys@lineto{-25.73979pt}{-2.13748pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.08522pt}{-2.13748pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}_{\tau}\
\mathit{lst}^{\prime},\gamma\left[\begin{array}[c]{@{}l@{}}\mathtt{status}_{t}:={\tt
ABORTED}\end{array}\right],\beta}$

Figure 6. Operational semantics for TMS2-RA

Operational semantics for TMS2-RA

To reason about clients that use abstract TMS2-ra transactions in a modular
fashion, we use configurations that are triples $(\mathit{lst},\gamma,\beta)$,
where $\mathit{lst}:\mathit{Reg}\to\mathit{Val}$ denotes the local register
state, $\gamma$ is the TMS2-ra state (which includes all transactional
variables described in Fig. 4) and $\beta$ is the C11 state of the client (see
(Dalvandi et al., 2020a, 2022), §A).

The transition relation for transactional operations is given in Fig. 6. These
follow the automata-style description given in Fig. 4, but make state
components that are affect more precise. The most interesting aspect of these
rules is the interaction between a releasing writing transaction and
subsequent committing reading transaction.

Note that each releasing writing transaction sets $S_{i}$ (where $i$ is last
index in $M$ at the time of writing) to either $\mathsf{R}$ or
$\mathsf{R}\mathsf{A}$. Additionally, the view of the thread at the time of
writing is recorded in $V_{i}$. A later transaction with an acquiring
annotation calculates a new view using the function ${\it view}$ as defined in
Fig. 4 and updates, among other components, the executing thread’s view in
$\beta$. This means that, as expected, if there is a release-acquire
synchronisation through a transactional memory library, then the client’s view
will be updated to match the synchronisation that occurs.

##  4\. A C11 STM implementation

In this section, we develop a release-acquire version of a transactional mutex
lock, that we call TML-ra, based on an SC implementation by Dalessandro et al
(Dalessandro et al., 2010). Our algorithm is provided in Fig. 7, where the
highlights indicate the fragments of code that we have introduced or modified.
The grey highlights represent code additional to Dalessandro et al’s original
implementation, and the blue highlights represent the necessary release-
acquire synchronisation.

We first discuss the core features of TML (§4.1), then discuss the extensions
introduced in TML-ra to optimise for C11 release-acquire synchronisation
(§4.2). We present the benchmarking results for both algorithms in §4.3. In
§6, we present a proof that TML-ra implements TMS2-ra, i.e., any observation a
client program makes when it uses TML-ra is a possible observation when it
uses TMS2-ra.

$\begin{array}[]{l@{\qquad}l}\lx@intercol${\bf Init: } ${\tt glb}:=0$
<EMAIL_ADDRESS>\begin{array}[t]{@{}l@{}}{\tt TxBegin}(${\it
regSet}$)\\\ B1\\!:{\tt regs}:=$ {\it regSet}$\\\
B2\\!:\hbox{\pagecolor{black!8}${\tt hasRead}:={\it false}$};\\\
B3\\!:\textsf{{do}}\ {\tt loc}\ \hbox{\pagecolor{blue!15}$\leftarrow^{\sf
A}$}\ {\tt glb};\\\ B4\\!:\textsf{{until}}\ even({\tt loc})\\\\[5.69054pt]
{\tt TxWrite}(x,v)\\\ W1\\!:\textsf{{if}}\ even({\tt loc})\ \textsf{{then}}\\\
W2\\!:\quad r_{1}\leftarrow\hbox{\pagecolor{blue!15}$\textsf{{CAS}}^{\sf
RA}$}({\tt glb},{\tt loc},{\tt loc+1})\\\ W3\\!:\quad\textsf{{if}}\ \neg
r_{1}\ \textsf{{then}}\\\ W4\\!:\qquad\forall s\in{\tt
regs}.\,s:=\bot;\textsf{{return}};\texttt{// ABORT}\\\
W5\\!:\quad\textsf{{else}}\ {\tt loc}:={\tt loc}+1;\\\ W6\\!:x\
\hbox{\pagecolor{blue!15}$:=^{\sf R}$}\ v;\texttt{ // WRITE OK}\\\\[5.69054pt]
{\tt TxEnd}\\\ E1\\!:\textsf{{if}}\ odd({\tt loc})\ \textsf{{then}}\\\
E2\\!:\quad{\tt glb}\ \hbox{\pagecolor{blue!15}$:=^{\sf R}$}\ {\tt
loc+1};\end{array}&\begin{array}[t]{@{}l@{~}l}\lx@intercol{\tt
TMRead}(x,r)\hfil\lx@intercol\\\ R1\\!:\hfil~{}&\textsf{{if}}\ r\in{\tt regs}\
\textsf{{then}}\\\ R2\\!:\hfil~{}&\quad r\
\hbox{\pagecolor{blue!15}$\leftarrow^{\sf A}$}\ x;\\\
R3\\!:\hfil~{}&\quad\textsf{{if}}\ \hbox{\pagecolor{black!8}${}\neg{\tt
hasRead}\wedge even({\tt loc})$}\ \textsf{{then}}\\\
R4\\!:\hfil~{}&\quad\quad\hbox{\pagecolor{black!8}$r_{1}\leftarrow\hbox{\pagecolor{blue!15}$\textsf{{CAS}}^{\sf
RA}$}({\tt glb},{\tt loc},{\tt loc})$}\\\
R5\\!:\hfil~{}&\quad\quad\hbox{\pagecolor{black!8}$\textsf{{if}}\ r_{1}\
\textsf{{then}}$}\\\ R6\\!:\hfil~{}&\quad\qquad\hbox{\pagecolor{black!8}${\tt
hasRead}:=true;$}\\\
R7\\!:\hfil~{}&\quad\qquad\hbox{\pagecolor{black!8}$\begin{array}[t]{@{}l@{}}\textsf{{return}};\
\ \texttt{// READ OK}\end{array}$}\\\ R8\\!:\hfil~{}&\quad\textsf{{else}}\\\
R9\\!:\hfil~{}&\quad\quad r_{1}\leftarrow{\tt glb};\\\
R10\\!:\hfil~{}&\quad\quad\textsf{{if}}\ r_{1}={\tt loc}\ \textsf{{then}}\\\
R11\\!:\hfil~{}&\quad\qquad\begin{array}[t]{@{}l@{}}\textsf{{return}};\ \
\texttt{// READ OK}\end{array}\\\ R12\\!:\hfil~{}&\forall s\in{\tt
regs}.\,s:=\bot;\texttt{// ABORT}\end{array}\end{array}$

Figure 7. TML-ra: A release-acquire transactional mutex lock. For simplicity,
the thread id is omitted

A release-acquire transactional mutex lock

###  4.1. TML

TML is synchronised using a single global counter glb, initialised to $0$,
where glb is even iff no writing transaction is currently executing.

A transaction begins by taking a snapshot of glb in local variable loc and
only begins if the value read is even.

A write operation checks that loc is even and if so, it attempts to increment
glb using the CAS at line $W2$. If this CAS succeeds, it increments loc (line
$W5$), then immediately updates the location $x$ (line $W6$). If the CAS
fails, the transaction aborts. Note that if loc is odd then the current
transaction “owns” the lock, meaning that lines $W2$-$W5$ can be bypassed.

A read operation (ignoring lines $R3$-$R7$ for now) reads the given location
into the given register $r$ (line $R2$). At lines $R9$ and $R10$ it checks
that glb is consistent with loc. If so, the read succeeds, otherwise, the
transaction aborts.

A transaction ends by checking whether the current transaction is a writing
transaction. This can be determined by checking whether loc is odd since a
writing transaction must have incremented glb via the CAS at line $W2$ and loc
via the write at line $W5$ making both their values odd. Therefore, a writing
transaction must increment glb to make it even again.

###  4.2. TML-ra

We now describe the necessary modifications to TML and the synchronisation
induced by TMS2-ra. We assume that transactions in TML-ra are all release-
acquiring and hence we omit the transaction annotation in TxBegin.

We assume all accesses to shared variables are either relaxed (e.g., the read
at line $R9$), releasing (e.g., the write at line $E2$), acquiring (e.g., the
read at line $B2$) or release-acquiring (e.g., the CAS at line $R4$).
Additionally, we introduce a new local variable hasRead, initially set to
${\it false}$ and a code path $R3$-$R7$, which is followed if a transaction
performs a read without having previously performed a read or a write. We
explain the purpose of this code path in more detail below.

##### Transaction synchronisation.

Recall that TMS2-ra requires that transactions are consistent w.r.t. a single
memory snapshot and that external reads of a transaction synchronise with
_some_ memory snapshot. This may not occur in a relaxed memory context without
adequate synchronisation. In particular, a writing transaction must perform a
releasing write to glb at line $E2$ so that if a later transaction reads from
this write, it synchronises with all of the writes performed by the writing
transaction. To ensure this, we require the read of glb at line $B3$ as well
as the CAS operations at lines $W2$ and $R4$ to be acquiring. Note that this
also guarantees release-acquire client synchronisation.

The second key synchronisation is between $W6$ performed by a writing
transaction $t_{w}$ and $R2$ performed by a (different) reading transaction
$t_{r}$. Suppose that both $t_{w}$ and $t_{r}$ are live. If $t_{r}$ happens to
read the write written at $W6$, it must now abort because $t_{r}$’s snapshot
of glb will be inconsistent with the latest value of glb installed by the
$t_{w}$. The release-acquire synchronisation between $W6$ and $R1$ ensures
that this will happen, i.e., $t_{r}$ will see the new glb written by $t_{w}$,
causing the test at $R10$ to fail and $t_{r}$ to abort.

##### Causal linearizability.

The design of TML-ra ensures that all transactions, including read-only
transactions are causally linearizable (Doherty et al., 2018), which is a
condition that additionally guarantees compositionality (or locality (Herlihy
and Wing, 1990; Sela et al., 2021)) of concurrent objects. This notion of
compositionality is that of Herlihy and Wing (Herlihy and Wing, 1990). In
particular, under SC memory, given a history comprising several concurrent
objects, if the history restricted to each object is linearizable, then the
history as a whole is linearizable. In a relaxed memory setting, Doherty et al
(Doherty et al., 2018) have shown that linearizability alone is insufficient
to guarantee compositionality, and it is necessary to induce a “happens-
before” relation when a specification induces a particular linearization.

The happens-before required by causal linearizability is naturally achieved
for writing transactions via the CAS at line $W2$. For a read-only
transaction, we introduce the CAS at line $R4$, which installs a new write to
glb without changing its value. All transactions that follow the CAS at line
$R4$ will be causally ordered after the reading transaction. Such a CAS must
only be performed once, thus we introduce a local variable hasRead, which is
set to true if the CAS succeeds so that later reads from the same transaction
can avoid the code path from $R3$-$R7$.

Note that the conditions necessary to guarantee causal linearizability (and
hence compositionality) could have been introduced at the level of TMS2-ra.
However, there are questions about whether the notion of compositionality
introduced by Herlihy and Wing (Herlihy and Wing, 1990) are appropriate in a
relaxed memory context (Raad et al., 2019a). Therefore we leave out the causal
linearizability conditions in TMS2-ra to avoid over-constraining the
specification.

Figure 8. Results of STAMP benchmarks for TML-ra and TML-sc

###  4.3. Benchmarking

We implemented two versions of the TML algorithm: TML-ra (see Fig. 7) and TML-
sc (the SC counterpart (Dalessandro et al., 2010)) and benchmarked both using
the STAMP benchmarking suite (Minh et al., 2008). Each experiment was repeated
20 times to rule out external loads on the test machine and an average of
these times was taken. The results of the six benchmarks that we ran with
STAMP are presented in Fig. 8. TML-ra is equivalent to or outperforms TML-sc
in almost all cases, with a maximum improvement of 20%. On average, TML-ra
performs 8.2% better than TML-sc.

Unsurprisingly, since TML optimises read-heavy workloads, its performance
degrades under high write contention, and this is consistent with prior
results (Dalessandro et al., 2010). However, it is interesting that the
degradation of TML-ra is not as severe as TML-sc for the Intruder and SSCA2
benchmarks.

TML-ra theoretically allows more parallelism than TML-sc since a read-only
transaction $t_{r}$ is not forced to abort if a writing transaction $t_{w}$
executes after $t_{r}$’s first read operation - $t_{r}$ must only aborts if it
sees $t_{w}$’s $glb$ update, or one of $t_{w}$’s writes. Both Intruder and
SSCA2 have a large number of short transactions; SSCA2 additionally has small
read/write sets (Minh et al., 2008). Here, TML-ra may be able to exploit the
theoretical parallelism. In the single-threaded case, TML-ra executes far
fewer heavyweight CASs.

As with prior results, we see that for the read-heavy benchmark Genome, the
performance of both TML-ra and TML-sc improves as the number of threads
increases.

##  5\. TARO: A logic for release-acquire TM

The development of view-based operational semantics for various fragments of
C11 (Kaiser et al., 2017; Dalvandi et al., 2020a; Kang et al., 2017) has
provided foundations for several logics for reasoning about C11 programs.
These include separation logics (Kaiser et al., 2017; Svendsen et al., 2018)
and extensions to Owicki-Gries reasoning (Wright et al., 2021; Lahav and
Vafeiadis, 2015; Dalvandi et al., 2022, 2020a). Our point of departure is the
Owicki-Gries encoding for RC11 RAR (Dalvandi et al., 2020a), which is the
fragment of C11 that we focus on in this paper.555These frameworks are based
on models that assume top-level parallelism only. Therefore, our framework
similarly re assumes top-level paralellism. This model can be extended to
support dynamic parallelism, but such extensions are uninteresting for the
purposes of this paper.

A key benefit of the logic in (Dalvandi et al., 2020a) is that it enables
reuse of standard Owicki-Gries proof decomposition rules and straightforward
mechanisation in Isabelle/HOL (Dalvandi et al., 2020b, 2022). As we shall see,
we maintain these benefits in the context of C11 with release-acquire
transactions. Our reasoning framework, called TARO, like Dalvandi et al
(Dalvandi et al., 2020a; Dalvandi and Dongol, 2021) uses view-based assertions
to abstractly describe the system state, allowing reasoning about the current
view of a thread, and view transfer from one thread to another through
release-acquire synchronisation. TARO introduces additional assertions to
enable reasoning about transactional views.

###  5.1. View-based assertions

In this section, we discuss the assertions and proof rules of TARO abstractly.
The proof rules can be used to reason syntactically about a program without
having to understand the low-level operational semantics of the C11 model. Our
operational semantics is an extension of prior works (Kaiser et al., 2017;
Dalvandi et al., 2020a; Kang et al., 2017) that include an encoding of
TMS2-ra.

$\begin{array}[]{@{}l@{~}||@{\,}l@{}}\lx@intercol\qquad{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[d=0]_{\tau{1}}\wedge[d=0]_{\tau{2}}\wedge[f=0]_{\tau{1}}\wedge[f=0]_{\tau{2}}\end{array}\right\\}}\hfil\\\
\begin{array}[t]{@{}l@{}}{\bf Thread}\ \tau{1}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{f}\approx
1]_{\tau{2}}\wedge[d=0]_{\tau{1}}\end{array}\right\\}}\\\ 1\\!:d:=5;\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{f}\approx
1]_{\tau{2}}\wedge[d=5]_{\tau{1}}\end{array}\right\\}}\\\
2\\!:\hbox{\pagecolor{black!8}${\tt TxBegin}(\sf R,\emptyset)$}\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{f}\approx
1]_{\tau{2}}\wedge[d=5]_{\tau{1}}\\\ {}\wedge{\it
Rel}_{\tau{1}}\end{array}\right\\}}\\\ 3\\!:\hbox{\pagecolor{black!8}${\tt
TxWrite}(f,1)$};\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\neg[\hat{f}\approx
1]_{\tau{2}}\wedge[d=5]_{\tau{1}}\\\ {}\wedge{\it
Rel}_{\tau{1}}\wedge(\hat{f},1)\in{\it WS}_{\tau{1}}\end{array}\right\\}}\\\
4\\!:\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}{\it
true}\end{array}\right\\}}\\\
\end{array}\hfil~{}&\begin{array}[t]{@{}r@{~}l@{}}\lx@intercol{\bf Thread}\
\tau{2}\hfil\lx@intercol\\\ 5\\!:~{}&\textsf{{do}}\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{f}=1\rangle[d=5]_{\tau{2}}\end{array}\right\\}}\hfil\\\
6\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxBegin}(\sf A,\\{r_{1}\\})$}\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{f}=1\rangle[d=5]_{\tau{2}}\wedge{\it
WS}_{\tau{2}}=\emptyset\wedge{\it Acq}_{\tau{2}}\end{array}\right\\}}\hfil\\\
7\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxRead}(f,r_{1})$};\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{f}=1\rangle[d=5]_{\tau{2}}\wedge{\it
WS}_{\tau{2}}=\emptyset\wedge{\it Acq}_{\tau{2}}\\\
{}\wedge(\hat{f},r_{1})\in{\it
RS}_{\tau{2}}\wedge(r_{1}=1\Rightarrow[d\stackrel{{\scriptstyle
S}}{{=}}5]_{\tau{2}})\end{array}\right\\}}\hfil\\\
8\\!:~{}&\hbox{\pagecolor{black!8}${\tt TxEnd}$};\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{f}=1\rangle[d=5]_{\tau{2}}\wedge(r_{1}=1\Rightarrow[d=5]_{\tau{2}})\end{array}\right\\}}\hfil\\\
9\\!:~{}&\textsf{{until}}\ r_{1}=1\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}[d=5]_{\tau{2}}\end{array}\right\\}}\hfil\\\
10\\!:~{}&r_{2}\leftarrow d\\\
\lx@intercol{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}r_{2}=5\end{array}\right\\}}\hfil\\\
\end{array}\end{array}$

$\\{r_{2}=5\\}$

Figure 9. Proof outline for transactional MP from Fig. 2

Proof outline for transactional MP

To motivate TARO, consider the proof outline in Fig. 9 for the transactional
message passing program from Fig. 2. We use ‘ $\hat{}$ ’ to distinguish
transactional locations in a proof. For the program in Fig. 9, we have a
transactional location $\hat{f}$.

####  5.1.1. View assertions

The proof outline contains three assertions from (Dalvandi et al., 2020a)
describing the views that each thread may have of the system state. Recall
(§3.1), that we can define the set of values that a thread can see in each
state using the function $OV$.

  * •

A definite value assertion, denoted $[x=v]_{\tau}$, holds iff thread $\tau$
sees the last write to location $x$ and this write has value $v$. Thus,
$[x=v]_{\tau}\Rightarrow OV_{\tau}(x)=\\{v\\}$.

  * •

A possible value assertion, denoted $[x\approx v]_{\tau}$, which holds iff
when $\tau$ can see a write to $x$ with value $v$. $[x\approx v]_{\tau}$ is
shorthand for $v\in OV_{\tau}(x)$.

  * •

A conditional value assertion, denoted $\langle y=u\rangle[x=v]_{\tau}$, which
holds iff an acquiring read of $y$ by $\tau$ that returns the value $u$ is
guaranteed to induce a release-acquire synchronisation so that $[x=v]_{\tau}$
holds after this read.

###### Example 0.

Consider the third state, i.e., $\sigma_{2}$ in Fig. 3. There, we have
$[d=5]_{\tau{1}}\wedge[f=1]_{\tau{1}}$ as well as $[f\approx
0]_{\tau{2}}\wedge[f\approx 1]_{\tau{2}}$. Moreover, we have $\langle
f=1\rangle[d=5]_{\tau{2}}$.

We ask the interested reader to consult (Dalvandi et al., 2020a, 2022) for
further details of these assertions.

####  5.1.2. Transactional assertions

As alluded to above, TARO introduces several new assertions to describe the
transactional state. These assertions are, in general, local to the
transaction being executed, and hence, stable under the execution of other
threads. Fig. 9 contains the following transaction local assertions:

  * •

${\it Rel}_{\tau}$, which holds iff $\tau$ is executing a releasing or
release-acquiring transaction.

  * •

${\it Acq}_{\tau}$, which holds iff $\tau$ is executing an acquiring or
release-acquiring transaction.

  * •

$(\hat{x},v)\in{\it WS}_{\tau}$ (and $(\hat{x},v)\in{\it RS}_{\tau}$), which
holds iff $\tau$ is executing a transaction whose write set (resp. read set)
contains a write to (resp. read of) $\hat{x}$ with value $v$.

  * •

$[x\stackrel{{\scriptstyle S}}{{=}}v]_{\tau}$, which holds iff $\tau$ is
executing a transaction such that committing this transaction results in the
definite value assertion $[x=v]_{\tau}$ (see above).

In addition, we include a number of assertions This section provides the
formal definition for the assertion language used in the verification of
client programs that use TMS2-RA (See §5.1). The assertion language presented
here is heavily inspired by the view-based assertion language presented in
(Dalvandi et al., 2020a).

A memory $i$ is visible to a transaction executed by a thread $\tau$ iff $i$
is greater than the transaction thread view of $\tau$ (${\tt txview}_{\tau}$)
and is less than the maximum index of the memory ($|M|-1$). We define the set
of visible memories $\mathit{OM}_{t}$ to be:

$\displaystyle\mathit{OM}_{\tau}=\\{n~{}|~{}n\geq{\tt txview}_{\tau}\land
n\leq|M|-1\\}$

  * •

A transactional definite observation assertion, denoted $[\hat{x}=v]_{t}$,
holds iff for all memory versions $i$, where $i$ is greater than or equal to
$\mathtt{beginIdx}_{t}$, the value of $\mathit{M}_{i}(x)$ is $v$. Formally,
for a transactional state $\gamma$:

$\displaystyle[\hat{x}=v]_{\tau}(\gamma)\ \ \mathrel{\hat{=}}\ \ \forall
i\in\gamma.\mathit{OM}_{\tau}.\ \gamma.\mathit{M}_{i}(\hat{x})=v$

These are lifted to client-object states $(\gamma,\beta)$ in the normal
manner, e.g., $[\hat{x}=v]_{\tau}(\gamma,\beta)=[\hat{x}=v]_{\tau}(\gamma)$

  * •

A transactional possible observation assertion, denoted $[\hat{x}\approx
v]_{\tau}$, holds iff there exists a memory version $i$ that has value $v$ for
$\hat{x}$. Formally:

$\displaystyle[\hat{x}\approx v]_{\tau}(\gamma)\ \ \mathrel{\hat{=}}\ \
\exists i\in\gamma.\mathit{OM}_{\tau}.\ \gamma.\mathit{M}_{i}(\hat{x})=v$

  * •

A transactional conditional observation assertion, denoted
$\langle\hat{y}=u\rangle[x=v]_{\tau}$, holds iff an acquiring transactional
read of $y$ by $\tau$ that returns a value $u$ is guaranteed to induce a
release-acquire synchronisation so that $[x\stackrel{{\scriptstyle
S}}{{=}}v]_{\tau}$ holds in the client state after the reading transaction
successfully commits. Formally:

$\displaystyle\langle\hat{y}=u\rangle[x=v]_{\tau}(\gamma,\beta)\ \
\mathrel{\hat{=}}\ \ \begin{array}[t]{@{}l@{}}\forall
i\in\gamma.\mathit{OM}_{\tau}.\ \gamma.\mathit{M}_{i}(\hat{y})=u\Rightarrow\\\
\qquad\gamma.{\it
V}_{i}(x)=\beta.last(x)\wedge\mathtt{val}(\beta.\mathit{last}(x))=v\land\gamma.\mathit{S}_{i}\end{array}$

where $last(x)$ is the last write to $x$ in the modification order. It is
important to note that this assertion is over two states: transaction state
$\gamma$ and client state $\beta$, explaining transfer of information across
two threads using the transactional memory. In particular, the transactional
view $V_{i}$ for the memory index $i$ must see the last write to $x$ in the
client state $\beta$. This means that the thread that committed the
transaction writing the value $u$ to $\hat{y}$ did so when it saw the last
write to $x$.

###### Example 0.

Returning to our transactional MP example (Fig. 9), the precondition of line 1
contains assertions $\neg[\hat{f}\approx 1]_{\tau{2}}$ and $[d=0]_{\tau{1}}$,
which ensure that, prior to executing line 1, thread $\tau{2}$ cannot see the
value $1$ for $\hat{f}$ and thread $\tau{1}$ must see the value $0$ for $d$,
respectively. In the postcondition of line 2, $[d=0]_{\tau{1}}$ changes to
$[d=5]_{\tau{1}}$ since $\tau{1}$ performs a write to $d$ with value $5$. The
other view-based assertions in $\tau{1}$ are similar. We explain the
transactional assertions involving ${\it Rel}$ and ${\it WS}$ below.

Now consider the assertions in thread $\tau{2}$. The precondition of line 6
(which is also the precondition of line 5) contains a conditional value
assertion $\langle\hat{f}=1\rangle[d=5]_{\tau{2}}$. This assertion ensures
that, if $\tau{2}$ reads the value 1 for $\hat{f}$ via an acquiring (or
release-acquiring) transaction, and this transaction successfuly commits, then
its view is guaranteed to be updated so that $[d=5]_{\tau{2}}$ holds. In a
transactional setting, we establish this fact in three steps.

  1. (1)

After executing line 7, we use $\langle\hat{f}=1\rangle[d=5]_{\tau{2}}$ to
establish that $r_{1}=1\Rightarrow[d\stackrel{{\scriptstyle
S}}{{=}}5]_{\tau{2}}$ holds. Note that $r_{2}$ stores the value $1$ returned
by a transactional read of $\hat{f}$. Thus,
$\langle\hat{f}=1\rangle[d=5]_{\tau{2}}$ is transformed into an implication
after the execution of line 7. The assertion $[d\stackrel{{\scriptstyle
S}}{{=}}5]_{\tau{2}}$ is a new assertion introduced in TARO, which states that
if the transaction executed by $\tau{2}$ commits, then $[d=5]_{\tau{2}}$ holds
in the post-state.

  2. (2)

If the transaction sucessfully commits (line 8), we use
$r_{1}=1\Rightarrow[d\stackrel{{\scriptstyle S}}{{=}}5]_{\tau{2}}$ to
establish $r_{1}=1\Rightarrow[d=5]_{\tau{2}}$ in the postcondition. Recall
that all registers used by a transaction are set to $\bot$ when a transaction
aborts, so if $\tau{2}$ reaches line 9 by aborting the transaction, then this
assertion is trivially true.

  3. (3)

We use $r_{1}=1\Rightarrow[d=5]_{\tau{2}}$ to establish $[d=5]_{\tau{2}}$
after the do-until loop, using the guard $r_{1}=1$ at line 9.

Finally, we use $[d=5]_{\tau{2}}$ in the precondition of line 10 to establish
the postcondition $r_{2}=5$. This is because $[d=5]_{\tau{2}}$ guarantees that
the only value $\tau{2}$ can read for $d$ is $5$.

###  5.2. TARO: Transactional Owicki-Gries Reasoning

Now that we have introduced the assertions used by TARO, we now review the
Owicki-Gries proof obligations. As discussed above, the use of view-based
assertions allows us to use the standard Owicki-Gries theory. Regardless, we
review the theory in the context of our language, which supports (abstract) TM
operations. Formally, we model programs as a labelled transition system, given
by the syntax in Fig. 10.

A command (of type ${\it ACom}$) is either a local assignment $r:={\it Exp}$,
a store to a shared location $x:=^{[{\sf R}]}{\it Exp}$, a load from a shared
location $r\leftarrow^{[{\sf A}]}x$, a compare-and-swap
$r\leftarrow\textsf{{CAS}}^{\sf[RX][R][A]}(x,u,v)$, or a transactional
operation. The annotations $\sf RX$, $\sf R$ and $\sf A$ are optional, as
indicated by the brackets ‘[’ and ‘]’. Thus, for example, both $x:=e$ and
$x:=^{\sf R}e$ are valid load commands; the former is relaxed and the latter
is releasing. A CAS may be annotated to be relaxed, or release and/or acquire.
Note that a CAS returns a boolean to indicate whether or not the compare-and-
swap has been successful. ${\tt TxBegin}([{\sf RX}][{\sf R}][{\sf A}])$, ${\tt
TxRead}(x,r)$, ${\tt TxWrite}(x,v)$ and ${\tt TxEnd}$ are transactional
operations, as defined by the TMS2-ra automata in Fig. 4.

$\begin{array}[]{@{} l
@{}}u,v\\!\in\\!\mathit{Val}\mathrel{\hat{=}}\mathbb{N}\qquad
x,y,\ldots\\!\in\\!{\it Loc}\qquad
r,r_{1},r_{2}\ldots\\!\in\\!\mathit{Reg}\qquad\tau,\tau{1},\tau{2},\ldots\\!\in\\!{\it
TId}\mathrel{\hat{=}}\mathbb{N}\qquad i,j,k,\ldots\\!\in\\!\mathit{Label}\\\
\begin{array}[]{@{} r @{\hspace{2pt}} l @{}}e\in{\it Exp}::=\hskip 2.0&v\mid
r\mid e{+}e\mid\cdots\\\ B\in{\it BExp}::=\hskip 2.0&{\it true}\mid B\land
B\mid\cdots\\\ \alpha\in{\it ACom}::=\hskip 2.0&r:={\it Exp}\mid
x:=^{\sf[R]}{\it Exp}\mid r\leftarrow^{\sf[A]}x\mid
r\leftarrow\textsf{{CAS}}^{\sf[RX][R][A]}(x,u,v)\mid{}\\\ \hskip 2.0&{\tt
TxBegin}([{\sf RX}][{\sf R}][{\sf A}],2^{\mathit{Reg}})\mid{\tt
TxRead}(x,r)\mid{\tt TxWrite}(x,v)\mid{\tt TxEnd}\\\\[2.84526pt]
ls\in\mathit{LCom}::=\hskip 2.0&\alpha\ {\bf goto}\ j\mid\textsf{{if}}\ B\
{\bf goto}\ j\ {\bf elseto}\ k\\\ \Pi\in{\it Prog}\mathrel{\hat{=}}\hskip
2.0&{\it TId}\times\mathit{Label}\to\mathit{LCom}\end{array}\end{array}$

Figure 10. Language syntax

Language syntax

We use a program counter variable $pc:{\it TId}\to Label$ to model control
flow, and model a program $\Pi$ as a function mapping each pair $(\tau,i)$ of
thread identifier and label to the _labelled statement_ (in $\mathit{LCom}$)
to be executed. A labelled statement may be  (i) a plain statement of the form
$\alpha\ {\bf goto}\ j$, comprising an atomic statement $\alpha$ to be
executed and the label $j$ of the next statement; or  (ii) a conditional
statement of the form $\textsf{{if}}\ B\ {\bf goto}\ j\ {\bf elseto}\ k$ to
accommodate branching, which proceeds to label $j$ if $B$ holds and to $k$,
otherwise.  We assume a designated label, $\iota\in\mathit{Label}$,
representing the _initial label_ ; i.e., each thread begins execution with
${\it pc}(\tau)=\iota$. Similarly, $\zeta\in\mathit{Label}$ represents the
_final label_.

We let ${\it Assertion}$ be the set of _assertions_ that use view-based
expressions. We model program annotations via an _annotation function_ , ${\it
ann}\in{\it Ann}={\it TId}\times\mathit{Label}\to{\it Assertion}$, associating
each program point $(\tau,i)$ with its associated assertion. A proof outline
is a tuple $({\it in},{\it ann},{\it fin})$, where ${\it in},{\it fin}\in{\it
Assertion}$ are the initial and final assertions.

###### Definition 0 (Validity).

A proof outline $({\it in},{\it ann},{\it fin})$ is valid for a program $\Pi$
iff each of the following holds:

Initialisation:

For all $\tau\in{\it TId}$, ${\it in}\Rightarrow{\it ann}(\tau,\iota)$.

Finalisation:

$(\forall\tau\in{\it TId}.\,{\it ann}(\tau,\zeta))\Rightarrow{\it fin}$

Local correctness:

For all $\tau\in{\it TId}$ and $i\in\mathit{Label}$, either:

  * •:

$\Pi(\tau,i)=\alpha\ {\bf goto}\ j$ and
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}{\it
ann}(\tau,i)\end{array}\right\\}}}\ \alpha\
{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}{\it
ann}(\tau,j)\end{array}\right\\}}}$; or

  * •:

$\Pi(\tau,i)=\textsf{{if}}\ B\ {\bf goto}\ j\ {\bf elseto}\ k$ and both ${\it
ann}(\tau,i)\wedge B\Rightarrow{\it ann}(\tau,j)$ and ${\it
ann}(\tau,i)\wedge\neg B\Rightarrow{\it ann}(\tau,k)$ hold.

Stability:

For all $\tau_{1},\tau_{2}\in{\it TId}$ such that $\tau_{1}\neq\tau_{2}$ and
$i_{1},i_{2}\in\mathit{Label}$ if $\Pi(\tau_{1},i_{1})=\alpha\ {\bf goto}\ j$,
then

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}{\it
ann}(\tau_{2},i_{2})\wedge{\it ann}(\tau_{1},i_{1})\end{array}\right\\}}\
\alpha\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}{\it
ann}(\tau_{2},i_{2})\end{array}\right\\}}$

Intuitively, Initialisation (resp. Finalisation) ensures that the initial
(resp. final) assertion of each thread holds at the beginning (resp. end);
Local correctness establishes validity for each thread; and Stability ensures
that each (local) thread annotation is interference-free under the execution
of other threads (Owicki and Gries, 1976).

To support Owicki-Gries reasoning, we have proved a number of high-level
rules, extending those of Dalvandi et al. (Dalvandi and Dongol, 2021; Dalvandi
et al., 2020a) to cope with transactional assertions from §5.1 and the
transactional commands. For instance, the following rules are used in the
proof of transactional message passing. A number of other rules are provided
as part of our Isabelle/HOL development.

###### Lemma 0.

Suppose $\tau{1}\neq\tau{2}$. Then each of the following holds:

$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}{\it
true}\end{array}\right\\}}\ \hbox{\pagecolor{black!8}${\tt
TxWrite}_{\tau}(x,v)$}\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{x},v)\in{\it
WS}_{\tau}\end{array}\right\\}}$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(x,u)\in{\it
WS}_{\tau{1}}\wedge{\it Rel}_{\tau{1}}\wedge{}{[}\hat{x}\not\approx
u]_{\tau{2}}\land[y=v]_{\tau{1}}\end{array}\right\\}}\
\hbox{\pagecolor{black!8}${\tt TxEnd}_{\tau{2}}$}\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}\langle\hat{x}=u\rangle[y=v]_{\tau{2}}\end{array}\right\\}}$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(x,\\_)\not\in{\it
WS}_{\tau}\wedge
Acq_{\tau}{}{}\wedge\langle\hat{x}=u\rangle[y=v]_{\tau}\end{array}\right\\}}\
\hbox{\pagecolor{black!8}${\tt TxRead}_{\tau}(x,r)$}\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{x},r)\in{\it
RS}_{\tau}\wedge{}(r=u\Rightarrow[y\stackrel{{\scriptstyle
S}}{{=}}v]_{\tau})\end{array}\right\\}}$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}(\hat{x},r)\in{\it
RS}_{\tau}\wedge(r=u\Rightarrow[y\stackrel{{\scriptstyle
S}}{{=}}v]_{\tau})\end{array}\right\\}}\ \hbox{\pagecolor{black!8}${\tt
TxEnd_{\tau}}$}\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{\begin{array}[c]{@{}l@{}}r=u\Rightarrow[y=m]_{\tau}\end{array}\right\\}}$

The rules in Lemma 4 have been verified in Isabelle/HOL w.r.t. the operational
semantics. Once proved, they can be used to show validity of proof outlines
such as those in Fig. 9 without having to consult the operational semantics.

###### Theorem 5.

The proof outline in Fig. 9 is valid.

This theorem has been verified in Isabelle/HOL, and it makes extensive use of
generic proof rules such as the ones proved in Lemma 4. In particular, given
such lemmas, like in previous works (Bila et al., 2022; Dalvandi et al., 2022;
Dalvandi and Dongol, 2021; Dalvandi et al., 2020a), Isabelle/HOL is
automatically able to find and apply the appropriate proof rule using the
built-in sledgehammer tool (Böhme and Nipkow, 2010). This automation has been
key to scaling mechanised verification of proof outlines in view-based logics.
For example, the proofs of TML-RA (see §6) requires verification of complex
invariants and proof outlines, and these proofs make use of the proof rules
developed in prior work (Dalvandi et al., 2020a). Similarly, TARO can be
applied to verify more complex porgrams that use transactions, for instance if
one were to develop transactional data structures. Interestingly, because
transactions provide isolation guarantees, many of the proofs are simplified
since the stability checks for in-flight transactions become trivial.

The proof outlines for the programs in Figs. 2 and 2 are provided in Appendix
E.

##  6\. Proving correctness of TML-ra

We now turn to the question of correctness of TML-ra with respect to the
TMS2-ra specification.

###  6.1. Refinement and Simulation for Weak Memory

Since we have an operational semantics with an interleaving semantics over
weak memory states, the development of our refinement theory closely follows
the standard approach under SC (de Roever and Engelhardt, 1998). Suppose $P$
is a program with initialisation $\mathbf{Init}$. An _execution_ of $P$ is
defined by a possibly infinite sequence
$\Delta_{0}\,\Delta_{1}\,\Delta_{2}\,\dots$ such that

  1. (1)

each $\Delta_{i}$ is a 4-tuple $(P_{i},\mathit{ls}_{i},\gamma_{i},\beta_{i})$
comprising a program to be executed, local state, global library state and
global client state, and

  2. (2)

$(P_{0},\mathit{ls}_{0},\gamma_{0},\beta_{0})=(P,\mathit{ls}_{\mathbf{Init}},\gamma_{\mathbf{Init}},\beta_{\mathbf{Init}})$,
and

  3. (3)

for each $i$, we have $\Delta_{i}\Longrightarrow\Delta_{i+1}$, where
$\Longrightarrow$ is the transition relation of the program (as defined by the
operational semantics).

Let $\mathit{LVar}_{P}$ be the set of local variables corresponding to a
program $P$. If $P$ is a client, a _client trace_ corresponding to an
execution $\Delta_{0}\,\Delta_{1}\,\Delta_{2}\dots$ is a sequence ${\it
ct}\in\Sigma_{P}^{*}$ such that ${\it
ct}_{i}=(\pi_{2}(\Delta_{i})_{|P},\pi_{4}(\Delta_{i}))$, where $\pi_{n}$ is a
projection function that extracts the $n$th component of a given tuple and
$\mathit{ls}_{|P}$ restricts the given local state $\mathit{ls}$ to the
variables in $\mathit{LVar}_{P}$. Thus, each ${\it ct}_{i}$ is the global
client state component of $\Delta_{i}$. After such a projection, the concrete
implementation may contain (finite or infinite) stuttering (de Roever and
Engelhardt, 1998), i.e., consecutive states in which the client state is
unchanged. We let ${\it rem\\_stut}({\it ct})$ be the function that removes
all stuttering from the trace ${\it ct}$, i.e., each consecutively repeating
state is replaced by a single instance of that state. We let ${\it
Tr_{SF}}(P)$ denote the set of _stutter-free traces_ of a program $P$, i.e.,
the stutter-free traces generated from the set of all executions of $P$.

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

###### Definition 0 (State and Trace Refinement).

We say a concrete client state $(\mathit{ls},\beta_{C})$ is a _refinement_ of
an abstract client state $(\mathit{als},\beta_{A})$, denoted
$(\mathit{ls},\beta_{C})\leq(\mathit{als},\beta_{A})$ iff
$\mathit{ls}=\mathit{als}$ and for all threads $\tau$ and $x\in{\it GVar}$, we
have $\beta_{C}.{\it OW}_{\tau}(x)\subseteq\beta_{A}.{\it OW}_{\tau}(x)$. We
say a concrete client trace ${\it ct}$ is a _refinement_ of an abstract client
trace ${\it at}$, denoted ${\it ct}\leq{\it at}$, iff ${\it ct}_{i}\leq{\it
at}_{i}$ for all $i$.

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

###### Definition 0 (Program Refinement).

A concrete program $P_{C}$ is a _refinement_ of an abstract program $P_{A}$,
denoted $P_{C}\leq P_{A}$, iff for any (stutter-free) client trace ${\it
ct}\in{\it Tr_{SF}}(P_{C})$ there exists a (stutter-free) client trace ${\it
at}\in{\it Tr_{SF}}(P_{A})$ such that ${\it ct}\leq{\it at}$.

Finally, we obtain a notion of contextual refinement for abstract objects. We
let $P[O]$ be the client program calling operations from object $O$. Note that
$O$ may be an abstract object, in which case execution of each method call
follows the abstract object semantics, or a concrete implementation.

###### Definition 0 (Contextual refinement).

We say a concrete object $CO$ is a _contextual refinement_ of an abstract
object $AO$ iff for any client program $P$, we have $P[CO]\leq P[AO]$.

Here, we use a _simulation-based_ proof method, which is a standard technique
from the literature that establishes refinement between TMS2-ra and TML-ra.
The difference in a relaxed memory setting is that the refinement relation is
between more complex configurations of the form $(\mathit{ls},\gamma,\beta)$,
where $\mathit{ls}$ describes the local state, $\gamma$ is the client state
and $\beta$ is a state of the TM in question. In particular, a simulation
relation, $R$, relates triples
$\Gamma_{A}\mathrel{\hat{=}}(\mathit{als},\gamma_{A},\beta_{A})$ of the
abstract system with triples
$\Gamma_{C}\mathrel{\hat{=}}(\mathit{ls},\gamma_{C},\beta_{C})$ of the
concrete system.

The definition below assumes a reflexive relation $\gamma_{C}\mathrel{\lower
1.0pt\hbox{$\mathrel{-}_{\vphantom{{}}}\mkern-8.0mu\stackrel{{\scriptstyle{\tt
tview}_{\tau}}}{{\cleaders\hbox{$\smash{\mkern-2.0mu\mathord{-}\mkern-2.0mu}$}\hfill\vphantom{\lower
1.0pt\hbox{$\rightarrow$}}_{\vphantom{{}}}}}\mkern-11.0mu\rightarrow$}}\gamma_{C}^{\prime}$
for each thread $\tau$ that arbitrarily advances the thread view of $\tau$
(for one or more locations).

###### Definition 0 (Forward simulation).

For an abstract object $AO$ and a concrete object $CO$, for a client program
$P$, we say
$R(\Gamma_{A},\Gamma_{C})\mathrel{\hat{=}}R_{V}((\mathit{als},\beta_{A}),(\mathit{ls},\beta_{C}))\wedge
R_{O}((\mathit{als}_{|AO},\gamma_{A}),(\mathit{ls}_{|CO},\gamma_{C}))$ is a
forward simulation between $A$ and $C$ iff each of the following holds:

Client observation.:

$\begin{array}[t]{@{}l}R_{V}((\mathit{als},\beta_{A}),(\mathit{ls},\beta_{C}))=\begin{array}[t]{@{}l@{}}\mathit{als}_{|P}=\mathit{ls}_{|P}\wedge(\forall\tau\in{\it
TId},x\in{\it Loc}.\ \ \beta_{A}.{\tt tview}(t,x)\leq\beta_{C}.{\tt
tview}(t,x))\end{array}\end{array}$

Thread view stability.:

For any thread $\tau$,

$\begin{array}[t]{@{}l@{}}R_{O}((\mathit{als}_{|AO},\gamma_{A}),(\mathit{ls}_{|CO},\gamma_{C}))\wedge(\gamma_{C}\mathrel{\lower
1.0pt\hbox{$\mathrel{-}_{\vphantom{{}}}\mkern-8.0mu\stackrel{{\scriptstyle{\tt
tview}_{\tau}}}{{\cleaders\hbox{$\smash{\mkern-2.0mu\mathord{-}\mkern-2.0mu}$}\hfill\vphantom{\lower
1.0pt\hbox{$\rightarrow$}}_{\vphantom{{}}}}}\mkern-11.0mu\rightarrow$}}\gamma_{C}^{\prime})\Rightarrow
R_{O}((\mathit{als}_{|AO},\gamma_{A}),(\mathit{ls}_{|CO},\gamma_{C}^{\prime}))\end{array}$

Initialisation.:

For any concrete initial state $\Gamma_{C}^{0}$, there exists an abstract
initial state $\Gamma_{A}^{0}$ such that $R(\Gamma_{A}^{0},\Gamma_{C}^{0})$.

Preservation.:

For any concrete states $\Gamma_{C}$, $\Gamma_{C}^{\prime}$ such that $C$ can
take an atomic transition from $\Gamma_{C}$ to $\Gamma_{C}^{\prime}$, if
$\Gamma_{A}$ is an abstract state such that $R(\Gamma_{A},\Gamma_{C})$, then
either

  * •:

$R(\Gamma_{A},\Gamma_{C}^{\prime})$, or (stuttering step)

  * •:

there exists a transition of $A$ from $\Gamma_{A}$ to some state
$\Gamma_{A}^{\prime}$ such that $R(\Gamma_{A}^{\prime},\Gamma_{C}^{\prime})$.
(non-stuttering step)

Initialisation and preservation are standard components of a forward
simulation. Client observation is necessary in a relaxed memory context to
ensure that the client-side observations of the concrete system are possible
observations of the abstract system. In particular, if an abstract object
specifies a particular client-side synchronisation, then this synchronisation
must also be present in the concrete implementation (see (Dalvandi and Dongol,
2021)). Thread view stability guarantees that the $R_{O}$ component of the
refinement relation is preserved when the thread view in the library is
shifted forward, e.g., due to synchronisation within a client.

Note that Definition 4 only guarantees preservation of safety. To additionally
preserve liveness, further progress guarantees are required in an
implementation (Gotsman and Yang, 2011; Dongol and Groves, 2016). We leave
liveness preservation through refinement for future work since notions of
fairness and progress of weak memory models is still at the early stages
(Lahav et al., 2021).

###### Theorem 5.

If $R$ is a forward simulation between $AO$ and $CO$, then for any client $P$
we have $P[CO]\leq P[AO]$.

###  6.2. Forward Simulation for TML-ra

Perhaps the most technically challenging aspect of this paper is the proof of
Theorem 6 below, which ensures the correctness of TML-ra w.r.t. TMS2-ra.

This section describes the simulation relation used to prove refinement
between TML-ra and TMS2-RA. Validity of the forward simulation itself has been
verified using Isabelle/HOL. The refinement relation

$R((\mathit{als},\gamma_{A},\beta_{A}),(ls,\gamma_{C},\beta_{C}))\ \
\mathrel{\hat{=}}\ \
\begin{array}[t]{@{}l@{}}R_{V}((\mathit{als},\beta_{A}),(\mathit{ls},\beta_{C}))\wedge(\ref{eq:rr0})\wedge{}\\\
(\forall t.\
(\ref{rr1})\land(\ref{rr2})\land(\ref{rr4})\land(\ref{rr5})\land(\ref{rr6})\land(\ref{rr7})\land(\ref{rr8})\land(\ref{rr9}))\end{array}$

The first conjunct (1) in the refinement relation $R$ states that the value of
the last write to ${\it glb}$ divided by 2
($\mathtt{wc}(n)\mathrel{\hat{=}}n\div 2$) is equal to the last version of
history written to $\mathit{M}$.

(1) $\mathtt{wc}(\gamma_{C}.\mathtt{lastval}(glb))=|\gamma_{A}.\mathit{M}|$

The next conjunct, (2), states that the last value written to any location $l$
in $\gamma_{C}$ is either the value of $l$ in the last abstract memory index
or in the write set of the executing transaction

(2) $\begin{split}&\forall l.~{}l\neq{\it
glb}\Rightarrow\begin{array}[t]{@{}l@{}}\gamma_{C}.\mathtt{lastval}(l)\in\\{\gamma_{A}.\mathit{M}_{|\gamma_{A}.\mathit{M}|}(l),\gamma_{A}.\mathtt{wrSet}_{t}(l)\\}\end{array}\end{split}$

where $\mathtt{lastval}(x)$ is a function that returns the value of the last
write written to a location $x$.

The next conjunct (3) is an on-the-fly simulation relation (i.e. the
transaction has begun and is not committed or aborted) and states that for all
threads $\tau$ if transaction $t$ ($\gamma_{A}.\mathtt{txn}_{\tau}=t$) is on-
the-fly, the value of $\mathtt{wc}(\gamma_{C}.loc_{\tau})$ will be greater
than or equal to $\mathtt{beginIdx}_{t}$ and the read set of $t$ will be
consistent with memory verison $\mathtt{wc}(\gamma_{C}.loc_{\tau})$:

(3)
$\begin{split}\gamma_{A}.\mathtt{beginIdx}_{t}\leq\mathtt{wc}(ls.loc_{t})\land\gamma_{A}.\mathtt{rdSet}_{t}\subseteq\gamma_{A}.\mathit{M}_{\mathtt{wc}(ls.loc_{t})}\end{split}$

Conjunct (4) states that if the value of $ls.loc_{t}$ is even then write set
of $\gamma_{A}$ must be empty:

(4)
$\begin{split}\mathtt{even}(ls.loc_{t})\Rightarrow\gamma_{A}.\mathtt{wrSet}_{t}=\emptyset\end{split}$

Also if a transaction $t$ that has already written to a location then the
write set of $\gamma_{A}$ is not empty:

(5)
$\begin{split}ls.\mathtt{hasWritten}_{t}\Rightarrow\gamma_{A}.\mathtt{wrSet}_{t}\neq\emptyset\end{split}$

If a transaction has not read any location yet in the concrete state, then the
read set of the abstract state should be empty:

(6) $\begin{split}\neg
ls.\mathtt{hasRead}_{t}\Rightarrow\gamma_{A}.\mathtt{rdSet}_{t}=\emptyset\end{split}$

If there is a write in the write set of the abstract state, then the value
should match the value of the last write written to that location by the
concrete implementation:

(7) $\begin{split}\forall
l\in\operatorname{\mathbf{dom}}(\gamma_{A}.\mathtt{wrSet}_{t}).\ \
\gamma_{A}.\mathtt{wrSet}_{t}(l)=\gamma_{C}.\mathtt{lastval}(l)\end{split}$

The value of a visible write of thread $\tau$ to variable $glb$ divided by two
is a visible memory by thread $\tau$ of the abstract state:

(8) $\begin{split}\forall w\in\gamma_{C}.OW_{\tau}(glb).\ \
\mathtt{wc}(\mathtt{val}(w))\in\gamma_{A}.vmems_{\tau}\end{split}$

All seen memory indices by the abstract transaction $t$ are less the value of
thread view of $glb$ for thread $\tau$ divided by 2:

(9) $\begin{split}\forall i\in\gamma_{A}.\mathtt{seenIdxs}_{t}.\ \
i\leq\mathtt{wc}(\mathtt{val}(\gamma_{C}.{\tt tview}_{\tau}(glb)))\end{split}$

###### Theorem 6.

$R$ is a forward simulation between TMS2-ra and TML-ra.

###### Proof.

This theorem has been verified in Isabelle/HOL. ∎

##  7\. Related work

##### Verifying C11 programs.

There are now several different approaches to program verification that
support different aspects of the C11 relaxed memory model using pen-and-paper
proofs (e.g., (Lahav and Vafeiadis, 2015; Turon et al., 2014; Alglave and
Cousot, 2017; Doko and Vafeiadis, 2017)), model checking (e.g.,
(Kokologiannakis et al., 2019; Abdulla et al., 2019)), specialised tools
(e.g., (Tassarotti et al., 2015; Krishna et al., 2020; Svendsen et al., 2018;
Summers and Müller, 2018)), and generalist theorem provers (e.g., (Dalvandi et
al., 2020a)). These cover a variety of (fragments of) memory models and
proceed via exhaustive state space exploration, separation logics, or Hoare-
style calculi. A related approach to TARO that uses a view-based semantics for
persistent x86-TSO has been developed by Bila et al. (2022).

Another series of works has focussed on semantics that support the relaxed
dependencies that are allowed by C11 (Paviotti et al., 2020; Kang et al.,
2017; Lee et al., 2020; Jagadeesan et al., 2020). These have been followed
more recently by logics and verification over this semantics (Wright et al.,
2021; Svendsen et al., 2018). However, relaxed dependencies produce high
levels of non-determinism, making verification significantly more complex. We
consider a verification framework that supports relaxed dependencies and STMs
to be a topic for future research.

More recent works include robustness of C11-style programs, which aims to show
“adequate synchronisation” so that the relaxed memory executions reduce to
executions under stronger memory models (Margalit and Lahav, 2021). Such
reductions, although automatic, are limited to finite state systems, and a
small number of threads. Furthermore, it is currently unclear how they would
handle client-library synchronisation or relaxed (non-SC) specifications.

##### Correctness conditions under relaxed memory.

Following the extensive literature on the semantics of relaxed memory
architectures, a natural next question has been the development of library
abstractions for relaxed memory. One aim has been to ensure observational
refinement and compositionality of the implemented objects. A series of works
have considered reforumulations of linearizability (Dongol et al., 2018b;
Doherty et al., 2018; Raad et al., 2019a) by presenting suitable weakenings
fine-tuned to the underlying memory model. This includes extensions of
linearizability, e.g., so that it is defined in terms of axiomatic (aka
declarative) relaxed memory models (Dongol et al., 2018b; Raad et al., 2019a)
and those that are based on the more abstract concept of execution structures
(Doherty et al., 2018). Recent works have covered verification of relaxed
memory concurrent data structures that have been developed to satisfy the
conditions described above (Krishna et al., 2020; Raad et al., 2019a; Dalvandi
and Dongol, 2021), but none of these cover transactions.

Khyzha and Lahav (2022) have recently developed notions of abstraction for
crash resilient libraries, providing correctness conditions (extending
linearizability) that ensure contextual refinement for concurrent objects
executed over the PSC (persistent sequential consistency) model. They do so by
exposing the internal synchronisation mechanisms that are used to implement an
object in the history (in addition to the invocations and responses). Our work
differs since we consider transactional memory libraries as opposed to
concurrent objects, use a different memory model and focus on verification of
contextual refinement directly. Nevertheless, in future work, it would be
interesting to see if their methods provide an alternative method for
specifying concurrent object and transactional memory libraries in C11.

Several papers have revisited transaction semantics in the context of relaxed
memory models (Raad et al., 2019b; Dongol et al., 2019, 2018a; Chong et al.,
2018). Raad et al have considered relaxed memory and _snapshot isolation_
(Raad et al., 2018, 2019b), which is a weaker condition that serializability
(and hence opacity and TMS2). The question of whether snapshot isolation can
be fully exploited by implementations in a relaxed memory setting remains a
topic of future research, with most transactional implementations aiming to
support at least serializability (Zardoshti et al., 2019). Dongol et al.
(2018a) and Chong et al. (2018) have provided axiomatic atransactional
semantics integrated with relaxed memory models, focussing on hardware memory
models and hardware transactions. Chong et al. (2018) additionally propose a
model for C11 transactions, but these models are focussed on transactions
within the compiler, as opposed to STMs. Finally, the axiomatic models
proposed in these earlier works (Dongol et al., 2018a; Chong et al., 2018) are
not suitable for operational verification, e.g., as supported by TARO, where
we require an operational semantics as provided by TMS2-ra.

Another set of works has focussed on distributed (relaxed) transactions (Xiong
et al., 2020; Beillahi et al., 2021a, b). Although there are analogues between
transactions in distributed systems and relaxed memory, constraints such as
replication consistency and session order are not factors in shared memory,
and hence the underlying issues are fundamentally different. Xiong et al.
(2020) describe a taxonomy of distributed transactional models supported by an
operational semantics. It would be interesting to investigate whether TARO can
be adapted to cope with client-object systems in their models.

##### Relaxed memory TM implementations.

There is a set of recent works on implementing TM algorithms in C11 (Spear et
al., 2020; Zardoshti et al., 2019). The focus here has been real-world
implementability of STMs via compiler support. Since the focus is on
benchmarks and real-world workflows, these works neither consider a formal
semantics nor provide a verification framework. Our work can thus be seen as
providing a formal basis to support to these efforts. In particular, we show
how the serialisability specifications assumed by Spear et al. (2020);
Zardoshti et al. (2019) can be relaxed, without impacting correctness, while
improving performance.

##  8\. Conclusions

In this paper, we have presented a new approach to release-acquire
transactions for RC11 RAR (a fragment of C11 that supports relaxed as well as
release-acquire atomics). We have developed a new TM specification, TMS2-ra,
that extends TMS2 to a relaxed memory context by describing the interactions
between transactions and their clients. We implement TMS2-ra by TML-ra, which
is an adaptation of an existing eager algorithm, TML. We show that TML-ra
outperforms TML-sc using the STAMP benchmarks.

Our second set of contributions covers the verification of release-acquire TM
implementations. We focus on proofs at two levels:  (i) correctness of client
programs that use TMS2-ra, and  (ii) correctness of implementations of
TMS2-ra.  For (i), we have developed a logic, TARO, extending (Dalvandi and
Dongol, 2021), and used this logic to prove that TMS2-ra does indeed guarantee
the desired client-side synchronisation properties. For (ii), we have applied
a simulation method, simular to (Dalvandi and Dongol, 2021) and proved a
forward simulation between TML-ra and TMS2-ra. All proofs for (i) and (ii) as
well as all meta-level soundness results are fully mechanised in the
Isabelle/HOL proof assistant, providing a high level of assurance to our
results.

Our motivation for using TML as the main implementation case study was to
start with a simple algorithm with an existing proof in SC (Derrick et al.,
2018). TML performs a global synchronisation through a CAS on a single
location, which degrades performance on write-heavy workloads. For improved
scalability, there are more sophisticated algorithms like TL2 (Dice et al.,
2006) that offer per-location locking as well as hybrid TM implementations
(Matveev and Shavit, 2015) that combine hardware and software TM. TMS2 is
known to be a sufficient abstraction for hybrid TMs in SC (Armstrong and
Dongol, 2017), so it is likely that TMS2-ra also provides a basis for