
\documentclass[12pt]{article}
\usepackage{amssymb,amsmath}



\def\newtheorems{\newtheorem{theorem}{Theorem}[section]
\newtheorem{cor}[theorem]{Corollary}
\newtheorem{prop}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{claim}[theorem]{Claim}
\newtheorem{example}[theorem]{Example}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{definition}[theorem]{Definition}}

\newtheorem{exercise}{Exercise}

\def\squarebox#1{\hbox to #1{\hfill\vbox to #1{\vfill}}}
\newcommand{\qed}{\hspace*{\fill}
\vbox{\hrule\hbox{\vrule\squarebox{.667em}\vrule}\hrule}\smallskip}




\newtheorems

\newcommand{\THEN}{{\sf then}}
\newcommand{\CONCURRENTLY}{{\sf concurrently}}
\newcommand{\DO}{{\sf do}}
\newcommand{\TO}{{\sf to}}
\newcommand{\FOR}{{\sf for}}
\newcommand{\ELSE}{{\sf else}}
\newcommand{\AND}{{\sf and}}


\newcommand{\Event}{\mbox{\it Event}}


\newcommand{\Read}{\mbox{\it read}}
\newcommand{\Write}{\mbox {\it {write}}}
\newcommand{\Update}{\mbox{\it Update}}
\newcommand{\Scan}{\mbox{\it Scan}}

\newcommand{\FORALL}{{\sf forall}}
\newcommand{\IF}{{\sf if}}
\newcommand{\REPEAT}{{\sf repeat}}
\newcommand{\UNTIL}{{\sf until}}
\newcommand{\RETURN}{{\sf return}}
\newcommand{\GOTO}{{\sf goto}}
\newcommand{\STOP}{{\sf stop}}


\newcommand{\FALSE}{{\rm false}}
\newcommand{\TRUE}{{\rm true}}

\newcommand{\MWR}{\mbox{\rm MWR}}
\newcommand{\HLP}{\mbox{\rm HLP}}

\newcommand{\Value}{\mbox{\it Value}}

\newcommand{\Val}{\mbox{\it val}}

\newcommand{\collect}{\mbox{\it collect}}

\newcommand{\End}{{\it end}}
\newcommand{\Begin}{{\it begin}}


\newcommand{\Data}{\mbox{\textit{Data}}}

\newcommand {\ignore} [1] {}


\begin{document}
\title{Atomic snapshots}
\author{Uri Abraham\\
Models for concurrency 2014}


\maketitle


\begin{abstract}
We describe the single-writer registers atomic snapshot algorithm of \cite{AtomicSnapshot}.
\end{abstract}



\section{Atomic snapshots}
\label{AS}

There are $N$ processes $P_1,\ldots, P_N$. Each process $P_i$ has a register on which it is the only writer
and which any process can read.
The processes can execute  two sorts of operations: \Update\ and \Scan.
 Process $P_i$ executes $\Update_i(v)$ operations where
$v$ is a parameter of type \Data, and any process can execute \Scan\ operations which
return an array of length $N$ of \Data\ values. For any \Update\ operation $U$ we denote
with $\Val(U)$ the value of the parameter $v$ with which $U$ is invoked, and for every
\Scan\ operation $S$, $\Val(S)$ is the array of length $N$ that $S$ returns and $\Val(S)[i]$ is the $i$-th
component of that array. The linear specification is simple. If the
operations are linearly ordered (and assuming initial $\Update_i(v_i)$ operations) every
\Scan\ operation $S$ returns an array $a=\Val(S)$ such that for every index $1\leq i \leq N$, 
$a[i]$ is the value of the last  $\Update_i$ operation that precedes $S$.

When the operations are not linearly ordered (an operation of process $P_i$ may be concurrent with an operation
of $P_j$) the atomicity requirement is that there is a linear ordering $<^\ast$ that extends the partially
ordered precedence relation $<$ and is such that the linear specifications described above hold for $<^\ast$.

\section{The  Single-Writer Scan Algorithm}
\label{Algo}
A variant of the algorithm of \cite{AtomicSnapshot} is in Figure \ref{DP}.
Every process $P_i$ has a register $R_i$ that carries values that are triples with fields $(data, sequence-number, report)$
where $data$ is in \Data, $sequence-number$ is a natural number, and $report$ is an array of length $N$ of \Data\ values.
We say that such a triple is a {\em register triple}.

\begin{figure}[ht]
 
\fbox{
\begin{minipage}[t]{\columnwidth}
\begin{tabbing}
***\=***\=***\=***\=\kill

\Update$(v)$ by $P_i$:\\

0. \> $s:=\Scan()$; \\

1.\> $seq_i:=seq_i+1$\\

2. \> $R_i:= (v,seq_i,s)$ \\
\\
\\
\\
\end{tabbing}
\end{minipage}
}
\fbox{
\begin{minipage}[t]{\columnwidth}
\begin{tabbing}
***\=***\=***\=***\=\kill

\Scan\: (by any process)\\

0. \> \FOR\ $k:= 0\ \TO\ N+1$ $a_k := \collect()$; \\

1.\> \underline{Case 1}: for some $k\in \{ 0\cdots N\}$ $a_k=a_{k+1}$ \\

\>\> \RETURN\ $(a_k[1].data,\ldots,a_k[N].data)$;\\

2. \> \underline{Case 2}: for some $1\leq i \leq N$ there are indexes\\
 \> $0\leq m < n < N+1$ such that\\
 \>\> $a_m[i]\not = a_{m+1}[i]$ and $a_n[i]\not = a_{n+1}[i]$\\
\> \RETURN   \ $a_{n+1}[i].report$

\end{tabbing}
\end{minipage}
}

\fbox{
\begin{minipage}[t]{\columnwidth}
\begin{tabbing}
***\=***\=***\=***\=\kill

\collect:\\

0. \> \FOR\ every $1\leq j \leq N$  $a[j]:= R_j$; \\

1.\> \RETURN\ $a$;

\end{tabbing}
\end{minipage}
}


\caption{A variant of the single-writer snapshot algorithm of \cite{AtomicSnapshot}.}
\label{DP}
\end{figure}

A \Scan \ operation can be a stand-alone \Scan\ or a \Scan\ that is part of an \Update\ operation.
Procedure \collect\ is called $N+2$ times in any \Scan\ execution. A \collect\ execution consists in
reading the registers $R_i$ for $1\leq i \leq N$ in any order and returning the values thus
collected. After recording the values obtained in these \collect\ invocations in local
variables $a_0,\ldots,a_{N+1}$, the \Scan\ algorithm decides on the snapshot value to return. 
There are two modes by which a \Scan\ operation can return. A {\em direct} return is a return
via \underline{Case 1}, and if Case 1 does not apply, then an {\em indirect} return is via \underline{Case 2}.
 We argue below (Lemma \ref{FLM}) that if Case 1 does not apply then it must be that Case 2 applies, 
so that any \Scan\ operation returns a value (that is an array of \Data\ values).

Consider now the \Update\ algorithm for $P_i$. A local variable $seq_i$ (initialize to $0$) is increased by 1 in each execution.
So that the $\ell$-th \Update\ execution has $\ell$ as the value of its sequence number. 
If $U$ is an \Update\ operation (by $P_i$) invoked with value $v$, then we write $v=\Val(U)$.  $U$ consists of some \Scan\ operation
$S$ which is denoted $\Scan(S)$, and a subsequent write on register $R_i$ of the value $(v,\ell, s)$ where $\ell$ is the the sequence
number of this execution, and $s$ is the value returned by the \Scan\ operation (an array of length $N$ of \Data\ values).


\begin{lemma}
\label{FLM}
If Case 1 does not apply to a \Scan\ operation execution $S$, then it must be that Case 2 applies.

\end{lemma}
{\bf Proof.}
Suppose that a \Scan\ operation does not return via Case 1. Then for every $k\in \{ 0,\ldots,N\}$ $a_k\not = a_{k+1}$.
And since procedure \collect\ returns an array of length $N$ (of register triples) there is some $i=i_k$
$(1\leq i \leq N$)
such that $a_k[i] \not = a_{k+1}[i]$. By the pigeon hole principle there are indices $0\leq m < n \leq N$ such that
$i_m=i_n$. That is,   $a_m[i]\not = a_{m+1}[i]$ and $a_n[i]\not = a_{n+1}[i]$. So Case 2 holds.\qed

This short argument exemplifies an idea that is central to our approach to concurrency, and although it is a very simple
idea it is a corner stone of the approach described in \cite{abraham}. The idea is that the correctness proof of a distributed
algorithm can be obtained in three phases.
\begin{enumerate}
\item  The first phase establishes some properties of operation executions by a process
$P_i$ that depend only on the algorithm of $P_i$ and not on the interactions of $P_i$ with the other processes or on
the properties of the communication devices that the processes employ. 

\item The second phase combines the properties obtained in the first stage with the specifications of the communication
devices employed, and obtains some abstract, higher level properties of the operation executions.

\item The third phase takes the abstract properties of the second phase and proves that they entail the 
desired correctness condition. Tarskian system executions serve in the third phase of the proof.

\end{enumerate}
The argument given above (Lemma \ref{FLM}) to show that any \Scan\ that does not return via Case 1 must return via Case 2, is an example
of a first phase argument. The proof of Lemma \ref{FLM} relies only on the code of the \Scan\ operation, it does not rely on any
 knowledge on the \Update\ algorithm or on the registers that are used.  The proof
 relies on the knowledge that the reads of register $R_j$ return register triple values, but not on the atomicity
of these registers. In other words, Lemma \ref{FLM} holds true even if the values returned by the read actions are determined
randomly, and there is absolutely no reference to the \Update\ algorithm in this lemma.


 We state in the following two lemmas, without proof, all the properties that are obtained in the first phase of the proof: those that are
obtained by reference to the \Scan\ operations, and those that are obtained by reference to the \Update\ operations.

\begin{lemma}
\label{FP}
Any \Scan\ operation $S$ is either direct or indirect.
\begin{enumerate}
\item
If $S$ is direct then 
there are two \collect\ executions $c_1<c_2$ in $S$ such that $\Val(c_1)=\Val(c_2)$. Say $a=\Val(c_1)$ is this common
array. The return value of $S$ is $\Val(S)=(a[1].data,\ldots,a[N].data)$.
\item If $S$ is indirect then there is some index $1\leq i \leq N$ and there are four read actions of register $R_i$
 in $S$, $r_1<r_2<r_3<r_4$, such that $\Val(r_1)\not = \Val(r_2)$ and $\Val(r_3)\not = \Val(r_4)$. Say $a=\Val(r_4)$. The value of $S$
in this case is $\Val(S)= a.report$.
\end{enumerate}

\end{lemma}

\begin{lemma}
\label{FP1}
If $U$ is the $\ell$-th \Update\ operation by process $P_i$, and if $\Val(U)=v$ is the value of $U$, 
then $U$ consists of a \Scan\ execution $S=\Scan(U)$ followed by a write action on register $R_i$ of the value $(v,\ell,\Val(S))$.

\end{lemma}

We emphasize that the proof of Lemma \ref{FP} depends only on the algorithm of the \Scan\ operation, and likewise the proof of
lemma \ref{FP1} depends only on the algorithm of the \Update\ operation. So essentially these are proofs about serial
algorithms, and concurrency issues do not enter in these proofs. A more elaborate discussion of this point will be given
in the last section. 

Now we move to the second phase of the proof. In this phase we combine the statements of lemmas \ref{FP} and \ref{FP1}
with the semantics of atomic registers. In fact, for simplicity we assume that all registers $R_i$ are serial, and leave
to the reader to find why we are allowed to do that. So the read/write actions on the different registers are assumed
to be linearly ordered by the precedence relation $<$.
\begin{exercise}
Show that if we prove atomicity of the \Scan/\Update\ operations under the assumption that the registers are serial, then
it follows that even if the registers are assumed to be atomic the desired atomicity of the snapshot algorithm follows.
\end{exercise}

If $r$ is any read action of register $R_i$ then $\omega(r)$ denotes the last write action $w$ on register $R_i$ such that
$w<r$. Following the semantics of serial registers we get that $\Val(\omega(r))=\Val(r)$.
It follows immediately that if $r_1<r_2$ are two read actions of some serial register $R$ then
$\omega(r_1)\leq \omega(r_2)$.
\begin{lemma}
\label{LEQ}
Suppose that $r_1$ and $r_2$ are two read actions of some register $R_i$ such that $\Val(r_1)=\Val(r_2)$.
Then $\omega(r_1)=\omega(r_2)$.
\end{lemma}
{\bf Proof.} If $\omega(r_1) \not=\omega(r_2)$, then for some $\ell_1\not = \ell_2$ $w_1=\omega(r_1)$ is in the $\ell_1$th
 \Update\ operation execution and $w_2=\omega(r_2)$ is in the $\ell_2$ \Update. But in this case
the sequence field of $w_1$ is $\ell_1$ and the sequence field of $w_2$ is $\ell_2$, and thus $Val(w_1)\not = \Val(w_2)$, which
implies that  $\Val(r_1)\not=\Val(r_2)$.\qed

Let $S$ be a direct \Scan\ operation. We define $\Omega(S)$ as the sequence of \Update\ operations whose \Data\
values $S$ return. In details, the definition of $\Omega(S)$ is as follows. 
\begin{definition}
\label{DOM}
By Lemma \ref{FP} there are two \collect\ executions $c_1<c_2$ in $S$ such that $\Val(c_1)=\Val(c_2)$, and if $a=\Val(c_1)$ then
 $\Val(S)=(a[1].data,\ldots,a[N].data)$. For every index $1\leq i\leq N$ we let $r^1(i)\in c_1$ be the read
action of register $R_i$ in $c_1$. Let $w_i=\omega(r^1(i))$ be the corresponding write action, and let $W_i$
be the \Update\ operation to which $w_i$ belongs. We then define $\Omega(S)=(W_1,\ldots,W_N)$. 
We shall use the notation $\Omega_i(S)=W_i$ for $1\leq i \leq N$.
\end{definition}

\begin{lemma}
\label{LOM}
The following properties of the function $\Omega_i$ hold (for $1\leq i \leq N$).
For any direct \Scan\ operation $S$:
\begin{enumerate}
\item $W_i=\Omega_i(S)$ is an \Update\ operation by $P_i$, and $\End(W_i)<\End(S)$.
\[ \Val(S) = (\Val(W_1), \ldots, \Val(W_N)).\]
\item If $V$ is any \Update\ operation by $P_i$ such that $V<S$ then $V\leq \Omega_i(S)$.

\item If $V$ is an \Update\ operation by $P_j$ such that  $\End(V) < \End(\Omega_i(S))$ 
($i$ is any index $1\leq i \leq N$)
then $V\leq \Omega_j(S)$. 
\end{enumerate}
\end{lemma}
{\bf Proof.} Items 1 and 2 of the lemma are rather easy to prove, and so we show the proof of
item 3. Let $S$ be a direct \Scan\ operation and suppose that $c_1<c_2$ are the two \collect\
operations in $S$ such that $\Val(c_1)=\Val(c_2)$ as in Lemma \ref{FP}(1). Suppose that $W_i=\Omega_i(S)$ and $V$ is
an \Update\ operation by $P_j$ such that $\End(V)<\End(W_i)$ (which means that the write action in $V$
precedes the write action in $W_i$). We have to prove that
$V\leq \Omega_j(S)$. By definition of $W_i$ there is a read action $r^1_i$ of register $R_i$ in $c_1$ 
such that $\omega(r^1_i)=w_i$ is the write action in $W_i$. By definition of $\End(W_i)$,
$\End(W_i)=w_i$. Now let $v=\End(V)$ be its write action,
and suppose that $v < w_i$. Let $r^2_j$ be the read in $c_2$ of register
$R_j$. We have that $v<w_i<r^1_i < r^2_j$. Hence $v < r^2_j$, and so $v\leq \omega(r^2_j)$. 
But if $r^1_j$ is the read action in $c_1$ of register $R_j$, then
$\Val(r^1_j) = \Val(r^2_j)$ (as $\Val(c_1)=\Val(c_2)$). Hence
 $\omega(r^1_j)=\omega(r^2_j)$ (by Lemma \ref{LEQ})
and hence $v\leq \omega(r^1_j)$.
This implies that $V\leq \Omega_j(S)$ as desired. \qed



Next, we analyze indirect
\Scan\ operations. Any \Scan\ operation $S$ begins with a series of $N+2$ collect operations $c_0,\ldots,c_{N+1}$ (an execution of line 0)\footnote{Actually there
is no need to execute all of these operations. The algorithm can stop immediately after the condition that allows Case 1 or Case 2
holds, and this is how the algorithm is originally presented.}. Every \collect\ execution contains $N$ read actions of the registers
$R_1,\ldots,R_N$ (in any order). We denote with $\Begin(S)$ the first read action in $c_0$, and $\End(S)$ denotes the last
read action in $c_{N+1}$. If $S_1$ and $S_2$ are \Scan\ operations, then $S_1 \sqsubset S_2$ means that
 $\Begin(S_2)<\Begin(S_1)$ and
$\End(S_1)< \End(S_2)$. That is, $S_1\sqsubset S_2$ says that the temporal extension of $S_1$ is strictly included in the extension
of $S_2$. Since any process is a serial agent that executes its operations in order, if $S_1\sqsubset S_2$ then $S_1$ and $S_2$
belong to different processes. And since there is a finite number of processes, relation $\sqsubset$ is well-founded: any descending sequence of \Scan\ operations must be finite.  Specifically, if $S_1\sqsupseteq S_2\sqsupseteq \cdots \sqsupseteq
S_{N+1}$ is a nested sequence of length $N+1$, then there is an index $n$ with $S_n=S_{n+1}$.   

\begin{lemma}
\label{LU}
 Suppose that $S$ is an indirect \Scan\ operation. Then there is an \Update\ operation $U$ such that
the following holds for $P=\Scan(U)$.
\begin{enumerate}
\item \Val(S)=\Val(P).
\item $P\sqsubset S$.
\end{enumerate}
\end{lemma}
{\bf Proof.}
 By Lemma \ref{FP}(2), there is some index $1\leq i \leq N$ and there are four read actions of register $R_i$
 in $S$, $r_1<r_2<r_3<r_4$, such that $\Val(r_1)\not = \Val(r_2)$ and $\Val(r_3)\not = \Val(r_4)$. Say $a=\Val(r_4)$. The value of $S$
 is $\Val(S)= a.report$.  Let $w=\omega(r_4)$ be the corresponding write action on register $R_i$. Then $r_3<w$ (or else
$w<r_3$ would imply that $w=\omega(r_3)=\omega(r_4)$ in contradiction to $\Val(r_3)\not = \Val(r_4)$). There is an \Update\
operation $U$ such that $w=\End(U)$. That is, $w$ is the write action of $U$. Let $P=\Scan(U)$. To prove the lemma it suffices
to show that $\Begin(S)<\Begin(P)$ (and $\End(S)<w<r_4\leq \End(S)$ is obvious). Suppose on the contrary that $\Begin(P)<\Begin(S)$.
Then we have that \[\Begin(P)<r_1<r_2<r_3<w.\] Since the last write on register $R_i$ that precede $w$ must be before $P$, this
relation implies that $\omega(r_1)=\omega(r_2)$ which is in contradiction to  $\Val(r_1)\not = \Val(r_2)$.\qed

For any indirect \Scan\ operation $S$ we define $Report(S)$ as follows. 
Let $U$ be that \Update\ operation that Lemma \ref{LU} provides, and define
$Report(S)= \Scan(U)$.   So
\begin{equation}
\label{EEq}
\Val(S) = \Val( Report(S)) \text{ and } Report(S)\sqsubset S.\end{equation} 


For any  \Scan\ operation $S_0$ we define the {\em report sequence} of $S_0$, as the sequence $S_0\sqsupseteq S_1\sqsupseteq \cdots$ by the following inductive definition. Suppose that $S_n$ is defined. If $S_n$ is a direct \Scan\ execution then we define $S_{n+1}=S_n$.
If $S_n$ is an indirect \Scan\
operation then we define $S_{n+1}=Report(S_n)$. Since $S\sqsupset T$ implies that $S$ and $T$ belong to different processes,
there is some $n\leq N$ such that $S_0\sqsupset \cdots \sqsupset S_n=S_{n+1}$ (and $S_n=S_k$ for all $k>n$). That is, $S_0,\ldots S_{n-1}$
are all indirect \Scan\ operations but $S_n$ is a direct one. Thus $\Omega(S_n)$ is defined, and we define $\Omega(S_0)=\Omega(S_n)$.
We also define $\Omega_i(S_0)=\Omega_i(S_n)$ for $1\leq i \leq N$.
\begin{theorem}
\label{MT}
The following properties of the function $\Omega_i$ hold (for $1\leq i \leq N$).
For any \Scan\ operation $S$ (direct or indirect):
\begin{enumerate}
\item $W_i=\Omega_i(S)$ is an \Update\ operation by $P_i$, and  $\End(W_i)<\End(S)$.
\[ \Val(S) = (\Val(W_1), \ldots, \Val(W_N))).\]
\item If $V$ is any \Update\ operation by $P_i$ such that $V<S$ then $V\leq \Omega_i(S)$.

\item If $V$ is an \Update\ operation by $P_j$ such that  $\End(V) < \End(\Omega_i(S))$ 
($i$ is any index $1\leq i \leq N$)
then $V\leq \Omega_j(S)$. 
\end{enumerate}

\end{theorem}
{\bf Proof.} Consider the report sequence $S=S_0\sqsupseteq\cdots \sqsupseteq S_n$. 
$\Val(S_0)=\Val(S_n)$ follows from (\ref{EEq})) and likewise
$S_n\sqsubseteq S_0$. So the properties that were established in Lemma \ref{LOM}
transfer to the present theorem. For example, the argument for item 2 is the following. 
If $V$ is an \Update\ operation by $P_i$
 such that  $V<S_0$, then $V<S_n$ (follows from $S_n\sqsubseteq S_0$) and hence $V\leq \Omega_i(S)$ by Lemma \ref{LOM}. \qed



We are now ready for the third phase of the proof: showing that the higher-level properties of the $\Omega$ function established
in Theorem \ref{MT} imply the snapshot properties. To make it absolutely clear that the statement of this third phase theorem
and its proof are independent of the algorithm, we first restate the properties established in Theorem \ref{MT} in a separate list
in Figure \ref{SL}. There is an important difference between the formulation in Theorem \ref{MT} and the properties of
Figure \ref{SL}. There are two kinds of \Scan\ operations: standalone operations, and \Scan\ operations that are part of
some \Update\ operation. So far there was no need to separate these operations since they have the same properties,
and what the theorem says is true both for the standalone operations and the \Scan\ operations that are invoked by
\Update\ operations. In the list of abstract properties of Figure \ref{SL} the term ``\Scan\ events'' refer to the standalone
\Scan\ events, and there is no need to refer to those \Scan\ events that are part of the \Update\ events. The point is that now
we are interested in the \Update/\Scan\ operations, and the fact that the \Update\ operations need (for the algorithm to work)
to invoke  \Scan\ operations is a detail that is abstracted away at this stage of the proof.  

 The system-execution language in which the properties of Figure \ref{SL} are stated has the following components. 
There are two sorts: the \Event\ and
\Data\ sorts. There are unary predicates \Scan\ and \Update\ and $P_1,\ldots,P_N$ on the \Event\ sort.
The binary precedence  relation symbol $<$. We have the following function symbols.
The \Val\ function returns \Data\ values when defined on \Update\ events, and on \Scan\ events $\Val$ returns $N$-tuples
of \Data\ values. We have  $\Omega_i:\Event\to\Event$ for the function that returns the $i$-th component of $\Omega$.
That is, for every \Scan\ event $S$, $\Omega(S)= (\Omega_1(S),\ldots,\Omega_N(S))$.
We also have a function $\End$ defined on the \Event\ sort. Intuitively, $\End(E)$ denotes the end of event $E$, and we think of
$\End(E)$ as some specific event (we would take it as a temporal value in temporal based system executions, but here we prefer
to have system executions in which the time-axis is not present).  There are two properties of the \End\ function which
we shall use.
\begin{enumerate}

\item[E1]  If $X<Y$ are \Scan/\Update\ events and $X<Y$ then $\End(X)<\End(Y)$.

%\item[E2] For every event $A$, $A<\End(A)$ and if $A<B$ then $\End(A)< B$.

%\item[E3] if $\End(A)<B$ then for every event $C$, if $B<C$ then $A<C$

\item[E2] For every events $A$ and $B$, if $A\not = B$ then either $\End(A)<\End(B)$ or else $\End(B)<\End(A)$. 
\end{enumerate}


\begin{figure}
\fbox{
\begin{minipage}[t]{\columnwidth}

\begin{enumerate}
\item[S1] Each $P_i$ is a serial process. For every \Update\ event $U$ there is a unique process index $i$ such that
$P_i(U)$.
\item[S2] For every \Scan\ event $S$, $W_i=\Omega_i(S)$ is an \Update\ event by $P_i$, and  $\End(W_i)<\End(S)$.
\[ \Val(S) = (\Val(W_1), \ldots, \Val(W_N))).\]
\item[S3] If $V$ is any \Update\ operation by $P_i$ and $S$ is any \Scan\ event such that $V<S$, then $V\leq \Omega_i(S)$.

\item[S4] If $V$ is an \Update\ operation by $P_j$ and $S$ is a \Scan\ event such that  $\End(V) < \End(\Omega_i(S))$ 
($i$ is any index $1\leq i \leq N$),
then $V\leq \Omega_j(S)$. 

\end{enumerate}
\end{minipage}
}
\caption{The higher level properties of the \cite{AtomicSnapshot} snapshot algorithm.}
\label{SL}
\end{figure} 
\begin{theorem}
Let $M$ be any system execution that satisfies the properties listed in Figure \ref{SL}. Then there is a linear ordering on the
\Scan/\Update\ events that satisfy the linear snapshot specifications of Section \ref{AS}.
\end{theorem}

The proof begins with the following lemma.

\begin{lemma}
\label{LSS}
Let $S_1$ and $S_2$ be two \Scan\ events and assume that for some $1\leq i \leq N$ $\Omega_i(S_1)<\Omega_i(S_2)$.
Then, for every $1\leq k \leq N$, $\Omega_k(S_1)\leq \Omega_k(S_2)$.
\end{lemma}
{\bf Proof.} Suppose on the contrary that $\Omega_i(S_1)<\Omega_i(S_2)$, but for some $1\leq k \leq N$ 

\begin{equation}
\label{E1}
\neg (\Omega_k(S_1) \leq \Omega_k(S_2) ) .
\end{equation}
Then the following is deduced.
\begin{enumerate}
\item
$\Omega_k(S_2)<\Omega_k(S_1)$.

\item Either $\End(\Omega_k(S_1) < \End( \Omega_i(S_2))$ or $\End(\Omega_i(S_2)) < \End(\Omega_k(S_1))$.

\item Suppose first that $\End(\Omega_k(S_1) < \End( \Omega_i(S_2) )$. Then $\Omega_k(S_1)\leq \Omega_k(S_2)$.
\item This is in contradiction to $\Omega_k(S_2)< \Omega_k(S_1)$.

\item Now assume that $\End(\Omega_i(S_2)) < \End(\Omega_k(S_1))$. Then $\Omega_i(S_2)\leq \Omega_i(S_1)$.
\item This is in contradiction to $\Omega_i(S_1)<\Omega_i(S_2)$.
\item Thus in both cases we have reached a contradiction and hence the lemma follows. \qed
\end{enumerate}

\begin{exercise}
Give a detailed justification for each line in the proof given above to Lemma \ref{LSS}.
Have you used all properties S1--S4 ?
\end{exercise} 




Let $X$ and $Y$ be two (different) \Scan/\Update\ events. We define $X<^\ast Y$ if and only if one of the following items 1 -- 4 holds:
\begin{enumerate}
\item[O1]
$X$ and $Y$ are both \Update\ events and $\End(X)<\End(Y)$.

\item[O2]
$X$ is an \Update\ event by process $P_k$, $Y$ a \Scan\ event, and $X\leq \Omega_k(Y)$.

\item[O3]
$X$ is a \Scan\ event, $Y$ an \Update\ event by process $P_k$, and $\Omega_k(X)< Y$.

\item[O4]
$X$ and $Y$ are both \Scan\ events and one of the following possibilities is the case:
\begin{enumerate}
\item For some $1\leq k \leq N$, $\Omega_k(X)<\Omega_k(Y)$, or
\item For all $1\leq k \leq N$  $\Omega_k(X) = \Omega_k(Y)$ and $\End(X)<\End(Y)$.
\end{enumerate} 
\end{enumerate}

We claim that $<^\ast$ is the required linear ordering that proves that the algorithm implements an atomic
\Scan/\Update\ system. We have to prove the following.
\begin{enumerate}

\item Relation $<^\ast$ extends the precedence relation $<$.

\item $<^\ast$ is irreflexive.

\item
For any two \Scan/\Update\ events $X\not = Y$, $X<^\ast Y$ or $Y<^\ast X$.

\item Relation $<^\ast$ is a transitive relation on the \Scan/\Update\ events.

\item For any \Scan\ event $S$, $\Val(S)$ is the correct array of \Data\ values  the the snapshot
specification requires (under the $<^\ast$ linear ordering). That is, if $\Val(S)= (d_1,\ldots, d_N)$ then, for every $1\leq k \leq N$,
$d_k=\Val(W_k)$ where $W_k$ is the $<^\ast$ last \Update\ event $W$ such that $W<^\ast S$.

\end{enumerate}
\begin{exercise}
Prove these five items using the following guidelines. 
\end{exercise}
\begin{enumerate}
\item
Assume that $X<Y$ are \Scan/\Update\ events. Prove (in great details) that $X<^\ast Y$ for each of the following cases.
\begin{enumerate}
\item $X$ and $Y$ are both \Update\ events.

\item $X$ is an \Update\ event, $Y$ is a \Scan \ event.

\item $X$ is a \Scan\ event and $Y$ is an \Update\ event.

\item $X$ and $Y$ are \Scan\ events.
\end{enumerate}

\item This is trivial since we define $X<^\ast Y$ only when $X\not = Y$, and so $X<^\ast X$ is impossible.

\item Suppose that $X$ and $Y$ are two different \Scan/\Update\ events. Prove that $X<^\ast Y$ or $Y<^\ast X$ in each of
the following cases.
\begin{enumerate}
\item
$X$ and $Y$ are both \Update\ events.

\item
$X$ and $Y$ are both \Scan\ events.

\item
One of $X$ and $Y$ is a \Scan\ and the other an \Update\ event. Say $X$ is a \Scan\ and $Y$ an \Update\ event.

\end{enumerate}

\item Assume that $X<^\ast Y <^\ast Z$. Prove that $X<^\ast Z$ in each of the following cases.
\begin{enumerate}
\item $X$ and $Y$ are both \Update\ events.

\begin{enumerate}
\item $Z$ is an \Update\ event.
\item $Z$ is a \Scan\ event.
\end{enumerate}

\item $X$ is an \Update\ event, $Y$ is a \Scan \ event.
\begin{enumerate}
\item $Z$ is an \Update\ event.
\item $Z$ is a \Scan\ event.
\end{enumerate}



\item $X$ is a \Scan\ event and $Y$ is an \Update\ event.
\begin{enumerate}
\item $Z$ is an \Update\ event.
\item $Z$ is a \Scan\ event.
\end{enumerate}

\item $X$ and $Y$ are \Scan\ events. Here you can use Lemma \ref{LSS}.
\begin{enumerate}
\item $Z$ is an \Update\ event.
\item $Z$ is a \Scan\ event.
\end{enumerate}
\end{enumerate}

\item Finally, prove that $<^\ast$ is correct. (This is immediate, but nevertheless give the details.)


\end{enumerate}


\noindent
{\bf Discussion.}
It may seem quite strange that the correctness proof that was given here to the snapshot algorithm did not consider the notion
of state. One may rightly argue that in order to prove the correctness of any algorithm it is necessary
to explicate the connection between the text of the algorithm and the resulting executions, and since states are necessary
for such an explication no correctness proof can do without them. Indeed states are necessary, but my claim here is that
only local states are necessary, and they suffice--we can do without global states.
A local state is a function defined on the local variables and which assigns to each such variable a value in its type.

In order to prove Lemma \ref{FP}, for example, we have to consider the algorithm of the
\Scan\ operation in isolation.
The local state variables of the \Scan\ operation are the variables $k$, $j$, $PC$ (for the program counter),
 and
we also have $N^2+2N$ variables $a_k[j]$ for $0\leq k \leq N+1$ and $1\leq j \leq N$. The values of these $a_k[j]$ variables are
register triples 
with fields $(data, sequence-number, report)$
where $data$ is in \Data, $sequence-number$ is a natural number, and $report$ is an array of length $N$ of \Data\ values 
(see section \ref{Algo}). 
Registers $R_i$ that the \Scan\ operation reads are not among its local state variables. 
This is a characteristics feature of the {\em non-restricted} semantics that we give here to the standalone
\Scan\ semantics. A way to think about it is by realizing that the correctness of Lemma \ref{FP} can be proved even
when the values returned by reads of registers $R_j$ are determined randomly (but within their types).
The resulting semantics is said to be ``unrestricted'' in \cite{abraham}. In the unrestricted semantics, each process
executes its algorithm but the registers that are read return arbitrary values (and the write actions are not recorded
in register variables since the registers are not state variables). The restricted semantics is
is obtained by imposing on the unrestricted semantics the specifications of the registers (atomicity), and the
correctness proof thus relies on the combination of the unrestricted semantics and the specifications of the communication
devices.

\begin{thebibliography}{33}

\bibitem{abraham} U. Abraham. {\em Models for Concurrency}. Gordon
and Breach, (1999).


\bibitem{AtomicSnapshot}Yehuda Afek, Hagit Attiya, Danny Dolev, Eli Gafni, Michael Merritt, and Nir Shavit. 1993.
 Atomic snapshots of shared memory. J. ACM 40, 4 (September 1993), 873-890. 

\bibitem{Multicore}
D. Imbs, M. Raynal, A simple snapshot algorithm for multicore systems. Proceedings of the
5th IEEE Latin-American Symposium on Dependable Computing (LADC’11), 2011 (IEEE
Press, New York, 2011), pp. 17–23



\end{thebibliography}

\end{document}

