\documentclass[10pt,envcountsame]{llncs}
%\usepackage{enumerate}
\usepackage{wrapfig}
\usepackage{graphicx}
%\usepackage[small,hang]{caption}
%\listfiles % liste de tous les fichiers utilisés
%%% Entêtes articles
\usepackage{amsmath} % font ams
\usepackage{amssymb}
\usepackage{gastex}
\usepackage{xspace} %% gestion des espaces dans les macros
\usepackage{cite}
\renewcommand{\thefootnote}{\roman{footnote}}
\newcommand{\macro}[2]{ \newcommand{#1}{{\ensuremath{#2}}\xspace}}
%%%%%%%%%%%%%%%%%%%% MACROS diverses
\newcommand{\ie}{{i.e.}}
%\input{abbrev-maths.tex}
%\input{abbrev.tex}
\macro{\N}{\mathbb N}
%%%%%%%%%%%%%%%%%%%%%%%%% MACROS symboles math
\newcommand{\bG}{\ensuremath{\mathbf G}\xspace}
\newcommand{\bH}{\ensuremath{\mathbf H}\xspace}
\newcommand{\bK}{\ensuremath{\mathbf K}\xspace}
\usepackage[vlined]{algorithm2e}
\usepackage{algorithmic}
\newcommand{\bT}{\ensuremath{\mathbf T}\xspace}
\newcommand{\zK}{\ensuremath{z_{\mathbf K}}}
\newcommand{\zG}{\ensuremath{z_{\mathbf G}}}
\newcommand{\figdelta}{\delta}
\newcommand{\figgamma}{\gamma}
\macro{\bB}{\ensuremath{\mathbf B}\xspace}
\macro{\ldigraph}{\mathcal{D}_\etiq}
\newcommand{\dist}{\ensuremath{\operatorname{dist}}\xspace}
\newcommand{\cF}{\ensuremath{\mathcal{F}}}
\newcommand{\GG}{\ensuremath{\mathcal G}}
\newcommand{\BB}{\ensuremath{\mathcal B}}
\newcommand{\AB}{\ensuremath{\mathcal B}}
\newcommand{\FF}{\ensuremath{\mathcal F}}
\newcommand{\KK}{\ensuremath{\mathcal K}}
\newcommand{\LL}{\ensuremath{\mathcal L}}
\newcommand{\MM}{\ensuremath{\mathcal M}}
\newcommand{\PP}{\ensuremath{\mathcal P}}
\newcommand{\Pfin}{\ensuremath{\mathcal{P}_{\mathrm{fin}}}}
\newcommand{\II}{\ensuremath{\mathcal I}}
\newcommand{\cS}{\ensuremath{\mathcal S}}
\newcommand{\NN}{\mathcal{N}}
\newcommand{\EE}{\ensuremath{\mathcal E}}
\newcommand{\TT}{\ensuremath{\mathcal T}}
\newcommand{\cA}{\ensuremath{\mathcal A}}
\macro{\mk}{\ensuremath{\mathcal M}}
\newcommand{\fleche}{\longrightarrow}
\renewcommand{\epsilon}{\varepsilon}
\newcommand{\coset}{\ensuremath{^{\mathrm{c}}}}
\newcommand{\ceil}[1]{\mathop\lceil #1 \mathop\rceil}
\newcommand{\NNNN}{\mathcal{P}_{\mathrm{fin}}(\N \times L \times \N^2)\xspace}
\def\card{\mbox{card}} \def\cG{{\cal G}} \def\cC{{\cal C}}
\def\cI{{\cal I}} \def\cT{{\cal T}} \def\cJ{{\cal J}}
\def\ra{\rightarrow}
\macro{\bD}{\ensuremath{\mathbf D}\xspace}
%%%%%%%%% Macros utiles %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\newcommand{\macro}[2]{ \newcommand{#1}{{\ensuremath{#2}}\xspace}}
\macro{\bF}{{\mathbf F}}
\macro{\grs}{\mathrel{{\mathcal R}}}
\macro{\gfam}{\cF}% graph family
%\macro{\N}{\mathbb N}
\newcommand{\Dir}[1]{\ensuremath{\operatorname{Dir}(#1)}\xspace}
\macro{\etiq}{L} % labels set
\newcommand{\lgraph}{\ensuremath{\cG_\etiq}\xspace} % family of all
% labelled graphs
\newcommand{\trees}{{\ensuremath{\mathcal T}}\xspace}
\newcommand{\gmin}{{\ensuremath{\mathcal G_{\mathrm{min}}}}\xspace}
%fonction caractéristique
\newcommand{\car}{\ensuremath{\raisebox{2pt}{\mbox{$\chi$}}}}
\macro{\simtaille}{\sim^{\mbox{\tiny\textsc{Taille}}}}
\newcommand{\fetiq}[1]{\ensuremath{\mbox{\underline{\textsc{#1}}}}\xspace}
% relation de réétiquetage
\newcommand{\RR}{\ensuremath{\mathrel{\mathcal R}}}
% the covering-relation
\newcommand{\covsim}{\ensuremath{\overset{*} \leftrightarrow}}
% booleens
\newcommand{\true}{\textsc{True}\xspace}
\newcommand{\false}{\textsc{False}\xspace}
\newcommand{\monetiq}[1]{\ensuremath{\mbox{\underline{\textsc{#1}}}}}
\newcommand{\yes}{\monetiq{Yes}}
\newcommand{\no}{\monetiq{No}}
\macro{\Z}{\ensuremath{\mathbb Z}\xspace}
\newtheorem{procedur}{Procedure}
\newtheorem{fact}{Fact}
\newcommand{\ignore}[1]{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %% enumeration perso
\newcommand{\romanitems}{\renewcommand{\labelenumii}{(\roman{enumii})}}
\renewcommand{\marginpar}{}
%\renewcommand{\captionfont}{\footnotesize}
%\renewcommand{\captionlabelfont}{\bf \footnotesize}
%\renewcommand{\captionlabeldelim}{.}
%\renewcommand{\belowcaptionskip}{-0.5cm}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%Définition pour précondition etc ....%%%%%%%%%%%%
\newcounter{rrulec}
\newenvironment{rrule}[1]{%
\begin{list}{\therrulec~:} { \usecounter{rrulec}
\newcommand{\therrule}{#1} } } {\end{list}}
\newcommand{\ritem}[4][\therrule\arabic{rrulec}]{
\renewcommand{\therrulec}{#1} \pagebreak[3] \item {\bf #2
}\nopagebreak[4] \begin{itemize} \item[] \underline{\em
Precondition~:} \begin{itemize} #3 \end{itemize} \item[]
\underline{\em Relabeling~:} \begin{itemize} #4 \end{itemize}
\end{itemize}{\vskip 0.5cm} }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%% TITLE
\title{On Snapshots and Stable Properties Detection
in Anonymous Fully Distributed Systems\\
(Extended abstract)
}
\author{J\'er\'emie Chalopin\inst{1} \and Yves M\'etivier\inst{2} \and Thomas Morsellino\inst{2}}
\institute{
LIF, CNRS \& Aix-Marseille Universit\'e\\
39, rue Joliot Curie\\
13453 Marseille Cedex 13, France\\
\texttt{jeremie.chalopin@lif.univ-mrs.fr}
\and
Universit\'e de Bordeaux, LaBRI, UMR CNRS 5800\\
351, cours de la Lib\'eration\\
33405 Talence, France\\
\texttt{\{metivier, morsellino\}@labri.fr}}
\begin{document}
\maketitle
%\pagestyle{plain}
\setcounter{footnote}{0}
\begin{abstract}
Most known snapshot algorithms assume that the vertices of the network have
unique identifiers and/or that there is exactly one initiator. This paper
concerns snapshot computation in an anonymous network and more generally what
stable properties of a distributed system can be computed anonymously with local
snapshots with multiple initiators when knowing an upper bound on the diameter
of the network.
\end{abstract}
\section{Introduction}
%%TMP-\vspace{-0.4cm}
\noindent
{\bf The problem.}
A distributed system $(P,C)$ consists of a collection $P$ of processes and a
communication subsystem $C.$ It is described by a simple connected undirected
graph $G=(V,E),$ where the vertices represent the processes and the edges
represent the bidirectional channels.
A message passing algorithm is defined as follows: to each process is associated
a state and a transition system which can modify the state of the process and
which can interact with the communication subsystem. The events which are
associated with a process are internal events, send events and receive events.
In a send (resp. receive) event a message is produced (resp. consumed).
Let $Q$ be the (recursive) set of possible states of $p.$ Let $\cal M$ be the
set of possible messages. The state of a channel is the multiset of messages
sent through this channel and not yet received. Let $p$ be a process, the {\it
local snapshot} with respect to $p$ is defined by the state of $p$ and by the
states of incoming channels to $p.$
The state of a distributed system $G$, also called its {\it global state,} is
defined by the state of each process and the state of each channel (or
equivalently by the set of local snapshots): it is precisely a {\it (global)
snapshot.} Thus a snapshot of a distributed system is an instantaneous map of
it, where each vertex (resp. each edge) is labelled by its state. It will be
denoted by ${\mathbf G}=(G,\lambda)$ where $\lambda$ is a labelling function
which associates to each vertex (resp. each edge) its state.
By definition, in a fully distributed asynchronous system there is no global
clock and no process has the knowledge of a snapshot; each processor knows, a
priori, only its state. It knows neither the states of the other processors nor
the state of any channel.
Given a distributed system, the aim of a snapshot algorithm is the computation
of such a global state.
As explained by Tel \cite{Tel} (p. 335-336), the construction of
snapshots can be useful to detect stable properties of the distributed
system (properties which remain true as soon as they are verified), to
restart the system from the last known snapshot (and not from the
initial configuration) when the system must be restarted (due to a
failure of a component), or to debug distributed algorithms.
A {\it consistent snapshot} of a distributed system is a global state of the
distributed system or a global state that the system could have reached. Since
the seminal paper of Chandy and Lamport \cite{CL85} which presents an algorithm
to compute a consistent snapshot, many papers give such algorithms according to
the model of the distributed system. They assume that processes have unique
identifiers and/or that there is exactly one initiator. Many papers give also
specific algorithms to detect some specific properties like termination or
deadlock.
Recently, Guerraoui and Ruppert \cite{GR05}, considering that a vast majority of
papers on distributed computing assume that processes have unique identifiers,
ask the following question: {\it What if processes do not have unique
identifiers or do not wish to divulge them for reasons of privacy?}
In this paper, we consider this question in the context of snapshots
computations and by considering stable properties of a distributed system that
can be detected anonymously. Furthermore, we look for fully distributed
solutions which admit several initiators.
\medskip
\noindent
{\bf The Model.}
As we said before, our model is the usual asynchronous message passing model
(\cite{Tel,YKsolvable}). A network is represented by a simple connected graph
$G=(V(G),E(G))=(V,E)$ where vertices correspond to processes and edges to direct
communication links. The state of each process (resp. each link $e$) is
represented by a label $\lambda(v)$ (resp. $\lambda(e)$) associated to the
corresponding vertex $v \in V(G)$ (resp. link $e\in E$); we denote by $\bG =
(G,\lambda)$ such a labelled graph. We assume the network to be anonymous: the
identities of processors are not necessarily unique.
We assume that each process can distinguish the different edges that are
incident to it, i.e., for each $u \in V(G)$ there exists a bijection $\delta_u$
between the neighbors of $u$ in $G$ and $[1,\deg_G(u)]$. We will denote by
$\delta$ the set of functions $\{\delta_u\mid u\in V(G)\}$. The numbers
associated by each vertex to its neighbors are called \emph{port-numbers} and
$\delta$ is called a \emph{port-numbering} of $G$. We will denote by
$(\bG,\delta)$ the labelled graph $\bG$ with the port-numbering $\delta$.
Each process $v$ in the network represents an entity that is capable of
performing computation steps, sending messages via some port and receiving any
message via some port that was sent by the corresponding neighbor. We consider
asynchronous systems, i.e., no global time is available and each computation may
take an unpredictable (but finite) amount of time. Note that we consider only
reliable systems: no fault can occur on processes or communication links. We
also assume that the channels are FIFO, i.e., for each channel, the messages are
delivered in the order they have been sent. In this model, a distributed
algorithm is given by a local algorithm that all processes should execute. A
local algorithm consists of a sequence of computation steps interspersed with
instructions to send and to receive messages.
We follow the presentation and definitions given in \cite{Tel} (p.
45-47) or \cite{Attiya} (p. 10-12).
\medskip
\noindent
{\bf Our Contribution.}
We assume that the network is anonymous and that several processes can be
initiators of computations thus no process of the network can compute a
snapshot, i.e., can know a map of the network with vertices and edges labelled
by states of processes and channels (it is a direct consequence of Theorem 5.5
in \cite{Angluin}). Furthermore we assume that each process knows an upper bound
of the diameter of the network.
First we give a very simple algorithm based on the composition of an algorithm
by Szymanski, Shy, and Prywes \cite{SSPj} with the Chandy-Lamport algorithm
which enables each process:
to detect an instant where all processes have obtained their local
snapshot, and
to associate the same number to all local snapshots.
By this way we obtain two applications: one to checkpoint and rollback recovery
and a second to detect termination of the execution of a distributed algorithm.
Then we prove that some stable properties can be anonymously detected
by proving we can compute a snapshot up to covering (called a weak
snapshot). In some sense, the weak snapshot is the ``global view'' or
the ``maximal knowledge'' of the distributed system that each vertex
can obtain anonymously.
\medskip
\noindent
{\bf Related Work.}
Many notions and algorithms concerning snapshots, stable properties,
checkpointing and rollback recovery can be found in \cite{KS}.
From a theoretical point of view, it is simple to know whether the global state
of a distributed system satisfies a stable property. A distinguished process
starts the Chandy-Lamport algorithm, then it collects states of processes and
states of channels, it computes a map of the network and finally it tests
whether the labelled network satisfies the given property.
To collect or to analyze local snapshots, different assumptions may be done (see
\cite{KRS95}): processes have unique identifiers, there is exactly one initiator
or one collector process.
Some results have been obtained for the computation of snapshots in asynchronous
shared-memory systems that are anonymous : \cite{GR05} (Section 5) gives a
survey. This paper also presents results concerning consensus and timestamping.
The question ``What can be computed anonymously?'' has been explored in the
asynchronous message passing model for the election problem, symmetry breaking
and more generally for computing functions \cite{Angluin,BVelection,JSsimsim,YKsolvable,YKcomputing,YKelection,BV}. Angluin
has introduced the classical proof techniques used for showing impossibilities
based on coverings.
%%TMP-\vspace{-0.4cm}
\section{The Chandy-Lamport Snapshot Algorithm}
%%TMP-\vspace{-0.4cm}
The aim of a snapshot algorithm is to construct a system configuration defined
by the state of each process and the state of each channel.
This section presents the Chandy-Lamport snapshot algorithm
\cite{CL85}; it is presented as Algorithm~\ref{CL}. Each process $p$
is equipped with: a boolean variable $taken_p$ which is initialized to
$false$ that indicates if the process $p$ has already recorded its
state, a boolean variable $local$-$snapshot_p$ initialized to $false$
that indicates if the process $p$ has recorded its state and the state
of incoming channels, and a multiset of messages $M_{p,i},$ initially
$M_{p,i}=\emptyset,$ for each incoming channel $i$ of $p$.
We assume that Algorithm \ref{CL} is initiated by at least one process which:
saves its state, sends a marker on each outcoming port and for each incoming
port memorizes messages which arrive until it receives a marker through this
port. When a process receives for the first time a marker, it does the same
thing that an initiator; the incoming channel by which it receives for the first
time a marker is saved as empty.
\begin{algorithm}[ht!]
{\scriptsize
${\mathbf Init}$-$CL_p:$ \{To initiate the algorithm by at least one process $p$
such that $taken_p=false$\}\\
\Begin{ \KwSty{record}$(\texttt {state}(p))$ ;\\
% $local$-$snapshot:=false;$\\
% $snapshot:=false;$\\
$taken_p:=true;$\\
\KwSty{send}$$ to each neighbor of $p$;\\
For each port $i$ the process $p$ records messages arriving
via $i$
}
\BlankLine
${\mathbf R}$-$CL_p:$ \{A marker has arrived at $p$ via port $j$\}\\
\Begin{ \KwSty{receive}$;$\\
\KwSty{mark} port $j;$\\
\eIf{$not$ $taken_p$}
{%$local$-$snapshot:=false:$\\
% $snapshot:=false;$\\
$taken_p:=true;$\\
\KwSty{record}$(\texttt {state}(p))$ ;\\
\KwSty{send}$$ via each port;\\
For each port $i\not= j$ the process $p$ records messages
arriving via $i$ in $M_{p,i}$
}
{ The process $p$ stops to record messages from the channel $j$ of $p;$\\
\KwSty{record}$(M_{p,j})$ }
\If{$p$ has received a marker via all incoming channels}
{$local$-$snapshot_p:=true$}
}}
\caption{The Chandy-Lamport snapshot algorithm.}
\label{CL}
\end{algorithm}
If we consider an execution of the Chandy-Lamport algorithm we obtain a
consistent snapshot within finite time after its initialization by at least one
process (see \cite{Tel} Theorem 10.7 ). In particular:
\begin{fact}\label{cl}
Within finite time after the initialization of the Chandy-Lamport algorithm,
each process $p$ has computed its local snapshot ($local$-$snapshot_p=true$).
\end{fact}
Once the computation of local snapshots is completed (for each process $p$ the
boolean $local$-$snapshot_p$ is true), the knowledge of the snapshot is
fully distributed over the system. The next question is ``how to exploit this
distributed knowledge?''.
A first answer is obtained by the construction of the global state of the system
centralized on a process. As is explained by Raynal \cite{RMIT}: {\it Providing
an algorithm for the calculation of a global state is a basic problem in
distributed systems.} Several assumptions can be done to obtain a global state:
exactly one initiator for the Chandy-Lamport algorithm, processes have unique
identifiers or global colors associated to each computation of a global state...
A global clock can be simulated by local logical clocks \cite{RMIT},
nevertheless it does not enable iterated computations of snapshots.
Another way to exploit the local knowledge is based on wave algorithms: a
message is passed to each process by a single initiator following the topology
of the network or a virtual topology (ring, tree, complete graph, ...), see
\cite{Matocha}.
These solutions are not available in the context of anonymous networks with no
distinguished process and no particular topology.
\section{Termination Detection of the Chandy-Lamport Snapshot Algorithm}
A first problem is the termination detection of the computation of all local
snapshots. It requires that all vertices certify, in a finite computation, that
they have completed the computation of the local snapshot. The algorithm by
Szymanski, Shy, and Prywes (the SSP algorithm for short) \cite{SSPj} does this
for a region of pre-specified diameter. The algorithm assumes that an upper
bound of the diameter of the entire network is known by each process. In the
sequel this upper bound is denoted by $\beta$ and we assume that each process
knows it. Now, we present the SSP algorithm we use in this paper.
\medskip
\noindent
{\bf The SSP algorithm.}
We consider a distributed algorithm which terminates when all processes reach
their local termination conditions. Each process is able to determine only its
own termination condition. SSP's algorithm detects an instant in which the
entire computation is achieved.
Let $G$ be a graph, to each process $p$ is associated a predicate $P(p)$ and an
integer $a(p).$ Initially $P(p)$ is false and $a(p)$ is equal to $-1.$
Transformations of the value of $a(p)$ are defined by the following rules.
Each local computation acts on the integer $a(p_0)$ associated to the
process $p_0;$ the new value of $a(p_0)$ depends on values associated
to neighbors of $p_0.$ More precisely, let $p_0$ be a process and let
$\{p_1,...,p_d\}$ the set of processes adjacent to $p_0.$ If
$P(p_0)=false$ then $a(p_0)=-1;$ if $P(p_0)=true$ then $a(p_0)= 1 +
Min\{a(p_k) \mid 1\leq k \leq d\}.$ We assume that for each process
$p$ the value of $P(p)$ eventually becomes true and remains true for
ever. To apply the SSP algorithm, the label of each process has two
items:
\begin{itemize}
\item $a(p) \in \Z$ is a counter and initially $a(p) = -1$, $a(p)$
represents the distance up to which all processes have the predicate
true;
\item $A(p) \in {\mathcal{P}_{\mathrm{fin}}(\N\times
\Z)}$\footnote{For any set $S$, ${\mathcal{P}_{\mathrm{fin}}(S)}$
denotes the set of finite subsets of $S.$} encodes the information
$p$ has about the values of $a(q)$ for each neighbor $q$. Initially,
$A(p)=\{(i,-1)\mid i \in [1,\deg_G(p)]\}$.
\end{itemize}
%% A precise desciption is given as Algorithm \ref{SSPA}.
%% \begin{algorithm}[ht!]
%% {\scriptsize
%% ${\mathbf Init}$-$SSP_p:$ \{To initiate termination detection on the process $p$
%% such that $P(p)=true$ \}\\
%% \Begin{ $a(p):=0;$\\
%% $m:=Min\{x\mid (i,x)\in A(p)\};$\\
%% \If{$m\geq a(p)$}
%% { $a(p):=m+1$ \;}
%% \KwSty{send}$$ to each neighbor of $p$\\
%% }
%% \BlankLine
%% ${\mathbf R}$-$SSP_p:$ \{An integer $<\alpha>$ has arrived at $p$ via port $j$\}\\
%% \Begin{ \KwSty{receive}$<\alpha>;$\\
%% $A(p):=(A(p)\setminus\{(j,x)\})\cup\{(j,\alpha)\};$\\
%% $m:=Min\{x\mid (i,x)\in A(p)\};$\\
%% \If{$(m\geq a(p)$ and $P(p)=true)$}
%% { $a(p):=m+1;$\\}
%% \eIf{$a(p)\geq\beta$}
%% { $p$ detects the entire termination: the predicate $P$ is true
%% for each process
%% }
%% {\KwSty{send}$$ via each port}
%% }}
%% \caption{The SSP algorithm.}
%% \label{SSPA}
%% \end{algorithm}
We consider an execution $\mathcal E$ of the SSP's algorithm on the
graph $\mathbf G$ and $(a_i(p))_{i\geq 0}$ the sequence defined by the
values of $a(p)$ for the execution $\mathcal E$. The predicate $P$ is
true for each process of the ball of radius $a_i(p)$ with center $p,$
i.e.:
\begin{proposition}\label{SSP}
Let $p$ be a process of $G,$ we suppose that $h=a_i(p)\geq 0.$
Then for each $q\in V(G), d(p,q)\leq h \Rightarrow a_i(q)
\geq 0$. \end{proposition}
Thus a process $p$ such that $a(p)$ is greater or equal than the
diameter of the graph knows that for each process $q$ of the graph
$P(q)$ is true, i.e., it detects the termination of the algorithm.
\subsection{An Algorithm to Detect Termination of the Local Snapshots
Computation.}
Now, we compose the application of the Chandy-Lamport algorithm and the SSP
algorithm to enable each process to detect an instant where all processes have
completed the computation of their local snapshot: it is given as Algorithm
\ref{TDCL}.
Since we want the algorithm to be able to compute snapshots at
different times in the execution, we add a variable
$snapshot$-$number_p$ which indicates the number of the snapshot
(initially, $snapshot$-$number_p=0$). This variable is not really
necessary in this section, but it will be used in the sequel.
Here, a process starts executing the SSP algorithm once it has
computed its $p$th local snapshot, i.e., when $local$-$snapshot_p$ is
true.
%% To apply the SSP algorithm, we add to the label of each process three items:
%% \begin{itemize}
%% \item $a(p) \in \Z$ is a counter and initially $a(p) = -1$. In some sense,
%% $a(p)$ represents the distance up to which all processes have completed the
%% computation of the local snapshot;
%% \item $A(p) \in {\mathcal{P}_{\mathrm{fin}}(\N\times \Z)}$ encodes the
%% information $p$ has about the values of $a(q)$ for each neighbor $q$. Initially,
%% $A(p)=\{(i,-1)\mid i \in [1,\deg_G(p)]\}$;
%% \end{itemize}
%% If a process has completed the computation of its local snapshot then it changes
%% the value of $a(p)$ to $0$ and it informs its neighbors. When a process $p$
%% receives a value $a(q)$ for some neighbor $q$ via the port $i$ then it
%% substitutes the new value $(i,a(q))$ to the old value $(i,x)$ in $A(p).$
%% Finally, $p$ computes the new value $a(p)=1+Min\{x \mid (i,x)\in A(p)\}.$
A process $p$ knows that each process has completed the computation of its local
snapshot as soon as $a(p)\geq \beta$ (we recall that $\beta$ is an upper bound
of the diameter of the network). Thus we add a boolean variable $snapshot$
initialized to false; it indicates if the process knows whether all processes
have completed the computation of the local snapshots.
\begin{algorithm}[ht!]
{\scriptsize
${\mathbf Init}$-$SSP_p:$ \{To initiate termination detection on the process $p$
such that $local$-$snapshot_p=true,$ $a(p)=-1$ and $snapshot=false$\}\\
\Begin{ $a(p):=0;$\\
$m:=Min\{x\mid (i,x)\in A(p)\};$\\
\If{$m\geq a(p)$}
{ $a(p):=m+1$ \;}
\KwSty{send}$$ to each neighbor of $p$
}
\BlankLine
${\mathbf R}$-$SSP_p:$ \{An integer $<\alpha>$ has arrived at $p$ via port $j$\}\\
\Begin{ \KwSty{receive}$<\alpha>;$\\
$A(p):=(A(p)\setminus\{(j,x)\})\cup\{(j,\alpha)\};$\\
$m:=Min\{x\mid (i,x)\in A(p)\};$\\
\If{$(m\geq a(p)$ and $local$-$snapshot_p=true)$}
{ $a(p):=m+1;$}
\eIf{$a(p)\geq\beta$}
{ $snapshot$-$number_p:=snapshot$-$number_p+1;$\\
$snapshot_p:=true$}
{ \KwSty{send}$$ via each port}
}}
\caption{Termination detection of the Chandy-Lamport snapshot algorithm.}
\label{TDCL}
\end{algorithm}
\begin{proposition}
let $(G,\lambda)$ be a network. Let $\beta$ be an upper bound of the diameter of
$G$ known by each process. Within finite time after the initialization of the
Chandy-Lamport algorithm, Algorithm \ref{TDCL} enables each process to know an
instant where all processes have completed the computation of their local
snapshots.
\end{proposition}
\section{Two Applications: ``Checkpoint and Rollback Recovery'' and
``Termination Detection''}
%%TMP-\vspace{-0.4cm}
This section presents two simple applications of the Chandy-Lamport algorithm
and of Algorithm \ref{TDCL} in the anonymous context, without unicity of an
initiator and assuming that each process knows an upper bound of the diameter of
the network:
1. to compute configurations to restart the system when a process fails (see
\cite{KS} Chapter 13 for a presentation of checkpointing and rollback recovery),
2. to detect the termination of an execution of a distributed algorithm.
\medskip
\noindent
{\bf An Application to Checkpoint and Rollback Recovery.}
A snapshot enables to restart a system if there is a failure. As explained in
\cite{KS} p. 456, {\it the saved state is called a checkpoint, and the procedure
of restarting from a previously checkpointed state is called rollback recovery.}
Our solution is obtained
by repeatedly executing the following steps:
\begin{enumerate}
\item at least one process initiates the Chandy-Lamport algorithm (Algorithm
\ref{CL});
\item each process $p$ detects an instant where the computation of its local
snapshot is completed: $local$-$snapshot_p=true;$
\item each process $p$ detects an instant where the computation of all local
snapshots is completed: $snapshot_p=true$ (Algorithm \ref{TDCL});
\item a new number (obtained by adding $1$ to the counter $snapshot$-$number_p$,
initially $snapshot$-$number_p=0$) is associated to this snapshot and each
process $p$ gives this number to its local snapshot. Each process $p$ saves its
last local snapshot associated to the number $snapshot$-$number_p.$ It enables
to restart if there is a failure.
\item Finally, variables for Algorithm \ref{CL} and Algorithm \ref{TDCL} are
reset at the end.
\end{enumerate}
\smallskip
\noindent
{\bf From Local Snapshots Computation to Termination Detection of the
Execution of a Distributed Algorithm.}
Let $\mathcal A$ be a distributed algorithm. Let $\mathcal E$ be an execution of
$\mathcal A.$ Our aim is to detect the termination of $\mathcal E$.
An execution $\mathcal E$ has terminated if and only if all the processes are
passive and all the channels are empty. Thus to detect the termination of the
execution $\mathcal E,$ it suffices that from time to time (to be defined) at
least one process initializes the computation of a snapshot and if its state is
passive and its incoming channels are empty it must detect if the same property
holds for all the processes. This is done by using an occurence of the SSP
algorithm. If variables of a process $p$ indicate that the execution is not
completed then $q$ emits a signal through the network to inform each process.
In this way, we obtain an algorithm to detect global termination of the
execution of a distributed algorithm. These repeated termination queries are
analogue to the solution described by Santoro in Section 8.3 of \cite{Santoro}.
\section{Coverings, Stable Properties and Weak Snapshots}
%%TMP-\vspace{-0.4cm}
We assume that the network is anonymous and that several processes can be
initiators of computations. Each process knows only an upper bound of the
diameter, denoted $\beta.$ Under these hypotheses, no process can compute a map
of the network. We prove that each process can compute a graph covered by the
network, i.e., a weak snapshot. We prove also that classical properties, as
stable properties, studied through snapshots can be still studied thanks to a
weak snapshot.
In the following, we will consider directed graphs (digraphs) with multiple arcs
and self-loops. A \emph{digraph} $D=(V(D),A(D),s_D,t_D)$ is defined by a set
$V(D)$ of vertices, a set $A(D)$ of arcs and by two maps $s_D$ and $t_D$ that
assign to each arc two elements of $V(D)$: a source and a target (in general,
the subscripts will be omitted).
A \emph{symmetric} digraph $D$ is a digraph endowed with a symmetry, that is, an
involution $Sym: A(D) \rightarrow A(D)$ such that for every $a \in A(D),
s(a)=t(Sym(a))$. In a symmetric digraph $D$, the degree of a vertex $v$ is
$\deg_D(v) = |\{a \mid s(a)=v\}| = |\{a \mid t(a) = v\}|.$
Let $(G,\lambda)$ be a labelled graph with the port-numbering $\delta.$ We will
denote by $(\Dir{\bG},\delta)$ the symmetric labelled digraph
$(\Dir{G},(\lambda,\delta))$ constructed in the following way. The vertices of
$\Dir{G}$ are the vertices of $G$ and they have the same labels in $\bG$ and in
$\Dir{\bG}$. Each edge $\{u,v\}$ of $G$ is replaced in $(\Dir{\bG},\delta)$ by
two arcs $a_{(u,v)}, a_{(v,u)} \in A(\Dir{G})$ such that $s(a_{(u,v)}) =
t(a_{(v,u)}) = u$, $t(a_{(u,v)}) = s(a_{(v,u)}) = v$, $\delta(a_{(u,v)}) =
(\delta_u(v),\delta_v(u))$ and $\delta(a_{(v,u)}) = (\delta_v(u),\delta_u(v))$.
Note that this digraph does not contain multiple arcs or loop.
\begin{figure}
\centering
\includegraphics[width=\textwidth]{revetement.pdf}
\caption{A graph $G$, the corresponding digraph $Dir(G)$ and a digraph
$D'$ such that $Dir(G)$ is a symmetric covering of $D'$.}
\end{figure}
The notion of coverings and of symmetric coverings are fundamental in this work;
definitions and main properties are presented in \cite{GT87,BVfibrations}. This
notion enables to express ``similarity'' between two digraphs.
A labelled digraph $\bD$ is a \emph{covering} of a labelled digraph $\bD'$ via
$\varphi$ if $\varphi$ is a homomorphism from $\bD$ to $\bD'$ such that for each
arc $a' \in A(D')$ and for each vertex $v \in \varphi^{-1}(t(a'))$ (resp. $v \in
\varphi^{-1}(s(a'))$, there exists a unique arc $a \in A(D)$ such that $t(a)=v$
(resp. $s(a) = v$) and $\varphi(a)=a'$.
A symmetric labelled digraph $\bD$ is a \emph{symmetric covering} of a symmetric
labelled digraph $\bD'$ via $\varphi$ if $\bD$ is a covering of $\bD'$ via
$\varphi$ and if for each arc $a \in A(D)$, $\varphi(Sym(a)) = Sym(\varphi(a))$.
The homomorphism $\varphi$ is a \emph{symmetric covering projection} from $\bD$
to $\bD'$.
Given a simple connected labelled graph $\bG =(G,\lambda)$ with a port-numbering
$\delta$ which defines a snapshot of a network $G$. Let $\bD=(\Dir{\bG},\delta)$
be the corresponding labelled digraph $(\Dir{G},(\lambda,\delta)).$ Let $\bD'$
be a labelled digraph such that $\bD=(\Dir{\bG},\delta)$ is a covering of
$\bD'.$ The labelled digraph $\bD'$ is called a weak snapshot of $G.$
Let $\mathbf G$ be a graph. Let $\mathcal D$ be a message passing algorithm and
let $\mathcal E$ be an execution of $\mathcal D$ over $\mathbf G.$
A property $P$ of configurations of $\mathcal E$ is stable: if $P$ is true
for a configuration $({\texttt {state}},M)$ then $P$ is true for any
configuration obtained from $({\texttt {state}},M).$
Among stable properties of distributed systems detected with snapshot, we
consider: termination, deadlock, loss of tokens and garbage collection (see
\cite{Tel,Santoro,KS}).
\noindent
{\bf Termination:}
An execution $\mathcal E$ has terminated if and only if all processes are
passive and channels are empty. The link of this property with the computation of a snapshot has been treated in Section 4.
\noindent
{\bf Deadlock:}
A deadlock happens in a distributed system if there is a cycle of processes each
waiting for the next in the cycle with no message in transit. It can be detected
by constructing the {\it wait-for-graph} (WFG for short): vertices are processes
and there is an arc from the vertex (process) $p$ to the vertex $q$ if $p$ is
blocked and is waiting for $q.$ There is a deadlock if and only if there exists
a cycle in the WFG (see \cite{Santoro,KS}).
\noindent
{\bf Loss of Tokens:} Some distributed systems need that tokens
circulate among processes. In order to check if the number of tokens
existing in the system is correct, it may be interesting to check
properties like ``there are exactly $k$ tokens'' or ``there are at
most $k$ tokens''; these properties are stable.
\noindent
{\bf Garbage Collection:} The aim is to decide if an object is
useful.We follow the presentation of Schiper and Sandoz \cite{SS}: Consider a system composed of a set of objects $O$, and a static subset $Root\subseteq O,$ called root objects. Root objects are invoked by some processes. An invocation
on object $o_i$ implies the execution of actions by $o_i.$ The set of objects
can be represented as a set of processes exchanging messages upon invocation,
and messages can carry references.
On the set $O$ of objects, define the descendant relation by: descendent
$(o_i,o_j)$ if object $o_i$ holds a reference on object $o_j$ or a reference on
$o_j$ is under way to $o_i.$ An object $o_i$ is reachable either if $o_i\in
Root$ or if $o_i$ is descendant of a reachable object. By definition an object
is useful if it is reachable. Only reachable object can send references to other
objects. An object that is no more reachable in the system is called garbage and
should be destroyed.
Thus reachable objects are detected as vertices $o$ for which there is a walk
from a root to $o.$
\medskip
\noindent
{\bf Stable properties and Snapshots.}
Usually, after the computation of a snapshot, stable properties are verified by
using a spanning tree or an embedded ring; they also may be verified in a
centralized way by computing on a vertex a map of the network each vertex and
each channel being labelled with its state.
These solutions are no longer possible in an anonymous network with no
distinguished vertex. In this context, the tool we use is covering.
\medskip
\noindent
{\bf Stable Properties in Distributed Systems and Weak Snapshot.}
Let $\mathbf D_1$ and $\mathbf D_2$ be two labelled digraphs such that $\mathbf
D_1$ is a covering of $\mathbf D_2$ via the homorphism $\varphi.$ A lift of a
walk $W_2$ in $\mathbf D_2$ is a walk $W_1$ in $\mathbf D_1$ such that $\varphi$
maps the arcs of $W_1$ onto the arcs of $W_2$ in the order of traversal.
Let $(\mathbf G,\delta)$ be a network with a port numbering $\delta.$ Let
$\mathbf D'$ be a labelled graph such that $(Dir(\mathbf G),\delta)$ is a
covering of $\mathbf D'.$
With our notations, Theorem 2.4.1 and Theorem 2.4.3 in \cite{GT87} can be
translated by:
\begin{enumerate}
\item Let $W$ be a walk in $\mathbf D'$ such that the initial vertex is $u.$
Then for each $u_i$ in $\varphi^{-1}(u)$ there is a unique lift of $W$ that
starts at $u_i.$
\item Let $C$ be a cycle in $\mathbf D'.$ Then $\varphi^{-1}(C)$ is an union of
cycles.
\end{enumerate}
From these two results, we deduce that if $\mathbf D_1$ is a covering
of $\mathbf D_2$ then deadlock and garbage detected in $\mathbf D_1$
can be detected in $\mathbf D_2.$ We recall that if $\mathbf D_1$ is a
covering of $\mathbf D_2$ via the homorphism $\varphi$ then there
exists an integer $\alpha$ such that for each vertex $u$ of $\mathbf
D_2$ the cardinality of $\varphi^{-1}(u)$ is equal to $\alpha.$ Thus
if there are $c_1$ tokens in $\mathbf D_1$ (for a non negative integer
$c_1$) then there are $c_2=c_1/\alpha$ tokens in $\mathbf D_2.$ From
this, we deduce that if the size of $\mathbf D_1$ is known then the
knowledge of $\mathbf D_2$ enables to detect loss of tokens in
$\mathbf D_2$. These facts are summarized by:
\begin{proposition}\label{prop:weak-snap}
Let $G$ be a distributed system. From any weak snapshot $\bD$ of $G$,
one can detect deadlock and termination and one can perform garbage
collection. Furthermore, if the processes know the size of $G$ then
loss of tokens can also be detected from a weak snapshot.
\end{proposition}
%%TMP-\vspace{-0.2cm}
%% Knowing an upper bound of the diameter of an anonymous network
%% $\mathbf D_1$ , we describe briefly a fully distributed algorithm (it
%% may admit several initiators) with termination detection, which
%% computes $\mathbf D_2$ such that $\mathbf D_1$ is a covering of
%% $\mathbf D_2$.
In the following, we describe a fully distributed algorithm (it may
admit several initiators) with termination detection, which computes
$\mathbf D_2$ such that $\mathbf D_1$ is a covering of $\mathbf D_2$.
Using such an algorithm, from Proposition~\ref{prop:weak-snap}, we can
solve stable properties detection. It suffices that:
\begin{enumerate}
\item at least one process initiates the Chandy-Lamport algorithm
(Algorithm \ref{CL});
\item each process detects an instant where the computation of all
local snapshots is completed (Algorithm~\ref{TDCL});
\item at least one process initiates the computation of a weak snapshot;
\item each process detects an instant where the computation of the weak snapshot
is completed and decides about the stable property.
\end{enumerate}
%%TMP-\vspace{0.8cm}
\medskip
\noindent
{\bf Computing Anonymously a Weak Snapshot.} Let $(\mathbf G,\delta)$
be a labelled graph with a port numbering $\delta$. We assume that
$\mathbf G$ is anonymous and each vertex of $G$ knows an upper bound,
denoted $\beta$, of the diameter of $G.$ There exists an algorithm,
denoted $\mk_{W-S}$, which computes a weak snapshot, i.e., a labelled
digraph $(\mathbf D,\delta')$ such that $(Dir(\mathbf G),\delta)$ is a
covering of $(\mathbf D,\delta')$. In some sense, the weak snapshot
$(\mathbf D,\delta')$ is the ``global view'' or the ``maximal
knowledge'' of the distributed system that each vertex can obtain
(\cite{Angluin}, Theorem 5.5). If processes know an upper bound of the
diameter of the network then they can detect the termination of
$\mk_{W-S}$. This algorithm has been presented in
\cite{Cthese,CMasynj} as an election algorithm when it is executed on
minimal graphs for the symmetric-covering relation (the graph
$(\mathbf G,\delta)$ is minimal if when $(Dir(\mathbf G),\delta)$ is a
symmetric-covering of $(\mathbf D,\delta')$ then $(Dir(\mathbf
G),\delta)$ is isomorphic to $(\mathbf D,\delta')$). This algorithm is
based on another election algorithm given by Mazurkiewicz in
\cite{Mazur2} and the SSP algorithm. During the execution of the
algorithm, each vertex $v$ attempts to get an identity which is a
number between $1$ and $|V(G)|$. Once a vertex $v$ has chosen a number
$n(v)$, it sends it to each neighbor $u$ with the port-number
$\delta_v(u)$. When a vertex $u$ receives a message from one neighbor
$v$, it stores the number $n(v)$ with the port-numbers $\delta_u(v)$
and $\delta_v(u)$. From all information it has gathered from its
neighbors, each vertex can construct its \emph{local view} (which is
the set of numbers of its neighbors associated with the corresponding
port-numbers). Then, a vertex broadcasts its number, its label and its
mailbox (which contains a set of {\em local views}). If a vertex $u$
discovers the existence of another vertex $v$ with the same number
then it should decide if it changes its identity. To this end it
compares its local view with the local view of $v$. If the label of
$u$ or the local view of $u$ is ``weaker'', then $u$ picks another
number --- its new temporary identity --- and broadcasts it again with
its local view. At the end of the computation, each vertex has
computed a graph $(\mathbf D,\delta')$ such that $(Dir(\mathbf
G),\delta)$ is a symmetric covering of $(\mathbf D,\delta').$
\newcommand{\etalchar}[1]{$^{#1}$}
\begin{thebibliography}{BCG{\etalchar{+}}96}
\bibitem[Ang80]{Angluin}
D.~Angluin.
\newblock Local and global properties in networks of processors.
\newblock In {\em Proceedings of the {12th} Symposium on Theory of Computing},
pages 82--93, 1980.
\bibitem[AW04]{Attiya}
H.~Attiya and J.~Welch.
\newblock {\em Distributed computing: fundamentals, simulations, and advanced
topics}.
\newblock John Wiley \& Sons, 2004.
\bibitem[BCG{\etalchar{+}}96]{BVelection}
P.~Boldi, B.~Codenotti, P.~Gemmell, S.~Shammah, J.~Simon, and S.~Vigna.
\newblock Symmetry breaking in anonymous networks: Characterizations.
\newblock In {\em Proc. 4th Israeli Symposium on Theory of Computing and
Systems}, pages 16--26. IEEE Press, 1996.
\bibitem[BV99]{BV}
P.~Boldi and S.~Vigna.
\newblock Computing anonymously with arbitrary knowledge.
\newblock In {\em Proceedings of the 18th ACM Symposium on principles of
distributed computing}, pages 181--188. ACM Press, 1999.
\bibitem[BV02]{BVfibrations}
P.~Boldi and S.~Vigna.
\newblock Fibrations of graphs.
\newblock {\em Discrete Math.}, 243:21--66, 2002.
\bibitem[Cha06]{Cthese}
J.~Chalopin.
\newblock {\em Algorithmique distribu{\'e}e, calculs locaux et homorphismes de
graphes}.
\newblock PhD thesis, universit{\'e} Bordeaux 1, 2006.
\bibitem[CL85]{CL85}
K.~M. Chandy and L.~Lamport.
\newblock Distributed snapshots: Determining global states of distributed
systems.
\newblock {\em ACM Trans. Comput. Syst.}, 3(1):63--75, 1985.
\bibitem[CM07]{CMasynj}
J.~Chalopin and Y.~M{\'e}tivier.
\newblock An efficient message passing election algorithm based on
mazurkiewicz's algorithm.
\newblock {\em Fundam. Inform.}, 80(1-3):221--246, 2007.
\bibitem[GR05]{GR05}
R.~Guerraoui and E.~Ruppert.
\newblock What can be implemented anonymously?
\newblock In {\em DISC}, pages 244--259, 2005.
\bibitem[GT87]{GT87}
J.~L. Gross and T.~W. Tucker.
\newblock {\em Topological graph theory}.
\newblock Wiley Interscience, 1987.
\bibitem[JS85]{JSsimsim}
R.E. Johnson and F.B. Schneider.
\newblock Symmetry and similarities in distributed systems.
\newblock In {\em Proc. 4th conf. on Principles of Distributed Computing},
pages 13--22, 1985.
\bibitem[KRS95]{KRS95}
A.~D. Kshemkalyani, M.~Raynal, and M.~Singhal.
\newblock An introduction to snapshot algorithms in distributed computing.
\newblock {\em Distributed Systems Engineering}, 2(4):224--233, 1995.
\bibitem[KS08]{KS}
A.~D. Kshemkalyani and M.~Singhal.
\newblock {\em Distributed computing}.
\newblock Cambridge, 2008.
\bibitem[Maz97]{Mazur2}
A.~Mazurkiewicz.
\newblock Distributed enumeration.
\newblock {\em Inf. Processing Letters}, 61:233--239, 1997.
\bibitem[MC98]{Matocha}
J.~Matocha and T.~Camp.
\newblock A taxonomy of distributed termination detection algorithms.
\newblock {\em Journal of Systems and Software}, 43(3):207--221, 1998.
\bibitem[Ray88]{RMIT}
M.~Raynal.
\newblock {\em Networks and distributed computation}.
\newblock MIT Press, 1988.
\bibitem[San07]{Santoro}
N.~Santoro.
\newblock {\em Design and analysis of distributed algorithm}.
\newblock Wiley, 2007.
\bibitem[SS94]{SS}
A.~Schiper and A.~Sandoz.
\newblock Strong stable properties in distributed systems.
\newblock {\em Distributed Computing}, 8(2):93--103, 1994.
\bibitem[SSP85]{SSPj}
B.~Szymanski, Y.~Shy, and N.~Prywes.
\newblock Synchronized distributed termination.
\newblock {\em IEEE Transactions on software engineering},
SE-11(10):1136--1140, 1985.
\bibitem[Tel00]{Tel}
G.~Tel.
\newblock {\em Introduction to distributed algorithms}.
\newblock Cambridge University Press, 2000.
\bibitem[YK96a]{YKcomputing}
M.~Yamashita and T.~Kameda.
\newblock Computing functions on asynchronous anonymous networks.
\newblock {\em Math. Systems Theory}, 29:331--356, 1996.
\bibitem[YK96b]{YKsolvable}
M.~Yamashita and T.~Kameda.
\newblock Computing on anonymous networks: Part i - characterizing the solvable
cases.
\newblock {\em IEEE Transactions on parallel and distributed systems},
7(1):69--89, 1996.
\bibitem[YK99]{YKelection}
M.~Yamashita and T.~Kameda.
\newblock Leader election problem on networks in which processor identity
numbers are not distinct.
\newblock {\em IEEE Transactions on parallel and distributed systems},
10(9):878--887, 1999.
\end{thebibliography}
\end{document}