Stéphane Devismes
email: stephane.devismes@univ-grenoble-alpes.fr

David Ilcinkas
email: ilcinkas@labri.fr

Colette Johnen
email: johnen@labri.fr

Silent Self-Stabilizing Scheme for Spanning-Tree-like Constructions *

Keywords: distributed algorithms, self-stabilization, spanning tree, leader election, spanning forest

We propose a general scheme, called Algorithm STlC, to compute spanning-tree-like data structures on arbitrary networks. STlC is self-stabilizing and silent and, despite its generality, is also efficient. It is written in the locally shared memory model with composite atomicity assuming the distributed unfair daemon, the weakest scheduling assumption of the model. Its stabilization time is in O(nmaxCC) rounds, where nmaxCC is the maximum number of processes in a connected component. We also exhibit polynomial upper bounds on its stabilization time in steps and process moves holding for large classes of instantiations of Algorithm STlC. We illustrate the versatility of our approach by proposing several such instantiations that efficiently solve classical problems such as leader election, as well as, unconstrained and shortest-path spanning tree constructions.

Introduction

A self-stabilizing algorithm [START_REF] Edsger | Self-stabilizing Systems in Spite of Distributed Control[END_REF] is able to recover a correct behavior in finite time, regardless of the arbitrary initial configuration of the system, and therefore also after a finite number of transient faults, provided that those faults do not alter the code of the processes. Among the vast self-stabilizing literature, many works (see [START_REF] Felix | A survey of self-stabilizing spanning-tree construction algorithms[END_REF] for a survey) focus on spanning-tree-like constructions, i.e. constructions of specific distributed spanning tree -or forest-shaped data structures. Most of these constructions actually achieve an additional property called silence [START_REF] Dolev | Memory requirements for silent stabilization[END_REF]: a silent self-stabilizing algorithm converges within finite time to a configuration from which the values of the communication registers used by the algorithm remain fixed. Silence is a desirable property. Indeed, as noted in [START_REF] Dolev | Memory requirements for silent stabilization[END_REF], the silent property usually implies more simplicity in the algorithm design. Moreover, a silent algorithm may utilize less communication operations and communication bandwidth.

Self-stabilizing spanning-tree-like constructions are widely used as a basic building block of more complex self-stabilizing solutions. Indeed, composition is a natural way to design self-stabilizing algorithms [START_REF] Tel | Introduction to distributed algorithms[END_REF] since it allows to simplify both the design and proofs of self-stabilizing algorithms. Various composition techniques have been introduced so far, e.g., collateral composition [START_REF] Gouda | Adaptive programming[END_REF], fair composition [START_REF] Dolev | Self-stabilization[END_REF], cross-over composition [START_REF] Beauquier | Cross-over composition -enforcement of fairness under unfair adversary[END_REF], and conditional composition [START_REF] Kumar Datta | Self-stabilizing network orientation algorithms in arbitrary rooted networks[END_REF]; and many self-stabilizing algorithms are actually made as a composition of a silent spanning-tree-like construction and another algorithm designed for tree/forest topologies, e.g., [START_REF] Arora | Composite routing protocols[END_REF][START_REF] Blin | Loop-free super-stabilizing spanning tree construction[END_REF][START_REF] Kumar Datta | Competitive self-stabilizing k-clustering[END_REF]. Notably, the silence property is not mandatory in such designs, however it allows to write simpler proofs [START_REF] Kumar Datta | Selfstabilizing small k-dominating sets[END_REF]. Finally, notice that silent spanning-tree-like constructions have also been used to build very general results, e.g., the self-stabilizing proof-labeling scheme constructions proposed in [START_REF] Blin | On proof-labeling schemes versus silent self-stabilizing algorithms[END_REF].

We consider the locally shared memory model with composite atomicity introduced by Dijkstra [START_REF] Edsger | Self-stabilizing Systems in Spite of Distributed Control[END_REF], which is the most commonly used model in self-stabilization. In this model, executions proceed in (atomic) steps and the asynchrony of the system is captured by the notion of daemon. The weakest (i.e., the most general) daemon is the distributed unfair daemon. Hence, solutions stabilizing under such an assumption are highly desirable, because they work under any other daemon assumption. Moreover, the stabilization time can also be bounded in terms of steps (and moves, i.e., local state updates) only when the algorithm works under an unfair daemon. Otherwise (e.g., under a weakly fair daemon), time complexity may only be evaluated in terms of rounds, which capture the execution time according to the slowest process. In contrast, step complexity captures the execution time according to the fastest process. If the average speed of the different processes are roughly equal, then the execution time is of the order of magnitude of the round complexity. Otherwise, if the system is truly asynchronous, then the execution time is of the order of magnitude of the step complexity. The stabilization time in moves captures the amount of computations an algorithm needs to recover a correct behavior. Notice that the number of moves and the number of steps are closely related: if an execution e contains x steps, then the number y of moves in e satisfies x ≤ y ≤ n • x, where n is the number of processes. 1 Finally, if, for example, an algorithm is self-stabilizing under a weakly fair daemon, but not under an unfair one, then this means that the stabilization time in moves cannot be bounded, so there are processes whose moves do not make the system progress in the convergence. In other words, these processes waste computation power and so energy. Such a situation should therefore be prevented, making the unfair daemon more desirable than the weakly fair one.

There are many self-stabilizing algorithms proven under the distributed unfair daemon, e.g., [START_REF] Altisen | Self-stabilizing leader election in polynomial steps[END_REF][START_REF] Carrier | Selfstabilizing (f, g)-alliances with safe convergence[END_REF][START_REF] Ajoy | An o(n)-time self-stabilizing leader election algorithm[END_REF][START_REF] Kumar Datta | Self-stabilizing leader election in optimal space under an arbitrary scheduler[END_REF][START_REF] Glacet | Disconnected components detection and rooted shortest-path tree maintenance in networks[END_REF]. However, analyses of the stabilization time in steps (or moves) is rather unusual and this may be an important issue. Indeed, recently, several self-stabilizing algorithms which work under a distributed unfair daemon have been shown to have an exponential stabilization time in steps in the worst case. In [START_REF] Altisen | Self-stabilizing leader election in polynomial steps[END_REF], silent leader election algorithms from [START_REF] Ajoy | An o(n)-time self-stabilizing leader election algorithm[END_REF][START_REF] Kumar Datta | Self-stabilizing leader election in optimal space under an arbitrary scheduler[END_REF] are shown to be exponential in steps in the worst case. In [START_REF] Devismes | Silent self-stabilizing {BFS} tree algorithms revisited[END_REF], the Breadth-First Search (BFS) algorithm of Huang and Chen [START_REF] Huang | A self-stabilizing algorithm for constructing breadth-first trees[END_REF] is also shown to be exponential in steps. Finally, in [START_REF] Glacet | Disconnected components detection and rooted shortest-path tree maintenance in networks -extended version[END_REF] authors show that the silent self-stabilizing algorithm they proposed in [START_REF] Glacet | Disconnected components detection and rooted shortest-path tree maintenance in networks[END_REF] is also exponential in steps.

Contribution. In this paper, we propose a general scheme, called Algorithm STlC (stands for Spanning-Tree-like Constructions), to compute spanning-tree-like data structures on bidirectional weighted networks of arbitrary topology (n.b., the topologies are not necessarily connected). Algorithm STlC is selfstabilizing and silent. It is written in the locally shared memory model with composite atomicity, assuming the distributed unfair daemon.

Despite its versatility, Algorithm STlC is efficient. Indeed, its stabilization time is at most 4n maxCC rounds, where n maxCC is the maximum number of processes in a connected component. Moreover, its stabilization time in moves is polynomial in the usual cases (see the example instantiations we propose). Precisely, we exhibit polynomial upper bounds on its stabilization time in moves that depend on the particular problems we consider.

To illustrate the versatility of our approach, we propose several instantiations of STlC solving classical spanning-tree-like problems. Assuming the network is identified (i.e., processes have distinct IDs), we propose two instantiations of STlC, for electing a leader in each connected component and building a spanning tree rooted at each leader. In one version, stabilizing in O(n maxCC2 • n) moves, the trees are of arbitrary topology, while trees are BFS in the other, which stabilizes in O(n maxCC 3 • n) moves. The former move complexity matches the best known step complexity for leader election [START_REF] Altisen | Self-stabilizing leader election in polynomial steps[END_REF]. Assuming then an input set of roots, we also propose an instance to compute a spanning forest of arbitrary shaped trees, with non-rooted components detection. 2 This instance stabilizes in O(n maxCC • n) moves, which matches the best known step complexity for spanning tree construction [START_REF] Cournier | A new polynomial silent stabilizing spanning-tree construction algorithm[END_REF] with explicit parent pointers. 3 Finally, assuming a rooted network, we propose a shortest-path spanning tree and DFS construction, with nonrooted components detection. The shortest-path spanning tree construction stabilizes in O(n maxCC 3 •n•W max ) moves (W max is the maximum weight of an edge). Again, this move complexity matches the best known move complexity for this problem [START_REF] Devismes | Self-stabilizing disconnected components detection and rooted shortest-path tree maintenance in polynomial steps[END_REF]. From these various examples, one can easily derive other silent self-stabilizing spanning-tree-like constructions.

Related Work. This work is inspired by [START_REF] Devismes | Self-stabilizing disconnected components detection and rooted shortest-path tree maintenance in polynomial steps[END_REF]. That paper also considers the composite atomicity model with distributed unfair daemon, is efficient both in terms of rounds and moves, tolerates disconnections, but it is restricted to the case of the shortest-path tree with a single root. Generalizing this work to obtain a generic yet efficient self-stabilizing algorithm requires a fine tuning of the algorithm (presented in Section 3) and a careful rewriting of the proofs of correctness (presented in the remaining sections). In particular, almost all the concepts used to prove termination or complexities need to be redefined to suit the new, more general setting. Consequently their new properties and the corresponding proofs are mostly novel (although of a similar flavor).

Another closely related work is the one of Cobb and Huang [START_REF] Cobb | Stabilization of Maximal-Metric Routing without Knowledge of Network Size[END_REF]. In that paper, a generic self-stabilizing algorithm is presented for constructing in a rooted connected network a spanning tree where a given metric is maximized. Now, since the network is assumed to be rooted (i.e., a leader node is already known), leader election is not an instance of their generic algorithm. Similarly, since they assume connected networks, the non-rooted components detection cannot be expressed too. Finally, their algorithm is proven in the composite atomicity model but only for the restricted centralized weakly-fair daemon.

General schemes for arbitrary connected and identified networks have been proposed to transform almost any algorithm (specifically, those algorithms that can be self-stabilized) into their corresponding stabilizing version [START_REF] Katz | Self-stabilizing extensions for message-passing systems[END_REF][START_REF] Boldi | Universal dynamic synchronous self-stabilization[END_REF][START_REF] Cournier | The expressive power of snap-stabilization[END_REF][START_REF] Godard | Snap-Stabilizing Tasks in Anonymous Networks[END_REF]. Such universal transformers are, by essence, inefficient both in terms of space and time complexities: their purpose is only to demonstrate the feasibility of the transformation. In [START_REF] Katz | Self-stabilizing extensions for message-passing systems[END_REF] and [START_REF] Boldi | Universal dynamic synchronous self-stabilization[END_REF], authors consider self-stabilization in asynchronous message-passing systems and in the synchronous locally shared memory model, while expressiveness of snap-stabilization is studied in [START_REF] Cournier | The expressive power of snap-stabilization[END_REF][START_REF] Godard | Snap-Stabilizing Tasks in Anonymous Networks[END_REF] assuming the locally shared memory model with composite atomicity and a distributed unfair daemon.

In [START_REF] Ducourthial | Self-stabilization with r-operators[END_REF][START_REF] Delaët | Self-stabilization with r-operators revisited[END_REF], authors propose a method to design silent self-stabilizing algorithms for a class of fix-point problems (namely fix-point problems which can be expressed using r-operators). Their solution works in directed networks using bounded memory per process. In [START_REF] Ducourthial | Self-stabilization with r-operators[END_REF], they consider the locally shared memory model with composite atomicity assuming a distributed unfair daemon, while in [START_REF] Delaët | Self-stabilization with r-operators revisited[END_REF], they generalize their approach to asynchronous message-passing systems. In both papers, they establish a stabilization time in O(D) rounds, where D is the network diameter, that holds for the synchronous case only.

The remainder of the related work only concerns the locally shared memory model with composite atomicity assuming a distributed unfair daemon.

In [START_REF] Blin | On proof-labeling schemes versus silent self-stabilizing algorithms[END_REF], authors use the concept of labeling scheme introduced by Korman et al. [START_REF] Korman | Proof labeling schemes[END_REF] to design silent self-stabilizing algorithms with bounded memory per process. Using their approach, they show that every static task has a silent self-stabilizing algorithm which converges within a linear number of rounds in an arbitrary identified network. No step (nor move) complexity is given.

Efficient and general schemes for snap-stabilizing waves in arbitrary connected and rooted networks are tackled in [START_REF] Cournier | Light enabling snap-stabilization of fundamental protocols[END_REF]. Using this approach, one can obtain snap-stabilizing algorithms that execute each wave in a polynomial number of rounds and steps.

Few other works consider the design of particular spanning-tree-like constructions and their step complexity. Self-stabilizing algorithms that construct BFS trees in arbitrary connected and rooted networks are proposed in [START_REF] Cournier | Light enabling snap-stabilization of fundamental protocols[END_REF][START_REF] Cournier | The first fully polynomial stabilizing algorithm for BFS tree construction[END_REF]. The algorithm in [START_REF] Cournier | Light enabling snap-stabilization of fundamental protocols[END_REF] is not silent and has a stabilization time in O(∆ • n 3 ) steps (∆ is the maximum degree of the network)). The silent algorithm given in [START_REF] Cournier | The first fully polynomial stabilizing algorithm for BFS tree construction[END_REF] has a stabilization time O(D 2 ) rounds and O(n 6 ) steps. Silent self-stabilizing algorithms that construct spanning trees of arbitrary topologies in arbitrary connected and rooted networks are given in [START_REF] Cournier | A new polynomial silent stabilizing spanning-tree construction algorithm[END_REF][START_REF] Kosowski | A self-stabilizing algorithm for finding a spanning tree in a polynomial number of moves[END_REF]. The solution proposed in [START_REF] Cournier | A new polynomial silent stabilizing spanning-tree construction algorithm[END_REF] stabilizes in at most 4 • n rounds and 5 • n 2 steps, while the algorithm given in [START_REF] Kosowski | A self-stabilizing algorithm for finding a spanning tree in a polynomial number of moves[END_REF] stabilizes in n • D moves. However, its round complexity is not analyzed and the parent of a process is not computed explicitly. Now, Cournier [START_REF] Cournier | A lower bound for the M ax + 1 algorithm[END_REF] showed that the straightforward variant of this algorithm where a parent pointer variable is added has a stabilization time in Ω(n 2 • D) steps in an infinite class of networks.

Several other papers propose self-stabilizing algorithms stabilizing in both a polynomial number of rounds and a polynomial number of steps, e.g., [START_REF] Altisen | Self-stabilizing leader election in polynomial steps[END_REF] (for the leader election in arbitrary identified and connected networks), and [START_REF] Cournier | Snap-stabilizing depth-first search on arbitrary networks[END_REF][START_REF] Cournier | A snap-stabilizing dfs with a lower space requirement[END_REF] (for the DFS token circulation in arbitrary connected and rooted networks). The silent leader election algorithm proposed in [START_REF] Altisen | Self-stabilizing leader election in polynomial steps[END_REF] stabilizes in at most 3 • n + D rounds and O(n 3 ) steps. DFS token circulations given in [START_REF] Cournier | Snap-stabilizing depth-first search on arbitrary networks[END_REF][START_REF] Cournier | A snap-stabilizing dfs with a lower space requirement[END_REF] execute each wave in O(n) rounds and O(n 2 ) steps using O(n • log n) space per process for the former, and O(n 3 ) rounds and O(n 3 ) steps using O(log n) space per process for the latter. Note that in [START_REF] Cournier | Snap-stabilizing depth-first search on arbitrary networks[END_REF], processes are additionally assumed to be identified.

Roadmap. In the next section, we present the computational model and basic definitions. In Section 3, we describe Algorithm STlC. Its proof of correctness and a complexity analysis in moves are given in Section 4, whereas an analysis of the stabilization time in rounds is proposed in Section 5. Five instantiations of STlC with their specific complexity analyses are presented in Section 6. Finally, we make concluding remarks in Section 7.

Preliminaries

We consider distributed systems made of n ≥ 1 interconnected processes. Each process can directly communicate with a subset of other processes, called its neighbors. Communication is assumed to be bidirectional. Hence, the topology of the system can be represented as a simple undirected graph G = (V, E), where V is the set of processes and E the set of edges, representing communication links. Every (undirected) edge {u, v} actually consists of two arcs: (u, v) (i.e., the directed link from u to v) and (v, u) (i.e., the directed link from v to u). For every process u, we denote by V u the set of processes (including u) in the same connected component of G as u. In the following, V u is simply referred to as the connected component of u. We denote by n maxCC the maximum number of processes in a connected component of G. By definition, n maxCC ≤ n.

Every process u can distinguish its neighbors using a local labeling of a given datatype Lbl. All labels of u's neighbors are stored into the set Γ (u). Moreover, we assume that each process u can identify its local label α u (v) in the set Γ (v) of each neighbor v. Such labeling is called indirect naming in the literature [START_REF] Sloman | Distributed systems and computer networks[END_REF]. When it is clear from the context, we use, by an abuse of notation, u to designate both the process u itself, and its local labels (i.e., we simply use

u instead of α u (v) for v ∈ Γ (u)). Let δ u = |Γ (u)| be the degree of process u. The maximal degree of G is ∆ = max u∈V δ u .
We use the composite atomicity model of computation [START_REF] Edsger | Self-stabilizing Systems in Spite of Distributed Control[END_REF][START_REF] Dolev | Self-stabilization[END_REF] in which the processes communicate using a finite number of locally shared registers, called variables. Each process can read its own variables and those of its neighbors, but can write only to its own variables. The state of a process is defined by the values of its local variables. A configuration of the system is a vector consisting of the states of each process.

A distributed algorithm consists of one local program per process. The program of each process consists of a finite set of rules of the form label : guard → action. Labels are only used to identify rules in the reasoning. A guard is a Boolean predicate involving the state of the process and that of its neighbors. The action part of a rule updates the state of the process. A rule can be executed only if its guard evaluates to true; in this case, the rule is said to be enabled. A process is said to be enabled if at least one of its rules is enabled. We denote by Enabled(γ) the subset of processes that are enabled in configuration γ.

When the configuration is γ and Enabled(γ) = ∅, a non-empty set X ⊆ Enabled(γ) is selected by the so-called daemon; then every process of X atomically executes one of its enabled rules, leading to a new configuration γ . The transition from γ to γ is called a step. We also say that each process of X performs a move or an action during γ to γ . The possible steps induce a binary relation over C, denoted by →. An execution is a maximal sequence of configurations e = γ 0 γ

1 • • • γ i • • • such that γ i-1 → γ i for all i > 0.
The term "maximal" means that the execution is either infinite, or ends at a terminal configuration in which no rule is enabled at any process.

Each step from a configuration to another is driven by a daemon. We define a daemon as a predicate over executions. We say that an execution e is an execution under the daemon S if S(e) holds. In this paper we assume that the daemon is distributed and unfair. "Distributed" means that while the configuration is not terminal, the daemon should select at least one enabled process, maybe more. "Unfair" means that there is no fairness constraint, i.e., the daemon might never select an enabled process unless it is the only enabled process. In other words, the distributed unfair daemon corresponds to the predicate true, i.e., this is the most general daemon.

In the composite atomicity model, an algorithm is silent if all its possible executions are finite. Hence, we can define silent self-stabilization as follows.

Definition 1 (Silent Self-Stabilization). Let L be a non-empty subset of configurations, called the set of legitimate configurations. A distributed system is silent and self-stabilizing under the daemon S for L if and only if the following two conditions hold:

all executions under S are finite, and all terminal configurations belong to L.

We use the notion of round [START_REF] Dolev | Self-stabilization of dynamic systems assuming only Read/Write atomicity[END_REF] to measure the time complexity. The definition of round uses the concept of neutralization: a process v is neutralized during a step γ i → γ i+1 , if v is enabled in γ i but not in configuration γ i+1 , and it is not activated in the step γ i → γ i+1 . Then, the rounds are inductively defined as follows. The first round of an execution e = γ 0 γ 1 • • • is the minimal prefix e = γ 0 • • • γ j , such that every process that is enabled in γ 0 either executes a rule or is neutralized during a step of e . Let e be the suffix γ j γ j+1 • • • of e. The second round of e is the first round of e , and so on.

The stabilization time of a silent self-stabilizing algorithm is the maximum time, in moves, steps or rounds, over every execution possible under the considered daemon S (starting from any initial configuration) to reach a terminal (legitimate) configuration.

Algorithm STlC

The problem

We propose a general silent self-stabilizing algorithm, called STlC (see Algorithm 1 for its formal code), which aims at converging to a terminal configuration where a specified spanning forest (maybe a single spanning tree) is (distributedly) defined. To that goal, each process u has two input constants. canBeRoot u : a boolean value, which is true if u is allowed to be root of a tree. In this case, u is called a candidate. In a terminal configuration, every tree root satisfies canBeRoot, but the converse is not necessarily true. Moreover, for every connected component GC, if there is at least one candidate u ∈ GC, then at least one process of GC should be a tree root in a terminal configuration. In contrast, if there is no candidate in a connected component, we require that all processes of the component converge to a particular terminal state, expressing the local detection of the absence of candidates. pname u : the name of u. pname u ∈ IDs, where IDs = N∪{⊥} is totally ordered by < and min < (IDs) = ⊥. The value of pname u is problem dependent. Actually, we consider here two particular cases of naming. In one case, ∀v ∈ V, pname v = ⊥. In the other case, ∀u, v ∈ V, pname u = ⊥ ∧ (u = v ⇒ pname u = pname v ), i.e., pname u is a unique global identifier.

Then, according to the specific problem we consider, we may want to minimize the weight of the trees using some kind of distance. To that goal, we assume that each edge {u, v} has two weights: ω u (v) denotes the weight of the arc (u, v) and ω v (u) denotes the weight of the arc (v, u). Both values belong to the domain DistSet. Let (DistSet, ⊕, ≺) be an ordered magma, i.e., ⊕ is a closed binary operation on DistSet and ≺ is a total order on this set. The definition of (DistSet, ⊕, ≺) is problem dependent and, if necessary, i.e., if the problem dependent predicate P _nodeImp(.) holds (P _nodeImp(v) is true if process v is required to act to minimize the weight of the tree), the weight of the trees will be minimized using the ordered magma and the distance values that each candidate u should take when it is the root of a tree. This latter value is given by the (problem dependent) function distRoot(u).

We assume that, for every edge {u, v} of E and for every value

d of DistSet, we have d ≺ d ⊕ ω u (v) and d ≺ d ⊕ ω v (u).
Besides, for every d1 and d2 in DistSet, and for every integer i ≥ 0, we define d1 ⊕ (i • d2) as follows:

-d1 ⊕ (0 • d2) = d1 -d1 ⊕ (i • d2) = (d1 ⊕ ((i -1) • d2) ⊕ d2 if i > 0.

The variables

In STlC, each process u maintains the following three variables. st u ∈ {I, C, EB, EF }: this variable gives the status of the process. I, C, EB, and EF respectively stand for Isolated, Correct, Error Broadcast, and Error Feedback. The two first status, I and C, are involved in the normal behavior of the algorithm, while the two last ones, EB and EF , are used during the correction mechanism. The meaning of EB and EF will be further detailed in Subsection 3.4. In a terminal configuration, if V u contains a candidate, then st u = C, otherwise st u = I. parent u ∈ {⊥} ∪ Lbl: In a terminal configuration, if V u contains a candidate, then either parent u = ⊥, i.e., u is a tree root, or parent u belongs to Γ (u), i.e., parent u designates a neighbor of u, referred to as its parent. Otherwise (V u does not contain a candidate), the value of parent u is meaningless. d u ∈ DistSet: In a terminal configuration, if V u contains a candidate, then d u is larger than or equal to the weight of the tree path from u to its tree root, otherwise the value of d u is meaningless.

Typical Execution

Assume the system starts from a configuration where, for every process u, st u = I. All processes that belong to a connected component containing no candidates are disabled forever. Focus now on a connected component GC where at least one process is candidate. Then, any process u of status I that is a candidate or a neighbor of a process of status C is enabled to execute rule R R : it eventually executes R R (u) to initiate a tree or to join a tree rooted at some candidate, choosing among the different possibilities the one that minimizes its distance value. Using this rule, it also switches its status to C and sets

d u to distRoot(u), or d v ⊕ ω u (v) if it chooses a parent v.
Executions of rule R R are asynchronously propagated in GC until all processes of GC have status C. In parallel, rules R U are executed to reduce the weight of the trees, if necessary: when a process u with status C satisfies P _nodeImp(u), this means that u can reduce d u by selecting another neighbor with status C as parent and this reduction is required by the specification of the problem to be solved (P _nodeImp(u) is problem dependent). In this case, u chooses the neighbor which allows to minimize the value of d u . In particular, notice that a candidate can lose its tree root condition using this rule, if it finds a sufficiently good parent in its neighborhood. Hence, eventually the system reaches a terminal configuration, where a specific spanning forest (maybe a single spanning tree) is defined (in a distributed manner) in connected components containing at least one candidate, while in other components all processes are isolated.

Error Correction

Assume now that the system is in an arbitrary configuration. Inconsistencies between the states of the processes are detected using predicate P _abnormalRoot. We call abnormal root any process u satisfying P _abnormalRoot(u). Informally (see Subsection 4.1, page 7, for the formal definition), a process u is an abnormal root if u is neither a normal root (i.e., ¬P _root(u), see Definition 2), nor isolated (i.e. st u = I), and satisfies one of the following three conditions:

1. its parent pointer does not designate a neighbor, 2. its distance d u is inconsistent with the distance of its parent, or 3. its status is inconsistent with the status of its parent.

Every process u that is neither an abnormal root nor isolated satisfies one of the two following cases.

Either u is a normal root, i.e., P _root(u), or u points to some neighbor (i.e., parent u ∈ Γ (u)) and the state of u is coherent w.r.t. the state of its parent. In this latter case, u ∈ Children(parent u ), i.e., u is a "real" child of its parent (see Subsection 4.1 for the formal definition). Consider a path P = u 0 , . . . , u k such that ∀i, 0 ≤ i < k, u i+1 ∈ Children(u i ). P is acyclic. If u 0 is either a normal or an abnormal root, then P is called a branch rooted at u 0 . Let u be a root (either normal or abnormal). We define the tree T (u) as the set of all processes that belong to a branch rooted at u. If u is a normal root, then T (u) is said to be a normal tree, otherwise u is an abnormal root and T (u) is said to be an abnormal tree.

We call any configuration without abnormal trees a normal configuration. So, to recover a normal configuration, it is necessary to remove all abnormal trees. For each abnormal tree T , we have two cases. If the abnormal root u of T can join another tree T using rule R U (u) (thus without increasing its distance value, since, in this case, P _nodeImp(u) holds), then it does so and T disappears by becoming a subtree of T . Otherwise, T is entirely removed in a top-down manner, starting from its abnormal root u. Now, in that case, we have to prevent the following situation: u leaves T ; this removal creates some abnormal trees, each of those being rooted at a previous child of u; and later u joins one of those (created) trees or a tree issued from them. (This issue is sometimes referred to as the count-to-infinity problem [START_REF] Leon | Communication Networks[END_REF].) Hence, the idea is to freeze T , before removing it. By freezing we mean assigning each member of the tree to a particular state, here EF , so that (1) no member v of the tree is allowed to execute R U (v), and (2) no process w can join the tree by executing R R (w) or R U (w). Once frozen, the tree can be safely deleted from its root to its leaves.

The freezing mechanism (inspired from [START_REF] Blin | An improved snap-stabilizing PIF algorithm[END_REF]) is achieved using the status EB and EF , and the rules R EB and R EF . If a process is not involved into any freezing operation, then its status is I or C. Otherwise, it has status EB or EF and no neighbor can select it as its parent. These two latter status are actually used to perform a "Propagation of Information with Feedback" [START_REF] Ernest | Echo Algorithms: Depth Parallel Operations on General Graphs[END_REF][START_REF] Segall | Distributed Network Protocols[END_REF] in the abnormal trees. This is why status EB means "Error Broadcast" and EF means "Error Feedback". From an abnormal root, the status EB is broadcast down in the tree using rule R EB . Then, once the EB wave reaches a leaf, the leaf initiates a convergecast EF -wave using rule R EF . Once the EF -wave reaches the abnormal root, the tree is said to be dead, meaning that all processes in the tree have status EF and, consequently, no other process can join it. So, the tree can be safely deleted from its abnormal root toward its leaves. There are several possibilities for the deletion depending on whether or not the process u to be deleted is a candidate or has a neighbor with status C. If u is a candidate and has no neighbor with status C: u becomes a normal root by executing beRoot(u) using the rule R R (u). If u has a neighbor with status C, again the rule R R (u) is executed: u tries to directly join another "alive" tree, however if u is candidate and becoming a normal root allows it to further minimize d u , it executes beRoot(u) to become a normal root. If u is not a candidate and has no neighbor with status C, the rule R I (u) is executed: u becomes isolated, and might join another tree later.

Let u be a process belonging to an abnormal tree of which it is not the root. Let v be its parent. From the previous explanation, it follows that during the correction, (st v , st u ) ∈ {(C, C), (EB, C), (EB, EB), (EB, EF ), (EF, EF )} until v resets by R R (v) or R I (v). Now, due to the arbitrary initialization, the status of u and v may not be coherent, in this case u is an abnormal root. Precisely, as formally defined in Algorithm 1, the status of u is incoherent w.r.t. the status of its parent v if st u = st v and st v = EB. For example, if a process u belongs to a tree (i.e., st u = I) and designates an isolated node v with parent u (i.e., parent u = v and st v = I), then the status of u is incoherent w.r.t. its parent v, i.e., u is actually an abnormal root.

Actually, the freezing mechanism ensures that if a process is the root of an alive abnormal tree, it is in that situation since the initial configuration (see Lemma 5, page 10). The bounded move complexity mainly relies on this strong property.

Correctness and Move Complexity of STlC

Definitions

Before proceeding with the proof of correctness and the move complexity analysis, we define some useful concepts and give some of their properties.

Root, Child, and Branch. Definition 2 (Normal and Abnormal Roots). Every process u that satisfies P _root(u) is said to be a normal root.

Every process u that satisfies P _abnormalRoot(u) is said to be an abnormal root.

Definition 3 (Alive Abnormal Root).

A process u is said to be an alive abnormal root (resp. a dead abnormal root) if u is an abnormal root and has a status different from EF (resp. has status EF ).

Definition 4 (Children).

For every process v, for every process u ∈ Children(v), u is said to be a child of v. Conversely, v is said to be the parent of u.

Observation 1 A process u is either a normal root, an isolated process (i.e. st u = I), an abnormal root, or a child of its parent (i.e., member of the set Children(v), where v = parent u ).

Predicates • P _root(u) ≡ canBeRootu ∧ stu = C ∧ parentu = ⊥ ∧ du = distRoot(u) • P _abnormalRoot(u) ≡ ¬P _root(u) ∧ stu = I ∧ [parentu / ∈ Γ (u) ∨ du ≺ dparent u ⊕ ωu(parentu)∨ (stu = stparent u ∧ stparent u = EB)] • P _reset(u) ≡ stu = EF ∧ P _abnormalRoot(u) • P _updateN ode(u) ≡ (∃v ∈ Γ (u) | stv = C ∧ dv ⊕ ωu(v) ≺ du) • P _updateRoot(u) ≡ canBeRootu ∧ distRoot(u) ≺ du • P _nodeImp(u)
(P _reset(u) ∨ stu = I)∧ → computeP ath(u); [canBeRootu ∨ (∃v ∈ Γ (u) | stv = C)]
Definition 5 (Branch). A branch is a sequence of processes v 0 , . . . , v k , for some integer k ≥ 0, such that v 0 is a normal or an abnormal root and, for every 0 ≤ i < k, we have v i+1 ∈ Children(v i ). The process v i is said to be at depth i and v i , . . . , v k is called a sub-branch. If v 0 is an abnormal root, the branch is said to be illegal, otherwise, the branch is said to be legal.

Observation 2 A branch depth is at most n maxCC -1. A process v having status I does not belong to any branch. If a process v has status C (resp. EF ), then all processes of a sub-branch starting at v have status C (resp. EF ).

One of the key properties allowing us to prove that STlC has a polynomial move complexity is the following result.

Legitimate Configurations. Definition 6 (Legitimate State).

A process u is said to be in a legitimate state of STlC if u satisfies one of the following conditions:

1. P _root(u), and ¬P _nodeImp(u), 2. there is a process satisfying

canBeRoot in V u , st u = C, parent u ∈ Γ (u), d u d parentu ⊕ω u (parent u ),
and ¬P _nodeImp(u), or 3. there is no process satisfying canBeRoot in V u and st u = I.

Definition 7 (Legitimate Configuration).

A legitimate configuration of STlC is a configuration where every process is in a legitimate state.

We will eventually prove that the terminal configurations are exactly the legitimate configurations. We first prove one of the two inclusions.

Lemma 1. Any legitimate configuration of STlC is terminal.

Proof. Let γ be a legitimate configuration of STlC and u be a process.

Assume first that there is no process of V u that satisfies canBeRoot in γ. Then, by definition of γ, every process v in V u satisfies st v = I. Hence, since ¬canBeRoot v ∧ st v = I for every process v in V u , no rule of STlC is enabled at any process of V u in γ.

Assume then that there is a process that satisfies canBeRoot in γ. Then, every process v ∈ V u satisfies (1) P _root(v) and ¬P _nodeImp(v), or [START_REF] Felix | A survey of self-stabilizing spanning-tree construction algorithms[END_REF]

st v = C, parent v ∈ Γ (v), d v d parentv ⊕ ω v (parent v ),

and ¬P _nodeImp(v). This in particular means that st

v = C, for every v ∈ V u . Hence, R EF (v), R I (v), and R R (v) are all disabled at every v ∈ V u in γ. ¬P _nodeImp(v) implies that R U (v) is disabled at every v ∈ V u . Finally, st v = C ∧ [P _root(v) ∨ (parent v ∈ Γ (v) ∧ d v d parentv ⊕ ω v (parent v ))] for every v ∈ V u implies ¬P _abnormalRoot(v) ∧ st parentv = EB for every v ∈ V u and so R EB (v) is disabled at every v ∈ V u in γ.
Hence, no rule of STlC is enabled at any process of V u in γ.

Partial Correctness

The following technical lemmas will help us to prove that any terminal configuration of STlC is legitimate.

Lemma 2. In any terminal configuration of STlC, every process has status I or C.

Proof. Assume that there exists some process that has status EB. Consider a process u with status EB having the largest distance value d u . Note that no process v that has status C can be a child of u, otherwise R U (v) or R EB (v) would be enabled. Therefore, process u has only children having the status EF . Thus R EF (u) is enabled, a contradiction.

Assume now that there exists some process that has status EF . Consider a process u with status EF having the smallest distance value d u . As no process has status EB (see the previous case), u is an abnormal root, and has the status EF . So, either R I (u) or R R (u) is enabled, a contradiction. Lemma 3. Let γ be a terminal configuration of STlC. Let u be a process such that V u contains at least one process satisfying canBeRoot in γ. In γ, u satisfies:

st u = C, -¬P _nodeImp(u), and

-P _root(u) or parent u ∈ Γ (u) ∧ d u d parentu ⊕ w u (parent u ).
Proof. Let v be a process of V u such that canBeRoot v in γ. We have st v / ∈ {EB, EF }, by Lemma 2, and also st v = I, because otherwise R R (v) would be enabled in γ. Therefore st v = C.

Assume then that there exists some process of V u that has status I in γ. Consider now a process w of V u such that w has status I and at least one of its neighbors has status C in γ (such a process exists because no process has status EB or EF in γ, by Lemma 2, whereas at least one process, e.g., v, of V u has status C). Then, R R (w) is enabled in γ, a contradiction. So, every process of V u (including u) has status C in γ.

Since st u = C in γ, ¬P _nodeImp(u) holds in γ (otherwise, R U (u) would be enabled).

In γ, u satisfies ¬P _abnormalRoot(u) because, otherwise, either R U (u) or R EB (u) would be enabled, as st u = C in γ. We can thus conclude by Observation 1 that u satisfies P _root(u) or

parent u ∈ Γ (u) ∧ d u d parentu ⊕ w u (parent u ) in γ.
In a connected component containing no candidates, all processes are isolated. Otherwise, the process u having the smallest distance d u (which would exist by Lemma 2) would be an abnormal root and thus would be enabled. Therefore, by Lemma 3, we obtain the following result.

Theorem 1. Any terminal configuration of STlC is legitimate.

In the remainder of Section 4, we establish some properties on every execution of STlC under a distributed unfair daemon. These properties allow us to show the termination under a distributed unfair daemon and exhibit an upper bound on the move complexity of any instance of STlC.

GC-segments

Let GC be a connected component of G and let γ be a configuration. Let SL(γ, GC) be the set of processes u ∈ GC such that, in γ, u is an alive abnormal root, or P _updateRoot(u) ∧ st u = C holds. We now prove that this set can never gain a new element. Lemma 4. Let γ → γ be a step where a process u executes the rule R U or R R . Then u is not an alive abnormal root in γ .

Proof. If parent u = ⊥ in γ , then u must have executed beRoot(u) in γ → γ . So P _root(u) is true in γ , which, in turn, implies ¬P _abnormalRoot(u).

Assume now that parent u = v in γ . Then st v = C in γ (because it is a requirement to execute R U or R R when beRoot(u) is not executed in γ → γ ). Consequently, the only rules that v may execute in γ → γ are R U or R EB . During γ → γ , v either takes the status EB, decreases its distance value, or does not change the value of its variables. In any case, u belongs to Children(v) in γ , which prevents u from being an alive abnormal root in γ .

Lemma 5. No alive abnormal root is created along any execution of STlC.

Proof. Let γ → γ be a step. Let u be a process that is not an alive abnormal root in γ. If the status of u is EF or I in γ , then u is not an alive abnormal root in γ . If u executes R U or R R during this step, then u is not an alive abnormal root in γ either, by Lemma 4. So the only rule that u may execute is R EB in γ → γ . Furthermore, both in γ and γ , u has status C or EB.

Assume first that parent u = ⊥ in γ . Then, parent u = ⊥ already holds in γ. We thus have P _root(u) in γ because ¬P _abnormalRoot(u) in γ. Consequently, u executes no move in γ → γ , and u is still a normal root in γ .

Assume now that parent u = v in γ . Whether u executes R EB or not, parent u is also v in γ. Also, ¬P _abnormalRoot(u) in γ implies that u ∈ Children(v) and st v ∈ {C, EB} in γ, further implying that the only rules that v may execute in γ → γ are R U or R EB . We conclude that, in any case, u still belongs to Children(v) in γ , which prevents u from being an alive abnormal root in γ . Lemma 6. If a process u satisfies P _updateRoot(u) ∧ st u = C, then it does so from the beginning of the execution.

Proof. Let u be a process satisfying P _updateRoot(u) ∧ st u = C. Note that the property does only depend on the local state on u. Moreover, this state must be the initial state, because any rule fixing st u to C also sets d u to a value not larger than distRoot u . This concludes the proof.

By the two preceding Lemmas, we obtain the following result. Let us now prove some properties on the moves made by a process in a GC-segment.

Lemma 7.

Let GC be a connected component of G and u be any process of GC. Let seg be a GCsegment. During seg, if u executes the rule R EF , then u does not execute any other rule in the remaining of seg.

Proof. Let γ 1 → γ 2 be a step of seg in which u executes R EF . Let γ 3 → γ 4 be the next step in which u executes a rule. (If one of these two steps does not exist, then the lemma trivially holds.)

Let v be the root (at depth 0) of any branch in γ 1 containing u. By Definition 4, v must have status EB, and must therefore be an alive abnormal root. This implies that v ∈ SL(γ 1 , GC). Note that we may have v = u. On the other hand, in γ 3 , u is the dead abnormal root of all branches it belongs to since st u = EF in γ 3 and u necessarily executes R I or R R in this step. This implies that v must have executed the rule R EF in the meantime: there is a step γ 5 → γ 6 , with γ 5 between γ 1 (included) and γ 3 (excluded) where v executes R EF . Since st v = EF in γ 6 , we have v / ∈ SL(γ 6 , GC). Therefore, the steps γ 1 → γ 2 , and γ 3 → γ 4 belong to two distinct GC-segments of the execution, by Corollary 1 and Definition 8. By Lemma 7,we obtain the following result.

Corollary 2.

Let GC be a connected component of G and u be any process of GC. The sequence of rules executed by u during a GC-segment belongs to the following language:

(R I + ε)(R R + ε)(R U ) * (R EB + ε)(R EF + ε) .
By Observation 3 and Corollary 2, we obtain the following result.

Theorem 2. If the number of R U executions by any process of GC in any GC-segment is bounded by nb_U N , then the total number of moves in any execution is bounded by

(nb_U N + 4) • (n maxCC + 1) • n.

Causal chains

We now use the notion of causal chain defined below to further analyze the number of moves and steps in a GC-segment.

Definition 9 (Causal Chain).

Let GC be a connected component of G. Let v 0 be a process of GC and seg be any GC-segment. A causal chain of seg rooted at v 0 is a non-empty sequence of actions a 1 , a 2 , . . . , a k executed in seg such that the action a 1 sets parent v1 to v 0 and for all 2 ≤ i ≤ k, the action a i sets parent vi to v i-1 after the action a i-1 but not later than v i-1 's next action.

Observation 4

Let GC be a connected component of G, v 0 be a process of GC, and seg be any GCsegment. Let a 1 , a 2 , . . . , a k be a causal chain of seg rooted at v 0 . Denote by v i the process that executes a i , for all i ∈ {1, . . . , k}.

-For all 1 ≤ i ≤ k, a i consists in the execution of computeP ath(v i ) (i.e., v i executes the rule R U or R R ), where v i is a process of GC. -Assume a 1 is executed in the step γ → γ of seg. Denote by ds 0 the distance value of process v 0 in γ, called the initiating value of the causal chain. For all

1 ≤ i ≤ k, a i sets d vi to ((ds 0 ⊕ w v1 (v 0 )) ⊕ • • • ) ⊕ w vi (v i-1 ).
Lemma 8. Let GC be a connected component of G. Let seg be a segment of GC.

-All actions in a causal chain of seg are executed by different processes of GC.

-Moreover, an execution of computeP ath(v) by some process v never belongs to any causal chain rooted at v.

Proof. First, by definition, all actions executed in a causal chain of seg are executed by processes in GC.

Then, note that any rule R U executed by a process v makes the value of d v decrease. Assume now, by contradiction, that there exists a process v such that, in some causal chain a 1 , a 2 , . . . , a k of seg, v is designated as parent in some action a i executed in step γ i → γ i+1 and executes the action a j in step γ j → γ j+1 , with j > i. v has status C in γ i , and the value of d v is strictly larger in γ j+1 than in γ i (Observation 4). So v must execute R EF between γ i+1 and γ j . Consequently, actions a i and a j are executed in two different segments (Lemma 7), a contradiction.

Therefore, all actions in a causal chain are caused by different processes, and a process never executes an action in a causal chain it is the root of.

Maximal Causal chains. Definition 10 (Maximal causal chain).

Let GC be a connected component of G. Let v 0 be a process of GC and let seg be any GC-segment.

A maximal causal chain of seg rooted at v 0 is a causal chain a 1 , a 2 , . . . , a k executed in seg such that the causal chain is maximal and, either v 0 is a normal root or the action a 1 sets parent v1 to v 0 not later than any action by v 0 in seg.

The following lemma adds an additional property to Observation 4 for the specific case of maximal causal chains. Lemma 9. Given any connected component GC, any GC-segment seg, and any process v ∈ GC, all maximal causal chains of seg rooted at v have the same initiating value.

Proof. For the purpose of contradiction, assume that there exist such GC, seg and v such that two maximal causal chains of seg rooted at v have different initiating values d 1 and d 2 . At least one of them, say d 1 , must be different from distRoot v . This value d 1 is necessarily the distance value of v at the beginning of seg, otherwise v would not be the root of the corresponding maximal causal chain. As a consequence, we must have

d 2 = distRoot v .
Since d 1 is the distance value of v at the beginning of seg, there must exist an action a executing beRoot(u) in seg. By Corollary 2, the action a is an execution of R U in the case when P _updateRoot(v)∧ st v = C holds. By definition of a GC-segment, the action a is thus executed during the last step of seg and thus no maximal causal chains of seg (which are never empty by definition) can be rooted at v with initiating value d 2 = distRoot v . This contradiction concludes the proof.

Definition 11 (SI seg,v ).

Let GC be a connected component of G. Let v be a process of GC and let seg be a segment of GC.

We define SI seg,v as the set of all the distance values obtained after executing an action belonging to the maximal causal chains of seg rooted at v. Lemma 10. Let GC be a connected component of G. Let v 0 be a process of GC and let seg be a segment of GC. The size of the set SI seg,v0 is bounded by n maxCC !.

Proof. Let us consider a distance value d obtained after executing an action a i belonging to a maximal causal chain a 1 , a 2 , . . . , a k of seg rooted at v 0 . Denote by v i the process that executes a i , for all i ∈ {1, . . . , k}. By Observation 4, we have d = ((ds

0 ⊕ w v1 (v 0 )) ⊕ • • • ) ⊕ w vi (v i-1
), with ds 0 being the initiating value common to all maximal causal chains of seg rooted at v 0 . Differently speaking, the value d is fully determined by the sequence of processes v 1 , . . . , v i (v 0 and seg being fixed). Moreover, note that all the v j , 0 ≤ j ≤ i are different processes, by Lemma 8. Therefore, |SI seg,v0 | is bounded by n maxCC !.

Move complexity of STlC

Lemma 11. Let GC be a connected component of G, u ∈ GC, and seg be a GC-segment. If the size of SI seg,v is bounded by X for any process v ∈ GC, then the number of R U moves done by u in seg is bounded by X • (n maxCC -1) + 1.

Proof. First, assume that R U (u) is executed in some step γ → γ of seg and later in some other step γ → γ of seg. By Corollary 2, any sequence of R U (u) executions in seg makes the value of d u decrease. Therefore, all the values of d u obtained by the R U executions done by u are different. By definitions 10 and 11, all these values belong to the set v∈GC\{u} SI seg,v ∪ {distRoot(u)}, which has size at most X • (n maxCC -1) + 1.

By Theorem 2 and Lemma 11, we obtain the following result.

Corollary 3.

If the size of SI seg,v is bounded by X for any connected component GC, any process v ∈ GC, and any GC-segment seg, then the total number of moves during any execution, is bounded by

(X • (n maxCC -1) + 5) • (n maxCC + 1) • n.
Combined with Lemma 10, this corollary already allows us to prove that STlC always terminates and has a bounded move complexity. Corollary 4. Algorithm STlC is silent self-stabilizing under the distributed unfair daemon and has a bounded move (and step) complexity.

Let W max = max{w u (v) : u ∈ V ∧ v ∈ Γ (u)}.
If all weights are strictly positive integers and ⊕ is the addition operator, then the size of any SI seg,u is bounded by W max (n maxCC -1) for all connected component GC, all GC-segment seg and all process u ∈ GC because S seg,u ⊆ [ds seg,u + 1, ds seg,u + W max (n cc -1)], where n cc ≤ n maxCC is the number of processes in GC, and ds seg,u is the common (by Lemma 9) initiating value of the maximal causal chains of seg rooted at u. Hence, we deduce the following theorem from Lemma 1, Theorem 1, and Corollary 3. We first introduce the notion of normal configurations, which will help us to partition the proof on the round complexity of STlC.

Definition 12 (Normal Process).

A process u is said to be normal if u satisfies the following two conditions:

1. st u / ∈ {EB, EF }, 2. ¬P _abnormalRoot(u).

Definition 13 (Normal Configuration).

Let γ be a configuration of STlC. γ is said to be normal if every process is normal in γ; otherwise γ is said to be abnormal.

Observation 5

In a normal configuration of STlC, only the rules R U or R R may be enabled on any process.

We first prove that, once a normal configuration is reached, all subsequent configurations will be normal as well.

Lemma 13. Any step from a normal configuration of STlC reaches a normal configuration of STlC.

Proof. Let γ → γ be a step such that γ is a normal configuration and let u be a process.

In γ, every process v satisfies st v / ∈ {EB, EF } and ¬P _abnormalRoot(v). Hence, both R EB (u) and R EF (u) are disabled in γ, and consequently st u / ∈ {EB, EF } still holds in γ . Moreover, since u is not an alive abnormal root in γ, Lemma 5 implies that u is not an alive abnormal root in γ either. Since st u = EF in γ , we obtain ¬P _abnormalRoot(u) in γ .

From an Arbitrary Configuration to a Normal Configuration

The first lemma below essentially claims that all processes that are in illegal branches progressively switch to status EB within n maxCC rounds, in order of increasing depth (Definition 5, page 9). Lemma 14. Let i ∈ N. From the beginning of round i+1, there does not exist any process both in state C and at depth less than i in an illegal branch.

Proof. We prove this lemma by induction on i. The base case (i = 0) is vacuum, so we assume that the lemma holds for some integer i ≥ 0.

From the beginning of round i + 1, no process can ever choose a parent which is at depth smaller than i in an illegal branch because those processes (if they exist) will never have status C, by induction hypothesis.

Then, let u be a process of status C in an illegal branch at the beginning of round i + 1. Its depth is thus at least i. By induction hypothesis, each of its ancestor at depth smaller than i has status EB and has at least one child not having status EF . Thus, no such ancestors can execute any rule, and consequently they cannot make the depth of u decreasing to i or smaller. Therefore, no process can take state C at depth smaller or equal to i in an illegal branch from the beginning of round i + 1.

Consider any process u with status C at depth i in an illegal branch at the beginning of the round i+1. By induction hypothesis, u is an abnormal root, or the parent of u is not in state C (i.e., it is in the state EB). During round i + 1, u will execute rule either R EB or R U and thus either switch to state EB, or join another branch at a depth greater than i, or become a normal root turning its branch to be legal. This concludes the proof of the lemma. Corollary 6. After at most n maxCC rounds, the system is in a configuration from which no process in any illegal branch has status C forever.

Moreover, once such a configuration is reached, each time a process executes a rule other than R EF , this process is outside any illegal branch forever.

The next lemma essentially claims that once no process in an illegal branch has status C forever, processes in illegal branches progressively switch to status EF within at most n maxCC rounds, in order of decreasing depth. Lemma 15. Let i ∈ N * . From the beginning of round n maxCC +i, any process at depth larger than n maxCC -i in an illegal branch has status EF .

Proof. We prove this lemma by induction on i. The base case (i = 1) is vacuum (by Observation 2, page 9), so we assume that the lemma holds for some integer i ≥ 1. At the beginning of round n maxCC + i, any process at depth larger than n maxCC -i has the status EF (by induction hypothesis). Therefore, processes with status EB at depth n maxCC -i in an illegal branch can execute the rule R EF at the beginning of round n maxCC + i. These processes will thus all execute within round n maxCC + i (they cannot be neutralized as no children can connect to them) and obtain status EF . We conclude the proof by noticing that, from Corollary 6, once round n maxCC has terminated, any process in an illegal branch that executes some rule either gets status EF , or will be outside any illegal branch forever.

The next lemma essentially claims that after the propagation of status EF in illegal branches, the maximum length of illegal branches progressively decreases until all illegal branches vanish. Lemma 16. Let i ∈ N * . From the beginning of round 2n maxCC + i, there does not exist any process at depth larger than n maxCC -i in an illegal branch.

Proof. We prove this lemma by induction on i. The base case (i = 1) is vacuum (by Observation 2), so we assume that the lemma holds for some integer i ≥ 1. By induction hypothesis, at the beginning of round 2n maxCC + i, no process is at depth larger than n maxCC -i in an illegal branch. All processes in an illegal branch have the status EF (by Lemma 15). So, at the beginning of round 2n maxCC +i, any abnormal root satisfies the predicate P _reset, and is enabled to execute either R I , or R R . So, all abnormal roots at the beginning of the round 2n maxCC + i are no more in an illegal branch at the end of this round: the maximal depth of the illegal branches has decreased, since by Corollary 6, no process can join an illegal tree during the round 2n maxCC + i.

By Lemmas 14-16, we obtain the following result. Theorem 4. After at most 3n maxCC rounds, a normal configuration of STlC is reached.

From a Normal Configuration to a Terminal Configuration

From a normal configuration, Algorithm STlC needs additional rounds to propagate the status C and the correct distances in the components of the graph containing at least one candidate. First, we observe the following fact.

Observation 6

In a normal configuration of STlC, all processes in connected components containing no process satisfying canBeRoot are in state I and thus are disabled.

Let u be a process having the status C in a normal configuration γ. Along any execution from γ, the distance of u cannot increase and u keeps the status C.

From the previous observation, we only need to focus on any connected component GC containing at least one process satisfying canBeRoot.

Let us fix an arbitrary execution ex of STlC in GC starting from a normal configuration γ. By Corollary 4 (page 13), a terminal configuration is eventually reached after a finite number of steps along ex. Lemma 17. Let ST GC (i, ex) be the set of processes defines by {u ∈ GC | u performs a move along ex after the beginning of the round i}.

If |ST GC (i, ex)| > 0 then |ST GC (i + 1, ex)| < |ST GC (i, ex)|.
Proof. By definition, ST GC (i + 1, ex) ⊆ ST GC (i, ex). It is thus sufficient to prove that at least one process of ST GC (i, ex) is enabled at the start of the i-th round and will do its last action during the ith round of ex.

Let γ i be the configuration at the start of round i of ex, and let γ f be the terminal configuration of ex. Let us consider the process u ∈ ST GC (i, ex) having the minimum distance d u in γ f , denoted by dmin(i). Along ex from γ i , any process w of ST GC (i, ex) satisfies dmin(i) d w or st w = I according to the definition of u and to Observation 6.

Case 1. In γ

f , parent u = ⊥.
This means that P _root(u) holds in γ f . This further implies that, along ex from γ i , the last action of u consists in executing beRoot(u). At that time, u satisfies P _updateRoot(u) ∨ st u = I. In fact, this must hold already from γ i , by Lemma 6, page 11) and Observation 6. To summarize, u performs only one action along ex from γ i , and u is enabled in γ i and stays enabled until u does an action. This action is thus done during the ith round of ex, and u ∈ ST GC (i + 1, ex), concluding the case. Case 2. In γ f , parent u = w.

By Observation 6, notice that along ex from γ i , the value min (v∈Γ (u) ∧ stv=C) (d v ⊕ ω u (v)) remains constant, and equal to dmin(i). Therefore, once u is disable, it stays disable according to P _nodeImp(u) properties (Algorithm 1, page 8). So u is enabled in γ i and stays enabled until u does an action. Therefore, this action is done during the i-th round of ex. After this action of u, we have ¬P _updateN ode(u) ∧ ¬P _updateRoot(u) ∧ st u = C (so u is disabled forever). Thus u ∈ ST GC (i + 1, ex), concluding the case.

From the previous lemma, Lemma 13 and Theorem 4, we obtain the following result.

Corollary 7.

A terminal legitimate configuration of any instantiation of STlC is reached in at most 4n maxCC rounds from any configuration.

Instantiations

In this section, we illustrate the versatility of Algorithm STlC by proposing several instantiations that solve various classical problems. Following the general bound (Corollary 7, page 16), all these instances reach a terminal configuration in at most 4n maxCC rounds, starting from an arbitrary one.

Spanning Forest and Non-Rooted Components Detection

Given an input set of processes rootSet, Algorithm Forest is the instantiation of STlC with the parameters given in Algorithm 2. Algorithm Forest computes (in a self-stabilizing manner) a spanning forest in each connected component of G containing at least one process of rootSet. The forest consists of trees (of arbitrary topology) rooted at each process of rootSet. Moreover, in any component containing no process of rootSet, the processes eventually detect the absence of root by taking the status I (Isolated).

Correctness of Forest. By Theorem 1, and Corollary 4 (resp. page 10, 13), Algorithm Forest self-stabilizes to a terminal legitimate configuration that satisfies the following requirements (see Definition 7, page 9).

Observation 7

In a terminal legitimate configuration of Forest, each process u satisfies one of the following conditions:

1. P _root(u), i.e., u is a tree-root and u ∈ rootSet, 2. there is a process of rootSet in V u , st u = C, parent u ∈ Γ (u), d u ≥ d parentu +1, and ¬P _nodeImp(u), i.e., u / ∈ rootSet belongs to a tree rooted at some process of rootSet and its neighbor parent u is its parent in the tree, 3. there is no process of rootSet in V u and st u = I, i.e., u is isolated.

Move Complexity of Forest. Since for every process u, P _nodeImp(u) ≡ P _updateRoot(u), rule R U is enabled at most once. Hence, the total number of moves (and steps) during any execution is bounded by 5 • (n maxCC + 1) • n, by Theorem 2 (page 11).

• DistSet = N • i1 ⊕ i2 = i1 + i2 • i1 ≺ i2 ≡ (i1 < i2)
• distRoot(u) = 0

Predicate

• P _nodeImp(u) ≡ P _updateRoot(u)

Leader Election

Assuming the network is identified, Algorithm LEM is the instantiation of STlC with the parameters given in Algorithm 3. In each connected component, Algorithm LEM elects the process u (i.e., P _leader(u) holds) of smallest identifier and builds a tree (of arbitrary topology) rooted at u that spans the whole connected component. Correctness of LEM. As canBeRoot is true for all processes, we can deduce, from Theorem 1 (page 10) and Definition 7 (page 9), that in a terminal configuration, st u = C for every process u. So, from Lemma 1 (page 9), Algorithm LEM self-stabilizes to a terminal legitimate configuration that satisfies the following requirements.

Observation 8

In a terminal legitimate configuration of LEM, each process u satisfies one of the following conditions: (1) P _root(u), or [START_REF] Felix | A survey of self-stabilizing spanning-tree construction algorithms[END_REF]

st u = C, parent u ∈ Γ (u), d u d parentu .
Correctness of LEM is proven by the following lemma.

Conclusion

We proposed a general scheme, Algorithm STlC, to compute spanning-tree-like data structures on arbitrary (not necessarily connected) bidirectional networks. Algorithm STlC is self-stabilizing and silent. It is written in the locally shared memory model with composite atomicity. We proved its correctness under the distributed unfair daemon hypothesis, the weakest scheduling assumption of the model. We also showed that its stabilization time is at most 4n maxCC rounds, where n maxCC is the maximum number of processes in a connected component. We illustrated the versatility of our approach by proposing several instantiations of STlC that solve various classical problems. In most of the cases, we exhibited polynomial upper bounds on its stabilization time in steps and process moves for the considered instantiation. For example, assuming the network is identified, we proposed two instances of STlC for electing a leader in each connected component and building a spanning tree rooted at each leader in a polynomial number of steps (resp. moves). In the first version, the trees are of arbitrary topology, while trees are BFS in the second. Using our scheme, one can easily derive other instances to obtain shortest-path trees for example. Assuming now an input set of roots, we also proposed an instance to compute in a polynomial number of steps (resp. moves) a spanning forest of arbitrary shaped trees, with non-rooted components detection. Again, one can easily enforce this latter construction to obtain BFS or shortest-path forests. Finally, assuming a rooted network, we proposed to compute in a polynomial number of steps (resp. moves) a shortest-path spanning tree construction, with non-rooted components detection. Again, BFS or arbitrary tree constructions can be easily derived from these latter instances. Notice that, for many of these latter problems, there was, until now, no solution in the literature where a polynomial step complexity upper bound was proven.

  is problem dependent. However, if P _nodeImp(u), then P _updateN ode(u) ∨ P _updateRoot(u); if P _updateRoot(u), then P _nodeImp(u); P _nodeImp(u) only depends on the values of stu, du, P _updateRoot(u), and min (v∈Γ (u) ∧ stv =C) (dv ⊕ ωu(v)).Macros•Children(u) = {v ∈ Γ (u) | stv = I ∧ parentv = u ∧ dv du ⊕ ωv(u) ∧ (stv = stu ∨ stu = EB)} • beRoot(u): stu := C; parentu := ⊥; du := distRoot(u); • computeP ath(u): if {v ∈ Γ (u) | stv = C} = ∅ then stu := C; parentu := argmin (v∈Γ (u) | stv =C) (dv ⊕ ωu(v)); du := dparent u ⊕ ωu(parentu); if P _updateRoot(u) then beRoot(u); else beRoot(u); end if Rules RU(u): stu = C ∧ P _nodeImp(u) → computeP ath(u); REB(u): stu = C ∧ ¬P _nodeImp(u)∧ → stu := EB; (P _abnormalRoot(u) ∨ stparent u = EB) REF(u): stu = EB ∧ (∀v ∈ Children(u) | stv = EF ) → stu := EF ; RI(u): P _reset(u) ∧ ¬canBeRootu ∧ (∀v ∈ Γ (u) | stv = C) → stu := I; RR(u):

Corollary 1 .

 1 For every step γ → γ , SL(γ , GC) ⊆ SL(γ, GC).Based on Corollary 1, we can use the notion of GC-segment defined below to bound the total number of moves in an execution.Definition 8 (GC-Segment). Let e = γ 0 γ 1 • • • be an execution of STlC. Let GC be a connected component of G. If there is no step γ i → γ i+1 in e such that |SL(γ i , GC)| > |SL(γ i+1 , GC)|, then the first GC-segment of e is e itselfand there is no other GC-segment. Otherwise, let γ i → γ i+1 be the first step of e such that |SL(γ i , GC)| > |SL(γ i+1 , GC)|. The first GC-segment of e is the prefix γ 0 • • • γ i+1 . The second GC-segment of e is the first GC-segment of the suffix γ i+1 γ i+2 • • • , and so forth. By Corollary 1, we have Observation 3 Let GC be a connected component of G. For every execution e of STlC, e contains at most n maxCC + 1 GC-segments, because |SL(γ i , GC)| ≤ n maxCC by definition.

Theorem 3 .Lemma 12 .Corollary 5 .

 3125 Algorithm STlC is silent self-stabilizing under the distributed unfair daemon and, when all weights are strictly positive integers and ⊕ is the addition operator, its stabilization time in moves (and steps) is at most(W max • (n maxCC -1) 2 + 5) • (n maxCC + 1) • n. Let GC be a connected component of G, v ∈ GC,and seg be GC-segment. If all edges have the same weight, then |SI seg,v | < n maxCC . Proof. Assume that all edges have the same weight w. According to Observation 4 and Lemma 8, we have SI seg,v ⊂ {ds seg,v ⊕ i.w | 1 ≤ i ≤ n maxCC -1}, with ds seg,v being the common (by Lemma 9) initiating value of the maximal causal chains of seg rooted at v. By Corollary 3 and Lemma 12, we obtain the following result. If all edges have the same weight, then the total number of moves (and steps) during any execution, is bounded by ((n maxCC -1) 2 + 4) • (n maxCC + 1) • n.

Algorithm 2 :

 2 Parameters for any process u in Algorithm ForestInputs • canBeRootu is true if and only if u ∈ rootSet • pnameu is ⊥ • ωu(v) = 1 for every v ∈ Γ (u) Ordered Magma

Algorithm 3 :

 3 Parameters for any process u in Algorithm LEMInputs• canBeRootu is true for any process• pnameu is the identifier of u (n.b., pnameu ∈ N)• ωu(v) = (⊥, 1) for every v ∈ Γ (u) Ordered Magma • DistSet = IDs × N; for every d = (a, b) ∈ DistSet, we let d.id = a and d.h = b • (id1, i1) ⊕ (id2, i2) = (id1, i1 + i2). • (id1, i1) ≺ (id2, i2) ≡ (id1 < id2) ∨ [(id1 = id2) ∧ (i1 < i2)] • distRoot(u) = (pnameu, 0) Predicates • P _nodeImp(u) ≡ ((∃v ∈ Γ (u) | stv = C ∧ dv.id < du.id)) ∨ P _updateRoot(u)• P _leader(u) ≡ P _root(u)

Algorithm 1 :

 1 Algorithm STlC, code for any process u

	Inputs
	• canBeRootu: a boolean value; it is true if u can be a root
	• pnameu: name of u
	Variables
	• stu ∈ {I, C, EB, EF }: the status of u
	• parentu ∈ {⊥} ∪ Lbl
	• du: the distance value associated to u

Actually, in this paper as in most of the literature, bounds on step complexity are established by proving upper bounds on the number of moves.

By non-rooted components detection, we mean that every process in a connected component that does not contain the root should eventually take a special state notifying that it detects the absence of a root.

Actually, there exists a solution with implicit parent pointer[START_REF] Kosowski | A self-stabilizing algorithm for finding a spanning tree in a polynomial number of moves[END_REF] that achieves a better complexity, O(n • D) moves, where D is the network diameter. However adding a parent pointer to this algorithm makes this solution more costly than ours in a large class of networks, as we will explain later.

This study has been partially supported by the anr projects Descartes (ANR-16-CE40-0023) and Estate (ANR-16-CE25-0009). This study has been carried out in the frame of "the Investments for the future" Programme IdEx Bordeauxcpu (ANR-10-IDEX-03-02).

Lemma 18. In a terminal legitimate configuration of Algorithm LEM, each process u satisfies one of the following conditions:

1. P _root(u) (≡ P _leader(u)) and u is the process of smallest identifier in V u , or 2. st u = C, parent u ∈ Γ (u), d u d parentu , and d u = (pname , -) where is the process of smallest identifier in V u .

Proof. First, from the previous observation, in a terminal configuration st u = C, for every process u. Then, consider any connected component GC. Assume, by the contradiction, that in a terminal configuration of LEM, we have two processes u, v ∈ GC such that d u .id = d v .id. Without the loss of generality, assume that u and v are neighbors and d u .id > d v .id. Then, P _nodeImp(u) holds, and since st u = st v = C, R U (u) is enabled, a contradiction. Hence, all processes of GC agree on the same leader identifier, and by definition of P _root(u), at most one process u can satisfy P _root(u), i.e., P _leader(u).

Assume, then, by the contradiction, that no process of GC that satisfies P _root in the terminal configuration. Let u ∈ GC such that d u is minimum in the terminal configuration. By Observation 8, parent u ∈ Γ (u) and d parentu ≺ d u , contradicting the minimality of d u . Hence, there is exactly one process in GC satisfying P _root( ) (≡ P _leader( )) in any terminal configuration. Moreover, by Observation 8, in a terminal configuration, parent variables describe a spanning tree rooted at .

Finally, assume, by the contradiction, that in a terminal configuration, the leader of GC is not the process of smallest identifier in GC. Let u be the process of smallest identifier in GC. Then, distRoot(u) = (pname u , 0) ≺ d u = (pname , x), with x ∈ N, i.e., P _updateRoot(u). Since

Move Complexity of LEM. During a GC-segment, a process can only execute R U to improve its ID. Since there are n maxCC initial values and n maxCC real IDs in its connected component, the total number of moves (and steps) during any execution is bounded by (2n maxCC + 4) • (n maxCC + 1) • n (Theorem 2, page 11) i.e., O(n maxCC 2 • n).

Shortest-Path Tree and Non-Rooted Components Detection

Assuming the existence of a unique root r and (strictly) positive integer weights for each edge, Algorithm RSP is the instantiation of STlC with the parameters given in Algorithm 4. Algorithm RSP computes (in a self-stabilizing manner) a shortest-path tree spanning the connected component of G containing r. Moreover, in any other component, the processes eventually detect the absence of r by taking the status I (Isolated).

Recall that the weight of a path is the sum of its edge weights. The weighted distance between the processes u and v, denoted by d(u, v), is the minimum weight of a path from u to v. A shortest path from u to v is then a path whose weight is d(u, v). A shortest-path (spanning) tree rooted at r is a tree rooted at r that spans V r and such that, for every process u, the unique path from u to r in T is a shortest path from u to r in V r .

Correctness of RSP.

It is given by the following lemma. • n • W max ).

Leader Election and Breadth-First Search Tree

Assuming the network is identified, Algorithm LEM_BFS is the instantiation of STlC with the parameters given in Algorithm 5. In each connected component, Algorithm LEM_BFS elects the process u (i.e., P _leader(u) holds) of smallest identifier and builds a breadth-first search (BFS) tree rooted at u that spans the whole connected component.

Recall that the weight of a path is the sum of its edge weights (in this case, each edge as weight 1). The weighted distance between the processes u and v, denoted by d(u, v), is the minimum weight of a path from u to v. A shortest path from u to v is then a path whose weight is d(u, v). When all edges have weight 1, a BFS spanning tree rooted at u is a shortest-path (spanning) tree rooted at process u that spans V u .

Predicates

• P _nodeImp(u) ≡ P _updateN ode(u) ∨ P _updateRoot(u)

Correctness of LEM_BFS. Following the same reasoning as for Algorithm LEM and P _nodeImp(u) definition. Algorithm LEM_BFS self-stabilizes to a terminal legitimate configuration that satisfies the following requirements.

Observation 10

In a terminal legitimate configuration of Algorithm LEM_BFS, each process u satisfies one of the following conditions:

1. P _root(u) (≡ P _leader(u)) and u is the process of smallest identifier in V u , or 2. [START_REF] Edsger | Self-stabilizing Systems in Spite of Distributed Control[END_REF], where is the process of smallest identifier in V u .

Move Complexity of LEM_BFS. All edges have the same weight, so the total number of moves (and steps) during any execution is bounded by ((n maxCC -1) 2 + 5) • (n maxCC + 1) • n (Corollary 5, page 13), i.e., O(n maxCC 3 • n).

Depth-First Search Tree and Non-Rooted Components Detection

Assume the existence of a unique root r. Algorithm RDFS is the instantiation of STlC with the parameters given in Algorithm 6. Algorithm RDFS computes (in a self-stabilizing manner) a depth-first search (DFS) tree spanning the connected component of G containing r. Moreover, in any other component, processes eventually detect the absence of r by taking the status I (Isolated).

Here, the weight of the arc (u, v) is α u (v), the local label of u in Γ (v). Let P = u k , u k-1 , . . . u 0 = r be a (directed) path from process u k to the root r. We define the weight of P as the sequence 0, α 1 (u 0 ), α 2 (u 1 ), . . . , α k (u k-1 ). The lexicographical distance from process u to the root r, denoted by d r lex (u), is the minimum weight of a path from u to r (according to the lexicographical order).

Correctness of RDFS.

Observation 11 Let T be a tree rooted at r that spans V r . Following the result of [START_REF] Collin | Self-stabilizing depth-first search[END_REF], if for every process u ∈ V r , the weight of the path from u to r in T is equal to d r lex (u), then T is a (first) DFS spanning tree of V r .

Following the same reasoning as for Algorithm RSP, we know that Algorithm RDFS self-stabilizes to a terminal legitimate configuration that satisfies the following requirements. Move Complexity of RDFS. For this instance, we cannot apply Theorem 3 (page 13) to obtain a polynomial move complexity. However, by Lemma 10 we have a rough estimation of the move complexity, i.e., at most n maxCC ! moves. We outline that this estimation is coarse-grained, and so can be further refined.