${\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}}}$.
By Lemma D.1, we have
${\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}}$.

We start with the
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\vartriangleleft{\sigma}{\mathit{r}_{i}}}$
case, where we can derive that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\vartriangleleft{f}\mathit{\underline{a}}}$:

${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\vartriangleleft{\sigma}{\mathit{r}_{i}}\sqsubset{\sigma}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{w_{i}}\mathit{x}\sqsubset{f}\mathit{\underline{a}}}$

which with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\vartriangleleft{w^{\prime}_{i}}{\mathit{a}}}$,
contradicts Fig. 3 by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}}$
occurring in between
${\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}}}$.

For 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}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}}$
case, we start by deriving
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{b}\sqsubset{w^{\prime}_{i}}\mathit{x}}$
by Eq. RB.1 over
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{b}\sqsubset{f}\mathit{\underline{a}}}$
and
${\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}}$,
since we cannot have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\sqsubset{f}\mathit{\underline{a}}}$
since that contradicts Fig. 3 by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}}$
occurring in between
${\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}}}$.
From this, we can derive that we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}\vartriangleleft{w^{\prime}_{i}}\mathit{x}}$
by
${\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{f}\mathit{b}\sqsubset{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^{\prime}_{i}}\mathit{x}}$,
which by Fig. 11 means we have
${\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^{\prime}_{i}}\mathit{x}}$,
thus we know that
${\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 us refer to these as
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f^{\prime}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f^{\prime\prime}}$
respectively. Thus again by Lemmas D.2 and 11 we have
${\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^{\prime}_{i}}\mathit{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}}\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}}}$.

By Lemma D.3 over
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f^{\prime}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f^{\prime\prime}}$,
there exists some
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f^{\prime\prime\prime}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime\prime}}\mathit{b}\not\vartriangleleft{f^{\prime}}\mathit{b}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime\prime}}\mathit{\underline{b}}\trianglelefteqslant{f^{\prime\prime}}\mathit{\underline{b}}}$.
By Fig. 8, we either have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}\vartriangleleft{f^{\prime\prime\prime}}\mathit{\underline{b}}}$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime\prime}}\mathit{\underline{b}}\trianglelefteqslant{f}\mathit{\underline{b}}}$.
In the first case, we have

${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}\vartriangleleft{f^{\prime\prime\prime}}\mathit{\underline{b}}\trianglelefteqslant{f^{\prime\prime}}\mathit{\underline{b}}\vartriangleleft{\sigma}{\mathit{b}_{i}}}$

which contradicts Fig. 8 by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime\prime}}\mathit{\underline{b}}}$
occurring in between
${\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}}}$.
In the second case, if we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime\prime}}\mathit{\underline{b}}\vartriangleleft{f}\mathit{\underline{b}}}$
then by Lemma 4.1, and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f}\mathit{\underline{b}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime\prime}}\mathit{\underline{b}}}$
being successful, we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime\prime}}\mathit{\underline{b}}\vartriangleleft{f}\mathit{b}}$,
and this also follows in the case of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime\prime}}\mathit{\underline{b}}={f}\mathit{\underline{b}}}$.
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{f^{\prime}}\mathit{b}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime\prime}}\mathit{b}\sqsubset{f^{\prime\prime\prime}}\mathit{\underline{b}}}$
we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\sqsubset{f^{\prime\prime\prime}}\mathit{\underline{b}}}$
since we cannot have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime\prime}}\mathit{b}\sqsubset{f^{\prime}}\mathit{b}}$
by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime\prime}}\mathit{b}\not\vartriangleleft{f^{\prime}}\mathit{b}}$.
Thus we have

${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\vartriangleleft{w^{\prime}_{i}}{\mathit{a}}\sqsubset{f^{\prime\prime\prime}}\mathit{\underline{b}}\vartriangleleft{f}\mathit{b}\sqsubset{f}\mathit{\underline{a}}}$

which contradicts Fig. 3 by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}}$
occurring in between
${\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}}}$.
∎

##  Appendix E Algorithms 2 and 3 Satisfy the Multi-Writer Forwarding
Signature

We will show the complete proofs that Algorithms 2 and 3 satisfy the multi-
writer forwarding signature (Fig. 11). We start by repeating the proof that
Algorithm 2 satisfies the signature.

######  Lemma 4.6 0.

Every execution of Algorithm 2 satisfies the $\mathsf{MWForwarding}$ signature
(Fig. 11).

###### Proof.

Since this algorithm is single scanner, we can simply define the set of
virtual scans to be the same as the set of abs scans and map each abs scan to
itself, i.e.,
${\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}S}$
and
${\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}$.
Each rep event directly corresponds to their equivalent variant in Algorithm
2, except for
${\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 set as
${\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}}}={\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}{\sigma}_{\mathit{\underline{off}}}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{off}}}$
respectively. Fig. 7 holds by each event being a subevent of itself
(${\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
e}$) and Fig. 7 holds since the algorithm is single-scanner. Properties (7) to
(11) and (11) to (11) holds directly by the structure of the algorithm and
Fig. 11 can be proven by Lemma C.1, the same lemma that established this
property for Algorithm 1, since the relative structure of
${\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}}}$
is the same. ∎

We next prove that Algorithm 3 satisfies signature. We first prove that the
phases of logical scans can only happen in sequence.

###### Lemma E.1.

Each
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}}$
that successfully wrote to $\mathtt{X}$ are ordered such that there exists
either
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}^{\prime}}$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}^{\prime}}$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}^{\prime}}$,
where we have either
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}\mathit{v}_{\mathit{off}}}$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}\mathit{v}_{\mathit{end}}}$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}\mathit{v}_{\mathit{on}}}$,
with the exception of the first
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}}$,
which observes the initial value of $\mathtt{X}$.

###### Proof.

Looking at Algorithm 3, we see that the only operations writing to
$\mathtt{X}$ are successful $\mathbf{SC}$ operations, which are only events
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}}$.
For either of these events to be successful, they need to observe the same
write as the latest
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}$
observed as per Fig. 8.

For
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}}$
to be successful, we must have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}\mathit{vx}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}\mathit{v}_{\mathit{on}}}$.
For the algorithm to execute
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}}$,
the write
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$
must have written 1 to $x.\mathtt{phase}$, which can only be either the
original initialization of $\mathtt{X}$ or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}}$.
Similarly, for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}}$,
it can only be executed if the write
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$
wrote 2 to $x.\mathtt{phase}$, thus
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$
can only be
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}}$,
and for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}}$,
it can only be executed if the write
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$
wrote 3 to $x.\mathtt{phase}$, thus
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$
can only be
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}}$.
∎

We instantiate the write and forward rep events for the event structures of
Fig. 10 with rep events of the same name. The structure of write and forward
ensures that Properties (7), (11) and (11) to (11) are satisfied.

We instantiate virtual scans as a logical object corresponding to the rep
events executed by pushVS constructing a complete logical scan. The interval
of a virtual scan
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
is instantiated as the smallest interval containing all its rep events. More
formally, if we have
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}$,
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}^{\prime}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}^{\prime\prime}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}\mathit{vx}^{\prime}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}\mathit{vx}^{\prime\prime}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}^{\prime\prime}}$
wrote to $\mathtt{SS}$, then there exists a virtual scan
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$.
Its rep events are instantiated using the rep events of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}$,
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}^{\prime}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}^{\prime\prime}}$
as follows and instantiate
${\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]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
iff
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}^{\prime\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s_{\mathit{ss}}}$.

$\displaystyle{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{r}_{i}}}$
$\displaystyle\triangleq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vr}_{i}}$
$\displaystyle{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}}$
$\displaystyle\triangleq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}}$
$\displaystyle{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{on}}}}$
$\displaystyle\triangleq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}^{\prime}}$
$\displaystyle{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{a}_{i}}}$
$\displaystyle\triangleq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{va}^{\prime}_{i}}$
$\displaystyle{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}}$
$\displaystyle\triangleq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}^{\prime}}$
$\displaystyle{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{off}}}}$
$\displaystyle\triangleq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}^{\prime\prime}}$
$\displaystyle{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}}$
$\displaystyle\triangleq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vb}^{\prime\prime}_{i}}$

We also let
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{init}}\triangleq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{ss}}}\triangleq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}^{\prime\prime}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}\triangleq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}^{\prime\prime\prime}}}$
where
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}^{\prime\prime\prime}}$
was successful and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}^{\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}\mathit{v}_{\mathit{end}}^{\prime\prime\prime}}$,
however these do not need to be in the interval of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$.
We can view the events as forming the following structure.

$\begin{array}[c]{ccccccc}\lx@intercol\hfil{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}\hfil\lx@intercol&&\lx@intercol\hfil{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}^{\prime}}\hfil\lx@intercol&&\lx<EMAIL_ADDRESS>\lx@intercol\hfil${\downbracefill}$\hfil\lx@intercol&&\lx@intercol\hfil${\downbracefill}$\hfil\lx@intercol&&\lx@intercol\hfil${\downbracefill}$\hfil\lx@intercol\\\
{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}\sqsubset}{}&{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vr}_{0}\cdots\mathit{vr}_{n-1}\sqsubset\mathit{v}_{\mathit{on}}}&{\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}}$}}}$}}}}{}&{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}^{\prime}\sqsubset\mathit{va}^{\prime}_{0}\cdots\mathit{va}^{\prime}_{n-1}\sqsubset\mathit{v}_{\mathit{off}}^{\prime}}&{\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}}$}}}$}}}}{}&{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}^{\prime\prime}\sqsubset\mathit{vb}^{\prime\prime}_{0}\cdots\mathit{vb}^{\prime\prime}_{n-1}}&{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{}\sqsubset\mathit{v}_{\mathit{\underline{ss}}}^{\prime\prime}}\\\
&\lx<EMAIL_ADDRESS>&\lx@intercol\hfil{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}\hfil\lx@intercol\end{array}$

Figs. 7, 7, 11 and 11 follows from the structure of virtual scans and the
algorithm.

###### Lemma E.2.

For every virtual scan
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}}$
have written to $\mathtt{X}$, there exists exactly one
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{ss}}}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\vartriangleleft{\sigma}_{\mathit{\underline{ss}}}\vartriangleleft{\sigma}_{\mathit{end}}}$.

###### Proof.

By induction on the number virtual scans performed. The base case corresponds
to where
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
is the very first virtual scan. We simultaneously consider the inductive step
case, where the inductive hypothesis states that all virtual scans
${\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^{\prime}}$
has exactly one
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{\underline{ss}}}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{off}}\vartriangleleft{\sigma^{\prime}}_{\mathit{\underline{ss}}}\vartriangleleft{\sigma^{\prime}}_{\mathit{end}}}$,
the inductive step follows that for
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
proceeding the virtual scans of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\Sigma^{\prime}}$,
there exists exactly one
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{ss}}}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\vartriangleleft{\sigma}_{\mathit{\underline{ss}}}\vartriangleleft{\sigma}_{\mathit{end}}}$.

For the base case, since no other virtual scans has finished prior, we must
have $x.\mathtt{sync}=\mathit{ss}.\mathtt{sync}$ before
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{off}}}}$
has been executed by initialization of $\mathtt{X}$ and $\mathtt{SS}$. For the
inductive step, we have $x.\mathtt{sync}=\mathit{ss}.\mathtt{sync}$ before
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{off}}}}$
executes, since it follows from each
${\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^{\prime}}$
having
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{\underline{ss}}}\vartriangleleft{\sigma^{\prime}}_{\mathit{end}}}$
and there only existing one
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{\underline{ss}}}}$
per
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}}$,
since after
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}}$
has executed, $x.\mathtt{sync}=\mathit{ss}.\mathtt{sync}$ by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{\underline{ss}}}}$
negating $\mathit{ss}.\mathtt{sync}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}}$
negating $x.\mathtt{sync}$, both exactly once.

With
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}}$
successfully writing, we know that the code of phase 3 (lines 31-43 of
Algorithm 3) must have been executed. Let
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}}$,
we also know that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v\underline{x}}}$
returned $\mathtt{true}$, since otherwise
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}}$
must have failed to write. If the value of $\mathit{ss}.\mathtt{sync}$ read by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{ss}}}$
is different from the value of $x.\mathtt{sync}$ read by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{off}}}}$,
then there must exist some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}^{\prime}}$
that negated $\mathit{ss}.\mathtt{sync}$ before
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{ss}}}$
(and thus before
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}}$),
but after
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}}$,
which fits our goal.

Otherwise, if $\mathit{ss}.\mathtt{sync}=x.\mathtt{sync}$, then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}}$
will be executed. If
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}}$
successfully wrote, then we trivially satisfy our goal. Otherwise, by Lemma
4.2, there has to exist some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}^{\prime}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}^{\prime}\not\vartriangleleft\mathit{v}_{\mathit{ss}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}^{\prime}\vartriangleleft\mathit{v}_{\mathit{\underline{ss}}}}$.
Since we must have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}^{\prime\prime}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}\mathit{vx}^{\prime}\sqsubset\mathit{v}_{\mathit{\underline{ss}}}^{\prime}}$
for some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}^{\prime\prime}}$,
consider if we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}=\mathit{v}_{\mathit{off}}^{\prime\prime}}$,
then we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\vartriangleleft\mathit{v}_{\mathit{\underline{ss}}}^{\prime}\vartriangleleft{\sigma}_{\mathit{end}}}$,
satisfying our goal. Consider instead we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\neq\mathit{v}_{\mathit{off}}^{\prime\prime}}$,
by Fig. 8, we either have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\vartriangleleft\mathit{v}_{\mathit{off}}^{\prime\prime}}$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}^{\prime\prime}\vartriangleleft{\sigma}_{\mathit{off}}}$,
where if we have the former then we must have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\vartriangleleft{\sigma}_{\mathit{end}}\vartriangleleft\mathit{v}_{\mathit{off}}^{\prime\prime}\vartriangleleft\mathit{v}_{\mathit{\underline{ss}}}^{\prime}}$
by Lemma E.1, inducing the cycle
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}\sqsubset{\sigma}_{\mathit{end}}\vartriangleleft\mathit{v}_{\mathit{\underline{ss}}}^{\prime}\vartriangleleft\mathit{v}_{\mathit{\underline{ss}}}}$
contradicting irreflexivity of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\vartriangleleft}$,
thus we must have the latter. By
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}^{\prime\prime}\vartriangleleft{\sigma}_{\mathit{off}}}$,
it must be the case that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}^{\prime}}$
correspond to some earlier executed virtual scan, which in the base case
contradicts
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
being the first virtual scan, while in the inductive step
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}^{\prime\prime}}$
corresponds to some
${\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^{\prime}}$,
it must be the case that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}^{\prime}\vartriangleleft{\sigma^{\prime}}_{\mathit{end}}\vartriangleleft{\sigma}_{\mathit{off}}\vartriangleleft\mathit{v}_{\mathit{ss}}}$
by the inductive hypothesis and Lemma E.1, which contradicts
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}^{\prime}\not\vartriangleleft\mathit{v}_{\mathit{ss}}}$.
∎

To efficiently reason about pushVS, we define the intervals of the phases. For
an execution
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}$
of pushVS,
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}.p_{1}}$,
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}.p_{2}}$,
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}.p_{3}}$
are the intervals of phases 1, 2, and 3. Each phase interval
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}$ of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}$
has a start event
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}$
which is some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}$
and an end event
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ee}}$
which is a $\mathbf{SC}$ event of $\mathtt{X}$, where start and end events
need to satisfy
${\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}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{ll}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ee}}}$.
For
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{1}}$
we have
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{1}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ee}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}}$
with either
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{1}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}$
observing the initial value of $\mathtt{X}$ or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}\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}p_{1}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}}$;
for
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{2}}$
we have
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{2}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ee}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}}$
with
${\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}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{2}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}}$;
and for
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{3}}$
we have
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{3}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ee}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}}$
with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\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}p_{3}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}}$.
Each phase
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}$ has
an _advancement event_ , which we encode with
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ae}}$,
which is the rep event successfully writing to $\mathtt{X}$ which advances the
logical scanner to the next phase. For some
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$,
we have
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{1}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ae}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{2}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ae}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{3}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ae}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}}$.

###### Lemma E.3.

For each phase
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}$,
there exists a
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ae}}$
such that
${\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}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ae}}\not\vartriangleleft{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}}$
and
${\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}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ae}}\trianglelefteqslant{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ee}}}$.

###### Proof.

By Lemma 4.2, there exists some successful writing event
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$
of $\mathtt{X}$ such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}\not\vartriangleleft{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}\trianglelefteqslant{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ee}}}$.
If
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ae}}$,
we are done, otherwise by Lemma E.1 we know that
${\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}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}}$
occur in order, so for example in the case of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{2}}$,
we have
${\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}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{2}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}}$,
by Fig. 8 we must have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{on}}\vartriangleleft
e_{r}}$, since
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}\vartriangleleft{\sigma}_{\mathit{on}}}$
contradicts
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}\not\vartriangleleft{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}}$.
Thus by Lemma E.1, there exists some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{2}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ae}}}$
in between
${\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}e_{r}}$,
which satisfies
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\trianglelefteqslant{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ee}}}$
by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\vartriangleleft
e_{r}\trianglelefteqslant{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{ee}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\not\vartriangleleft{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}}$
since
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}\vartriangleleft{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}}$
contradicts Fig. 8 by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{off}}}$
occurring in between
${\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}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{2}}.{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{se}}}$.
The other phases follow by similar arguments. ∎

###### Lemma E.4.

For any terminated pushVS execution
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}$,
there exists some
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
such that for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}$
being the first rep event of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$
being the last, then and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}\not\vartriangleleft{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}\trianglelefteqslant{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}}$.

###### Proof.

Consider whether
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{3}}$
was executed or not by
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}$.
If
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{3}}$
was executed, then by Lemma E.3 we satisfy our goal. Otherwise, if it was not
executed, this means either
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{1}}$
or
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{2}}$
were executed, i.e., there is some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}}$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}}$
setting $x.\mathtt{phase}$, thus there is another chance for
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{3}}$
to run. If again it was not run, we are either in
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{1}}$
or
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}p_{2}}$
by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}/{\sigma^{\prime}}_{\mathit{on}}}$,
by Lemma E.3 the execution of virtual scans must have progressed, and by Lemma
E.1 there must be some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime\prime}}_{\mathit{end}}}$
between
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}/{\sigma}_{\mathit{on}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}/{\sigma^{\prime}}_{\mathit{on}}}$,
where
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime\prime}}_{\mathit{end}}}$
may be equal to
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}}$.
Thus
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime\prime}}_{\mathit{end}}}$
satisfies our goal. ∎

###### Lemma E.5.

For any terminated pushVS executions
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}^{\prime}}$
where
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}\sqsubset\mathit{v}^{\prime}}$,
there exists some
${\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}\sigma^{\prime}}$
such that for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}$
being the first rep event of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}$,
then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}\not\vartriangleleft{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}\vartriangleleft{\sigma^{\prime}}_{\mathit{end}}}$.

###### Proof.

By Lemma E.4 over
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}^{\prime}}$,
we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}\not\vartriangleleft{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}\trianglelefteqslant{\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}{\sigma^{\prime}}_{\mathit{end}}\not\vartriangleleft{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}^{\prime}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}\trianglelefteqslant{\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}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e^{\prime}_{r}}$
are the last events of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}^{\prime}}$
respectively. By Fig. 8, we must have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}\vartriangleleft{\sigma^{\prime}}_{\mathit{end}}}$,
since if we instead had
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}\trianglelefteqslant{\sigma}_{\mathit{end}}}$,
we contradict
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}\not\vartriangleleft{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}^{\prime}}}$
by having
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}\trianglelefteqslant{\sigma}_{\mathit{end}}\trianglelefteqslant{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}\sqsubset{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}^{\prime}}}$.
∎

######  Fig. 7 0.

For any abs 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}$,
we have
${\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}$.

###### Proof.

With Lemma E.5, we can show for
${\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}$
that there exists some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}\vartriangleleft{\sigma^{\prime\prime}}_{\mathit{end}}}$
in between
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{sv_{1}}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{sv_{2}}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}\not\vartriangleleft{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}}$
where
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}$
is the first rep event of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{sv_{1}}}$.
For
${\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}}$,
we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}\vartriangleleft{\sigma}_{\mathit{init}}}$
since some new logical scan must have started after
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}}$
by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime\prime}}_{\mathit{end}}}$
occurring after it, and by the instantiation of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}[-]^{\bullet}}$
we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{ss}}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s_{\mathit{ss}}}$,
thus for all $i$ we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}\vartriangleleft{\sigma}_{\mathit{init}}\sqsubset{\sigma}{\mathit{r}_{i}}\sqsubset{\sigma}{\mathit{b}_{i}}\sqsubset{\sigma}_{\mathit{\underline{ss}}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s_{\mathit{ss}}}$.
Our goal is to establish
${\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}.\mathsf{start}\leq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{r}_{i}}}.\mathsf{start}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}}.\mathsf{end}\leq{\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 show this by showing that we neither 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}s}.\mathsf{start}>{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{r}_{i}}}.\mathsf{start}$
nor
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}}.\mathsf{end}>{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
  * •

Assume 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}s}.\mathsf{start}>{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{r}_{i}}}.\mathsf{start}$,
we derive a contradiction. By definition of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{init}}\sqsubset{\sigma}{\mathit{r}_{i}}}$,
we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{init}}}.\mathsf{end}<{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{r}_{i}}}.\mathsf{start}$,
which implies
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{init}}}.\mathsf{end}<{\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 thus
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}}\sqsubset{\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 in turn implies
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}\sqsubset\mathit{vx}}$
since
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}\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}$,
which contradicts
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}\not\vartriangleleft{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}}$
by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}\vartriangleleft{\sigma}_{\mathit{init}}\sqsubset\mathit{vx}}$.

  * •

Assume we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}}.\mathsf{end}>{\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 derive a contradiction. By definition of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}\sqsubset{\sigma}_{\mathit{\underline{ss}}}}$,
we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}}.\mathsf{end}<{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{ss}}}}.\mathsf{start}$,
which 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}s}.\mathsf{end}<{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{ss}}}}.\mathsf{start}$
and thus
${\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}\sqsubset{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{ss}}}}$.
This in turn implies
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}s_{\mathit{ss}}\sqsubset{\sigma}_{\mathit{\underline{ss}}}}$
since
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}s_{\mathit{ss}}}\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}$,
which contradict irreflexivity of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\vartriangleleft}$
by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}s_{\mathit{ss}}\sqsubset{\sigma}_{\mathit{\underline{ss}}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s_{\mathit{ss}}}$.
∎

######  Fig. 11 0.

For any
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}$
reading $\mathtt{X}$, 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}}$}}}$}}}e_{r}}$
iff we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}\vartriangleleft
e_{r}}$ and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{off}}\not\vartriangleleft
e_{r}}$.

###### Proof.

  * $(\mathord{\implies})$

${\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}}$
trivially implies
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}\vartriangleleft{w_{i}}\mathit{x}}$,
and if we were to have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{off}}\vartriangleleft{w_{i}}\mathit{x}}$
we contradict Fig. 3 since
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{off}}}$
would happen in-between
${\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}e_{r}}$.

  * $(\mathord{\impliedby})$

By the fact that only virtual scans change $\mathtt{X}$ and by Lemma E.1
forcing these changes to be of an order of form
${\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}}$}}}$}}}{s}_{\mathit{off}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}_{\mathit{end}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{s^{\prime}}_{\mathit{on}}\dots}\
$, we know that any write to $\mathtt{X}$ other than
${\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}}}$
either happens before
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}}$
or after
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{off}}}$.
Since
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}\mathit{x}}$
has to observe something when it finishes, it must observe
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s}_{\mathit{on}}}$,
since any other observation leads to a contradiction. ∎

######  Fig. 7 0.

For two distinct virtual scans
${\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}\sigma^{\prime}}$,
we either have
${\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}$.

###### Proof.

By the instantiation of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
and Lemma E.1, we have that each virtual scan must be separated by some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}}$,
i.e., we either have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}\vartriangleleft{\sigma^{\prime}}_{\mathit{init}}}$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}\vartriangleleft{\sigma}_{\mathit{init}}}$.
By Lemma E.2, we know that for each
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
there is exactly one
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{ss}}}}$
occurring before
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}}$,
thus we have either
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{ss}}}\vartriangleleft{\sigma}_{\mathit{end}}\vartriangleleft{\sigma^{\prime}}_{\mathit{init}}}$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{\underline{ss}}}\vartriangleleft{\sigma^{\prime}}_{\mathit{end}}\vartriangleleft{\sigma}_{\mathit{init}}}$.
If we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{ss}}}\vartriangleleft{\sigma}_{\mathit{end}}\vartriangleleft{\sigma^{\prime}}_{\mathit{init}}}$
then we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}\sqsubset{\sigma}_{\mathit{\underline{ss}}}\vartriangleleft{\sigma}_{\mathit{end}}\vartriangleleft{\sigma^{\prime}}_{\mathit{init}}\sqsubset{\sigma^{\prime}}{\mathit{r}_{i}}}$,
and dually for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{\underline{ss}}}\vartriangleleft{\sigma^{\prime}}_{\mathit{end}}\vartriangleleft{\sigma}_{\mathit{init}}}$,
thus we either have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}\sqsubset{\sigma^{\prime}}{\mathit{r}_{i}}}$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}{\mathit{b}_{i}}\sqsubset{\sigma}{\mathit{r}_{i}}}$
for each $i$, which matches the defined bounds of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$,
i.e., we either have
${\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}$,
which is our goal. ∎

##  Appendix F Algorithm 4 Satisfies the Snapshot Signature

We show that Algorithm 4 satisfies the $\mathsf{Snapshot}$ signatures (Fig.
5). We employ virtual scans as a simplification mechanism that allows us to
elide write views from consideration when establishing $\mathsf{Snapshot}$. A
virtual scan will denote a scan that detected no change in the array, i.e., it
returned at line 18. Formally, a virtual scan
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
consists of rep events
${\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}}}$
for each $i$, where both
${\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}}}$
observe the same write (i.e., no change detected), and every
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{a}_{i}}}$
occurs before any
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{j}}}$:

$\forall{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma},i.$ | $\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}}\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}{w_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}{\mathit{b}_{i}}}$ | (5 revisited)
---|---|---
$\forall{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma},i,j.$ | ${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{a}_{i}}\sqsubset{\sigma}{\mathit{b}_{j}}}$ | (5 revisited)

To each abs scan, we can associate a virtual scan as follows. If the abs scan
terminated because it detected no change, than it immediately is a virtual
scan. If the abs scan terminated by returning a view from a write, i.e.,
returned at line 13, then that view itself is an abs scan which can,
recursively, be associated with a virtual scan. We formally define this 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}[-]}^{\bullet}}$
as follows:

${\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}}\triangleq\begin{cases}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}&\text{where}\quad\exists
k.\ \forall i.\
{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{a}_{i}}={s_{k}}{\mathit{a}_{i}}}\land{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}={s_{k}}{\mathit{b}_{i}}}\\\
\hline\cr\\\\[-10.00002pt]
{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}^{\bullet}}&\text{where}\quad\begin{aligned}
\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}w^{\prime}_{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\prime}_{i}},j,k.\
j<k\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\prime}_{i}\sqsubset
w^{\prime}_{i}\sqsubset w_{i}}\land{}\\\
&{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime\prime}_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{s_{j}}{\mathit{a}_{i}}}\land{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{s_{k}}{\mathit{a}_{i}}}\land{\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}}$}}}$}}}{s_{k}}{\mathit{b}_{i}}}\end{aligned}\end{cases}$

We instantiate
${\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}}$
to be the set of all 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}}\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_{i}}$
where
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
is defined; these are the writes that executed their effect. We also
instantiate the visibility relations
${\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}$
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>as follows, using the helper relation
${\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{\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}}$
$\displaystyle\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}}}$
$\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@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<EMAIL_ADDRESS>
In English, the 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}$
reads from, and also observes,
${\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}}$
iff there is an appropriate rep event in the virtual scan
${\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}}$
that reads from
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
at the level of rep events.

###### Lemma F.1.

${\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}[-]}^{\bullet}}$
is a well-founded recursive definition.

###### Proof.

The first case of
${\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}[-]}^{\bullet}}$
is immediately well-founded. For the second case it is well-founded because
the ending time of the scan
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}$
on the right is smaller than the ending time 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}$
on the left, and the ending times are bounded from below by $0$. To see that
the ending time of
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}$
is below that 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}$,
suppose otherwise. Then it must be
${\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}\sqsubset{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$,
because from the code of write we have that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}\sqsubset{w_{i}}{\mathit{a}}}$.
In particular,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{k}}{\mathit{b}_{i}}}\sqsubset{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
for every $k$. But, because
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
is observed by some rep read 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}$,
we also 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}}$}}}$}}}{s_{k}}{\mathit{b}_{i}}}$
for some $k$. Thus, we have an event
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{k}}{\mathit{b}_{i}}}$
that terminated before the event
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
that it observes, which contradicts Eq. V.1. ∎

###### Lemma F.2.

For each 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}$,
we have
${\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}$.

###### Proof.

If
${\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]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
corresponds to the first case, then this is trivial, since
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$
consists of the selected rep events 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}$,
i.e.,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{a}_{i}}={s_{k}}{\mathit{a}_{i}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}={s_{k}}{\mathit{b}_{i}}}$.
Otherwise,
${\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]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}})^{\bullet}}$
corresponds to the second case for some write view
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}$.
By recursion on the definition of
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}[-]^{\bullet}}$
it must be
${\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]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}({\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}})^{\bullet}}\subseteq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}$,
so it suffices to show
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}\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}$.
By definition, if 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}s}.\mathsf{start}\leq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}.\mathsf{start}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}.\mathsf{end}\leq{\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 we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}\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}$.
During the scan, at least three different writes must have been observed:
${\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}}$}}}$}}}{s_{k}}{\mathit{b}_{i}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{s_{k}}{\mathit{a}_{i}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime\prime}_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{s_{j}}{\mathit{a}_{i}}}$
where 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\prime}_{i}\sqsubset
w^{\prime}_{i}\sqsubset w_{i}}$ by the algorithm being single-writer. If we
have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\sqsubset{s_{j}}{\mathit{a}_{i}}}$
we contradict Fig. 3 for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime\prime}_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{s_{j}}{\mathit{a}_{i}}}$
since we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime\prime}_{i}}{\mathit{a}}\sqsubset{w^{\prime}_{i}}{\mathit{a}}\sqsubset{s_{j}}{\mathit{a}_{i}}}$,
thus we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\not\sqsubset{s_{j}}{\mathit{a}_{i}}}$,
which by definition gives us
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{j}}{\mathit{a}_{i}}}.\mathsf{start}\leq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}}.\mathsf{end}$.
Similarly, if we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}\sqsubset{s_{j}}{\mathit{a}_{i}}}$
we contradict Fig. 3 for
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime\prime}_{i}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{s_{j}}{\mathit{a}_{i}}}$
since we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime\prime}_{i}}{\mathit{a}}\sqsubset{w^{\prime}_{i}}{\mathit{a}}\sqsubset{s_{j}}{\mathit{a}_{i}}}$,
thus we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{k}}{\mathit{b}_{i}}}\not\sqsubset{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$,
which by definition gives us
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}.\mathsf{start}\leq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{k}}{\mathit{b}_{i}}}.\mathsf{end}$.
Together, 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}s}.\mathsf{start}<{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{j}}{\mathit{a}_{i}}}.\mathsf{start}\leq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}}.\mathsf{end}<{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}.\mathsf{start}\
,$

and

${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}.\mathsf{end}<{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}.\mathsf{start}\leq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{k}}{\mathit{b}_{i}}}.\mathsf{end}<{\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 gives us
${\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}.\mathsf{start}\leq{\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}.\mathsf{start}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}.\mathsf{end}\leq{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>i.e.,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}\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}$.
∎

######  Eq. V.1 0.

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}}$
then we cannot 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^{\prime}\sqsubseteq
e}$.

###### Proof.

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
${\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}}$
can only hold 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>i.e., 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]{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}s}$
and
${\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}}$
such that
${\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}}}$.
We have 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}e^{\prime}\sqsubseteq
e}$ can only be
${\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}\sqsubset
e}$, since
${\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}}$
cannot be equal events 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}e}$
being a write 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}}$
being a scan. But then, by Eqs. RB.2 and F.2, 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}e^{\prime}\sqsubset
e}$ we derive
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{a}_{i}}\sqsubset{w_{i}}{\mathit{a}}}$,
which contradicts Eq. V.1 for registers. ∎

######  Fig. 5 0.

For every terminated 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}$
and index $i$, there exists some 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}}$
such that
${\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}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>
######  Fig. 5 0.

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]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>then we must 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_{i}=w^{\prime}_{i}}$.

###### Proof.

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]{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}{w_{i}}{\mathit{a}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}}$
are both observed by some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{a}_{i}}}$,
i.e., the same read. Thus, by Fig. 3,
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}={w^{\prime}_{i}}{\mathit{a}}}$,
and since each write executes
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
only once by Property (ES.2), it must be
${\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^{\prime}_{i}}$.
∎

###### Proof.

The structure of the algorithm ensures that at every return of scan, writes of
every memory cell are observed and returned. ∎

######  Fig. 5 0.

For two distinct 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}}$,
we have either
${\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}}$ 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^{\prime}_{i}\vartriangleleft
w_{i}}$.

###### Proof.

Holds by the assumption that the algorithm is single-writer. ∎

######  Fig. 5 0.

Every terminated write is effectful, i.e.,
$\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}W_{i}})\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}\mathbb{W}_{i}}$.

###### Proof.

Since each terminated write must have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
defined, which is how we define 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}\mathbb{W}_{i}}$,
thus every terminated write must be in some
${\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}}$.
∎

###### Lemma F.3.

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}\vartriangleleft
s}$ then
${\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{\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}}}$.

###### Proof.

This proof follows similarly to the proof of Lemma B.1. By viewing
${\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
s}$ 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}}$,
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_{i}\vartriangleleft_{1}\dots\vartriangleleft_{1}s}$.
By induction on the length of the chain. In our base case 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_{i}\vartriangleleft_{1}s}$,
which splits into 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_{i}\sqsubset
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_{i}\prec
s}$, where the latter can only be
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>For
${\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
s}$, by Eqs. RB.2 and F.2, 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_{i}\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}^{\bullet}}}$.
For
${\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}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}}}$
directly from 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>The inductive step is similar. ∎

###### Lemma F.4.

Choose some $j$. 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}$
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 either 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}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}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}}$
is defined or a virtual 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}e^{\prime}}={\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\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\vartriangleleft
e^{\prime}}$ holds 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}}$
such that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}\vartriangleleft
e^{\prime}_{r}}$, where 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}={\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}W_{i}}$
then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
and 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}={\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}$
then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{j}}}$,
and dually for
${\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}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e^{\prime}_{r}}$.

###### Proof.

This proof follows similarly to the proof of Lemma 3.1. 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{\hbox{\pagecolor{lightergray}$\displaystyle\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
the structure of the algorithm, 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. 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 either being a write, thus having
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
defined by assumption, or being a virtual scan, which are first defined when a
scan returns.

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}}$ where 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}={\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}W_{i}}$
then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
and 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}={\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}$
then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e_{r}}={\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{j}}}$,
and dually for
${\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}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}e^{\prime}_{r}}$.
For
${\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
${\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}}}$.
By Section 5 we construct
${\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}}\sqsubset{\sigma^{\prime}}{\mathit{b}_{j}}}$
which gives us our goal
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\vartriangleleft{\sigma^{\prime}}{\mathit{b}_{j}}}$.
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}$
to join events. ∎

######  Fig. 5 0.

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 there does not exist 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}$ holds.

###### Proof.

Given
${\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 assume there 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}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}$, we derive a contradiction. By assumption,
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_{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}}$
for
${\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}}$.
By Lemma F.3 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}\vartriangleleft s}$, we can derive
${\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{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}}$,
and then by Lemma F.4, also
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}\vartriangleleft{w^{\prime}_{i}}{\mathit{a}}\vartriangleleft{\sigma}{\mathit{b}_{i}}}$.
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>and Section 5,
${\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}}$
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}},{\sigma}{\mathit{b}_{i}}}$.
But then
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{i}}{\mathit{a}}}$
occurrs between
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{b}_{i}}}$,
contradicting Fig. 3 and
${\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{b}_{i}}}$.
∎

######  Fig. 5 0.

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},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}}$ then we cannot 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}}$.

###### Proof.

Given
${\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}}$, we show that also having
${\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 a contradiction. We unfold 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{\hbox{\pagecolor{lightergray}$\displaystyle\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{\hbox{\pagecolor{lightergray}$\displaystyle\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}}$.
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>and Section 5, 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_{j}\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}}$
we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{j}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}{\mathit{a}_{j}},{\sigma}{\mathit{b}_{j}}}$,
and similarly for
${\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}\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^{\prime}}}$.
By Section 5 we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{a}_{j}}\sqsubset{\sigma}{\mathit{b}_{i}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}{\mathit{a}_{i}}\sqsubset{\sigma^{\prime}}{\mathit{b}_{j}}}$.
By Eq. RB.1, it is either
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}{\mathit{a}_{j}}\sqsubset{\sigma^{\prime}}{\mathit{b}_{j}}}$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}{\mathit{a}_{i}}\sqsubset{\sigma}{\mathit{b}_{i}}}$.
In the first case (the second is symmetric) we can construct
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{j}}{\mathit{a}}\vartriangleleft{w_{j}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma}{\mathit{a}_{j}}\sqsubset{\sigma^{\prime}}{\mathit{b}_{j}}}$,
meaning that we have
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{j}}{\mathit{a}}\vartriangleleft{w_{j}}{\mathit{a}}\vartriangleleft{\sigma^{\prime}}{\mathit{b}_{j}}}$
contradicting Fig. 3 by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{j}}{\mathit{a}}}$
occurring between
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w^{\prime}_{j}}{\mathit{a}}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}{\sigma^{\prime}}{\mathit{b}_{j}}}$.
∎