Algorithm 1 and Lemma D.2 for Algorithms 2 and 3. We use the statement
${\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}w_{i}\sqsubset\trianglelefteqslant\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$,
instead of potentially another statement involving
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{off}}}$
(as Jayanti’s original statement does), because it makes the forwarding
signature export fewer rep events, thus making it a bit more parsimonious.

  * •

${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\vartriangleleft{\sigma}{\mathit{a}_{i}}}$
states that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
wrote to $\mathtt{A}[i]$ before
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{a}_{i}}}$
read from it, which directly corresponds to the negation of Statement (i).

For Principle (2a), we need to further deviate from Jayanti’s original
formulation, since the latter is too specific to Algorithm 1, and does not
scale as-is to the multi-writer algorithms. The point of this principle is to
ensure that a writer may only forward values that are, intuitively, “current”.
The principle itself ensures this property, but only in the single-writer case
of Algorithm 1. Indeed, in Algorithm 1, a writer only forwards its own value
(and other writes to the same pointer are prohibited by assumption);
therefore, if a write is concurrent to the scan, then it can only forward a
value that is current. But in a multi-writer case, as we shall see in Section
4, we want to allow a writer to forward values of other writers. In
particular, a writer that writes and then stalls indefinitely could still be
forwarded by another write to some concurrent scan. But we still need to
ensure that the forwarded write is not arbitrarily old. We do so by insisting
that a write
${\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}w_{i}}$
forwarded to
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
cannot occur before a write
${\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}w^{\prime}_{i}}$
which wrote to $\mathtt{A}[i]$ with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
before
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
started, i.e., executed
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{r}_{i}}}$.
In other words, we require that the forwarded write
${\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}w_{i}}$
does not “happen before” any write
${\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}w^{\prime}_{i}}$
that started before the start of the scan. A write
${\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}w^{\prime}_{i}}$
has a _newer_ value, so its existence should prevent
${\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}w_{i}}$
from being forwarded. We formalize this as Fig. 7.

$\forall{\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}w_{i}},{\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}w^{\prime}_{i}},{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}.$ | ${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{fwd}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}\land{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\vartriangleleft{\sigma}{\mathit{r}_{i}}}$ | ${}\implies{\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}w_{i}\not\vartriangleleft w^{\prime}_{i}}$ | (7 revisited)
---|---|---|---

This captures that writers must forward to scan
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
either the latest write that wrote to $\mathtt{A}[i]$ before
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{r}_{i}}}$,
or some write that occurred after
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{r}_{i}}}$,
thus ensuring that the forwarded write is current.

Lastly, Fig. 7 relates to the contrapositive of Principle (2b).

$\forall{\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}w_{i}},{\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}w^{\prime}_{i}},{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}.$ | ${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{fwd}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}\land{\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}w^{\prime}_{i}\sqsubset\trianglelefteqslant\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$ | ${}\implies{\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}w_{i}\not\vartriangleleft w^{\prime}_{i}}$ | (7 revisited)
---|---|---|---

Again,
${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{fwd}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$
directly corresponds to Statement (iv). Formal statement
${\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}w^{\prime}_{i}\sqsubset\trianglelefteqslant\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$
corresponds to the negation of Statement (vii), for the same reason as in Fig.
7, since (ii) is the negation of (vii). Finally,
${\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}w_{i}\not\vartriangleleft
w^{\prime}_{i}}$ directly corresponds to the negation of (vi), with the
exception that we use $\vartriangleleft$ instead of Jayanti’s “executed after”
to relate the writes
${\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}w_{i}}$
and
${\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}w^{\prime}_{i}}$.
The two correspond in the single-writer case, but our statement extends to the
multi-writer case as well.

Algorithm 1 satisfies this set of properties of the $\mathsf{Forwarding}$
signature, and they are sufficient to prove that an algorithm is a snapshot
algorithm according to the $\mathsf{Snapshot}$ signature, which is in turn
sufficient to prove linearizability. In Section 3 we sketch why these claims
holds, and in Section 4 we sketch how Algorithms 2 and 3 satisfy the
$\mathsf{Forwarding}$ signature. The complete proofs are available in the
appendix.

##  3\. Proof Sketches for Algorithm 1

We now sketch the proofs of our signatures implying linearizability, to
illustrate the gist of reasoning by visibility. We begin by showing how
histories that satisfy the $\mathsf{Snapshot}$ signature are linearizable.
This proof is based on a similar proof by Chakraborty et al. (2015) for
queues.

######  Lemma 2.3 0.

Histories satisfying $\mathsf{Snapshot}$ signature (Fig. 5) are linearizable.

###### Proof sketch.

Following Definition 2.2 of linearizability, we start by choosing a visibility
relation
${\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}\prec}$
that constructs the set
${\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}E_{c}}=\\{{\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}e}\mid\exists{\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}e^{\prime}}\in\mathcal{T}({\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}E}).\
{\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}e\prec^{*}e^{\prime}}\\}$,
and then extend it to a linearization
${\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}<}$.
Let
${\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}\prec}$
be the visibility relation obtained by restricting the visibility relation
postulated by $\mathsf{Snapshot}$ to
$\mathcal{T}({\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}S})\cup\bigcup_{i}{\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}\mathbb{W}_{i}}$.
Events outside of the restriction are non-terminated scans or writes that have
not executed their effect yet; they do not modify the abstract state, and are
hence not necessary for linearization. Additionally, by Fig. 5 we know that
every terminated write is effectful. Thus going forward, we consider
${\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}E_{c}}=\mathcal{T}({\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}S})\cup\bigcup_{i}{\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}\mathbb{W}_{i}}$.

We next extend the happens-before order
${\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}\vartriangleleft}$
on the selected set of events as follows. The idea is to keep extending this
order with more relations between the events of the selected set until we
reach a total order, which will be the desired linearization order. We first
induce a helper order

${\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}\vartriangleleft_{w}}\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}({\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}\vartriangleleft}\
\cup\
{\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}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{wrDiff}}$}}}$}}}})^{+}$

which ranges over writes (into different cells), where
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>holds if $i\neq j$ and there exists a write
${\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}w_{j}}$
and a scan
${\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}s}$
such that
${\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}w_{i},w_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s}$
and
${\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}w_{j}\vartriangleleft
w^{\prime}_{j}}$. Or, in English, we order
${\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}w_{i}}$
before
${\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}w^{\prime}_{j}}$,
if
${\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}w_{i}}$
is observed by some scan along with
${\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}w_{j}}$,
and
${\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}w_{j}}$
is ordered before
${\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}w^{\prime}_{j}}$.
The
${\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}\vartriangleleft_{w}}$
order is a (strict) partial order by Figs. 5, 5, 5, 5 and 5 (see Lemma A.2 for
the complete proof).

Next, we select an arbitrary total order
${\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}<_{w}}$
over writes that extends
${\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}\vartriangleleft_{w}}$.
Since the set of selected events is finite, such a total order always exists
by Zorn’s Lemma. We use the order
${\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}<_{w}}$
to determine which event we will consider as being last in the eventually
constructed linearization order. We say that a write is latest-in-time if it
is the greatest in
${\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}<_{w}}$,
while a scan is latest-in-time if it is maximal in
${\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}\vartriangleleft}$
and all the writes that it observes are the greatest in
${\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}<_{w}}$
for their respective memory cell. As long as the set of events is non-empty,
there will exist a latest-in-time event under this definition by Figs. 5, 5, 5
and 5 (see Lemma A.4 for the complete proof). By inductively selecting the
latest-in-time event, we construct a total order of events that is consistent
with
${\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}\vartriangleleft}$
and snapshot semantics, and is thus a linearization order. More concretely, we
add the latest-in-time event to the end of the linearization order, forming a
chain with previously added events, and repeat this step with the set of
events excluding the last selected. ∎

Next, we show that histories satisfying the $\mathsf{Forwarding}$ signature
also satisfy the $\mathsf{Snapshot}$ signature. Because some
$\mathsf{Forwarding}$ properties use rep events, to be able to efficiently use
them, we first need a lemma that turns a
${\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}\vartriangleleft}$
relation between virtual or abs events into a
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\vartriangleleft}$
relation between rep events. The lemma will also be useful in showing that
Algorithm 1 (and Algorithms 2 and 3 in Section 4) satisfy the
$\mathsf{Forwarding}$ signature, once Figs. 7 and 7 have been proven.

###### Lemma 3.1 (Happens-before of subevents).

Assume Figs. 7 and 7. For events
${\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}e},{\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}e^{\prime}}\in\bigcup_{i}{\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}W_{i}}\cup{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\Sigma}$
of the $\mathsf{Forwarding}$ signature (Fig. 7) where
${\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}e^{\prime}}$
is populated with at least one rep event from its event structure (Fig. 6), if
${\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}e\vartriangleleft
e^{\prime}}$ holds (where
${\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}\vartriangleleft}$
follows the definition from Fig. 7) then there exists
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e^{\prime}_{r}}$
where
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}\vartriangleleft
e^{\prime}_{r}}$ holds, with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e^{\prime}_{r}}$
belonging to
${\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}e}$
and
${\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}e^{\prime}}$
respectively.

###### Proof.

We can view
${\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}e\vartriangleleft
e^{\prime}}$ as a chain of
${\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}\vartriangleleft_{1}}$
relations connecting
${\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}e}$
and
${\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}e^{\prime}}$;
that is,
${\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}e\vartriangleleft_{1}\cdots\vartriangleleft_{1}e^{\prime}}$,
where by definition
${\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}\vartriangleleft_{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}\sqsubset}\cup{\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}\prec})=({\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}\sqsubset}\cup{\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}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{wr}}$}}}$}}}}\cup{\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}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}})$.
It is easy to see that each abs event in this chain is populated with a rep
event. Indeed, if an abs event’s relation
${\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}\vartriangleleft_{1}}$
to its successor is realized by
${\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}\sqsubset}$,
then the event is terminated and all of its rep events are executed (and by
our axioms, each abs event must have at least one rep event). Alternatively,
if the abs event’s relation
${\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}\vartriangleleft_{1}}$
to its successor is realized by
${\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}\prec}$,
then the event must be populated as per the definitions of reads-from and
writing visibility in Fig. 7, and in the
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>case by Fig. 7. This leaves out
${\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}e^{\prime}}$,
which has no successor, but
${\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}e^{\prime}}$
is populated by assumption.

Now the proof is by induction on the length of the above chain. The base case
is when
${\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}e\vartriangleleft_{1}e^{\prime}}$.
If
${\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}e\sqsubset
e^{\prime}}$, the proof is by Eq. RB.2 giving us
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}\sqsubset
e^{\prime}_{r}}$ for arbitrary
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e^{\prime}_{r}}$
belonging to
${\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}e}$
and
${\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}e^{\prime}}$
respectively. If
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>the proof is by the definition of
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>in Fig. 7, giving us
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\vartriangleleft{w^{\prime}_{i}}{\mathit{a}}}$
with
${\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}e}={\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}w_{i}}$
and
${\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}e^{\prime}}={\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}w^{\prime}_{i}}$.
For the last case,
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>we have
${\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}e}={\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}w_{i}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}}={\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}e^{\prime}}$
with either
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma^{\prime}}{\mathit{a}_{i}}}$
or
${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{fwd}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}}}$.
The former case directly exhibits rep events that satisfy our goal. The latter
does so as well, since by Fig. 7, it must be
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\vartriangleleft{\sigma^{\prime}}{\mathit{b}_{i}}}$.
The inductive step is similar, with the addition that we need transitivity of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\vartriangleleft}$
and Fig. 7 to join events. ∎

###### Lemma 3.2.

Histories satisfying $\mathsf{Forwarding}$ signature (Fig. 7) also satisfy
$\mathsf{Snapshot}$ signature.

###### Proof sketch.

We start by determining the instantiations of
${\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}\mathbb{W}_{i}}$,
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
${\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}\prec}$
for the $\mathsf{Snapshot}$ signature. Since the effect of
${\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}w_{i}}$
is observable only after the execution of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$,
we let
${\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}w_{i}}\in{\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}\mathbb{W}_{i}}$
iff
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
is defined. For the other notions, we first define a helper visibility over
scans
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>which we use to define
${\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}\prec}$.
The highlighted relations
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>originate from the $\mathsf{Forwarding}$ signature.

$\displaystyle{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}{\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\hbox{\pagecolor{lightergray}$\displaystyle\scriptstyle\mathbf{rf}$}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\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}s}^{\bullet}}}$
$\displaystyle{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\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}s}^{\bullet}}\sqsubset{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\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}s^{\prime}}^{\bullet}}}$
$\displaystyle{\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}\prec}$
$\displaystyle\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}{\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}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}}\cup{\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}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\hbox{\pagecolor{lightergray}$\displaystyle\scriptstyle\mathbf{wr}$}}$}}}$}}}}\cup{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
Eq. V.1 holds since if
${\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}e\prec^{+}e^{\prime}}$
and
${\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}e^{\prime}\sqsubseteq
e}$, then we can construct a
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\vartriangleleft}$-cycle
of rep events with Lemma 3.1, contradicting irreflexivity of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\vartriangleleft}$
(Lemma 2.1). Fig. 5 holds directly by Fig. 7. Fig. 5 holds because by the
definition of
${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\hbox{\pagecolor{lightergray}$\displaystyle\scriptstyle\mathbf{rf}$}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$
in $\mathsf{Forwarding}$ signature, it is either
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}{\mathit{a}_{i}}}$
for which Fig. 3 ensures uniqueness, or
${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{fwd}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$
where Fig. 7 ensures uniqueness. Fig. 5 of total ordering on effectful writes
follows because in $\mathsf{Forwarding}$ signature,
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is defined as
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\vartriangleleft{w^{\prime}_{i}}{\mathit{a}}}$,
and the rep writes are totally ordered by Fig. 3. Fig. 5 that all terminated
writes are effectful holds because for every terminated write
${\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}w_{i}}$
we must have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
defined.

We next prove Fig. 5. We sketch the proof by assuming there is a write
${\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}w^{\prime}_{i}}$
such that
${\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}w_{i}\vartriangleleft
w^{\prime}_{i}\vartriangleleft s}$ where
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and then deriving a contradiction. Unfolding the definition of
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>in
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>we get
${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\hbox{\pagecolor{lightergray}$\displaystyle\scriptstyle\mathbf{rf}$}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$
where
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\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}s}^{\bullet}}$.
Also, from
${\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}w^{\prime}_{i}\vartriangleleft
s}$, using Fig. 7, it turns out that
${\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}w^{\prime}_{i}\vartriangleleft{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$,
and moreover, the latter splits into two possible cases:
${\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}w^{\prime}_{i}\sqsubset\trianglelefteqslant\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\vartriangleleft{\sigma}{\mathit{r}_{i}}}$.
The full proof of how the cases follow from the premise and that they exhaust
the possibilities is given in Appendix B. Note that the proposition
${\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}w^{\prime}_{i}\sqsubset\trianglelefteqslant\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$
is the key part of Figs. 7 and 7, while
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\vartriangleleft{\sigma}{\mathit{r}_{i}}}$
is the key part of Fig. 7; in fact, this exhaustion of cases of
${\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}w^{\prime}_{i}\vartriangleleft{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$
is what let us rediscover and mathematically formulate the forwarding
principles. The proof now proceeds by analyzing
${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\hbox{\pagecolor{lightergray}$\displaystyle\scriptstyle\mathbf{rf}$}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$.
From the definition of reads-from visibility in Fig. 7, we also get two cases:
$({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}{\mathit{a}_{i}}}\land{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{r}_{i}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}{\mathit{b}_{i}}})$
and
${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{fwd}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$,
for a total of four cases when combined with the above. In each case,
contradiction follows easily, relying in different cases on a different subset
of Figs. 7, 7, 7 and 3.

Finally, we prove Fig. 5; that is,
${\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}w_{i},w_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s}$
and
${\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}w^{\prime}_{i},w^{\prime}_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s^{\prime}}$
with
${\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}w_{i}\vartriangleleft
w^{\prime}_{i}}$ and
${\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}w^{\prime}_{j}\vartriangleleft
w_{j}}$ lead to contradiction. As before, we first transform the assumptions
${\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}w_{i},w_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s}$
and
${\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}w^{\prime}_{i},w^{\prime}_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s^{\prime}}$
into
${\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}w_{i},w_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$
and
${\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}w^{\prime}_{i},w^{\prime}_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}}}$,
where
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\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}s}^{\bullet}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\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}s^{\prime}}^{\bullet}}$.
Next, by property Fig. 7, the virtual scans are totally ordered by
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sqsubset}$,
thus either
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma\sqsubset\sigma^{\prime}}$
or
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}\sqsubset\sigma}$
(the case when
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}}$
contradicts reads-from uniqueness Fig. 5). In the first case (the second is
symmetric), we have
${\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}w^{\prime}_{j}\vartriangleleft
w_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma\sqsubset\sigma^{\prime}}}$,
and thus also
${\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}w^{\prime}_{j}\vartriangleleft
w_{j}\vartriangleleft{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}}}$.
In other words, we have a scan
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}}$
observing a write
${\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}w^{\prime}_{j}}$
with another intervening write
${\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}w_{j}}$
showing up in between. But this contradicts the argument we carried out for
Fig. 5 above. ∎

###### Lemma 3.3.

Every execution of Algorithm 1 satisfies the $\mathsf{Forwarding}$ signature
(Fig. 7).

###### Proof sketch.

We instantiate the set of virtual scans to be the same as the set of abs scans
(since Algorithm 1 is single-scanner), and define
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}[-]^{\bullet}}$
by
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\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}s}^{\bullet}}={\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}s}$.
Fig. 7, requiring
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\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}s}^{\bullet}}\in{\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}s}$,
follows immediately because every event
${\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}e}$
satisfies
${\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}e}\subseteq{\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}e}$.
Since Algorithm 1 is a single-scanner algorithm, the total order of virtual
scans Fig. 7 naturally follows.

We instantiate forwarding visibility
${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{fwd}}$}}}$}}}s}\triangleq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}\mathit{b}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{s}{\mathit{b}_{i}}}$,
to directly capture how forwarding is defined for Algorithm 1. Properties (7),
(7), (7) and (7) hold by the structure of the algorithm, while Figs. 7, 7 and
7 follows from the
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>instantiation (proved in Appendix C). For the remaining Properties (7) to (7),
we need two helper lemmas (also proved in Appendix C):

  * •

Lemma C.1:
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{w_{i}}\mathit{x}}$
iff we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}\vartriangleleft{w_{i}}\mathit{x}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{off}}\not\vartriangleleft{w_{i}}\mathit{x}}$.

  * •

Lemma C.2: If
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{off}}\not\vartriangleleft{w^{\prime}_{i}}\mathit{x}}$
and if
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}\mathit{b}}$
was executed, then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}\mathit{b}\vartriangleleft{s}{\mathit{b}_{i}}}$.

We focus here on proving Fig. 7 which involves showing if
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}{\mathit{r}_{i}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{s}{\mathit{b}_{i}}}$
then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\vartriangleleft{s}{\mathit{a}_{i}}}$.
By Lemma C.2, we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{off}}\not\vartriangleleft{w^{\prime}_{i}}\mathit{b}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}\mathit{b}\vartriangleleft{s}{\mathit{b}_{i}}}$
if
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}\mathit{b}}$
was executed. Consider if we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}\vartriangleleft{w^{\prime}_{i}}\mathit{x}}$,
then by Lemma C.1 we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{w^{\prime}_{i}}\mathit{x}}$
which in turn implies that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}\mathit{b}}$
must have executed, however that contradicts Fig. 3 by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}\mathit{b}}$
occurring in between
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}{\mathit{r}_{i}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{s}{\mathit{b}_{i}}}$,
thus we must have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}\not\vartriangleleft{w^{\prime}_{i}}\mathit{x}}$.
By Eq. RB.1 over
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\sqsubset{w^{\prime}_{i}}\mathit{x}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}\sqsubset{s}{\mathit{a}_{i}}}$,
since
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}\not\vartriangleleft{w^{\prime}_{i}}\mathit{x}}$
contradicts
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}\sqsubset{w^{\prime}_{i}}\mathit{x}}$,
we must have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\sqsubset{s}{\mathit{a}_{i}}}$,
which is our goal. ∎

##  4\. Multi-Writer Algorithms

To allow for correct non-blocking algorithms with multiple concurrent writers,
as well as for multiple concurrent scanners in the case of Algorithm 3,
Jayanti uses $\mathbf{LL}$ (load-link), $\mathbf{SC}$ (store-conditional) and
$\mathbf{VL}$ (validate) operations (Jensen et al., 1987) in addition to
simple memory mutation and dereference. We thus need to extend the register
signature to account for the new operations. Additionally, Algorithms 2 and 3,
both being multi-writer algorithms share more structure than what we capture
in the $\mathsf{Forwarding}$ signature of Fig. 7. We thus introduce a new
$\mathsf{MWForwarding}$ signature to capture the commonality of the multi-
writer algorithms. We then show that histories satisfying
$\mathsf{MWForwarding}$ also satisfy $\mathsf{Forwarding}$ and that Algorithms
2 and 3 satisfy $\mathsf{MWForwarding}$.

###  4.1. LL/SC Registers

For a memory cell $\mathtt{X}$, $\mathbf{LL}(\mathtt{X})$, or load-link, reads
from, and returns the value of $\mathtt{X}$. It also records the time of the
read, for use in future $\mathbf{SC}$ and $\mathbf{VL}$ operations of the same
thread. $\mathbf{SC}(\mathtt{X},v)$, or store-conditional, writes $v$ into
$\mathtt{X}$ and returns $\mathtt{true}$ if no other write into $\mathtt{X}$
occurred since the most recent $\mathbf{LL}(\mathtt{X})$ from the same thread.
Otherwise, $\mathbf{SC}$ returns $\mathtt{false}$, keeping $\mathtt{X}$
unchanged. Finally, $\mathbf{VL}(\mathtt{X})$, or validate, returns truth
values identically to $\mathbf{SC}$, but does not mutate $\mathtt{X}$.

signature $\mathsf{LLReg}$ $\triangleq$ |  $\mathbf{LL}$/$\mathbf{SC}$ Register
---|---

Let | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}R},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{LL}},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{VL}}$ | Set of all writes, reads, LL, SC, and VL operations
---|---|---
| ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}}$ | ${}\subseteq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{VL}}$ | Set of all successful SC and VL operations
| ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W_{c}}$ | ${}\mathrlap{\ \ \\!=}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W}\cup({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cap{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}})$ | Set of all write-like events of the register
| ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}R_{c}}$ | ${}\mathrlap{\ \ \\!=}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}R}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{LL}}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{VL}}$ | Set of all read-like events of the register

$\mathrlap{\scaleobj{1.2}{\sum}}{\hskip 15.00002pt}$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\prec}$ | ${}\subseteq({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}R_{c}})^{2}$ | Visibility relation
---|---|---|---
| ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}}$ | ${}\subseteq\mathord{{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\prec}}\cap{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W_{c}}\times{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}R_{c}}$ | Reads-from visibility
| ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}}$ | ${}\subseteq\mathord{{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\prec}}\cap{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{LL}}\times({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{VL}})$ |  LL visibility

Let | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\vartriangleleft}$ | ${}\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\sqsubset}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\prec})^{+}$ | Happens-before order
---|---|---|---

$\forall{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e^{\prime}}.$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e\prec^{+}e^{\prime}}$ | ${}\implies{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e^{\prime}\not\sqsubseteq e}$ | (V.1)
---|---|---|---
$\forall{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}r}\in\mathcal{T}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}R_{c}}).$ | $\exists{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W_{c}}.\ {\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}r}$ | (M+.1a)
$\forall{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W_{c}},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}r}\in\mathcal{T}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}R}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{LL}}).$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}r}$ | ${}\implies{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w}.\mathsf{in}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}r}.\mathsf{out}$ | (M+.1b)
$\forall{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}\in\mathcal{T}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{VL}}).$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}.\mathsf{out}=\mathsf{booleanOf}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}})$ | (M+.1c)
$\forall{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W_{c}},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}r}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}R_{c}}.$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}r}$ | ${}\implies\nexists{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W_{c}}.\ {\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\vartriangleleft w^{\prime}\vartriangleleft r}$ | (M+.2)
$\forall{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}r}.$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}r}\land{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}r}$ | ${}\implies{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w=w^{\prime}}$ | (M+.3)
$\forall{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W_{c}}.$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\neq w^{\prime}}$ | ${}\implies{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\vartriangleleft w^{\prime}}\lor{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\vartriangleleft w}$ | (M+.4)
$\forall{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{VL}}.$ | $\exists{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l}\in\mathcal{T}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{LL}}).\ {\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}c}$ | (M+.5)
$\forall{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}.$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}c}\implies{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l}.\mathsf{parent}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}.\mathsf{parent}\land\nexists{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime}}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{LL}}.\ {\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l\vartriangleleft l^{\prime}\vartriangleleft c}$ | (M+.6)
$\forall{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}.$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}c}\land{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}l}\land{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}c}$ | ${}\implies({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w=w^{\prime}}\iff{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}})$ | (M+.7)

Figure 8. Signature for atomic register with
$\mathbf{LL}$/$\mathbf{SC}$/$\mathbf{VL}$ operations.

To capture the properties of memory with the $\mathbf{LL}$, $\mathbf{SC}$ and
$\mathbf{VL}$ operations, we introduce a new signature in Fig. 8, which we
call $\mathbf{LL}$/$\mathbf{SC}$ registers, or $\mathsf{LLReg}$ for short. It
extends $\mathsf{AReg}$ from Fig. 3. We will treat each execution of
$\mathbf{LL}$, $\mathbf{SC}$ and $\mathbf{VL}$ as a read-like event, i.e.,
they will observe some write by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}}$.
Additionally, we denote the LL visibility
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}}$
to link $\mathbf{LL}$ events with their corresponding
$\mathbf{SC}$/$\mathbf{VL}$ events. To capture the concept of
$\mathbf{SC}$/$\mathbf{VL}$ operations being successful, we introduce the set
of successful events
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}}$.
If an $\mathbf{SC}$ event is in
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}}$,
it was successful and must have written to memory, therefore we treat it as a
write-like event. These sets are formally defined in the top part of Fig. 8.

Further, referring to Fig. 8, the Properties (8) to (8) are almost identical
to (3) to (3) from $\mathsf{AReg}$ from Fig. 3. The main difference is that we
substitute quantification over writes and reads with quantification over
write-like events
(${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W_{c}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W}\cup({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cap{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}})$)
and read-like events
(${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}R_{c}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}R}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{LL}}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{VL}}$),
respectively. We also split Fig. 3 into three: (8) says that each terminated
read-like event has some observed write-like event; (8) says that the output
of reads and $\mathbf{LL}$ is the same as the input of the observed write-like
event, and (8) says that the output of $\mathbf{SC}$ and $\mathbf{VL}$ depends
on its success. Additionally, Fig. 8 states that each $\mathbf{SC}$ and
$\mathbf{VL}$ event has a terminated $\mathbf{LL}$ event it is related to in
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}}$.
Fig. 8 says that each
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}}$
pair has the same abs parent, capturing that the two events of the pair were
executed in the same thread (as per our assumption in Section 2.2.1 that each
event is single-threaded), and that no other $\mathbf{LL}$ event occurs in
between the pair. Finally, Fig. 8 captures that successful events observe the
same write-like event as their
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}}$-related
$\mathbf{LL}$ event, meaning no other modifications occurred between the
$\mathbf{LL}$ event and the successful event.

$\mathbf{LL}$$\mathbf{SC}$$\mathcal{S}$$\mathbf{LL}$$\mathbf{SC}$$\mathcal{S}$
(a) Lemma 4.1: Successful $\mathbf{LL}$/$\mathbf{SC}$ pairs do not overlap.

$\mathbf{LL}$$\mathbf{SC}$$\exists w$ (b) Lemma 4.2: There will always exist
some write-like event in between an $\mathbf{LL}$/$\mathbf{SC}$ pair.

$\mathbf{LL}$$\mathbf{SC}$$\mathbf{LL}$$\mathbf{SC}$$\exists$$\mathbf{LL}$$\mathbf{SC}$$\mathcal{S}$
(c) Lemma 4.3: If $\mathbf{SC}$ is the only kind of write, then there exists a
writing $\mathbf{LL}$/$\mathbf{SC}$ pair in the interval of two consecutive
$\mathbf{LL}$/$\mathbf{SC}$ pairs.

Figure 9. Illustration of key properties of $\mathbf{LL}$/$\mathbf{SC}$.

There are several important properties of
$\mathbf{LL}/\mathbf{SC}/\mathbf{VL}$ that the algorithms relies upon for
synchronization. We codify them in the following three lemmas and illustrate
in Fig. 9. For each of the lemmas, the events $l$, $c$, $w$, and variants,
operate over the same memory cell $\mathtt{X}:\mathsf{LLReg}$.

###### Lemma 4.1.

Let
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}c}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}c^{\prime}}$
with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}}\in\mathcal{T}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cap{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}})$.
If
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c\vartriangleleft
c^{\prime}}$ then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c\vartriangleleft
l^{\prime}}$.

###### Proof.

By Fig. 8, we know that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime}}$
are terminated, and by Fig. 8, we have that each of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l}$,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime}}$,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}}$
observes some write-like event. By Fig. 8 with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}}$,
then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}$
observe the same write-like event, and dually for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}}$,
i.e., there exists
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}l}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}c}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}l^{\prime}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}c^{\prime}}$.
By Fig. 3, we either have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\vartriangleleft
c}$ or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c\trianglelefteqslant
w^{\prime}}$. In the former case, we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\vartriangleleft
c\vartriangleleft c^{\prime}}$, which contradicts Fig. 3 by there being a
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}$ in
between
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}c^{\prime}}$.
Thus, we must have the latter case, giving us
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c\trianglelefteqslant
w^{\prime}}$, letting us construct
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c\trianglelefteqslant
w^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}l^{\prime}}$
which implies our goal
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c\vartriangleleft
l^{\prime}}$. ∎

###### Lemma 4.2.

Let
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}c}$
with either
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}\in\mathcal{T}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}})$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}\in\mathcal{T}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{VL}}\setminus{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}})$.
Then there exists some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W_{c}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\not\vartriangleleft
l}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\trianglelefteqslant
c}$.

###### Proof.

If
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}\in\mathcal{T}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cap{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}})$,
then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}$
must have successfully written; thus
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w}$
trivially satisfies
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\trianglelefteqslant
c}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\not\vartriangleleft
l}$. The latter holds, because otherwise we get
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c\vartriangleleft
l}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l\trianglelefteqslant
c}$ and thus
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c\vartriangleleft
c}$ which contradicts irreflexivity of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\vartriangleleft}$.
Next, consider
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}\notin{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}}$,
where
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}\in\mathcal{T}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cup{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{VL}})$.

By Fig. 8,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l}$ is
terminated, and by Fig. 8, for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}$
there exist write-like events
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}W_{c}}$
observed by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}$,
respectively. By Fig. 8, these write-like events must be distinct, because
otherwise
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}$
would have been successful. In other words,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}l}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}c}$
where
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w}\neq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}}$.
Taking
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}}$
to be the required write of the lemma, we trivially have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\trianglelefteqslant
c}$. To show that also
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\not\vartriangleleft
l}$, we assume
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\vartriangleleft
l}$ and derive a contradiction. By Fig. 3, we either have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\vartriangleleft
w^{\prime}}$ or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\vartriangleleft
w}$. In the first case, we contradict Fig. 8 for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}l}$
by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\vartriangleleft
w^{\prime}\vartriangleleft l}$. In the second case, we contradict Fig. 8 for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}c}$
by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w^{\prime}\vartriangleleft
w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}l\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}c}$.
∎

###### Lemma 4.3.

Let
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}c\sqsubset
l^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}c^{\prime}}$
where
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}}\in\mathcal{T}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}})$.
If within the time frame of the events
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l}$,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime}}$,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c}$,
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}}$
there are no mutations to register $\mathtt{X}$ except by $\mathbf{SC}$, then
there exist some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime\prime}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime\prime}}$
(over $\mathtt{X}$) with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}c^{\prime\prime}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime\prime}\not\vartriangleleft
l}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime\prime}\trianglelefteqslant
c^{\prime}}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime\prime}}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cap{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}}$.

###### Proof.

From the assumption, by Lemma 4.2, there exists some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c_{0}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}_{0}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c_{0}\not\vartriangleleft
l}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c_{0}\trianglelefteqslant
c}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}_{0}\not\vartriangleleft
l^{\prime}}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}_{0}\trianglelefteqslant
c^{\prime}}$. Since there are no other writes, we can only have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c_{0}},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}_{0}}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cap{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}}$,
by Fig. 8 there has to be some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime}_{0}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime}_{0}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}c^{\prime}_{0}}$.
Let
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime}_{0}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}_{0}}$
be the existentials, we trivially have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}_{0}\trianglelefteqslant
c^{\prime}}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}_{0}}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{SC}}\cap{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathcal{S}}$.
For
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime}_{0}\not\vartriangleleft
l}$, assume we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}l^{\prime}_{0}\vartriangleleft
l}$, we derive a contradiction. We must have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c_{0}\vartriangleleft
c^{\prime}_{0}}$, since we otherwise we contradict
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}_{0}\not\vartriangleleft
l^{\prime}}$ by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}_{0}\vartriangleleft
c_{0}\trianglelefteqslant c\sqsubset l^{\prime}}$, meaning we also must have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c_{0}\vartriangleleft
l^{\prime}_{0}}$ for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c^{\prime}_{0}}$
to be successful, however this contradicts
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c_{0}\not\vartriangleleft
l}$ by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}c_{0}\vartriangleleft
l^{\prime}_{0}\vartriangleleft l}$. ∎

Lemma 4.1 says that if we have two successful $\mathbf{LL}$/$\mathbf{SC}$
pairs, then the intervals of the two pairs do not overlap. To see the
intuition behind the other two lemmas, consider the special case when the
order
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\vartriangleleft}$
is total (e.g., it is a linearization order), so that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\not\vartriangleleft}$
is equivalent to
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\trianglerighteqslant}$.
In that case, Lemma 4.2 says that an $\mathbf{LL}$/$\mathbf{SC}$ interval, or
an $\mathbf{LL}$/$\mathbf{VL}$ interval with a failing $\mathbf{VL}$, must
contain some succesful write-like event. Similarly, Lemma 4.3 says there
exists a successful $\mathbf{LL}/\mathbf{SC}$ interval contained within the
interval defined by two sequential $\mathbf{LL}/\mathbf{SC}$ intervals, even
if the latter two intervals themselves correspond to failing $\mathbf{SC}$’s.
The last property will be used by multi-writer algorithms as follows.
Referring to Algorithm 2, a write procedure will try to execute forwarding by
invoking two sequential intervals of $\mathbf{LL}/\mathbf{SC}$ pairs into the
cell $\mathtt{B}[i]$. Even if both $\mathbf{SC}$’s fail, Lemma 4.3 guarantees
that another concurrent write will have invoked a successful
$\mathbf{LL}/\mathbf{SC}$ interval, thus forwarding the same value on behalf
of the original write.

###  4.2. Multi-Writer Forwarding Signature

1:$\mathtt{A}:\mathbf{array}[n]\ \mathbf{of}\ \mathsf{val}$

2:$\mathtt{B}:\mathbf{array}[n]\ \mathbf{of}\
\mathsf{val}\cup\left\\{\bot\right\\}$

3:$\mathtt{X}:\mathbb{B}\vcentcolon=\mathtt{false}$

4:

5:write($i:\mathbb{N},v:\mathsf{val}$) $\triangleq$ $\triangleright$ $w_{i}$

6:$\mathtt{A}[i]\vcentcolon=v$ $\triangleright$ ${w_{i}}{\mathit{a}}$

7:$x\leftarrow\mathbf{LL}(\mathtt{X})$ $\triangleright$ ${w_{i}}\mathit{x}$

8:if $x$ then

9: forward($i,x$) $\triangleright$
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{w_{i}}\mathit{f_{1}}}$

10: forward($i,x$) $\triangleright$
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{w_{i}}\mathit{f_{2}}}$

11:

12:forward($i:\mathbb{N}$) $\triangleq$ $\triangleright$
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f}$

13:$\mathbf{LL}(\mathtt{B}[i])$ $\triangleright$ ${f}\mathit{b}$

14:$v\leftarrow\mathtt{A}[i]$ $\triangleright$ ${f}\mathit{\underline{a}}$

15:$x^{\prime}\leftarrow\mathbf{VL}(\mathtt{X})$ $\triangleright$
${f}\mathit{\underline{x}}$

16:if $x^{\prime}$ then $\mathbf{SC}(\mathtt{B}[i],v)$ $\triangleright$
${f}\mathit{\underline{b}}$

17:scan$:$ $\mathbf{array}[n]\ \mathbf{of}\ \mathsf{val}$ $\triangleq$
$\triangleright$ $s$

18:for $i\in\left\\{0\dots n-1\right\\}$ do

19: $\mathtt{B}[i]\vcentcolon=\bot$ $\triangleright$ ${s}{\mathit{r}_{i}}$

20:$\mathtt{X}\vcentcolon=\mathtt{true}$ $\triangleright$ ${s}_{\mathit{on}}$

21:for $i\in\left\\{0\dots n-1\right\\}$ do

22: $a\leftarrow\mathtt{A}[i]$ $\triangleright$ ${s}{\mathit{a}_{i}}$

23: $V[i]\vcentcolon=a$

24:$\mathtt{X}\vcentcolon=\mathtt{false}$ $\triangleright$
${s}_{\mathit{off}}$

25:for $i\in\left\\{0\dots n-1\right\\}$ do

26: $b\leftarrow\mathtt{B}[i]$ $\triangleright$ ${s}{\mathit{b}_{i}}$

27: if $b\neq\bot$ then $V[i]\vcentcolon=b$

28:return $V$

Algorithm 2:  Jayanti’s multi-writer, single-scanner snapshot algorithm.

resource
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{A}}\mathrlap{\
\ :}\hphantom{{}\subseteq{}}\mathbf{array}[n]\ \mathbf{of}\ \mathsf{AReg}$
---
resource
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{X}}\mathrlap{\
\ :}\hphantom{{}\subseteq{}}\mathsf{LLReg}$

event signature vscan\+ $\triangleq$
---
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{B}}$ |  ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}$$\mathbf{array}[n]\ \mathbf{of}\ \mathsf{LLReg}$
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}r_{i}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{B}[i].W}$
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}a_{i}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{A}[i].R}$
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}b_{i}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{B}[i].R}$
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{on}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{X}.W_{c}}$
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\underline{\mathit{on}}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{X}.W_{c}}\,\mathrm{or}\,{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{X}.R_{c}}$
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{off}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{X}.W_{c}}$
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\underline{\mathit{off}}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{X}.W_{c}}\,\mathrm{or}\,{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{X}.R_{c}}$

event signature $\textsc{write}_{i}$\+ $\triangleq$
---
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}a}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{A}[i].W}$
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}x}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{X}.\mathit{LL}}$
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f_{1}},{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f_{2}}$ | ${}\in\textsc{forward}_{i}$

event signature $\textsc{forward}_{i}$ $\triangleq$
---
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{B}_{\mathtt{cell}}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}\mathsf{LLReg}$
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}b}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{B}_{\mathtt{cell}}.\mathit{LL}}$
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\underline{a}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{A}[i].R}$
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\underline{x}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{X}.\mathit{VL}}$
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\underline{b}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{B}_{\mathtt{cell}}.\mathit{SC}}$

Figure 10. Resources and event signatures for abs writes, virtual scans and
virtual forwarding corresponding to $\mathsf{MWForwarding}$. The rep events
correspond to the rep events with the same suffix in Algorithm 2, with the
exception of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\underline{\mathit{on}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\underline{\mathit{off}}}$
which are new and correspond to a potential observer of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{on}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{off}}$
respectively.

signature $\mathsf{MWForwarding}$ $\triangleq$ | Multi-Writer snapshot with forwarding
---|---

Let | ${\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}W_{i}}$ | Set of all writes of cell $i$ of the snapshot in history with each ${\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}w_{i}}\in\textsc{write}_{i}$+
---|---|---
| ${\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}S}$ | Set of all scans of the snapshot in history
| ${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}F_{i}}$ | Set of all forwarding events in history with each ${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f}\in\textsc{forward}_{i}$

$\mathrlap{\scaleobj{1.2}{\sum}}{\hskip 15.00002pt}$ | ${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\Sigma}$ |  | Set of virtual scans with each ${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}\in\textsc{vscan}$+
---|---|---|---
| ${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}[-]^{\bullet}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\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}S}\rightharpoonup{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\Sigma}$ | Partial mapping of abs scans into virtual scans
| ${\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}[{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}-}]_{w}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}F_{i}}\to{\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}W_{i}}$ | Write which executed the forwarding event
| ${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}[-]_{\sigma}}$ | ${}\mathrlap{\ \ :}\hphantom{{}\subseteq{}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}F_{i}}\to{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\Sigma}$ | Virtual scan observed by forwarding event

Let | ${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{fwd}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$ | ${}\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}\exists{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f}\in{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}F_{i}}.\ {\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{f}\mathit{\underline{a}}}\land{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}{\mathit{b}_{i}}}$ | Forwarding visibility
---|---|---|---
| ${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$ | ${}\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}{\mathit{a}_{i}}}\land{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{r}_{i}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}{\mathit{b}_{i}}})\lor{\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{fwd}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$ | Reading visibility
| ${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>| ${}\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\vartriangleleft{w^{\prime}_{i}}{\mathit{a}}}$ | Writing visibility
| ${\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}\prec}$ | ${}\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}{\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}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}}\cup{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>| Visibility relation
| ${\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}\vartriangleleft}$ | ${}\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}({\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}\sqsubset}\cup{\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}\prec})^{+}$ | Happens-before order

$\forall{\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}s}\in\mathsf{dom}({\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}[-]^{\bullet}}).$ | ${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\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}s}^{\bullet}}\subseteq{\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}s}$ | (7)
---|---|---
$\forall i,{\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}s}\in\mathcal{T}({\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}S}).$ | $\exists{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>{\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\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}s}^{\bullet}}}\land{\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}w_{i}}.\mathsf{in}={\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>| (7)
$\forall{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{A}[i].W}.$ | $\exists{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$ | (7)
$\forall{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}.\mathtt{B}[i].W_{c}}.$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}.\mathsf{in}=\bot$ | ${}\iff\exists{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}}.\ {\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}{\mathit{r}_{i}}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$ | (7)
$\forall{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}.\mathtt{B}[i].W_{c}}.$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}.\mathsf{in}\neq\bot$ | ${}\iff\exists{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f}.\ {\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$ | (F+.3c)
$\forall{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma},{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}\in{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathtt{X}.R_{c}}.$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}e_{r}}$ | ${}\iff{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}\vartriangleleft e_{r}}\land{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\not\vartriangleleft e_{r}}$ | (F+.3d)
$\forall{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma},{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}}\in{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\Sigma}.$ | ${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma\neq\sigma^{\prime}}$ | ${}\ \,\implies{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma\sqsubset\sigma^{\prime}}\lor{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}\sqsubset\sigma}$ | (7)
$\forall{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}\in{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\Sigma}.$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{r}_{i}}\sqsubset{\sigma}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xRightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}_{\mathit{\underline{on}}}\sqsubset{\sigma}{\mathit{a}_{i}}\sqsubset{\sigma}_{\mathit{off}}\mathrel{\raisebox{-2.0pt}{{$\xRightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}_{\mathit{\underline{off}}}\sqsubset{\sigma}{\mathit{b}_{i}}}$ | (F+.4b)
$\forall{\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}w_{i}}\in{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>| ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\sqsubset{w_{i}}\mathit{x}\sqsubset{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{w_{i}}\mathit{f_{1}}\sqsubset{w_{i}}\mathit{f_{2}}}}$ | (F+.4c)
$\forall{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f}\in{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}F_{i}}.$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{b}\sqsubset{f}\mathit{\underline{a}}\sqsubset{f}\mathit{\underline{x}}\sqsubset{f}\mathit{\underline{b}}}\land{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{b}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}{f}\mathit{\underline{b}}}$ | (F+.4d)
$\forall{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f},{\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}w_{i}},{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}.$ | ${\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}w_{i}}={\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}[{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f}]_{w}}\land{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}[f]_{\sigma}}$ | ${}\ \,\implies{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{w_{i}}\mathit{x}}\sqsubset{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f}\land{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f}.\mathtt{B}_{\mathtt{cell}}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}.\mathtt{B}[i]$ | (F+.5a)
$\forall{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f}\in{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}F_{i}}.$ | $\mathsf{def}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}})$ | ${}\ \,\implies\exists{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}.\ {\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}[f]_{\sigma}}\land{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{f}\mathit{\underline{x}}}$ | (F+.5b)

Figure 11. Signatures for multi-writer snapshot data-structure with
$\mathbf{LL}$/$\mathbf{SC}$ forwarding (Algorithms 2 and 3).

####  4.2.1. Description of Algorithm 2

We first discuss Algorithm 2, which will motivate the definition of
$\mathsf{MWForwarding}$ signature. The common aspect with Algorithm 1 is that
the writer communicates its value to the data structure by writing into
$\mathtt{A}[i]$. Whereas Algorithm 1 may try to communicate the same value
_again_ by forwarding to $\mathtt{B}[i]$, in Algorithm 2, the forwarding
procedure reads whichever value is currently present in $\mathtt{A}[i]$ and
attempts to forward it to $\mathtt{B}[i]$ by means of $\mathbf{LL}$ and
$\mathbf{SC}$. Because multiple writes may be racing on $\mathtt{A}[i]$, the
forwarding procedure may read and forward a different value from
$\mathtt{A}[i]$ than the one the writer initially wrote. The forwarding
procedure may even fail to forward anything. Nevertheless, Lemma 4.3 provides
a guarantee that there will exist _some_ successful forwarding among the
concurrent processes, forwarding a value that is current (i.e., written by
another overlapping write). This is the key property facilitating
linearizability.

Other than that, the scan procedure is mostly the same in Algorithm 2 compared
to Algorithm 1; the main difference is that the order between
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}}$
and each
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}{\mathit{r}_{i}}}$
is swapped, which is done in preparation for Algorithm 3. In Algorithm 1 this
swap would result in a bug, causing interference between forwarding and
initialization of $\mathtt{B}$; the writes may fail to forward their value
because the forwarding flag is turned on too late, or scans may erase
forwarded values by the initializations. But this is safe to do in Algorithm 2
because the use of $\mathbf{LL}$, $\mathbf{SC}$ and $\mathbf{VL}$ over
$\mathtt{X}$ and $\mathtt{B}$ ensures that no forwarding (intended for a scan
${\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}s^{\prime}}$
prior to
${\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}s}$)
can succeed in-between
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}{\mathit{r}_{i}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}}$
of
${\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}s}$.
This is substantiated by the following lemma.

###### Lemma 4.4.

Let
${\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}s^{\prime}}$
be a scan prior to
${\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}s}$,
i.e.,
${\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}s^{\prime}\sqsubset
s}$. If
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{x}}}$
succeeds observing the same
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s^{\prime}}_{\mathit{on}}}$
that the
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}\mathit{x}}$
preceding
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{x}}}$
observed, i.e.,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s^{\prime}}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{f}\mathit{\underline{x}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s^{\prime}}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{w_{i}}\mathit{x}}$,
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}{\mathit{r}_{i}}\vartriangleleft{f}\mathit{\underline{b}}}$,
then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}}$
must fail to write.

###### Proof.

We assume that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}}$
is successful, and derive contradiction. By Fig. 8, there exists some write-
like event
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{f}\mathit{b}}$,
and by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}}$
being successful, Fig. 8 implies that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}}$
observes the same write-like event as
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{b}}$,
i.e.
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{f}\mathit{\underline{b}}}$.
By Fig. 8, we either have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}{\mathit{r}_{i}}\vartriangleleft
w}$ or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\trianglelefteqslant{s}{\mathit{r}_{i}}}$,
in the latter case we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\vartriangleleft{s}{\mathit{r}_{i}}\vartriangleleft{f}\mathit{\underline{b}}}$,
contradicting Fig. 8 by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}{\mathit{r}_{i}}}$
being in between
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}w\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{f}\mathit{\underline{b}}}$,
thus we can only have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}{\mathit{r}_{i}}\trianglelefteqslant
w}$. Since Algorithm 2 is single-scanner, it follows that
${\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}s}$
only starts after
${\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}s^{\prime}}$
has finished, thus we can derive the following:

${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s^{\prime}}_{\mathit{on}}\sqsubset{s^{\prime}}_{\mathit{off}}\sqsubset{s}{\mathit{r}_{i}}\trianglelefteqslant
w\vartriangleleft{f}\mathit{b}\vartriangleleft{f}\mathit{\underline{x}}}$

which implies that we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s^{\prime}}_{\mathit{off}}}$
in between
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s^{\prime}}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{f}\mathit{\underline{x}}}$,
contradicting Fig. 8. ∎

####  4.2.2. The $\mathsf{MWForwarding}$ Signature

The rep-event signatures for multi-writer algorithms in Fig. 10 correspond
closely to the rep events of Algorithm 2. Fig. 10 extends Fig. 6, adding the
$\mathbf{LL}/\mathbf{SC}$ register $\mathtt{X}$ and extending the event
signatures. $\textsc{write}_{i}$\+ extends $\textsc{write}_{i}$ by events
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}\mathit{x}}$,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}\mathit{f_{1}}}$,
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}\mathit{f_{2}}}$
from Algorithm 2, along with an event signature $\textsc{forward}_{i}$
corresponding to the procedure forward from Algorithm 2. vscan\+ extends vscan
by updating $\mathtt{B}$ to be an array of $\mathbf{LL}/\mathbf{SC}$
registers, and adding four additional rep events:
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}}$
corresponding to
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{off}}}$
from Algorithm 2, and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{on}}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{off}}}}$
which are providing support for multi-scanner Algorithm 3. As we shall see in
Section 4.3, in Algorithm 3,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}}$
might not return before
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{a}_{i}}}$,
and similarly for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}}$.
Thus, we need events that observe
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}}$
returning before
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{a}_{i}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}}$
respectively. For Algorithm 2, we simply take
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{on}}}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{off}}}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}}$.

Signature $\mathsf{MWForwarding}$ in Fig. 11 captures the common structure of
Algorithms 2 and 3. Some aspects are preserved from Algorithm 1; for instance
Figs. 7, 7, 7, 7 and 7 are the same as in $\mathsf{Forwarding}$ signature of
Fig. 7. One difference is that we now have sets of forwarding events
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}F_{i}}$
that are instances of the forwarding procedure. The new signature introduces
operations over such forwardings:
${\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}[{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}-}]_{w}}$
maps a forwarding to the write that invoked it, and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}[{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}-}]_{\sigma}}$
maps a forwarding to the virtual scan it is forwarding to. Forwarding
visibility
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>is also updated: it now says that a forwarding reads a value of a write from
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
and relays this value by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f_{i}}\mathit{\underline{b}}}$.

Among the new properties, (11) encodes that only
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}}$
performs forwarding writes into
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}.\mathtt{B}[i]$.
Fig. 11 ensures that nothing wrote to $\mathtt{X}$ other than
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}}$
directly after
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}}$.
Figs. 11, 11 and 11 corresponds to the rep event order of scans, writes and
forwarding respectively. Lastly, Fig. 11 ensures that every forwarding has a
virtual scan to forward to, while Fig. 11 states that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}}$
can only be performed if
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{x}}}$
observed
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}}$.

###### Lemma 4.5.

Histories satisfying $\mathsf{MWForwarding}$ signature also satisfy
$\mathsf{Forwarding}$ signature.

###### Proof sketch.

We instantiate
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\Sigma}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}[-]^{\bullet}}$
of $\mathsf{Forwarding}$ to be the same as the corresponding instantiations of
$\mathsf{MWForwarding}$. Figs. 7, 7, 7, 7 and 7 are shared between the
signatures, therefore they trivially hold.

We next focus on proving Fig. 7, leaving the remaining properties for Appendix
D. Proving Fig. 7 requires showing that
${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{fwd}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$
and
${\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}w^{\prime}_{i}\sqsubset\trianglelefteqslant\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$
and
${\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}w_{i}\vartriangleleft
w^{\prime}_{i}}$ derive a contradiction. To show this, we need a helper lemma,
proved in Appendix D (Lemma D.2): If
${\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}w_{i}\sqsubset\trianglelefteqslant\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$
then surely
${\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}w_{i}}$
will be able to forward to
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
in time, i.e., we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\not\vartriangleleft{w_{i}}\mathit{x}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\not\vartriangleleft{f}\mathit{\underline{x}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}\vartriangleleft{\sigma}{\mathit{b}_{i}}}$
for every
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f}$
executed by
${\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}w_{i}}$.
From
${\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}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{fwd}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$,
by the definition of
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{f}\mathit{\underline{a}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}{\mathit{b}_{i}}}$
for some
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f}$. By
Lemma 3.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}w_{i}\vartriangleleft
w^{\prime}_{i}}$ implies
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\vartriangleleft{w^{\prime}_{i}}{\mathit{a}}}$.
We can also infer (full proof in Appendix D) that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}\vartriangleleft{w^{\prime}_{i}}\mathit{x}}$.

By Lemma D.2, we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\not\vartriangleleft{w_{i}}\mathit{x}}$,
thus by Fig. 11 we derive
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{w_{i}}\mathit{x}}$,
implying
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{w^{\prime}_{i}}\mathit{f_{1}}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{w^{\prime}_{i}}\mathit{f_{2}}}$
will be executed, let
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f^{\prime}}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{w^{\prime}_{i}}\mathit{f_{1}}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f^{\prime\prime}}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{w^{\prime}_{i}}\mathit{f_{2}}}$.
By Lemma D.2, we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\not\vartriangleleft{f^{\prime}}\mathit{\underline{x}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\not\vartriangleleft{f^{\prime\prime}}\mathit{\underline{x}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime}}\mathit{\underline{b}}\vartriangleleft{\sigma}{\mathit{b}_{i}}}$,
similarly to above with Fig. 11 we derive
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{f^{\prime}}\mathit{\underline{x}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{f^{\prime\prime}}\mathit{\underline{x}}}$,
meaning
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime}}\mathit{\underline{b}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime}}\mathit{\underline{b}}}$
will be executed, meaning we have two consecutive $\mathbf{LL}$/$\mathbf{SC}$
pairs of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f^{\prime}}$
and