University of California at Berkeley<EMAIL_ADDRESS>IIT Bombay, India
<EMAIL_ADDRESS>Institute of Theoretical Computer Science,
Braunschweig, Germany<EMAIL_ADDRESS>Adwait Godbole, S. Krishna, Roland
Meyer [500]Concurrency, Verification

# Safety Verification of Parameterized Systems under Release-Acquire

Adwait Godbole 111This work was done when Adwait Godbole was a final year
undergraduate student at IIT Bombay Shankara Narayanan Krishna  Roland Meyer

###### Abstract

We study the safety verification problem for parameterized systems under the
release-acquire (RA) semantics. It has been shown that the problem is
intractable for systems with unlimited access to atomic compare-and-swap (CAS)
instructions. We show that, from a verification perspective where approximate
results help, this is overly pessimistic. We study parameterized systems
consisting of an unbounded number of environment threads executing identical
but CAS-free programs and a fixed number of distinguished threads that are
unrestricted.

Our first contribution is a new semantics that considerably simplifies RA but
is still equivalent for the above systems as far as safety verification is
concerned. We apply this (general) result to two subclasses of our model. We
show that safety verification is only $\mathsf{PSPACE}$-complete for the
bounded model checking problem where the distinguished threads are loop-free.
Interestingly, we can still afford the unbounded environment. We show that the
complexity jumps to $\mathsf{NEXPTIME}$-complete for thread-modular
verification where an unrestricted distinguished ‘ego’ thread interacts with
an environment of CAS-free threads plus loop-free distinguished threads (as in
the earlier setting). Besides the usefulness for verification, the results are
strong in that they delineate the tractability border for an established
semantics.

###### keywords:

release acquire, parameterized systems

###### category:

##  1 Introduction

Release-acquire (RA) is a popular fragment of C++11 [14] (in which reads are
annotated by acquire and writes by release) that strikes a good balance
between programmability and performance and has received considerable
attention (see e.g., [47, 49, 60, 51, 8, 53, 64, 63, 41]). The model is not
limited to concurrent programs, though. RA has tight links [52] with causal
consistency (CC) [7], a prominent consistency guarantee in distributed
databases [55]. Common to RA implementations and distributed databases is that
they tend to offer functionality to multi-threaded client programs, be it
means of synchronization or access to shared data.

We are interested in verifying such implementations on top of RA. For
verification, we can abstract the client program to invocations of the offered
functionality [20]. The result is a so-called instance of the implementation
in which concurrent threads execute the code of interest. There is a subtlety.
As the RA implementation should be correct for every client, we cannot fix the
instance to be verified. We have to prove correctness irrespective of the
number of threads executing the code. This is the classical formulation of a
parameterized system as it has been studied over the last 35 years [20].

We are interested in the decidability and complexity of safety verification
for parameterized programs under RA. The goal is to identify expressive
classes of programs for which the problem is tractable. There are good
arguments in favor of this agenda. From a pragmatic point of view, even if the
implementation at hand does not fall into one of the classes identified, we
may hope for a reasonably precise encoding. From a conceptual point of view,
tractability of verification is linked to programmability, and understanding
the complexity may lead to suggestions for better consistency notions [50] or
programming guidelines, e.g. in the form of type systems [56]. Safety
verification is a good fit for linearizability [43], the de-facto standard
correctness conditions for concurrency libraries, and has to be settled before
going to more complicated notions.

To explain the challenges of parameterized verification under RA, it will be
helpful to have an understanding of how to program under RA. The slogan of RA
is _never read “overwritten” values_ [52]. Assume we have shared variables g
and d, initially $0$, and a thread first stores $1$ to d and then $1$ to g.
Assume a second thread reads the $1$ from g. Under RA, that thread can no
longer claim $\texttt{d}=0$. Formulated axiomatically [9], the reads-from,
modification order, program order, and from-read should be acyclic [52]. While
less concise, there are operational formulations of RA that make explicit,
information about the computation which will be useful for our development
[59, 48, 47]. The mechanism is as follows. Program and modification order are
encoded as natural numbers, called _timestamps_. Each thread stores locally a
_view_ object, a map from shared variables to timestamps. This map reflects
the thread’s progress in terms of seeing (or as above hearing from) stores to
a shared variable. The communication is organized in a way that achieves the
desired acyclicity. Store instructions generate _messages_ that decorate the
variable-value pair by a view. This view is the one held by the thread except
that the timestamp of the variable being written is raised to a strictly
higher value. The shared memory is implemented as a pool to which the
generated messages are added and in which they remain forever. When loading a
message from the pool, the timestamp of the variable given by the message must
be at least the timestamp in the thread. The views are then joined so that the
receiver cannot load values older than what the sender has seen.

The timestamps render the RA semantics infinite-state, which makes algorithmic
verification difficult. Indeed, the problem of solving safety verification
under RA in a complete way has been studied very recently in the non-
parameterized setting and proven to be undecidable even for programs with
finite control flow and finite data domains [1]. With this insight, [1]
proposes to give up completeness and show how to encode an under-approximation
of the safety verification problem into sequential consistency [54]. Lahav and
Boker [50] drew a different conclusion. They proposed strong release-acquire
(SRA) as a new consistency guarantee under which safety verification is
decidable for general non-parameterized programs. Unfortunately, the lower
bound is again non-primitive recursive. Also the related problem of checking
CC itself for a given implementation has been studied. It is undecidable in
general, but EXPSPACE-complete under the assumption of data independence [22].

To sum up, despite recent efforts [22, 1, 50] we are missing an expressive
class of programs for which the safety verification problem under RA is
tractable. The parameterized verification problem has not been studied.

Problem Statement. The parameterized systems of interest have the form
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}\parallel\dots\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{n}$.
We have a fixed number of distinguished threads collectively referred to as
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
and executing programs
$\mathsf{c}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}}^{1},\cdots\mathsf{c}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}}^{n}$,
respectively. Moreover, we have an environment consisting of arbitrarily many
threads executing the same program
$\mathsf{c}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$.
We obtain an _instance_ of the system by also fixing the number of number of
environment threads. The safety verification problem is as follows:

> _Safety Verification for Parameterized Systems_ :
> Given a parameterized system
> ${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}\parallel\dots\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{n}$,
> is there an instance of the system and a computation in that instance that
> reaches an assertion violation?

The complexity of the problem depends on the system class under consideration.
We denote system classes by signatures of the form
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{type}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}(\mathsf{type}_{1})\parallel\dots\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{n}(\mathsf{type}_{n})$,
where the types constrain the programs executed by the threads. The parameters
are the structure of the control flow, which may be loop-free, denoted by
$\mathsf{acyc}$, and the instruction set, which may forbid the atomic compare-
and-swap (CAS) command, denoted by $\mathsf{nocas}$. We drop the type if no
restriction applies. If a thread is not present, we do not mention it in the
signature. With this,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}(\mathsf{acyc})\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{2}(\mathsf{nocas})\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{3}$
is a non-parameterized system (without
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads) having three
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads executing: a loop-free
$\mathsf{c}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}}^{1}$,
$\mathsf{c}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}}^{2}$
which does not have CAS instructions, and
$\mathsf{c}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}}^{3}$
which is free of restrictions, respectively.

Justifying the Parameters. In [1], the safety verification problem under RA
has been shown to be undecidable for non-parameterized
(${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$-free)
systems from
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}(\mathsf{nocas})\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{2}(\mathsf{nocas})\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{3}\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{4}$
and non-primitive-recursive for systems from
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}(\mathsf{nocas})\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{2}(\mathsf{nocas})$.
There are several conclusions to draw from this.

With distinguished threads, we cannot hope to arrive at a tractable
verification problem. We take the bounded model checking [28] approach and
consider loop-free code. Acyclic programs, however, are not very expressive.
Fortunately, RA implementations tend to be parameterized, and, as we will see,
this frees us from the acyclicity restriction. The fact that parameterization
simplifies verification has been observed in various works [46, 39, 62, 33, 5]
that we discuss below.

Restricting the use of CAS requires an explanation. The class
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
of unconstrained environment threads enables what we call leader isolation: an
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread can distinguish itself from the others by acquiring a CAS-based lock.
Even just $t$ CAS operations allows for the isolation of $t$ distinguished
threads, which takes us back to the results of [1] for $t=2$ resp. $t=4$.
Acyclicity will not help in this case, in section 3 we show that safety
verification for
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{acyc})$
is undecidable.

Contributions. We state our main results and present the technical details in
the later parts.

A Simplified Semantics. We consider parameterized systems of the form
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{nocas})\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}\parallel\dots\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{n}$.
Our first contribution is a simplified semantics (Section 4) that is
equivalent with the standard RA semantics as far as safety verification is
concerned. The simplified semantics uses the notion of timestamp abstraction,
which allows us to be imprecise about the exact timestamps of the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads. Note that we do not make any assumptions on the form of the
distinguished threads but support cyclic control flow and CAS. So the result
in particular applies to the intractable classes from [1], even when extended
with a parameterized environment. Supporting CAS in the distinguished threads
is important. Without it, there is no way to capture the optimistic
synchronization strategies used in performance critical programming [42].

We continue to apply the simplified semantics to prove tight complexity bounds
for the safety verification problem in two particular cases of
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
programs.

Loop-Free Setting. In Section 5, we show a $\mathsf{PSPACE}$-upper bound for
the safety verification problem of parameterized programs from
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{nocas})\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}(\mathsf{acyc})\parallel\cdots\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{n}(\mathsf{acyc})$.
The class reflects the bounded model checking problem [28], which unrolls a
given program into a loop-free under-approximation. Interestingly, we can
sequeeze into $\mathsf{PSPACE}$ the unbounded environment of cyclic threads.
Our decision procedure is not only optimal complexity-wise, it also has the
potential of being practical (we do not have experiments). We show how to
encode the safety verification problem into the query evaluation problem for
linear Datalog, the format supported by Horn-clause solvers [18, 17], a state-
of-the-art backend in verification.

Leader Setting. We continue to show an $\mathsf{NEXPTIME}$-upper bound for
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{nocas})\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}(\mathsf{acyc})\parallel\cdots\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{n}(\mathsf{acyc})\parallel{\color[rgb]{0.0,0.42,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.42,0.24}\mathsf{ldr}}$
in Section 6. These systems add an unconstrained distinguished thread, called
the leader (denoted
${\color[rgb]{0.0,0.42,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.42,0.24}\mathsf{ldr}}$),
to the system from Section 5. The class is in the spirit of thread-modular
verification techniques [57, 35], where the safety of a single ‘ego’ thread is
verified when interacting with an environment.

We note that these results delineate the border of tractability: adding
another
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
thread results in a non-primitive-recursive lower bound [1], and adding CAS
operations to
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
results in undecidability (section 3).

Lower Bounds. Our last contributions are matching lower bounds for the two
classes. Interestingly, they hold even in the absence of CAS. We show that the
safety verification problem is $\mathsf{PSPACE}$-hard already for
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{nocas},\mathsf{acyc})$,
while it is $\mathsf{NEXPTIME}$-hard for
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{nocas},\mathsf{acyc})\parallel{\color[rgb]{0.0,0.42,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.42,0.24}\mathsf{ldr}}(\mathsf{nocas})$.

Related Work. There is a vast body of work on algorithmic verification under
consistency models. Since our interest is in decidability and complexity, we
focus on complete methods. We have already discussed the related work on RA
and CC.
_Other Consistency models._ Atig et al. have shown that safety verification is
decidable for assembly programs running on TSO, the consistency model of x86
architectures [11]. The result has been generalized to consistency models with
non-speculative writes [12] and very recently to models with persistence [3].
It has also been generalized to parameterized programs executed by an
unbounded number of threads [4]. Behind the decision procedures are (often
drastic) reformulations of the semantics combined with well-structuredness
arguments [6]. A notable exception is [5], showing that safety verification
under TSO can be solved in $\mathsf{PSPACE}$ for cas-free parameterized
programs, called
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{nocas})$
here. On the widely-used Power architecture safety is undecidable [2].

The decidability and complexity of verification problems has been studied also
for distributed databases and data structures. Enea et al. considered the
problem of checking eventual consistency (EC) [66] of replicated databases and
developed a surprising link to vector addition systems [23] that yields
decidability and complexity results for the safety and liveness aspects of EC.
For concurrent data structures, the default correctness criterion is
linearizability wrt. a specification [43]. While checking linearizability is
$\mathsf{EXPSpace}$-complete in general [10, 40], important data structures
(for which the specification is then fixed) admit $\mathsf{PSPACE}$-algorithms
[21].
_Parameterized Systems with Asynchronous Communication_. We exploit a pleasant
interplay between the asynchronous communication in RA and the
parameterization of our systems in the number of threads. Kahlon [46] was the
first to observe that parameterization simplifies verification in the case of
concurrent pushdowns. Hague [39] showed that safety verification remains
decidable when adding a distinguished leader thread. Esparza, Ganty, Majumdar
studied the complexity of what is now called leader-contributor systems [33].
It is surprisingly low, $\mathsf{NP}$-complete for systems of finite-state
components and $\mathsf{PSPACE}$-completeness for systems of pushdowns. At the
heart of their technique is the so-called copycat-lemma. The work has been
generalized [62] to all classes of models that are closed under regular
intersection and have a computable downward-closure. It has also been
generalized to liveness verification [31, 36]. Finally, the study has been
generalized to parameterized complexity, for safety [27] and liveness [25].
Our work is related in that the distinguished threads behave like a leader.
Moreover, our simplified semantics relies on an infinite-supply property the
proof of which gives a copycat variant for RA. Our Datalog encoding is
reminiscent of the notion of Strahler number [34].

Leader-contributor systems are closely related to broadcast networks [32, 61].
Also there, safety verification has been found to be suprisingly cheap, namely
$\mathsf{PTIME}$-complete [30]. For liveness verification, there was a gap
between $\mathsf{EXPSpace}$ and $\mathsf{PTIME}$ that was settled recently
with a non-trivial polynomial-time algorithm [26]. What is new in broadcast
networks and neither occurs in leader-contributor systems nor in our setting
is the problem of reconfiguration [29, 13, 16].

##  2 The Release-Acquire Semantics

A parameterized system consists of an unknown and potentially large number of
threads, all running the same program. Threads compute locally over a set of
registers and interact with each other by writing to and reading from a shared
memory. The interaction with the shared memory is under the Release Acquire
(RA) semantics [52, 59, 48].

$\begin{array}[]{c}\begin{array}[]{cccc}\inferrule{(\mathsf{c}_{1},\mathsf{rv},\mathsf{vw})\xrightharpoondown{\mathsf{msg}}(\mathsf{c}_{1}^{\prime},\mathsf{rv}^{\prime},\mathsf{vw}^{\prime})}{(\mathsf{c}_{1};\mathsf{c}_{2},\mathsf{rv},\mathsf{vw})\xrightharpoondown{\mathsf{msg}}(\mathsf{c}_{1}^{\prime};\mathsf{c}_{2},\mathsf{rv}^{\prime},\mathsf{vw}^{\prime})}&\inferrule{i=1,2}{(\mathsf{c}_{1}\oplus\mathsf{c}_{2},\mathsf{rv},\mathsf{vw})\xrightharpoondown{}(\mathsf{c}_{i},\mathsf{rv},\mathsf{vw})}&\inferrule{\leavevmode\nobreak\
}{(\mathsf{skip};\mathsf{c},\mathsf{rv},\mathsf{vw})\xrightharpoondown{}(\mathsf{c},\mathsf{rv},\mathsf{vw})}&\inferrule{\leavevmode\nobreak\
}{(\mathsf{assert}\;{\texttt{false}},\mathsf{rv},\mathsf{vw})\xrightharpoondown{}\bot}\end{array}\\\\[14.22636pt]
\begin{array}[]{ccc}\inferrule{\leavevmode\nobreak\
}{(\mathsf{c}^{*},\mathsf{rv},\mathsf{vw})\xrightharpoondown{}(\mathsf{skip}\oplus\mathsf{c};\mathsf{c}^{*},\mathsf{rv},\mathsf{vw})}&\inferrule{[\\![\mathsf{e}]\\!](\mathsf{rv}(\overline{\mathsf{r}}))=\mathsf{d}\quad\mathsf{rv}^{\prime}=\mathsf{rv}[\mathsf{r}\mapsto
\mathsf{d}]}{(\mathsf{r}
\coloneqq\mathsf{e}(\overline{\mathsf{r}}),\mathsf{rv},\mathsf{vw})\xrightharpoondown{}(\mathsf{skip},\mathsf{rv}^{\prime},\mathsf{vw})}&\inferrule{[\\![\mathsf{e}]\\!](\mathsf{rv}(\overline{\mathsf{r}}))\neq
0}{(\mathsf{assume}\;{\mathsf{e}(\overline{\mathsf{r}})},\mathsf{rv},\mathsf{vw})\xrightharpoondown{}(\mathsf{skip},\mathsf{rv},\mathsf{vw})}\end{array}\\\\[14.22636pt]
\begin{array}[]{cc}\textsc{(ST-
local)}\quad\inferrule{\mathsf{rv}(\mathsf{r})=\mathsf{d}\quad\mathsf{vw}<_{\mathsf{x}}\mathsf{vw}^{\prime}}{(\mathsf{x}
\coloneqq\mathsf{r},\mathsf{rv},\mathsf{vw})\xrightharpoondown{\mathsf{st},(\mathsf{x},\mathsf{d},\mathsf{vw}^{\prime})}(\mathsf{skip},\mathsf{rv},\mathsf{vw}^{\prime})}&\hskip
14.22636pt\textsc{(LD-
local)}\quad\inferrule{\mathsf{vw}(\mathsf{x})\leq\mathsf{vw}^{\prime}(\mathsf{x})\quad\mathsf{rv}^{\prime}=\mathsf{rv}[\mathsf{r}\mapsto
\mathsf{d}]}{(\mathsf{r}
\coloneqq\mathsf{x},\mathsf{rv},\mathsf{vw})\xrightharpoondown{\mathsf{ld},(\mathsf{x},\mathsf{d},\mathsf{vw}^{\prime})}(\mathsf{skip},\mathsf{rv}^{\prime},\mathsf{vw}\sqcup\mathsf{vw}^{\prime})}\end{array}\\\\[14.22636pt]
\small{\textsc{(CAS-
local)}\quad\inferrule{\mathsf{rv}(\mathsf{r}_{1})=\mathsf{d}_{1}\quad
\mathsf{rv}(\mathsf{r}_{2})=\mathsf{d}_{2}\quad\mathsf{vw}(\mathsf{x})\leq\mathsf{vw}^{\prime}(\mathsf{x})=\mathsf{ts}\\\
\widetilde{\mathsf{vw}}=\mathsf{vw}^{\prime}[\mathsf{x}\mapsto\mathsf{ts}+1]\quad\mathsf{vw}^{\prime\prime}=\mathsf{vw}\sqcup\widetilde{\mathsf{vw}}}{(\mathsf{cas}(\mathsf{x},\mathsf{r}_{1},\mathsf{r}_{2}),\mathsf{rv},\mathsf{vw})\xrightharpoondown{\mathsf{ld},(\mathsf{x},\mathsf{d}_{1},\mathsf{vw}^{\prime})}\xrightharpoondown{\mathsf{st},(\mathsf{x},\mathsf{d}_{2},\mathsf{vw}^{\prime\prime})}(\mathsf{skip},\mathsf{rv},\mathsf{vw}^{\prime\prime})}}\\\\[14.22636pt]
\hline\cr\begin{array}[]{cc}\textsc{(LD-global)}\leavevmode\nobreak\
\leavevmode\nobreak\
\inferrule{\mathsf{lcfm}(\mathsf{t})=\mathsf{lcf}\quad\mathsf{lcf}\xrightharpoondown{\mathsf{ld},\mathsf{msg}}\mathsf{lcf}^{\prime}\quad\mathsf{msg}\in\mathsf{m}}{(\mathsf{m},\mathsf{lcfm})\xrightarrow{(\mathsf{t},\mathsf{msg})}(\mathsf{m},\mathsf{lcfm}[\mathsf{t}\mapsto\mathsf{lcf}^{\prime}])}&\hskip
14.22636pt\textsc{(ST-global)}\leavevmode\nobreak\ \leavevmode\nobreak\
\inferrule{\mathsf{lcfm}(\mathsf{t})=\mathsf{lcf}\quad\mathsf{lcf}\xrightharpoondown{\mathsf{st},\mathsf{msg}}\mathsf{lcf}^{\prime}\quad\mathsf{msg}\;\\#\;\mathsf{m}}{(\mathsf{m},\mathsf{lcfm})\xrightarrow{(\mathsf{t},\mathsf{msg})}(\mathsf{m}\cup\\{\mathsf{msg}\\},\mathsf{lcfm}[\mathsf{t}\mapsto\mathsf{lcf}^{\prime}])}\end{array}\\\
\begin{array}[]{cc}\textsc{(CAS-global)}\leavevmode\nobreak\
\inferrule{\mathsf{lcfm}(\mathsf{t})=\mathsf{lcf}\quad\mathsf{lcf}\xrightharpoondown{\mathsf{ld},\mathsf{msg}_{l}}\xrightharpoondown{\mathsf{st},\mathsf{msg}_{s}}\mathsf{lcf}^{\prime}\quad\mathsf{msg}_{l}\in\mathsf{m}\quad\mathsf{msg}_{s}\;\\#\;\mathsf{m}}{(\mathsf{m},\mathsf{lcfm})\xrightarrow{(\mathsf{t},\mathsf{msg})}(\mathsf{m}\cup\\{\mathsf{msg}_{s}\\},\mathsf{lcfm}[\mathsf{t}\mapsto\mathsf{lcf}^{\prime}])}&\hskip
14.22636pt\textsc{(Unlabelled)}\leavevmode\nobreak\
\inferrule{\mathsf{lcfm}(\mathsf{t})=\mathsf{lcf}\quad\mathsf{lcf}\xrightharpoondown{}\mathsf{lcf}^{\prime}}{(\mathsf{m},\mathsf{lcfm})\xrightarrow{\mathsf{t}}(\mathsf{m},\mathsf{lcfm}[\mathsf{t}\mapsto\mathsf{lcf}^{\prime}])}\end{array}\end{array}$

Figure 1: Local transition relation: silent (thread-local) transitions (pink),
shared memory transitions (blue). Global transition relation (below in green)

###  2.1 Program Syntax

We model the individual threads in our system as (non-deterministic)
sequential programs. Assume a standard while-language $\mathsf{Com}$ defined
by:

$\displaystyle\mathsf{c}\;::=$
$\displaystyle\quad\mathsf{skip}\;\mid\;\mathsf{assume}\;{\mathsf{e}(\overline{\mathsf{r}})}\;\mid\;\mathsf{assert}\;{\texttt{false}}\;\mid\;\mathsf{r}
\coloneqq\mathsf{e}(\overline{\mathsf{r}})\;\mid\;\mathsf{c};\mathsf{c}\;\mid\;\mathsf{c}\oplus\mathsf{c}\;\mid\;\mathsf{c}^{*}\;\mid\;$
$\displaystyle\quad\mathsf{r} \coloneqq\mathsf{x}\;\mid\;\mathsf{x}
\coloneqq\mathsf{r}\;\mid\;\mathsf{cas}(\mathsf{x},\mathsf{r}_{1},\mathsf{r}_{2})$

The programs compute on (thread-local) registers $\mathsf{r}$ from the finite
set $\mathsf{Reg}$ using assume, assert, assignments, sequential composition,
non-deterministic choice, and iteration. Conditionals $\mathsf{if}$ and
iteratives $\mathsf{while}$ can be derived from these operators, and we use
them where convenient. The shared memory variables $\mathsf{x}$ are accessed
only by means of load, store and compare-and-swap (CAS) operations as
$\mathsf{r} \coloneqq\mathsf{x}$, $\mathsf{x} \coloneqq\mathsf{r}$ and
$\mathsf{cas}(\mathsf{x},\mathsf{r}_{1},\mathsf{r}_{2})$, respectively. These
instructions are also referred to as _events_. We have a finite set
$\mathsf{Var}$ of shared variables, and work with the data domain
$\mathsf{Dom}={\rm Nature}$. We do not insist on a shape of expressions
$\mathsf{e}$ but require an interpretation
$[\\![\mathsf{e}]\\!]:\mathsf{Dom}^{n}\rightarrow\mathsf{Dom}$ that respects
the arity $n$ of the expression.

###  2.2 Release-Acquire (RA) Semantics

We give the semantics of parameterized systems under release-acquire
consistency. We opted for an operational [59, 48] over an axiomatic [52]
definition, and follow [1]. What makes the operational definition attractive
is that it comes with a notion of configuration or state of the system that we
use to reason about computations. We first define thread-local configurations,
then add the shared memory, and give the global transition relation.

Local Configurations. The RA semantics enforces a total order on all stores to
the same variable that have been performed in the computation. We model these
total orders by
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{Time}}={\rm
Nature}$ and refer to elements of
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{Time}}$
as timestamps. Using the total orders, each thread keeps track of its progress
in the computation. It maintains a _view_ from
$\mathsf{View}=\mathsf{Var}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{Time}}$,
a function, that for a shared variable $\mathsf{x}$, returns the timestamp of
the most recent event the thread has observed on $\mathsf{x}$. Besides, the
thread keeps track of the command to be executed next (which can be
represented as program counter) and the register valuation from
$\mathsf{RVal}=\mathsf{Reg}\rightarrow\mathsf{Dom}$. The set of _thread-local
configurations_ is thus

$\displaystyle\mathsf{LCF}\;=\;\mathsf{Com}\times
\mathsf{RVal}\times\mathsf{View}.$

Unbounded Threads. The number of threads executing in the system is not known
a priori. As long as we restrict ourselves to safety properties, there are two
ways of modeling this. One way is to define _instance programs_ for a given
number of threads, and then requiring correctness of all instances, as has
been done in [19]. The alternative is to consider an infinite number of
threads right away. We take the latter approach and define $\mathsf{TID}={\rm
Nature}$ to be the set of thread identifiers. The thread-local configuration
map then assigns a local configuration to each thread:

$\displaystyle\mathsf{LCFMap}\;=\;\mathsf{TID}\rightarrow\mathsf{LCF}.$

Views. The views maintained by the threads are used for synchronization. They
determine where in the (appropriate) total order a thread can place a store
and from which stores it can load a value. To achieve this, the shared memory
consists of _messages_ , which are variable value pairs enriched by a view,
with the form $(\mathsf{x},\mathsf{d},\mathsf{vw})$:

$\displaystyle\mathsf{Msgs}\;=\;\mathsf{Var}\times\mathsf{Dom}\times\mathsf{View}.$

Shared Memory. A _memory state_ is a set of such messages, and we use
$\mathsf{Mem}=2^{\mathsf{Msgs}}$ for the set of all memory states. With this,
the set of all _configurations_ of parametrized systems under release-acquire
is

$\displaystyle\mathsf{CF}=\mathsf{Mem}\times\mathsf{LCFMap}.$

Transitions. To define the transition relation among configurations, we first
give a _thread-local transition relation_ among thread-local configurations
$\xrightharpoondown{}\
\subseteq\mathsf{LCF}\times\mathsf{LAB}\times\mathsf{LCF}$ in Figure 1.
Thread-local transitions may be labeled or unlabeled, indicated by
$\mathsf{LAB}=\\{\varepsilon\\}\cup(\\{\mathsf{ld},\mathsf{st},\mathsf{cas}\\}\times\mathsf{Msgs})$.
The unlabeled transitions capture the control flow within a thread and
properly handle assignments and assumes. They are standard. The message-
labeled transitions capture the interaction of the thread with the shared
memory. We elaborate on the load, store, and CAS transitions by which a thread
with local view $\mathsf{vw}$, interacts with the shared memory.

Load. A load transition $\mathsf{r} \coloneqq\mathsf{x}$ picks a message
$(\mathsf{x},\mathsf{d},\mathsf{vw}^{\prime})$ from the shared memory where
$\mathsf{d}$ is the value stored in the message and updates its register
$\mathsf{r}$ with value $\mathsf{d}$. The message should not be outdated,
which means the timestamp of $\mathsf{x}$ in the message,
$\mathsf{vw}^{\prime}(\mathsf{x})$, should be at least the thread’s current
timestamp for $\mathsf{x}$, $\mathsf{vw}(\mathsf{x})$. The timestamps of other
variables do not influence the feasibility of the load transition. They are
taken into account, however, when the load is performed. The thread’s local
view is updated by joining the thread’s current view $\mathsf{vw}$ and
$\mathsf{vw}^{\prime}$ by taking the maximum timestamp per address;
$(\mathsf{vw}\sqcup\mathsf{vw}^{\prime})=\lambda\mathsf{x}.\max(\mathsf{vw}(\mathsf{x}),\mathsf{vw}^{\prime}(\mathsf{x}))$.

Store. When a thread executes a store $\mathsf{x} \coloneqq\mathsf{r}$ it adds
a message $(\mathsf{x},\mathsf{d},\mathsf{vw}^{\prime})$ to the memory, where
$\mathsf{d}$ is the value held by the register $\mathsf{r}$. The new thread-
local view (and the message view), $\mathsf{vw}^{\prime}$, is obtained from
the current $\mathsf{vw}$ by increasing the time-stamp of $\mathsf{x}$. We use
$\mathsf{vw}<_{x}\mathsf{vw}^{\prime}$ to mean
$\mathsf{vw}(\mathsf{x})<\mathsf{vw}^{\prime}(\mathsf{x})$ and
$\mathsf{vw}(\mathsf{y})=\mathsf{vw}^{\prime}(\mathsf{y})$ for all variables
$\mathsf{y}\neq\mathsf{x}$.

CAS. A CAS transition is a load and store instruction executed atomically.
$\mathsf{cas}(\mathsf{x},\mathsf{r}_{1},\mathsf{r}_{2})$ has the intuitive
meaning $\mathsf{atomic\\{}\mathsf{r}
\coloneqq\mathsf{x};\;\mathsf{assume}\;{\mathsf{r}=\mathsf{r}_{1}};\;\mathsf{x}
\coloneqq\mathsf{r}_{2}\mathsf{\\}}$. The instruction checks whether the
shared variable $\mathsf{x}$ holds the value of $\mathsf{r}_{1}$ and, in case
it does, sets it to the value of $\mathsf{r}_{2}$. The check and the
assignment happen atomically. Under RA, this means the timestamp $\mathsf{ts}$
of the load instruction and the timestamp $\mathsf{ts}^{\prime}$ of the store
instruction involved in the CAS should be adjacent,
$\mathsf{ts}^{\prime}=\mathsf{ts}+1$.

The transition relation among configurations $\xrightarrow{}\
\subseteq\mathsf{CF}\times\mathsf{TID}\times(\mathsf{Msgs}\cup\\{\varepsilon\\})\times\mathsf{CF}$
is defined in Figure 1. It is labeled by a thread identifier and possibly
message (if the transition interacts with the shared memory). The relation
expects a thread $\mathsf{t}$ which performs the transition. In the case of
local computations, there are no more requirements and the transition
propagates to the configuration. In the case of loads, we require the memory
to hold the message to be loaded. In the case of stores, the message to be
stored should not conflict with the memory. In the case of CAS, we require
both of the above, and that the two messages should have consecutive
timestamps. We defer the definition of non-conflicting messages for the moment
until we can give it in broader perspective.

Fix a parametrized system of interest $\mathsf{c}$. The initial thread-local
configuration is
$\mathsf{lcf}_{\mathsf{init}}=(\mathsf{c},\mathsf{rv}_{0},\mathsf{vw}_{0})$,
where the register valuation assigns $\mathsf{rv}_{0}(\mathsf{r})=0$ to all
registers and the view has $\mathsf{vw}_{0}(\mathsf{x})=0$ for all
$\mathsf{x}\in\mathsf{Var}$. The _initial configuration_ of the parametrized
system is
$\mathsf{cf}_{0}=(\mathsf{Mem}_{\mathsf{init}},\mathsf{lcfm}_{\mathsf{init}})$
with an initial memory $\mathsf{Mem}_{\mathsf{init}}$ consisting of messages
where all shared variables store the value
$\mathsf{d}_{\mathsf{init}}\in\mathsf{Dom}$, along with the initial view which
assigns time stamp 0 to all shared variables, and
$\mathsf{lcfm}_{\mathsf{init}}(\mathsf{t})=\mathsf{lcf}_{\mathsf{init}}$ for
all threads. A _computation_ (or a run) is a finite sequence of consecutive
transitions

$\displaystyle\rho\;=\;\mathsf{cf}_{0}\xrightarrow{(\mathsf{t}_{1},\mathsf{msg}_{1})}\mathsf{cf}_{1}\xrightarrow{(\mathsf{t}_{2},\mathsf{msg}_{2})}\ldots\xrightarrow{(\mathsf{t}_{n},\mathsf{msg}_{n})}\mathsf{cf}_{n}.$

The computation is initialized if
$\mathsf{cf}_{0}=\mathsf{cf}_{\mathsf{init}}$. We use $\mathsf{TS}(\rho)$ for
the set of all non-zero timestamps that occur in all configurations across all
variables. We use $\mathsf{TID}(\rho)$ to refer to the set of thread
identifiers labeling the transitions. For a set
$\mathsf{TID}^{\prime}\subseteq\mathsf{TID}$ of thread identifiers, we use
$\rho\\!\downarrow_{\mathsf{TID}^{\prime}}$ to project the computation to
transitions from the given threads. With
$\mathsf{first}(\rho)=\mathsf{cf}_{0}$, $\mathsf{last}(\rho)=\mathsf{cf}_{n}$
we access the first/last configurations in the computation.

######  Example 2.1.

Consider the program given in Figure 2 which implements a simplified version
of the Dekker’s mutual exclusion protocol for two threads. There are two
shared variables $\mathsf{x}$ and $\mathsf{y}$. Both $\mathsf{x},\mathsf{y}$
are initialized to 0, and at instructions $\lambda_{0},\lambda^{\prime}_{0}$
the registers $\mathsf{r}_{1},\mathsf{r}^{\prime}_{1}$ are initialized to 1.
The first thread $\mathsf{t}_{1}$ signals that it wants to enter the critical
section by writing the value 1 to $\mathsf{x}$. It then checks if thread
$\mathsf{t}_{2}$ has asked to enter the critical section by reading the value
of $\mathsf{y}$ and storing it into the register $\mathsf{r}_{1}$. The thread
$\mathsf{t}_{1}$ is allowed to enter the critical section only if the value
stored in the register $\mathsf{r}_{1}$ is 0. The second thread
$\mathsf{t}_{2}$ behaves in a symmetric manner.

$\begin{array}[]{c}\text{Variables }\mathsf{x}\text{ and }\mathsf{y}\text{
have been initialized to 0}\\\ \begin{array}[]{l|l}\hline\cr\text{Thread
}\mathsf{t}_{1}&\text{Thread }\mathsf{t}_{2}\\\
\hline\cr\lambda_{0}:\leavevmode\nobreak\ \mathsf{r}_{1} \coloneqq
1&\lambda^{\prime}_{0}:\leavevmode\nobreak\ \mathsf{r}^{\prime}_{1} \coloneqq
1\\\ \lambda_{1}:\leavevmode\nobreak\ \mathsf{x}
\coloneqq\mathsf{r}_{1}&\lambda^{\prime}_{1}:\leavevmode\nobreak\ \mathsf{y}
\coloneqq\mathsf{r}^{\prime}_{1}\\\ \lambda_{2}:\leavevmode\nobreak\
\mathsf{r}_{1} \coloneqq\mathsf{y}&\lambda^{\prime}_{2}:\leavevmode\nobreak\
\mathsf{r}^{\prime}_{1} \coloneqq\mathsf{x}\\\
\lambda_{3}:\leavevmode\nobreak\
\texttt{if}(\mathsf{r}_{1}==0):&\lambda^{\prime}_{3}:\leavevmode\nobreak\
\texttt{if}(\mathsf{r}^{\prime}_{1}==0):\\\
\quad\qquad\texttt{criticalsection}&\quad\qquad\texttt{criticalsection}\\\
\hline\cr\end{array}\end{array}$

Figure 2: On the top, is a simplified version of Dekker’s mutual exclusion
protocol. Below, is a partial execution sequence under RA. The rectangles show
the contents (messages) of the shared memory. Messages have three components -
(1) the variable, (2) value of the message and (3) the message view - a map
from $\\{\mathsf{x},\mathsf{y}\\}$ to the set of timestamps
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{Time}}$
($\mathbb{N}$). The lines below show the thread-local state - instruction-
pointer, register valuation and thread-local view

.

Under Sequential Consistency (SC) [54], which is a stronger notion of
consistency, the mutual exclusion property (i.e., at most one thread is in the
critical section at any time) is preserved. However, this is not the case
under the RA memory model. To see why, consider the execution sequence
presented in Fig 2. At each instant, the figure shows where the instruction-
counter (i.e., the label of the next instruction to get executed) resides in
each of the threads, along with the values of the registers. The black arrows
with instruction labels $\lambda_{1},\lambda^{\prime}_{1}$ show the evolution
of the run on executing the instruction labeled
$\lambda_{1},\lambda^{\prime}_{1}$ respectively. Let $\mathsf{m}_{\lambda}$
represent the memory obtained after executing the instruction labeled
$\lambda$, and let $\mathsf{msg}_{\lambda}$ be the unique new message (if any)
that is part of $\mathsf{m}_{\lambda}$ after the execution of the instruction
labeled $\lambda$. The initial memory is $\mathsf{m}_{\mathsf{init}}$ where
$\mathsf{x},\mathsf{y}$ have values and timestamps 0;
$\mathsf{msg}_{\mathsf{x}},\mathsf{msg}_{\mathsf{y}}$ represent the messages
in $\mathsf{m}_{\mathsf{init}}$ corresponding to $\mathsf{x},\mathsf{y}$. The
execution of the instruction labeled by $\lambda_{1}$ results in the addition
of a new message $\mathsf{msg}_{\lambda_{1}}$ to the memory whose timestamp
(10) is higher than 0 (which is the current timestamp of the variable
$\mathsf{x}$ for $\mathsf{t}_{1}$). The view of $\mathsf{t}_{1}$ is then
updated to $\mathsf{x}\mapsto 10,\mathsf{y}\mapsto 0$. Likewise, the execution
of the instruction labeled by $\lambda^{\prime}_{1}$ results in the addition
of a new message $\mathsf{msg}_{\lambda^{\prime}_{1}}$ to the memory with a
higher time stamp (7). This will result in the update of the view of
$\mathsf{t}_{2}$ to $\mathsf{x}\mapsto 0,\mathsf{y}\mapsto 7$, wrt. the
variable $\mathsf{y}$. The read instruction labeled by $\lambda_{2}$ is then
allowed to use the message $\mathsf{msg}_{\mathsf{y}}$ to fetch the value of
$\mathsf{y}$, since the view of $\mathsf{t}_{1}$ wrt. $\mathsf{y}$ is 0.
Likewise, in the case of $\mathsf{t}_{2}$ concerning the execution of the
instruction labeled by $\lambda^{\prime}_{2}$, the message
$\mathsf{msg}_{\mathsf{x}}$ is used since the view of $\mathsf{t}_{2}$ wrt.
$x$ is 0. After these steps, both threads enter their respective critical
section.

####  2.2.1 Conflict

We need a notion of conflict not only for messages, but also for memories,
configurations, and computations. Two messages are non-conflicting, denoted by
$(\mathsf{x}_{1},\mathsf{d}_{1},\mathsf{vw}_{1})\;\\#\;(\mathsf{x}_{2},\mathsf{d}_{2},\mathsf{vw}_{2})$,
if either their variables are different, $\mathsf{x}_{1}\neq\mathsf{x}_{2}$,
the timestamps are different,
$\mathsf{vw}_{1}(\mathsf{x}_{1})\neq\mathsf{vw}_{2}(\mathsf{x}_{2})$, or the
timestamps are zero,
$\mathsf{vw}_{1}(\mathsf{x}_{1}){=}0{=}\mathsf{vw}_{2}(\mathsf{x}_{2})$.
Observe that initial messages do not conflict with any other message.

Two memory states are non-conflicting, $\mathsf{m}_{1}\;\\#\;\mathsf{m}_{2}$,
if for all $\mathsf{msg}_{1}\in\mathsf{m}_{1}$ and all
$\mathsf{msg}_{2}\in\mathsf{m}_{2}$ we have
$\mathsf{msg}_{1}\;\\#\;\mathsf{msg}_{2}$. Two configurations are non-
conflicting, $\mathsf{cf}_{1}\;\\#\;\mathsf{cf}_{2}$, if their memory states
are non-conflicting. Two computations are non-conflicting, denoted
$\rho\;\\#\;\rho^{\prime}$, if they use different threads and non-conflicting
messages, $\mathsf{TID}(\rho)\cap\mathsf{TID}(\rho^{\prime})=\emptyset$ and
$\mathsf{last}(\rho)\;\\#\;\mathsf{last}(\rho^{\prime})$.

##  3 Undecidability of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{acyc})$

In this section, we establish the undecidabililty of the class
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{acyc})$,
that is the class with loop-free
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads (which can execute arbitrarily-many CAS operations) and without any
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads. This result essentially shows that even with the loop-free
assumption, allowing
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads to perform CAS operations is in itself intractable from a safety
verification viewpoint. Hence, the $\mathsf{nocas}$ restriction that we impose
on
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads is a justified means of achieving tractabililty.

In fact, we will show a stronger result. We will show that we can transform a
non-paramterized system consisting of $k$ distinguished threads having full
instruction set and loops under RA (the class
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}\parallel\cdots\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{k}$)
to a parameterized system corresponding to the class
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{acyc})$
such that, control-state reachability is preserved. With this equivalence, the
claim would follow by the undecidability result of [1].

###  3.1 Constructing the equivalent loop-free program

To show this result, we transform an input of $n$ programs
$\\{\mathsf{c}_{1},\mathsf{c}_{2},\cdots,\mathsf{c}_{n}\\}$ and a failure
state label $\lambda_{\mathsf{fail}}$ in some $\mathsf{c}_{i}$ (with possibly
full instruction set and loops) and transform them into a single program
$\mathsf{c}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
and failure state $\lambda_{\mathsf{fail}}^{\prime}$, the control flow for
which is loop-free but uses the full instruction set including CAS operations.
We claim that the state label $\lambda_{\mathsf{fail}}$ is reachable in
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}\parallel\cdots\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{n}$
with
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}$
executing $\mathsf{c}_{i}$ if and only if the state label
$\lambda_{\mathsf{fail}}^{\prime}$ is reachable in the system
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{acyc})$
with the environment threads executing
$\mathsf{c}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$.
Let the variable set, data domain and register set of the original system be
$\mathsf{Var}$, $\mathsf{Dom}$ and
$\mathsf{Reg}=\\{\mathsf{r}_{1},\cdots,\mathsf{r}_{k}\\}$ as usual. We assume
that the memory is initialized to 0 on all variables.

Converting a single program $\mathsf{c}_{i}$ to $\mathsf{c}_{i}^{\prime}$ We
show how we can convert one thread program $\mathsf{c}_{i}$ into a loop-free
program $\mathsf{c}_{i}^{\prime}$ and then show how we can combine all the
programs together into a single loop-free program
$\mathsf{c}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$.
Consider for an $i$, the program $\mathsf{c}_{i}$. For the purposes of this
construction, we will assume that the program $\mathsf{c}_{i}$ has been
specified as a transition system rather than in the while-language syntax. It
is clear that both representations are equivalent and can be interconverted
with only polynomial overhead. Hence we assume that
$\mathsf{c}_{i}=(Q,\Delta,\iota)$ where $Q$ is the set of control states,
$\Delta$ is the transition relation and $\iota$ maps each transition to its
corresponding instruction from
$\\{\mathsf{skip},\mathsf{assume}\;{\mathsf{e}(\overline{\mathsf{r}})},\mathsf{r}
\coloneqq\mathsf{e}(\overline{\mathsf{r}}),\mathsf{r}
\coloneqq\mathsf{x},\mathsf{x}
\coloneqq\mathsf{r},\mathsf{cas}(\mathsf{x},\mathsf{r}_{1},\mathsf{r}_{2})\\}$.
We transform $\mathsf{c}_{i}$ to a loop-free program as follows. Let
$Q=\\{q_{0},\cdots,q_{n}\\}$ and with $q_{0}$ as the initial state.

In this conversion, we add extra variables and values such that
$\mathsf{Var}^{\prime}=\mathsf{Var}\uplus\\{t_{i},\mathfrak{r}_{i}^{1},\cdots,\mathfrak{r}_{i}^{|\mathsf{Reg}|}\\}$
and
$\mathsf{Dom}^{\prime}=\mathsf{Dom}\cup\\{0,\cdots,|Q|-1,\Lambda^{\bot}\\}$
where $\uplus$ denotes disjoint union. Now we specify the new transition
system $\mathsf{c}_{i}^{\prime}$ which needs to be loop-free. For each
transition $\partial=(q_{a},q_{b})\in\Delta$, with source and end states
$q_{a}$ and $q_{b}$ respectively and instruction $\iota(\partial)$, we
transform it into the following three transition sequence (a sequence of green
transitions starting with a CAS, followed by $k$ load operations; the
transition corresponding to $\iota(\partial)$, followed by the sequence of
pink transitions consisting of $k$ store operations ending with a CAS) denoted
as $\mbox{\Lightning}(\partial)$.

$\displaystyle\mbox{\Lightning}(\partial)\leavevmode\nobreak\ =$
$\displaystyle\leavevmode\nobreak\
{\color[rgb]{0,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0.5}q_{\mathsf{start}}\xrightarrow{\mathsf{cas}(t_{i},a,\Lambda^{\bot})}q_{\partial}^{0}\xrightarrow{\mathsf{r}_{1}
\coloneqq\mathfrak{r}_{i}^{1}}q_{\partial}^{1}\cdots
q_{\partial}^{k-1}\xrightarrow{\mathsf{r}_{k}
\coloneqq\mathfrak{r}_{i}^{k}}}q_{\partial}^{k}\xrightarrow{\iota(\partial)}q_{\partial}^{k+1}\cdots\quad\text{(contd.
below)}$ $\displaystyle\leavevmode\nobreak\ \cdots
q_{\partial}^{k+1}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\xrightarrow{\mathfrak{r}_{i}^{1}
\coloneqq\mathsf{r}_{1}}q_{\partial}^{k+2}\cdots
q_{\partial}^{2k-1}\xrightarrow{\mathfrak{r}_{i}^{k}
\coloneqq\mathsf{r}_{k}}q_{\partial}^{2k}\xrightarrow{\mathsf{cas}(t_{i},\Lambda^{\bot},b)}q_{\mathsf{end}}}$

We construct $\mbox{\Lightning}(\partial)$ for each transition $\partial$ in
$\Delta$ to get the complete transition system. The initial/final
(collectively called terminal) nodes of this transition system are
$q_{\mathsf{start}},q_{\mathsf{end}}$ (which are common to all
$\mbox{\Lightning}(\partial)$). The internal $q_{\partial}^{\\_}$ states are
all distinct across the $\mbox{\Lightning}(\partial)$ for different
$\partial$. The transition system that we obtain has size
$\mathcal{O}(|\mathsf{Reg}||\Delta|)$ (each original transition from $q_{a}$
to $q_{b}$ is transformed into a sequence of $2|\mathsf{Reg}|+3$ transitions
between $q_{\mathsf{start}}$ and $q_{\mathsf{end}}$). It is clearly loop-free.
See Figure 3 showing an example if we start with
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{j}$.

Combining individual $\mathsf{c}_{i}^{\prime}$ We construct programs
$\mathsf{c}_{i}^{\prime}$ as described above for each thread
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}$.
Now we combine these individual programs into a single program
$\mathsf{c}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$.We
ensure that the newly added shared variables ($t_{i}$,
$\mathfrak{r}_{i}^{\\_}$ for
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}$)
are also disjoint across threads. Hence the variable set is now
$\mathsf{Var}^{\prime}=\mathsf{Var}\uplus\\{t_{1},\cdots,t_{n}\\}\uplus\\{\mathfrak{r}_{i}^{j}\\}_{i\in[n],j\in[|\mathsf{Reg}|]}$
(where $\mathsf{Var}$ was the original variable set
$\\{\mathsf{c}_{1},\mathsf{c}_{2},\cdots,\mathsf{c}_{n}\\}$ were operating
with). Finally, the combined data domain is simply a union of individual data
domains (which possibly overlap). We combine the individual programs as

$\mathsf{c}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}=\mathsf{c}_{1}^{\prime}\oplus\mathsf{c}_{2}^{\prime}\oplus\cdots\oplus\mathsf{c}_{n}^{\prime}$

where $\oplus$ denotes non-deterministic choice. It is clear that
$\mathsf{c}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
is loop-free. Additionally,
$|\mathsf{c}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}|$,
and the new $|\mathsf{Dom}^{\prime}|$ and $|\mathsf{Var}^{\prime}|$ is
polynomial in $\sum_{i}|\mathsf{c}_{i}|$ and previous $|\mathsf{Var}|$ and
$|\mathsf{Dom}|$.

$q_{0}$$q_{2}$$q_{0}$$q_{1}$$q_{2}$$q_{1}$$\partial_{1}$$\partial_{2}$$\partial_{5}$$\partial_{3}$$\partial_{4}$Program
$\mathsf{c}_{i}$Program
$\mathsf{c}_{j}$$q_{\mathsf{end}}$$q_{\mathsf{end}}$$q_{\mathsf{start}}$$q_{\mathsf{start}}$Transformed
program $\mathsf{c}^{\prime}_{j}$Transformed program
$\mathsf{c}^{\prime}_{i}$$\iota(\partial_{1})$$\iota(\partial_{2})$$\iota(\partial_{3})$$\iota(\partial_{4})$$\iota(\partial_{5})$register
loadsregister loadsregister storesregister
stores$\mathsf{cas}(t_{i},0,\Lambda^{\bot})$$\mathsf{cas}(t_{i},1,\Lambda^{\bot})$$\mathsf{cas}(t_{i},\Lambda^{\bot},2)$$\mathsf{cas}(t_{i},\Lambda^{\bot},1)$$\mathsf{cas}(t_{j},\Lambda^{\bot},1)$$\mathsf{cas}(t_{j},\Lambda^{\bot},1)$$\mathsf{cas}(t_{j},0,\Lambda^{\bot})$$\mathsf{cas}(t_{j},2,\Lambda^{\bot})$$\mathsf{cas}(t_{j},1,\Lambda^{\bot})$$\mathsf{cas}(t_{j},\Lambda^{\bot},2)$

Figure 3: Examples of two
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}$
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{j}$
executing programs $\mathsf{c}_{i},\mathsf{c}_{j}$ and the corresponding
transformed programs $\mathsf{c}^{\prime}_{i},\mathsf{c}^{\prime}_{j}$. The
program $c_{i}$ has 2 transitions while $c_{j}$ has 3 transitions. Note how
the read-write value for CAS operations in the transformed program match with
the transitions in the original program.

###  3.2 Proof of Equivalence

We now prove that the system
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{acyc})$
with the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads executing the program
$\mathsf{c}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
as defined above respect the original system. We defer the notion of
‘maintaining reachability’ for a bit later. We first observe the program
$\mathsf{c}_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
and make some observations.

####  3.2.1 Simulation of individual threads

Locking/unlocking of $\mathsf{c}_{i}^{\prime}$. For any single transformed
program $\mathsf{c}_{i}^{\prime}$, we note that at any given point, only one
thread can be in any internal (not initial/final) state of
$\mathsf{c}_{i}^{\prime}$. To see this, note the two atomic CAS operations
flanking each 3-path in $\mathsf{c}_{i}^{\prime}$. All these CAS operations
are on the same variable $t_{i}$ and moreover there are no other operations on
$t_{i}$. Hence at any given point in time, there is only one message on
$t_{i}$ (the most recent write) that is available for a CAS operation. The
value of this message dictates whether the operation will succeed. When it
succeeds, the most recent write value changes to the value written by the CAS.

Now note that $t_{i}$ is initialized with value 0; hence initially one thread,
say $\mathsf{t}$ can take perform a CAS and change the recent value to
$\Lambda^{\bot}$. Now, there is no transition from $q_{\mathsf{start}}$ that
performs a CAS with a read of $\Lambda^{\bot}$. Hence all other threads are
kept waiting until the recent value on $t_{i}$ changes from $\Lambda^{\bot}$.
This is possible only when the initial thread $\mathsf{t}$, executes the final
transition and reaches $q_{\mathsf{end}}$, maintaining the claim. Hence these
CAS operations perform the role of a mutual-exclusion lock. But then they
perform another function too.

State transference. We now know that for each $i$, only one thread may execute
$\mathsf{c}_{i}^{\prime}$ at any given time. However the locking/unlocking
operations using CAS also enable threads to transfer their state to their
successors. There are three components to the state, which we handle in turn:

  * •

Control-state: Note that the recent value on variable $t_{i}$ is
$v\neq\Lambda^{\bot}$ only if the previous thread terminated after simulating
some transition ending at $q_{v}$. Additionally, a locking CAS operation for
$\mbox{\Lightning}(\partial)$ reads value $v$ only if $\partial$ is a
transition from $q_{v}$ to some other state. Hence, it is guaranteed that the
successive thread will execute some transition that emerges from a state where
the previous thread left off. Note how this is true for the first thread as
well since the initial value on all variables is 0 and the initial state of
the transition system is $q_{0}$.

  * •

View: The second component that we consider is the view. This also is
transferred from a thread to its successor through the CAS operation. In
particular, when a thread $\mathsf{t}$ executes the final CAS operation to
reach $q_{\mathsf{end}}$, it generates a message on $t_{i}$ which is read by
its successor. This read implies that the successor will take the join on its
own (initial) view with that of the message and hence essentially accumulate
the exact view that the previous thread left with. So, the view is transferred
as well.

  * •

Register valuations: The previous thread $\mathsf{t}$ stores its register
valuations in the shared variables $\mathfrak{r}_{i}^{j}$ in the final
sequence of store operations before terminating. These are then accessed by
the successor thread through the initial sequence of load operations.

In this way we see that not only is exclusion ensured, but the thread states
are transferred from one thread to the next. Together, these sequences of
threads simulate the entire run of the original
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}$
in fragments. The above holds for all $i\in[n]$. Hence at any given point,
there are at most $n$ threads simulating the original ones.

####  3.2.2 The Complete Simulation

Now we formalize the notion of equivalence in reachability. We say that an
original state with the threads
$\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1},\cdots,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{n}\\}$
is equivalent to a new state when we have the following.

  * •

if the control states of threads
$\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1},\cdots,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{n}\\}$
are $(q_{i_{1}},q_{i_{2}},\cdots,q_{i_{n}})$ respectively then in the new
system with
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$,
the recent value of shared variable $t_{j}$ is $i_{j}$,

  * •

the register valuation of each original
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}$
is reflected ($\mathsf{r}_{j}$ = most recent write to $\mathfrak{r}_{i}^{j}$)
in the most recent writes to the variables $\mathfrak{r}_{i}^{\\_}$ for each
thread $i$,

  * •

the view of
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}$
is the view stored in the most recent message to $t_{i}$ (again projected on
the original variable set) and

  * •

the global memory (projected) is identical across the original and
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
states.

We claim the following: a state in the original system can be reached if and
only some equivalent state in the new system can be reached. We can prove this
by induction. The base case is that all threads are in their initial states,
registers and views with the memory only with initial messages (0 on each
variable). This trivially satisfies the requirement, both in the forward and
reverse directions.

Now for the inductive case ($\Rightarrow$). Assume that it was true at some
instant. Let some
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}$
execute an instruction for the transition $\partial$. In the new system, we
can simulate this as a new
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread $\mathsf{t}$ taking the path corresponding to
$\mbox{\Lightning}(\partial)$ in $\mathsf{c}_{i}^{\prime}$. We note by the
observations above that the invariants for the thread-local state (control-
state, register valuations and view) is maintained. Additionally, if
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}$
wrote a message to the memory, then so can $\mathsf{t}$. In particular, since
the view of $\mathsf{t}$ is obtained from the CAS read, it matches that of
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}$.
Hence the message added by $\mathsf{t}$ can have the same timestamps as
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}$.

Inductive case ($\Leftarrow$). The same argument works in the reverse
direction. Assume that a pair of equivalent states have been reached. Now,
consider a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread path $\mbox{\Lightning}(\partial)$ in $\mathsf{c}_{i}^{\prime}$ where
$\partial=(q_{a},q_{b})$. Then, by the induction hypothesis this means that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{i}$
is in state $q_{a}$ in the original run. Given the equality of thread and
memory state initially, it too can take the transition $(q_{a},q_{b})$. Once
again, the invariant follows from the earlier observations.

This gives a sketch of the proof. In particular, note that even though we give
an equivalence between the control state in the original system and a variable
value in the new system, this can be easily converted to an equivalence
between control states themselves. This means that the reachability problem
for
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}\parallel\cdots\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{n}$
can can converted to a reachability problem for
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{acyc})$.
This prompts us to restrict
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads to a reduced (cas-free) instruction set and motivates the idea of
modelling CAS instructions in a run via computations of the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads.

##  4 A Simplified Semantics

In this section, we propose a simplified semantics for the class of systems
given by
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}(\mathsf{nocas})\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}\parallel\dots\parallel{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{n}$.
The core of this result relies on the _Infinite Supply Lemma_ which shows that
if some
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread could generate a message $(\mathsf{x},\mathsf{val},\mathsf{vw})$, then
a clone of that thread could generate the message
$(\mathsf{x},\mathsf{val},\mathsf{vw}^{\prime})$ with
$\mathsf{vw}^{\prime}=\mathsf{vw}[\mathsf{x}\mapsto t]$ for some
$t>\mathsf{vw}(\mathsf{x})$.

There are two assumptions that the infinite supply lemma and hence our
semantic simplification result rely on:

  * •

arbitrarily many
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads executing identical programs.

  * •

the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads do not have atomic instructions (CAS).

The first assumption allows us to have clone
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads that duplicate the computation and hence the messages generated in it.
The second assumption is required for the duplicated computation to remain
valid under RA.

While performing the duplication, one must keep in mind the dependency between
stores and loads across threads. The fact that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads are not replicatable (their messages cannot be duplicated) adds to the
challenge. To ensure that the clone threads can follow in the footsteps of the
original computation we require that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
messages can be read by the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
clones whenever they can be read by the original
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads. This necessitates that we respect relative order among timestamps
between
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads.

We develop some intermediate concepts that help us in developing a valid
duplicate run. In order to accommodate the clone threads, we must make space
(create unused timestamps) along
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{Time}}$
for clones to write messages. We do this via timestamp liftings. Having done
this, we need to define how we can combine the original computation with that
of the clones. We develop the concept of superposition of computations to do
this. Finally, the infinite supply (of messages) lemma shows how, using the
earlier two concepts, we can generate copies of messages, with higher
timestamps.

This ‘duplication-at-will’ of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
messages means that we need not store the entire set of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
messages produced. Those with the smallest timestamps act as good
representatives of the set. Additionally when any thread reads from an
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
message, we need not be bothered about timestamp comparisons since we could
always generate a copy of that message with as high timestamp as required. It
is this observation that gives us the timestamp abstraction and with it the
simplified semantics.

###  4.1 Infinite Supply

We now make these arguments precise. Our strategy is to split up the
timestamps (hence the computation) and separate the part originating from the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads from the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
part (which can be duplicated at will). We write
$\rho\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$
and
$\rho\\!\downarrow_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}}$
to denote the projections of $\rho$ to
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
respectively.

####  4.1.1 Timestamp Lifting

In our development we will make use of _timestamp transformations_
$\mathsf{tf}:{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{Time}}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{Time}}$.
We extend these to views $\mathsf{vw}$ with per variable timestamp
transformations
$\mathsf{tf}=\\{\mathsf{tf}^{\mathsf{x}}\\}_{\mathsf{x}\in\mathsf{Var}}$,
where $\mathsf{tf}^{\mathsf{x}}$ only transforms the timestamps for the
variable $\mathsf{x}$. The transformed view
$\mathsf{tf}(\mathsf{vw}):\mathsf{Var}\rightarrow{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{Time}}$
is defined by
$(\mathsf{tf}(\mathsf{vw}))(\mathsf{x})=\mathsf{tf}^{\mathsf{x}}(\mathsf{vw}(\mathsf{x}))$
for every variable $\mathsf{x}$.

As an example consider shared variables $\mathsf{x},\mathsf{y}$ and views
$\mathsf{vw}_{1},\mathsf{vw}_{2}$ such that
$\mathsf{vw}_{1}=[\mathsf{x}\mapsto 2,\mathsf{y}\mapsto 5]$ and
$\mathsf{vw}_{2}=[\mathsf{x}\mapsto 10,\mathsf{y}\mapsto 0]$. Using the
timestamp transformation
$\mathsf{tf}=\\{\mathsf{tf}^{\mathsf{x}},\mathsf{tf}^{\mathsf{y}}\\}$ where
$\mathsf{tf}^{\mathsf{x}}(0)=\mathsf{tf}^{\mathsf{y}}(0)=0$,
$\mathsf{tf}^{\mathsf{x}}(t)=t+2$ and $\mathsf{tf}^{\mathsf{y}}(t)=t+7$ for
$t>0$, we obtain $\mathsf{tf}(\mathsf{vw}_{1})=[\mathsf{x}\mapsto
4,\mathsf{y}\mapsto 12]$ and $\mathsf{tf}(\mathsf{vw}_{2})=[\mathsf{x}\mapsto
12,\mathsf{y}\mapsto 0]$. We also apply the timestamp transformation to
messages, memories, configurations, and computations by transforming all view
components.

RA-valid timestamp lifting. An _RA-valid timestamp lifting_ for a run $\rho$
is a (per variable) timestamp transformation
$\mathcal{M}=\\{\mu^{\mathsf{x}}\\}_{\mathsf{x}\in\mathsf{Var}}$ satisfying
two properties for each $\mathsf{x}\in\mathsf{Var}$: (1) it is strictly
increasing, $\mu^{\mathsf{x}}(0)=0$; for all $t_{1},t_{2}\in{\rm Nature}$ with
$t_{1}<t_{2}$ we have $\mu^{\mathsf{x}}(t_{1})<\mu^{\mathsf{x}}(t_{2})$ and
(2) if there is a CAS operation on $\mathsf{x}$ with (load, store) timestamps
as $(t,t+1)$ then $\mu^{\mathsf{x}}(t+1)=\mu^{\mathsf{x}}(t)+1$, i.e.
consecution of CAS-timestamps is maintained. Note that
$\mu(\mathsf{cf}_{\mathsf{init}})=\mathsf{cf}_{\mathsf{init}}$. In the example
above, $\mathsf{tf}$ is a RA-valid timestamp lifting.

Lemma 4.1 says that the run $\mathcal{M}(\rho)$ obtained by modifying the
timestamps of a valid run $\rho$ with an RA-valid timestamp lifting
$\mathcal{M}$ is also a valid under the RA semantics.

######  Lemma 4.1 (Timestamp Lifting Lemma).

Let $\mathcal{M}=\\{\mu^{\mathsf{x}}\\}_{\mathsf{x}\in\mathsf{Var}}$ be an RA-
valid timestamp lifting. If $\rho$ is a computation under RA, then so is
$\mathcal{M}(\rho)$. Hence if a configuration $\mathsf{cf}$ is reachable under
RA then so is $\mathcal{M}(\mathsf{cf})$.

######  Proof 4.2.

This result follows since timestamp lifting is just a relabelling of
timestamps for each shared variable. The lemma relies on the following
facts/observations:

  * •

There are no timestamp comparisons across variables, $\mathsf{vw}(\mathsf{x})$
is never compared with $\mathsf{vw}(\mathsf{x}^{\prime})$ for
$\mathsf{x}\neq\mathsf{x}^{\prime}$.

  * •

The relative order between timestamps on the same variable is preserved due to
the strictly increasing property. Additionally, $\mu(0)=0$, maintaining the
timestamps of the $\mathsf{init}$ messages.

  * •

The load, store timestamps of (CAS-local) operations still remain consecutive.

In particular the lemma can be formally proven by induction on the length of
the run. The base case is trivial and the inductive case follows by showing
that each instruction - read, write, CAS - that can be executed in $\rho$ can
be executed in the lifted run, $\mathcal{M}(\rho)$.

The duplication of messages by the clone
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads requires us to copy computations and then merge them such that the RA
semantics are not violated. This requries (1) timestamps of merging
computations to not conflict and (2) the reads-from dependencies between
threads are respected. With this in mind, we introduce the idea of
superposition.

####  4.1.2 Superposition

We define the _superposition_ $\rho\triangleright\rho^{\prime}$ of two
computations $\rho,\rho^{\prime}$ as the computation that first executes
$\rho$ and then $\rho^{\prime}$. This requires us to combine the memory in
$\mathsf{last}(\rho)$ with that of every configuration in $\rho^{\prime}$.
Moreover, the threads transitioning in $\rho,\rho^{\prime}$ must be disjoint.
Given these considerations, the operation requires the computations to be non-
conflicting, $\rho\;\\#\;\rho^{\prime}$ (see Section 2.2.1), and is defined as
follows:

$\displaystyle\rho\triangleright\rho^{\prime}\;=\;\rho;(\mathsf{last}(\rho)+\rho^{\prime}).$

The addition of a configuration $\mathsf{cf}$ to a computation
$\rho\;=\;\mathsf{cf}_{0}\raisebox{-0.85pt}{$\smash{\mathrel{\stackon[-4.5pt]{\xrightarrow{\makebox[64.57784pt]{}}}{\scriptstyle(\mathsf{t}_{1},\mathsf{msg}_{1})\,}}}$}\ldots\raisebox{-0.85pt}{$\smash{\mathrel{\stackon[-4.5pt]{\xrightarrow{\makebox[65.46675pt]{}}}{\scriptstyle(\mathsf{t}_{n},\mathsf{msg}_{n})\,}}}$}\mathsf{cf}_{n}$
yields the new computation

$\displaystyle\mathsf{cf}+\rho\;=\;(\mathsf{cf}+\mathsf{cf}_{0})\xrightarrow{(\mathsf{t}_{1},\mathsf{msg}_{1})}\ldots\xrightarrow{(\mathsf{t}_{n},\mathsf{msg}_{n})}(\mathsf{cf}+\mathsf{cf}_{n}).$

Addition of configurations
$\mathsf{cf}_{1}=(\mathsf{m}_{1},\mathsf{lcfm}_{1})$ and
$\mathsf{cf}_{2}=(\mathsf{m}_{2},\mathsf{lcfm}_{2})$ is the configuration
$\mathsf{cf}_{1}+\mathsf{cf}_{2}=(\mathsf{m}_{1}\cup\mathsf{m}_{2},\mathsf{lcfm})$,
where $\mathsf{lcfm}(\mathsf{t})=\mathsf{lcfm}_{1}(\mathsf{t})$ if
$\mathsf{lcfm}_{1}(\mathsf{t})\neq\mathsf{lcf}_{\mathsf{init}}$ and
$\mathsf{lcfm}(\mathsf{t})=\mathsf{lcfm}_{2}(\mathsf{t})$ otherwise.

When $\rho\;\\#\;\rho^{\prime}$ holds, we have: (1) for any thread
$\mathsf{t}$, if it has transitioned in $\rho$, then it cannot in
$\rho^{\prime}$; likewise, if it has not transitioned in $\rho$, then it can
in $\rho^{\prime}$.

(2) $\mathsf{last}(\rho)\;\\#\;\mathsf{last}(\rho^{\prime})$, and since the
memory in earlier configurations of $\rho$ is a subset of that in
$\mathsf{last}(\rho)$, the memory unions performed above involve
nonconflicting memories. An initial configuration is neutral for addition, in
particular
$\mathsf{last}(\rho^{\prime})+\mathsf{first}(\rho)=\mathsf{last}(\rho^{\prime})$.
The operation of concatenation $\rho_{1};\rho_{2}$ expects two computations
$\rho_{1}$ and $\rho_{2}$ that satisfy
$\mathsf{last}(\rho_{1})=\mathsf{first}(\rho_{2})$ and returns the sequence
consisting of the transitions in $\rho_{1}$ followed by the transitions in
$\rho_{2}$. This need not be a valid computation under RA, but under the
following conditions it is.

Let $\mathsf{Msgs}(\rho)$ be the memory in $\mathsf{last}(\rho)$. Likewise,
let
$\mathsf{Msgs}(\rho\\!\downarrow_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}})\subseteq\mathsf{Msgs}(\rho)$
be the subset of memory in $\mathsf{last}(\rho)$, which have been added by
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads during $\rho$.

######  Lemma 4.3 (Superposition).

Consider valid computations $\rho,\rho^{\prime}$ of a parametrized system
under RA such that
$\rho\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}\\#\rho^{\prime}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$
and that
$\mathsf{Msgs}(\rho\\!\downarrow_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}})=\mathsf{Msgs}(\rho^{\prime}\\!\downarrow_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}})$.
Then the superposition
$\rho\triangleright\rho^{\prime}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$
is a valid computation under RA.

######  Proof 4.4.

Since there are arbitrarily many
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads, we distinguish apart the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads in $\rho^{\prime}$ from the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads in $\rho$. By doing so we ensure that the threads operating (changing
state) in $\rho$ and
$\rho^{\prime}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$
are disjoint.

Now consider the global state obtained after executing $\rho$ (which is a
valid run under RA). By hypothesis, the memory state contains messages from
$\rho\\!\downarrow_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}}$,
which are identical to those in
$\rho^{\prime}\\!\downarrow_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}}$.
After execution of $\rho$ is complete, we claim that we can execute
$\rho^{\prime}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$
one step at a time.

  * •

Whenever a
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
thread loads from a message generated by a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread in $\rho$, the same can happen in
$\rho\triangleright\rho^{\prime}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$.
Likewise, the relative time stamps between the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads and the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads in $\rho^{\prime}$ are the same; so
$\rho^{\prime}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$
can be executed after $\rho$.

  * •

Likewise, reads made by some
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread on $\rho,\rho^{\prime}$ either from another
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread or a
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
thread also continues exactly in the same way in
$\rho\triangleright\rho^{\prime}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$,
since the messages added by
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads are exactly same in $\rho,\rho^{\prime}$, and the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads are disjoint.

  * •

The above two points show that we have exactly the same reads-from
dependencies
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\leftrightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
in $\rho$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\leftrightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
in $\rho^{\prime}$) in
$\rho\triangleright\rho^{\prime}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$.
The reason is that
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads are disjoint and the messages added by
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads are the same in $\rho,\rho^{\prime}$. Finally, all writes made by the
respective
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads of $\rho,\rho^{\prime}$ can be done in
$\rho\triangleright\rho^{\prime}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$;
likewise, all writes made by the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads in $\rho$ can also be made in
$\rho\triangleright\rho^{\prime}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$.
The reason is that
$\rho\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}\\#\rho^{\prime}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$,
and trivially, we have
$\rho^{\prime}\\!\downarrow_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}}\\#\rho^{\prime}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$.
This ensures no conflict of write-timestamps.

Formally this can be proven by induction on the length of $\rho^{\prime}$.

Now we develop the infinite supply lemma. Recall that our goal is to generate
arbitrarily many copies of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
messages with the same variable and value but higher timestamp. Let us fix one
such message, $\mathsf{msg}=(\mathsf{x},\mathsf{d},\mathsf{vw})$, for our
discussion here and see how we can replicate it. Towards this end, consider a
computation $\rho$ in which it is generated. We ‘spread-apart’ the timestamps
of $\mathsf{Msgs}(\rho)$, using timestamp liftings so that we create ‘holes’
(unused timestamps) along
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{Time}}$.
Then we generate copies of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads, denoted as
$\mathsf{copy}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$
(possible since
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads can be replicated).

The holes accomodate for the timestamps of
$\mathsf{copy}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$
and the (higher) timestamp of the copy of $\mathsf{msg}$. Throughout this, we
preserve the order of timestamps of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}},\mathsf{copy}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$
threads relative to those of
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads. This ensures that reads-from dependencies are maintained -
$\mathsf{copy}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$
can read a
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
message whenever
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
can do so.

We define the computation $\widetilde{\rho}$ as a copy of
$\rho\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$
executed by
$\mathsf{copy}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$
threads. The write timestamps used by
$\mathsf{copy}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$
threads are the unoccupied timestamps generated by the timestamp lifting
operation $\mathcal{M}(\rho)$. We show an example of this via a graphic. Let
${\color[rgb]{1,0.1,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.1}\mathsf{e}}{{\color[rgb]{0.1,0.1,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.1,0.1}\pgfsys@color@gray@stroke{0.1}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{0.1,0.1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.1,1}\mathsf{d}}{{\color[rgb]{0.1,0.1,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.1,0.1}\pgfsys@color@gray@stroke{0.1}\pgfsys@color<EMAIL_ADDRESS>respectively denote the timestamps chosen by
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
along $\rho$ (first row).

$\displaystyle\rho\\!:\leavevmode\nobreak\ $
$\displaystyle{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{d}}\mathsf{T}^{0}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}\mathsf{T}^{0}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{d}}\mathsf{T}^{1}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}\mathsf{T}^{1}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}\mathsf{T}^{2}\leavevmode\nobreak\
\leavevmode\nobreak\ $ $\displaystyle\mathcal{M}(\rho)\\!:\leavevmode\nobreak\
$
$\displaystyle{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{d}}\mathsf{T}^{0}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.8,0.8}\mathsf{e}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}\mathsf{T}^{0}_{\mathsf{a}}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{d}}\mathsf{T}^{1}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.8,0.8}\mathsf{e}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}\mathsf{T}^{1}_{\mathsf{a}}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.8,0.8}\mathsf{e}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}\mathsf{T}^{2}_{\mathsf{a}}$
$\displaystyle\widetilde{\rho}\\!:\leavevmode\nobreak\ $
$\displaystyle{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{0.8,0.8,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,1}\mathsf{d}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}\mathsf{T}^{0}_{\mathsf{b}}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.8,0.8}\mathsf{e}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{0.8,0.8,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,1}\mathsf{d}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}\mathsf{T}^{1}_{\mathsf{b}}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.8,0.8}\mathsf{e}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}\mathsf{T}^{2}_{\mathsf{b}}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.8,0.8}\mathsf{e}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>
The second row shows lifted timestamps (with subscript $\mathsf{a}$) of
$\mathcal{M}(\rho)$ and the holes (faded). The third row shows holes being
used by
$\mathsf{copy}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$
for $\widetilde{\rho}$ (these have subscript $\mathsf{b}$). The construction
guarantees $\mathcal{M}(\rho)\;\\#\;\widetilde{\rho}$ and superposition
$\mathcal{M}(\rho)\triangleright\widetilde{\rho}$ is allowed. In this
computation, $\widetilde{\rho}$ generates a copy of $\mathsf{msg}$,
$\mathsf{msg}^{\prime}=(\mathsf{x},\mathsf{val},\mathsf{vw}^{\prime})$ with
higher $\mathsf{vw}^{\prime}(\mathsf{x})$. Additionally, since
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}\mathsf{T}^{i}_{\mathsf{a}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}\mathsf{T}^{i}_{\mathsf{b}}$
have the same position relative to all
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{d}}\mathsf{T}^{j}$
timestamps, so will $\mathsf{vw}(\mathsf{y}),\mathsf{vw}^{\prime}(\mathsf{y})$
for $\mathsf{y}\neq\mathsf{x}$.

Now we state the Infinite Supply Lemma. As helper notation, for a run $\rho$
and each variable $\mathsf{x}$, we denote the timestamps of stores of
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads on $\mathsf{x}$ as
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\text{ts}}^{\mathsf{x}}_{0}<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\text{ts}}^{\mathsf{x}}_{1}<\cdots$.

######  Lemma 4.5 (Infinite Supply).

Let $\rho$ be a valid run under the RA semantics, in which the message
$(\mathsf{x},\mathsf{d},\mathsf{vw})$ has been generated by an
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread. Then for each timestamp
${\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}t^{*}}\in\mathbb{N}$,
there exist two timestamp lifting functions $\mathcal{M}_{1}$,
$\mathcal{M}_{2}$ and a run $\rho_{1}$ such that
$\mathcal{M}_{1}(\rho)\triangleright\mathcal{M}_{2}(\rho\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}})\triangleright\rho_{1}$
is a valid run. This run contains a message
$(\mathsf{x},\mathsf{d},\mathsf{vw}^{\prime})$ satisfying (ts comes from
$\rho$)

  1. 1.

$\forall i$
(${\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}t^{*}}\leq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\text{ts}}^{\mathsf{x}}_{i}\land\mathsf{vw}(\mathsf{x})\leq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\text{ts}}^{\mathsf{x}}_{i})\implies\mathsf{vw}^{\prime}(\mathsf{x})\leq\mu_{1}^{\mathsf{x}}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\text{ts}}^{\mathsf{x}}_{i})$

  2. 2.

$\mathsf{vw}^{\prime}(\mathsf{x})\geq\mu_{2}^{\mathsf{x}}({\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}t^{*}})$

  3. 3.

$\forall\mathsf{x}^{\prime}\neq\mathsf{x}$, $\forall i$,
$\mathsf{vw}(\mathsf{x}^{\prime})\leq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\text{ts}}^{\mathsf{x}^{\prime}}_{i}\implies\mathsf{vw}^{\prime}(\mathsf{x}^{\prime})\leq\mu_{1}^{\mathsf{x}^{\prime}}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\text{ts}}^{\mathsf{x}^{\prime}}_{i}})$

######  Proof 4.6.

Without loss of generality, we assume that in the run $\rho$, the timestamps
on each variable are consecutive. If that is not the case, we can always use a
timestamp lowering operation that ‘fills in the gaps’ between non-consecutive
timestamps, while maintaining consecution of the load,store timestamps of
(CAS-local) operations.

We will give a constructive proof. We specify
$\mathcal{M}_{1}(\rho)\triangleright\mathcal{M}(\rho\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}})\triangleright\rho_{1}$
by defining $\mathcal{M}_{1}$, $\mathcal{M}_{2}$ and $\rho_{1}$, and showing
that the resulting run is valid under RA. Then we show how a copy of the
message $(\mathsf{x},\mathsf{d},\mathsf{vw})$ can be obtained as claimed.

First, we describe how to copy runs.

  1. 1.

Copying a run. For a variable $\mathsf{x}$, we define the lifting functions as
follows. With the consecutiveness assumption, the messages on $\mathsf{x}$
have consecutive timestamps and are generated by either
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
or
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$,
which we will denote below as
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}$
and
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}$
respectively. For developing intution quickly, consider the following sequence
of consecutive timestamps on some variable.

${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{0}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{1}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{0}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{2}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{1}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{2}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{3}$

Intuitively, the new interleaved run is obtained by triplicating each
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}$
timestamp into three adjacent timestamps,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}_{a}$,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}_{b}$
and
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}_{c}$.
The
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}_{a}$
timestamps belongs to the lifted run $\mathcal{M}_{1}(\rho)$, the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}_{b}$
timestamp belongs to $\mathcal{M}_{2}(\rho)$ and the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}_{c}$
timestamp belongs to $\rho_{1}$. The $a,b,c$ copies are ordered as $b<c<a$
giving us the following timestamp sequence from the one above.

${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{0}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{1}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{0}_{b}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{0}_{c}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{0}_{a}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{2}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{1}_{b}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{1}_{c}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{1}_{a}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{2}_{b}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{2}_{c}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{2}_{a}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{3}$

We can formalize $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ by counting the
number of
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}$
timestamps smaller than the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{i}$
timestamp, but for ease of presentation, we will keep this implicit. The total
shift can be done for instance, using the function which maps a time stamp
$p\in{\rm Nature}$ corresponding to a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread to the (number of
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads appearing before $p$) + 3(number of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads appearing before $p$)+3, while for a
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
time stamp $p\in\mathbb{N}$, one can map it to (number of
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads appearing before $p$) + 3(number of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads appearing before $p$)+1. So for instance, the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{0}$
at timestamp 3 moves to the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{0}_{a}$
time stamp 5, while the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{3}$
moves to the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{3}$
time stamp 3+ 3(3)+1=13.

$\mathcal{M}_{1}$ maps the timestamp
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{i}$
to the timestamp
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{i}_{a}$
timestamp. Similarly, $\mathcal{M}_{2}$ maps the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{i}$
timestamp to the timestamp
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{i}_{b}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{i}_{a}-2$.
Finally, we have
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{i}_{c}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{i}_{a}-1$.
We call these adjacent timestamps ‘triplets’. Additionally, $\mathcal{M}_{1}$
and $\mathcal{M}_{2}$ map the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{i}$
timestamp to the corresponding
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{i}$
timestamp in the expanded run.

We first note that $\mathcal{M}_{1}$ satisfies the premise of the timestamp
lifting lemma, that for (CAS-local) operations, consecutive load,store
timestamps for CAS remain consecutive. This follows since only
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
can perform (CAS-local) and under $\mathcal{M}_{1}$, consecution is maintained
both for
$({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{i-1},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{i})$
timestamps as well as
$({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}_{a},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{i})$
as depicted in the following timestamp sequence. Thus, by the timestamp
lifting lemma, $\mathcal{M}_{1}(\rho)$ is a valid run under RA.

${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{0}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{1}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.8,0.8}\mathsf{env}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{1,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.8,0.8}\mathsf{env}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{0}_{a}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{2}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.8,0.8}\mathsf{env}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{1,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.8,0.8}\mathsf{env}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{2}_{a}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{1,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.8,0.8}\mathsf{env}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{1,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.8,0.8}\mathsf{env}}{{\color[rgb]{0.8,0.8,0.8}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@stroke{0.8}\pgfsys@color<EMAIL_ADDRESS>\leavevmode\nobreak\
{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{3}_{a}\leavevmode\nobreak\
\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{3}$

  2. 2.

The first superposition gives a valid run. We now claim that the run
$\mathcal{M}_{1}(\rho)\triangleright\mathcal{M}_{2}(\rho\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}})$
is a valid run under RA. For a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread $\mathsf{t}$ in $\rho$ we denote by $\mathsf{copyB}(\mathsf{t})$ as its
‘copy’ ($\mathsf{TID}$ distinguished apart) in
$\mathcal{M}_{2}(\rho\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}})$
($\mathsf{B}$ since it occupies the $b$ timestamps). We will show that
$\mathsf{copyB}(\mathsf{t})$ copies the transitions that $\mathsf{t}$ took. We
use the following invariant relating the view $\mathsf{vw}_{1}$ of thread
$\mathsf{t}$ in $\rho$ with the view $\mathsf{vw}_{2}$ of
$\mathsf{copyB}(\mathsf{t})$ for showing this. Let $\mathsf{TS}(t)$ denote the
set of timestamps used by thread $t$ in a run $\rho$.

> For every shared variable $\mathsf{x}$, if
> $\mathsf{vw}_{1}(\mathsf{x})\in\mathsf{TS}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$,
> then $\mathsf{vw}_{2}(\mathsf{x})=\mathsf{vw}_{1}(\mathsf{x})-2$, else if
> $\mathsf{vw}_{1}(\mathsf{x})\in\mathsf{TS}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}})$
> then $\mathsf{vw}_{2}(\mathsf{x})=\mathsf{vw}_{1}(\mathsf{x})$

Now we can reason by induction on the length of the run that whenever
$\mathsf{t}$ takes a transition in $\rho$, $\mathsf{copyB}(\mathsf{t})$ can
replicate it but with the view as given by the above invariant. More
precisely, whenever a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread $\mathsf{t}$ makes a store with timestamp
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}$,
$\mathsf{copyB}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$
will make a store with timestamp
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}-2$.
Similarly, when a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread $\mathsf{t}$ makes a load,

    1. (a)

if the load is from a message by a
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
thread,
$\mathsf{copyB}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$
also loads from the same message

    2. (b)

if the load is from a message by some
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread $\mathsf{t}^{\prime}$ in $\rho$,
$\mathsf{copyB}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$
loads from $\mathsf{copyB}(\mathsf{t}^{\prime})$

It is easy to check that the view invariant is maintained through this
simulation. Crucially we have
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{i}_{a}<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{j}\iff{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}^{i}_{b}<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}\mathsf{T}^{j}$.
Thus $\mathsf{t}$ and $\mathsf{copyB}(\mathsf{t})$ can always read the same
set of
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
messages. Thus we have that
$\mathcal{M}_{1}(\rho)\triangleright\mathcal{M}_{2}(\rho\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}})$
is valid under RA. Now we focus on message generation by $\rho_{1}$.
Intuitively, $\rho_{1}$ will also be a copy of $\rho$ but will occupy the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}\mathsf{T}_{c}$
timestamps.

  3. 3.

Generating a copy of the message. Now we will describe how we can use
$\rho_{1}$ to generate the message
$(\mathsf{x},\mathsf{d},\mathsf{vw}^{\prime})$. Let $\rho_{p}$ be the prefix
of $\rho$ just (one transition) before the message
$(\mathsf{x},\mathsf{d},\mathsf{vw})$ is generated. We generate the run
$\rho^{\prime}$ by copying the
$\rho_{p}\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}$
using the $c$-timestamps. The run obtained is
$\mathcal{M}_{1}(\rho)\triangleright\mathcal{M}_{2}(\rho\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}})\triangleright\rho^{\prime}$.
Using similar reasoning as earlier, we can show that this is a valid run under
the RA semantics.

Now let
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread $\mathsf{t}$ be the thread which generates the message
$(\mathsf{x},\mathsf{d},\mathsf{vw})$ in $\rho$. Then there is a copy of
$\mathsf{t}$, thread $\mathsf{copyC}(\mathsf{t})$ in $\rho^{\prime}$, that is
now in a control state enabling it to generate a message on variable
$\mathsf{x}$ with value $\mathsf{d}$ (since the transitions have been
replicated exactly across
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
and
$\mathsf{copyC}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$).
Now we need to reason about the view of the message generated by
$\mathsf{copyC}(\mathsf{t})$. If the view of $\mathsf{t}$ is $\mathsf{vw}_{a}$
and that of $\mathsf{copyC}(\mathsf{t})$ is $\mathsf{vw}_{c}$ we have the
following, which again follows from the invariant mentioned above.

> For each variable $\mathsf{x}^{\prime}$, if
> $\mathsf{vw}_{a}(\mathsf{x}^{\prime})\in\mathsf{TS}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$,
> then
> $\mathsf{vw}_{c}(\mathsf{x}^{\prime})=\mathsf{vw}_{a}(\mathsf{x}^{\prime})-1$,
> else if
> $\mathsf{vw}_{a}(\mathsf{x}^{\prime})\in\mathsf{TS}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}})$
> then
> $\mathsf{vw}_{c}(\mathsf{x}^{\prime})=\mathsf{vw}_{a}(\mathsf{x}^{\prime})$

Observe how this satisfies the condition (3) in the lemma immediately since in
both cases above, we have
$\mathsf{vw}_{c}(\mathsf{x}^{\prime})\leq\mathsf{vw}_{a}(\mathsf{x}^{\prime})$.
Now the thread $\mathsf{copyC}(\mathsf{t})$ will choose the timestamp for
variable $\mathsf{x}$, $\mathsf{vw}^{\prime}(\mathsf{x})$. Assume
$t^{*}\in{\rm Nature}$ has been given. We have two cases, (i)
$t^{*}\leq\mathsf{vw}(\mathsf{x})$ and (ii) $t^{*}>\mathsf{vw}(\mathsf{x})$.

    1. (i)

In this case there is nothing to prove as the original message is lifted to
$(\mathsf{x},\mathsf{d},\mathsf{vw}^{\prime})$ where
$\mathsf{vw}^{\prime}(\mathsf{x})=\mu_{1}^{\mathsf{x}}(t^{*})$ which satisfies
both conditions (1) and (2).

    2. (ii)

We choose $\mathsf{vw}^{\prime}(\mathsf{x})=\mu_{2}^{\mathsf{x}}(t^{*})+1$,
which satisfies (2). Note that this timestamp is higher than
$\mathsf{vw}_{c}(\mathsf{x})$ since
$\mu_{2}^{\mathsf{x}}(t^{*})\geq\mu_{1}^{\mathsf{x}}(\mathsf{vw}(\mathsf{x}))=\mathsf{vw}_{a}(\mathsf{x})>\mathsf{vw}_{c}(\mathsf{x})$.
We have
$\mathsf{vw}^{\prime}(\mathsf{x})=\mu_{2}^{\mathsf{x}}(t^{*})+1=\mu_{1}^{\mathsf{x}}(t^{*})-1$
due to the construction of $\mathcal{M}_{1},\mathcal{M}_{2},\rho_{1}$.
Additionally,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\text{ts}}^{\mathsf{x}}_{i}\geq
t^{*}\implies\mu_{1}^{\mathsf{x}}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\text{ts}}^{\mathsf{x}}_{i})\geq\mu_{1}^{\mathsf{x}}(t^{*})>\mathsf{vw}^{\prime}(\mathsf{x})$
satisfiying condition (1). In this case $\rho_{1}$ is defined as
$\rho^{\prime}$ extended by the store transition generating the message. Note
that since it is a $c$-type message, the timestamp is available.

Thus in both cases, we have a message
$(\mathsf{x},\mathsf{d},\mathsf{vw}^{\prime})$ with $\mathsf{vw}^{\prime}$
satisfying the required conditions. This proves the theorem.

To sum up, we interpret the infinite supply as this: $\mathcal{M}_{1}(\rho)$
is the lifted run with holes.
$\mathcal{M}_{2}(\rho\\!\downarrow_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}})$
is the
$\mathsf{copy}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}})$
run and $\rho_{1}$ is obtained by running another copy that generates the new
message. We note that run triplication is not strictly necessary for message
duplication, but makes the proof easier. We note, points (1) and (3) above
refer to relative ordering between
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
timestamps and (2) refers to the new message with an arbitrarily high
timestamp.

###  4.2 Abstracting the Timestamps

We introduce the _timestamp abstraction_ , which is a building block for the
simplified semantics. Let us call a message $\mathsf{msg}$ an
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$)
message if it is generated by a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$)
thread. With the intuition that
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
messages can be replicated with arbitrarily high timestamps, while
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
or initial messages cannot be, we distinguish the write timestamps of the two
types of messages.

Timestamp Abstraction. If a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
thread has read a message $(\mathsf{x},d,\mathsf{vw})$ from a
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
thread with a timestamp $\mathsf{ts}=\mathsf{vw}(\mathsf{x})$ and has
generated a message $\mathsf{msg}$ on $\mathsf{x}$, then copies of
$\mathsf{msg}$ are available with arbitrarily high timestamps at least as high
as $\mathsf{ts}$. To capture this in our abstraction, we assign the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
message $\mathsf{msg}$, a timestamp $\mathsf{ts}^{\textbf{+}}$ that is by
definition, larger than $\mathsf{ts}$.

We define the set of timestamps in the simplified semantics as ${\rm
Nature}\uplus{\rm Nature}^{\textbf{+}}$, where ${\rm Nature}^{\textbf{+}}$
contains for each $\mathsf{ts}\in{\rm Nature}$, a timestamp
$\mathsf{ts}^{\textbf{+}}$. The timestamps are equipped with the order
$\preceq$ in which $\mathsf{ts}^{\textbf{+}}$ is greater than $\mathsf{ts}$
and smaller than $\mathsf{ts}+1$:

$0\prec 0^{\textbf{+}}\prec 1\prec 1^{\textbf{+}}\prec\ldots$

Timestamps of form $\mathsf{ts}\in\mathbb{N}$ are used for the stores of
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads while those of form $\mathsf{ts}^{\textbf{+}}$ are used for stores of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads. We allow multiple stores with the same timestamp of form
$\mathsf{ts}^{\textbf{+}}$, while allowing at most one store for timestamps of
form $\mathsf{ts}$. This abstracts timestamps of multiple
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
messages between two
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
messages by a single $\mathsf{ts}^{\textbf{+}}$ timestamp. Initial messages
have timestamp 0 as usual.

We utilize this timestamp abstraction by defining a simplified semantics; note
that this simplification is not per se a simpler formulation but rather is
simple in the sense that it will pave the way for efficient verification
procedures (as detailed in Section 5, Section 6). We then show that a run
$\rho$ in the classical RA semantics has an equivalent run in the simplified
semantics where the timestamps are transformed according to some timestamp
transformation $\mathcal{M}$ as defined above. We show that reachability
across the two semantics is preserved since both order and consecution between
timestamps is maintained.

RA semantics, simplified. As in the classical RA semantics, the transition
rules of the simplified semantics will require us to increase timestamps (upon
writing messages). We define the function $\mathsf{raise}(-)$ on ${\rm
Nature}\uplus{\rm Nature}^{\textbf{+}}$ by

$\displaystyle\mathsf{raise}(\mathsf{ts})=\mathsf{raise}(\mathsf{ts}^{\textbf{+}})=\mathsf{ts}^{\textbf{+}},\mathsf{ts}\in{\rm
Nature}.$

The definition of the simplified semantics replaces the domain
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{Time}}$
by $\mathbb{P}={\rm Nature}\uplus{\rm Nature}^{\textbf{+}}$. We use the term
_abstract_ to refer to the resulting views, messages, memory, local
configurations, and configurations and use a superscript
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{d}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}}$
(shortened
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}/{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$)
to indicate that an element is abstract. So an abstract view is a function,
$\mathsf{vw}^{{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{d}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{e}}}}$
that maps shared variables to $\mathbb{P}$. We now specify the transitions in
the abstract semantics. Owing to their different nature (one is replicatable,
the other is not) the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
and
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads will have different transition rules in the simplified semantics.

For storing a value, the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads use a rule (ST-localenv) that coincides with rule (ST-local) from the
RA semantics (Figure 1) except that it replaces relation $<_{\mathsf{x}}$ by
$<^{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}_{\mathsf{x}}$
defined as follows:

$\displaystyle\mathsf{vw}_{1}<^{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}_{\mathsf{x}}\mathsf{vw}_{2}\quad\text{iff}\leavevmode\nobreak\
\begin{cases}\mathsf{raise}(\mathsf{vw}_{1}(\mathsf{x}))\preceq\mathsf{vw}_{2}(\mathsf{x})\in\mathbb{N}^{+}&\\\
\mathsf{vw}_{1}(\mathsf{y})=\mathsf{vw}_{2}(\mathsf{y})\qquad\text{ for
}\mathsf{y}\neq\mathsf{x}.\end{cases}$

Additionally, for stores of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads, we no longer require the timestamp of the message to be unused. So we
disregard the $\mathsf{msg}\\#\mathsf{m}$ check in the global (ST-global) rule
(note crucially this is for
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
only). The
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
threads use (ST-local) from the RA semantics without modifications, and hence
choose a timestamp in ${\rm Nature}$, not a raised value.

For load instructions, we distinguish between messages generated by
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
and
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads. This is a natural consequence of the different nature of timestamps,
$\mathsf{ts}$ for
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
and $\mathsf{ts}^{\textbf{+}}$ for
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
messages. For loading a
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
message, we use rule (LD-local) (Figure 1) from the RA semantics without
changes.

For loading from
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads, we introduce a new rule (LD-localenv). It is defined by replacing
$\sqcup$ in (LD-local) by
$\sqcup^{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}_{x}$.
We drop the check on the order of timestamps (overwrite it by true); a
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
message may always be read, independent of the reading thread’s view. The join
is dependent on the variable being read from, $\mathsf{x}$. To define
$\mathsf{vw}_{1}\sqcup^{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}_{\mathsf{x}}\mathsf{vw}_{2}$,
let $\mathsf{vw}_{1}$ be the view of the thread thread loading the message and
$\mathsf{vw}_{2}$ be the view in the message.

$\displaystyle\mathsf{vw}_{1}\sqcup^{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}_{\mathsf{x}}\mathsf{vw}_{2}=(\mathsf{vw}_{1}[\mathsf{x}\mapsto\mathsf{raise}(\mathsf{vw}_{1}(\mathsf{x}))])\sqcup\mathsf{vw}_{2}$

Thus, if $\mathsf{vw}_{1}(\mathsf{x})=4$ and
$\mathsf{vw}_{2}(\mathsf{x})=2^{+}$, then
$(\mathsf{vw}_{1}\sqcup_{\mathsf{x}}^{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}}\mathsf{vw}_{2})(\mathsf{x})=4^{+}$.
The update to $\mathsf{raise}(\mathsf{vw}_{1}(\mathsf{x}))$ ensures that if it
the timestamp on $\mathsf{x}$ was $\mathsf{ts}$, it is at least
$\mathsf{ts}^{\textbf{+}}$, and hence it cannot read a
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$)
message with timestamp $\mathsf{ts}$ again. We note that the above join
operation is not commutative.

Now we consider the atomic operation - (CAS-local) \- which can only be
performed by
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$.
We have two cases depending on whether (CAS-local) loads from a
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
or
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
message. If it is the latter, then the transition is identical to ((LD-
localenv); (ST-local)) with the additional condition that the load and store
timestamps must be $\mathsf{ts}^{\textbf{+}}$ and $\mathsf{ts}+1$ for some
$\mathsf{ts}$.

If it is the former (load from
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$)
then the load and store timestamps must be $\mathsf{ts}$ and $\mathsf{ts}+1$.
Consequently, there cannot be any messages with timestamp
$\mathsf{ts}^{\textbf{+}}$. Conversely, if there is (atleast one) message with
timestamp $\mathsf{ts}^{\textbf{+}}$, then the (CAS-local) operation with load
and store timestamps $\mathsf{ts}$ and $\mathsf{ts}+1$ is forbidden. We keep
track of such ‘blocked’ intervals $(\mathsf{ts},\mathsf{ts}+1)$ by adding a
set $\mathsf{B}$ to the global state in the simplified semantics. The global
and local transition relations of the full simplified semantics are in Figure
6, 7.

We formally proof equivalence w.r.t. reachability of the simplified semantics
with the original RA semantics. But before that, we give an example to
illustrate timestamp abstraction in the simplified semantics.

$q_{0}$$q_{2}$$q_{0}$$q_{1}$$q_{2}$$q_{1}$$\partial_{1}$$\partial_{2}$$\partial_{5}$$\partial_{3}$$\partial_{4}$Program
$\mathsf{c}_{i}$Program
$\mathsf{c}_{j}$$q_{\mathsf{end}}$$q_{\mathsf{end}}$$q_{\mathsf{start}}$$q_{\mathsf{start}}$Transformed
program $\mathsf{c}^{\prime}_{j}$Transformed program
$\mathsf{c}^{\prime}_{i}$$\iota(\partial_{1})$$\iota(\partial_{2})$$\iota(\partial_{3})$$\iota(\partial_{4})$$\iota(\partial_{5})$register
loadsregister loadsregister storesregister
stores$\mathsf{cas}(t_{i},0,\Lambda^{\bot})$$\mathsf{cas}(t_{i},1,\Lambda^{\bot})$$\mathsf{cas}(t_{i},\Lambda^{\bot},2)$$\mathsf{cas}(t_{i},\Lambda^{\bot},1)$$\mathsf{cas}(t_{j},\Lambda^{\bot},1)$$\mathsf{cas}(t_{j},\Lambda^{\bot},1)$$\mathsf{cas}(t_{j},0,\Lambda^{\bot})$$\mathsf{cas}(t_{j},2,\Lambda^{\bot})$$\mathsf{cas}(t_{j},1,\Lambda^{\bot})$$\mathsf{cas}(t_{j},\Lambda^{\bot},2)$$\begin{array}[]{c}\text{Variables
}\mathsf{x}\text{ and }\mathsf{y}\text{ have been initialized to 0}\\\
\begin{array}[]{l|l}\hline\cr\mathsf{producer}&\mathsf{consumer}\\\
\hline\cr\lambda_{1}:\leavevmode\nobreak\ \mathsf{r}_{1}
\coloneqq\mathsf{y}&\lambda^{\prime}_{1}:\leavevmode\nobreak\ \mathsf{y}
\coloneqq 1\\\ \lambda_{2}:\leavevmode\nobreak\
\texttt{if}(\mathsf{r}_{1}==1):&\lambda^{\prime}_{2}:\leavevmode\nobreak\
\texttt{for i in {1..z}}:\\\ \lambda_{3}:\leavevmode\nobreak\ \qquad\mathsf{x}
\coloneqq 1\oplus\quad\quad\cdots\oplus\mathsf{x} \coloneqq
l&\lambda^{\prime}_{3}:\leavevmode\nobreak\ \quad\quad\mathsf{r}^{\prime}_{1}
\coloneqq\mathsf{x}\\\ &\lambda^{\prime}_{4}:\leavevmode\nobreak\
\quad\quad\mathsf{assume}\;{\mathsf{r}^{\prime}_{1}=\texttt{(i \%\% l)+1}}\\\
\hline\cr\end{array}\end{array}$

Figure 4: Above is a (non-parameterized) producer-consumer program, and below
is a sample execution snippet with threads $t_{1}$ and $t_{2}$ playing the
roles of producer and consumer respectively. Figure 5: Execution under the
simplified semantics.
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{producer}}$
transitions and messages in red,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{consumer}}$
transitions and messages in blue. The execution begins with the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{consumer}}$
thread generating a message on $\mathsf{y}$ with value 1 and timestamp 1
leading to the memory $\mathsf{m}_{\lambda^{\prime}_{1}}$. The
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{producer}}$
threads executing $\lambda_{1}^{1\dots l}$ read from this message and reach
states $\lambda_{2}^{1\dots l}$. They generate messages on $\mathsf{x}$ with
values $\\{1,\dots,l\\}$ shown in memory $\mathsf{m}_{\lambda_{3}}$. These are
then read by the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{consumer}}$
as it loops around $\lambda^{\prime}_{3}$, $\lambda^{\prime}_{4}$ for
different iterates i, (i=1, i=2, i>2) as shown along the transition edge.

Simplified Semantics, on an Example. In Figure 5 we give an example of a
computation under the simplified semantics by parameterizing the program from
Figure 4. The parameterized program has a single distinguished
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}$
thread which runs the program
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{consumer}}$,
and arbitrarily many
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads which run
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{producer}}$.
We consider a computation in which
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}_{1}$,
and $l$ (out of the unboundedly many)
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads participate. We label different instances of the
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads (and their instruction labels) by superscripts from $\\{1,\dots,l\\}$
(eg., $\lambda_{1}^{1},\dots\lambda_{1}^{l}$ for $\lambda_{1}$).

The
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{consumer}}$
generates write timestamps of the form $\mathsf{ts}$ (1 in example), while
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{producer}}$
threads have write timestamps of the form
$\mathsf{ts}_{1}^{+},\dots,\mathsf{ts}_{l}^{+}$. While the timestamp 1 is now
occupied, there can be several writes with timestamps of the form
$\mathsf{ts}^{+}$, (in particular some $\mathsf{ts}_{i}^{+}$ may be equal).
Additionally, when reading from these
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{producer}}$
generated messages,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{consumer}}$
does not perform any timestamp checks, rather simply updates its view by
taking joins. Hence we point out that the load with value 2 during the second
loop iteration (i=2), is feasible even if
$\mathsf{ts}_{2}^{+}<\mathsf{ts}_{1}^{+}$; unlike the classical RA semantics.
In this example, the
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{dis}}$
thread, after looping around $l$ times and reading from
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
messages, has the view on $\mathsf{x}$ as $\max\\{\mathsf{ts}_{i}^{+}\\}$. Due
to the lack of timestamp comparisons,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{consumer}}$
can perform the loop arbitrarily many times ($\mathsf{z}>l$ times), moreover,
the number of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
threads needed is independent of z. We see that this relieves the burden of
timestamp comparisons, for
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{env}}$
messages.