% 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<i\) in which a message \(m\) is received
over  port \(p\), \(p \in \mathsf{prev\_ports}^i_v\)\@.
 Let \(\pi_j\) be the
last such operation before \(q_i\)\@.
From Claim 2, \(p \in \mathsf{prev\_ports}_v^l\), and
  \(\mathsf{msg}(m) = \mathsf{prev}^i_v = \mathsf{prev}^l_v\) for \(j+1 \leq l \leq i\)\@.
%
\apar{Proof of Claim 3-2}
To complete the proof of the first part of the claim, we prove
 that if the value of \(\mathsf{selected}_v\) has changed in \(\pi_l\),
\(j+1 \leq l \leq i\), then in the last such change \(\mathsf{selected}_v\)
was set to \(zero_v\); otherwise it was set to \(zero_v\) in
\(\pi_j\),
and thus \(\mathsf{selected}_v^i = \mathsf{selected}_v^j = zero_v\)\@.
To prove this,  consider an operation
\(\pi_r\), \(j \leq r<i\)  such that  \(\pi_r\) is the
last time  before \(\pi_i\) that the value of
 \(\mathsf{selected}_v\) is changed\@.
Notice that such an operation exists\@.
%
\apar{Proof of Claim 3-3}
Assume, to the contrary,
that there is no such operation \(\pi_r\).
Then, in \(\pi_j\), \(v\) receives a message \(m\) such that
\(\mathsf{msg}(m) = \mathsf{prev}^i_v\) and
select(\(\mathsf{prev}^i_v\), \(\mathsf{selected}^i_v\)) =
 select(\(\mathsf{prev}^i_v\), \(\mathsf{selected}^j_v\)) =
\(\mathsf{prev}^i_v\). 
Hence \(\mathsf{selected}_v\) must have changed its value in \(\pi_j\)
by lines 9--16, in contradiction to the fact that there is no change in the
value of \(\mathsf{selected}_v\)
in any operation \(j \leq r <i\)\@.
%
\apar{Proof of Claim 3-4}
By definition of \(\pi_r\), \(\mathsf{selected}^{r+1}_v
= \mathsf{selected}_v^i\)\@.
The value of \(\mathsf{selected}_v\) changes in \(\pi_r\) to either
\(\mathsf{prev}_v^r\) or \(zero_v\)
(either in line 11 or lines 6--14)\@.
%
\apar{Proof of Claim 3-5}
In the latter case,  \(\mathsf{selected}^{r+1}_v = \mathsf{selected}_v^i =
zero_v\), and
the claim follows\@.
We claim the former is impossible, i.e., \(\mathsf{selected}_v\) may
not change
to \(\mathsf{prev}_v\) in \(\pi_r\)\@. Otherwise,
 \(\mathsf{prev}_v^{r+1} = \mathsf{selected}^{r+1}_v\), and since \(\mathsf{prev}_v^{r+1} =
\mathsf{prev}_v^i\), then \(\mathsf{prev}^i_v = \mathsf{selected}^i_v\), in contradiction to
Equation~1\@.
%
\apar{Proof of Claim 3-6}
In \(\pi_r\), node \(v\) also sends
a message with the \textsf{msg} part equal to \textsf{next}\((zero_v,p)\) (lines 8
or 16)\@.
In all the
operations \(r<k<i\), \(\mathsf{selected}_v^k = zero_v\), and \(v\) can send
a message only
by performing a procedure time-out (lines 28--30), such that the \textsf{msg} part
equals \(\mathsf{next}(\mathsf{selected}_v^k,p) = \mathsf{next}(zero_v,p)\); hence the 
second part of the claim holds\@.
{\nopagebreakbeginpar\markendlst{Proof of Claim 3}}
\end{alabsubtext}
%
\begin{alabsubtext}{Claim}{4}{} \label{claim2}
Let \(\pi_l\) be an operation after \(s_1\) but before state \(q_i\)\@.
If in \(\pi_l\) \(v\) sends to its outgoing neighbor
\(w\) message \(m_l\), such that
\(\mathsf{msg}(m_l) = \mathsf{next}(zero_v,\mathsf{out\_port}_v(w))\),
and if either
%
\begin{enumerate}
\item message \(m_l\)  is the last message that
arrives at \(w\) before \(q_i\), or
\item  message \(m_l\) has not yet arrived at \(w\) in state \(q_i\),
\end{enumerate}
%
then in state \(q_i\) there is no phony
block \(\mathit{bl}^i\) such that both \(v\) and \(w\) are \(\in \mathit{bl}^i\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Claim}{4}{}
\prooffontshape
\apar{Proof of Claim 4-1}\\
Case 1: Let \(\pi_j\) be the operation in which
message \(m_l\) is received by node \(w\)\@.
%
\apar{Proof of Claim 4-2}
If in \(q_i\) there is a block \(\mathrm{bl}^{i}\)
such that \(v,w\in \mathrm{bl}^i\), then
parent\(_w^i = \mathsf{in\_port}_w(v)\), and from Claim 1,
\(\mathsf{selected}_{w^i}\) equals the \textsf{msg} part of \(m_l\), the
last message
that was received from the parent port\@.
Hence \(\mathsf{selected}_v^i = \mathsf{next}(zero_v,\mathsf{out\_port}_v(w))\), a
contradiction to the fact that \(\mathrm{bl}^i\) is  a phony block\@.
%
\apar{Proof of Claim 4-3}
Case 2: Message \(m^l\) has not yet been received by \(w\)\@.
Assume the opposite, that \(v,w\in \mathrm{bl}^i\)\@.
Thus \(\{v \vec{m} w\}\) \(\subseteq \mathrm{bl}^i\), \(m^l\) \(\in \vec{m}\)\@.
By the definition of a block, \textsf{selected}\(_w^i = \mathsf{msg}(m^l)\)
= \(\mathsf{next}(zero_v,\mathsf{out\_port}_v(w))\),
and again this is a contradiction to the fact that the
block is a phony block\@.
{\nopagebreakbeginpar\markendlst{Proof of Claim 4}}
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{3}{}
\prooffontshape
\apar{Proof of Lemma 3-1}
Let us prove that subblock \(\mathrm{sbl}^i\)
must exist in state \(q_i\)\@.
To prove this, assume such an \(\mathrm{sbl}^i\) does not exist\@.
%
\apar{Proof of Lemma 3-2}
Then if the tail(\(\mathrm{bl}^{i+1})\) element exists in \(q_i\), then let
\(e\) be the first element (message or node) along the path induced
by \(\mathrm{bl}^{i+1}\) that may not be a member of \(\mathrm{sbl}^i\) because either it
has a different selected (when \(e\) is a node) or an inconsistent
parameter (when \(e\) is a message)\@. There are four cases to consider:
\begin{enumerate}
\item tail(\(\mathrm{bl}^{i+1})\) does not exist in \(q_i\),
\item \(e\) is a node,
\item \(e\) is a message, and
\item \(e\) does not exist\@.
\end{enumerate}
A general remark: by the code,
an operation \(\pi_i\) is exactly one
of the following:
\begin{enumerate}
\item sending one new message (by procedure time-out),
\item receiving one message,
\item receiving one message and sending one new message
without changing the node state, and
\item receiving one message, changing the state of node \(v\),
 and sending one new message from node \(v\)\@.
 \end{enumerate}
%
\apar{Proof of Lemma 3-3}
Case 1: Tail(\(\mathrm{bl}^{i+1}\)) does not exist in \(q_i\)\@.
If tail(\(\mathrm{bl}^{i+1}\)) is  a node, then this node has changed
its selected in \(\pi_i\)\@.
If tail(\(\mathrm{bl}^{i+1}\)) is a message, it must have been generated in
\(\pi_i\)\@.
Let us consider each of the two subcases (tail(\(\mathrm{bl}^{i+1}\)) is a node,
or a message)\@.
%
\apar{Proof of Lemma 3-4}
In the former subcase, let \(v\) be the node captured in \(\pi_i\)\@.
By Claim 3, if \(w\) is an outgoing neighbor of \(v\),
then the last message that \(v\) sent before
state \(q_i\) was message \(m\), such that
msg\((m) = \mathsf{next}(zero_v,\mathsf{out\_port}_v(w))\)\@.
%
\apar{Proof of Lemma 3-5}
By Claim~4, \(v\) and \(w\) may not be in the same phony
block in
state \(q_{i+1}\)\@.
Since \(v\) is the tail of block \(\mathrm{bl}^{i+1},\)
\(\mathrm{bl}^{i+1}\) contains only one node, \(v\)\@.
In operation \(\pi_i\), node \(v\) was captured after receiving a
message \(m'\),
and sent a strong message,
\(\widehat{m}\), with \(\mathsf{msg}(\widehat{m}) = \mathsf{next}(\mathsf{msg}(m'),\mathsf{out\_port}_v(u))\),
where \(u\) is an outgoing neighbor of \(v\) (by lines 11--13)\@.
Thus we are at case 5 of Lemma 3\@.
%
\apar{Proof of Lemma 3-6}
In the latter case, in operation \(\pi_i\),
some node \(v\) generates message \(m\), which is the tail of
\(\mathrm{bl}^{i+1}\)\@.
We claim that this case is impossible\@.
Message \(m\) is sent by \(v\) to outgoing neighbor \(w\) using the
procedure
\textsf{send\_neighbors}\@.  By performing this procedure, node \(v\) sent the
message
\(\mathsf{next}(\mathsf{selected}_v^{i+1},\mathsf{out\_port}_v(w))\)\@.  Hence from the
definition of a block and the fact that \(m\in \mathrm{bl}^{i+1}\),
\(v\cup \mathrm{bl}^{i+1}\) is also a block, a contradiction to the fact
that \(\mathrm{bl}^{i+1}\) is a block (violating condition 6 of the block
definition (Definition 5))\@.
%
\apar{Proof of Lemma 3-7}
Case 2: \(e\) is a node\@.
Thus \textsf{selected}\(_e^i \neq
\mathsf{selected}_e^{i+1}\), and
node \(e\) was captured in operation \(\pi_i\) (lines 11 and 12)\@.
By Claim 3, \textsf{selected}\(_e^i = zero_e\), and before state \(q_i\),
the last message \(e\) sent to its outgoing neighbor \(w\) was
a message such that \textsf{msg}\((e) = \mathsf{next}(zero_e,\mathsf{out\_port}_e(w))\)\@.
From Claim 4,  \(e\) and \(w\) cannot be at the same phony block at state
\(q_{i+1}\)\@; therefore we are again at case 5 of the lemma\@.
%
\apar{Proof of Lemma 3-8}
Case 3: \(e\) is a message\@.
If \(e\) is a weak message, then the
message was generated in \(\pi_i\)\@.  A weak message can be generated
only by
time-out (lines 29--31)\@.  Thus we are at case 2 of the lemma\@.
%
\apar{Proof of Lemma 3-9}
If \(e\) is a strong message, then the message was created in \(\pi_i\)
by some node \(v\)\@.
We claim that \(v\in \mathrm{sbl}^i\) and \(v\in \mathrm{bl}^{i+1}\)\@.
If \(v\in \) \(\mathrm{bl}^{i+1}\) and \(v\notin \mathrm{sbl}^i\), then
 \(e\) is that node \(v\) and not the message, a contradiction\@.
If \(v \notin \mathrm{bl}^{i+1}\), then in state \(q_{i+1}\) the message
\(\mathsf{msg}(e) = \mathsf{next}(\mathsf{selected}_v^{i+1},l)\) where 
\(l\)  is the port id of the link on which \(e\) is sent (procedure
send-neighbors)\@.  By the definition of block, \(v\cup \mathrm{bl}^{i+1}\)
is a block, in contradiction to condition 6 of
Definition 5\@.
Therefore,  \(v\in \mathrm{sbl}^i\) and \(v\in \mathrm{bl}^{i+1}\)\@.
Thus \(\mathsf{selected}_v^{i} = \mathsf{selected}_v^{i+1}\)\@.
A strong message may be sent without changing the status of a node
by performing:
\begin{enumerate}
\item line 29 (time-out), but then parent\(_v =\) nil and
\(\mathsf{selected}_v^{i+1} = zero_v\)
(from line 1), and this is a contradiction to the fact that the block is
a phony block; and
\item lines 3 and 4, which corresponds to case 3 of the lemma\@.
\end{enumerate}
%
\apar{Proof of Lemma 3-10}
Case 4: \(e\) does not exist\@.
In this case, we should check
if there is an element induced by \(\mathrm{sbl}^i\)
that is not a member of \(\mathrm{bl}^{i+1}\)\@.
Let \(d\) be the first element (message or node) along the path
induced by \(\mathrm{sbl}^i\) which is not a member of \(\mathrm{bl}^{i+1}\)\@.  We consider
two cases: (1) \(d\) is a node; and (2) \(d\) is a message\@.
If \(d\) does not exist,
then we are in case 6 of the lemma, \(\mathrm{sbl}^i = \mathrm{bl}^{i+1}\)\@.
%
\apar{Proof of Lemma 3-11}
\emph{Subcase 1: \(d\) is a message}. In operation \(\pi_i\),
some node \(v\) 
received \(d\)\@.
If \(v \in \mathrm{sbl}^i\), then if \(d\) is a strong message we are at case 3
of the lemma
(lines 3 and 4), and if \(d\) is a weak message, then we are at case 1 of
the lemma
(a weak message can only change the selected of a node to zero)\@.
If \(v\notin \mathrm{sbl}^i\), then \(d\) is the head of \(\mathrm{sbl}^i\)\@. If \(v\in
\mathrm{bl}^{i+1}\), we are
at the case that a new node is captured, which is case 5 of the lemma\@.
If \(v\notin \mathrm{bl}^{i+1}\), then only this message disappeared; thus we
are at case 1 of the lemma if it is a weak message,
or case 4 if it is a strong message\@.
%
\apar{Proof of Lemma 3-12}
\emph{Subcase 2: \(d\) is a node}. We show that in this case,
\(d\in \mathrm{sbl}^i\), but \(d\notin \mathrm{bl}^{i+1}\), which is impossible; thus, this
entire case is impossible\@. If \(d\) is the tail
of \(\mathrm{sbl}^i\), then without loss of generality, \(\mathrm{sbl}^i\) is defined as
the subblock of \(\mathrm{sbl}^i \setminus \{v\}\)\@.
If the head of \(\mathrm{sbl}^i\) is node \(x\) but \( x \notin \mathrm{bl}^{i+1}\),
then without loss of generality, \(\mathrm{sbl}^i\) is defined as
the subblock of \(\mathrm{sbl}^i \setminus x \)\@. Hence
head(\(\mathrm{sbl}^i) \in \mathrm{bl}^{i+1}\), and tail(\(\mathrm{sbl}^i) \in \mathrm{bl}^{i+1}\)\@.
Therefore without loss of generality, \(d\) is not the head or the tail
of \(\mathrm{sbl}^i\)
and there exists a node or a message \(r \in \mathrm{sbl}^i\)
which is the following
node or
message along the block \(\mathrm{sbl}^{i}\), and also \(r \in \mathrm{bl}^{i+1}\)\@.
Similarly, there
exists a node or a message \(y \in \mathrm{sbl}^i\)
that is a previous node or message along the block \(\mathrm{sbl}^i\), and also
\(y \in \mathrm{bl}^{i+1}\)\@.
In operation
\(\pi_i\), \(d\) changed its \(\mathsf{selected}_d\) or \(\mathsf{parent}_d\) so that
\(d \in \mathrm{sbl}^i\) but \(d\notin \mathrm{bl}^{i+1}\), however, the state of \(r\)
and \(y\) did not change; thus it is easy to see that
according to the definition of a block it
cannot be that both \(r\) and \(y\) are in the same block \(\mathrm{bl}^{i+1}\)\@.
{\nopagebreakbeginpar\markendlst{Proof of Lemma 3}}
\end{alabsubtext}
%
\begin{alabsubtext}{Corollary}{4}{}
\label{cor:1}
Let \(\pi_i\) be an operation after state \(s_1\). Then
potential(\(\mathit{sbl}^i) \geq potential(\mathit{bl}^{i+1})\)\@.
\end{alabsubtext}
%
\apar{6.2-7}
In Lemma 4, we prove that after
\(O(nB)\) time the potential of any phony block
reduces to zero\@.  More specifically, we show that all the strong
messages in a phony block disappear after (at most) that much
time\@.  To do that, we pick an arbitrary message on a phony
block, track its traversal of the block, and argue
that such a traversal cannot last more than \(O(nB)\)
units of time\@.
For the purpose of the proof, a strong message that is relayed
by a node from its in-port to its out-port is considered the same
message\@.
%
\apar{6.2-7}
In the formal proof, we follow the distance between the tracked
message and the head of the block (defined as
the \(remainder\) in Definition 10)\@.
However, this process and definition is problematic: in
continuing from the location of a specific message, a block may
branch into several blocks, because the overall structure is that
of a tree\@.  Thus, the specific block traversed by the message
is not well defined, and neither is the remainder of the
message\@.
To overcome this difficulty, we break the proof into
three steps\@.
In the first two steps of the proof, we run the algorithm
forward and then observe the block in a backward execution
of the same run\@.
This solves our problem, because when the algorithm is run backwards,
every block has a unique source subblock (based on Lemma 3)\@.
Then in the third step, we make the arguments necessary for the
proof on the sequence of steps and blocks defined in the
second step\@.
%
\apar{6.2-8}
The three steps of the proof are thus:
%
\begin{enumerate}
\item Run the algorithm forward \(nB+n+3\) time units, and
assume to the contrary that there
exists a block with  a nonzero potential,
and hence there is a strong message
in it\@. 
%
\item By a  backward simulation of the run on this block
and this message in previous states, build the progression
of the block and the traversal
of that message in different states\@.
%
\item Prove on the forward sequence of blocks that the
remainder of the message in that block,
\(nB+n+3\) time units after the initial step, is zero\@.
This last step is based on three points:
%
  \begin{enumerate}
  \item The remainder of the message in the initial state
  is at most \(n+1\)\@.
  \item At least \(nB+n+3\) times, the remainder of the message
  decreases by one,
  since at each time unit the message advances at least one more
  hop in the block\@.
  \item The number of times the remainder of the
  message increases by one is at most \(nB+1\), the initial potential of
  the block\@.
  The correctness of the third statement is based on the following
  points:
    \begin{itemize}
    \item the remainder of the message increases if a new node is
    captured by the block; 
    \item the block loses one strong message
    for every  node  that is captured by the block (except perhaps for
    the first node that is captured to the block; see Claim 5);
    \item the number of strong messages in the block is at most \(nB+1\); and
    \item by Lemma 3, the number of strong messages in a block
    cannot increase\@.
    \end{itemize}
  \end{enumerate}
\end{enumerate}
%
\begin{alabsubtext}{Lemma}{4}{}
\label{lem:4}
In \(O(nB)\) time units after state \(s_1\),
the potential of every phony block
is zero\@.
\end{alabsubtext}
%
\apar{6.2-9}
Before we prove the lemma, let us discuss some definitions\@.
%
\begin{alabsubtext}{Definition}{10}{}
\label{defrm}
Let \(\mathit{bl} = \ \{\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} \}\)
be a subblock\@. Define for each message \(m
\in\)  \(\vec{m}_j\), \(remainder(m,bl) = l+1-j\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Observation}{4}{}
\label{obs:re}
In any state, for every message \(m\) and subblock \(\mathit{bl}\),
\(0 \leq remainder(m,bl) \leq n+1\)\@.
\end{alabsubtext}
%
Let \(\pi_i\) be an operation after \(s_1\)\@.
Let \(\mathit{bl}^{i+1}\) be a phony block in state \(q_{i+1}\)\@.
%
\begin{alabsubtext}{Definition}{11}{}
The subsource of block \(\mathit{bl}^{i+1}\) is the
subblock \(\mathit{sbl}^i\) in state \(q_i\), as defined in Lemma 3
for block \(\mathit{bl}^{i+1}\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Definition}{12}{}
The origin of message \(m^{i+1}\) is the strong
message \(m^i\) in  \(\mathit{sbl}^i\) where:
\begin{enumerate}
\item
if in \(\pi_i\), \(v\) sends \(m^{i+1},\)
then \(m^i\) is the message that in response to its reception
\(v\) sent \(m^{i+1}\)\@; and
\item
otherwise, \(m^{i} = m^{i+1}\)\@.
\end{enumerate}
\end{alabsubtext}
%
\begin{alabsubtext}{Definition}{13}{}
The source block of block \(\mathit{bl}^{i+1}\) is block \(\mathit{bl}^{i}\),
whose suffix is the subsource of block \(\mathit{sbl}^{i}\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Observation}{5}{}
\label{obs:re2}
 \(Remainder(m^{i},\mathit{sbl}^i) = remainder(m^{i},\mathit{bl}^{i})\)\@.
\end{alabsubtext}
%
The observation follows from the fact that the
subsource block \(\mathit{sbl}^i\) is a suffix of the source block \(\mathit{bl}^i\)\@.
%
\begin{alabsubtext}{Observation}{6}{}
\label{obs:po2}
\(Potential(\mathit{bl}^{i+1}) \leq potential(\mathit{bl}^{i})\)\@.
\end{alabsubtext}
%
The observation derives from the following facts:
\begin{itemize}
\item \(potential(\mathit{sbl}^{i}) \leq potential(\mathit{bl}^{i})\)
since  \(\mathit{sbl}^i\) is the suffix of \(\mathit{bl}^i\); and
\item \(potential(\mathit{bl}^{i+1}) \leq potential(\mathit{sbl}^{i})\)
(by Corollary 4)\@.
\end{itemize}
%
\begin{alabsubtext}{Corollary}{5}{} \label{cor:4}
%
Let \(m^i\) be the origin of \(m^{i+1}\). Then there are three possible
values for \(remainder(m^{i+1},\mathit{bl}^{i+1})\)
as a function of \(remainder(m^{i},\mathit{bl}^{i})-1\):
%
\begin{enumerate}
\item \(remainder(m^{i+1},\mathit{bl}^{i+1}) = remainder(m^{i},\mathit{bl}^{i})-1\),
if in \(\pi_i\) message \(m^i\) was relayed
by a node and sent on the next link on the block;
\item \(remainder(m^{i+1},\mathit{bl}^{i+1}) = remainder(m^i,\mathit{bl}^i)+1\),
if in \(\pi_i\) block \(\mathit{bl}^i\), in which
message \(m^i\) resides, captures a node;
\item \(remainder(m^{i+1},\mathit{bl}^{i+1}) = remainder(m^i,\mathit{bl}^i)\),
which happens in either of the following two cases:
  \begin{itemize}
  \item
  The head of  \(\mathit{bl}^i\) is message \(m^i\), and in \(\pi_i\)
  message \(m^i\) captures a new node and \(m^{i+1}\) is
  relayed by the captured node\@.  In this  case, the remainder of
  the head message remains zero\@, and hence 
  \(remainder(m^{i+1},\mathit{bl}^{i+1}) = remainder(m^{i},\mathit{bl}^{i}) = 0\)\@.
  This case is considered to be the
  simultaneous occurrence of the first two possibilities\@.
  \item
  \(remainder(m^{i+1},\mathit{bl}^{i+1}) = remainder(m^{i},\mathit{bl}^{i})\) 
  if neither of the first two cases occurs. Then
  in \(\pi_i\) no new node is captured by \(\mathit{bl}^i\), and \(\pi_i\)
  does not affect \(m^i\)\@.
  \end{itemize}
\end{enumerate}
\end{alabsubtext}
%
Corollary~5 is based on Lemma~3 and Observation~5\@.
%
\begin{alabsubtext}{Definition}{14}{}
\label{deftb}
The progression of \(\mathit{bl}^w\)
from  state \(q_k\) to state \(q_w\), \(k \leq w\), is the series of blocks
\(\mathit{bl}^{k} \mathit{bl}^{k+1}  \dots  \mathit{bl}^{w}\)
at states  \(q_k q_{k+1} \dots q_w\), such that
for \(k \leq i \leq w\), \(\mathit{bl}^i\) is the source block
of \(\mathit{bl}^{i+1}\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Remark}{2}{}
Note that the progression of a block is defined backwards; i.e.,
\(\mathit{bl}^w\) is the first step, and
the source relationship between \(\mathit{bl}^i\) and \(\mathit{bl}^{i+1}\) continues
the definition from \(i+1\)  to \(i\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Definition}{15}{}
\label{deftm}
The strong message \(m^w\) traversal of block \(\mathit{bl}^w\)
from state \(q_k\) to state \(q_w\), \(k \leq w\), is the series of
strong messages \(m^k, m^{k+1} \dots m^w\) at states \(q_k, q_{k+1}
\dots q_w\), such that
for \(k \leq i \leq w\), \(m^i\)  is the origin of \(m^{i+1}\),
\(m^i \in \mathit{bl}^i\), and \(m^{i+1} \in \mathit{bl}^{i+1}\),
and \(\mathit{bl}^i\) is the source block of \(\mathit{bl}^{i+1}\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Remark}{3}{}
Note that as in the definition of block progression,
the message-traversal definition is also inductively
backwards; i.e., the basis of the induction is message
\(m^w\) and block \(\mathit{bl}^w\), and the
step of the induction is the origin relationship between \(m^i\) and
\(m^{i+1}\)\@.
\end{alabsubtext}
%
\apar{6.2-10}
Before we start the formal proof of Lemma 4,
we will state and prove a basic claim
that corresponds to the second bulleted point (at the end of the intuition paragraph
before Lemma 4)\@.
Let \(\mathrm{bl}^w\) be a block in state \(q^w\), and let
\(\mathrm{bl}^0\), \(\mathrm{bl}^1, \dots, \mathrm{bl}^w\) be the progression of  the block
from state \(q^0\) to \(q^w\)\@.
Let \(\{ \pi_{i_1}, \pi_{i_2}, \dots ,\pi_{i_k}\}\) be a maximal
series of operations such that for every \(j\),
a new node is captured by \(\mathrm{bl}^{i_j-1}\) in \(\pi_{i_j}\)\@.
%
\begin{alabsubtext}{Claim}{5}{}
\label{cla:3}
For every \(j\), \(0 \leq j \leq k-1\),
there exists an operation \(\pi_l\),
\(i_j < l < i_{j+1}\)
such that \(potential(bl^{l+1}) \leq potential(\mathit{bl}^{l})-1\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Claim}{5}{}
\prooffontshape
\apar{Proof of Claim 5-1}
Let \(v\) be the node that is captured by subsource block
\(\mathrm{bl}^{i_j}\) in operation \(\pi_{i_j}\)\@.  Let \(u\) be
the node captured by source block
\(\mathrm{bl}^{i_{j+1}}\) in operation \(\pi_{i_{j+1}}\)\@.
Node \(u\) is the outgoing neighbor of \(v\)\@.
This follows from the fact that
the series of \(\{ \pi_{i_1} \pi_{i_2} \dots \pi_{i_k}\}\)
is maximal, and from the definition of the progression
\(\mathrm{bl}^0,\mathrm{bl}^1 \dots \mathrm{bl}^w\)\@.
%
\apar{Proof of Claim 5-2}
The last message that \(v\) sends to
\(u\) before operation \(\pi_{i_j}\) is  \(m1\), such that
\(\mathsf{msg}(m1) = \) \(\mathsf{next}(zero_v,\mathsf{out\_port}_v(u))\) (by Claim 3)\@.
In operation \(\pi_{i_j}\), node \(v\) sends to \(u\) a strong message,
\(m2\), such that \(\mathsf{msg}(m2) = \) \(\mathsf{next}(\mathsf{selected}_v,\mathsf{out\_port}_v(u))\)
where \(m2 \in \mathrm{bl}^{i_j+1}\)  (case 5 of Lemma 3)\@.
Hence \(\mathsf{msg}(m2) \neq \mathsf{msg}(m1)\) (since \(\mathrm{bl}^{i_j}\) is a phony block)\@.
%
\apar{Proof of Claim 5-3}
Let \(\pi_l\) be
the operation in which \(u\) receives message \(m2\)\@.
To complete the proof we show that (1)
\(i_j < l < i_{j+1}\), and (2)
\(potential(\mathrm{bl}^{l+1}) \leq potential(\mathrm{bl}^{l})-1\)\@.
%
\begin{enumerate}
\item By the definition of \(\pi_l\),
clearly \(i_j < l\)\@.
Since \(u \notin \mathrm{bl}^l\), it is clear that \(l<j+1\)\@.
Assume to the contrary that \(u \in \mathrm{bl}^i\), then by Claim 1
\(\mathsf{selected}_u\) equals the body of the
last message received from \(v\)\@. Since \(m1\) is the last message
\(u\) received from \(v\), \(\mathsf{selected}_v =
next(zero_v,\mathsf{out\_port}_v(u))\)\@.
This contradicts the fact that \(\mathrm{bl}^l\) is a phony block\@.
%
\item Assume, to the contrary, that \(potential(\mathrm{bl}^{l+1})>
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}

