Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Revisited Convergence of Dolev et al BFS Spanning Tree Algorithm

Karine Altisen, Marius Bozga

TL;DR

The paper tackles the convergence of Dolev et al's BFS spanning tree algorithm under the most general execution model with an unfair daemon. It introduces a novel, constructive convergence proof built around a carefully designed potential function and a structured decomposition of steps, all formalized and certified in the PADEC Coq framework. The authors report a substantial Coq development (about $5{,}155$ lines) and demonstrate that the approach yields a sound constructive termination argument even with unbounded variables. This work not only validates the algorithm under broad conditions but also showcases PADEC's capability to handle complex distributed proofs, with implications for future complexity analyses of self-stabilizing algorithms.

Abstract

We provide a constructive proof for the convergence of Dolev et al's BFS spanning tree algorithm running under the general assumption of an unfair daemon. Already known proofs of this algorithm are either using non-constructive principles (e.g., proofs by contradiction) or are restricted to less general execution daemons (e.g., weakly fair). In this work, we address these limitations by defining the well-founded orders and potential functions ensuring convergence in the general case. The proof has been fully formalized in PADEC, a Coq-based framework for certification of self-stabilization algorithm.

Revisited Convergence of Dolev et al BFS Spanning Tree Algorithm

TL;DR

The paper tackles the convergence of Dolev et al's BFS spanning tree algorithm under the most general execution model with an unfair daemon. It introduces a novel, constructive convergence proof built around a carefully designed potential function and a structured decomposition of steps, all formalized and certified in the PADEC Coq framework. The authors report a substantial Coq development (about lines) and demonstrate that the approach yields a sound constructive termination argument even with unbounded variables. This work not only validates the algorithm under broad conditions but also showcases PADEC's capability to handle complex distributed proofs, with implications for future complexity analyses of self-stabilizing algorithms.

Abstract

We provide a constructive proof for the convergence of Dolev et al's BFS spanning tree algorithm running under the general assumption of an unfair daemon. Already known proofs of this algorithm are either using non-constructive principles (e.g., proofs by contradiction) or are restricted to less general execution daemons (e.g., weakly fair). In this work, we address these limitations by defining the well-founded orders and potential functions ensuring convergence in the general case. The proof has been fully formalized in PADEC, a Coq-based framework for certification of self-stabilization algorithm.

Paper Structure

This paper contains 13 sections, 9 theorems, 10 equations, 2 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Contributions
  4. Coq Development.
  5. Organization.
  6. Dolev et al's BFS Spanning Tree Algorithm
  7. The PADEC Framework
  8. Overview of the Proof
  9. A Decreasing Potential Function for $d$-steps
  10. Bounds on Distance Values
  11. Smooth and Non-smooth $d$-steps
  12. Potential Function and Proof of Proposition \ref{['prop:dstep-potential']}
  13. Conclusion

Key Result

proposition thmcounterproposition

Let $R_1, R_2$ be relations, $x$ an element. Assume that (1) $R_2$ is well-founded and (2) there exist a set $B_1$ and relations $R_1'$ well-founded, $E_1$ transitive such that We can conclude that $(\mathsf{Acc}~ (R_1 \cup R_2)~ x)$ holds.

Figures (2)

  • Figure 1: Smooth and non-smooth steps
  • Figure 2: Possible evolutions of a non-smooth edge $e^*=(p,q)$ with minimal rank $k^*$: (i) only $p$ executes, (ii) only $q$ executes (iii) $p$ and $q$ executes

Theorems & Definitions (16)

  • proposition thmcounterproposition
  • proof
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • theorem thmcountertheorem
  • proof
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • ...and 6 more