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