\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_1n$). 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