${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}f^{\prime\prime}}$.
Since 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}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{f^{\prime\prime}}\mathit{\underline{b}}\vartriangleleft{\sigma}{\mathit{b}_{i}}}$,
it is not possible for any
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}{\mathit{r}_{i}}}$
to occur in the intervals of the $\mathbf{LL}$/$\mathbf{SC}$ pairs, therefore
we can apply Lemma 4.3, thus 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}}}$.
∎

###### Lemma 4.6.

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}}}$.
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. ∎

###  4.3. Multi-Writer, Multi-Scanner

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

2:$\mathtt{A}_{p}:\mathbf{array}[n]\ \mathbf{of}\ \mathsf{val}$

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

4:$\mathtt{X}:\scaleleftright[1.75ex]{<}{\,\begin{aligned}
\mathtt{phase}&:\left\\{1,2,3\right\\}\vcentcolon=1\\\
\mathsf{p}_{\mathtt{A}}\ \mathsf{p}_{\mathtt{B}}&:\mathtt{PID}\\\
\mathtt{sync}&:\mathbb{B}\vcentcolon=\mathtt{false}\end{aligned}\,}{>}$

5:$\mathtt{SS}:\scaleleftright[1.75ex]{<}{\,\begin{aligned}
\mathtt{img}&:\mathbf{array}[n]\ \mathbf{of}\ \mathsf{val}\\\
\mathtt{sync}&:\mathbb{B}\vcentcolon=\mathtt{false}\end{aligned}\,}{>}$

6:

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

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

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

10:if $x.\mathtt{phase}=2$ then

11: forward($i,x.\mathsf{p}_{\mathtt{B}}$) $\triangleright$
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{w_{i}}\mathit{f_{1}}}$

12: forward($i,x.\mathsf{p}_{\mathtt{B}}$) $\triangleright$
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{w_{i}}\mathit{f_{2}}}$

13:

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

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

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

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

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

19:

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

21:$p\leftarrow\mathsf{get}\mathtt{PID}$

22:pushVS($p$) $\triangleright$
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{sv_{1}}}$

23:pushVS($p$) $\triangleright$
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{sv_{2}}}$

24:$\mathit{ss}\leftarrow\mathtt{SS}$ $\triangleright$ $s_{\mathit{ss}}$

25:return $\mathit{ss}.\mathtt{img}$

26:pushVS($p:\mathtt{PID}$) $\triangleq$ $\triangleright$
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}}$

27:$x\leftarrow\mathbf{LL}(\mathtt{X})$ $\triangleright$ $\mathit{vx}$

28:if $x.\mathtt{phase}=1$ then

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

30: $\mathtt{B}_{p}[i]\vcentcolon=\bot$ $\triangleright$ $\mathit{vr}_{i}$

31: $\mathbf{SC}(\mathtt{X},\left\langle
2,x.\mathsf{p}_{\mathtt{A}},p,x.\mathtt{sync}\right\rangle)$ $\triangleright$
$\mathit{v}_{\mathit{on}}$

32: $x\leftarrow\mathbf{LL}(\mathtt{X})$ $\triangleright$ $\mathit{vx}$

33:if $x.\mathtt{phase}=2$ then

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

35: $a\leftarrow\mathtt{A}[i]$ $\triangleright$ $\mathit{va}_{i}$

36: $\mathtt{A}_{p}[i]\vcentcolon=a$ $\triangleright$
$\mathit{v\overline{a}}_{i}$

37: $\mathbf{SC}(\mathtt{X},\left\langle
3,p,x.\mathsf{p}_{\mathtt{B}},x.\mathtt{sync}\right\rangle)$ $\triangleright$
$\mathit{v}_{\mathit{off}}$

38: $x\leftarrow\mathbf{LL}(\mathtt{X})$ $\triangleright$ $\mathit{vx}$

39:if $x.\mathtt{phase}=3$ then

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

41: $b\leftarrow\mathtt{B}_{x.\mathsf{p}_{\mathtt{B}}}[i]$ $\triangleright$
$\mathit{vb}_{i}$

42: if $b\neq\bot$ then

43: $V[i]\vcentcolon=b$

44: else

45: $a\leftarrow\mathtt{A}_{x.\mathsf{p}_{\mathtt{A}}}[i]$ $\triangleright$
$\mathit{v\underline{a}}_{i}$

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

47: $\mathit{ss}\leftarrow\mathbf{LL}(\mathtt{SS})$ $\triangleright$
$\mathit{v}_{\mathit{ss}}$

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

49: if $\mathit{ss}.\mathtt{sync}=x.\mathtt{sync}\land x^{\prime}$ then

50: $\mathbf{SC}(\mathtt{SS},\left\langle
V,\neg\mathit{ss}.\mathtt{sync}\right\rangle)$ $\triangleright$
$\mathit{v}_{\mathit{\underline{ss}}}$

51: $\mathbf{SC}(\mathtt{X},\left\langle
1,x.\mathsf{p}_{\mathtt{A}},x.\mathsf{p}_{\mathtt{B}},\neg
x.\mathtt{sync}\right\rangle)$ $\triangleright$ $\mathit{v}_{\mathit{end}}$

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

Algorithm 3 is the final of the Jayanti’s snapshot algorithms, allowing
unconstrained write and scan operations. It differs from Algorithm 2 in the
implementation of scan, while write is mostly unchanged. While Algorithm 3
allows for multiple concurrently running physical scanners, under the hood, at
most one _virtual_ scanner can be logically viewed as running at any point in
time. The physical scans maintain their own local snapshot and forwarding
arrays, but the shared resource $\mathtt{X}$, via the fields
$\mathtt{X}.\mathsf{p}_{\mathtt{A}}$ and $\mathtt{X}.\mathsf{p}_{\mathtt{B}}$,
keeps track which local snapshot array and local forwarding array,
respectively, should be considered as the current data of the virtual scan.
The physical scanners race to modify these fields in order to promote their
own local arrays as the arrays of the virtual scan. However, $\mathtt{X}$ can
be modified only by $\mathbf{SC}$; thus, by Lemma 4.1, mutations to
$\mathtt{X}$ occur sequentially, and by Lemma 4.2, at least one mutation
exists. The sequential nature of these mutations justifies viewing them as
belonging to a single, albeit virtual, scan. Once the virtual scan terminates,
a snapshot is copied into $\mathtt{SS}$
(${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}}$),
which scanners read
(${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}s_{\mathit{ss}}}$)
and return. We follow Jayanti in assuming that $\mathtt{SS}$, even though
physically a compound object, can still be considered an
$\mathbf{LL}$/$\mathbf{SC}$ register; this is not a loss of generality, as
multi-word $\mathbf{LL}$/$\mathbf{SC}$ registers exist (Jayanti and Petrovic,
2005).

The pushVS procedure (short for “push virtual scan”) propels the virtual
scanner to its completion, producing a snapshot in $\mathtt{SS}$. The
procedure is divided into three phases, tracked by the field
$\mathtt{X}.\mathtt{phase}$, corresponding to the three phases of the previous
algorithms: the first phase sets each memory cell in $\mathtt{B}$ to $\bot$
with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vr}_{i}}$;
the second phase reads the main memory $\mathtt{A}$ with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{va}_{i}}$;
and the third phase reads the forwarding memory $\mathtt{B}$ with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vb}_{i}}$.
However, unlike before when $\mathtt{B}$ was a global array, here we have one
$\mathtt{B}_{p}$ for each scan process $p$. A scanner that successfully writes
with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}}$
in the first phase will have its $\mathtt{B}_{p}$ used for forwarding in the
current virtual scan. For the second phase, the algorithm uses
$\mathtt{A}_{p}$ to store the results of reading $\mathtt{A}$, and similarly
the process $p$ which successfully writes with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{off}}}$
will have its $\mathtt{A}_{p}$ used for the next phase. The third phase uses
$\mathtt{A}_{p}$ and $\mathtt{B}_{q}$ from the processes stored in
$\mathtt{X}$ to construct the snapshot, which is then stored in $\mathtt{SS}$
with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}}$.

Each phase starts with an $\mathbf{LL}(\mathtt{X})$ (three lines labeled
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}$)
and ends with an $\mathbf{SC}(\mathtt{X})$. This ensures that if multiple
physical scanners run a phase simultaneously, only a single $\mathbf{SC}$
operation succeeds writing to $\mathtt{X}$, committing the results of the
phase. Thus, considered across all physical scanners, successful phases cannot
overlap, by Lemma 4.1. Also, phases must run consecutively, because a phase in
some scanner can only start if the previous phase, maybe executed by some
other scanner, has been terminated, incrementing $\mathtt{X}.\mathtt{phase}$
to enable the next phase
(${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{on}}}$,
${\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}}}$).
Because the phases cannot overlap, must be executed in order, and correspond
to the scanner phases in the previous algorithms, a trace of a virtual scan in
Algorithm 3 has essentially the same structure as a trace of a physical scan
in the Algorithms 1 and 2.

To ensure that $\mathtt{SS}$ is only mutated once per virtual scan, we have
two toggle bits $\mathtt{X}.\mathtt{sync}$ and $\mathtt{SS}.\mathtt{sync}$ as
part of $\mathtt{X}$ and $\mathtt{SS}$ respectively. These function such that
every time
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}}$
successfully writes, $\mathtt{X}.\mathtt{sync}$ is negated. $\mathtt{SS}$ can
only be written to by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}}$,
which can only be executed if $\mathtt{X}.\mathtt{sync}$ and
$\mathtt{SS}.\mathtt{sync}$ are equal111Jayanti’s original presentation is
dual, as the sync bits need to be distinct for writing to $\mathtt{SS}$, but
this is equivalent. and $\mathtt{X}$ did not change during the phase. Once
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}}$
successfully writes, $\mathtt{SS}.\mathtt{sync}$ will be negated, meaning no
more writes into $\mathtt{SS}$ can occur in this phase since
$\mathtt{X}.\mathtt{sync}$ and $\mathtt{SS}.\mathtt{sync}$ are now distinct.
We also know that there has to be exactly one successful write with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}}$
before
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}}$,
since
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}}$
only fails if some other
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{\underline{ss}}}}$
succeeded, or some other
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{v}_{\mathit{end}}}$
ended the phase.

It is also vital for linearizability that the virtual scan is in the time
interval of the abs scan returning it. To ensure the virtual scan ends before
the abs scanner ends, the latest virtual scan is finished before pushVS
terminates. Dually, to ensure that the virtual scan was not started before the
abs scanner starts, pushVS is executed twice; once to finish the currently
running virtual scan, and once to generate a virtual scan that can be used by
the abs scanner. Executing pushVS twice is similar to the idea of executing
forward twice in Algorithm 2.

###### Lemma 4.7.

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

###### Proof sketch.

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 virtual 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}$.
Figs. 7, 7, 11 and 11 follows from this structure, which we show in the
Appendix E.

The most involved part is proving Figs. 7 and 7, corresponding to
${\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}$
and
(${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma\sqsubset\sigma^{\prime}}\lor{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}\sqsubset\sigma}$)
respectively, which require us to establish the following helper lemmas,
presented in Appendix E: By Lemma E.2, we have exactly one
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{ss}}}}$
per
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}$,
satisfying
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{\underline{ss}}}\vartriangleleft{\sigma}_{\mathit{end}}}$,
and by Lemma E.5, for any terminated
${\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}}$
of pushVS with
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{v}\sqsubset\mathit{v}^{\prime}}$,
there exists
${\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
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma}_{\mathit{end}}\vartriangleleft{\sigma^{\prime}}_{\mathit{end}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}\not\vartriangleleft{\sigma}_{\mathit{end}}}$.
With Lemma E.2, we can that show for every $i$ we either 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}}}$
or
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}{\mathit{b}_{i}}\sqsubset{\sigma^{\prime}}_{\mathit{\underline{ss}}}\vartriangleleft{\sigma^{\prime}}_{\mathit{end}}\vartriangleleft{\sigma}_{\mathit{init}}\sqsubset{\sigma}{\mathit{r}_{i}}}$,
implying Fig. 7. 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.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime}}$
and
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma^{\prime\prime}}$
with
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}\vartriangleleft{\sigma^{\prime\prime}}_{\mathit{end}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}\not\vartriangleleft{\sigma^{\prime}}_{\mathit{end}}}$
where
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}\mathit{vx}}\subseteq{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\mathit{sv_{1}}}$.
This implies that if we have
${\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}}$,
then
${\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 virtual scan must have started after
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}_{\mathit{end}}}$,
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}}}$,
implying
${\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}\sigma}\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}$
and Fig. 7, the last step is further explained in Appendix E. ∎

##  5\. Applying to Other Snapshot Algorithms

To show the generality of our approach, we next apply it to the snapshot
algorithm of Afek et al. (1993), presented as Algorithm 4. It is a single-
writer, multi-scanner algorithm. At its core, scan of Algorithm 4 collects
snapshots by reading the memory array $\mathtt{A}$ twice. We denote the first
read of index $i$ by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{k}}{\mathit{a}_{i}}}$,
and the second by
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{k}}{\mathit{b}_{i}}}$.
The algorithm looks for changes in the array. If a change is detected, the
reading is restarted in the next iteration. The index $k$ on the reading
events identifies the iteration in which the event occurs. If no change to the
array is detected between the first and second read events, then what was read
is a valid snapshot, reflecting what was in the array at the moment the last
index was first read in the current iteration. To ensure that changes to the
array are properly recognized, each memory cell holds a version number
($\mathtt{A}[i].\mathtt{ver}$) of the latest write, which is a number that is
incremented each time a new value is written to the cell.

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

2: $\scaleleftright[1.75ex]{<}{\,\begin{aligned}
\mathtt{data}&:\mathsf{val}\\\ \mathtt{ver}&:\mathbb{N}\\\
\mathtt{view}&:\mathbf{array}[n]\ \mathbf{of}\
\mathsf{val}\end{aligned}\,}{>}$

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

4:$s\vcentcolon=\textsc{scan}()$ $\triangleright$ ${w_{i}}{\mathit{s}}$

5:$\mathtt{A}[i]\vcentcolon=\left\langle
v,\mathtt{A}[i].\mathtt{ver}+1,s\right\rangle$ $\triangleright$
${w_{i}}{\mathit{a}}$

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

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

3: $\mathit{moved}[i]\vcentcolon=\mathtt{false}$

4:while $\mathtt{true}$ do $k$-th iteration of loop

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

6: $a[i]\vcentcolon=\mathtt{A}[i]$ $\triangleright$ ${s_{k}}{\mathit{a}_{i}}$

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

8: $b[i]\vcentcolon=\mathtt{A}[i]$ $\triangleright$ ${s_{k}}{\mathit{b}_{i}}$

9: $\mathit{changed}\vcentcolon=\mathtt{false}$

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

11: if $a[i].\mathtt{ver}\neq b[i].\mathtt{ver}$ then

12: if $\mathit{moved}[i]$ then

13: return $b[i].\mathtt{view}$

14: else

15: $\mathit{changed}\vcentcolon=\mathtt{true}$

16: $\mathit{moved}[i]\vcentcolon=\mathtt{true}$

17: if $\neg\mathit{changed}$ then

18: return $(b[0].\mathtt{data},\dots,b[n-1].\mathtt{data})$

19:end while

Algorithm 4:  Single-writer, multi-scanner snapshot algorithm of Afek et al.
(1993).

If scan detects that some index $i$ has changed twice during scanning, it can
immediately terminate, returning the _view_ of the latest write into $i$
($\mathtt{A}[i].\mathtt{view}$). The view itself is a snapshot each write
collects by calling scan before writing its value. Keeping views ensures that
the snapshot methods are wait-free. scan tracks how many times index $i$ has
changed by updating the local variable $\mathit{moved}[i]$ each time it
detects a change. Each write commits its value simultaneously with
incrementing the version number and updating the view.

We next use visibility relations to show that Algorithm 4 satisfies the
$\mathsf{Snapshot}$ signature, and is thus linearizable by Lemma 2.3.

###### Lemma 5.1.

Every execution of Algorithm 4 satisfies the $\mathsf{Snapshot}$ signature
(Fig. 5).

###### Proof sketch.

To prove that Algorithm 4 satisfies the $\mathsf{Snapshot}$ signature, 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. 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. Importantly, given
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}$,
the associated 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}}$
satisfies
${\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}$,
from which we shall derive the $\mathsf{Snapshot}$ axioms.

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}}}$ | (A.1)
---|---|---
$\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}}}$ | (A.2)

If 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}$
returned at line 18, we simply define 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}}$
as the set of rep events
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{k}}{\mathit{a}_{i}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{k}}{\mathit{b}_{i}}}$,
where $k$ is the last reading iteration 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}$.
If 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}$
returned at line 13, 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}s}$
returns the view of 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}w_{i}}$,
and we define
${\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}}$.
This is a well-founded recursive definition, 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.

Next, we show that
${\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}$.
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}s}$
terminated with no changes detected, this is trivial, since
${\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}}$
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}$.
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}}$,
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}$.
This holds because, to reach the return at line 13, two changes of
$\mathtt{A}[i]$ must have occurred, thus there are two different writes to
$\mathtt{A}[i]$ before
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}}$
that where observed by some rep event 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}$,
implying
${\color[rgb]{1,0,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}$
starts before
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}}$
and thus also before
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}$.
Additionally, since some
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{k}}{\mathit{b}_{i}}}$
must have read
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$,
i.e.,
${\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}}}$,
it must be that
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{s}}}$
ends before
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}s}$,
as otherwise
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{s_{k}}{\mathit{b}_{i}}\sqsubset{w_{i}}{\mathit{a}}}$
contradicts Eq. V.1.

We next proceed to establish the $\mathsf{Snapshot}$ signature. First, 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. Second, we
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. We now argue that the definitions of the
visibility relations satisfy the $\mathsf{Snapshot}$ properties. Eq. V.1 holds
since if
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}e\prec^{+}e^{\prime}}$
and
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}e^{\prime}\sqsubseteq
e}$ then
${\color[rgb]{1,0,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.,
${\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}}}$.
But then, by Eq. RB.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}\sqsubseteq
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 holds by the structure of the
algorithm. Fig. 5 holds since if
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<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 observed by 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}}$.
Fig. 5 holds because the algorithm is assumed to be single-writer. Fig. 5
holds 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}}$.

Next, Fig. 5 says that 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>there exists no
${\color[rgb]{1,0,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}$. To prove it, we assume that
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w^{\prime}_{i}}$
exists, and 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}}$.
From
${\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}}\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}$,
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 Section 5, 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}}}$.
We elide the proof of the last derivation; it is similar to Lemma 3.1 and is
in Appendix F. 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}}}$.

Lastly, we prove Fig. 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},w_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s}$
and
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w^{\prime}_{i},w^{\prime}_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s^{\prime}}$
with
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}\vartriangleleft
w^{\prime}_{i}}$ and
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w^{\prime}_{j}\vartriangleleft
w_{j}}$ lead to contradiction. 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 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}}}$,
and 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 for
${\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}}}$
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}}}$
and
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{\sigma^{\prime}}{\mathit{b}_{j}}}$.
∎

We conclude this section by observing that the inverse of Lemma 2.3 also
holds; that is, $\mathsf{Snapshot}$ signature is actually satisfiable by every
linearizable snapshot algorithm. This follows by instantiating
${\color[rgb]{1,0,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}$
with the linearization order, defining
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>to relate each read with the latest write before that read in the
linearization, and defining
${\color[rgb]{1,0,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}}$
as the set of all writes in the linearization. The axioms of the signature
then simply state straightforward properties of the linearization order and of
sequential execution in that order. That said, we have established
$\mathsf{Snapshot}$ signature for Algorithm 4 _without_ assuming
linearizability, so that we can derive linearizability by Lemma 2.3.

##  6\. Related Work

The idea to use visibility relations for proving linearizability has first
been proposed by Henzinger et al. (2013) and applied to concurrent queue
algorithms. The explicit motivation of this approach was to modularize the
linearizability proofs. The work on time-stamped stack algorithm of Dodds et
al. (2015) builds on this by introducing a hybrid approach, combining the
visibility method together with the linearization points method. Visibility
has also been applied on algorithms over weak memory, where it is typically
called communication order (Raad et al., 2019). Another related approach of
visibility by Emmi and Enea (2019); Krishna et al. (2020) formulates weakened
specifications for linearizability, where all operations do not have to
linearly occur one after another in a simulation, but occur in partial order,
allowing for certain operations to miss another.

Concerning Jayanti’s algorithms specifically, Jayanti (2005) sketched
linearizability of the first algorithm by describing its linearization points.
He also argued informally, based on forwarding principles, that the changes
between the algorithms preserve linearizability. Delbianco et al. (2017) gave
a proof formalized in Coq of the first algorithm, by constructing a
linearization order along the execution of the algorithm. The proof is
specific to the implementation, making it is unclear how to lift it to the
other two algorithms. Based on that development, Jacobs (2018) developed a
mechanized proof, also of the first algorithm, in VeriFast using prophecy
variables. Petrank and Timnat (2013) and Timnat (2015) present an algorithm
based on the forwarding idea of Jayanti, which implements a set interface with
insert, remove and contains operations, along with an iterator which is a
generalized form of scanner. The set operations can be forwarded to the
scanner, generalizing Jayanti’s forwarding which applies only to write
operations. In the future, we will consider how to generalize our proof to
apply to this algorithm as well. This would involve axiomatizing the set data-
structure, but also what it means abstractly to be a forwarding structure, so
that both Jayanti’s snapshot and the set structure of Petrank and Timnat are
instances.

Afek et al. (1993) proved their algorithm linearizable by using the
linearization point method. While the use of the linearization point method is
fairly straightforward for this algorithm, we showed that we can reuse our
snapshot axiomatization for its proof.

##  7\. Conclusion and Future Work

We presented proofs of linearizability of Jayanti’s three snapshot algorithms
developed in a modular fashion, using the method of visibility relations. More
concretely, the linearizability proofs are decomposed into proof modules, with
many of the modules being shared between the three algorithms; they are
developed once and reused three times to reduce proof complexity.

Importantly, the module interfaces are signatures consisting of relations and
axioms on them that encode the key idea of “forwarding principles”
underpinning Jayanti’s design. We thus show that a formalism based on
visibility relations is powerful enough to mathematically capture these
principles; previously, Jayanti has only presented them informally in English.

In the future, we plan to apply the visibility methods to other algorithms,
and potentially also use the developed modules and signatures as guides in
designing new and more efficient algorithms, much like Jayanti’s three
algorithms start with the single-writer/single-scanner variant and build to
the ultimately desired multi-writer/multi-scanner variant. We shall also study
how the visibility method applies to non-linearizable algorithms, and how to
mechanize our proof in a proof assistant.

###### Acknowledgements.

We thank the anonymous reviewers from the POPL’22 PC for their feedback. This
research was partially supported by the Spanish MICINN projects BOSCO
(PGC2018-102210-B-I00) and the European Research Council project Mathador
(ERC2016-COG-724464).

## References

  * (1)
  * Abadi and Lamport (1991) Martín Abadi and Leslie Lamport. 1991.  The existence of refinement mappings.  _Theoretical Computer Science_ 82, 2 (1991), 253–284.  https://doi.org/10.1016/0304-3975(91)90224-P
  * Afek et al. (1993) Yehuda Afek, Hagit Attiya, Danny Dolev, Eli Gafni, Michael Merritt, and Nir Shavit. 1993\.  Atomic snapshots of shared memory.  _J. ACM_ 40, 4 (Sept. 1993), 873–890.  https://doi.org/10.1145/153724.153741
  * Bouajjani et al. (2017) Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Suha Orhun Mutluergil. 2017.  Proving linearizability using forward simulations. In _Computer-Aided Verification (CAV)_ _(LNCS, Vol. 10427)_. 542–563.  https://doi.org/10.1007/978-3-319-63390-9_28
  * Chakraborty et al. (2015) Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. 2015.  Aspect-oriented linearizability proofs.  _Logical Methods in Computer Science_ Volume 11, Issue 1 (2015).  https://doi.org/10.2168/LMCS-11(1:20)2015
  * Delbianco et al. (2017) Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2017.  Concurrent Data Structures Linked in Time. In _European Conference on Object-Oriented Programming, ECOOP_ _(LIPIcs, Vol. 74)_. 8:1–8:30.  https://doi.org/10.4230/LIPIcs.ECOOP.2017.8
  * Dodds et al. (2015) Mike Dodds, Andreas Haas, and Christoph M. Kirsch. 2015\.  A scalable, correct time-stamped stack. In _Symposium on Principles of Programming Languages_ _(POPL)_. 233–246.  https://doi.org/10.1145/2676726.2676963
  * Emmi and Enea (2019) Michael Emmi and Constantin Enea. 2019.  Weak-consistency specification via visibility relaxation.  _Proc. ACM Program. Lang._ 3, POPL (2019), 60:1–60:28.  https://doi.org/10.1145/3290373
  * Felsner (1992) Stefan Felsner. 1992\.  _Interval orders: combinatorial structure and algorithms_.  Ph.D. Dissertation. Technical University of Berlin.  http://page.math.tu-berlin.de/~felsner/Paper/diss.pdf
  * Henzinger et al. (2013) Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. 2013\.  Aspect-oriented linearizability proofs. In _International Conference on Concurrency Theory (CONCUR)_. 242–256.  https://doi.org/10.1007/978-3-642-40184-8_18
  * Herlihy and Shavit (2008) Maurice Herlihy and Nir Shavit. 2008.  _The art of multiprocessor programming_.  M. Kaufmann.  https://doi.org/10.1108/03684920810907904
  * Herlihy and Wing (1990) Maurice P. Herlihy and Jeannette M. Wing. 1990.  Linearizability: a correctness condition for concurrent objects.  _ACM Trans. Program. Lang. Syst._ 12, 3 (1990), 463–492.  https://doi.org/10.1145/78969.78972
  * Jacobs (2018) Bart Jacobs. 2018\.  Jayanti’s algorithm using prophecies in VeriFast.  https://github.com/verifast/verifast/blob/master/examples/jayanti
  * Jacobs et al. (2018) Bart Jacobs, Willem Penninckx, and Amin Timany. 2018\.  _Abstract I/O specification_.  Technical report CW714. Department Of Computer Science KU Leuven.  https://lirias.kuleuven.be/2088062
  * Jayanti (2005) Prasad Jayanti. 2005\.  An optimal multi-writer snapshot algorithm. In _Symposium on Theory of Computing_ _(STOC ’05)_. 723–732.  https://doi.org/10.1145/1060590.1060697
  * Jayanti and Petrovic (2005) Prasad Jayanti and Srdjan Petrovic. 2005.  Efficient wait-free implementation of multiword LL/SC variables. In _International Conference on Distributed Computing Systems (ICDCS)_. 59–68.  https://doi.org/10.1109/ICDCS.2005.29
  * Jensen et al. (1987) Eric H Jensen, Gary W Hagensen, and Jeffrey M Broughton. 1987\.  _A new approach to exclusive data access in shared memory multiprocessors_.  Technical report UCRL-97663. Lawrence Livermore National Laboratory.  https://llnl.primo.exlibrisgroup.com/permalink/01LLNL_INST/1g1o79t/alma991001081569706316
  * Jung et al. (2020) Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. 2020.  The future is ours: prophecy variables in separation logic.  _Proc. ACM Program. Lang._ 4, POPL (2020), 45:1–45:32.  https://doi.org/10.1145/3371113
  * Krishna et al. (2020) Siddharth Krishna, Michael Emmi, Constantin Enea, and Dejan Jovanovic. 2020.  Verifying visibility-based weak consistency. In _European Symposium on Programming (ESOP)_ _(LNCS, Vol. 12075)_. 280–307.  https://doi.org/10.1007/978-3-030-44914-8_11
  * Lynch and Vaandrager (1995) Nancy A. Lynch and Frits W. Vaandrager. 1995.  Forward and Backward Simulations: I. Untimed Systems.  _Inf. Comput._ 121, 2 (1995), 214–233.  https://doi.org/10.1006/inco.1995.1134
  * Petrank and Timnat (2013) Erez Petrank and Shahar Timnat. 2013.  Lock-free data-structure iterators. In _International Symposium on Distributed Computing (DISC)_. 224–238.  https://doi.org/10.1007/978-3-642-41527-2_16
  * Raad et al. (2019) Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis. 2019.  On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models.  _Proc. ACM Program. Lang._ 3, POPL, Article 68 (2019).  https://doi.org/10.1145/3290381
  * Timnat (2015) Shahar Timnat. 2015\.  _Practical parallel data structures_.  Ph.D. Dissertation. Computer Science Department, Technion.  http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2015/PHD/PHD-2015-06
  * Viotti and Vukolić (2016) Paolo Viotti and Marko Vukolić. 2016.  Consistency in non-transactional distributed storage systems.  _ACM Comput. Surv._ 49, 1, Article 19 (2016).  https://doi.org/10.1145/2926965

##  Appendix A Snapshot Signature Implies Linearizability

Here we prove that every algorithm with histories satisfying the
$\mathsf{Snapshot}$ signature is linearizable. This proof is based on a
similar proof for queues by Chakraborty et al. (2015).

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

To move towards the construction of a linearization, we will first construct a
partial order
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\vartriangleleft_{w}}$
over all write events that contains all logically implied orderings. We will
in steps expand this order, until we have a total order.

###### Definition A.1.

Let
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>be defined if $i\neq j$ and there exists a write
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{j}}$
and a scan
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}s}$
such that
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i},w_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s}$
and
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{j}\vartriangleleft
w^{\prime}_{j}}$. Let
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\vartriangleleft_{w}}\triangleq({\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\vartriangleleft}\
\cup\
{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{wrDiff}}$}}}$}}}})^{+}$.

###### Lemma A.2.

The 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_{w}}$
is a strict partial order.

###### Proof.

For a relation to be a strict partial order, it needs to be transitive and
irreflexive. The 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_{w}}$
is transitive by definition since it is a transitive closure. We prove
irreflexivity by proving acyclicity 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_{w1}}={\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\vartriangleleft}\
\cup\
{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>i.e., we prove there exists no cycle of the following form:

${\color[rgb]{1,0,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_{1}\vartriangleleft_{w1}w_{2}\vartriangleleft_{w1}\cdots\vartriangleleft_{w1}w_{n}\vartriangleleft_{w1}w_{1}}$

We show this by showing that there exists no cycle of size $n=1$ and that we
can shrink any cycle of size $n\geq 2$, meaning that we can recursively shrink
a cycle until it is of size $n=1$. For a cycle with $n=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_{1}\vartriangleleft_{w1}w_{1}}$,
which can only be the case
${\color[rgb]{1,0,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_{1}\vartriangleleft
w_{1}}$, since two writes joined by
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>must come from distinct memory cells. However, 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_{1}\vartriangleleft
w_{1}}$ either, since it contradicts
${\color[rgb]{1,0,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}$
being irreflexive (Lemma 2.1). We show that we can shrink any cycle of $n\geq
2$ by doing a case analysis on the first two instances 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_{w1}}$
in the cycle:

  1. (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_{1}\vartriangleleft
w_{2}\vartriangleleft w_{3}\vartriangleleft_{w1}^{*}w_{1}}$. By transitivity
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}$
we can shrink the cycle to the smaller cycle
${\color[rgb]{1,0,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_{1}\vartriangleleft
w_{3}\vartriangleleft_{w1}^{*}w_{1}}$.

  2. (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<EMAIL_ADDRESS>w_{3}\vartriangleleft_{w1}^{*}w_{1}}$, i.e.,
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{1}}={\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}}$
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_{2}}={\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w^{\prime}_{j}}$
with $i\neq j$ and 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_{j}}$
such that
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i},w_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s}$
and
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{j}\vartriangleleft
w^{\prime}_{j}}$ 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_{2}\vartriangleleft
w_{3}\vartriangleleft_{w1}^{*}w_{1}}$. Let
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{3}}={\color[rgb]{1,0,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}_{k}}$
where $k$ can either be equal to $i$ or $j$ or some other distinct index.
Since each scan is terminated and thus observes the entire memory by Fig. 5,
there must exist 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}w_{k}}$
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>By comparing
${\color[rgb]{1,0,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_{k}}$
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\prime}_{k}}$
with Fig. 5, 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^{\prime\prime}_{k}\trianglelefteqslant
w_{k}}$ 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_{k}\vartriangleleft
w^{\prime\prime}_{k}}$. 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}w^{\prime\prime}_{k}\trianglelefteqslant
w_{k}}$ then we also 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
s}$ by
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w^{\prime}_{j}\vartriangleleft
w^{\prime\prime}_{k}\trianglelefteqslant
w_{k}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s}$,
which implies that
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w^{\prime}_{j}}$
happens between
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{j}}$
and
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}s}$,
contradicting Fig. 5. Thus 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_{k}\vartriangleleft
w^{\prime\prime}_{k}}$, which lets us construct
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>giving us a shorter cycle.

  3. (3)

We have
${\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]{1,0,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_{1}}={\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}}$
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_{2}}={\color[rgb]{1,0,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}}$
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_{3}}={\color[rgb]{1,0,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}_{k}}$
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},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}_{j},w^{\prime}_{k}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s^{\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}w_{j}\vartriangleleft
w^{\prime}_{j}}$ and
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w^{\prime}_{k}\vartriangleleft
w^{\prime\prime}_{k}}$ 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_{3}\vartriangleleft_{w1}^{*}w_{1}}$
where $i\neq j$ and $j\neq k$. Similar to the previous case, by Fig. 5, there
must exist a
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{k}}$
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>By Fig. 5 with
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{j},w_{k}\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}_{j},w^{\prime}_{k}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s^{\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}w_{j}\vartriangleleft
w^{\prime}_{j}}$, it must follow that
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w^{\prime}_{k}\not\vartriangleleft
w_{k}}$, which by Fig. 5 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_{k}\trianglelefteqslant
w^{\prime}_{k}}$, giving 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}w_{k}\vartriangleleft
w^{\prime\prime}_{k}}$ by
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{k}\trianglelefteqslant
w^{\prime}_{k}\vartriangleleft w^{\prime\prime}_{k}}$. This lets us construct
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>giving us a shorter cycle.

  4. (4)

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_{1}\vartriangleleft
w_{2}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{wrDiff}}$}}}$}}}w_{3}\vartriangleleft_{w1}^{*}w_{1}}$.
For this case we simply _rotate_ the cycle to move the first instance to the
end of the cycle, i.e.,
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>w_{2}}$, and case match on the next two
${\color[rgb]{1,0,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_{w1}}$
instances to create a scenario where we either use case (2) or case (3). ∎

By Zorn’s Lemma, we can arbitrarily choose a total order
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$
extending
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\vartriangleleft_{w}}$,
for which we define the concept of maximal candidate, which we use to
construct the complete total order.

###### Definition A.3.

An event
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}e}$
is called a maximal candidate of
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$
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}$
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}\vartriangleleft}$-maximal
(i.e., there exists no greater event in
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\vartriangleleft}$,
which may not necessarily be unique) and one of the following holds:

  1. (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}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}}$
is a write with no scans observing it and it is the greatest write 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}}$,

  2. (2)

${\color[rgb]{1,0,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}s}$
is a scan with for all $i$, 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_{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}}$
is the greatest event of order
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$
in
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathbb{W}_{i}}$.

###### Lemma A.4.

For any non-empty history satisfying the $\mathsf{Snapshot}$ signature, there
exists a maximal candidate of
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$.

###### Proof.

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}<_{w}}$
is a total order over a finite set, there exists a unique greatest 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}}$,
consider the following cases:

  1. (1)

If nothing reads
${\color[rgb]{1,0,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_{i}}$
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}\vartriangleleft}$-maximal,
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}}$
is trivially a maximal candidate.

  2. (2)

If nothing reads
${\color[rgb]{1,0,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_{i}}$
is not
${\color[rgb]{1,0,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}$-maximal,
then there exists an event
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}e}$
greater than
${\color[rgb]{1,0,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@cmyk@fill{0}{1}{0}{0}w_{i}\vartriangleleft
e}$. The event cannot be a write event
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}e}={\color[rgb]{1,0,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}}$,
since that would imply
${\color[rgb]{1,0,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}w^{\prime}_{j}}$,
contradicting
${\color[rgb]{1,0,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}}$
being
${\color[rgb]{1,0,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}}$-maximal.
Thus it must be a scan event
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}e}={\color[rgb]{1,0,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 Fig. 5 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<EMAIL_ADDRESS>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}}\neq{\color[rgb]{1,0,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}}$,
since nothing reads
${\color[rgb]{1,0,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}}$.
Since we have
${\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}\vartriangleleft
s}$, it must be the case 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}}$
does not happen in-between
${\color[rgb]{1,0,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}}$
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}s}$
as per Fig. 5, 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}w^{\prime}_{i}\not\vartriangleleft
w_{i}}$, thus by Fig. 5 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
w^{\prime}_{i}}$. 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}}$
being
${\color[rgb]{1,0,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}}$-maximal,
we also 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}_{i}<_{w}w_{i}}$,
however this contradicts
${\color[rgb]{1,0,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}}$.

  3. (3)

If 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}s}$
such that
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>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}s}$
being
${\color[rgb]{1,0,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}$-maximal,
then we show that
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}s}$
is a maximal candidate 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}$
to be a maximal candidate, we need for all $j$, there 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>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_{j}}$
is
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$-maximal
in
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathbb{W}_{j}}$.
By Fig. 5, we know that there exists 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}w_{j}}$
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>Suppose for each $j\neq 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_{j}}$
is not
${\color[rgb]{1,0,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}}$-maximal
in
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathbb{W}_{j}}$,
then 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}_{j}}$
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_{j}<_{w}w^{\prime}_{j}}$.
This 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_{j}\vartriangleleft
w^{\prime}_{j}}$ by Fig. 5 and 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}<_{w}}$
extends
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\vartriangleleft}$,
which by
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i},w_{j}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}s}$
and
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{j}\vartriangleleft
w^{\prime}_{j}}$ lets us construct
${\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 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}<_{w}w^{\prime}_{j}}$,
however this contradicts maximality of
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}}$.
Thus each
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{j}}$
is
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$-maximal
in
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathbb{W}_{j}}$,
meaning
${\color[rgb]{1,0,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}$
is a maximal candidate.

  4. (4)

If 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}s}$
such that
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>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}s}$
not being
${\color[rgb]{1,0,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}$-maximal,
then there must exist some other event
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}e}$
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}s\vartriangleleft
e}$. If there exists multiple scans observing
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}}$
we let
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}s}$
be the
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\vartriangleleft}$-greatest
among them. 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}$
is a write event
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}e}={\color[rgb]{1,0,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}}$
then 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
w^{\prime}_{j}}$ since
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>w^{\prime}_{j}}$, which contradicts
${\color[rgb]{1,0,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}}$
being the greatest write 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}}$.
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}$
is a scan
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}e}={\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}s^{\prime}}$
then we either have
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>or
${\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 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^{\prime}_{i}}\neq{\color[rgb]{1,0,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}}$,
however the former contradicts our selection 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}$
since both
${\color[rgb]{1,0,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]{1,0,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}}$
observe
${\color[rgb]{1,0,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}}$,
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}s\vartriangleleft
s^{\prime}}$ contradicts that
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}s}$
be the
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\vartriangleleft}$-greatest
among scans observing
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}}$.
We thus have 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 since we also 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
s^{\prime}}$ by
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>s^{\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}w_{i}}$
is in-between
${\color[rgb]{1,0,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}}$
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}s^{\prime}}$
we contradict Fig. 5, thus 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}_{i}\not\vartriangleleft
w_{i}}$ which by Fig. 5 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}\vartriangleleft
w^{\prime}_{i}}$, which contradicts 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}}$
is
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$-maximal.
∎

To construct the total order, we recursively select a maximal candidate, which
we make the last event of the total order and remove from consecutive steps.

###### Theorem A.5.

Every history satisfying our snapshot specifications is linearizable, i.e.,
there exists a total order
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<}$
over each event which forms a legal sequential snapshot behavior and extends
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$
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}\vartriangleleft}$.

###### Proof.

By induction on the number of events in the history. The minimal history, the
one that only consists of the initial writes, is clearly linearizable, no
matter what order
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$
we have.

Our inductive hypothesis is that for some history
${\color[rgb]{1,0,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_{c}}$ satisfying the axioms under
${\color[rgb]{1,0,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}$,
there exists a total order
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<}$
over
${\color[rgb]{1,0,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}$
that forms a legal sequential snapshot behavior and extends
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$
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}\vartriangleleft}$
when only considering events 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}E}$.
For the inductive step, we need to prove for a there exists such a total order
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<^{\prime}}$
of history
${\color[rgb]{1,0,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 extends
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}E}$
by the single event
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}e}$,
with
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}e}$
being an arbitrary maximal candidate of
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$
under history
${\color[rgb]{1,0,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}}$.
By Lemma A.4, 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^{\prime}}$
is non-empty, there must exist a maximal candidate. Consider the two following
cases 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}$.

  * •

${\color[rgb]{1,0,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}}$
is a write. By the definition of being a maximal candidate, we know that there
exists no scan 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}E^{\prime}}$
observing
${\color[rgb]{1,0,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}}$.
If we remove
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}}$
from
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}E^{\prime}}$
then the new history
${\color[rgb]{1,0,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}$
still satisfies the snapshot properties since it is safe to remove any event
that is not read visible. By the inductive hypothesis we have a total order
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<}$
over
${\color[rgb]{1,0,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}$
that forms a legal snapshot behavior and extends
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$
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}\vartriangleleft}$.
To construct the total order
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<^{\prime}}$
over
${\color[rgb]{1,0,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}}$,
we extend
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<}$
with 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}}$
being the last event in the order. Since any write event added to the end 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}<^{\prime}}$
cannot influence the result of previous scan events, it means that 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}<}$
forms a legal snapshot behavior, so must
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<^{\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}={\color[rgb]{1,0,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}$
is a scan. By the definition of being a maximal candidate, we know that all
the writes
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}s}$
observe are maximal under
${\color[rgb]{1,0,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}}$
in their respective memory cell. If we remove
${\color[rgb]{1,0,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}$
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}}$
then the new history
${\color[rgb]{1,0,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}$
still satisfies the snapshot properties since no other events depend on scans.
By the inductive hypothesis we have a total order
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<}$
over
${\color[rgb]{1,0,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}$
that forms legal snapshot behavior and extends
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$
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}\vartriangleleft}$.
To construct the total order
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<^{\prime}}$
over
${\color[rgb]{1,0,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}}$,
we extend
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<}$
with 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}$
being the last event in the order. 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}<^{\prime}}$
order forms a legal snapshot behavior, since any write
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}}$
that
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}s}$
observes is maximal in
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<_{w}}$,
it is impossible for another write to be in-between
${\color[rgb]{1,0,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}s}$,
thus 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}<}$
forms a legal snapshot behavior, so does
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}<^{\prime}}$.
∎

##  Appendix B Forwarding Signature Implies Snapshot Signature

We here give the full proof that any history satisfying the
$\mathsf{Forwarding}$ signature (Fig. 7) also satisfies the
$\mathsf{Snapshot}$ signature (Fig. 5). We start by determining the
instantiations of
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathbb{W}_{i}}$
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>and
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\prec}$
for the $\mathsf{Snapshot}$ signature. Let
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}}\in{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathbb{W}_{i}}$
iff
${\color[rgb]{1,0,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}}$
has executed
${\color[rgb]{0,0,0.6}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.6}{w_{i}}{\mathit{a}}}$,
since the effect of
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}}$
is only observable after this execution. We define a helper notion of
visibility over scans
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>which we use to define
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\prec}$.
The highlighted relations
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>originate from the $\mathsf{Forwarding}$ signature.

$\displaystyle{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w_{i}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\hbox{\pagecolor{lightergray}$\displaystyle\scriptstyle\mathbf{rf}$}}$}}}$}}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}s}^{\bullet}}}$
$\displaystyle{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}s}^{\bullet}}\sqsubset{\color[rgb]{0,0.4,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.4,0}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}s^{\prime}}^{\bullet}}}$
$\displaystyle{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\prec}$
$\displaystyle\mathrlap{\quad\triangleq}\hphantom{{}\implies{}}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\mathbf{rf}}$}}}$}}}}\cup{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrel{\raisebox{-2.0pt}{{$\xrightarrow{{\raisebox{-2.0pt}[0.0pt][0.0pt]{$\scriptstyle{\hbox{\pagecolor{lightergray}$\displaystyle\scriptstyle\mathbf{wr}$}}$}}}$}}}}\cup{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
We prove the $\mathsf{Snapshot}$ properties by unfolding the definition of
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>in the properties so that we can apply the $\mathsf{Forwarding}$ properties.

######  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