Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability

We consider a distributed system of $n$ interconnected processes. The interconnection network is modeled by an undirected connected graph $G=(V,E)$ where $V$ is a set of vertices representing the processes and $E$ a set of edges representing bidirectional communication links between processes. The set of neighbors of a process $p$ will be denoted $N(p)$. Arora and al’s synchronous unison [4] is showcased in Algorithm 1. It is written in the atomic-state model, a locally shared memory model of computation where each node can directly read its state and those of its neighbors, but can only modify its own state.

Given an integer parameter $m$ common to all processes and called period, each process $p$ holds a single variable $p.c\in \{0,\mathrm{\dots },m-1\}$, which represents its clock. The state of a process is then its clock value. The configuration of the system is modeled by the vector associating each process with its state (its clock value). The set of possible configurations of the system is denoted by ${\mathrm{\Gamma }}_{n,m}={\{0,\mathrm{\dots },m-1\}}^n$. The local algorithm of each process $p$ is made of a single rule of the form $guard\mapsto action$. The guard of the rule of $p$ is a predicate on the state of $p$ and those of its neighbors. The action part modifies the state of $p$ and, in this case, is thus an assignment of the clock of $p$. In a given configuration, a process’s rule is said to be enabled if its guard is true. A configuration where no rule can be enabled is said to be terminal. The system is assumed to be synchronous: as long as the system is not in a terminal configuration, iterations are executed as follows. All processes whose rule can be enabled in the current configuration ${\gamma }_i$ simultaneously execute their rule’s action, thus generating a new configuration ${\gamma }_{i+1}$, and so on. An execution of the algorithm is therefore a sequence of configurations ${\gamma }_0,\mathrm{\dots },{\gamma }_i,\mathrm{\dots }$ such that for all $i>0$, ${\gamma }_i$ is obtained from ${\gamma }_{i-1}$ in one synchronous iteration of the algorithm.

The goal of the unison algorithm is to reach a configuration where all clocks are synchronized to an identical value. To this end, at each iteration, each process $p$ computes the minimum clock value $c_{\min }$ in its closed neighborhood (i.e., $N(p)\cup \{p\}$), and then modifies, if necessary, its clock $p.c$ to $(c_{\min }+1)modm$ (see Algorithm 1). Gradually, the smallest values propagate in the network. This progress can only be disturbed by the appearance of 0 at some processes after their entire closed neighborhood has reached the maximum value $m-1$. However, Arora et al. have shown that when $m$ is chosen sufficiently large (i.e., $m\ge \max (2.2𝒟-1)$ where $𝒟$ is the diameter of $G$), these local resets cannot prevent the system from converging: regardless of the initial configuration ${\gamma }_0$, there necessarily exists a value $t\ge 0$ such that all clocks have the same value in ${\gamma }_t$. Conversely, if $m$ is chosen too small, the execution may never converge. In this case, there exists a cycle between illegitimate configurations (i.e., configurations containing at least two different clock values).

Since the total number of possible configurations is $m^n$, if the system is still in an illegitimate configuration after $m^n-1$ iterations, we can claim that the execution will never converge. Thus, it is sufficient to observe the first $t_f=m^n$ configurations of an execution in order to decide whether the execution converges or diverges. This number is very large and can lead to exponential modeling. We can therefore choose a more reasonable value for $t_f$, even if it means not being able to decide in some cases.

In the previous example, a legitimate configuration, where the clocks are synchronized, is eventually reached by the algorithm. However, when $m$ is chosen too small, there may exist configurations from which the clocks never synchronize. In this case, we will say that the system diverges. The convergence and divergence properties, formally defined below, highlight the importance of studying the behavior of distributed algorithms, and particularly synchronous unison, according to their parameter values (in this case, the period)  [16, 20].

Our analysis will focus on the impact of graph topology and the period $m$ on synchronization. The following theorem provides an interesting general bound on the maximum number of iterations in a connected graph.

Finally, we stress out that we have carefully selected the synchronous unison as our case study with the goal of generalization to a broader class of distributed algorithms in mind. More precisely, we deal with the atomic-state model because it is the most commonly used model in the self-stabilizing literature and it is also close to other important models widely used in distributed computing, e.g., the local and congest models [29, 23]. The atomic-state model is a locally shared memory model so our approach can be straightforwardly generalized to handle algorithms working in systems where communication is made using communication registers. Furthermore, Synchronous Unison is representative of classical techniques used in self-stabilization. For example, the way clocks are updated follows the so-called “$min+1$” rule that is used in many self-stabilizing algorithms such as the Breadth-First Search (BFS) spanning tree construction [22] and the asynchronous version of the unison [16]. More generally, we believe that our guidelines to model the transition relations are very general while issues related to symmetries that we tackle in the paper are also pretty usual in self-stabilization.

Let $X$ be a set of propositional variables. A literal is a variable $x\in X$ or its negation $\overline{x}$. A clause is a disjunction of literals. A formula in Conjunctive Normal Form (CNF) is a conjunction of clauses. An assignment $I:X\to$ {True, False} associates each variable with a Boolean value and can be represented as a set of literals. A literal is satisfied by an assignment $I$ if $l\in I$, otherwise it is falsified by $I$. A clause is satisfied by an assignment $I$ if at least one of its literals is satisfied by $I$, otherwise it is falsified by $I$. A CNF formula is satisfiable if there exists an assignment that satisfies all its clauses, otherwise it is unsatisfiable. The satisfiability problem (SAT) thus consists in determining whether a given CNF formula is satisfiable. Although SAT is NP-complete[15], modern solvers based on the Conflict Driven Clause Learning (CDCL)[30] algorithm are efficient and can solve instances involving a large number of variables and clauses. Indeed, beyond clause learning and non-chronological backtracking, these solvers integrate powerful mechanisms such as lazy structures, dedicated branching heuristics, and restarts[10]. Moreover, the SAT problem is widely used to model and solve many complex combinatorial problems from various fields, notably in formal verification[14, 8], but also in cryptography, bioinformatics and planning, among many others [10].

Logic-based model checking has been a cornerstone in the formal verification of algorithms and systems. In particular, Bounded Model Checking (BMC) [7], which verifies whether a finite-state model satisfies a given specification within a bounded execution length, has gained significant traction over the past decade, especially when encoded as satisfiability (SAT) or satisfiability modulo theories (SMT) problems. Early efforts in the formal verification of distributed self-stabilizing algorithms were led by Lakhnech and Siegel [33, 27], who introduced theoretical frameworks for computer-aided verification, although no practical toolsets emerged from their work. Subsequent research explored symbolic BMC for distributed algorithms such as the work of Chen and Kulkarni who applied SMT-based BMC to assess the stabilization properties of distributed algorithms, particularly Dijkstra’s token ring, Ghosh’s Mutual Exclusion and a version tree-based mutual exclusion [13]. However, while SMT solvers offer expressive modeling capabilities, their higher-level abstraction can hinder fine-grained analysis and scalability. More recently, a SAT-based formal approach was proposed in [19] to detect Byzantine faults in synchronous systems with complete network topologies. This propositional encoding demonstrates the viability of SAT-based reasoning for distributed fault-tolerant systems and opens the door to more scalable and precise verification frameworks for self-stabilizing algorithms.

In the following sections, we thus focus on modeling the behavior of the synchronous unison algorithm, applied to an arbitrarily connected graph. The objective is to apply bounded model checking through SAT to characterize the conditions of convergence or divergence of the algorithm. This involves modeling the states of the processes using logical formulas, which must be expressed in such a way that they can be effectively solved by a SAT solver. Finally, we mention that previous literature introduces cardinality constraints having the form ${\sum }_i{l}_i=1$ where each $l_i$ is a literal, and which can be efficiently encoded into CNF form [32].

We recall that the network is modeled by an undirected connected graph $G=(V,E)$ where $V=\{0,\mathrm{\dots },n-1\}$ is a set of $n$ vertices representing the processes and $E$ is a set of edges representing bidirectional communication links between pairs of processes. $M=\{0,\mathrm{\dots },m-1\}$ denotes the set of possible clock values, where $m$ is the period. We are interested in the first $t_f$ configurations of any execution of the algorithm on $G$. The configurations will thus be indexed from 0 to $t_f-1$ and the set of indices will be denoted $T=\{0,\mathrm{\dots },t_f-1\}$. To model the execution of the algorithm, it is also necessary to reason on the state of the process clocks in the different configurations. To do this, we introduce the clock variables $h_{p,t,v}$, for all $(p,t,v)\in V\times T\times M$. Each variable $h_{p,t,v}$ will indicate whether the clock of process $p$ is equal to the value $v$ in configuration $t$. This is sufficient to model execution and detect convergence. However, modeling divergence requires other variables, in particular to represent the presence of a cycle between illegitimate configurations during execution and to simplify the transformation of constraints into conjunctive normal form. The set of variables we will use is detailed below:

• $\mathrm{■}$

  Clock variables: $h_{p,t,v}$ where $(p,t,v)\in V\times T\times M$. These variables are assigned to $True$ if process $p$ has clock value $v$ in configuration $t$, $False$ otherwise.

• $\mathrm{■}$

  Cycle variables: $c_t$ where $t\in T$. These variables are assigned to $True$ if the configuration $t\in T$ and the initial configuration are identical, i.e., if the clock value of each process is identical in both configurations.

• $\mathrm{■}$

  Clock-Similarity variables: $s_{p,t,v}$ where $(p,t,v)\in V\times T\times M$. These variables are assigned to True if process $p$ has the same clock value in configuration $t\in T$ and the initial configuration.

First, we focus on formalizing the constraints modeling a valid execution of synchronous unison. More specifically, we define clock uniqueness constraints as well as update rules ensuring the correct computation of clock values at each iteration.

Convergence occurs when the system has reached a legitimate configuration, where all clock values are identical. An algorithm is said to be convergent if, starting from any initial configuration, such a legitimate configuration is always reached within a finite number of iterations. To demonstrate this property, we will reason by contradiction by assuming that convergence is never reached from some initial configuration. In other words, there exists (at least) one initial configuration from which no legitimate configuration can be obtained. Since a legitimate configuration necessarily generates another legitimate configuration after an iteration of the algorithm, it suffices to show that the last configuration $t_f-1$ is illegitimate for some initial configuration. This property is thus translated by the following constraint:

Thus, it is clear that the CNF formula $\varphi$ obtained thanks to the constraints (1), (3), and (4) is unsatisfiable if and only if the synchronous unison algorithm converges. Indeed, if $\varphi$ is satisfiable, the provided model allows to exhibit an initial configuration ${\lambda }_0\in {\mathrm{\Gamma }}_{n,m}$ deduced from the clock variables $h_{p,0,v}$ which are set to true for $p\in V$ and $v\in M$, from which the algorithm does not converge. More specifically, in the valid execution of the unison algorithm from ${\lambda }_0$ (ensured by the constraints (1) and (3)), we exhibit, at the level of the last configuration ${\lambda }_{t_f-1}$ and for any possible clock value $v\in M$, a process $p\in V$ whose clock does not hold the value $v$ in ${\lambda }_{t_f-1}$ (ensured by constraint (4)). In terms of complexity, since constraint (4) requires only $O(m)$ clauses, our model for convergence requires only $O(n\times t_f\times m)$ variables with a number of clauses bounded by $O(n\ast t_f\ast m^{d_{\max }+1})$ where $d_{\max }$ is the maximum degree of the graph. We also note that the maximum clause size of the model is $\max (m,n+2)$.

Additionally, we can notice that constraint (4) can be further imposed on any subset of configurations in $T^{\prime }\subseteq T\setminus \{t_f-1\}$ as showcased in (5). Adding these redundant constraints does not alter the overall complexity of the model but may accelerate the detection of convergence. Specifically, these constraints can enable the solver to identify a valid configuration without requiring all necessary propagations to simulate the system execution until the final iteration from a given initial configuration. Consequently, if we consider the set $X=T\setminus \{t_f-1\}$, the model will ensure that the presence of a legitimate configuration is verified at each iteration of the algorithm whereas the set guarantees that this verification occurs every $m$ iterations, while necessarily including the initial configuration. We will thus refer to the following constraint as IC (for iterative convergence) and we denote $I{C}_{T^{\prime }}$ the constraint with the corresponding set $T^{\prime }\in \{P,X\}$.

Divergence implies the existence of two identical illegitimate configurations in the execution. Indeed, the set of legitimate configurations is trivially closed, and since the algorithm is synchronous and deterministic, such a cycle repeats itself infinitely. Let two configurations $(t_1,t_2)\in T$ such that , where the clock values of the processes at $t_2$ are identical to those at $t_1$. We will call such an occurrence a cycle at the level of configurations $(t_1,t_2)$. To establish the divergence, we must therefore model the existence of a cycle at the level of two possible illegitimate configurations reached by the algorithm. To simplify the modeling, we consider the existence of a cycle with respect to the initial configuration, i.e., $t_1=0$. Indeed, even if $t_1>0$, it is always possible to reduce the analysis to the initial configuration by taking the configuration in $t_1$ as the initial configuration of the system (n.b., a self-stabilizing algorithm must converge from any initial configuration). Furthermore, to ensure that the cycle configurations are illegitimate, it is sufficient to check that the initial configuration is illegitimate. We recall that the variables $c_t$ where $t\in T$, defined previously, represent the existence of a cycle at configuration $t$. Thus, the existence of a cycle between illegitimate configurations can be enforced by the following constraints:

Clearly, the constraint (6a) models the existence of a cycle $(0,t)$ where $t\in T$; while the constraint (6b) guarantees that configuration 0, and therefore the configurations of the cycle, are illegitimate. To establish the semantic meaning of the cycle variables, it is necessary to guarantee that, if these variables are set to true, then there is a cycle $(0,t)$, i.e., the clock values in configuration $t$ are identical to those in the initial configuration. In this context, the clock similarity variables $s_{p,t,v}$ where $(p,t,v)\in V\times T\times M$ can play the intermediate role of guaranteeing the same clock value in configuration $t\in T$ and the initial configuration. Thus, we add the following constraints:

The constraint (7a) thus ensures that the corresponding configuration $t\in T$ has the same clock values as configuration $0$ or, more formally, that $c_t\to {\bigwedge }_{p\in V}{\bigvee }_{v\in M}{s}_{p,t,v}$. The normal form presented in the constraint (7a) can be simply obtained by the clausal rewriting of the implication as well as the distributivity of disjunctions over logical conjunctions. The constraint (7b) is necessary to establish the semantic meaning of the variables $s_{p,t,v}$ which are set to $True$ when the process $p\in V$ has the same clock value $v\in V$ at configurations $0$ and $t$. More formally, we have $s_{p,t,v}\to h_{p,0,v}\wedge h_{p,t,v}$ and its normal form presented in the constraint (7b) can also be deduced by rewriting the implication and applying the distributivity of disjunction.

It is clear that the CNF formula $\psi$ obtained by the constraints (1), (3), (6) and (7) is satisfiable if and only if the unison algorithm diverges on the given input network with period $m$. Indeed, a model of $\psi$ allows to exhibit an initial configuration ${\lambda }_0\in {\mathrm{\Gamma }}_{n,m}$ from which a valid execution of the synchronous unison generates a cycle $(0,t)$ of illegitimate configurations, given by a cycle variable assigned to $True$ at the level of the clausal constraint (6a). Moreover, in terms of encoding complexity for divergence, it is clear that the constraints (6) and (7) introduce a bounded number of clauses in $O(n\times t_f\times m)$ and, consequently, the model has a complexity similar to the convergence case, mainly governed by the constraint (3), i.e., in $O(n\ast t_f\ast m^{d_{\max }+1})$ where $d_{\max }$ is the maximum degree of the graph. However, the model requires a larger number of variables, but which remains in $O(n\times t_f\times m)$.

In this section, we aim at reducing the number of initial configurations to be processed by removing redundant configurations. In other words, the goal is to eliminate configurations for which the algorithm’s behavior is identical to that of other configurations we already consider in the analysis. This approach optimizes the algorithm’s execution by avoiding processing situations that, although different in their representation, do not lead to different results.

We consider the following classical network topologies: chains, rings, and stars (see Figures 1, 2, and 5 respectively) [34]. The properties of the considered graphs and periods are summarized in Table 3. We encoded our models in Python using the PySAT library [25] ³³3Our code and benchmark are available in the following GitHub repository and solved these instances using the state-of-the-art solvers Cadical [9] and MapleSAT [28] ⁴⁴4For lack of space, we present the results with Cadical and we provide a comparison on the initial models of convergence and divergence in the appendix (refer to Tables 10, 9 and 8). Tests were performed on a machine equipped with an Intel Core i7 processor clocked at 3.80 GHz, running under Ubuntu 22.04. A timeout of 7200 seconds was set for each instance. We have generated the instances associated with all our models, totaling 4968 instances. For each type of topology among rings and chains, we took graph sizes $n$ ranging from $3$ to $20$ nodes, and we varied the period $m$ from $2$ to $20$. For the star topology, we took graph sizes $n$ ranging from $3$ to $10$ nodes, and we varied the period $m$ from $2$ to $10$. In particular, we generated 756 instances (342 for chains and rings and 72 for stars) for the initial model of convergence ($IN{I}_{CNV}$) which is described by the constraints (1), (3) and (4). Similarly we generated the same number of instances for the divergence model ($IN{I}_{DIV}$) described through the constraints (1), (3), (6) and (7).

Furthermore, for topologies where initial configuration elimination constraints can be applied, we also generate the corresponding instances. Thus, we generated 828 instances of convergence and divergence for ring and star topologies with the rotation elimination (RE) constraint. For the lexicographic order (LO) constraint, we generated 144 instances of convergence and divergence for the star topology. Moreover, we generated 756 instances of convergence for ring, chain, and star topologies for each constraint $I{C}_P$ and $I{C}_X$, added on top of the initial models. 414 instances of convergence were generated for ring and star topologies with each combinations $RE+I{C}_P$ and $RE+I{C}_X$. Finally, we generated 72 instances of convergence for star topology for each combination $LO+I{C}_P$ and $LO+I{C}_X$. The number of allowed configurations is set to $t_f=3𝒟$ for all topologies where $𝒟$ is the diameter of the considered graph. We also note that the Cardinality Network encoding [5] was used to rewrite constraint (1) in CNF form.

The results presented in Figures 3(a),  3(b), and 4 illustrate the behavior of the synchronous unison in terms of convergence and divergence on the different topologies (rings, chains, and stars) as a function of size $n$ and period $m$. For the studied graph topologies, we clearly notice that the results are coherent with Theorem 5 when $m\ge \max \{2,2𝒟-1\}$. revealing a convergence for the corresponding instances. Notably, the generated results demonstrate unison behavior on many instances across different topologies for which it was previously unknown. In particular, we were able to detect the convergence of the algorithm for the three topologies for values of . However, some instances remain unsolved, most likely due to the chosen upper limit on the number of allowed steps (i.e., $3𝒟$). It is also interesting to note that our results show that the bound proposed in the theorem 5 is tight in the case of stars. Indeed, this theorem states that convergence is guaranteed in stars (of diameter 2) from a period $m$ greater than or equal to 3 ($\max (2,2\times 2-1)=3$). Our results exhibit a case of divergence with $m=2$ in star graphs as shown in Figure 4, independently of their sizes. Thus, the synchronous unison algorithm converges in a star if and only if $m\ge 3$. We demonstrate this property in following proposition.

In this section, we analyze the performance of the models on the different topologies in terms of number of solved instances and average solving time per graph size. The results obtained for ring and star graphs are presented respectively in Tables 5 and 7, with respect to the graph sizes, the analyzed property, and the considered model. Due to the lack of space, the results obtained for chain graphs have been moved to the appendix (refer to Table 6). The results indicate that the initial model manages to solve most of the instances but it clearly encounters increasing difficulties with increasing graph sizes, particularly for the star and ring topologies. It thus manages to solve 329 (resp. 321) instances out of 342 for the convergence (resp. divergence) check on rings and 58 (resp. 59) instances out of 72 for the convergence (resp. divergence) check on stars. For chains, all instances were solved for convergence with the initial model whereas 328 out of 342 were solved for divergence. This behavior is not surprising especially for stars, since the star topology has a maximum degree $d_{\max }=n-1$, which leads to a combinatorial explosion in the number of clauses generated by the constraint (3). Indeed, it increases with a complexity of the order $O(n\times t_f\times m^n)$, which explains the model’s difficulty in handling larger instances. Figures 6 (resp. 7) illustrates the evolution of the solving time of instances generated for convergence (resp. divergence) verification for the initial model, as a function of graph size $n$ and period $m$, for ring, chain and star topologies. These curves highlight a progressive increase in resolution time as these two parameters increase. We observe in particular that, in the case of star graphs, this increase is much more pronounced for relatively smaller values of $n$ and $m$ compared to the other topologies. This trend, which remains similar both for convergence and divergence corroborates our previous observations and confirms the increased complexity of the model for topologies whose maximal node degree is high.

Next, we focus on comparing the initial convergence model (INI_CNV) with its counterparts augmented with the $IC$ constraint, specifically $I{C}_P$ and $I{C}_X$, across ring, star, and chain topologies. In the ring topology (Table 5), $I{C}_X$ consistently outperforms $I{C}_P$ and INI_CNV in larger instances, achieving the lowest solving times (-10,21% w.r.t INI_CNV) and highest number of solved instances (+3 w.r.t INI_CNV). For the star topology (Table 6), although convergence times are higher overall, $I{C}_X$ still shows better performance than $I{C}_P$ in mid-sized to larger instances. In the chain topology (Table 7), $I{C}_X$ also stands out as it achieves the lowest convergence times (-5,97% w.r.t $IN{I}_{CNV}$). Overall, $I{C}_X$ added on top of the initial model emerges as the most effective in convergence detection, balancing low solving times with a higher number of solved instances.

Finally, we study the formulations augmented by the constraints eliminating the initial configurations. As illustrated in Tables 5 and 6, the comparison with the initial models highlights the relevance of introducing these constraints, particularly for the divergence analysis. The results show a significant reduction in solving time for ring and star topologies thanks to rotation elimination (RE) and lexicographic order (LO), particularly when they are combined with Iterative Convergence (IC) constraints. More specifically, for ring graphs, the ER and IC_X combination model achieves the best overall performance, with an average solving time of 324.10s for convergence. For divergence, RE achieves better performance with respect to the initial model with an average solving time of 596.52s, across all graph sizes tested. Compared to the initial model, ER + IC_X thus reduces the total solving time by 10,5% with a higher number of solved instances (+4 w.r.t INI_CNV) for convergence and ER reduces it by 55,14% for divergence while solving 15 additional instance with respect to INI_DIV. These results demonstrate the positive impact of the symmetry-breaking constraints on the analysis of synchronous unison behavior. The star graph reveals a better dynamic with LO which demonstrates a significant improvement in the divergence time with an average of 15,80s, a reduction of 81.5% compared to the initial model (59,29s) with a higher number of solved instances (+1 w.r.t INI_DIV). On the other hand, LO + IC_P presents a significant reduction in solving time for convergence with a total of 215,23s, a reduction of 90,71% compared to the initial model (1631,35s) and a higher number of solved instances (+2 w.r.t INI_CNV). These observations are also confirmed by Table 6 and highlight the relevance of this optimization in structures where interactions are highly centralized around a central node.