# Outils d'analyse d'algorithmes distribués spécifiés dans le modèle à états

Erwan Jahier, Karine Altisen, Stéphane Devismes

► To cite this version:

Erwan Jahier, Karine Altisen, Stéphane Devismes. Outils d'analyse d'algorithmes distribués spécifiés dans le modèle à états. ALGOTEL 2025 – 27èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications, Jun 2025, Saint Valéry-sur-Somme, France. hal-05012468

HAL Id: hal-05012468

https://hal.science/hal-05012468v1

Submitted on 31 Mar 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

Public Domain
# Outils d'analyse d'algorithmes distribués spécifiés dans le modèle à états†

Erwan Jahier¹ et Karine Altisen¹ et Stéphane Devismes²

¹Université Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, France

²Université de Picardie Jules Verne, MIS, France

## 1 Introduction

Les algorithmes distribués, bien que difficiles à concevoir et à analyser, sont généralement étudiés sans outillage. Leur nature combinatoire (notamment due à l'exécution concurrente et asynchrone des nœuds du réseau) rend pourtant très difficile la prise en compte de tous les scénarios possibles. Ainsi, faire de la simulation ou de la vérification peut être d'une grande aide. C'est pourquoi nous proposons une suite d'outils permettant de simuler (SASA) et vérifier (SALUT) formellement des algorithmes distribués. Cet article est une synthèse de nos publications faites sur ce sujet [1, 2, 2, 11, 12].

Ces outils ont été conçus pour analyser des algorithmes spécifiés dans un modèle introduit par Dijks-tra [5] pour l'étude des algorithmes autostabilisants. Ce modèle, dit à états, est suffisamment abstrait pour permettre des simulations et des vérifications efficaces, et général pour encoder toutes sortes d'algorithmes.

La section 2 présente succinctement le modèle à états à partir d'un exemple d'algorithmme distribué autostabilisant qui servira de fil rouge. La section 3 explique comment nous traitons les topologies. Les sections 4 et 5 présentent comment faire des simulations interactives, et des campagnes de simulations par lots. La section 6 présente des méthodes et outils d'études de pire cas de temps de convergence. La section 7 montre comment vérifier formellement de tels algorithmes par model-checking.

## 2 Synchronisation d'horloges dans le modèle à états

Nous présentons le modèle à états [5] à partir d'un exemple d'algorithmme simple qui vise à synchroniser des horloges dans un réseau. Cet algorithmme nous servira par la suite pour illustrer l'utilisation de nos outils.

Dans le modèle à états, le réseau est représenté par un *graphe* dont chaque nœud héberge un programme (appelé *algorithme local*) qui peut lire son état ainsi que celui de ses voisins, mais ne peut modifier que le sien. L'ensemble des programmes forme un *algorithme distribué* qui s'exécute en étapes atomiques. Chaque algorithme local est décrit sous la forme d'actions gardées : quand une garde (une expression Booléenne portant sur les états lus) est vraie, le nœud est dit *activable*; dans ce cas l'action correspondante est susceptible d'être exécutée pour modifier son état. Une entité externe, nommée *démon*, choisit d'activer au moins un des nœuds activables à chaque étape, ce qui modélise l'asynchronisme du réseau.

L'algorithme d'unisson synchrone utilisé comme fil rouge est paramétré par un entier naturel *m* et suppose un réseau bidirectionnel connexe quelconque. Tous les nœuds du réseau exécutent le même *algorithme local*, celui de la figure 1. Chaque nœud possède un état formé d'une unique variable entière, l'horloge, prenant ses valeurs dans l'intervalle $[0, m - 1]$. La garde de l'unique action de cet algorithme est vraie si et seulement si la valeur de son horloge est différente de celle calculée par la macro *NewClockValue*. Cette macro calcule le minimum des valeurs d'horloges dans le voisinage clos du nœud (c'est-à-dire, le nœud et ses voisins), l'incrémente, puis en calcule la valeur modulo *m*.

L'intérêt de cet algorithme est que l'on peut montrer [1] que si le démon active à chaque étape tous les nœuds activables (on parle dans ce cas de *démon synchrone*), alors au bout d'un nombre fini d'étapes (borné par $3D - 1$, où *D* est le diamètre du graphe), toutes les horloges sont synchronisées à la même valeur.

<footnote>†Ce travail a été soutenu par les projets ANR SkyData (ANR-22-CE25-0008) et PaVeDyS (ANR-23-CE48-0005).</footnote>
**Entrées :** $m$ : un entier, $m \ge \max\{2, 2\mathcal{D} - 1\}$

$p.N$ : l'ensemble des voisins de $p$

**Variables :** $p.clock \in [0, m-1]$ : l'horloge de $p$

**Macro :** NewClockValue($p$) = (min($\{q.clock : q \in p.N\} \cup \{p.clock\}$) + 1) mod $m$

**Action :** Incr :: $p.clock \neq NewClockValue(p) \leftarrow p.clock \leftarrow NewClockValue(p)$

<caption>FIGURE 1 : L'algorithme local pour l'unisson synchronise [1]</caption>

## 3 Topologies

Les outils que nous présentons dans la suite fonctionnent à partir d'une topologie fixe, donnée sous la forme d'un graphe au format DOT [7]. Une convention de nommage (d'attributs DOT) nous permet de définir les divers paramètres de l'algorithme, et en particulier d'associer à chaque nœuds du graphe son algorithme local [8]. Un exemple est donné en annexe A. Notre suite d'outils comporte également un générateur de topologies [9] qui permet d'obtenir diverses sortes de graphes : des anneaux, des lignes, des grilles, des étoiles, des cliques, des arbres, ainsi que diverses sortes de graphes aléatoires (Erdős-Rényi, Barabási-Albert, disque unitaire). La gauche de la figure 2 montre la visualisation d'un graphe généré aléatoirement.

<figure><img src="image_1.png" /><figcaption>FIGURE 2 : Une copie d'écran d'une session de simulation interactive de l'unisson synchronise.</figcaption></figure>

## 4 Simulations interactives

À partir d'un graphe décrit au format DOT, et d'un encodage de l'algorithme en OCAML ou en LUSTRE (l'encodage de la figure 1 est donnée en annexe B), nos outils permettent à l'utilisateur de faire des simulations interactives étape par étape, ou bien ronde à ronde,‡ en se déplaçant en avant ou en arrière, tout en visualisant l'ensemble des états des nœuds, ainsi que leur statut (activable, activé). L'utilisateur peut choisir d'utiliser l'un des 4 démons prédéfinis dans l'outil : le démon synchronisé ; le démon distribué, qui active au moins un nœud activable ; le démon central, qui active un seul nœud activable ; et le démon localement central, qui est un démon distribué qui n'active jamais 2 nœuds voisins. L'utilisateur peut également choisir lui-même quels nœuds activer. L'utilisation de ce simulateur interactif est illustré en figure 2, qui montre sur sa partie gauche une visualisation de la topologie, décorée avec la valeur des états et où les nœuds activables sont en vert ; la partie droite montre le panneau de commandes interactives, qui permet, entre autres, de choisir le démon, ou de naviguer en avant ou en arrière dans la simulation.

<footnote>‡. La première ronde d'une exécution se termine dès lors que tous les nœuds étaient initialement activables ont soit exécuté une règle, soit été rendus inactivables. La seconde ronde commence à la fin de la première, etc. Ainsi, pour un démon synchronisé, une étape correspond à une ronde. Pour plus d'informations, voir les publications relatives à SASA [3] et les tutoriaux en ligne [9].</footnote>
# 5 Campagne de simulations par lots

Nos outils permettent également de faire des campagnes de simulations par lots [3]. Cela peut être très utile pour étudier expérimentalement le comportement asymptotique des algorithmes, en particulier leurs temps de convergence vers une configuration § légitime, à partir de laquelle la spécification du problème est satisfaite. En phase de conception, cela peut donner des indications sur la forme algébrique d'une éventuelle borne. Et quand une borne est connue, ces simulations permettent de vérifier en pratique, en fonction du type de topologie, ou du type de démon, si ces bornes sont atteintes ou très pessimistes. Une borne connue peut également servir d'oracle à des tests qui vérifient la correction des algorithmes, ou de leurs encodages.

<figure><img src="image_2.png" /><figcaption>FIGURE 3 : Résultats d'une campagne de simulations sur l'algorithme d'unisson synchrone</figcaption></figure>

La figure 3 visualise les données générées par une campagne de simulations effectuée sur l'algorithme de la figure 1, et permet d'observer l'évolution des temps de convergence quand la taille de la topologie augmente. Nous avons généré 10 topologies de différentes tailles (de 3 à 1089), et de 4 types (anneau, clique, grille, et aléatoire de type Erdős-Rényi – *er*), et nous avons mesuré le nombre d'étapes (à gauche), de mouvements ¶ (au milieu), et de rondes (à droite). Chaque expérience a été faite plusieurs fois (jusqu'à ce que la taille relative de l'intervalle de confiance soit assez petite), en faisant juste varier la configuration initiale. La figure représente les valeurs minimales, maximales, et moyennes obtenues. L'annexe C contient le code qui a permis de générer ces toutes données. Nous pouvons observer (sans surprise) que cet algorithme converge plus lentement sur des anneaux que sur des cliques. Plus de détails sur comment de telles campagnes de simulations peuvent être mises en place sont disponibles dans les tutoriaux en ligne [9].

# 6 Exploration des pires cas

Hormis les topologies aléatoires, le non-déterminisme dans les simulations de la figure 3 ne provient que d'une source¹: la valeur de l'état initial. Pour rechercher des états initiaux menant à des pires temps de convergence, des techniques de recherches locales, où l'on fait varier l'état initial dans les directions qui maximisent le temps de convergence, donnent parfois de bons résultats [11].

Pour l'unisson synchrone, le seul démon valide est le démon synchrone, qui est déterministe. Cependant, il existe plusieurs démons non-déterministes, tels que le démon central. Par ailleurs, ce dernier permet pour la plupart des algorithmes d'obtenir les pires temps de convergence en étapes. Ainsi, pour cette source de non-déterminisme, nous avons également conçu et implémenté une heuristique qui permet d'obtenir plus rapidement ces pires cas. Cette heuristique exploite une fonction de potentiel (quand elle existe) qui mesure la distance d'une configuration à l'ensemble des configurations légitimes. Cela permet d'utiliser des techniques dites de *branch-and-bound*. De plus, en donnant priorité aux choix qui font le moins baisser la valeur du potentiel, on peut souvent accélérer la découverte du pire cas [11].

<footnote>§. Une configuration est formée par l'ensemble des états des nœuds.</footnote>

<footnote>¶. On appelle *mouvement* l'exécution d'une règle par un nœud.</footnote>

<footnote>II. Une autre source de non-déterminisme est due au démon, mais ce n'est pas le cas ici, car le démon est synchrone.</footnote>
# 7 Model-checking

Notre suite d'outils comporte également SALUT, un traducteur de DOT en LUSTRE [12], qui permet, une fois la spécification des algorithmes encodés en LUSTRE, de faire de la vérification formelle par model-checking, en utilisant LESAR [14] ou KIND2 [4].

La vérification est donc effectuée pour une topologie particulière. Cette approche peut-être vue comme une façon de faire des simulations, pour laquelle à partir d'une topologie fixée, typiquement assez petite (entre 3 et 20 noeuds selon les algorithmes), tous les cas sont exhaustivement explorés. Pour peu que cette vérification puisse être menée sur des topologies de tailles raisonnables, les garanties sur la correction de l'algorithme sont grandes.

En cas d'erreur (dans l'algorithme, dans la propriété, ou dans leurs formalisations), un contre-exemple minimal est généré. Par exemple, si l'on essaye de montrer la correction d'unisson avec un démon distribué sur la topologie de la figure 2, le contre-exemple en une étape est instantanément généré : à partir d'une configuration initiale où tous les nœuds ont une horloge nulle (une configuration légitime), et où tous les nœuds sont activables, l'outil propose un scénario où tous les nœuds ne sont pas activés, ce qui mène en effet à une configuration où les horloges sont désynchronisées. Plus d'informations sur ce sujet sont disponibles dans les publications relatives à SASA [12] et dans les tutoriaux en ligne [9].

# 8 Conclusion

Nous avons présenté un aperçu de notre suite d'outils : celle-ci est basée sur des méthodes formelles et permet la simulation, le test, l'évaluation et la vérification d'algorithmes distribués, en particulier autostabilisants et définis dans le modèle à états introduit par Dijkstra [5]. L'ensemble des fonctionnalités de cette suite est fourni dans la figure 4.

<figure><img src="image_3.png" /><figcaption>FIGURE 4 : Résumé des fonctionnalités de la suite d'outils SASA</figcaption></figure>

Nous avons, lors de la conception de ces outils, fait le choix, dans la mesure du possible, de tirer partie d'outils existants, en les adaptant aux particularités des algorithmes distribués. En particulier, nous avons choisi de ne pas inventer de langage de description de topologies (nous utilisons DOT [7]) ou de définition d'algorithmes (nous utilisons les langages OCAML [15] ou LUSTRE [13]). La vérification formelle est également basée sur des outils existants [4]. Les outils de test et de simulation interactive sont basés sur des outils conçus à l'origine pour des programmes écrits dans des langages synchrones [10]; cela a été possible grâce à la proximité sémantique entre les langages de programmations synchrones et le modèle à états.
Références

[1] K. Altisen, S. Devismes, S. Dubois, and F. Petit. *Introduction to Distributed Self-Stabilizing Algorithms*, volume 8 of *Synthesis Lectures on Distributed Computing Theory*. Morgan & Claypool Publishers, 2019.

[2] K. Altisen, S. Devismes, and E. Jahier. SASA : A simulator of self-stabilizing algorithms. In *Tests and Proofs - 14th International Conference, TAP@STAF 2020, Bergen, Norway, June 22-23, 2020, Proceedings [postponed]*, volume 12165 of *Lecture Notes in Computer Science*, pages 143–154. Springer, 2020.

[3] K. Altisen, S. Devismes, and E. Jahier. sasa : a simulator of self-stabilizing algorithms. *Comput. J.*, 66(4):796–814, 2023.

[4] A. Champion, A. Mebsout, C. Sticksel, and C. Tinelli. The kind 2 model checker. In *CAV*, 2016.

[5] E. W. Dijkstra. Self-stabilizing systems in spite of distributed control. *Commun. ACM*, 1974.

[6] P. Erdös and A. Rényi. On random graphs. *Publicationes Mathematicae Debrecen*, 6:290–297, 1959.

[7] E. R. Gansner and S. C. North. An open graph visualization system and its applications to software engineering. *Softw. Pract. Exper.*, 30(11):1203–1233, 2000.

[8] E. Jahier. SASA : a Simulator of Self-stabilizing Algorithms. http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa.

[9] E. Jahier. Verimag Tools Tutorials : Tutorials related to SASA. https://www-verimag.imag.fr/vtt/tags/sasa/.

[10] E. Jahier. RDBG : a Reactive Programs Extensible Debugger. In *SCOPES*, 2016.

[11] E. Jahier, K. Altisen, and S. Devismes. Exploring worst cases of self-stabilizing algorithms using simulations. In *25th International Symposium on Stabilization, Safety, and Security of Distributed Systems*, Jersey City, New Jersey, USA, October 2023.

[12] E. Jahier, K. Altisen, S. Devismes, and G. B. Sant'Anna. Model Checking of Distributed Algorithms using Synchronous Programs. In *25th International Symposium on Stabilization, Safety, and Security of Distributed Systems*, New Jersey, United States, Oct 2023.

[13] E. Jahier, P. Raymond, and N. Halbwachs. *The Lustre V6 Reference Manual*, 2020.

[14] C. Ratel, Nicolas, and P. Raymond. Programming and verifying critical systems by means of the synchronous data-flow programming language Lustre. In *ACM-SIGSOFT*, page 112–119, 1991.

[15] The OCaml Development Team. *Ocaml*. https://ocaml.org/.
## A Un exemple de topologie au format DOT, avec les conventions de nommage (d'attributs) requises par notre suite d'outils

```DOT
// generated by:
// gg ER -n 8 -p 0.4 -o er8_unison.dot
// gg-deco "0::unison.ml" er8_unison.dot -o er8_unison.dot
graph er8_unison {
  graph [minDeg=2 meanDeg=2.75 maxDeg=3 is_connected=true is_cyclic=true
        is_tree=false links_number=11 is_rooted=false]
    p0 [algo="unison.ml"] p1 [algo="unison.ml"] p2 [algo="unison.ml"]
    p3 [algo="unison.ml"] p4 [algo="unison.ml"] p5 [algo="unison.ml"]
    p6 [algo="unison.ml"] p7 [algo="unison.ml"]
    p2 -- p1 p3 -- p0 p4 -- p0 p4 -- p1 p4 -- p3 p5 -- p0
    p6 -- p2 p6 -- p5 p7 -- p2 p7 -- p3 p7 -- p6
}
```

Ce fichier au format DOT, dont on peut voir une visualisation en figure 2, a été généré par l'outil présenté en section 3, en utilisant un algorithme de génération aléatoire de graphes [6]. Le fichier `unison.ml`, référencé ici comme un attribut de nœud, est celui de l'annexe B ci-dessous.

## B L'encodage en OCAML de l'algorithme de la figure 1

La seule chose demandée à l'utilisateur pour utiliser notre suite d'outils est d'encoder la garde (`enable_f`) et l'action (`step_f`) des commandes gardées décrivant l'algorithme. L'encodage en LUSTRE est de taille similaire.

```OCaml
open Algo
let m = State.m
let (init_state: int -> string -> 'v) = fun _ _ -> Random.int m
let new_clock_value n1 clock =
    let cl = List.map (fun n -> state n) n1 in
    let min_clock = List.fold_left min clock cl in
    (min_clock + 1) mod m
let (enable_f: 'v -> 'v neighbor list -> action list) =
    fun clock n1 ->
        if (new_clock_value n1 clock) <> clock then ["g"] else []
let (step_f : 'v -> 'v neighbor list -> action -> 'v) =
    fun clock n1 _ ->
        new_clock_value n1 clock
```

## C Le script ayant permis de générer la figure 3

Ce script, qui utilise des fonctions fournies dans la suite d'outils, a été adapté de celui décrit ici https://www-verimag.imag.fr/vtt/articles/comparing-randomized-coloring/.

```OCaml
#use "genExpeMakefiles.ml";
precision := 0.1;
max_simu_nb := 1000;
timeout_in_sec := 60;
let algos = ["../../test/unison"]
let daemons = ["-sd"]
let base_size = 3
let base_size_2 = base_size * base_size
let cliques = List.init 10 (fun n -> Clique (base_size_2*(n+2)*(n+2)))
let rings = List.init 10 (fun n -> Ring (base_size_2*(n+2)*(n+2)))
let grid = List.init 10 (fun n -> Grid (base_size*(n+2), base_size*(n+2)))
let er = List.init 10 (fun n -> ER (base_size_2*(n+2)*(n+2), 0.4))
let networks = (cliques@rings@er@grid)
let gen_make_rules () = gen_makefile "Makefile.expe-rules" daemons algos networks;
#use "parseLog.ml";
let gen_pdf () =
    let gl = ["clique"; "ring"; "er"; "grid"] in
    parse_log ["Unison", "unison"] gl daemons;
sh ("./gen_pdf_algotel.r nonreg")
```