% The Chicago Journal of Theoretical Computer Science, Volume 1998, Article 3
% Published by MIT Press, Cambridge, Massachusetts USA
% Copyright 1998 by Massachusetts Institute of Technology
%
\newtoks\rstyle
\rstyle={cjlook}
%
\documentclass[v1.1,published]{cjstruct}
%
% Local style resources for this article.
%
\usestyleresource{amstex,psfig}
%
% Local macro definitions for this article.
%
\catcode`\@=11
\ifx\nopagebreakbeginpar\undeftex
\newcommand{\nopagebreakbeginpar}{\@beginparpenalty10000}
\fi
\ifx\nopagebreakendpar\undeftex
\newcommand{\nopagebreakendpar}{\@endparpenalty10000}
\fi
\ifx\nopagebreakinteritem\undeftex
\newcommand{\nopagebreakinteritem}{\@itempenalty10000}
\fi
\catcode`\@=12
%
\newcommand{\prooffontshape}{\fontshape{n}\selectfont}
%
\newcommand{\setof}[2]{\left\{\,#1:#2\,\right\}}
\def\registered{\({}^{\ooalign%
{\hfil\raise.07ex\hbox{{\tiny\textup{R}}}%
\hfil\crcr\scriptsize\mathhexbox20D\cr}}\)}
\tolerance=9000
%
% end of local macro definitions for this article
%
\begin{document}
%
\begin{articleinfo}
%
\publisher{The MIT Press}
%
\publishercomment{%
{\Large
\begin{center}
Volume 1998, Article 3\\
\textit{7 December 1998}
\end{center}
}
\par\noindent
ISSN 1073--0486\@. MIT Press Journals, Five Cambridge Center,
Cambridge, MA
02142-1493 USA; (617)253-2889;
\emph{journals-orders@mit.edu, journals-info@mit.edu}\@.
Published one article at a time in \LaTeX\ source form on the
Internet\@. Pagination varies from copy to copy\@. For more
information and other articles see:
\begin{itemize}
\item \emph{http://mitpress.mit.edu/CJTCS/}
\item \emph{http://www.cs.uchicago.edu/publications/cjtcs/}
\item \emph{ftp://mitpress.mit.edu/pub/CJTCS}
\item \emph{ftp://cs.uchicago.edu/pub/publications/cjtcs}
\end{itemize}
\sentence
\par\noindent
The \emph{Chicago Journal of Theoretical Computer Science} is
abstracted or indexed in \emph{Research Alert,\registered
SciSearch,\registered Current Contents\registered/Engineering
Computing \& Technology}, and \emph{CompuMath Citation
Index\@.\registered}
}
%
\copyrightstmt{%
\copyright 1998 The Massachusetts Institute of Technology\@.
Subscribers are licensed to use journal articles in a variety of
ways, limited only as required to insure fair attribution to authors
and the journal, and to prohibit use in a competing commercial
product\@. See the journal's World Wide Web site for further
details\@. Address inquiries to the Subsidiary Rights Manager, MIT
Press Journals; (617)253-2864;
\emph{journals-rights@mit.edu}\@.\pagebreak[2]
}
%
\journal{Chicago\nolinebreak[1] Journal of Theoretical
Computer\nolinebreak[1] Science}
\journalcomment{%
The \emph{Chicago Journal of Theoretical Computer Science}
is a peer-reviewed scholarly journal in theoretical computer
science\@. The journal is committed to providing a forum for
significant results on theoretical aspects of all topics in computer
science\@.
\par
\begin{trivlist}
\item[\emph{Editor in chief:}] Janos Simon
\item[\emph{Consulting editors:}]
Joseph Halpern, Stuart A.\ Kurtz, Raimund Seidel
\item[\emph{Editors:}]
\begin{tabular}[t]{lll}
Martin Abadi & Greg Frederickson & John Mitchell \\
Pankaj Agarwal & Andrew Goldberg & Ketan Mulmuley \\
Eric Allender & Georg Gottlob & Gil Neiger \\
Tetsuo Asano & Vassos Hadzilacos & David Peleg \\
Laszl\'o Babai & Juris Hartmanis & Andrew Pitts \\
Eric Bach & Maurice Herlihy & James Royer \\
Stephen Brookes & Ted Herman & Alan Selman \\
Jin-Yi Cai & Stephen Homer & Nir Shavit \\
Anne Condon & Neil Immerman & Eva Tardos \\
Cynthia Dwork & Howard Karloff & Sam Toueg \\
David Eppstein & Philip Klein & Moshe Vardi \\
Ronald Fagin & Phokion Kolaitis & Jennifer Welch \\
Lance Fortnow & Stephen Mahaney & Pierre Wolper \\
Steven Fortune & Michael Merritt
\end{tabular}
\vspace{1ex}
\item[\emph{Managing editor:}] Michael J.\ O'Donnell
\vspace{1ex}
\item[\emph{Electronic mail:}] \emph{chicago-journal@cs.uchicago.edu}
\end{trivlist}
\sentence
}
%
\bannerfile{cjtcs-banner.tex}
%
\volume{1998}
%
\articleid{3}
%
\selfcitation{
@article{cj98-03,
author={Yehuda Afek and Anat Bremler},
title={Self-Stabilizing Unidirectional Network Algorithms by
Power Supply},
journal={Chicago Journal of Theoretical Computer Science},
volume={1998},
number={3},
publisher={MIT Press},
month={December},
year={1998}
}
}
%
\begin{retrievalinfo}
\end{retrievalinfo}
%
\title{Self-Stabilizing Unidirectional Network Algorithms by Power Supply}
\shorttitle{Self-Stabilizing Algorithms}
%
\begin{authorinfo}
%
% Correction to error in cjstruct.sty version 1.1.
%
\def\fixversion{1.1}
\ifx\cjversion\fixversion
\renewcommand{\printname}[1]{
\global\authorstring={#1}
\global\authorstrue
\ifinfo\item Printed name: #1\fi
}
\fi
%
% End of correction.
%
\printname{Yehuda Afek}
\collname{}{Afek, Yehuda}
\begin{institutioninfo}
\instname{Tel-Aviv University}
\department{Department of Computer Science}
\address{}{}{}{Israel}{69978}
\end{institutioninfo}
\email{afek@math.tau.ac.il}
\end{authorinfo}
\begin{authorinfo}
\printname{Anat Bremler}
\collname{}{Bremler, Anat}
\begin{institutioninfo}
\instname{Tel-Aviv University}
\department{Department of Computer Science}
\address{}{}{}{Israel}{69978}
\end{institutioninfo}
\email{natali@math.tau.ac.il}
\end{authorinfo}
%
\shortauthors{Afek and Bremler}
%
\support{
We would like to thank Shlomi Dolev for several helpful discussions\@.
This work was supported by the Broadband Telecommunications
R\&D Consortium, administered by the chief scientist of the
Israeli Ministry of Industry and Trade\@.
}
%
\begin{editinfo}
\published{7}{12}{1998}
\end{editinfo}
%
\end{articleinfo}
%
\begin{articletext}
\begin{abstract}
%
Power supply, a surprisingly simple and new general paradigm for
the development of self-stabilizing algorithms in
different models, is introduced\@.
The paradigm is exemplified by developing
simple and efficient self-stabilizing algorithms for leader election
and either breadth-first search or depth-first search spanning-tree constructions, in
strongly connected unidirectional and bidirectional dynamic networks
(synchronous and asynchronous)\@.
The different algorithms stabilize in \(O(n)\) time in
both synchronous and asynchronous networks without assuming
any knowledge of the network topology or size, where \(n\) is
the total number of nodes\@. Following the leader election
algorithms, we present a generic self-stabilizing spanning tree
and/or leader election algorithm that produces a whole spectrum of
new and efficient algorithms for these problems\@.
Two variations that produce either a
rooted depth-first search tree or a rooted breadth-first search tree
are presented\@.
%
\end{abstract}
%
\asection{1}{Introduction}
%
\apar{1-1}
A distributed system is self-stabilizing if the system automatically
enters a global legal state in a bounded amount of time after the last fault or
corruption has occurred---regardless of the local
state of each of its processors, the level of RAM corruption in any processor,
or the placement of messages on its communication
channels\@.
Once in a legal and correct state, the system remains in a legal
state unless another fault or topological change has occurred\@.
The notion of self-stabilization was introduced by Dijkstra in
1974 \cite{cj98-03-16} and since then many algorithms for
different problems and configurations have been developed\@.
Self-stabilizing algorithms for message passing or
shared memory systems were
developed for either unidirectional or bidirectional rings
\cite{cj98-03-16,cj98-03-02,cj98-03-08,cj98-03-29,cj98-03-28,cj98-03-30,cj98-03-14,cj98-03-12,cj98-03-24,cj98-03-25,cj98-03-26,cj98-03-03,cj98-03-13}
and for bidirectional arbitrary topology networks
\cite{cj98-03-18,cj98-03-07,cj98-03-09,cj98-03-11,cj98-03-13,cj98-03-05,cj98-03-06}\@.
In this article, we develop simple and efficient self-stabilizing
algorithms for unidirectional, arbitrary, topology-dynamic networks\@.
The techniques developed here also produce new simple and efficient
algorithms for the bidirectional case\@.
In either case, our algorithms do not make any assumptions about the
network size or the messages and variables used in the
algorithms\@.
%
\apar{1-2}
The major obstacle in designing unidirectional self-stabilizing
algorithms is the lack of acknowledgments\@. Bidirectional
communication is heavily used by the nodes in the bidirectional
self-stabilizing system to compare the states of neighboring nodes
and to check their consistency, as, for example, in the local
checking algorithms \cite{cj98-03-07,cj98-03-09,cj98-03-10}\@.
%
\apar{1-3}
In this paper, we overcome the lack of bidirectional communication
with a new and surprisingly simple technique called \emph{power supply}\@.
Using this technique, we present leader-election algorithms for
synchronous (Section~3) and asynchronous (Section~4)
networks\@. Subsequently, we generalize
these algorithms (Section~5) with a new observation of
Collin and Dolev \cite{cj98-03-15} to a
family of algorithms either for electing a leader, or for constructing
a spanning tree\@. Two versions of the general algorithm produce
a breadth-first search (BFS) tree and a depth-first search (DFS) tree,
with or without a predistinguished
leader; other versions are possible\@.
Although there could be as much as \(O(E)\) corrupted messages in a global
state of the system, the time complexities (stabilization times) for our
algorithms are \(O(n)\) without making any assumption about the
size of the network\@.
The space complexity (overhead) of our algorithms is \(O(\log n)\) bits
per node\@.
%
\asubsection{1.1}{The Paper in a Nutshell, and Related Works}
%
\apar{1.1-1}
The design of self-stabilizing algorithms for unidirectional
networks has started to receive attention only in recent years
with the works of Mayer, Ostrovsky, and Yung \cite{cj98-03-29}
and with Afek and Lev \cite{cj98-03-08}\@. These works have designed algorithms
mostly for unidirectional rings, which leaves the arbitrary topology open\@.
Our work is motivated by these works and by the requirements
posed by SDH/SONET unidirectional networks \cite{cj98-03-08}\@.
%
\apar{1.1-2}
Only a few non-fault-tolerant distributed algorithms for
unidirectional networks have been developed in the past; see, e.g.,
\cite{cj98-03-21,cj98-03-04,cj98-03-23,cj98-03-22,cj98-03-27,cj98-03-20,cj98-03-32,cj98-03-31,cj98-03-19}\@.
%
\apar{1.1-3}
This paper proceeds from simple (Section~3) to more difficult
(Sections~4 and~5)\@. Let us enumerate the key ideas:
%
\begin{enumerate}
\item \emph{The basics.}
The basic algorithms developed are leader-election algorithms that elect
the smallest id as a leader\@. However, in self-stabilization, simply
choosing the smallest id is not safe, because a fake id that is
smaller than all the ids in the network may falsely be chosen by all
the nodes\@.
\item \emph{Addressing fake ids.}
A standard technique to overcome this problem is to
assign each node with its distance from the node whose identity it
has selected as a leader \cite{cj98-03-33,cj98-03-18}\@.
To ensure self-stabilization, every node
periodically checks that its distance is one more than its parent
distance (the parent is the neighbor through which the node has
discovered the leader with the distance parameter it believes in, which is
nil if the node under consideration is the root)\@. Still, this
principle by itself is not sufficient, because, for example, a false id
might circulate around a cycle increasing its distance parameter
without bound, and the problem could go undetected\@.
\item \emph{Resolving a fake id's effects.}
This problem has been overcome in several different ways: in
\cite{cj98-03-18} a predefined tree subnetwork was assumed; in
\cite{cj98-03-07} a special mechanism was developed to overcome the
problem; in \cite{cj98-03-09,cj98-03-11} a reset protocol was invoked
each time an inconsistent situation was detected; and in
\cite{cj98-03-05}, the knowledge of a bound \(b\) on the network diameter
was assumed\@. In this paper, a new technique is suggested, which
has the advantage over the above strategies in that it also works in
unidirectional networks without making any assumptions
(\cite{cj98-03-05} also works in unidirectional networks but
requires the knowledge of a bound on the network size)\@.
\item \emph{Power supply.}
``Power,'' the first basic idea in this paper, has two
parts. First, a legal leader becomes a source of
power which is disseminated, while fake identities may
not produce power (a legal leader is a node that is the
leader of itself)\@. Second, to be captured by a new leader,
a node consumes a fixed amount of that leader's power\@.
Hence, fake ids that have no source of power eventually
disappear\@.
\item \emph{The synchronous case.}
The implementation of the ``power'' idea in a synchronous network is
simple: to be captured by a new \(\mathrm{id}_{\mathrm{min}}\), a node has to receive
a message with \(\mathrm{id}_{\mathrm{min}}\) in two consecutive rounds from the same
neighbor and no smaller id from any other neighbor\@. However,
if after being captured by \(\mathrm{id}_x\) a node does not receive an \(\mathrm{id}_x\)
message in any one round, it immediately becomes the leader of
itself\@.
\item \emph{The asynchronous case.}
The implementation of the above idea in an asynchronous network
is problematic, because on the one hand, nodes in a self-stabilizing
asynchronous network have to periodically transmit messages; and
on the other hand, the transmission of such messages may
``give'' power to a fake id\@. This problem is solved here
by distinguishing between two kinds of messages,
\emph{weak} and \emph{strong}\@.
Weak messages have no power, and are sent periodically
between neighbors to ensure the consistency of the global state\@.
Any inconsistency that is detected causes the detecting node to become
the leader of itself\@. Strong messages, on the other hand, carry
power\@. Only leader nodes periodically produce strong messages\@.
Every other node relays a strong message to each of its neighbors
only when it receives a strong message from its parent\@.
To be captured by a new id, \(\mathrm{id}_{\mathrm{min}}\), a node has to receive two
strong messages with \(\mathrm{id}_{\mathrm{min}}\) from the same neighbor, and at the
same time, this id is smaller than any other id it receives\@.
\item \emph{A generic self-stabilizing algorithm.}
In this discussion we introduce another idea which is orthogonal to
the power-supply concept\@. We replace the minimum
distance parameter (point 2 above) by a general metric that may
accommodate different parameters and rules for their update,
e.g., the beautiful and simple parameter introduced by Collin
and Dolev [CD94]\@. In combination with any of our other techniques
(e.g., power supply), this new metric generates
a DFS tree (instead of a BFS tree with the distance parameter) rooted at
the elected leader\@. An example of a third metric is given in
Section~5\@.
\end{enumerate}
\asection{2}{The Model}
\label{sec:model}
%
\apar{2-1}
We consider a unidirectional strongly connected network with a set
\(V\) of \(n\) nodes and a set \(E\) of unidirectional links
\cite{cj98-03-04}\@.
A unidirectional
link is a point-to-point (node-to-node) communication line over
which information may flow in only one direction\@.
We make the standard and realistic assumption that each node \(v\) has
a unique identity called \(\mathrm{id}_v\)\@.
%
\apar{2-2}
An incoming link of a node is a link directed into the node, and
an outgoing link of a node is the link directed away from
that node\@. In the asynchronous network,
the number of messages that may be present on any link at the
same time is bounded by a constant \(B\) (independent of the
network size)\@. This assumption is not only realistic, but is also
necessary, as it is shown in \cite{cj98-03-17}
that almost any nontrivial task cannot be solved in a
self-stabilizing manner if link capacities are unbounded\@.
However, when bounded capacity links are used, a deadlock may
be formed unless messages are handled with care\@.
In this article, we maintain a buffer for each
outgoing link (incoming link) where the last two different messages
that could not have been sent (received) because the link is
too slow (too fast), are stored\@.
When the link (processor) becomes available again,
these messages are the first to be sent (processed)\@. However,
for the sake of clarity in describing the algorithms, we
disregard this mechanism; i.e., we assume bounded capacity links exist,
and that deadlocks are not formed\@.
It is easy to see that
the two models are equivalent (see the remark at the end of
Section~4 for more details)\@.
%
\apar{2-3}
Our algorithms also recover from corrupted messages and transmission
errors\@. During stabilization, after failures and topological changes
stop, each link is assumed to reliably transmit messages from the tail
node to the head node of the link\@.
Each message that arrives at a node is tagged by the port number
over which it arrives, and messages are processed in the order of
arrival\@.
Moreover, messages arrive at one end of a link in the order
that they have been sent from the other end (FIFO); otherwise,
bounded-time self-stabilization is prohibited\@.
%
\apar{2-4}
Another assumption that we make (and without which no
self-stabilizing message-passing algorithm may work in a
dynamic network) is that each node knows which of its incoming
links are up and operational and which are down. Otherwise, nodes
might be stuck in the asynchronous case, waiting for messages over
a link that is no longer operational \cite{cj98-03-01}\@.
%
\apar{2-5}
In Section~3, we describe our power-supply algorithm in a
synchronous network\@.
All the processors in a synchronous network receive, at the same
time, an infinite sequence of evenly spaced clock ticks\@.
In each clock tick (pulse), the
processor, based on its local state and on messages received from
its neighbors at the beginning of the pulse, makes a transition into a
new state and may send a message to any of its neighbors\@. Each
message sent immediately after a pulse is received by its
destination before the next pulse\@.
The time interval between two consecutive clock pulses is called a
\emph{round}\@.
%
\apar{2-6}
In an asynchronous network, the
processors operate at arbitrary rates which might vary over time, and the
messages incur unbounded and unpredictable, but finite, delays\@.
%
\apar{2-7}
The diameter of a network \(G\) whose set of nodes is \(V\) is defined
as follows:
diameter\((G)=\max_{u,v\in V}\mathrm{dist}(u,v)\), where \(\mathrm{dist}(u,v)\) is
the number
of edges in the shortest
directed path from \(u\) to \(v\)\@.
%
\asection{3}{The Synchronous Unidirectional Power-Supply Algorithm}
\label{sec:sync}
%
\apar{3-1}
Here we present a simple
algorithm for synchronous unidirectional
networks (see Figure 1)\@. It stabilizes in \(O(n)\) rounds, and does
not assume any bound on the diameter or on any other
parameter of the network\@.
(We remark that by a slight change in the
algorithm, its stabilizing time may be reduced to be
proportional to the length of the longest simple path in the network,
which is \(O(n)\) for general networks\@. However, this change leads
to much more complex proofs, so we do not present it here)\@.
%
\apar{3-2}
In this algorithm, again the smallest node identity is elected
as a leader\@. Fake ids are eliminated by using the distance
parameter and the following two rules:
%
\begin{enumerate}
\item
to remain under the leadership of a leader \(L\) at distance \(d\), \(d>0\), the
minimum leader message the node receives at each round should
be \(L\) with distance \(d-1\); and
\item
to be captured for the first time by a leader \(L\) at distance \(d\),
the minimum leader message the node receives in \emph{two}
rounds in a row should be \(L\), with distance \(d-1\)\@.
\end{enumerate}
%
The first rule ensures that nodes owned by a fake leader
and with the smallest distance parameter overall
(which is necessarily
larger than zero) at a round would abandon that leader in the
next round\@. This ensures that the minimum distance parameter
associated with a fake leader increases by one in each
round\@. The second rule stipulates that the maximum distance
parameter associated with a fake leader cannot grow by one in every
round; instead, it can grow by one only every two rounds. It thus consumes the
leader's power, because fake leaders do not have a
power supply (a source for leader messages)\@.
Therefore, if in the
initial faulty state the number of distinct distances
associated with a fake leader is denoted as \(\Delta d\), then
within at most \(2\Delta d\) rounds that fake leader id vanishes
(all of its power is consumed)\@.
%
\apar{3-3}
Once all fake ids have been eliminated, the smallest id in the
network captures all the nodes, each with the correct
shortest distance to the elected leader\@.
\begin{figure*}[htbp]
\begin{center}
\fbox{
\begin{minipage}{\textwidth}
\vspace*{1ex}
{\footnotesize
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXX\=XXX\kill
{\bfseries \mathversion{bold} Procedure for Node \(v\)}\\
{\bf Type}\\
\> \textsf{leader\_info} = record: [\textsf{id}, \textsf{dist}]\\
%
{\bf Var}\\
\>\(\mathrm{id}_v\)\`\{the unique id of node \(v\), fixed by the hardware\}\\
\>\textsf{leader, new, prev}: of type \textsf{leader\_info}\\
\>\textsf{m}: message of type \textsf{leader\_info}\\
\>\textsf{M}: set of messages of type \textsf{leader\_info} that have been received in the current round\\
\\
{\bf Each round do}\\
%
1 \>\textsf{M} := \textsf{M}\(\cup\)\{[\(\mathsf{id}_v\) , 0]\};\\
2 \>\textsf{new.id} := \(\min_{m \in M} \mathsf{m.id};\) \\
3 \>\textsf{new.dist} := \(\min_{m \in M} \{\mathsf{m.dist}+1|\mathsf{m.id} = \mathsf{new.id}\}\);\\
4 \>\textbf{If} \textsf{leader} \(\neq\) \textsf{new} \textbf{Then} \\
5 \>\> \textbf{If} \textsf{prev} = \textsf{new} \textbf{Then} \`\{second time the node receives the new information\}\\
6 \>\> \> \textsf{leader} :=\textsf{new};\\
7 \>\> \textbf{Else} \`\{first time the node receives the new information\}\\
8 \>\>\> \textsf{leader} :=[ \(\mathsf{id}_v\), 0 ]\`\ \{Node\(v\) becomes a self-leader\};\\
9 \> \textsf{prev} :=\textsf{new}\`\{saving the information from the last round\};\\
10 \>send(\textsf{leader} record) on all outgoing links\@.\\
\end{tabbing}
}
\end{minipage}
}
\afigcap{1}{The synchronous algorithm}
\label{fig:synch}
\end{center}
\vspace*{-.25in}
\end{figure*}
\asubsection{3.1}{The Correctness of the Algorithm}
%
\apar{3.1-1}
For the proof of correctness, we consider the execution of the
algorithm in the network following the last changes and
faults; that is, we assume that the execution starts in an
arbitrary state, and that no faults or topological changes occur
during the execution\@.
%
\apar{3.1-2}
Clearly, two rounds after the initial state, the variables
(\textsf{new}, \textsf{prev}, and \textsf{leader})
at all the nodes hold values that were actually sent by their
neighbors\@.
In the first theorem, we prove that in \(O(n)\) time after this
state, all fake ids disappear\@.
In the second theorem, we prove that \(O(D)\) is the
time after all the fake
ids have disappeared, where \(D\) is the diameter of the network\@.
The smallest id in the network is elected leader
by all of the nodes\@.
%
\apar{3.1-3}
In Theorem 1, we prove that fake leaders eventually disappear\@.
%
\begin{alabsubtext}{Theorem}{1}{} \label{the:0}
Eventually, all nodes in the variable \textsf{leader} have
\(id \in \mathrm{ID}\), where \(\mathrm{ID} =\{ id_v | v \in V \}\)\@.
\end{alabsubtext}
%
Let \(f\)id be a fake id in the network, i.e., \(f\mathrm{id} \notin V\)\@.
%
\begin{alabsubtext}{Definition}{1}{}
The \emph{heights group} of the fake id \(f\)id in a state of the
system is:
%
\[
\mathrm{heights}(f\mathrm{id}) =\{\mathsf{leader}_v.\mathrm{dist}|\exists v\in G,
\mathsf{leader}_v.\mathrm{id} =f\mathrm{id}\}
\]
\end{alabsubtext}
%
\apar{3.1-4}
We claim that for any fake id \(f\)id, the size of
\(\mathrm{heights} f\mathrm{id}\) is decreasing with time\@.
In Lemma 1, it is proved that the size of \(\mathrm{heights} f\mathrm{id}\)
may not increase, and in Lemma 2
it is proved that the size of \(\mathrm{heights} f\mathrm{id}\)
decreases every two rounds\@.
%
\apar{3.1-5}
Let \(\mathsf{X}^i_v\) denote variable \textsf{X} at node \(v\) at round
\(i\)\@.
%
\begin{alabsubtext}{Lemma}{1}{} \label{lem:1}
\(|\mathrm{heights}^{r-1}(f\mathrm{id})|\geq |\mathrm{heights}^r (f\mathrm{id})|\)
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{1}{}
\prooffontshape
The lemma follows from the code, since
for each \(d\in \mathrm{heights}^r (f\mathrm{id})\), \(d \geq 2\), there must have been a
\(d-1\in \mathrm{heights}^{r-1}(f\mathrm{id})\)\@. Otherwise, no node would have
distance \(d\) in the current round\@. Specifically, a node \(u\) whose
leader is \(f\mathrm{id}\) with distance \(d\) must have
received in the beginning of round \(r\)
the message: [\(f\mathrm{id}\), \(d-1\)] (by line 3)\@. Hence, there must
have been
an incoming neighbor of \(u\), \(v\), such that in round \(r-1\)
\(\mathsf{leader}_v\) :=[\(f\mathrm{id}, d-1]\)\@.
{\nopagebreakbeginpar\markendlst{Proof of Lemma 1}}
\end{alabsubtext}
%
\begin{alabsubtext}{Lemma}{2}{} \label{lem:2}
\(\|\mathrm{heights}^{r-2 }(f\mathrm{id})|>|\mathrm{heights}^r(f\mathrm{id})|\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{2}{}
\prooffontshape
\apar{Proof of Lemma 2-1}
By Lemma 1, for every
\(d\in \mathrm{heights}^r(f\mathrm{id})\), there is a \(d-2 \in \mathrm{heights}^{r-2
}(f\mathrm{id})\)\@. To prove the current lemma, we show that there is
at least one value \(dm\) in \(\mathrm{heights}^{r-2 }(f\mathrm{id})\) for which
there is no \(dm + 2\) in \(\mathrm{heights}^r(f\mathrm{id})\)\@.
Let \(dm = \max \{\mathrm{heights}^{r-2 }(f\mathrm{id})\}\)\@. Assume by
contradiction that \(dm + 2\in \mathrm{heights}^r(f\mathrm{id})\), and that \(v\) is a
node with \(\mathsf{leader}^r_v = [f\mathrm{id}, dm + 2]\)\@.
%
\apar{Proof of Lemma 2-2}
Clearly, in round \(r-2\), \(\mathsf{leader}_v \neq\)[\(f\mathrm{id}\),
\(dm + 2\)]\@.
%
\apar{Proof of Lemma 2-3}
Hence there are two possible cases:
either \(\mathsf{leader}_v\) = [\(f\mathrm{id}, dm + 2\)] also in rounds \(r\) and
\(r-1\), or, only at round \(r\)\@.
We show that in either case,
\(\mathsf{new}^{r-1}_v\) = [\(f\mathrm{id}, dm + 2\)],
hence node \(v\) must have received a message [\(f\mathrm{id}\),
\(dm+1\)] in round \(r-1\)\@. Thus there has been a \(u\), an
incoming neighbor of \(v\), such that
\(\mathsf{leader}_u\) = [\(f\mathrm{id}\), \(dm+1\)] in round \(r-2\), a
contradiction\@.
%
\apar{Proof of Lemma 2-4}
In the first case, since \(\mathsf{leader}^{r-1}_v\) = [\(f\mathrm{id}, dm + 2\)],
node \(v\) performs line 5, and
\(\mathsf{leader}_v^{r-1} = \mathsf{new}^{r-1} =\) [\(f\mathrm{id}, dm + 2\)]\@.
%
\apar{Proof of Lemma 2-5}
In the second case, since \(\mathsf{leader}^r_v =\) [\(f\mathrm{id}, dm + 2\)],
node \(v\) performs line 5, and
\(\mathsf{leader}_v^{r} = \mathsf{new}^{r} = \mathsf{prev}^{r} =\) [\(f\mathrm{id}\),
\(dm + 2\)]\@.
Since \(\mathsf{prev}^{r} = \mathsf{new}^{r-1}\) (by line 9),
\(\mathsf{new}^{r-1} =\)[\(f\mathrm{id}, dm + 2\)]\@.
%
{\nopagebreakbeginpar\markendlst{Proof of Lemma 2}}
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Theorem}{1}{}
\prooffontshape
From the two lemmas, it follows
that the size of \(\mathrm{heights}(f\mathrm{id})\) decreases by at least one
every two rounds\@. Hence, Theorem 1 holds\@.
{\nopagebreakbeginpar\markendlst{Proof of Theorem 1}}
\end{alabsubtext}
%
\begin{alabsubtext}{Corollary}{1}{}
Within \(O(n)\) rounds after the last fault or topological change, all
fake ids disappear\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Theorem}{2}{} \label{the:1}
At \(O(D)\) rounds after all fake ids have been eliminated, the
minimum id in the network is elected leader by all the nodes,
where \(D\) is the diameter
of the network\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Theorem}{2}{}
\prooffontshape
Let \(\textrm{ID}_v\) be the smallest id in the network\@.
The theorem follows by a simple induction
on the rounds, because of the elimination of all fake ids in round
\(r_0\)\@.
Clearly, \(\mathsf{leader}_v.id = \textrm{ID}_v\) in round \(r_0\)\@.
In round \(r_0 + 2\), every node \(u\) whose distance from \(v\) is one
has
\(v\) as its leader at distance one\@. In round \(r_0 +2D\), the
leader of all the nodes is \(\mathrm{ID}_v\)\@.
{\nopagebreakbeginpar\markendlst{Proof of Theorem 2}}
\end{alabsubtext}
%
\begin{alabsubtext}{Corollary}{2}{}
The time complexity of this part is \(O(D)\)\@.
\end{alabsubtext}
%
\apar{3.1-6}
Hence, the time complexity of the algorithm is \(O(n)\)\@.
Also, \(\Omega (n)\) is the lower bound on the time complexity of our
algorithm, as is shown in the Appendix\@.
\asection{4}{The Asynchronous Power-Supply Algorithm}
\label{sec:asyn}
%
\apar{4-1}
A fundamental characteristic of asynchronous self-stabilizing
algorithms is that nodes have to periodically exchange messages
with their neighbors (using time-outs)\@. Otherwise, the
system could be placed in a global state in which each node is
waiting for a message from another node\@. This fundamental
characteristic breaks our power-supply algorithm, because every node
in an asynchronous environment spontaneously generates an unbounded
number of messages, regardless of the number of messages it receives\@.
%
\apar{4-2}
Therefore, we introduce a new idea to implement the
power-supply principle in an asynchronous network\@. We distinguish
between two types of messages: \emph{weak} and \emph{strong}\@.
Weak messages are periodically sent by each
node to its neighbors, ensuring that neighboring nodes are in
a consistent state and no node is stuck waiting indefinitely for a
message from the other node\@. Strong messages, on the other
hand, play the role
of the power messages from the synchronous algorithm; that is,
only leader nodes generate strong messages spontaneously, and
each of the other nodes sends one strong message to each of its neighbors
for every correct and consistent strong message received over its
parent port-id (the port through which
a leader has captured a node, by two consecutive strong messages;
details below)\@.
%
\begin{figure*}[htbp]
\begin{center}
\fbox{
\begin{minipage}{\textwidth}
{\footnotesize
\begin{tabbing}
XX\=XX\=XX\=XX\=XX\=XX\=XX\=XX\=XX\=XX\kill
%
{\bf Procedure at Node \(\mathbf{v}\):}\\
%
{\bf Type}\\
\> \textsf{leader\_info} = record: [\textsf{id}, \textsf{dist}]\\
%
{\bf Var}\\
\>\(\textrm{id}_v\); \`\{the unique id of node \(v\), fixed by the hardware\}\\
\>\textsf{current\_leader},\textsf{prev},\(\mathsf{msg}\): of type \textsf{leader\_info}; \\
\>\textsf{parent}: port-id;\\
\> set \textsf{prev\_ports} of \{port-ids\}; \\
%
\\
{\bfseries \mathversion{bold} Upon receiving message (\(\mathsf{msg}, \mathsf{ mtype}\)) arriving at incoming port-id \(p\)} \\
%
1 \> \textbf{if} \textsf{parent} = nil \textbf{then} \textsf{current\_leader} := [\(\textrm{id}_v\), \(0\)]\`\{to be consistent\};\\
2 \> \textbf{if} [\(\textrm{id}_v\), \(0\)] \(\leq\) \(_{\textrm{lexic}}\) \textsf{current\_leader} \textbf{then} \textsf{current\_leader} := [\(\textrm{id}_v\), \(0\)]; parent := nil;\\
3 \> \textbf{if} (\(p\) = \textsf{parent}) \(\wedge\) (\(\mathsf{msg}\) = \textsf{current\_leader})\\
4 \>\> \textbf{then} \textbf{if} (\(\mathsf{mtype}\) = strong) \textbf{then} \textsf{send\_neighbors}(strong); \\
5 \> \textbf{if} (\(p\) = \textsf{parent}) \(\wedge\) (\textsf{current\_leader} \(\neq\) \(\mathsf{msg}\))\`\{inconsistent message from the parent\}\\
6 \>\> \textbf{then} \= \textsf{current} := [\(\textrm{id}_v, 0\)];\\
7 \>\>\> \textsf{parent} := nil;\\
8 \>\>\> send\_neigbors(strong);\\
9 \> \textbf{if} (\(\mathsf{msg}\) \(<_{\textrm{lexic}} \)\textsf{current\_leader}) \textbf{then} \\
10 \> \> \textbf{if} (\(\mathsf{mtype}\) = \textsf{strong}) \(\wedge\) (\textsf{prev} = \(\mathsf{msg}\)) \(\wedge\) (\(p \in \) \textsf{prev\_ports})\\ \`\{the second lexicographically smallest message\}\\
11 \>\>\> \textbf{then} \=\textsf{current\_leader} := \(\mathsf{msg}\);\`\{the node is captured\}\\
12 \>\>\>\> \textsf{parent} = \(p\); \\
13 \>\>\>\> send\_neigbors(strong);\\
14 \>\>\> \textbf{else}{} \= \textsf{current\_leader} := [\(\textrm{id}_v, 0\)]\`\{the first lexicographically smallest message\};\\
15 \>\>\>\> \textsf{parent} := nil;\\
16 \>\>\>\> send\_neigbors(strong);\\\\
17 \> \textbf{if} (\(\mathsf{msg}\) \(<_{\textrm{lexic}}\) \textsf{prev}) \= \textbf{then} \small\bf{case}(\(\mathsf{mtype}\))\`\{updating \textsf{prev} and \textsf{prev\_ports}\}\\
18 \>\> \textsf{strong}:\= \textsf{prev} = \(\mathsf{msg}\); \textsf{prev\_ports} := \{\(p\)\};\\
19 \>\> \textsf{weak}:\>\textsf{prev} = [\(\textrm{id}_v, 0\)];\textsf{prev\_ports} := \(\emptyset\);\\
20 \> \textbf{if} (\(\mathsf{msg}\) = \textsf{prev}) \(\wedge\) (\(\mathsf{mtype}\) = \textsf{strong}) \(\wedge\) (\(p\) \(\notin\) \textsf{prev\_ports}) \textbf{then} \textsf{prev\_ports} := \textsf{prev\_ports} \(\cup\) \{\(p\)\};\\
21 \>\= \textbf{if} (\(\mathsf{msg} >_{\textrm{lexic}}\) \textsf{prev}) \(\wedge\) (\(p \in\) \textsf{prev\_ports}) \textbf{then} \textsf{prev\_ports} := \textsf{prev\_ports} \(\setminus\) \{\(p\)\}; \\
\\
\=22 \>for every \(p\) \(\in\) \textsf{prev\_ports}\`\{to make the algorithm work in a dynamic network\} \\
23 \>\>\textbf{if} \(p\) is not alive \textbf{then} \textsf{prev\_ports} := \textsf{prev\_ports} \(\setminus\) \{\(p\)\};\\
24 \>\>\textbf{if} (\textsf{prev\_ports} \(=\) \(\emptyset\)) \textbf{then} \textsf{prev} := [\(\textrm{id}_v\), \(0\)]; \\
25 \>\>\textbf{if} (\textsf{parent} is not alive) \textbf{then} \textsf{current\_leader} := [\(\textrm{id}_v\), \(0\)]; \textsf{parent} := nil\\
\\
26 {\bfseries \mathversion{bold} Procedure \textsf{send\_neighbors}(\(\mathsf{mtype}\))}\\
27 \>\> send ( [\textsf{current\_leader.id}, \textsf{current\_leader.dist+1}], \(\mathsf{mtype}\)) to all neighbors;\\
\\
28 {\bfseries \mathversion{bold} Upon time-out() at node \(v\)} \\
29 \>\> \textbf{if} \textsf{parent} = nil \=\textbf{then} \= \textsf{send\_neighbors} (strong); \\
30 \>\>\> \textbf{else} \> \textsf{send\_neighbors} (weak);
\end{tabbing}
}
\end{minipage}
}
\afigcap{2}{The asynchronous power-supply algorithm}
\label{fig:Asynchronous Algorithm}
\end{center}
\end{figure*}
%
\apar{4-3}
Specifically (the code is given in Figure 2),
each node has a \textsf{current\_leader} record with
an id field and a distance field as in the synchronous
algorithm, plus a \textsf{parent} pointer, which is either nil if
the node is itself a leader or is pointing to one of its
ports\@. A node that is owned by another id becomes
a leader if its state is inconsistent with the neighbor's message, which
happens in either of the following two cases:
%
\begin{enumerate}
\item it receives a message (weak or
strong) through its \textsf{parent} port-id that is different from its
\textsf{current\_leader}; i.e., a message with an id
different from the node's \textsf{current\_leader.id} or with a
distance different from \textsf{leader}.dist, or
\item it receives a message (\textsf{msg}), weak or strong, through any
port-id that is lexicographically
smaller than \textsf{current\_leader}; i.e., either
\textsf{msg.id} is smaller than its \textsf{current\_leader.id}, or
\textsf{msg.id} equals the \textsf{current\_leader.id} and
msg.dist is smaller than \textsf{leader}.dist\@.
\end{enumerate}
%
%Insert Fig. 2 near here
%
\apar{4-4}
A node that has been captured by a certain leader will be captured by
a new leader only if either the new leader identity is smaller, or
the new leader identity is the same as the old one but the new leader comes
with a smaller distance parameter (that is, the new leader's
information is lexicographically smaller than the old leader's
information)\@.
%
\asubsection{4.1}{The Principle of Power Supply}
%
\apar{4.1-1}
To be captured, \emph{two} consecutive strong messages with the new
lexicographically smaller information must be received through the
same port-id (i.e., with only consistently weak messages received through the
port-id in between them), and at the same time no lexicographically
smaller message can arrive through any other port-id\@.
The first lexicographically smaller message to arrive
immediately changes the \textsf{current\_leader} of the node to
itself at distance zero, and only the second message changes the
\textsf{current\_leader} to the new information\@.
%
\apar{4.1-2}
This principle ensures that strong fake-id messages eventually disappear
from the network, since strong messages cannot flow in a cycle,
and the number of strong fake-id messages is reduced for each
node being captured by the fake id\@. On every path, the
number of strong messages cannot increase, because
a node sends a strong fake-id message only in response to receiving one\@.
An important point for the proof of correctness is
that whenever a node changes its \textsf{current\_leader}, the
node sends a strong message with its new \textsf{current\_leader}\@.
Thus all the neighbors of this node would notice that it
went through a state change\@.
In particular, whenever node \(v\) that is owned by \emph{old} is being
captured by a new leader, \emph{new}, it assigns \(\textrm{id}_v\) to its
\textsf{current\_leader} in between these changes and sends strong
messages containing \(\textrm{id}_v\) before sending the new strong messages\@.
%
\apar{4.1-3}
The implementation of the above in the code
(Figure 2) uses a \textsf{prev} variable to
store the smallest message body received in recent
message exchanges, and \textsf{prev\_ports}, which is the set of port-ids
through which this new information has arrived\@.
%
\apar{4.1-4}
For the algorithm to operate correctly and in a self-stabilizing
manner in a dynamic network, several local conditions have to be
repeatedly checked; if they are found inconsistent, they should be
corrected. These conditions are:
\begin{itemize}
\item
The link connected to the \textsf{parent} port-id should be up\@.
If the \textsf{parent} link is found to be down, then the node should
become a leader of itself (line 25)\@.
\item
If any port-id in \textsf{prev\_ports} is found to be a port to a link
that is down, it is removed
from the set\@. If the set \textsf{prev\_ports} becomes empty, then
\textsf{prev} is reset (lines 22--25)\@.
\item
If the \textsf{parent} of node \(v\) is nil, then \textsf{current\_leader}
has to be [id\(_v\), \(0\)] and vice versa (lines 1--2)\@.
\item
If \textsf{current\_leader.id} is larger than the node's id, then
again \textsf{current\_leader} is reset to [id\(_v\), \(0\)] (lines 1--2)\@.
\item
Each message must conform to the expected syntax, and
negative numbers are not allowed\@.
A node that receives an illegal message becomes a leader of itself\@.
\end{itemize}
%
\apar{4.1-5}
Since the asynchronous algorithm is an instance of the generic
algorithm, its time complexity is \(O(n)\), as we show for the
generic algorithm\@. Similarly, the correctness of the algorithm
follows from the proof of correctness for the generic algorithm
given in Section~6\@.
%
\asubsection{4.2}{A Remark about the Model}
%
\apar{4.2-1}
As stated in Section~2, the number of messages on a
link in a certain state is bounded by \(B\)\@.
Thus if either a tail node tries to
transmit faster than the rate of the link, or if a receiving head
node is too slow to receive the messages at the rate they arrive
over the link, messages might be lost\@. For our algorithms, this
does not pose a problem\@. We assume that at both end ports of a
link there is a process that works as follows: at each end port, the link
keeps a buffer with room for two messages\@. At the outgoing
end (tail), whenever the algorithm produces messages at a rate higher
than the link rate, the process keeps the last two different
messages that were not sent\@. These messages will be
sent out as if the two-message buffer were part of the link\@.
%
\apar{4.2-2}
Similarly, at the receiving end, the process maintains a two-message
buffer that contains only the last two different
messages that have arrived and have not been processed by the algorithm\@.
This ensures that if a node changes its state several times, the
last change will never be lost, and each of the node's neighbors
will notice that it went through a state change\@.
%
\asection{5}{A Generic Power-Supply Algorithm}
\label{sec:gen}
\apar{5-1}
The two self-stabilizing algorithms presented in
Sections~3 and~4, and most of the other
algorithms known \cite{cj98-03-18,cj98-03-07,cj98-03-09,cj98-03-05,cj98-03-06},
rely on the distance parameter,
i.e., on the fact that each node selects the node closest to the
leader and updates its distance to be one more\@. Yet, in \cite{cj98-03-15},
Collin and Dolev present a self-stabilizing algorithm that relies
on another metric, which in turn produces a DFS tree rather than a
BFS tree\@. These results suggest that perhaps there is a basic
principle unifying these metrics\@. In this section, we develop
a generic algorithm into which different metrics may be plugged,
e.g., one of the above two, or new ones\@. An example of such
a new metric is given below\@.
%
\apar{5-2}
The general algorithm produces a whole spectrum of
self-stabilizing algorithms for both unidirectional and
bidirectional networks, and is given in Figure 4\@.
The algorithm is a combination of the power-supply principle from
the previous sections, with a general scheme to produce spanning
trees\@. The BFS principle as in \cite{cj98-03-33} is one instance
of the general scheme to construct a BFS spanning tree, while the
Collin-Dolev principle given in \cite{cj98-03-15} is another instance
producing a DFS\@.
%
%Insert Fig. 4 near here
\apar{5-3}
From any initial state, the generalization guarantees to stabilize
in \(O(n)\) time units if the underlying principle that
ensures a tree structure does not send huge amounts of information
(i.e., as long as the message size is kept to \(O(\log n)\) bits, or in a
model that allows sending large messages in one time unit)\@.
If messages
are larger than the model can allow, then the time complexity
might be larger\@.
%
\begin{figure*}[bthp]
\begin{center}
\fbox{
\small
\begin{minipage}{\textwidth}
\vspace*{1ex}
\begin{tabbing}
%
XX\=XX\=XX\=XX\=XX\=XX\=XX\=XX\=XX\=XX\kill
%
{\bfseries\mathversion{bold} The Type Info}\\
\>\small\bf{case} ALGORITHM: \\
\>\>LE + BFS, LE + DFS, LE + FP, FP: \= {\bf Type} \textsf{info} = record: [\textsf{id},
\textsf{param}]; \\
\>\>BFS, DFS: \> {\bf Type} \textsf{info} = record: [\textsf{param}]; \\
\\
{\bfseries\mathversion{bold} The value \(zero\) type \textsf{info} at node \(v\):}\\
\>\small \bf{case} ALGORITHM: \\
\>\>LE + BFS: \= \(zero\) := [\(\textrm{id}_v\), \(0\) ]; \\
\>\>LE + DFS, LE + FP: \= \(zero\) := [\(\textrm{id}_v\), \(\bot\) ]; \\
\>\>BFS: \> \textbf{if} \(v\) is the root \= \textbf{then} \= \(zero\) := [\(0\)]; \\
\>\>\>\> \textbf{else} \> \(zero\) := [\(\infty\)];\\
\>\>DFS: \> \textbf{if} \(v\) is the root \> \textbf{then} \> \(zero\) := [\(\bot\)]; \\
\>\>\>\> \textbf{else} \> \(zero\) := [\(\infty\)];\\
\>\>FP: \> \textbf{if} \(v\) is the root \> \textbf{then} \> \(zero\) := [0,\(\bot\)]; \\
\>\>\>\> \textbf{else} \> \(zero\) := [\(\infty, \bot\)];\\
\\
{\bfseries\mathversion{bold} If \(v\) is a root then \textsf{parent} := nil;}\\
\\
{\bfseries\mathversion{bold} Function \textsf{next}(\textsf{selected} of type \textsf{info}, \(p\) of type
port-id): \textsf{info}} \\
\>\small\bf{case} ALGORITHM: \\
\>\> FP, LE + FP, LE + DFS:\= return [\textsf{selected.id}, \textsf{selected.param} \(\circ\) \(p\) ]; \\
\>\>LE + BFS:\> return [\textsf{selected.id}, \textsf{selected.param} + 1]; \\
\>\>BFS:\> return [\textsf{selected.param}+1];\\
\>\>DFS:\> return [\textsf{selected.param} \(\circ\) \(p\)]; \\
\\
{\bfseries\mathversion{bold} Function select(\textsf{selected} of type \textsf{info}, \textsf{msg} of
type \textsf{info}): \textsf{info}}\\
\>\small\bf{case} ALGORITHM: \\
\>\> BFS + LE, DFS + LE, BFS, DFS:\= \textbf{if} \textsf{msg} \(<_{\mathrm{lexic}} \textsf{selected}\) \\
\>\>\> \textbf{then} \= return \textsf{msg}; \\
\>\>\> \textbf{else} \> return \textsf{selected};\\
\>\> FP, LE + FP: \= \textbf{if} (\(\mathrm{id}_v \notin \mathsf{msg.param}\)) \(\wedge\) \\
\>\>\> ( (\(\mathrm{id}_v \in\) \textsf{selected.param}) \(\vee\) (\textsf{msg.id} \(<\) \textsf{selected.id})) \\
\>\>\> \textbf{then} \= return \textsf{msg}; \\
\>\>\> \textbf{else} \> return \textsf{selected};\\
\end{tabbing}
\end{minipage}
}
\afigcap{3}{The generic framework}
\label{fig:Gsetting}
\end{center}
\vspace*{-.25in}
\end{figure*}
%
\apar{5-4}
Let us first describe the underlying principles and properties of
the family of tree-producing schemes that fit our general
algorithm\@.
All of these schemes work according to the following general
mechanism: each node that is a candidate for leadership has a
unique value called the \emph{zero} of that node\@.
In the algorithms
for constructing a tree rooted at a predistinguished node, only that
predistinguished node is a candidate\@.
%
\apar{5-5}
The \emph{zero} value of each candidate is fixed in hardware (i.e.,
in stable and reliable memory), and it is usually based
on the node's unique identity\@. In the algorithm, each candidate
tries to ``convince'' all other nodes to choose its \emph{zero} value as
their selected values, and thus to capture them\@.
To do so, every candidate suggests that each
of its neighbors should be its selected parent, by sending each neighbor
a special value computed by applying a function called
\emph{next} on the \emph{zero} value\@. Each node \(v\) selects (according
to a particular selection rule) one of the suggestions it receives,
assigns it to its selected variable, and selects the link over
which it arrives as its parent\@.
Node \(v\) transitively suggests its neighbors should join the same
selected candidate by sending them a special message
computed by again applying the function \emph{next} on \(v\)'s
selected value\@. This process continues transitively until one
candidate captures the entire network\@.
The process thus described constructs a tree structure that traces the
paths along which the \emph{zero} value of the tree root has
disseminated\@.
%
\apar{5-6}
For such a scheme to generate a self-stabilizing algorithm when
combined with the power-supply technique, it
has to satisfy particular characteristics\@.
Each such scheme has three components: (1) the \emph{next} function, used to
compute the suggestions; (2) the selection rule, which
each node applies to choose its selected variable
from the suggestions it receives; and (3) a set of \emph{zero} values,
which are all the \emph{zero} values of nodes in the network\@.
This set of \emph{zero} values has to satisfy the following three properties:
\begin{enumerate}
\item
No legal sequence of selected values along a path may cycle;
that is, in any cycle of parent links and selected values, at
least one node locally detects (by observing its predecessor
selection and its own selection) that its selected value is
wrong\@.
\item
If there are no faults or erroneous values, then exactly one
candidate node captures the whole network\@. This node does not
select a parent link (its parent is nil)\@.
\item
If there are no faults or erroneous values, then the process
reaches a fixed point: the network reaches a state after
which no node changes its selection\@.
\end{enumerate}
%
\apar{5-7}
Any scheme that satisfies these properties reaches a stable state
in which the parent links induce a rooted tree spanning the network\@.
Different schemes' \emph{next} functions, selection rules, and sets of
\emph{zero} values produce different trees\@.
In this paper, three basic schemes are used that produce a
BFS tree, a DFS tree, or an arbitrary tree\@.
%
\apar{5-8}
A scheme that satisfies the above guidelines to construct a DFS
tree was given by Collin and Dolev \cite{cj98-03-15}\@.
The \emph{zero} of a root node in that variation is the symbol \(\bot\),
and the selected value of each node is a string of output port-ids
along a simple path from the root (candidate for leadership) to
that node\@. The selection rule selects the neighbor such that
its \emph{next selected} value (or sequence of link ports) is
lexicographically smallest\@. Note that in this case the \emph{next}
function also takes the port-id leading to each neighbor as a
parameter\@.
%
\apar{5-9}
In another example of the generic algorithm, each node maintains the
sequence of nodes on a path from the root to itself\@. In the generic
implementation, each node \(v\) selects and extends the list of
a neighbor whose list does not include \(v\)\@.
%
\apar{5-10}
The different variations of the scheme are specified in Figure 3,
for inclusion with the power-supply code
in Figure 4\@.
We present the parameterization of the \emph{zero} values, the \emph{next}
function, and the selection rules to produce the following variations:
%
\begin{enumerate}
\item
a leader-election algorithm that also produces a rooted breadth-first
search tree (as denoted in the previous section
as LE + BFS);
\item
a leader-election algorithm that also produces a rooted \emph{depth}-first search
tree (denoted as LE + DFS);
\item
an algorithm that produces a BFS tree, given a distinguished
root (denoted as BFS);
\item
an algorithm that produces a DFS tree, given a distinguished
root (denoted as DFS);
\item
a leader-election algorithm that produces an arbitrary rooted
tree (denoted as LE + FP); and
\item
an algorithm that produces an arbitrary tree, given a distinguished
root (denoted as FP)\@.
\end{enumerate}
%
%Insert Fig. 3 near here
%
\apar{5-11}
The various schemes satisfy each property in different ways\@.
In the BFS and DFS schemes, the no-cycle property is
satisfied, because the set of all possible suggestions
and \emph{zero} values is a total
ordered set; and, for any value \(x\), \emph{next}\((x) > x\)\@.
%
\apar{5-12}
In the third scheme, FP, the no-cycle property is trivially satisfied
since each suggestion is a string of ids, and the function \emph{next}
at node \(v\) simply appends id\(_v\) to \(v\)'s selected string\@.
A node does not select a suggestion that contains its own id\@.
%
\apar{5-13}
The no-cycle property together with the power-supply technique
ensures that any phony suggested value eventually disappears\@.
%
\apar{5-14}
The formal proof of the algorithm's properties is given in Section~6\@.
%
\apar{5-15}
Note that in the cases involving a predistinguished leader (BFS or DFS),
it is unnecessary for each node in the system to have a unique id\@.
The time complexity of the general algorithm
is \(O(n)\) (proof in Section~6)\@.
In the case of a BFS with a predistinguished leader,
the time complexity is lower,
\(O(D)\), which is also the optimal time complexity for this problem\@.
%
\begin{figure*}[bthp]
\begin{center}
\fbox{
\begin{minipage}{\textwidth}
\vspace*{1ex}
{\footnotesize
\begin{tabbing}
%
XX\=XX\=XX\=XX\=XX\=XX\=XX\=XX\=XX\=XX\kill
%
{\bfseries\mathversion{bold}Procedure at Node \(v\)}\\
%
{\bf Type}\\
\> \textsf{info} = record: [\textsf{id}, \textsf{param}] \\
%
{\bf Var}\\
\>\textsf{selected},\textsf{prev},\textsf{msg}: of type \textsf{info}; \\
\>\textsf{parent}: port-id;\\
\> set \textsf{prev\_ports} of \{port-ids\}; \\
%
\\
%
{\bfseries \mathversion{bold} Upon receiving message (\textsf{msg, mtype}) arriving at incoming port-id \(p\)}\\
%
1 \> \textbf{if} \textsf{parent} = nil \textbf{then} \textsf{selected} := \emph{zero}\`\{to be consistent\};\\
2 \> \textbf{if} (select(\textsf{selected}, zero) = \emph{zero}) then \textsf{selected} := \emph{zero}; parent := nil\\
3 \> \textbf{if} (\(p\) = \textsf{parent}) \(\wedge\) (\textsf{msg} = \textsf{selected}) \`\{send a message\}\\
4 \>\> \textbf{then} \textbf{if} (\textsf{mtype} = strong) \textbf{then} \textsf{send\_neighbors}(strong); \\
%
5 \> \textbf{if} ((\(p\) = \textsf{parent}) \(\wedge\) (\textsf{selected} \(\neq\) \textsf{msg}))\`\{inconsistent message from the parent\}\\
6 \>\> \textbf{then} \= \textsf{selected} := \emph{zero};\\
7 \>\>\> \textsf{parent} := nil;\\
8 \>\>\> \textsf{send\_neighbors}(strong);\\
9 \> \textbf{if} (select(\textsf{selected}, \textsf{msg}) = \textsf{msg}) \textbf{then} \\
10 \> \> \textbf{if} (\textsf{mtype} = \textsf{strong}) \(\wedge\) (\textsf{prev} = \textsf{msg}) \(\wedge\) (\(p \in \) \textsf{prev\_ports})\`\{the second selected message\}\\
11 \>\>\> \textbf{then} \=\textsf{selected} := \textsf{msg};\`\{the node is captured\} \\
12 \>\>\>\> \textsf{parent} = \(p\); \\
13 \>\>\>\> \textsf{send\_neighbors}(strong);\\
14 \>\>\> else{} \= \textsf{selected} := \emph{zero};\`\{the first selected message\} \\
15 \>\>\>\> \textsf{parent} := nil;\\
16 \>\>\>\> \textsf{send\_neighbors}(strong);\\
\\
17 \> \textbf{if} (select(\textsf{prev}, \textsf{msg}) = \textsf{msg}) \= \textbf{then} \small\bf{case}(\textsf{mtype}) \`\{updating \textsf{prev} and \textsf{prev\_ports} \}\\
18 \>\> \textsf{strong}:\= \textsf{prev} = \textsf{msg}; \textsf{prev\_ports} := \{\(p\)\};\\
19 \>\> \textsf{weak}:\>\textsf{prev} = \emph{zero};\textsf{prev\_ports} := \(\emptyset\);\\
20 \> \textbf{if} (\textsf{msg} = \textsf{prev}) \(\wedge\) (\textsf{mtype} = \textsf{strong}) \(\wedge\) (\(p\) \( \notin\) \textsf{prev\_ports}) \textbf{then} \textsf{prev\_ports} := \textsf{prev\_ports} \(\cup\) \{\(p\)\};\\
21 \>\= \textbf{if} (select(\textsf{prev}, \textsf{msg}) \(\neq\) \textsf{msg}) \(\wedge\) (\(p \in\) \textsf{prev\_ports}) \textbf{then} \textsf{prev\_ports} := \textsf{prev\_ports} \(\setminus\) \{\(p\)\}; \\
\ \ \ \\\=
22 \> for every \(p\) \(\in\) \textsf{prev\_ports} \`\{to make the algorithm work in a dynamic network\} \\
23 \>\> \textbf{if} \(p\) is not alive \textbf{then} \textsf{prev\_ports} := \textsf{prev\_ports} \(\setminus\) \{\(p\)\};\\
%
24 \>\> \textbf{if} \textsf{prev\_ports} \(=\) \(\emptyset\) \textbf{then} \textsf{prev} := \emph{zero}; \\
25 \>\> \textbf{if} (\textsf{parent} is not alive) \textbf{then} \textsf{selected} := \emph{zero};\textsf{parent} := nil; \\
\\\=
26 {\bf procedure \textsf{send\_neighbors}(\textsf{mtype}) }\\
27 \>\> for every \(p\) \(\in\) \textsf{prev\_ports}\\
28 \>\>\> send (\textsf{next}(\textsf{selected}, \(p\)), \textsf{mtype}) to neighbor \(p\);\\
\\
%
29 {\bfseries \mathversion{bold} upon time-out() at node \(v\)} \\
30 \>\> \textbf{if} \textsf{parent} = nil \=\textbf{then} \= \textsf{send\_neighbors} (strong); \\
31 \>\> \textbf{else} \> \textsf{send\_neighbors} (weak); \\
%
\end{tabbing}
}
\end{minipage}
}
\afigcap{4}{The generic power-supply algorithm}\label{fig:GAlg}
\end{center}
\vspace*{-.25in}
\end{figure*}
\asection{6}{Correctness of the Generic Asynchronous Algorithm}
\label{sec:proof_asyn}
\asubsection{6.1}{The Central Theorem}
%
\apar{6.1-1}
In this section we prove the main theorem\@.
% \begin{theorem}
\begin{alabsubtext}{Theorem}{3}{}
Within \(O(nB)\) units of time after the last topological change
or erroneous state change, a stable tree spans the network\@.
% \end{theorem}
\end{alabsubtext}
%
\apar{6.1-2}
There are three major steps in the proof:
\begin{itemize}
\item
First, we show that in linear time after the last change
or error in the network, all erroneous and illegal strong messages
disappear (Lemma 4), and are never generated again\@.
\item
Second, we show that in \(O(n)\) time after the first step, erroneous or
illegal weak messages do not exist, and are never generated again
(Lemma 6)\@.
\item
Third, we show that in \(O(n)\) time after the second step, a stable rooted tree
spans the network (Lemma~8)\@.
\end{itemize}
%
\apar{6.1-3}
Let us start with some definitions:
%
\begin{alabsubtext}{Definition}{2}{}
Two functions are associated with each message \(m\):
\(\mathsf{mtype}(m)\), the type of the message (strong or weak), and \(\mathsf{msg}(m)\), the
body of the message, which is of type \textsf{info} (see the code)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Definition}{3}{}
A message sequence, denoted by
\(\vec{m} = \{m_1 m_2,\dots, m_k\}\),
is a contiguous sequence of messages
(strong and weak) on a link such that they all have the same
\(\mathsf{msg}\) value\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Remark}{1}{}
A message sequence can be empty\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Definition}{4}{}
We denote by \(\mathsf{in\_port}_{v}(w)\) the port id
through which the \((wv)\) link enters \(v\)\@.
We denote by \(\mathsf{out\_port}_{v}(w)\) the port id
through which the \((vw)\) link leaves \(v\)\@.
\end{alabsubtext}
%
\apar{6.1-4}
If we observe the edges that are covered by the union
of message sequences that appear to have been
originated from the same candidate,
then this structure may look like a forest\@.
However, in the proof, it is easier and much simpler
to argue about the union of such sequences along a path, rather
than along the edges of a tree\@. Below we formally define such
sequences as \emph{blocks}\@. Clearly, if we prove statements like
``there are no more blocks with property \(p\) in the network,''
then it is true that the same holds for the corresponding
trees with the same property\@. Therefore, it is enough to consider
blocks, as defined below, rather then the more complicated trees\@.
%
\begin{alabsubtext}{Definition}{5}{}
\label{block}
A block---denoted by \(\mathrm{bl} = \{\vec{m}_0 v_0 \vec{m}_1 v_1
\dots \vec{m}_l v_l
\vec{m}_{l+1}\}\) \(l\geq 0\)---is a sequence of messages
interleaved with zero or more nodes in one state of the system,
such that the following hold (see Figure 5):
%
\begin{enumerate}
\item
\(\{v_0\), \(v_1, \dots v_l\}\) is a directed path\@.
\item
For \(i = 0, \dots , l+1\), \(\vec{m}_i = \{ m_{i,1} m_{i,2},
\dots , m_{i,k_0}\) \} is a
message sequence on the link from \(v_i\) to \(v_{i+1}\)\@.
Except for \(\vec{m}_{l+1}\), each
\(\vec{m}_{i}\) contains all the messages on the corresponding
link\@.
If \(\vec{m}_0\) is not
empty, then \(m_{0,k_0}\) is
the first message on the link entering \(v_0\), and
we denote by \(\mathsf{begin\_port}\) the port-id at node \(v_0\) through
which message \(m_{0,k_0}\) arrives\@. If \(\vec{m}_0\) is empty,
then \(\mathsf{begin\_port}\) is a
port-id of some incoming neighbor of \(v_0\)\@.
If \(\vec{m}_{l+1}\) is not empty, then \(m_{l+1,0}\) is the
last message sent by \(v_l\) on the corresponding outgoing link and
we denote by \(\mathsf{end\_port}\) the port-id at node \(v_l\) through which
message \(m_{l+1,0}\) was sent\@.
\item
For \(i = 0, \dots ,l, \textit{ for all m} \in \vec{m}_i\), \(
\mathsf{msg}(m) = \mathsf{selected}_{v_i}\)\@.\\
For \(i = l+1, \textit{ for all m} \in \vec{m}_{l+1}\), \(
\mathsf{msg}(m) = \textsf{next}(\mathsf{selected}_{v_l},\mathsf{end\_port})\)\@.
%
\item
For \(i = 0, \dots ,l-1\), \(
next(\mathsf{selected}_{v_i},\mathsf{out\_port}_{v_i}(v_{i+1})) = \mathsf{selected}_{v_{i+1}}\)\@.
%
\item
For \(i = 1, \dots , l\), \( \mathsf{parent}_{v_i} = \mathsf{in\_port}_{v_i}(v_{i-1})\)\@. \\
For \(i = 0, \mathsf{parent}_{v_0} = \mathsf{begin\_port}\)\@.
%
\item
There is no \(v\) in \(G\) such
that \(\ \{ v \vec{m}_0 v_0 \vec{m}_1 v_1 \dots \vec{m}_l
v_l \vec{m}_{l+1}\}\) \(l\geq 0\)
satisfies conditions 1--5, and there is no message \(m\) such that \\
\(\ \{\{m\} \cup \vec{m}_0 v_0 \vec{m}_1 v_1 \dots
\vec{m}_l v_l \vec{m}_{l+1}\}\) \(l\geq 0\) satisfies conditions 1--5\@.
\end{enumerate}
\end{alabsubtext}
%
\begin{alabsubtext}{Observation}{1}{}
\label{obs:n}
The maximum number of nodes in a block is \(n\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Observation}{2}{}
\label{obs:no-cycle}
Every block induces a simple directed path\@.
\end{alabsubtext}
%
\apar{6.1-5}
Observation 2 follows from point 4 of Definition 5
and from the particular properties of the spanning-tree construction
scheme\@. The no-cycle property
has to be proved separately for each spanning-tree scheme that is used\@.
It is easy to verify the property for the three major schemes we use: the BFS,
DFS, and FP (see the discussion in the previous section)\@.
%
\begin{alabsubtext}{Definition}{6}{}
\label{potential}
The potential(bl) of a block bl
is the total number of strong messages in the block
(see Figure 5)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Corollary}{3}{}
\label{cor:pon}
The potential of a block is at most \(nB\)\@.
\end{alabsubtext}
%
\apar{6.1-6}
Were we proving the leader-election algorithm of
Section~4, we would argue that blocks with fake ids
eventually
disappear\@. However, in the generic algorithm we have generalized
the notion of id, and thus we define the notion of a \emph{phony}
block as follows.
%
\begin{alabsubtext}{Definition}{7}{}
\label{phony}
A block \(\{\vec{m}_0 v_0 \vec{m}_1 v_1 \dots \vec{m}_l v_l
\vec{m}_{l+1}\}\) \(l\geq 0\) is a phony block, if this block
is a result of a ``maliciously'' erroneous initial state; that is,
a block that was created after state \(s_0\) and was truncated may not
be considered to be a phony block\@. Formally, a block
\(\{\vec{m}_0 v_0 \vec{m}_1 v_1 \dots \vec{m}_l v_l
\vec{m}_{l+1}\}\) \(l\geq 0\) is a phony block, if
there is no way to assign values to \textsf{selected} fields of
nodes \(v_{-h}, v_{-(h-1)}, \dots , v_{-1}\) such that
\(\{v_{-h}, v_{-(h-1)}, \dots , v_{-1} \vec{m}_0 v_0
\vec{m}_1 v_1 \dots \vec{m}_l v_l \vec{m}_{l+1}\}\) is a legal block and
\textsf{selected}\(_{v_{-h}}\) equals zero\(_{v_{-h}}\) (see Figure
5)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Definition}{8}{}
\label{tail}
Let \(\{\vec{m}_0 v_0 \vec{m}_1 v_1 \dots \vec{m}_l v_l
\vec{m}_{l+1}\}\) \(l\geq 0\) be a block\@.
Then \(m_{0,0}\) is the tail
of the block, or if \(\vec{m}_0\) is empty, then
\(v_0\) is the tail of the block\@. Similarly, \(m_{l+1,k_{l+1}}\)
is
the head of the block, or if \(\vec{m}_{l+1}\) is empty,
then \(v_l\) is the head of the block (see Figure
5)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Definition}{9}{}
\label{subblock}
A subblock is a subsegment of a block that satisfies
all the conditions of Definition 5, except condition 6
(see Figure 5)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Observation}{3}{}
\label{obs:subB}
Every block is also a subblock\@.
\end{alabsubtext}
%
\begin{figure*}[htbp]
\begin{center}
\fbox{
\psfig{file=cj9803f5.eps}
}
\afigcap{5}{
An example of a block, including the
head and tail of a block, the potential, a phony block, and the subblock\@.
The example is given in the framework of LE + BFS\@.
Each node has an id. Under the node we see the
node record [leader, distance], and similarly, the record of the messages on the
links\@.
We symbolize the type of message by \emph{s} for strong
and \emph{w} for weak\@. The block in the figure is
\protect\(
\{
m_{0,1} = [s,[5,1]],m_{0,2} = [w,[5,1]], v_1 = \{\mathrm{id}_v = 30, [5,1]\},
m_{1,1} = [s,[5,2]],m_{1,2} = [w,[5,2]], v_2 = \{\mathrm{id}_v = 50, [5,2]\},
m_{2,1} = [5,3]
\}
\protect\)\@.
The potential of the block is 4, which is the number of strong messages
in the block\@. The message \protect\(m_{0,1} = [s,[5,1]]\protect\)
is the head of the block,
and the message \protect\(m_{2,1} = [5,3]\protect\) is its tail\@.
\par
The sequence
\protect\(
\{
m_{0,1} = [w,[5,1]], v_1 = \{\mathrm{id}_v = 30, [5,1]\}, m_{1,1} = [s,[5,2]],
m_{1,2} = [w,[5,2]], v_2 = \{\mathrm{id}_v = 50, [5,2]\}, m_{2,1} = [5,3]
\}
\protect\)
is an example of a subblock, in the same way as any other suffix of
the block\@.
}
\end{center}
\end{figure*}
%
\begin{alabsubtext}{Proof of Theorem}{3}{The Formal Proof}
\prooffontshape
\apar{Preoof of Theorem 3-1}
The proof argues about runs of the system that start in an
arbitrary state \(s_0\) and in which there are no failures
or topological changes\@. Starting in state \(s_0\), the
system behavior is modeled by a run, which is an infinite sequence
\(q_0 \pi_0 q_1 \pi_1\dots \)\ of alternating states and atomic
operations, such that \(q_0 = s_0\)\@.
Each atomic operation \(\pi _i\) is either receiving and processing
a message, and sending any resulting message, or a time-out event
that results in sending messages\@.
Each state includes a complete description of all the variables and
messages in all the processors of the system\@.
State \(q_{i+1}\) is the state of the system after applying
operation \(\pi_i\) to state \(q_i\)\@.
%
\apar{Preoof of Theorem 3-2}
For the purpose of time-complexity analysis, we assume that each
message is delivered in at most one unit of time, i.e., one unit of
time is the time it takes the slowest message to reach its
destination\@.
%
\apar{Preoof of Theorem 3-3}
We proceed by proving that following global state \(s_0\), the system
must progress through a sequence of global states that contains
subsequence \(s_0\), \(s_1\), \(s_2\), \(s_3\), and \(s_4\), such that in
each of these
states an additional global and \emph{stable} property holds until in state
\(s_4\) the desired spanning-tree property stably holds\@.
The sequence of stable properties that hold in the run
suffixes starting at states \(s_0\), \(s_1\),
\(s_2\), \(s_3\), \(s_4\) are correspondingly as follows:
%
\begin{enumerate}
\item
Starting with global state \(s_0\), there are no failures
or topological changes by assumption\@.
\item
Starting with global state \(s_1\), all messages and all state
variables (\textsf{parent, selected, prev,prev\_ports}) hold
values that result from reception of messages sent after \(s_0\)\@.
It is easy to see that state \(s_1\)
is at most two time units after state \(s_0\)\@.
\item
Starting from global state \(s_2\),
there are no erroneous and illegal strong messages in the network\@.
\item
Starting from global state \(s_3\),
there are no erroneous or illegal weak
messages in the network\@.
\item
Starting from global
state \(s_4\), a stable rooted tree spans the network\@.
\end{enumerate}
{\nopagebreakbeginpar\markendlst{Proof of Theorem 3}}
\end{alabsubtext}
\asubsection{6.2}{Proof Intuition}
\apar{6.2-1}
In the first (and major) step of the proof we show that phony blocks
eventually disappear, by arguing that the lifetime of a phony block
is bounded by the potential of the block (i.e., the potential of
a phony block monotonically decreases)\@.
The potential of a phony block (by Definition 6)
equals the maximum number of new nodes that the phony block
may capture before disappearing (because the potential is the
total number of strong messages, and the capture of a new node
consumes at least one strong message)\@.
Once all the phony blocks disappear, the system
reaches a stable legal state in \(O(n)\) time\@.
%
\apar{6.2-2}
Intuitively, the proof that phony blocks disappear after \(O(nB)\) time
is based on the following three points:
%
\begin{itemize}
\item{P1:} By Observation 2, a block cannot cycle\@.
\item{P2:} A new node can be added to a block only if it is captured by two
strong messages sent from the block (the power-supply principle)\@.
Therefore, in capturing a node, the phony block potential decreases by one\@.
\item{P3:} The potential of a phony block cannot increase\@. It can only
increase if one of the following conditions exists:
\begin{enumerate}
\item it has the power supply to generate new strong messages
(this is obviously not true in a phony block); or
\item two or more phony blocks are united, thus creating a larger
potential\@. But blocks cannot unite,
because whenever a node changes its state, it first sends a message
with its \emph{zero} state to each of its neighbors\@. Upon
receiving this message, each of the neighbors that is at the
same block as the node also goes through a change\@. Thus,
an element (message or node state) separating blocks never
disappears (until the blocks it separates disappear)\@.
\end{enumerate}
\end{itemize}
%
\apar{6.2-3}
Based on points P1 and P2, in \(O(nB)\) time after the initial state,
the potential of a phony block
reduces to zero\@. To observe this, let us track any
strong message \emph{m} on a phony block until it disappears\@.
In each time-unit message, \emph{m} propagates at least one more
node along the phony block\@. The length of the phony block
thus traversed is at most \(n + nB + 1\), with \(n\) nodes in the original
block, and \(nB + 1\) that may be captured until its potential
reaches zero\@.
Therefore, after \(O(nB)\) units of time, there is no strong message
in any phony block, and the block potential is zero\@.
Based on point P1, a phony block disappears in \(O(n)\) time after
its potential is equal to zero\@.
%
\apar{6.2-4}
In Lemma 3, we prove that the potential of a phony block
does not increase after state \(s_1\) (point P3); i.e., distinct
blocks cannot join together into a
larger block\@.
More formally, if in state \(q_{i + 1}\) there is a block
with \(m\) nodes, then in state \(q_i\) there is a corresponding block
with at least \(m-1\) nodes and with at least as many strong messages\@.
In the lemma we address all possible events and show that the potential does not
increase in any of them\@.
%
\apar{6.2-5}
Let \textsf{X}\(^i_v\) denote variable \textsf{X} at node \(v\) in state
\(q_i\)\@.
%
\begin{alabsubtext}{Lemma}{3}{}
\label{lem:3}
Let \(q_{i+1}\) be a state, after state \(s_1\)\@.
If in state \(q_{i+1}\) there exists a phony block
\(\mathit{bl}^{i+1}\) = \(\ \{\vec{m}_0 v_0 \vec{m}_1 v_1 \dots \vec{m}_l v_l
\vec{m}_{l+1}\}\) \(l\geq 0\),
then in state \(q_i\) there is a subphony block \(\mathit{sbl}^i\),
and exactly one of the following holds:
%
\begin{enumerate}
\item
Node \(v_j\) receives a weak message:
\(\mathit{sbl}^i = \ \{\vec{m'}_0 v_0 \vec{m'}_1 v_1 \dots \vec{m'}_{l-1} v_{l-1}
\vec{m'}_{l} v_l \vec{m'}_{l+1}\}.\)
Only one message sequence, \(\vec{m'}_j\), \( 0\leq j\leq l+1\)
in \(\mathit{sbl}^{i}\), is not the same as in \(\mathit{bl}^{i+1}\)\@.
Let \(\vec{m'}_{j} = \{m_{j,1} \dots m_{j,k_j-1} m_{j,k_j}\}\)
in state \(q_i\). Then \(\vec{m}_j = \{m_{j,1} \dots m_{j,k_j-1} \}\)
in state \(q_{i+1}\), where \(m_{j,k_j}\) is a weak message and \(k_j
\geq 1\)\@.
%
\item
Node \(v_j\) sends a weak message:
\(\mathit{sbl}^i = \ \{\vec{m'}_0 v_0 \vec{m'}_1 v_1 \dots \vec{m'}_{l-1} v_{l-1}
\vec{m'}_{l} v_l \vec{m'}_{l+1}\}.\)
Only one message sequence, \(\vec{m'}_j\), \( 1\leq j\leq l+1\)
in \(\mathit{sbl}^{i}\), is not the
same as in \(\mathit{bl}^{i+1}\)\@. Let \(\vec{m'}_{j} = \{m_{j,1} \dots
m_{j,k_j}\}\) in state \(q_i\). Then \(\vec{m}_j = \{ m' m_{j,1} \dots m_{j,k_j} \}\)
in state \(q_{i+ 1} \), where \(m'\) is a weak message\@.
\item
Node \(v_j\) receives a strong message and sends a strong
message:
\(\mathit{sbl}^i = \ \{\vec{m'}_0 v_0 \vec{m'}_1 v_1 \dots \vec{m'}_{l-1} v_{l-1}
\vec{m'}_{l} v_l \vec{m'}_{l+1}\}.\)
Only two message sequences, \(\vec{m'}_j\) and \(\vec{m'}_{j+1}\),
\(0 \leq j\leq l\) in \(\mathit{sbl}^{i}\) are not the same as in \(\mathit{bl}^{i+1}\)\@.
Let \(\vec{m'}_j = \{m_{j,1} \dots m_{j,k_j-1} m_{j,k_j} \}\)
and \(\vec{m'}_{j+1} = \{m_{j+1,1} \dots m_{j+1,k_j}\}\) in
state \(q_i\). Then \(\vec{m}_j = \{m_{j,1} \dots m_{j,k_j-1} \}\) and
\(\vec{m}_{j+1} = \{ m'm_{j+1,1} \dots m_{j+1,k_j}\}\),
where \(m_{j,k_j}\) and \(m'\) are strong messages\@.
\item
A node that is not in the block receives \(m_{l+1,k_l}\), a
strong message from the block:
\(\mathit{sbl}^i = \ \{\vec{m'}_0 v_0 \vec{m'}_1 v_1 \dots \vec{m'}_{l-1} v_{l-1}
\vec{m'}_{l} v_l \vec{m'}_{l+1} \}\).
Only \(\vec{m'}_{l+1}\) in \(\mathit{sbl}^{i}\) is not the same as in
\(\mathit{bl}^{i+1}\)\@.
Let \(\vec{m'}_{l+1} = \{m_{l+1,1} \dots m_{l+1,k_l-1} m_{l+1,k_l}\}\)
in state \(q_i\). Then \(\vec{m}_{l+1} = \{m_{l+1,1} \dots
m_{l+1,k_j-1}\}\)
in state \(q_{i+1}\), where \(m_{l+1,k_l}\) is a strong message\@.
\item
A new node is added to the block after receiving a strong
message from the block:
\(\mathit{sbl}^i = \ \{\vec{m'}_0 v_0 \vec{m'}_1 v_1 \dots \vec{m'}_{l-1} v_{l-1}
\vec{m'}_{l} \}\)\@.
\(\vec{m'}_{l}\) in \(\mathit{sbl}^{i}\) is not the same as in \(\mathit{bl}^{i+1}\); and
both \(v_l\) and \(\vec{m}_{l+1}\) in \(\mathit{bl}^{i+1}\), but not in
\(\mathit{sbl}^i\)\@.
Let \(\vec{m'}_{l} = \{m_{l,1} \dots m_{l,k_l-1} m_{l,k_l} \}\)
in state \(q_i\). Then \(\vec{m_l} = \{m_{l,1} \dots m_{l,k_j-1}\}\)
in state \(q_{i+1}\)\@. In operation \(\pi_i\), \(v_l\) changes its state
and is captured to \(\mathit{sbl}^i\) after it receives the strong message \(m_{l,k_l}\) and sends
the strong message \(m'\), where \(\vec{m}_{l+1} = \{ m' \}\)\@.
%
\item
The block did not change: \(\mathit{bl}^{i+1}\) = \(\mathit{sbl}^{i}\)\@.
%
\end{enumerate}
\end{alabsubtext}
%
\apar{6.2-6}
Before we prove the lemma, we will state and prove a few claims
that are used in the proof of the lemma\@.
%
\begin{alabsubtext}{Claim}{1}{}
\label{claim0}
If \(\mathsf{parent}_w^i \neq \mathsf{nil}\) in state \(q_i\), which is after \(s_1\),
then \(\mathsf{selected}_w^i\) is equal to the body part of the last message
received through port \(\mathsf{parent}_w^i\)\@.
% \end{claim}
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Claim}{1}{}
\prooffontshape
\apar{Proof of Claim 1-1}
Let \(\pi_j\) be the last operation before state \(q_i\) in
which a message \(m\) is received over port \(\mathsf{parent}_w^i\)\@.
By the time-out procedure and by the definition of state
\(s_1\), such a \(\pi_j\) exists\@. The value of \(\mathsf{parent}_w\) does
not change
in all the states from \(q_{j+1}\) to \(q_i\), because if it
changes in \(\pi_k\), then it changes either to nil or to the
port over which a message was received in \(\pi_k\) (lines 11--13)\@.
%
\apar{Proof of Claim 1-2}
Since by the code, whenever the value of selected changes, the value of
parent changes too, neither \(\mathsf{selected}_w\) has changed in any
state from
state \(q_{j+1}\) to \(q_i\)\@. Thus
\(\mathsf{selected}_w^{j+1} = \mathsf{selected}_w^i\)\@.
To complete the proof, we need to show that
\(\mathsf{selected}_w^{j+1} = \mathsf{msg}(m)\)\@.
We consider two cases: either \(\mathsf{selected}_w\) changes in \(\pi_j\), or
it does not change\@. In the former, \(\mathsf{selected}_w^{j+1} = \mathsf{msg}(m)\) by
lines 11 and 12;
and in the latter, \(\mathsf{selected}_w^{j+1} = \mathsf{msg}(m)\) by line 5\@.
{\nopagebreakbeginpar\markendlst{Proof of Claim 1}}
\end{alabsubtext}
%
\begin{alabsubtext}{Claim}{2}{}
\label{claim0.5}
If \(\mathsf{prev}_v^i \neq zero_v\) in state \(q_i\) which is after \(s_1\),
then \(\mathsf{prev\_ports} \neq \emptyset\), and
for every \(p\) such that \(p \in \mathsf{prev\_ports}^i_v\),
\(\mathsf{prev}_v^i\) equals the body part of the last message
received through port \(p\) at operation \(\pi_j\), and
\(p \in \mathsf{prev\_ports}_v^l\) and
\(\mathsf{prev}^i_v = \mathsf{prev}^l_v\) for \(j+1 \leq l \leq i\)\@.
% \end{claim}
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Claim}{2}{}
\prooffontshape
\apar{Proof of Claim 2-1}
Since \(\mathsf{prev}^i_v \neq zero_v\), then \(
\mathsf{prev\_ports}^i_v \neq \emptyset\) (by line 24)\@.
%
\apar{Proof of Claim 2-2}
Let \(\pi_j\) be the last operation before state \(q_i\) in
which a message \(m\) is received over port \(p\)\@.
Since port \(p\) is alive (lines 22 and 23) as argued in the previous
proof, such a \(\pi_j\) exists\@.
%
\apar{Proof of Claim 2-3}
Port \(p \in \mathsf{prev\_ports}_v\)
in all the states from \(q_{j+1}\) to \(q_i\), because otherwise
\(\mathsf{prev\_ports}_v^i\) does not include \(p\) (lines 17--21)\@.
%
\apar{Proof of Claim 2-4}
Since (by the code) whenever the value of \textsf{prev} changes, the group
of \textsf{prev\_ports} changes too (line 18),
neither \textsf{prev\_v} has changed in any state from
state \(q_{j+1}\) to \(q_i\)\@. Thus \(\mathsf{prev}_v^i = \mathsf{prev}_v^{j+1}\)\@.
To complete the proof, we need to show that \(\mathsf{prev}_v^{j+1} = \mathsf{msg}(m)\)\@.
We consider two cases: either \(\mathsf{prev}_v\) changes in \(\pi_j\), or
it does not change\@. In the former, \(\mathsf{prev}_v^{j+1} = \mathsf{msg}(m)\) by line 18;
and in the latter, \(\mathsf{selected}_w^{j+1} = \mathsf{msg}(m)\) by line 20\@.
{\nopagebreakbeginpar\markendlst{Proof of Claim 2}}
\end{alabsubtext}
%
\begin{alabsubtext}{Claim}{3}{}
\label{claim1}
If in operation \(\pi_i\), after state \(s_1\),
node \(v\) is captured
by another node (i.e., \(v\) performs lines 11 and 12 and \(\mathsf{selected}_v\)
is changed to
a value different from \(zero_v\)), then:
\begin{enumerate}
\item \(\mathsf{selected}_v^{i} = zero_v\), and
\item the \textsf{msg} part of the last message that \(v\) sends to each of its
outgoing neighbors
before operation \(\pi_i\) is equal to \(\mathsf{next}(zero_v,p)\),
where \(p\) is the port-id through which the message is sent\@.
\end{enumerate}
% \end{claim}
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Claim}{3}{}
\prooffontshape
\apar{Proof of Claim 3-1}
Since node \(v\) is captured at operation \(\pi_i\), then in state,
\(q_i\), by lines 9 and 10,
\begin{equation}
\label{eq1}
select(\mathsf{prev}^i_v,\mathsf{selected}^i_v) = \mathsf{prev}^i_v
\end{equation}
If \(\mathsf{prev}^i_v = zero_v\), then \(\mathsf{selected}^i_v = zero_v\) (by Equation 1 and line
2), and
we are done\@.
Otherwise, \(\mathsf{prev}^i_v \neq zero_v\), and hence \(
\mathsf{prev\_ports}^i_v \neq \emptyset\) (by line 24)\@.
From Claim 2 there exists an
operation \(\pi_k,k*
potential(\mathrm{bl}^{l})-1\)\@.
Hence in \(\pi_l\) after receiving \(m2\),
\(u\) sends another strong message that belongs to \(\mathrm{bl}^{l+1}\)
and \(u\) performs lines 3 and 4 or 10--12\@. Let us consider the two cases:
%
\begin{enumerate}
\item If line 4 is performed,
then \(\mathsf{in\_port}_u(v) = parent^l_u\), and \(\mathsf{msg}(m2) = \mathsf{selected}_u^l\)
(line 3); but
by Claim 1, \(\mathsf{selected}_u^l = \mathsf{msg}(m1)\),
and this is a contradiction since
\(\mathsf{msg}(m1) \neq \mathsf{msg}(m2)\)\@.
\item In case lines 8 and 9 are performed,
then \(\mathsf{in\_port}_u(v) \in \mathsf{prev\_ports}^l\) and \(\mathsf{prev}_u^l = \mathsf{msg}(m2)\)
(line 10), but by Claim 2, \(\mathsf{prev}_u^l = \mathsf{msg}(m1)\),
and this is a contradiction because \(\mathsf{msg}(m1) \neq \mathsf{msg}(m2)\)\@.
Hence \(potential(\mathrm{bl}^{l+1}) \leq potential(\mathrm{bl}^{l})-1\)\@.
\end{enumerate}
\end{enumerate}
%
{\nopagebreakbeginpar\markendlst{Proof of Claim 5}}
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{4}{}
\prooffontshape
\apar{Proof of Lemma 4-1}
Let \(q_s\) be a state after \(s_1\), and let \(q_w\) be a state that
is \(nB + n + 3\) time units after \(q_s\)\@.
We prove that at state \(q_w\)
the potential of every phony block reaches zero\@.
Assume to the contrary that in state \(q_w\)
the potential of a particular block \(\mathrm{bl}^w\) is not zero\@.
Hence, there exists a strong message which we denote as \(m^w\),
where \(m^w \in \mathrm{bl}^w\)\@.
Let \(\mathrm{bl}^{s} \mathrm{bl}^{s+1} \dots \mathrm{bl}^{w}\) be the progression of
the block from state \(q_s\) to \(q_w\), and
let \(m^s m^{s+1} \dots m^w\) be the traversal of the message
in the different states \(q_s q_{s+1} \dots q_w\)\@.
%
\apar{Proof of Lemma 4-2}
Let us look at the group of operations \(\{\pi_i\}_{s \leq i \leq
w-1}\)\@.
The following two observations about the remainder of
\(m^i\) and the potential
of \(\mathrm{bl}^i\) are true:
%
\begin{enumerate}
\item
At least \(nB + n + 3\) times, there is an operation \(\pi_{i}\)
such that a node in \(\mathrm{bl}^i\) receives \(m^{i}\)
and sends \(m^{i+1}\) (cases 1 and 3 of Corollary 5)\@.
Hence at least \(nB+n+3\) times,
\(remainder(m^{i+1},\mathrm{bl}^{i+1}) = remainder(m^{i},sb^{i})-1\)\@.
%
\item
At most \(nB+1\) times, an operation \(\pi_i\) exists such that
a node is captured by block \(\mathrm{bl}^i\)
(cases 2 and 3 of Corollary 5)\@.
%
\par\noindent This follows from three main points:
%
\begin{enumerate}
\item by Observation 6, \(potential(\mathrm{bl}^{i+1}) \leq potential(\mathrm{bl}^{i})\)\;
\item by Claim 5, between every two consecutive operations in which
a node is captured by the block, there is an operation \(\pi_l\) such that
\(potential(\mathrm{bl}^{l+1}) \leq potential(\mathrm{bl}^{l})-1\)\@; and
\item by Corollary 3, \(potential(\mathrm{bl}^s) \leq nB\)\@.
\end{enumerate}
\end{enumerate}
%
By Observation 4, \(remainder(m^s,\mathrm{bl}^s) \leq n+1\)\@.
\(remainder(m^{w},\mathrm{bl}^{w}) = remainder(m^s,\mathrm{bl}^s)+
\Sigma_s^{w-1} (remainder(m^{i+1},\mathrm{bl}^{i+1}) -
remainder(m^{i},\mathrm{bl}^{i}))
\leq n+1 + (-1)*(nB+n+3) + (+1)*(nB+1) = -1 < 0\)\@.
This is a contradiction, since by Observation
4 \(remainder(m^w,\mathrm{bl}^w) \geq 0\)\@.
{\nopagebreakbeginpar\markendlst{Proof of Lemma 4}}
\end{alabsubtext}
%
\apar{6.2-11}
Let \(s_2\) be the state where the potential of every phony
block equals zero\@.
Let \(q_m\) be a state, after state \(s_2\), and let \(q_p\) be a state
that is two time units after \(q_m\)\@.
Let \(\mathrm{bl}^m \mathrm{bl}^{m+1} \dots \mathrm{bl}^p = \mathrm{bl}\) be the
progression of a phony block \(\mathrm{bl}\) from state \(q_m\) to state \(q_p\)\@.
%
\begin{alabsubtext}{Lemma}{5}{}
\label{lem:4.5}
If the number of nodes in \(\mathit{bl}^p\)
is \(k\), then the number of nodes
in \(\mathit{bl}^m\) at state \(q^m\) is at least \(k+1\)\@.
\end{alabsubtext}
\begin{alabsubtext}{Proof of Lemma}{5}{}
\prooffontshape
\apar{Proof of Lemma 5-1}
Let \(v\) be the tail node in \(\mathrm{bl}^m\) at state \(q_m\)\@.
Clearly, \(\mathsf{parent}_v \neq\) nil, since otherwise
\(\mathsf{selected}_v = zero_v\) (by line 1),
which is a contradiction to the fact that \(v\) belongs to a phony
block\@.
Let \(\mathsf{parent}_v = \mathsf{in\_port}_v(u)\), where \(u\) is an outgoing neighbor
of \(v\)\@.
%
\apar{Proof of Lemma 5-2}
To prove the lemma, we
show that at a maximum of two time units after \(q_m\)
there exists an operation such that \(\mathsf{selected}_v\) changes\@.
This is sufficient, since no new nodes can be captured by
any phony block after
state \(s_2\)\@.
%
\apar{Proof of Lemma 5-3}
Let \(p\) be the previous
element to the tail of block \(\mathrm{bl}^m\) at \(q_m\)\@.
By property 6 of the block definition, \(p \cup \mathrm{bl}^m\) is not a block\@.
%
\apar{Proof of Lemma 5-4}
There are two cases to consider: (1) \(p\) is a message \(m\) that is
transfered from \(u\) to \(v\), or
(2) \(p\) is node \(u\)\@.
%
\apar{Proof of Lemma 5-5}
In case \(p\) is a message, then
after a maximum of one time unit the first node in the block
receives \(m\) from its parent such that \(\mathsf{msg}(m) \neq \mathsf{selected}_v\)
(since \(m\) cannot be added to the block) and \(\mathsf{selected}_v\)
changes to \(zero_v\) by lines 6 and 7\@.
%
\apar{Proof of Lemma 5-6}
In case \(p\) is a node, then after at most one time unit from \(q_m\),
\(u\) sends a message \(m\) by time-out\@.
Message \(m\) cannot be added to the phony block,
and after one time unit node \(u\) still cannot be added to the block
(no new phony nodes can be captured after \(s_2\))\@.
Hence, we are again in case 1\@.
{\nopagebreakbeginpar\markendlst{Proof of Lemma 5}}
\end{alabsubtext}
%
\begin{alabsubtext}{Lemma}{6}{}
\label{lem:5}
In \(O(n)\) time units after \(s_2\), there are no phony blocks\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{6}{}
\prooffontshape
\apar{Proof of Lemma 6-1}
Within \(O(n)\) time units after \(s_2\), the
block contains only a weak message sequence (no nodes at all)\@.
This follows from the following facts:
\begin{itemize}
\item by Lemma 5, in each \(O(1)\) time units
after state \(q_m\), the number of nodes
in a block is reduced by at least one;
\item there are at most \(n\) nodes in a phony block to start with; and
\item no new nodes can be added to a phony block after state
\(s_2\) (since the potential of a phony block equals zero)\@.
\end{itemize}
%
\apar{Proof of Lemma 6-2}
Within \(O(1)\) time units after that state, the weak-message sequence
also disappears\@. This follows from the following statements:
(1) weak messages can be sent only in a time-out; and (2) there is no
node in the phony block to send them\@.
{\nopagebreakbeginpar\markendlst{Proof of Lemma 6}}
\end{alabsubtext}
%
Let \(s_3\) be the global state in which there are no phony blocks\@.
%
\begin{alabsubtext}{Definition}{16}{}
\label{sec:sta}
\(\mathsf{Selected}_v^i\), the \textsf{selected} value of node \(v\) at state
\(q_i\),
is a derivative of \(zero_u\) if there is a \(u\)-to-\(v\) path,
\(\{ v_1 v_2 \dots v_k \}\), where \(u = v_1\) and \(v = v_k\),
and an assignment to the variables of all the nodes along the path
that defines a block on the path subject to
\(\mathsf{selected}_u = zero_u\) and
\(\mathsf{selected}^i_{v_{j+1}} = \mathsf{next}(\mathsf{selected}^i_{v_j},
\mathsf{out\_port}_{v_j}(v_{j+1}))\), where \(0 \leq j \leq k-1\)\@.
The path is called the \emph{derivation path from u to v}\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Observation}{7}{}
\label{ob:der}
The selected value of any node in a state after \(s_3\)
is a derivative of some zero value of a node in the network\@.
\end{alabsubtext}
%
The observation follows, since there are no phony blocks in the network\@.
%
\begin{alabsubtext}{Definition}{17}{}
{\bf (Stabilization Properties)}\\
Each framework that is suitable for our generic algorithm
defines a set of legal global and final states such that
the following properties hold:
\begin{enumerate}
\item
Each node has a stable and legal \textsf{selected} value\@.
Node \(v\) has a legal \textsf{selected} value at the state after \(s_3\),
if its derivation
path, \(\{ v_0, v_1, \dots, v_k, v \}\), denoted by the legal derivation
path of
\(v\), satisfies the following properties:
%
\begin{enumerate}
\item
There is a unique node denoted \(r\), the root of the tree,
such that \(v = r\) and \(r\)'s legal \textsf{selected} value is \(zero_r\)\@.
Otherwise, if \(v \neq r\),
\(\mathsf{selected}_v\), the legal value of node \(v\), is a derivative of
\(zero_r\), i.e., \(v_0 = r\)\@.
\item
For every \(0 \leq i \leq k\), \(\{ v_0, v_1, \dots , v_i \}\) is a legal
derivation path for a legal \(\mathsf{selected}_{v_i}\) value\@.
\item
A legal \textsf{selected} value of node \(v\) is
selected as \(\mathsf{selected}_v\) over any other suggestion for
a nonlegal \textsf{selected} value which is a derivative of some
zero value of a node in the network\@.
\end{enumerate}
\item
Each node has a stable parent\@. The parent of \(r\) is nil, and
the parent of every other node is
a pointer to one of its incoming neighbors\@.
The graph induced by the parent relationship is a tree\@.
\end{enumerate}
\end{alabsubtext}
%
\begin{alabsubtext}{Definition}{18}{}
A block is a legal derivation block of \(v\) laid over the derivation path
\emph{dp}, if the block is on the path dp and
the assignment of the \textsf{selected} values of all the nodes
along dp is legal\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Remark}{4}{}
A node can have more than one legal \textsf{selected}
value; hence there can be more than one legal derivation path and
legal derivation block\@.
\end{alabsubtext}
\begin{alabsubtext}{Observation}{8}{}
\label{ob:dbl}
If \(v\) has a legal \textsf{selected} value after \(s_3\), then any block
that contains \(v\) must be a block or a subblock of a legal
derivation block\@.
\end{alabsubtext}
%
\apar{6.2-12}
The observation follows from property (b)\@.
%
\begin{alabsubtext}{Observation}{9}{}
\label{ob:sb}
Let \(\mathit{bl}\) be a block or a subblock of a legal derivation block.
Then the source of \(\mathit{bl}\) is a block or subblock of a legal derivation
block\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Lemma}{7}{}
\label{lem:b}
In any state \(q_i\) which is \(O(n)\) or more time units after \(s_3\),
if \(\mathsf{selected}_v\) is legal, then there exists a legal derivation
block based on the derivation path from \(r\) to \(v\)\@.
\end{alabsubtext}
%
\apar{6.2-13}
Before proving the lemma, let us define:
%
\begin{alabsubtext}{Definition}{19}{}
A block without power supply is a block whose
tail's \textsf{selected} value is not a \emph{zero} value\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Observation}{10}{}
\label{ob:po}
A legal derivation block is a block with power supply\@.
\end{alabsubtext}
%
\apar{6.2-13}
The proof of the lemma is based on the following two claims:
%
\begin{alabsubtext}{Claim}{6}{}
\label{cla:11}
Let \(\mathit{bl}\) be a block without power supply at a state after \(s_3\),
then after \(O(n)\) time units the block disappears\@.
% \end{claim}
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Claim}{6}{}
\prooffontshape
The proof of the claim is similar to the
proof of Lemma 6, and will not be repeated here\@.
The intuition is that a phony block is also a block without power
supply\@.
The same properties hold for a phony block that disappears
and a block without power supply\@.
{\nopagebreakbeginpar\markendlst{Proof of Claim 6}}
\end{alabsubtext}
%
Consider a state \(q_i\) after \(s_3\) in which \(\mathsf{selected}_u\)
is a legal
value, and a legal derivation block is laid over
\emph{ldp}, the legal derivation path from
\(r\) to \(u\). Then the following claim applies.
%
\begin{alabsubtext}{Claim}{7}{}
\label{cla:22}
At any state after \(q_i\), \(u\) has a legal derivation block which is
laid over ldp\@.
% \end{claim}
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Claim}{7}{}
\prooffontshape
\apar{Proof of Claim 7-1}
Assume, to the contrary, that there is an operation \(\pi_w\)
such that at state \(q_w\), after \(q_i\), there is a
legal derivation block laid over ldp, and
in state \(q_{w+1}\) after this operation
there is no legal derivation block on ldp\@.
%
\apar{Proof of Claim 7-2}
Hence, some node from ldp changes its state in operation
\(\pi_w\)\@. Let \(v\) be that node\@. By property (b) of a legal
derivation path,
\(v\) has a legal \textsf{selected} value\@. By property (c), it cannot be
that \(v\) changes its state in \(\pi_w\)\@: contradiction\@.
{\nopagebreakbeginpar\markendlst{Proof of Claim 7}}
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{7}{}
\prooffontshape
%
\apar{Proof of Lemma 7-1}
Assume, to the contrary, that
there exists a node \(v\) in state \(q_i\), \(O(n)\) after \(s_3\)
such that \(\mathsf{selected}_v\) is
legal, but there is no legal derivation block\@.
Let \(\mathrm{bl}'\) be a block that contains \(v\)\@.
Block \(\mathrm{bl}'\) must be a subblock of a legal derivation block at
state \(q_i\) (by Observation 8);
hence by Observation 10, \(\mathrm{bl}'\) is a block without power
supply\@.
%
\apar{Proof of Lemma 7-2}
By Claim 6, the source of \(\mathrm{bl}'\) at state \(q_m\) before
\(s_3\) is a block with power supply\@.
Therefore, there is an operation after \(s_3\), denoted by \(\pi_p\),
because of which the block is without power supply\@.
But this is impossible, since at state \(q_p\) the source of \(\mathrm{bl}'\)
is a legal derivation block (by Observation 9)
and by Claim 7, the source
of \(\mathrm{bl}'\) at state \(q_{p+1}\) is also
a legal derivation block; hence a block with power supply
(by Observation 10)\@. This is a contradiction; hence the lemma\@.
{\nopagebreakbeginpar\markendlst{Proof of Lemma 7}}
\end{alabsubtext}
%
\begin{alabsubtext}{Lemma}{8}{}
\label{lem:s}
In \(O(n)\) time units after \(s_h\), the network enters state \(s_4\) and
a legal final state \(L\) such that in any state after \(s_4\) the
network is in state \(L\)\@.
In the legal final state \(L\),
a rooted tree (as required) spans the network\@.
%
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{8}{}
\prooffontshape
\apar{Proof of Lemma 8-1}
The proof is based on an inductive assumption that
at state \(q_k\) (which is at least \(2k\) time units after \(s_h\)),
every node that has at least one
legal derivation path that contains \(k\) nodes in its \textsf{selected}
value is legal\@.
%
\apar{Proof of Lemma 8-2}
\emph{Base}: For \(k = 1\), we should prove that the inductive assumption
holds for \(r\)\@. By property (a) of legal derivation path,
\(zero_r\) is
selected as a legal value of \(\mathsf{selected}_r\)
from all the derivative \textsf{selected} values for node \(r\)\@.
Hence by line 2 and by Observation~7 the result holds\@.
%
\apar{Proof of Lemma 8-3}
\emph{Step}: Assuming the inductive assumption holds for \(k\), then
we prove
it for \(k+1\)\@.
Let \(v\) be a node that has a legal derivation path with \(k+1\) nodes\@.
By property (b) of a legal derivation block,
node \(v\) has a neighbor \(w\) with a legal derivation
path with \(k\) nodes, and hence the inductive assumption holds for node
\(w\)\@. Therefore, by Lemma 7, a legal derivation block exists for
node \(w\) at state \(q_k\) which is at least \(2k\) time units after
\(s_h\)\@.
Node \(w\) receives a strong message in every time unit from its parent
in the legal derivation block\@. This follows from the fact that
the tail of a legal derivation block is \(r\) and
\(\mathsf{selected}_r = zero_r\)
(by property a of a legal derivation block),
and \(r\) sends a strong message on all of its outgoing links
every time unit (by procedure time-out line 30)\@.
Hence at \(q_{k+1}\), the state that is at least \(2(k+1)\) time
units after \(s_h\), \(v\) receives two strong messages from \(w\)\@. The body
part of these messages is a suggestion for a legal \textsf{selected}\@.
If those suggestions are selected as \(\mathsf{selected}_v\), then
upon receiving the first message, \textsf{prev} is updated
(lines 14--21), and upon receiving the second message,
\textsf{selected} is updated (lines 11--13)\@.
Therefore, at \(q_{k+1}\), \(\mathsf{selected}_v\)
has a legal value\@.
Otherwise, this suggestion for \(\mathsf{selected}_v\)
is not selected as \(\mathsf{selected}_v\)\@.
By property c of a legal derivation block,
the latter can happen only if \(\mathsf{selected}_v\) already has
a legal \textsf{\emph{selected}} value\@. Hence the lemma holds\@.
{\nopagebreakbeginpar\markendlst{Proof of Lemma 8}}
\end{alabsubtext}
%
\apar{6.2-14}
This completes the proof of the main theorem\@.
%
\begin{alabsubtext}{Lemma}{9}{}
\label{lem:6}
The time complexity of the BFS is \(O(D)\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{9}{}
\prooffontshape
The same inductive assumption as in Lemma 8
holds, with some changes when the starting point is a state after \(s_1\)
and
not after \(s_3\)\@.
{\nopagebreakbeginpar\markendlst{Proof of Lemma 9}}
\end{alabsubtext}
%
\begin{alabsubtext}{Remark}{5}{}
The proof ignored a remark that was made about
the model in Sections~2 and~4,
thus assuming that the rate at which messages are processed
is faster than the rate at which links transmit them\@.
It is easy to modify the proof to hold with the remark\@.
In effect, the remark is equivalent to losing some messages
on the links which may only
decrease the potential of phony blocks, and does not disturb the
power-supply principle\@. Notice that in the remark we introduce two
buffers at each port, thus preventing the possibility of a
few blocks uniting into one block, i.e., not affecting the correctness
of Lemma 3\@.
\end{alabsubtext}
%
\asubsection{6.3}{Conclusions}
\apar{6.3-1}
A simple method for designing self-stabilizing algorithms
for unidirectional and bi-directional networks has been
presented in this paper. The key advantages of our methodology
are its simplicity, it works in arbitrary synchronous and
asynchronous unidirectional networks, and it does not require
any a priori knowledge about the network topology or size.
The algorithms presented here stabilize in \emph{O(n)} time units,
and any fake message disappears in time that is
proportional to the number of the fake messages in the greatest
phony block. To demonstrate the capabilities of our
methodology, we present algorithms for constructing DFS and BFS trees.
These trees are up-trees, that is, there exists a path in the
tree from the root to any node.
%
\apar{6.3-2}
An open question is to design an algorithm under similar
assumptions and complexities but for the construction of a
down-tree, that is, a tree in which there is a unidirectional
path from any node to the root. The combination of up-tree
and down-tree algorithms would facilitate the automatic
translation of any bidirectional distributed algorithm into a
unidirectional self-stabilizing version of the algorithm.
% set appendix as A-hed, but spell out 'Appendix'
\asection{Appendix:}{The Lower Bound of the Synchronous Algorithm} \label{sec:example}
\appendix
%
\apar{A-1}
In Figure 6, a simple scenario in which our algorithm has
\(\Omega (n)\) time complexity is presented\@.
In the figure, beside each node we have placed the record
[leader, distance from the leader], plus the node id in bold-face type\@.
Let us look at the block of size \(n-1\) with a fake id of 1\@.
To simplify, we describe the scenario under the synchronous model\@.
In every round, only one node from the block with fake id 1 disappears;
this is the node with the smallest distance in the block\@.
%
\apar{A-2}
For example, in the first round, the node with an id of 80
changes its state, since it receives only one message [10, 0] from node
10, and according to this message its leader should be 10
and not 1\@.
Assuming this is the first time node 80 receives the change, the node
changes its state to [80, 0]; otherwise, it changes to [10, 1]\@.
All other nodes in the block with fake id 1 do not change their
state, because they get a message that reassures their state from their
incoming neigbor in the block of fake id 1\@.
Similarly, in the next round, node 70 changes its
state, since it receives the messages [80, 0] or [10, 1] from node
80 and [10, 0] from node 10, which do not support its current leader, 1\@.
All other nodes in the block with a fake id of 1 do not
change their states because they get messages that reassure their
states from their incoming neigbors in the block with fake id of 1\@.
Hence, after only \(n-1\) rounds,
the block with a fake id of 1 disappears, even though the diameter of the
network is 2\@.
%
\begin{figure*}[htbp]
\begin{center}
\fbox{
%\psfig{file=example.eps}
\psfig{file=cj9803f6.eps}
}
\afigcap{6}{An example}
\end{center}
\label{fig:ex}
\end{figure*}
\clearpage
\end{articletext}
%
\begin{articlebib}
\bibliographystyle{alpha}
\bibliography{cj98-03}
\end{articlebib}
%
\end{document}
*