Alain Cournier
email: alain.cournier@u-picardie.fr

Stephane Rovedakis
email: stephane.rovedakis@cnam.fr

Vincent Villain
email: vincent.villain@u-picardie.fr

An improved stabilizing BFS tree construction *

Keywords: Distributed algorithm, Fault-tolerance, Self-stabilization, Spanning tree construction

The construction of a spanning tree is a fundamental task in distributed systems which allows to resolve other tasks (i.e., routing, mutual exclusion, network reset). In this paper, we are interested in the problem of constructing a Breadth First Search (BFS) tree. Stabilization is a versatile technique which ensures that the system recover a correct behaviour from an arbitrary global state resulting from transient faults. A silent algorithm always reaches a terminal global state in a finite time.

We present a first silent stabilizing algorithm to resolve a problem in which each node requests a permission (delivered by a subset of network nodes) in order to perform a defined computation. Using this first algorithm, we present a silent stabilizing algorithm constructing a BFS tree working in O(D 2 ) rounds (D is the diameter of the network) under a distributed daemon without any fairness assumptions. The complexity in terms of steps is O(mn 4 ) where m and n are the number of edges and nodes of the network, respectively, so it is polynomial with respect to n. To our knowledge, since in general the diameter of a network is much smaller than the number of nodes, this algorithm gets the best compromise of the literature between the complexities in terms of rounds and in terms of steps.

Introduction

The construction of spanning trees is a fundamental problem in the field of distributed systems. A spanning tree is a virtual structure which contains no cycle and interconnects all the nodes of a network. In distributed systems, the construction of a spanning tree is commonly used to design algorithms resolving other distributed tasks, like routing, token circulation or message broadcasting in a network. Spanning trees are also used to obtain algorithms resolving a particular distributed problem with a better time complexity compared to algorithms for the same problem which do not use this structure. There are many different spanning tree construction problems guaranteeing various properties, e.g., the construction of a depth first search (DFS) tree, a spanning tree of minimum weight or a spanning tree of minimum diameter. A crucial class of spanning trees is the construction of a Breadth First Search (BFS) tree, which contains shortest paths (in hops) from every node to the root of the tree. This structure is mainly used in networks to quickly broadcast information from a source node. When a cost is associated to communication links, this problem is known as the construction of a Shortest Path tree.

Self-stabilization introduced first by Dijkstra in [START_REF] Edsger | Self-stabilizing systems in spite of distributed control[END_REF] and later publicized by several books [START_REF] Dolev | Self-Stabilization[END_REF][START_REF] Tel | Introduction to distributed algorithm[END_REF] is one of the most versatile techniques to handle transient faults arising in distributed systems. A distributed algorithm is self-stabilizing if starting from any arbitrary global state (due to faults or attacks)

Programs. In our model, protocols are semi-uniform, i.e., each processor executes the same program except r. We consider the local shared memory model of computation which is an abstraction of the message-passing model. In this model, the program of every processor consists in a set of shared variables (henceforth, referred to as variables) and an ordered finite set of actions inducing a priority. This priority follows the order of appearance of the actions into the text of the protocol. A processor can write to its own variable only, and read its own variables and that of its neighbors. Each action is constituted as follows: < label > :: < guard > → < statement > . The guard of an action in the program of p is a boolean expression involving variables of p and its neighbors. The statement of an action of p updates one or more variables of p. An action can be executed only if its guard is satisfied. The state of a processor is defined by the value of its variables. The state of a system is the product of the states of all processors. We will refer to the state of a processor and the system as a (local) state and (global) configuration, respectively. We note C the set of all possible configuration of the system. Let γ ∈ C and A an action of p (p ∈ V ). A is said enabled at p in γ if and only if the guard of A is satisfied by p in γ. Processor p is said to be enabled in γ if and only if at least one action is enabled at p in γ. When several actions are enabled simultaneously at a processor p: only the priority enabled action can be activated.

Let a distributed protocol P be a collection of binary transition relations denoted by →, on C. A computation of a protocol P is a maximal sequence of configurations e = (γ 0 ,γ 1 ,...,γ i ,γ i+1 ,...) such that, ∀i ≥ 0, γ i → γ i+1 (called a step) if γ i+1 exists, else γ i is a terminal configuration. Maximality means that the sequence is either finite (and no action of P is enabled in the terminal configuration) or infinite. All computations considered here are assumed to be maximal. E is the set of all possible computations of P .

As we already said, each execution is decomposed into steps. Each step is shared into three sequential phases atomically executed: (i) every processor evaluates its guards, (ii) a daemon (also called scheduler) chooses some enabled processors, (iii) each chosen processor executes its priority enabled action. When the three phases are done, the next step begins.

A daemon can be defined in terms of fairness and distributivity. In this paper, we use the notion of weakly fairness: if a daemon is weakly fair, then every continuously enabled processor is eventually chosen by the daemon to execute an action. We also use the notion of unfairness: the unfair daemon can forever prevent a processor to execute an action except if it is the only enabled processor. Concerning the distributivity, we assume that the daemon is distributed meaning that, at each step, if one or more processors are enabled, then the daemon chooses at least one of these processors to execute an action.

We consider that any processor p executed a disabling action in the computation step γ i → γ i+1 if p was enabled in γ i and not enabled in γ i+1 , but did not execute any protocol action in γ i → γ i+1 . The disabling action represents the following situation: at least one neighbor of p changes its state in γ i → γ i+1 , and this change effectively made the guard of all actions of p false in γ i+1 .

To compute the time complexity, we use the definition of round. This definition captures the execution rate of the slowest processor in any computation. Given a computation e (e ∈ E), the first round of e (let us call it e ′ ) is the minimal prefix of e containing the execution of one action (an action of the protocol or a disabling action) of every enabled processor from the initial configuration. Let e ′′ be the suffix of e such that e = e ′ e ′′ . The second round of e is the first round of e ′′ , and so on.

Question-Answer problem

In this section, we first present the Question-Answer problem, then a snap-stabilizing algorithm is given to resolve this problem.

Let a static forest F of trees in a network G = (V, E). Let some processors which request a permission to make a defined computation and a set of processors AP ⊂ V authorized to deliver permissions. We consider a local predicate Allowed(p) which indicates if processor p is in AP or not. Each processor p ∈ AP is a root of a tree T ∈ F, i.e., we have Allowed(p) ⇒ root(T ). Given a processor p in a tree T ∈ F which requests a permission, the Question-Answer problem is to deliver a permission (or acknowledgement) to p if and only if there is a processor q ∈ AP such that q is the root of T .

We give a formal specification for the Question-Answer problem defined above.

Specification 1 (Question-Answer) Let G = (V, E) be a network and F the static forest of trees in G.

Let a tree T ∈ F and root(T ) the root of T . T is an allowed tree if root(T ) ∈ AP and not allowed otherwise. A protocol P which resolves the Question-Answer problem satisfies:

[Liveness 1] During an infinite computation, if a processor has to send infinitely often a request and it cannot send its request in an allowed tree, then there exist an infinite number of requests which were sent.

[Liveness 2] For every computation suffix, if a processor in an allowed tree has sent a request at time t, then there exist at least one processor in the same tree which receives an acknowledgement to its own sent request at time t ′ > t.

[Safety 1] Every processor which has sent a request receives at most one acknowledgement causally related to its sent request.

[Safety 2] Every processor in a not allowed tree which has sent a request never receives an acknowledgement.

Remark that only semi-algorithms can satisfy Specification 1, that is no acknowledgement is sent to processors in a not allowed tree, from Property [Safety 2] of Specification 1.

Question-Answer algorithm

In this section, we present a snap-stabilizing algorithm for the Question-Answer problem, a formal description is given by Algorithm 1. This is a non-uniform algorithm because some rules are only executed by one or several processors p ∈ V satisfying Predicate Allowed(p).

Given a forest F of trees and a set of processors Q ∈ V which request a permission. A priority is associated to each request when permission is requested at any processor p ∈ V . Algorithm 1 must transmit the request of each processor p ∈ Q to the root root(T ) of the tree T ∈ F whose p belongs to. If processor root(T ) satisfies Allowed(root(T )) then an acknowledgement must be delivered to one of these p with the highest priority at least. This is to inform p that it is authorized to make a defined computation. By using correctly the priority at processors, we can ensure with this algorithm that eventually each processor determines if it belongs to a tree T rooted at a processor root(T ) which satisfies Predicate Allowed(root(T )). (Algorithm 2 given in Section 4 illustrate how to use Algorithm 1 to obtain this property.)

Variables

We define below the different variables used by Algorithm 1.

Shared variable.

Each processor p ∈ V has a local shared variable p.Req which allows an external algorithm, called Algorithm A, to monitor the Question-Answer algorithm at p. This shared variable can take four values: ASK, W AIT, REP, and OU T . By setting the shared variable p.Req to ASK in Algorithm A, p requests a permission through the Question-Answer algorithm to its root of the tree. To this end, Question-Answer algorithm tries to send a request to the root of the tree and sets the shared variable p.Req to W AIT . At least the request of a requesting processor with the highest priority will reach the root of the tree and then receive a permission (an acknowledgement). When a processor p receives an acknowledgement, it sets the shared variable p.Req to REP . Finally, Algorithm A must set the variable p.Req to OU T to request another permission through Question-Answer algorithm to the root of the tree.

Local variables. Each processor p ∈ V maintains two local variables:

• p.Q: it defines the status of the Question-Answer algorithm at processor p. There are three distinct status: R, W, and A. Status R notifies that p transmits a request to the root of the tree, whereas Status W indicates that p waits for an acknowledgement from the root for the transmitted request. The third status, Status A, indicates that p has received an acknowledgement from the root.

• p.P Q: it stores the priority associated to the request sent or transmitted by processor p.

Algorithm description

Each processor p ∈ V takes different inputs in Algorithm 1: N eig p gives the set of neighbors of p in the network, Child(p) defines the set of children of p in the tree it belongs to, P arent(p) is the parent of p

≡ p.Q = A ∧ (∀q ∈ Child(p) :: q.Q = W ⇒ q.P Q = p.P Q) Retransmit(p) ≡ p.Q = W ∧ (∃q ∈ Child(p) :: q.Q = R ∧ q.P Q = p.P Q) Error(p) ≡ p.Q = A ∧ [(p.Req ∈ {ASK, W AIT } ∧ p.P Q = P riority(p)) ∨(p.P Q = P riority(p) ∧ (p.Req = REP ⇒ (∀q ∈ Child(p) :: q.P Q = p.P Q ⇒ q.Q = A)))] Request(p) ≡ p.Req = ASK ∧ (|P rioRC(p)| > 0 ⇒ P riority(p) ≥ (Chp).P Q) RequestT (p) ≡ p.Req = REP ∧ |P rioRC(p)| > 0 ∧ [((Chp).P Q ≤ p.P Q ⇒ T ransmit(p)) ∨ Retransmit(p

Algorithm for p such that Allowed(p):

Predicates: Any processor p ∈ V in an allowed tree T ∈ F is informed that a permission is needed at p using the shared variable p.Req setted to ASK by an external algorithm at p. In this case, we say that p has a local request to send to the root of the tree it belongs to. Before to send such a local request, p must verify if it has a child sending a request (|P rioRC(p)| > 0) with a higher priority than its local request, i.e., P riority(p) ≥ (Ch p ).P Q with Ch p the child of p sending the request with highest priority among p's children (see Predicate Request(p)). If this is not the case, p executes QR-action to set variables p.Req, p.Q, and p.P Q to W AIT, R, and to P riority(p) respectively to send its local request to the root. Moreover, the external algorithm is informed that the request is sent since p.Req = W AIT .

W aitR(p) ≡ p.Q = R ∧ (∀q ∈ Child(p) :: q.P Q = p.P Q ⇒ q.Q = W ) AnswerR(p) ≡ p.Q = W
Predicates: W ait(p) ≡ P arent(p).Q = R ∧ p.Q = R ∧ P arent(p).P Q = p.P Q ∧(∀q ∈ Child(p) :: q.P Q = p.P Q ⇒ q.Q = W ) Answer(p) ≡ P arent(p).Q = A ∧ p.Q = W ∧ P arent(p
An internal processor p in the tree could have to transmit requests from its children (the request with highest priority first), only if no permission is received and used by the external algorithm at p (i.e., p.Req = REP ). A processor p transmits a request from a child in the following cases:

• p has a child sending a request with a higher priority than the current request transmitted by p (i.e., (Ch p ).P Q > p.P Q);

• there is no request with a higher priority than the current one treated by p and p has received an acknowledgement also received by all its children waiting it. That is, the acknowledgement to a request of highest priority is no more needed at p (see Predicate T ransmit(p));

• p is waiting for an acknowledgement and a new request is transmitted by a child of p with the same priority than the current one transmitted by p (see Predicate Retransmit(p)).

In all these above cases, p executes QRC-action to set p.Q to R and p.P Q to the highest priority among the requests that p have to treat (i.e., p.P Q = (Ch p ).P Q). If an internal processor q receives several requests from its children, then q transmits first the request with the highest priority (given by Macro Ch q ). Moreover, if p is sending a local request (i.e., p.Req = W AIT ) then by executing QRC-action, to transmit a request with higher priority than its local request (i.e., p.P Q > P riority(p)), p sets its shared variable p.Req to ASK to send later its local request when it is possible. A processor p sending a local request transmitted by its parent (see Predicate W ait(p)) sets its variable p.Q to W using QW -action in order to notice that it waits for an acknowledgement for its local request. This status is propagated up in the tree to the root using QW -action. Note that every processor q which has sent a local request or transmitted a request from a child with the same priority as p's request waits for an acknowledgement, only if all children of q transmitting a request with the same priority are in Status W (see Predicate W ait(p)). Indeed, this allows to remove bad requests due to an incorrect initial configuration and to synchronize request transmissions of same priority.

Unless a request of higher priority than p's request is treated at the root root(T ) of the tree T , when root(T ) is in Status W then it delivers its permission to p's request (see Predicate AnswerR). To this end, since root(T ) is the root of an allowed tree (i.e., it satisfies Allowed(root(T ))) then it executes QA-action to set its variable root(T ).Q to A. This permission is propagated down in the tree. Any processor q waiting for the acknowledgement of p's request on the path between root(T ) and p in the tree T with a parent having an acknowledgement to p's request (i.e., P arent(q).Q = A and q.P Q = P arent(q).P Q = p.P Q) also executes QA-action to transmit the acknowledgement (see Predicate Answer(q)). Finally, p executes QA-action to receive the acknowledgement to its local request, since p.Req = W AIT then p sets the shared variable p.Req to REP in order to notify to the external algorithm (Algorithm A) that the permission is delivered for the local request at p. Moreover, if a child x of p is also waiting for an acknowledgement to a request with the same priority than p's local request, then x executes QA-action too. Note that as soon as a received acknowledgement is no more needed at a processor p (i.e., p.Req is setted to OU T by the external algorithm), then a request transmitted by a child of p can be transmitted by p up in the tree using QRC-action.

However, a processor must be able to detect wrong requests due to an incorrect initial configuration. A request treated by a processor p is a wrong request in the following cases (see Predicate Error(p)):

• p is sending a local request whereas it has no local request (i.e., p.Q = A∧p.Req ∈ {ASK, W AIT } and p.P Q = P riority(p));

• p is transmitting a request from a child, but there is no child of p having a request with the same priority (i.e., p.Q = A ∧ p.P Q = P riority(p) ∧ (∀q ∈ Child(p), q.P Q = p.P Q ⇒ q.Q = A)).

When a processor p detects a wrong request, then p executes QE-action. Definition 2 (Allowed tree) A tree T rooted at processor p such that (p = root(T ) ∧ Allowed(p)) is called an allowed tree. Any tree T ′ rooted at processor q such that (q = root(T ′ ) ∧ ¬Allowed(q) is called a not allowed tree.

In the following, we consider a static forest F of trees constructed in the network G = (V, E). In the reminder, we make the hypothesis that the extern algorithm (Algorithm A) sets in finite time the shared variable p.Req from REP to OU T when a permission delivered at p is no more needed.

Proof assuming a weakly fair daemon

The following theorem proves that any execution of Question-Answer algorithm is deadlock-free.

Theorem 1 Let the set of configurations B ⊆ C such that there is at least one processor p ∈ V in an allowed tree which has a request to send or has sent a request and it does not receive an acknowledgement in every configuration

γ ∈ B. ∀γ ∈ B, ∃q ∈ V such that q is enabled in γ.

Proof.

Assume, by the contradiction, that ∃γ ∈ B such that ∀q ∈ V no action is enabled at q in γ. Assume then that there exists at least one allowed tree T in γ in which ∃p ∈ T such that p.Req = ASK. Consider the processor p ∈ T with the request of highest priority in T , i.e., (∀x ∈ T ::

x.Req = ASK ∧ P riority(p) > P riority(x)). In this case, either p.Req = ASK and QR-action is enabled at p, a contradiction, or ∃q ∈ P(root(T ), p) such that q.P Q = p.P Q. Moreover, since p's request is of highest priority in T then q satisfies p.P Q = (Ch q ).P Q and |P rioRC(q)| > 0. We assume that p.Req = REP, otherwise by hypothesis p.Req is setted to OU T in finite time. In this case, either we have (p.P Q > q.P Q ⇒ RequestT (q)) and QRC-action is enabled at q, a contradiction. Otherwise, q has transmitted a request with the same priority, i.e., we have p.P Q = q.P Q and q.Q = W (see Predicate Retransmit(q)), and QRC-action is enabled at q, a contradiction. The execution of QR-action sets p.Req to W AIT . Hence, by contradiction, p.Q = R, p.P Q = P riority(p) and p.Req = W AIT at p and ∀q ∈ P(root(T ), p), q.P Q = p.P Q. If ∃q ∈ P(root(T ), p) such that q.Q = W then QRC-action is enabled at q (see Predicate Retransmit(q)), a contradiction. Thus, ∀x ∈ P(root(T ), p), x.P Q = p.P Q ∧ x.Q = R. Then, we have (P arent(p).P Q = p.P Q ∧ p.P Q = P riority(p)) ⇒ W ait(p) and QW -action is enabled at p, a contradiction. If ∃q ∈ P(root(T ), p) such that q.Q = R ∧ (∃s ∈ Child(q) :: s.Q = W ) then QW -action is enabled at q, a contradiction. Hence, by contradiction, ∀x ∈ P(root(T ), p), x.P Q = p.P Q ∧ x.Q = W . Thus, QA-action is enabled at root(T ), a contradiction. If ∃q ∈ P(root(T ), p) such that P arent(q).Q = A ∧ q.Q = W then QA-action is enabled at q, a contradiction.

2

Lemma 1 Let an allowed tree T in a static forest F. After executing QE-action at a processor p ∈ T , QE-action is disabled at p until p sends or transmits another request.

Proof.

Assume, by the contradiction, that QE-action is enabled at a processor p ∈ T before p sends or transmits another request. After the first execution of QE-action, we have p.Q = A at p. If p can execute QE-action again then this implies that we have p.Q = A (because (p.Q = A ⇒ ¬Error(p))). Since we assume that p does not execute QR-action and QRC-action, then this implies that p.Q = W obtained by executing QW -action at p, a contradiction because W ait(p

) ⇒ p.Q = R at p (or W aitR(p) ⇒ p.Q = R if p = root(T )). 2
Lemma 2 Let an allowed tree T in a static forest F. When QR-action is enabled at processor p ∈ T , it remains enabled until p executes it and p remains in T .

Proof. Let γ → γ ′ be a step. Assume, by the contradiction, that QR-action is enabled at p in γ and not in γ ′ (i.e., ¬Request(p) in γ ′ ) but p did not execute QR-action in γ → γ ′ . According to the hypothesis of the lemma, we assume that p has no child with a request of priority higher than p's request (i.e., P riority(p) ≥ (Ch p ).P Q). QR-action is the enabled action at p which has the highest priority, otherwise according to Lemma 1 after executing QE-action then it is disabled at p. Moreover, we assume that p remains in T in γ ′ , so p.Req = ASK in γ ′ . Since p did not move in γ → γ ′ , we have p.P Q = P riority(p). Thus, Request(p) is satisfied in γ ′ , a contradiction.

2

Lemma 3 Let any allowed tree T in a static forest F. Every processor p ∈ T transmits the request with highest priority in its neighborhood.

Proof. According to formal description of Algorithm 1, to transmit a request a processor executes QR-action or QRC-action. Assume, by the contradiction, that there is a processor p ∈ T which does not transmit a request. That is, QR-action and QRC-action are disabled or they are not the enabled actions of highest priority at p.

We first show that QR-action and QRC-action are enabled at p. We must consider two cases: p has a local request to send with a priority higher than its children requests or p has a request from a child to transmit of highest priority. If p has a local request to send then p.Req ∈ {ASK, W AIT }. Since QR-action is not enabled at p, this implies that p.Req = W AIT and p has already sent its request, a contradiction. In first case, p's request has the highest priority in p's neighborhood (i.e., |P rioRC(p)| = 0 or P riority(p) ≥ (Ch p ).P Q). So QR-action is enabled at p, a contradiction. Otherwise, p has a child request with a priority higher than the priority of its local request (i.e., we have p.Req = REP and |P rioRC(p)| > 0). Consider the child q of p such that Ch p = q. We have that QR-action is disabled and by contradiction QRC-action is not enabled at p. Thus, to have ¬RequestT (p) this implies we have (Ch p ).P Q ≤ p.P Q and we must consider two subcases at p: p.Q = A or ∃s ∈ Child(p) such that s.Q = W ∧ s.P Q = p.P Q. Either p.Q = A then this implies that (Ch p ).P Q = p.P Q and p has already transmitted the request of q, a contradiction. Or ∃s ∈ Child(p) such that s.Q = W ∧ s.P Q = p.P Q. This implies that either s = q and p has already transmitted q's request or s = q and s.P Q > q.P Q, a contradiction because (Ch p ) = q. Thus, QR-action or QRC-action is enabled at every processor p ∈ T which has a local request or a request from a child to transmit of highest priority.

We must show that QR-action or QRC-action is the enabled action of highest priority for every processor p ∈ T which has a local request or a request from a child to transmit of highest priority. If QR-action or QRC-action are not the action of highest priority at p then this implies that QE-action is always enabled. According to Lemma 1, after executing QE-action it is not enabled at p (unless QR-action or QRC-action is executed), a contradiction. So, QE-action is disabled at p. According to Lemma 2, QR-action is enabled until it is executed at every processor p ∈ T having a request of priority higher than its children requests (i.e., P riority(p) ≥ (Ch p ).P Q). Otherwise, we have QR-action is disabled. Therefore, since QE-action and QR-action are disabled then QRC-action is the enabled action of highest priority for every processor p ∈ T which has a request of highest priority from a child to transmit.

2

Corollary 1 Let an allowed tree T in a static forest F. The request with highest priority in T is transmitted to root(T ).

Lemma 4 Let any allowed tree T in a static forest F. Every processor p ∈ T waits for an acknowledgement if p's parent transmits the request of highest priority in p's neighborhood.

Proof.

According to formal description of Algorithm 1, to wait for an acknowledgement to a request a processor executes QW -action. Assume, by the contradiction, that there is a processor p ∈ T which does not wait for an acknowledgement while p transmits the request of highest priority in its neighborhood. That is, QW -action is disabled or it is not the enabled action of highest priority at p.

We first show that QW -action is enabled at p. According to Lemma 3, for processor p we have p.Q = R, p.P Q = P riority(p), and p.Req = W AIT if p has sent a local request, or p.Q = R, p.P Q = P riority(p), and p.Req = REP otherwise. We must consider two cases: p's parent has not transmitted p's request or there is a child of p with a request of same priority which is not waiting for the acknowledgement (i.e., ¬[P arent(p).Q = R ∧ P arent(p).P Q = p.P Q] or ∃q ∈ Child(p) such that q.P Q = p.P Q ∧ q.Q = W ). Note that for root(T ) only the second case must be considered. If ¬[P arent(p).Q = R ∧ P arent(p).P Q = p.P Q] then this implies that the request transmitted by p's parent is not the request of highest priority in the neighborhood of p's parent (since its parent has transmitted another request), a contradiction with assumption of lemma to prove. Otherwise, ∃q ∈ Child(p) such that q.P Q = p.P Q ∧ q.Q = W . Then there is a path P(p, s) in T such that x.P Q = P riority(s) = q.LQ for every processor x ∈ P(p, s). Moreover, there is a processor y ∈ P(p, s) such that y.Q = W and P arent(y).Q = R. Thus, QW -action is enabled at P arent(y) from the first case. By induction on the length of path P(p, s) when every processor x has executed QW -action then q.Q = W , a contradiction.

We must show that QW -action is the enabled action of highest priority for every processor which transmits the request of highest priority in its neighborhood also transmitted by their parent. Assume, by the contradiction, that QW -action is not the enabled action of highest priority at p. Suppose that QE-action is the enabled action of highest priority at p. According to Lemma 1, after executing QEaction it is not enabled at p, a contradiction. So, QE-action is disabled at p. Suppose that QR-action or QRC-action is enabled at p, a contradiction because we assume that p has transmitted the request of highest priority in its neighborhood (i.e., ((p.

Req = W AIT ∧ p.Q = A) ⇒ ¬Request(p)) or ((p.Req = REP ∧ p.Q = A) ⇒ ¬RequestT (p))). 2
Corollary 2 Let an allowed tree T in a static forest F. root(T ) waits for an acknowledgement for the request of highest priority in T .

Lemma 5 Let an allowed tree T in a static forest F. A processor p ∈ T waiting for an acknowledgement to a transmitted request transmits again the request of a child with the same priority, if it is the request of highest priority in p's neighborhood.

Proof.

According to formal description of Algorithm 1, a processor p ∈ T waiting for an acknowledgement executes QRC-action to transmit again a request from a child with the same priority.

As there is a child request of highest priority in p's neighborhood transmitted by p, then we have p.Req = REP ∧|P rioRC(p)| > 0. Assume, by the contradiction, that p does not execute QRC-action to transmit again the request with the same priority. Either for every child q of p we have q.Q = R or q.P Q = p.P Q because (∀q ∈ Child(p) :: q.Q = R ∨ q.P Q = p.P Q) ⇒ ¬Retransmit(p). Either q.Q = R then q has no request to transmit because its request was already transmitted (i.e., q.Q = W ) or an acknowledgement was received (i.e., q.Q = A), a contradiction. Or q.P Q = p.P Q then the request to transmit again by p is not of highest priority in p's neighborhood (i.e., (Ch p ).P Q = q.P Q), a contradiction with the hypothesis of the lemma.

2

Lemma 6 Let any allowed tree T in a static forest F and a processor s ∈ T sending the request of highest priority in T . Every processor p ∈ P(root(T ), s) transmits the acknowledgement to the request of s.

Proof.

According to formal description of Algorithm 1, to transmit the acknowledgement to a request a processor executes QA-action. Assume, by the contradiction, that there is a processor p ∈ P(root(T ), s) which does not transmit the acknowledgement to the request of s. That is, QAaction is disabled or it is not the enabled action of highest priority at p.

We first show that QA-action is enabled at p. According to Lemma 4, for processor p we have p.Q = W , p.P Q = P riority(s), and p.Req = W AIT if p = s, or p.Q = W , p.P Q = P riority(s) = P riority(p) and p.Req = REP otherwise. We must consider two cases: p = root(T ) or p = root(T ). Consider processor root(T ), if QA-action is disabled then this implies that root(T ).Q = W , a contradiction with the assumption that for every processor q ∈ P(root(T ), s) we have q.Q = W . Now, p = root(T ). Consider p is the child of root(T ) such that p ∈ P(root(T ), s). If QA-action is disabled at p then either P arent(p).Q = A or P arent(p).P Q = p.P Q or p.Q = W , a contradiction because root(T ).Q = A from first case and we assume for every processor q ∈ P(root(T ), s) we have p.Q = W , p.P Q = P riority(s). Otherwise, p = root(T ) and p is not the child of root(T ). By induction on the length of path P(root(T ), s), the arguments used for processor p can be applied for every processor q ∈ P(root(T ), s). Thus, QA-action is enabled for every processor q ∈ P(root(T ), s).

We must show that QA-action is the enabled action of highest priority for every processor p ∈ P(root(T ), s). Assume, by the contradiction, that QA-action is not the enabled action of highest priority at p. According to Lemma 1, after executing QE-action it is not enabled at p, a contradiction. So, QE-action is disabled at p. Suppose that QR-action or QRC-action is enabled at p, a contradiction because we assume that p has transmitted the request of highest priority in its neighborhood (i.e., ((p.

Req = W AIT ∧ p.Q = A) ⇒ ¬Request(p)) or ((p.Req = REP ∧ p.Q = A) ⇒ ¬RequestT (p))). Suppose that QW -action is enabled at p, a contradiction because p.Q = R. 2
Lemma 7 Let an allowed tree T in a static forest F. Between the reception of two acknowledgements to a request, every processor p ∈ T has sent a new request.

Proof.

According to formal description of Algorithm 1, to receive an acknowledgement to a request in an allowed tree T a processor executes QA-action. Assume, by the contradiction, that there is a processor p ∈ T which receives two acknowledgements for the same request. That is, QR-action and QRC-action are not executed by p between two consecutive executions of QA-action.

After the first execution of QA-action by p, we have p.Q = A in configuration γ i . To execute QAaction in step γ j-1 → γ j , with i < j, this implies we had p.Q = W in γ j-1 because Answer(p) ⇒ p.Q = W (or AnswerR(p) ⇒ p.Q = W , if p = root(T )). Thus, QW -action was executed in step γ j-2 → γ j-1 . However, to execute QW -action in step γ j-2 → γ j-1 this implies we had

p.Q = R in γ j-2 because W ait(p) ⇒ p.Q = R (or W aitR(p) ⇒ p.Q = R, if p = root(T ))
. So, by formal description of Algorithm 1 QR-action or QRC-action was executed in step γ j-3 → γ j-2 , with i < j -3, a contradiction.

2

Lemma 8 Let an allowed tree T in a static forest F and a processor p ∈ T at height k with a local request of highest priority in T . From any configuration, in at most k+1 rounds p's request is transmitted to root(T ).

Proof. We show by induction the following proposition: If at height less than k in T there is no processor q ∈ T such that QR-action is enabled at q and ∃p ∈ T at height k such that p.Req = ASK, then in at most j + 1 rounds we have ∀q ∈ P(root(T ), p), q.Q = R ∧ q.P Q = P riority(p) at height ≥ kj in T . In the base case j = 0 and we consider p. According to Lemma 2, if Request(p) is satisfied at p then p executes QR-action and we have p.Q = R and p.P Q = P riority(p) at p. Consider that in first configuration of round 0 p satisfies Error(p), then p can execute QE-action and as the daemon is weakly fair at the end of round 0 we have p.Q = A and p.P Q = P riority(p). At the first configuration of round 1, p satisfies Request(p) and it can execute QR-action. Since the daemon is weakly fair, thus the proposition is verified because at the last configuration of round 1 we have p.Q = R and p.P Q = P riority(p) at p. Induction case: We assume that in round j = k -1 the proposition is true for any processor at height h, kj ≤ h ≤ k in P(root(T ), p). We have to show that if at height less than k in T there is no processor q ∈ T such that QR-action is enabled at q, then in round j + 1 for any processor q ∈ P(root(T ), p) at height h, k -(j + 1) ≤ h ≤ k, we have q.Q = R ∧ q.P Q = P riority(p). So, we consider the processor x ∈ P(root(T ), p) at height k -(j +1) in T . If QE-action is enabled at x in the beginning of round j then as the daemon is weakly fair we have (x.Q = A ∧ x.P Q = P riority(x)) ⇒ ¬Error(x) at the first configuration of round j + 1. Since there is no processor s ∈ T, s = p at height lower than k such that QR-action is enabled at s, then |P rioRC(x)| > 0 and Ch x = q such that q.Q = R and q.P Q = P riority(p). Either P riority(p) > x.P Q, then QRC-action is enabled at x in round j + 1. Or P riority(p) ≤ x.P Q, then as the daemon is weakly fair we have (∀s ∈ Child(x) :: s.Q = W ⇒ s.P Q = x.P Q), so T ransmit(x) is satisfied (remind that x has no request to send so x.Req = REP and x.Q = A) and QRC-action is enabled at x in round j + 1. In all the above cases, as the daemon is weakly fair in the last configuration of round j + 1 so we have x.Q = R and x.P Q = P riority(p) at x ∈ P(root(T ), p), which verifies the proposition. Therefore, since |P(root(T ), p)| = k in at most k + 1 rounds we have ∀q ∈ P(root(T ), p), q.Q = R ∧ q.P Q = P riority(p).

2

Lemma 9 Let an allowed tree T in a static forest F and a processor p ∈ T at height k with a local request of highest priority in T transmitted to root(T ). In at most k + 1 additional rounds, every processor q ∈ T waits for an acknowledgement if q transmits p's request.

Proof.

According to Lemma 8, since p.Req = W AIT ∧ p.Q = R ∧ p.P Q = P riority(p) at processor p ∈ T at height k then in at most k + 1 rounds we have ∀q ∈ P(root(T ), p), q.Q = R ∧ q.P Q = P riority(p).

We show by induction the following proposition: If at height less than k in T there is no processor q ∈ T such that QR-action is enabled at q, and ∀q ∈ P(root(T ), p), q.Q = R ∧ q.P Q = P riority(p), then in at most j + 1 rounds we have ∀q ∈ P(root(T ), p), q.Q = W ∧ q.P Q = P riority(p) at height ≥ kj in T . In the base case j = 0 and we consider p. We have (∀q ∈ P(root(T ), p), q.Q = R ∧ q.P Q = P riority(p)), in particular for P arent(p) and p. Thus, the proposition is verified for p because QWaction is enabled at p in round 0, and in the first configuration of round 1 we have p.Q = W and p.P Q = P riority(p) at p (since the daemon is weakly fair). Induction case: We assume that in round j = k -1 the proposition is true for any processor at height h, kj ≤ h ≤ k in P(root(T ), p). We have to show that if at height less than k in T there is no processor q ∈ T such that QR-action is enabled at q, then in round j + 1 for any processor q ∈ P(root(T ), p) at height h, k -(j + 1) ≤ h ≤ k, we have q.Q = W ∧ q.P Q = P riority(p). By induction hypothesis, in the first configuration of round j + 1 we have for any processor s ∈ P(root(T ), p) at height ≥ j we have s.Q = W ∧ s.P Q = P riority(p). Thus, ∃s ∈ Child(q), s.Q = W ∧ s.P Q = q.P Q, and q.Q = R so QW -action is enabled at q in round j + 1. So, since the daemon is weakly fair we have q.Q = W and q.P Q = P riority(p) at q, in the last configuration of round j + 1, which verifies the proposition. Therefore, since |P(root(T ), p)| = k in at most k + 1 additional rounds we have ∀q ∈ P(root(T ), p), q.Q = W ∧ q.P Q = P riority(p).

2

Lemma 10 Let an allowed tree T in a static forest F and a processor p ∈ T at height k with a local request of highest priority in T transmitted to root(T ). In at most k + 1 additional rounds, every processor q ∈ T transmits the acknowledgement to p's request if q has transmitted p's request.

Proof. According to Lemmas 8 and 9, in at most 2(k+1) rounds we have ∀q ∈ P(root(T ), p), q.Q = W ∧ q.P Q = P riority(p).

We show by induction the following proposition: If at height less than k in T there is no processor q ∈ T such that QR-action is enabled at q, and ∀q ∈ P(root(T ), p), q.Q = W ∧ q.P Q = P riority(p), then in at most j + 1 rounds we have x.Q = A ∧ x.P Q = P riority(p) at processor x ∈ P(root(T ), p) of height ≤ j in T . In the base case j = 0 and we consider x = root(T ). We have (∀q ∈ P(root(T ), p), q.Q = W ∧ q.P Q = P riority(p)), in particular for root(T ). The proposition is verified for x because we have (x.Q = W ⇒ AnswerR(x)) and QA-action is enabled at x in round 0. Thus, in the first configuration of round 1 we have x.Q = W ∧ x.P Q = P riority(p) at x (since the daemon is weakly fair). Induction case: We assume that in round j the proposition is true for every processor at height ≤ j in P(root(T ), p). We have to show that if at height less than k in T there is no processor q ∈ T such that QR-action is enabled at q, then in round j + 1 for processor x ∈ P(root(T ), p) at height j + 1, we have x.Q = A ∧ x.P Q = P riority(p). By induction hypothesis, in the first configuration of round j + 1 we have P arent(x).Q = A ∧ P arent(x).P Q = x.P Q ∧ x.Q = W at x, so QA-action is enabled at x in round j + 1. Therefore, since the daemon is weakly fair we have x.Q = A and x.P Q = P riority(p) at x, in the first configuration of round j + 1 which verifies the proposition. Moreover, we have |P(root(T ), p)| = k because p is at height k in T . According to formal description of Algorithm 1, if x.P Q = P riority(x) when QA-action is executed at x then we have x.Req = REP . So we have x = p, and in most k + 1 additional rounds we have p.Req = REP ∧ p.Q = A ∧ p.P Q = P riority(p). 2 Lemma 11 Let the set of configurations B ⊆ C such that in every γ ∈ B there is no request and every processor p ∈ V has received an acknowledgement. In every configuration γ ∈ B, for every processor p ∈ V no action of Algorithm 1 is enabled.

Proof.

Since there is no request in γ then for every processor p ∈ V we have p.Req = ASK and p.Req = W AIT . Moreover, observe that according to formal description of Algorithm 1 for every processor p ∈ V we have p.Q = A either when p.Req = W AIT or when p.Req = OU T or p.Req = ASK with a descendant x of p such that x.Req = W AIT . However, as ∀p ∈ V, p.Req = ASK and therefore p.Req = W AIT this implies we have ∀p ∈ V, p.Q = A in γ.

Assume, by the contradiction, that ∃γ ∈ B such that ∃p ∈ V with an enabled action of Algorithm 1. If QE-action is enabled at p then this implies that p.Q = A, a contradiction. If QR-action is enabled at p then this implies that p.Req = ASK, a contradiction since ∀p ∈ V, p.Req = ASK. If QRC-action is enabled at p then there is a child q of p such that q.Q = A (i.e., |P rioRC(p)| > 0), a contradiction because ((∀p ∈ V, p.Q = A) ⇒ |P rioRC(p)| = 0). If QW -action is enabled at p then this implies that p.Q = R, a contradiction because ∀p ∈ V, p.Q = A. If QA-action is enabled at p then this implies that p.Q = W , a contradiction because ∀p ∈ V, p.Q = A.

2

Lemma 12 Let a tree T in a static forest F. From any configuration where a processor p ∈ T executes QR-action, the execution satisfies Specification 1.

Proof. We have to show that starting from any configuration the execution of Algorithm 1 verifies all the properties of Specification 1.

We first show that Property [Liveness 1] is satisfied. Let an allowed tree T in a static forest F. From any configuration according to Lemmas 2 and 8 a processor in T which has a local request of highest priority in T sends this request to root(T ) in finite time with Algorithm 1. Assume, by the contradiction, that there is a processor p ∈ T which has infinitely often a request to send but it can not send its request to root(T ), although there are a finite number of requests sent in T . This implies either that an infinite time is needed to send a request from p to root(T ), a contradiction with Lemmas 2 and 8, or the request sent by p is never the request of highest priority in T , a contradiction with the hypothesis of a finite number of requests sent in T . This satisfies Property [Liveness 1] of Specification 1.

We now show that Property [Liveness 2] is satisfied. Let a processor p ∈ T which has sent a request in an allowed tree T and waits for the acknowledgement to its request. According to Theorem 1, the execution of Algorithm 1 is not done. Moreover, by Lemma 6 a processor which has sent a request with highest priority in T receives an acknowledgement from root(T ) in finite time. Thus, at least one processor receives an acknowledgement from root(T ) in a finite time, the processor waiting for the acknowledgement to the request of highest priority in T . This satisfies Property [Liveness 2] of Specification 1.

We now show that Property [Safety 1] is satisfied. According to Lemma 6, a processor p which has sent a local request in an allowed tree T receives at least one acknowledgement to its request. Moreover, by Lemma 7 a processor p receives at most one acknowledgement to a sent request. This satisfies Property [Safety 1] of Specification 1.

We now show that Property [Safety 2] is satisfied. Assume, by the contradiction, that there is a processor p sending a request in a not allowed tree T which receives an acknowledgement from root(T ). Since root(T ) is the root of a not allowed tree, we have ¬Allowed(root(T )) and P arent(root(T )) ∈ N eig root(T ) . So, there is a cycle in T because every processor in T has a parent. Moreover, if p receives an acknowledgement from root(T ) then root(T ) can execute QA-action. This implies that P arent(root(T )).Q = A because Answer(p) ⇒ P arent(root(T )).Q = A. So, either root(T ).Q = R or root(T ).Q = W ∧ root(T ).P Q = P arent(root(T )).P Q then P arent(root(T )) executes QRCaction (because T ransmit(P arent(root(T ))) ⇒ RequestT (P arent(root(T )))), a contradiction. Otherwise, we have P arent(root(T )).Q = A ∧ (∀q ∈ Child(P arent(root(T ))), q.Q = W ∧ q.P Q = P arent(root(T )).P Q) given by an initial configuration of the system, a contradiction. This satisfies Property [Safety 2] of Specification 1.

2

By Theorem 1 and Lemmas 11 and 12, the result below follows:

Theorem 2 Algorithm 1 is snap-stabilizing for Specification 1 under a weakly fair daemon.

Proof assuming an unfair daemon

Lemma 13 Let any allowed tree T in a static forest F and any processor p ∈ T with a local request of highest priority in T . If there is no new request with higher or equal priority than p's request in T , then p's request is transmitted to root(T ) in at most 2n steps, with n the number of processors in the network.

Proof.

According to Lemma 3, if there is no new request with higher or equal priority than p's request in T then every processor q ∈ P(root(T ), p)\{p} executes QRC-action to transmit p's request to root(T ). Observe that |P(root(T ), p)| ≤ n and QR-action is disabled at every processor q ∈ P(root(T ), p)\{p}. Suppose that for every processor q the enabled action of highest priority is QEaction, then after executing QE-action we have q.Q = A and q.P Q = P riority(q) and QE-action is disabled at q according to Lemma 1. Then, QRC-action is the enabled action of highest priority at q. As |P(root(T ), p)| ≤ n, in at most 2n steps p's request is transmitted to root(T ).

2

Lemma 14 Let any allowed tree T in a static forest F and any processor p ∈ T with a local request of highest priority in T transmitted to root(T ). If there is no new request with higher or equal priority than p's request in T , then p receives an acknowledgement from root(T ) in at most 2n steps, with n the number of processors in the network.

Proof.

We assume there is no new request with higher or equal priority than p's request in T . Thus according to Lemma 3, we have q.Q = R and q.P Q = P riority(p) for every processor q ∈ P(root(T ), p). Moreover, the following actions are disabled for every processor q ∈ P(root(T ), p): QE-action because there exists a child s of q such that s.P Q = q.P Q∧s.Q = A (in case of p, p.Req = W AIT ); QR-action because q.Req = ASK or P riority(q) < q.P Q = (Ch q ).P Q; and QRCaction because q.Q = R∧(∀s ∈ Child(q), s.Q = W ∧s.P Q = q.P Q). According to Lemmas 4 and 6, since there is no new request with higher or equal priority than p's request in T thus every processor q ∈ P(root(T ), p) executes QW -action to wait for an acknowledgement to p's request and then executes QA-action to transmit the acknowledgement from root(T ) to p. Observe that |P(root(T ), p)| ≤ n, thus in at most 2n steps p receives the acknowledgement from root(T ) to its local request.

2

Lemma 15 Let any allowed tree T in a static forest F. In at most O(n 2 ) steps, at least one processor p with a local request receives an acknowledgement from root(T ) to its request.

Proof. Assume without loss of generality that forest F is composed of a single tree T containing the n processors of the network. By Lemma 3, a request of highest priority stops the transmission of the acknowledgement of a request of lowest priority at a processor q ∈ T because (Ch q ).P Q > q.P Q ⇒ RequestT (q). Moreover, by Lemma 7 it is also the case at a processor q ∈ T if there is a new request with the same priority than the previous request of highest priority because Retransmit(q) ⇒ RequestT (q). According to Lemma 13, if there is no new request with higher or equal priority than p's request in T then in at most 2n steps the processor p receives an acknowledgement. However, since there is at most n requests in parallel in T then the acknowledgement of p's request can be stopped at most n -1 times.

2

Corollary 3 Let a static forest of trees F and a given set of requests. If there is no new request in F then in at most O(n 3 ) steps every processor with a local request has received an acknowledgement to its request.

Proof. First observe that given a static forest F, we can have a local request from at most each processor in F, i.e., at most n processors have a local request to send. According to Lemma 15, in at most O(n 2 ) steps at least one processor sending a request receives an acknowledgement and as we have at most n processors with a local request in F, then the corollary follows. 2

Spanning Tree Construction

In this section, we are interested in to the problem of constructing a tree spanning all the processors of the network. To this end, we give a snap-stabilizing algorithm which uses the algorithm presented in the precedent section as a black box. Moreover, we consider there is a particular root processor, noted r, which is used to construct a spanning tree. More precisely, we consider the construction of a Breadth First Search (BFS) tree rooted at processor r. We can define a BFS tree as in Definition 4.

Definition 4 (BFS Tree)

Let G = (V, E) be a network and r a node called the root. A graph T = (V T , E T ) of G is called a Breadth First Search tree if the following conditions are satisfied:

1. V T = V and E T ⊆ E, and
2.
T is a connected graph (i.e., there exists a path in T between any pair of nodes x, y ∈ V T ) and

|E T | = |V | -1, and
3. For each node p ∈ V T , there exists no shorter path (in hops) between p and r in G than the path between p and r in T .

We give a formal specification to the problem of constructing a stabilizing BFS tree, stated in Specification 2.

Specification 2 (Tree Construction)

Let C the set of all possible configurations of the system. An algorithm A BFS solving the problem of constructing a stabilizing BFS tree satisfies the following conditions:

Breadth first search tree algorithm

In this section, we present a snap-stabilizing algorithm, called BFS, to construct a BFS tree. Algorithm BFS is a semi-uniform algorithm, this means that exactly one of the processors, called the root and denoted r, is distinguished. This distinguished processor is used in Algorithm BFS as the root of the spanning tree.

Algorithm BFS is a composition of two algorithms: Algorithm 1 which solves the Question-Answer problem (see Section 3) and Algorithm 2 which allows to a processor to connect to a tree. These two algorithms are executed concurrently at each processor p ∈ V . To construct a BFS tree, Algorithm 2 plays the role of Algorithm A for Algorithm 1 as described in Section 3. That is, Algorithm 2 interrogates Algorithm 1 to obtain permissions allowing processors to connect correctly in order to construct a BFS tree. More precisely, given a forest of trees F we must designate for every processor p ∈ V with Predicate Allowed(p) the set of processors which are allowed to deliver permissions, according to Algorithm 1. For the construction of a BFS tree rooted at processor r, we must define that Allowed(p) ≡ (p = r) for every processor p ∈ V . The idea behind this is to only authorize processor connections to the tree rooted at r and to forbid the connections to the other trees of forest F. Each processor p ∈ V has a status in Algorithm 2 which is used to notify if p belongs to the tree rooted at r or not. When a processor p = r determines it is the root of a tree in F, then it informs the processors in its tree that they are not in the tree rooted at r and these processors set their status to E. In the same way, each processor in the tree rooted at r sets its status to C. Thereby, when a processor p in the tree rooted at r (i.e., in Status C) detects a neighbor q in Status E or whose q's parent level is bigger than p's level, then Algorithm 2 generates a local request at p to obtain a permission, delivered by Algorithm 1. The computation associated to a delivered permission at a processor p is to authorize its neighbors to connect to p. Therefore, if a permission is given to processor p then its neighbors q can execute Algorithm 2 to join the tree p belongs to.

Algorithm 1 can be viewed as a synchronizer allowing the BFS tree construction layer by layer, the addition of any new layer of processors depending of a permission request. It is easy to see that this construction needs O(D 2 ) rounds. In another hand, the mechanism we use for deleting the abnormal trees is obviously in O(n) rounds, since the height of such a tree can be in O(n). But any processor in an abnormal tree far from the root of this tree will become the neighbour of at least a processor of the normal BFS tree in O(D 2 ) rounds and will hook to it even if the abnormal tree is not yet deleted. So the global round complexity is still O(D 2 ) (see Lemma 19). In fact, the role of the deleting part is to ensure that any processor cannot hook the same abnormal tree arbitrarily often and finally we limit the step complexity to O(mn 4 ) (see Lemma 29).

Variables

We define below the different variables used by Algorithm 2.

Shared variable.

Each processor p ∈ V has a local shared variable p.Req which is used by Algorithm 2 to monitor Algorithm 1 at p. This shared variable can take four values: ASK, W AIT, REP, and OU T . By setting the shared variable p.Req to ASK, Algorithm 2 informs Algorithm 1 that a permission from the root of the tree that p belongs to is needed at p. In this case, Algorithm 1 tries to send a request and to obtain a permission for p if it is possible (i.e., if p belongs to an allowed tree and this request has the highest priority during enough time). If a permission is delivered to processor p, then Algorithm 1 sets this shared variable to REP in order to inform Algorithm 2. Then, every neighbor of p can execute Algorithm 2 to join the tree that p belongs to. When there is no neighbor of p to connect, then Algorithm 2 sets p.Req to OU T which allows to Algorithm 2 to request another permission through Algorithm 1 if needed.

Local variables. Each processor p ∈ V maintains three local variables:

• p.P : it gives the parent of p in the tree it belongs to, p.P = ⊥ for processor p = r.

• p.L: it stores the level (or height) of p in the tree it belongs to, p.L = 0 for processor p = r.

• p.S: it defines the status of processor p. It can take two values: E if p does not belong to a tree rooted to a processor x satisfying Predicate Allowed(x), C otherwise. We have p.S = C for processor p = r.

Algorithm description

As described before, we consider a forest F of trees and a distinguished processor r which is the only processor authorized to deliver permissions in the network (i.e., Allowed(p) ≡ (p = r) for every processor p ∈ V ). We can notice that in a tree there is a strong constraint between the level of a processor and the level of its parent in the tree: For any processor p = r, the level of p's parent must be equal to p's level minus 1. Therefore, the root of a tree in forest F is either (i) processor r, or (ii) a processor p = r such that p.L ≤ (p.P ).L (it is used to detect cycles in the network). Since we want to construct a spanning tree, in case (ii) we say that processor p is an abnormal root. Moreover, any processor p = r in a tree in F rooted at an abnormal root belongs to an abnormal tree. Every processor p ∈ V in an abnormal tree can execute E-action to change its Status to E (i.e., p.S = E) and to inform its descendants in the tree (see the formal description of Algorithm 2). Note that to reduce the number of moves executed by Algorithm BFS, a processor p ∈ V in an abnormal tree does not ask any permission.

Processor p waits until a neighbor q in the tree rooted at r authorizes p to connect to q. When a BFS tree is constructed, the following property is verified at each processor p ∈ V, p = r: The level of p's parent is equal to p's level minus 1 (i.e., (p = r) ⇒ (p.L = (p.P ).L + 1)). For processor r, we have the following constant values: r has no parent and a level equal to zero (i.e., (p = r) ⇒ (p.P = ⊥ ∧ p.L = 0)). Moreover, according to Claim 3 of Definition 4 we must have that the deviation on the level values between any processor p ∈ V and its neighbors does not exceed one (i.e., ∀q ∈ N eig p , |q.Lp.L| < 1). If one of these above constraints are not verified then a BFS tree is not constructed. Therefore, we have either at least one abnormal tree in F or there is a processor p ∈ V with a neighbor q such that q.Lp.L > 1 (i.e., Predicate GP -REP (p) is satisfied at p). In these cases, processor p executes A-action to set the shared variable p.Req to ASK in order to ask the permission to allow q to connect to p, if p is not already asking a permission (i.e., we have p.Req = OU T ). To this end, Algorithm 1 sends a request to the root of the tree.

Inputs for Algorithm 1. In order to allows Algorithm 1 to send a request the following inputs are given at processor p: (i) Child(p) is the set of children of p in the tree (i.e., Child(p) ≡ {q ∈ N eig p : q.P = p}), (ii) P arent(p) is the parent of p in the tree (i.e., P arent(p) ≡ p.P ), (iii) P riority(p) is the priority of the local request of p which is equal to the opposite of p's level in the tree for the task of constructing a BFS tree (i.e., P riority(p) ≡ -p.L), and (iv) Allowed(p) is a predicate which notifies if p can deliver permissions (i.e., Allowed(p) ≡ (p = r)). Remind that Allowed(p) must be satisfied only at processor p = r in Algorithm 1 to allow that eventually every processor joins the tree rooted at r, since eventually the processors cannot join another tree in forest F.

In the case a permission is delivered at processor p (i.e., we have p.Req = REP ), then each neighbor q of p can execute C-action to connect to p. However to construct a BFS tree without an overcost on moves, processor q waits for until its neighbor x with the smallest level in a normal tree gives its authorization to q to connect by executing C-action (i.e., we have x.Req = REP ∧ x = M inChP ar(q)). When processor q executes C-action then it sets its variables p.P and p.L according to its new parent in the tree, and it changes its status to Status C and its shared variable p.Req to OU T . Finally, if there is no neighbor for which processor p needs a permission (i.e., Predicate GP -REP (p) is no more satisfied at p), then p executes O-action to set its shared variable p.Req to OU T . This informs Algorithm 1 that the permission can be removed at p, then this allows p to ask a new permission later.

Note that a request mechanism was also used in previous stabilizing spanning tree construction algorithms [START_REF] Afek | Memory-efficient self-stabilizing protocols for general networks[END_REF][START_REF] Cournier | Snap-stabilizing pif and useless computations[END_REF]. However the mechanism in [START_REF] Cournier | Snap-stabilizing pif and useless computations[END_REF] gives strong guarantees due to the PIF task. Indeed, the nodes in abnormal trees are frozen and these nodes can leave the tree after the agreement of the root. The goal is to insure that every processor of the network belongs to the same tree before the propagation of the information. In our approach, the nodes in an abnormal tree are autonomous to take a decision and to leave the tree if possible, which leads to a time complexity in terms of rounds independent of the number of network nodes. Moreover, contrary to [START_REF] Afek | Memory-efficient self-stabilizing protocols for general networks[END_REF], abnormal trees are detected more efficiently since the detection is done locally and not using node identifiers. This allows to avoid a part of useless node additions.

Composition. Algorithm BFS is obtained by composition of Algorithm 1 and Algorithm 2. These two algorithms are composed together at each processor p ∈ V with a conditional composition (first introduced in [START_REF] Kumar Datta | Self-stabilizing network orientation algorithms in arbitrary rooted networks[END_REF]): Algorithm 2 • | Cond(p) Algorithm 1, where each guard g of the actions of Algorithm 1 at each processor p ∈ V has the form Cond(p) ∧ g with Predicate Cond(p) defined below (see Algorithm 2 for the description of predicates): Cond(p) ≡ GoodT (p) ∧ GoodL(p).

Using this composition, each processor p ∈ V can execute Algorithm 1 (i) to transmit requests and acknowledgements only if the tree containing p is locally correct (i.e., Predicate GoodT (p) is satisfied), and (ii) to ask a permission if needed (i.e., Predicate GoodL(p) is satisfied). Moreover, actions of Algorithm 1 and Algorithm 2 can be enabled at p simultaneously. In this case, Algorithm 1 is executed before Algorithm 2 at processor p. We give below the definitions used in this section, in particular we define precisely the notion of tree and normal tree.

Definition 5 (Tree) ∀p ∈ V such that Allowed(p) ∨ (p.P ).L ≥ p.L, we define a set T ree(p) of processors as follows: ∀q ∈ V, q ∈ T ree(p) if and only if ∃P(p, q). Definition 6 (Normal tree) A tree T rooted at processor root(T ) containing only processors p such that (p = root(T ) ∧ Allowed(p)) ∨ (p.S = C ∧ p.L = (p.P ).L + 1) is called a normal tree. Any tree T ′ rooted at processor root(T ′ ) such that ¬Allowed(root(T ′ )) is called an abnormal tree.

In the following, we consider there is only one processor p ∈ V which is allowed to send an acknowledgement to a request, the root r, i.e., Allowed(p) ≡ (p = r). Therefore, there is only one normal tree, the tree T ree(r) rooted at r. Moreover, given two processors u, v ∈ V we define by d H (u, v) the distance (in hops) between u and v in the subgraph H.

Remark 1

The system always contains one normal tree: the tree rooted at processor r.

Remark 2 All actions of Question-Answer algorithm are disabled for every processor p ∈ V \{r} such that p.S = E or p.L = (p.P ).L + 1 or (∃q ∈ N eig p :: p.L > q.L + 1).

The above remark comes from the conditional composition of Algorithm BFS. In the two first cases, a processor p cannot execute Question-Answer algorithm because Predicate GoodT (p) is not satisfied, whereas the third case does not satisfy Predicate GoodL(p). Proof. Assume, by the contradiction, that ∃γ ∈ (C -B) such that ∀p ∈ V no action is enabled at p in γ. Since γ ∈ B, there is at least one abnormal tree T in γ. Consider first every node p ∈ T such that p.S = C. According to formal description of Algorithm 2, every processor p ∈ V, p = r, has a parent (i.e., p.P ∈ N eig p ). So, if p = root(T ) then we have (p.P ).L ≥ p.L (see Definition 5), and E-action is enabled at p, a contradiction. If ∃p ∈ T such that (p.P ).S = E, then E-action is enabled at p, a contradiction. Now, in any abnormal tree T we have ∀p ∈ T, p.S = E. Since γ ∈ B, then there is at least one abnormal tree T or ∃q ∈ N eig p , q.Lp.L > 1 for a processor p ∈ V . So, ∃p ∈ T ree(r), such that GP -REP (p). In this case, either p.Req = OU T then A-action is enabled at p, a contradiction. Hence, by the contradiction, ∀p ∈ T ree(r), p.Req = OU T . If p.Req = ASK then according to Lemma 18 in a finite time p.Req = REP . Thus, we assume that p.Req = REP . Either, GP -REP (p) then there exists a processor q ∈ N eig p such that C-action is enabled at q since ((GP -REP (p)∧p.Req = REP ) ⇒ (∃q ∈ N eig p , Connect(q))), a contradiction. Or, ¬GP -REP (p) then O-action is enabled at p, a contradiction.

2

Lemma 16 Let an abnormal tree T of height h. From any configuration, in at most h + 1 rounds we have ∀p ∈ T, p.S = E.

Proof.

We show by induction the following proposition: In at most j + 1 rounds, we have ∀p ∈ T, (d T (root(T ), p) ≤ j ⇒ p.S = E). In base case j = 0. Consider any processor p such that (p.P ).L ≥ p.L. If p.S = E then E-action is enabled at p in round 0. Therefore, since the daemon is weakly fair then in the first configuration of round 1, we have p.S = E at p which verifies the proposition. Induction case: We assume that in round j = h -1 we have ∀q ∈ T, (d T (root(T ), q) ≤ j ⇒ q.S = E). We have to show that in round j + 1 we have ∀p ∈ T, (d T (root(T ), p) ≤ j + 1 ⇒ p.S = E). Consider any node p ∈ T of height j+1 in T . By induction hypothesis, we have (p.P ).S = E and if p.S = E then E-action is enabled at p in round j. Thus, since the daemon is weakly fair then in the first configuration of round j + 1 we have p.S = E and we have also ∀q ∈ T, (d T (root(T ), q) ≤ j ⇒ q.S = E). Therefore, in at most h + 1 rounds we have ∀p ∈ T, (d T (root(T ), p) ≤ h ⇒ p.S = E). 2

T ree(r) is connected. Observe that, the subgraph T ree(r) is a spanning tree of the network G. Indeed, every processor p ∈ V has a parent in T ree(r) except r which has no parent (i.e., there is an unique path between p and r) and T ree(r) is connected, so the subgraph T ree(r) contains no cycle. Thus, these remarks imply that the configuration γ verifies Claims 1 and 2 of Definition 4. To show the last Claim of Definition 4, assume by the contradiction that T ree(r) is not a breadth first search tree. This implies that ∃p ∈ T ree(r) such that (∃q ∈ N eig p :: q.L < (p.P ).L). That is, we have p.Lq.L > 1 which contradicts the proposition verified by every processor p ∈ T ree(r) according to the induction proof above. Therefore, Claim 3 of Definition 4 is verified, which finishes to show the lemma. 2

Corollary 4 From any configuration, in at most O(D 2 ) rounds there is no abnormal tree in forest F, with D the diameter of the network.

Lemma 20

In every configuration γ ∈ C satisfying Definition 4, for every processor p ∈ V no action of Algorithm 2 is enabled in γ.

Proof. Observe first that since γ satisfies Definition 4, then for every processor p ∈ V we have ∀q ∈ N eig p , |p.Lq.L| ≤ 1. Moreover, there is a single tree spanning every processor p ∈ V , thus there exists no abnormal tree and by Definition 5 for every processor p ∈ V we have p.S = C ∧ p.L = (p.P ).L + 1. These two observations imply that every processor p ∈ V is locally healthy in γ (see Definition 7).

Assume, by the contradiction, that ∃γ ∈ C satisfying Definition 4 such that ∃p ∈ V with an enabled action of Algorithm 2 at p. If E-action is enabled at p then (p.P ).S = E or (p.P ).L ≥ p.L, a contradiction because p is a locally healthy processor in γ. If C-action is enabled at p and p.S = C then ∃q ∈ N eig p such that p.L-q.L > 1, a contradiction because p is locally healthy. If A-action is enabled at p then ∃q ∈ N eig p such that either q.S = E, a contradiction because we have ∀p ∈ V, p.S = C in γ, otherwise ∃q ∈ N eig p , q.Lp.L > 1, a contradiction because p is locally healthy. Finally, if O-action is enabled at p then p.Req = REP and p can execute O-action in step γ → γ ′ . In configuration γ ′ , we have p.S = C ∧ p.Req = OU T so O-action is disabled. Moreover, there is no request because every processor p ∈ V is locally healthy in γ ′ , a contradiction.

2

By Lemmas 11 and 20, we have the following corollary.

Corollary 5

In every configuration γ ∈ C satisfying Definition 4, every action of Algorithm BFS is disabled at each processor p ∈ V in γ.

Lemma 21

From any configuration, the execution satisfies Specification 2.

Proof.

We have to show that starting from any configuration the execution of Algorithm BFS verifies Property [TC1] and [TC2] of Specification 2.

According to Lemma Remark 3 For every processor p ∈ T ree(r), E-action is disabled at p.

Remark 4 E-action, C-action, and A-action are disabled at a locally healthy processor p ∈ V .

Proposition 1 Every processor p ∈ V is hooked on to the neighbor q such that ∀s ∈ N eig p , q.L ≤ s.L.

Proof.

According to formal description of Algorithm 2, a processor hooks on to a neighbor using C-action. Assume, by the contradiction, that there is a processor p ∈ V such that ∃s ∈ N eig p , (p.P ).L > s.L. We must consider two cases: s is in an abnormal tree or not. If s is in an abnormal tree then either s.S = E then s ∈ M inChP ar(p) ⇒ ¬Connect(p) a contradiction, or s.S = C then by Property [Safety 2] of Specification 1 s never receives an acknowledgement and we have that s.Req = REP ⇒ ¬Connect(p), otherwise C-action is enabled at p, a contradiction. If s is in a normal tree then by Property [Liveness 2] of Specification 1 we have that s.Req = REP and C-action is enabled at p, a contradiction.

2

Lemma 22 Let any abnormal tree T ∈ F and the set of processors B = {p ∈ V : p ∈ T ∧ (∃q ∈ N eig p :: q ∈ T )}. In an execution, only processors in B can hook on to T .

Proof. Consider any abnormal tree T ∈ F in configuration γ ∈ C. According to formal description of Algorithm 2, a processor p must execute C-action to hook on to a tree, i.e., there is a neighbor q such that q.Req = REP . Suppose that every processor q ∈ B executes C-action and they are hooked on to T in configuration γ k . Note that after executing C-action, we have q.Req = OU T at every processor q ∈ B. Assume, by the contradiction, that there is a processor p ∈ T in configuration γ k which hooks on to T in step γ k → γ k+j , j > 0. This implies that p hooks on to a neighbor q ∈ B (by definition of B) such that q.Req = REP , a contradiction by Property [Safety 2] of Specification 1 because q can not receive an acknowledgement from root(T ) since T is an abnormal tree.

2

Corollary 6 Let any abnormal tree T ∈ F and the set of processors B = {p ∈ V : p ∈ T ∧ (∃q ∈ N eig p :: q ∈ T )}. In an execution, at most |B| processors can hook on to T .

Proposition 2 Let a processor p ∈ V which hooks on to a tree T in configuration γ i ∈ C. If another processor q ∈ V hooks on to T by p in γ i+j , j > 0, then T is a normal tree.

Proof.

According to Lemma 22, the expansion of an abnormal tree T ′ is limited at distance one from T ′ . After p hooks on to T , to allow the processor q to hook on to T by p then p receives an acknowledgement from root(T ). Therefore, T is a normal tree by Specification 1.

2

Lemma 23 Let any abnormal tree T ∈ F. A processor p ∈ V can hook on to T at most once by the same neighbor q ∈ T .

Proof.

Assume, by the contradiction, that there is a configuration γ k ∈ C such that there is a processor p ∈ V which hooks on to T by the same neighbor q ∈ T a second time. To hook on to T , p must execute C-action, i.e., there is a neighbor x ∈ T of p such that x.S = C and x.Req = REP . According to Proposition 1, p hooks on to the neighbor x ∈ V such that x.S = C ∧ (∀s ∈ N eig p , x.L ≤ s.L). Suppose that p hooks on to T by the neighbor q a first time in step γ i-1 → γ i ∈ C, then p hooks on to another neighbor s of p, s = q, in step γ j-1 → γ j ∈ C, j > i. Now, we must consider several cases in configuration γ k , i < j < k. If p is hooked on to s in γ j because q.S = E and s.Req = REP in γ i then since q ∈ T we have q.S = E in γ k and q ∈ M inChP ar(p) ⇒ ¬Connect(p), a contradiction. Otherwise s.S = q.S = C and p is hooked on to s in γ j , i < j < k, because s.L < q.L and s.Req = REP . When p hooks on to q the first time in step γ i-1 → γ i , we have s.S = E or s.L > q.L. Since we have s.S = C ∧ s.L < q.L ∧ s.Req = REP and p hooks on to s in step γ j-1 → γ j , this implies that s is in a normal tree in γ j according to Proposition 2. Thus, we have s.S = C ∧ s.L < q.L in γ k and q ∈ M inChP ar(p) ⇒ ¬Connect(p), a contradiction.

2

Lemma 24 In an execution, every processor p ∈ V \{r} produces at most 2∆ topological changes in forest F while p ∈ T ree(r), with ∆ the maximum degree of a processor in the network.

Proof. To hook on to a tree, a processor p ∈ V must execute C-action. According to Lemma 23, p cannot hooks on to an abnormal tree T ∈ F twice by the same neighbor q of p. Since a processor can have at most ∆ neighbors, p can hook on at most ∆ times to an abnormal tree. Observe that E-action has a higher priority than C-action and E-action can be executed between two executions of C-action, i.e., at most ∆ times while p ∈ T ree(r). Therefore, by Definition 8 the lemma follows.

2

Lemma 25 In an execution, every processor p ∈ V \{r} produces at most n topological changes in forest F while p ∈ T ree(r), with n the number of processors in the network.

Proof. Observe that for every processor p ∈ T ree(r) we have p.S = C. Moreover, by Remark 3 for every processor p ∈ T ree(r) we have that E-action is disabled. So, by Definition 8 the only topological change in F that a processor p ∈ T ree(r) can produce is to execute C-action in order to reduce its level in T ree(r). Thus, by Proposition 1 each execution of C-action by a processor p ∈ T ree(r) in step γ i → γ i+1 implies that p hooks on to the neighbor with the lowest level in γ i+1 and p.L in γ i is higher than p.L in γ i+1 . Therefore, since the size of T ree(r) is bounded by n then any processor p can hook on to at most n -1 processors by executing C-action while p ∈ T ree(r).

2

Lemma 26 In an execution, every processor p ∈ V \{r} produces at most 2∆ + n topological changes in forest F.

Proof. This comes from Lemmas 24 and 25. 2

Corollary 7 From any configuration, Algorithm 2 produces at most 2∆n + n 2 topological changes in forest F.

Lemma 27

In an execution, each topological change in forest F generates at most ∆ requests.

Proof. Let any processor p ∈ V which produces a topological change in forest F. By Definition 8, we must consider two cases: p.S = E (in this case p = r) or p.S = C ∧ (∃q ∈ N eig p , q.Lp.L > 1). If p.S = E then we can have p.S = E ⇒ GP -REP (q) at a neighbor q of p, so since a processor can have at most ∆ neighbors this can generate at most ∆ requests. Otherwise we have p.S = C ∧ (∃q ∈ N eig p , q.Lp.L > 1) at p, then p sends a request in order to allow each neighbor q such that q.Lp.L > 1 to hook on to p. Therefore, at most ∆ requests are generated by a topological change at p. 2

Lemma 28 From any configuration, Algorithm 2 produces at most 2∆m + mn requests to reach a configuration satisfying Definition 4.

Proof. This comes from Corollary 7 and Lemma 27. Proof. By Corollary 7, from any configuration Algorithm 2 generates at most 2∆n+n 2 topological changes to reach a configuration satisfying Definition 4. Thus, by Definition 8 this implies that E-action and C-action are executed at most ∆n + n 2 times. Moreover, by Corollary 8 from any configuration A-action and O-action are executed at most 2∆m + mn times to send a local request. According to Corollary 3, an acknowledgement to a request is received in at most O(n 3 ) steps. Therefore, from any configuration in at most O(∆mn 3 + mn 4 ) steps a legitimate configuration is reached. 2

Conclusion

In this paper a silent snap-stabilizing algorithm resolving the Question-Answer problem has been given, in which each node requests a permission (delivered by a subset of network nodes) in order to perform a defined computation. Based on this first algorithm, a silent snap-stabilizing algorithm for the construction of a Breadth First Search tree has been presented. The complexity of this algorithm in terms of rounds is O(D 2 ) and in terms of steps is O(mn 4 ), with D the diameter, m the number of edges and n the number of nodes in the network. Moreover, a distributed daemon without any fairness assumptions is considered. To our knowledge, since in general the diameter of a network is much smaller than the number of nodes, the presented BFS construction algorithm gets the best compromise of the literature between the complexities in terms of rounds and in terms of steps.

  )] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  Actions: QE-action :: Error(p) → p.Q := A; p.P Q := P riority(p); QR-action :: Request(p) → p.Q := R; p.P Q := P riority(p); p.Req = W AIT ; QRC-action :: RequestT (p) → p.Q := R; p.P Q := (Chp).P Q; if p.P Q > P riority(p) ∧ p.Req = W AIT then p.Req := ASK; fi QW -action :: W aitR(p) → p.Q := W ; QA-action :: AnswerR(p) → p.Q := A; if p.Req = W AIT then p.Req := REP ; fi Algorithm for p such that ¬Allowed(p):

[

  TC1] Algorithm A BFS reaches a set of terminal configurations T ⊆ C in finite time, and [TC2] Every configuration γ ∈ T satisfies Definition 4.

Algorithm 2

 2 Spanning Tree Construction for any p ∈ V Inputs: N eigp: set of (locally) ordered neighbors of p; Shared variable: p.Req ∈ {ASK, W AIT, REP, OU T }; . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Macros: Child(p) = {q ∈ N eigp :: q.P = p ∧ q.L = p.L + 1} P arent(p) = p.P P riority(p) = -p.L ChP ar(p) = {q ∈ N eigp\Child(p) :: q.S = C} M inChP ar(p) = min{q ∈ ChP ar(p) :: ∀t ∈ ChP ar(p), q.L ≤ t.L} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Global Predicates: GoodT (p) ≡ p.S = E ∧ (p = r ⇒ p.L = (p.P ).L + 1) GoodL(p) ≡ (∀q ∈ N eigp :: |p.Lq.L| > 1 ⇒ (p.L < q.L ∨ q.S = E)) GP -REP (p) ≡ (∃q ∈ N eigp :: q.S = E ∨ q.Lp.L > 1) Start(p) ≡ p.Req = OU T ∧ GP -REP (p) End(p) ≡ p.Req = REP ∧ ¬GP -REP (p) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Algorithm for p = r: Constants: p.S = C; p.P = ⊥; p.L = 0; Predicates: Allowed(p) ≡ true Actions: A-action :: Start(p) → p.Req := ASK; O-action :: End(p) → p.Req := OU T ; Algorithm for p = r: Variables: p.S ∈ {C, E}; p.P ∈ N eigp; p.L ∈ N; Predicates: Allowed(p) ≡ f alse AbnormalT ree(p) ≡ p.S = C ∧ ((p.P ).S = E ∨ (p.P ).L ≥ p.L) Connect(p) ≡ (∃q ∈ N eigp :: q.Req = REP ∧ q = M inChP ar(p) ∧ (p.S = C ⇒ p.Lq.L > 1)) Actions: E-action :: AbnormalT ree(p) → p.S := E; C-action :: Connect(p) → p.S := C; p.P := M inChP ar(p); p.L := (p.P ).L + 1; p.Req := OU T ; A-action :: Start(p) → p.Req := ASK; O-action :: End(p) → p.Req := OU T ;

Definition 7 (

 7 Locally healthy processor) Let a tree T ∈ F. A processor p ∈ T is called locally healthy if p satisfies the following predicate: p.S = C ∧ p.L = (p.P ).L + 1 ∧ ¬GP -REP (p).

4. 2 . 2

 22 Proof assuming a weakly fair daemon Theorem 3 Let the set of configurations B ⊆ C such that every configuration γ ∈ B satisfies Definition 4. ∀γ ∈ (C -B), ∃p ∈ V such that p is enabled in γ.

2 Theorem 3 andTheorem 4 4 . 2 . 3 Proof assuming an unfair daemon Definition 8 (

 2344238 19 and Corollary 5, from any configuration Algorithm BFS reaches a configuration γ ∈ C in finite time and γ is a terminal configuration, which verifies Property [TC1] of Specification 2. Moreover, according to Lemma 19 the terminal configuration γ reached by Algorithm BFS satisfies Definition 4, which verifies Property [TC2] of Specification 2. Lemma 21 imply the following theorem. Algorithm BFS is snap-stabilizing for Specification 2 under a weakly fair daemon. Topological change) Given a forest F of trees in a configuration γ ∈ C. A topological change in F is obtained by the execution of one of the following actions at a processor p ∈ V in step γ → γ ′ : p executes E-action, or p executes C-action.

2 Corollary 8 Lemma 29

 2829 In an execution, A-action and O-action are executed at most 2∆m + mn times in the network. From any configuration, at most O(∆mn 3 + mn 4 ) steps are needed by Algorithm BFS to reach a configuration satisfying Definition 4.

  Shared variable: p.Req ∈ {ASK, W AIT, REP, OU T }; Variables: p.Q ∈ {R, W, A}; p.P Q ∈ Z; . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	Macros:
	RC(p)
	Global Predicates:
	T ransmit(p)

Algorithm 1 Question-Answer algorithm for any p ∈ V Inputs: N eigp: set of (locally) ordered neighbors of p; Child(p): set of neighbors considered as children of p in the tree; Allowed(p): predicate which indicates if p is able to acknowledge to a request; P arent(p): parent of p in the tree, equal to a processor q ∈ N eigp if ¬Allowed(p) or equal to ⊥ otherwise ; P riority(p): priority of p's local request; = {q ∈ Child(p) :: q.Q ∈ {R, W }} P rioRC(p) = {q ∈ RC(p) :: ∀t ∈ RC(p), q.P Q ≥ t.P Q} Chp = min{q ∈ P rioRC(p)}

  Allowed(p) then P arent(p) = ⊥) and P riority(p) is the priority (defined by Algorithm A) of the request that p has to send to the root of its tree.

	in the tree (if p satisfies
			if p.P Q > P riority(p) ∧ p.Req = W AIT then p.Req := ASK; fi
	QW -action	:: W ait(p)	→ p.Q := W ;
	QA-action	:: Answer(p)	→ p.Q := A;
			if p.Req = W AIT then p.Req := REP ; fi

).P Q = p.P Q Actions: QE-action :: Error(p) → p.Q := A; p.P Q := P riority(p); QR-action :: Request(p) → p.Q := R; p.P Q := P riority(p); p.Req = W AIT ; QRC-action :: RequestT (p) → p.Q := R; p.P Q := (Chp).P Q;

2 Proof of Question-Answer algorithm 3.2.1 Definitions Definition 1 (Path) The

  sequence of processors P(x, y) =< p 0 = x, p 1 , . . . , p k = y > is called a path if ∀i, 1 ≤ i ≤ k, P arent(p i ) = p i-1 .The processors p 0 and p k are termed as the extremities of P. The length of P is noted |P| = k.

	This action has the highest
	priority among the actions at p, and it reinitiates p's state like if an acknowledgement to a local request
	was received (without changing the state of the shared variable p.Req), i.e., to set p.Q to A and p.P Q
	to P riority(p).
	3.

Definition 3 (Request priority) Given

  a tree T in forest F and k processors in T sending a request. Let R = {R p 1 , . . . , R p k } be the set of requests sent by processors p i , 1 ≤ i ≤ k, in T . A request R p i has a higher priority than request R p j , 1 ≤ i, j ≤ k, if P riority(p i ) > P riority(p j ) with P riority(p) be the priority given in input of Algorithm 1 at processor p. A request R p

i sent (or transmitted) by a processor p ∈ T is of highest priority in the neighborhood of p if ∀q ∈ N eig p \{P arent(p)} the request R p j sent (or transmitted) by q we have P riority(p j ) < P riority(p i ).

Lemma 17 Let a normal tree T in a static forest F and a processor p ∈ T at height k with a local request. From any configuration, in at most O(k 2 ) rounds the request of p is transmitted to root(T ).

Proof. We show by induction the following proposition: For any node p ∈ T at height j ≥ 0 in T such that p.Req = W AIT , in at most O(j 2 ) rounds we have ∀q ∈ P(root(T ), p), q.Q = R ∧ q.P Q = P riority(p). In the base case j = 0 and we consider p = root(T ). According to Lemma 8, in at most j + 1 = 1 round we have p.Q = R ∧ p.P Q = P riority(p), which verifies the proposition. Induction case: We assume that for j = k -1 after O(j 2 ) rounds for each node p ∈ T at height k -1 in T such that p.Req = W AIT we have ∀q ∈ P(root(T ), p), q.Q = R and q.P Q = P riority(p). Consider any node p ∈ T of height j + 1 in T . We have to show that in at most O((j + 1) 2 ) rounds we have ∀q ∈ P(root(T ), p), (P riority(q) ≤ j + 1 ⇒ (q.Q = R ∧ q.P Q = P riority(p))). According to Lemmas 9 and 10, in at most O(j) additional rounds we have x.Req = REP and x.Q = A at each node x of height j in T (in particular at node x = p.P ). According to Lemma 8, in at most j + 1 additional rounds we have ∀q ∈ P(root(T ), p), (P riority(q) ≤ j + 1 ⇒ (q.Q = R ∧ q.P Q = P riority(p))). Thus, in at most j 2 + (j -1) + (j + 1) < O(j 2 ) rounds we have ∀q ∈ P(root(T ), p), (P riority(q) ≤ j + 1 ⇒ (q.Q = R ∧ q.P Q = P riority(p))), and the proposition is verified at p on height j + 1 in T . 2 Lemma 18 Let a normal tree T in a static forest F and a processor p ∈ T at height k with a local request. From any configuration, in at most O(k 2 ) rounds p receives an acknowledgement to its local request.

Proof. Let a processor p ∈ T such that p.Req = ASK of height k in T . According to Lemma 17, from any configuration in at most O(k 2 ) rounds we have ∀q ∈ P(root(T ), p), q.Q = R ∧ q.P Q = P riority(p). Thus, we can apply Lemma 10 and in at most k + 1 additional rounds we have p.Req = REP ∧ p.Q = A ∧ p.P Q = P riority(p) at p.

Proof.

Note that by definition of Predicate Allowed(p) ≡ (p = r) and according to Property [Safety 2] of Specification 1, only the nodes sending a request in the tree rooted at r can receive an acknowledgement to a request. Moreover, we have the following constant values at r: r.S = C, r.P = ⊥, and r.L = 0.

We first show by induction on the distance of the network the following proposition: in at most O(j 2 ) rounds, ∀p ∈ V, (d G (r, p) ≤ j ⇒ (p ∈ T ree(r) ∧ (∀q ∈ N eig p , q ∈ T ree(r) ∧ q.Lp.L ≤ 1))).

In base case j = 0. We have first that r ∈ T ree(r). To verify the proposition at r, we must consider any neighbor q of r in the network such that r = M inChP ar(q).

• First consider that q ∈ T ree(r), q ∈ T . Either case (A) d G (root(T ), q) ≤ j then according to Lemma 16 in at most O(1) rounds q has detected it is in an abnormal tree, thus we have (q.S = E ⇒ GP -REP (r)). In this case, E-action is not enabled at q and according to Property [Liveness 2] of Specification 1 and to Lemma 18 in at most O(j 2 ) = O(1 2 ) rounds we have r.Req = REP at r. Thus, q can execute C-action, so in O(1) additional rounds we have q.S = C, q.P = r, and q.L = 1 at q. Or case (B) d G (root(T ), q) > j, we must consider two subcases: (B1) d G (root(T ), q) = j + 1 = 2 or (B2) d G (root(T ), q) > 2.

-In the subcase (B1), d G (root(T ), q) = 2. According to Lemma 16 in at most j + 1 = O(1) rounds q.P has detected it is in an abnormal tree T and we have (q.P ).S = E, thus q can execute E-action and in O(1) additional rounds we have q.S = E leading to the case (A).

-In the subcase (B2), d G (root(T ), q) > 2. E-action is not enabled at q and d G (root(T ), q) > 2 ⇒ q.Lr.L > 1. Thus, according to Property [Liveness 2] of Specification 1 and to Lemma 18 in at most O(j 2 ) = O(1 2 ) rounds we have r.Req = REP at r. Then, C-action is the enabled action with the highest priority at q and in O(1) additional rounds it is executed by q to obtain q.S = C, q.P = r, and q.L = 1.

• Otherwise, consider that q ∈ T ree(r) then we have q.S = C and E-action is not enabled at q. We must consider the case such that q.Lr.L > 1 at q. We have (q.Lr.L > 1 ⇒ GP -REP (r)) and according to Property [Liveness 2] of Specification 1 and to Lemma 18 in at most O(j 2 ) = O(1 2 ) rounds we have r.Req = REP at r. So q can execute C-action and in O(1) additional rounds we have q.S = C, q.P = r, and q.L = 1 at q.

Therefore, since the daemon is weakly fair in at most O(1) rounds for every neighbor q of r the parent of q is r (i.e., q ∈ T ree(r)) and q.Lr.L ≤ 1, which verifies the proposition. Induction case: We assume the proposition is verified for every node at distance j -1 from r in the network. We have to show the proposition is also verified for every node at distance j from r. Consider any node p at distance j from r. By induction hypothesis, we have p ∈ T ree(r). Let any node q ∈ N eig p such that p = M inChP ar(q).

• First consider that q ∈ T ree(r), q ∈ T . Either case (A) d G (root(T ), q) ≤ j, then according to Lemma 16 in at most j + 1 rounds q has detected it is in an abnormal tree T and we have (q.S = E ⇒ GP -REP (p)). In this case, E-action is not enabled at q and according to Property [Liveness 2] of Specification 1 and to Lemma 18 in at most O(j 2 ) rounds we have p.Req = REP at p. Thus, q can execute C-action, so in O(1) additional rounds we have q.S = C, q.P = p, and q.L = p.L + 1 at q. Or case (B) d G (root(T ), q) > j, we must consider two subcases: (B1)

-In the subcase (B1), d G (root(T ), q) = j + 1. According to Lemma 16 in at most j + 1 rounds q.P has detected it is in an abnormal tree T and we have (q.P ).S = E, thus q can execute E-action and in O(1) additional rounds we have q.S = E leading to the case (A).

-In the subcase (B2), d G (root(T ), q) > j+1. E-action is not enabled at q and d G (root(T ), q) > j + 1 ⇒ q.Lp.L > 1. Thus, according to Property [Liveness 2] of Specification 1 and to Lemma 18 in at most O(j 2 ) rounds we have p.Req = REP at p. Then, C-action is the enabled action with the highest priority at q and in O(1) additional rounds it is executed by q to obtain q.S = C, q.P = p, and q.L = p.L + 1.

• Otherwise, consider that q ∈ T ree(r) then we have q.S = C and E-action is not enabled at q. We must consider the case such that q.Lp.L > 1 at q. We have (q.Lp.L > 1 ⇒ GP -REP (p)) and according to Property [Liveness 2] of Specification 1 and to Lemma 18 in at most O(j 2 ) rounds we have p.Req = REP at p. So q can execute C-action and in O(1) additional rounds we have q.S = C, q.P = p, and q.L = p.L + 1 at q.

Therefore, since the daemon is weakly fair in at most O(j 2 ) rounds for every neighbor q of p we have q ∈ T ree(r) and q.Lp.L ≤ 1, which verifies the proposition. Note that, at distance j from r when the proposition is verified for any processor p ∈ T ree(r) then p can execute O-action. So, since the daemon is weakly fair in at most O(j 2 ) rounds we have ∀p ∈ V, (d G (r, p) ≤ j ⇒ (p ∈ T ree(r) ∧ p.Req = OU T ).

We now show that the configuration γ reached by Algorithm BFS in O(D 2 ) rounds verifies Definition 4. Let D the diameter of the network G. In the proof above, any processor p ∈ V at distance D from r belongs to the subgraph T ree(r) in at most O(D 2 ) rounds, otherwise G is not a connected network. Moreover, there is a path between any processor p ∈ V and r in T ree(r), so the subgraph