Verification and Synthesis of Symmetric Uni-Rings for Leads-To Properties

TL;DR

This paper explores the verification and synthesis of symmetric uni-ring protocols satisfying leadsto properties, revealing undecidability in verification but decidability and polynomial-time synthesis methods for protocol generation.

Contribution

It establishes the undecidability of verification and introduces a decidable, polynomial-time synthesis approach for symmetric uni-ring protocols satisfying leadsto properties.

Findings

Verification of leadsto properties is undecidable.

Synthesis of protocols satisfying leadsto is decidable and efficient.

Synthesized protocols include agreement and parity protocols.

Abstract

This paper investigates the verification and synthesis of parameterized protocols that satisfy leadsto properties $R \leadsto Q$ on symmetric unidirectional rings (a.k.a. uni-rings) of deterministic and constant-space processes under no fairness and interleaving semantics, where $R$ and $Q$ are global state predicates. First, we show that verifying $R \leadsto Q$ for parameterized protocols on symmetric uni-rings is undecidable, even for deterministic and constant-space processes, and conjunctive state predicates. Then, we show that surprisingly synthesizing symmetric uni-ring protocols that satisfy $R \leadsto Q$ is actually decidable. We identify necessary and sufficient conditions for the decidability of synthesis based on which we devise a sound and complete polynomial-time algorithm that takes the predicates $R$ and $Q$, and automatically generates a parameterized protocol that satisfies $R \leadsto Q$ for unbounded (but finite) ring sizes. Moreover, we present some decidability results for cases where leadsto is required from multiple distinct $R$ predicates to different $Q$ predicates. To demonstrate the practicality of our synthesis method, we synthesize some parameterized protocols, including agreement and parity protocols.

Equations

$$((x_{i-1},x_i)\in \text{mboxPre}(\delta ))⟶x_i:=\delta (x_{i-1},x_i);$$

Full text

1 Introduction

This paper investigates the verification and synthesis of parameterized protocols that satisfy leadsto properties $R\leadsto Q$ on symmetric unidirectional rings (a.k.a. uni-rings) of deterministic and constant-space processes under no fairness and interleaving semantics, where $R$ and $Q$ represent global state predicates. The significance of this problem is two-fold. First, ring is a simple, but important topology for distributed systems whose underlying communication graph includes cycles (which is the case in many practical domains). Second, the leadsto property $R\leadsto Q$ is a critical liveness requirement in numerous contexts where system executions should guarantee eventual response (i.e., reaching the set of states $Q$) to specific stimuli (i.e., being in the set of states $R$). In a symmetric ring, the code of each process is generated from the code of a template/representative process by a simple variable renaming. Moreover, the number of processes in the ring is unbounded (but finite). In this paper, we first extend Suzuki’s undecidability results of verifying Linear Temporal Logic (LTL) properties of uni-rings [56] to the special case of verifying leadsto properties for symmetric uni-rings of deterministic and constant-space processes, and show that the verification problem remains undecidable. We then present a surprising result that, despite the undecidability of verification, synthesizing uni-rings that satisfy leadsto properties is actually decidable. This is a counterintuitive result as it is believed [47] that the synthesis of distributed systems is harder than their verification.

Most existing synthesis methods for parameterized protocols are extensions/variants of bounded and parameterized synthesis with a focus on Temporal Logic (TL) properties [20] for general communication topologies and under fairness assumptions. For example, Finkbeiner and Schewe [27] formulate the synthesis of fixed-size protocols as a set of constraints, and use Satisfiability Modulo Theory (SMT) solvers [14] to find a protocol that is accepted by a Universal Co-Buchi Tree (UCT) automaton generated from TL specifications. The search for a protocol is conducted up to a certain bound in the state space of processes and/or their automata-theoretic product; i.e., bounded synthesis. Jacobs and Bloem [37] extend bounded synthesis to parameterized protocols by identifying cutoff bounds, where a solution exists for a protocol with cutoff number of processes iff (if and only if) a solution exists for the parameterized protocol with unbounded number of processes (a.k.a. parameterized synthesis). Then, they apply the SMT-based bounded synthesis for an instance of the problem with at most cutoff processes. QBF-based bounded synthesis [29] takes an incomplete design (a.k.a. sketch) of a protocol and uses bounded synthesis towards generating fault-tolerant protocols in a bounded space. While methods for verification and synthesis of parameterized programs inspire our work, they (1) are mainly based on bounded/parameterized synthesis from temporal logic specifications; (2) make assumptions about synchrony, weak/strong fairness and complete knowledge of the network for each process; (3) the iterative nature of bounded and parameterized synthesis makes them computationally expensive and sensitive to their input (in part due to using SMT solvers), and (4) mostly focus on safety and local liveness properties that are specified in terms of the neighborhood of a proper subset of processes (e.g., progress of each process).

This paper puts forward a paradigm shift where we make a step towards developing a topology and property-specific approach. Our long-term objective is to create an extensible library of synthesis algorithms and tools that can efficiently generate parameterized protocols for specific elementary topologies (e.g., ring, tree, mesh, etc.) and basic temporal properties (e.g., leadsto, until, safety, etc.). Another component of this new paradigm includes methods that compose parameterized protocols with elementary topologies while preserving correctness, which is beyond the scope of this work. The core novelty of the proposed approach of this paper lies in identifying local characterizations of global properties (e.g., reachability, livelocks) towards enabling synthesis in the local state space of the template process for global correctness. Such local characterizations would enable more efficient automated reasoning methods, where the time/space complexity of synthesis will be in terms of the size of the local state space of template processes instead of semi-decision procedures that conduct backward/forward reachability analysis [13].

In the case of symmetric uni-rings that satisfy leadsto properties $R\leadsto Q$, we first show that verifying $R\leadsto Q$ remains undecidable even for protocols with constant-space and deterministic processes, and for conjunctive state predicates $R=\forall i\in\mathbb{Z}_{N}:r(x_{i-1},x_{i})$ and $Q=\forall i\in\mathbb{Z}_{N}:q(x_{i-1},x_{i})$, where $N$ denotes the number of processes in the ring, $\mathbb{Z}_{N}$ represents values modulo $N$, and $x_{i}$ captures an abstraction of all writeable variables of the template process $P_{i}$. (Conjunctive predicates may seem restricted but they have important applications for many systems [60, 33].) We then show some negative results that satisfying $R\leadsto Q$ by reaching states in $Q$ where $x_{i-1}\neq x_{i}$ is impossible. Intuitively, this negative result is an outcome of the impossibility of recovery to an $L$-coloring in symmetric uni-rings from any state (due to Bernard et al.’s [8]). Subsequently, we show that synthesizing a parameterized protocol that satisfies $R\leadsto Q$ is decidable iff (if and only if) there are some distinct values $v,\gamma\in$Dom$(x_{i})$ for which $q(\gamma,\gamma)$ and $q(v,\gamma)$ hold. Our necessary and sufficient conditions are based on the intuition that a parameterized protocol on a uni-ring that satisfies $R\leadsto Q$ exists iff there is a sequence of steps for every process towards satisfying $q(\gamma,\gamma)$ locally, starting from a state that satisfies $R$. We then provide a sound and complete algorithm that takes the state predicates $R$ and $Q$, and generates the parameterized actions of the template process, if a solution exists. The time complexity of the proposed algorithm is polynomial in the state space of the template process, which is often a small value for constant-space processes. We also show that synthesis remains decidable for cases where leadsto is required from the conjunction/disjunction of a set of predicates $R_{1},\cdots,R_{k}$, where $k>1$, to the conjunction/disjunction of two predicates $Q_{1}$ and $Q_{2}$. To demonstrate the practicality of our algorithm, we present a few case studies including a protocol that ensures reaching agreement in uni-rings when processes of the ring disagree on a value, and a parity protocol that guarantees a common parity amongst the processes. We conjecture that the implementation of our algorithm will provide a highly efficient synthesis tool as our previous work [18] on the synthesis of fault-tolerant parameterized uni-rings confirms our belief.

Organization.  Section 2 presents some basic concepts. Section 3 shows that verifying leadsto on uni-rings is undecidable. Section 4 identifies necessary and sufficient conditions for decidability of synthesizing symmetric uni-rings that satisfy leadsto properties. Section 5 presents a few case studies, including an agreement and a parity protocol. Section 6 discusses related work, and Section 7 summarizes our contributions and outlines some future work.

2 Preliminaries

This section presents the definition of parameterized protocols and their representation as action graphs. Wlog, we use the term protocol to refer to finite-state symmetric uni-rings as we conduct our investigation in the context of network protocols. Such rings are parameterized in the number of processes in the ring. A protocol $p$ for a computer network includes $N>1$ processes (finite-state machines), where each process $P_{i}$ has a finite set of readable and writeable variables. Any local state of a process (a.k.a. locality/neighborhood) is determined by a unique valuation of its readable variables. We assume that any writeable variable is also readable. The global state of a protocol is defined by a snapshot of the local states of all processes. The state space of a protocol, denoted by $\Sigma$, is the universal set of all global states. A state predicate is a subset of $\Sigma$. A process acts (i.e., transitions) when it atomically updates its state based on its locality. The locality of a process is defined by the network topology. For example, in a uni-ring consisting of $N$ processes, each process $P_{i}$ (where $i\in\mathbb{Z}_{N}$, i.e., $0\leq i\leq N-1$) has a neighbor/predecessor $P_{i-1}$, where subtraction and addition are in modulo $N$. We assume that processes act one at a time (i.e., interleaving semantics). Thus, each global transition corresponds to the action of a single process from some global state. An execution/computation of a protocol is a sequence of states $s_{0},s_{1},\dots,s_{k}$ where there is a transition from $s_{i}$ to $s_{i+1}$ for every $i\in\mathbb{Z}_{k}$. We consider parameterized protocols that consist of families of symmetric processes. Each family is represented by a template process from which the code of all family members is instantiated by a simple variable renaming/re-indexing. For instance, a symmetric uni-ring includes just one family for which we use triples of the form $(a,b,c)$ to denote actions $(x_{i-1}=a\land x_{i}=b\longrightarrow x_{i}\mathrel{\mathop{:}}=c;)$ of the template process $P_{i}$. An action has two components; a guard, which is a Boolean expression in terms of readable variables and a statement that atomically updates the state (i.e., writeable variables) of the process once the guard evaluates to true; i.e., the action is enabled.

Definition \thedefinition (Transition Function).

Let $P_{i}$ be any process with a state variable $x_{i}$ in a uni-ring protocol $p$. We define its transition function $\delta:\Sigma\times\Sigma\to\Sigma$ as a partial function such that $\delta(a,b)=c$ if and only if $P_{i}$ has an action $(x_{i-1}=a\land x_{i}=b\longrightarrow x_{i}\mathrel{\mathop{:}}=c;)$. In other words, $\delta$ can be used to define all actions of $P_{i}$ in the form of a single parametric action:

[TABLE]

where $(x_{i-1},x_{i})\in\textnormal{\sf\small\mbox{}{Pre}}(\delta)$ checks to see if the current $x_{i-1}$ and $x_{i}$ values are in the preimage of $\delta$. For other topologies, the same definition of transition function holds except that the preimage of $\delta$ might be specified differently depending on the locality of each process.

Definition \thedefinition (Action Graph).

We depict the set of actions of the template process of a symmetric uni-ring by a labeled directed multigraph $G=(V,A)$, called the action graph, where each vertex $v\in V$ represents a value in $\mathbb{Z}_{M}$, where $M$ denotes the domain size of $x_{i}$ and each arc $(a,c)\in A$ with a label $b$ captures an action $x_{i-1}=a\land x_{i}=b\longrightarrow x_{i}\mathrel{\mathop{:}}=c$.

For example, consider the Sum-Not-2 protocol given in [25]. Each process $P_{i}$ has a variable $x_{i}\in\mathbb{Z}_{3}$ and actions $x_{i-1}=0\land x_{i}=2\longrightarrow x_{i}\mathrel{\mathop{:}}=1$, $x_{i-1}=1\land x_{i}=1\longrightarrow x_{i}\mathrel{\mathop{:}}=2$, and $x_{i-1}=2\land x_{i}=0\longrightarrow x_{i}\mathrel{\mathop{:}}=1$. This protocol ensures that, from any global state, a state is reached where the sum of each two consecutive $x$ values does not equal $2$. The set of such states is formally specified as the state predicate $\forall i\in\mathbb{Z}_{N}:(x_{i-1}+x_{i}\neq 2)$. We can represent this protocol as a graph containing arcs $(0,2,1)$, $(1,1,2)$, and $(2,0,1)$ as shown in Figure 1.

For simplicity, we assume that protocols consist of self-disabling processes. As such, an action $(a,b,c)$ cannot coexist with action $(a,c,d)$ for any $d$. Moreover, a deterministic process cannot have two actions enabled at the same time; i.e., an action $(a,b,c)$ cannot coexist with an action $(a,b,d)$ where $d\neq c$.

Definition \thedefinition (Leadsto Properties).

The focus of this paper is on leadsto properties that are specified as $\Box(R\Rightarrow\Diamond Q)$ in Linear Temporal Logic (LTL), also denoted $R\leadsto Q$, where $\Box$ and $\Diamond$ respectively denote the universality and eventuality modalities, and $R=\forall i\in\mathbb{Z}_{N}:r(x_{i-1},x_{i})$ and $Q=\forall i\in\mathbb{Z}_{N}:q(x_{i-1},x_{i})$ represent conjunctive state predicates for a uni-ring of $N$ processes. A computation $\sigma=\langle s_{0},s_{1},\cdots\rangle$ of a protocol $p$ satisfies $\Box S$ iff the state predicate $S$ holds in every state $s_{i}\in\sigma$, for all $i\geq 0$. A computation $\sigma=\langle s_{0},s_{1},\cdots\rangle$ of a protocol $p$ satisfies $\Diamond S$ iff there is some $i\geq 0$ such that the state predicate $S$ holds in the state $s_{i}\in\sigma$. A computation $\sigma=\langle s_{0},s_{1},\cdots\rangle$ of a protocol $p$ satisfies $R\leadsto Q$ iff $s_{0}\in R$ implies that there is some $i\geq 0$ such that $s_{i}\in Q$. A symmetric uni-ring protocol $p$ satisfies $R\leadsto Q$ iff all the computations of $p$ satisfy $R\leadsto Q$, for unbounded (but finite) ring sizes.

Definition \thedefinition (Fairness).

A strongly fair scheduler ensures that any action that is infinitely often enabled will be executed infinitely often (due to Gouda [31]). A weakly fair scheduler guarantees that if an action is continuously enabled, then it will be executed infinitely often.

Livelock, deadlock, and closure.  A global livelock of a protocol $p$ is an infinite computation $l=\langle s_{0},s_{1},\cdots,s_{0}\rangle$, where $s_{i}$ is a global state, for all $i\geq 0$. A local livelock of a process $P$ of protocol $p$ is an infinite execution $l=\langle s_{0},s_{1},\cdots,s_{0}\rangle$, where $s_{i}$ is a local state of $P$, for all $i\geq 0$. Unless stated otherwise, we use the terms ‘’livelock” and ‘’global livelock” interchangeably. For satisfying a leadsto property $R\leadsto Q$, a reachable livelock $l$ that includes at least one state in $Q$ is acceptable; otherwise, it is considered as a failure towards satisfying $R\leadsto Q$. A deadlock of $p$ is a state that has no outgoing transition; i.e., no process is enabled to act. A state predicate $I$ is closed under $p$ iff there is no transition $(s,s^{\prime})$, where $s\in I$ but $s^{\prime}\notin I$.

Definition \thedefinition (Self-Stabilization and Convergence).

A protocol $p$ is self-stabilizing [15] to a state predicate $I$ (under no fairness) iff from any state in $\neg I$, every computation of $p$ reaches a state in $I$ (i.e., convergence) and remains in $I$ (i.e., closure). That is, $p$ is livelock-free and deadlock-free in $\neg I$, and $I$ is closed under $p$. A protocol $p$ is silent-stabilizing to $I$ iff $p$ converges to $I$ and $p$ has no computation starting in $I$. Notice that, in LTL, convergence to $I$ is specified as $\Box\Diamond I$, which is logically equivalent to true $\leadsto I$.

Definition \thedefinition (Weak Stabilization).

A weakly stabilizing protocol to $I$ ensures that from each state in $\neg I$, there is some computation that reaches a state in $I$ (a.k.a., weak convergence) and remains in $I$.

Notice that, any self-stabilizing protocol is also weakly stabilizing but the reverse is not true.

Definition \thedefinition (Locality Graphs).

Consider a state predicate $Q=\forall i:q(x_{i-1},x_{i})$ for a uni-ring. The relation $q(x_{i-1},x_{i})$ captures a set of local states, representing an acceptable relation between each process $P_{i}$ and its predecessor. The relation $q(x_{i-1},x_{i})$ must also be locally correctable in that, for any value of $x_{i-1}$, there is always a sequence of steps that $P_{i}$ can take to establish $q$ by updating $x_{i}$ only. To simplify reasoning, we represent $q(x_{i-1},x_{i})$ as a digraph $G=(V,A)$, called the locality graph, such that each vertex $v\in V$ represents a value in $\mathbb{Z}_{M}$, and an arc $(a,b)$ is in $A$ iff $q(a,b)$ is true.

Figure 2 illustrates the locality graph of the Sum-Not-2 protocol introduced in this section for the state predicate $Q=\forall i\in\mathbb{Z}_{N}:(x_{i-1}\oplus x_{i}\neq 2)$ where $M=4$ and $\oplus$ represents addition modulo $4$. Each closed walk in the locality graph characterizes a class of global states in the state predicate $Q$. For example, the closed walk $(0,1,3,1,0)$ captures the global states of ring sizes $4\times k$ where the $x_{i}$ value of processes follow a repeated pattern of $0,1,3,1$, and $k$ is a positive integer. We now represent one of our previous results [25] on the relation between closed walks in locality graphs and global states of parameterized uni-rings.

Theorem 2.1**.**

Any closed walk of length $L\geq 1$ in the locality graph of a conjunctive predicate $Q$ of a uni-ring characterizes global states in $Q$ of ring sizes of $L\times k$, where $k$ is a positive integer. (Proof in [25])

A corollary of Theorem 2.1 is as follows:

Corollary \thecorollary.

Any conjunctive state predicate $Z=\forall i:i\in\mathbb{Z}_{N}:z(x_{i-1},x_{i})$ whose locality graph $G_{Z}$ is acyclic specifies an empty set of states in a parameterized symmetric uni-ring.

Next, we represent some of our previous results regarding livelocks (from [25, 39]) that we shall use in this paper.

Propagations and Collisions.  When a process acts and enables its successor in a uni-ring, it propagates its ability to act. The successor may enable its own successor by acting, and the pattern may continue indefinitely. Such behaviors can be represented as sequences of actions that are propagated in a ring, called propagations. A propagation is a walk through the action graph. For example, the Sum-Not-2 protocol has a propagation $\langle(0,2,1),(1,1,2),(2,0,1),(1,1,2)\rangle$ whose actions can be executed in order by processes $P_{i}$, $P_{i+1}$, $P_{i+2}$, and $P_{i+3}$ from a state $(x_{i-1}\mathchar 44\relax x_{i}\mathchar 44\relax x_{i+1}\mathchar 44\relax x_{i+2}\mathchar 44\relax x_{i+3})=(0\mathchar 44\relax 2\mathchar 44\relax 1\mathchar 44\relax 0\mathchar 44\relax 1)$. A propagation is periodic with period $n$ iff its $j$-th action and $(j+n)$-th action are the same for every index $j$. A propagation with period $n\geq 1$ corresponds to a closed walk of length $n$ in the action graph. The Sum-Not-2 protocol has such a propagation of period $2$: $\langle(1,1,2),(2,0,1)\rangle$ (see Figure 1). A collision occurs when two consecutive processes, say $P_{i}$ and $P_{i+1}$, have enabled actions; e.g., $(a,b,c)$ and $(b,e,f)$, where $b\neq c$. In such a scenario, $x_{i-1}{=}a,x_{i}{=}b,x_{i+1}{=}e$. A collision occurs when $P_{i}$ executes and assigns $c$ to $x_{i}$. If that occurs, $P_{i}$ will be disabled (because processes are self-disabling), and $P_{i+1}$ becomes disabled too because $x_{i}$ is no longer equal to $b$. As a result, two enabled processes become disabled by one action.

“Leads” Relation.  Consider two actions $A_{1}$ and $A_{2}$ in a process $P_{i}$. We say the action $A_{1}$ leads $A_{2}$ iff the value of the variable $x_{i}$ after executing $A_{1}$ is the same as the value required for $P_{i}$ to execute $A_{2}$. Formally, this means an action $(a,b,c)$ leads $(d,e,f)$ iff $e=c$. Similarly, a propagation leads another iff for every index $j$, its $j$-th action leads the $j$-th action of the other propagation. In the action graph, this corresponds to two walks where the label of the destination node of the $j$-th arc in the first walk matches the arc label of the $j$-th arc in the second walk (for each index $j$). In [39, 41], we prove the following theorem:

Theorem 2.2**.**

A uni-ring protocol of symmetric, deterministic and self-disabling processes has a livelock for some ring size iff there exist $m$ propagations with some period $n$, where the $(i-1)$-th propagation leads the $i$-th propagation for each index $i$ modulo $m$, for $m>1$ and $n\geq 1$; i.e., the propagations successively lead each other modulo $m$.

We have shown [25] that verifying deadlock-freedom in uni-rings is decidable. However, checking livelock-freedom is an undecidable problem for uni-ring protocols (with self-disabling and deterministic processes) [39, 41].

Theorem 2.3**.**

Verifying livelock-freedom in a symmetric uni-ring protocol (with self-disabling and deterministic processes) is undecidable [39, 41].

We have also shown that verifying livelock-freedom remains undecidable even for a special type of livelocks, where exactly one process is enabled in every state of the livelocked computation; i.e., deterministic livelocks [39].

Theorem 2.4**.**

Verifying livelock-freedom in a symmetric uni-ring protocol (with self-disabling and deterministic processes) remains undecidable even for deterministic livelocks [39].

Since in every state of a deterministic livelock there is exactly one enabled process, the choice of fairness policy has no impact on which process will be executed in each state because the scheduler has only one enabled process to select.

Corollary \thecorollary.

Verifying livelock-freedom in a symmetric uni-ring protocol (with self-disabling and deterministic processes) remains undecidable regardless of the fairness assumption (i.e., scheduling policy) [39].

The above results imply the undecidability of verifying self-stabilization for symmetric uni-rings.

Theorem 2.5**.**

Verifying silent-stabilization (and self-stabilization) for a symmetric uni-ring protocol (with self-disabling and deterministic processes) is undecidable [39].

While verifying self-stabilization for uni-rings is undecidable, we have shown that synthesis of self-stabilizing uni-rings is surprisingly decidable.

Theorem 2.6**.**

Synthesizing silent-stabilization for a parameterized uni-ring protocol (with self-disabling, deterministic and constant-space processes) is decidable [42, 18].

Theorem 2.7**.**

Let $x_{i}$ denote a variable representing the local state space of each process $P_{i}$ in a symmetric uni-ring of $N$ processes (where $i\in\mathbb{Z}_{N}$), and the domain size of $x_{i}$ be a fixed value regardless of $N$. Then, there is a protocol $p$ that self-stabilizes to a state predicate $Q=\forall i\in\mathbb{Z}_{N}:q(x_{i-1},x_{i})$ for unbounded (but finite) ring size $N$ iff there is a vertex $\gamma$ in the locality graph of $Q$, where $\gamma$ has a self-loop (i.e., $q(\gamma,\gamma)$ holds) that can be reached from another vertex.

3 Undecidability of Verification

This section presents some impossibility results for the verification and synthesis of symmetric uni-ring protocols that satisfy leads-to properties. Throughout the rest of the paper, $R=\forall i\in\mathbb{Z}_{N}:r(x_{i-1},x_{i})$ and $Q=\forall i\in\mathbb{Z}_{N}:q(x_{i-1},x_{i})$ represent conjunctive state predicates. First, we formulate the verification problem as follows:

Problem \theproblem (Verification of LeadsTo).

Let $p$ be a symmetric parameterized protocol on a uni-ring, and $R$ and $Q$ represent conjunctive state predicates. Does $p$ satisfy $R\leadsto Q$ for unbounded (but finite) ring sizes?

Theorem 3.1**.**

Problem 3 is undecidable for uni-rings of self-disabling, constant-space and deterministic processes.

Proof.

For a symmetric protocol $p$ to satisfy $R\leadsto Q$ on a uni-ring, $p$ should ensure that starting in $R$, its computations will eventually reach some state in $Q$ under no fairness and interleaving semantics. This requires deadlock and livelock-freedom of computations of $p$ that start in $R$. Due to undecidability of verifying livelock-freedom on symmetric uni-rings (Theorem 2.3), Problem 3 is also undecidable. ∎

Problem \theproblem (Synthesis of LeadsTo).

Let $R$ and $Q$ be conjunctive state predicates. Consider a symmetric uni-ring of self-disabling, constant-space and deterministic processes. Does there exist a symmetric protocol $p$ on the ring that satisfies $R\leadsto Q$ for unbounded (but finite) ring sizes?

To investigate Problem 3, we first consider a special case of this problem where $R$=true.

Problem \theproblem (Synthesis of Convergence).

Let $Q$ be a conjunctive state predicate. Consider a symmetric uni-ring of self-disabling, constant-space and deterministic processes. Does there exist a symmetric protocol $p$ on the ring that satisfies $true\leadsto Q$ for unbounded (but finite) ring sizes?

Converging to a state where $Q=\forall i\in\mathbb{Z}_{N}:q(x_{i-1},x_{i})$ holds in a uni-ring can be achieved in two ways. First, there may be some value $c\in\mathbb{Z}_{M}$ such that $q(c,c)$ holds. Such values represent themselves as self-loops in the locality graph of $q(x_{i-1},x_{i})$. Second, $L$ values $c_{0},c_{1},\cdots,c_{L-1}\in\mathbb{Z}_{M}$ satisfy $q(x_{i-1},x_{i})$ in a circular fashion, where $q(c_{0},c_{1}),q(c_{1},c_{2}),\cdots,q(c_{L-2},c_{L-1}),q(c_{L-1},c_{0})$ hold and $L>1$. Such values form a cycle of length $L$ in the locality graph of $q(x_{i-1},x_{i})$. A cycle like that represents a family of rings that include global states where $Q$ holds through an ordered placement of the values that appear in the cycle. The sizes of such rings are multiples of $L$; i.e., ring sizes of $k\cdot L$, where $k$ is a positive integer (Theorem 2.1). To design a parameterized symmetric protocol $p$ that satisfies $\Diamond Q$ from some initial states captured by a state predicate $R$, developers should design $p$ in such a way that it ensures convergence to one of the aforementioned scenarios (under no fairness and interleaving semantics). We first show that, there is no protocol that can ensure convergence through the second scenario.

Definition \thedefinition (Ordered $L$-coloring).

Consider a set of $L$ distinct colors and a permutation function $next(c)$ (i.e., a bijective function from $L$ to $L$) that takes a color $c\in L$ and returns a color $c^{\prime}\in L$ where $c\neq c^{\prime}$. An ordered $L$-coloring of a uni-ring is an $L$-coloring where $\forall i\in\mathbb{Z}_{N}:c_{i}=next(c_{i\ominus 1})$, $N$ denotes the number of processes in the ring, and $\ominus$ represents subtraction modulo $N$.

Theorem 3.2**.**

No protocol exists that converges to an ordered $L$-coloring on symmetric uni-rings for rings of $N>L$ processes.

Proof.

Bernard et al.’s [8] show that no converging $L$-coloring protocol exists on symmetric uni-rings for rings of $N>L$ processes. By contradiction, assume there is a converging protocol $p$ that ensures an ordered $L$-coloring for some uni-ring with size $N>L$. Such an ordered $L$-coloring is a legitimate $L$-coloring. Thus, $p$ converges to an $L$-coloring, which is a contradiction with [8]. ∎

Corollary \thecorollary.

Theorem 3.2 holds under any fairness assumption, including strong fairness. In other words, Theorem 3.2 holds for weak convergence too.

Proof.

By contradiction, suppose Theorem 3.2 is falsified assuming strong fairness. That is, there is a weakly converging protocol that guarantees $L$-coloring on uni-rings of $N>L$ processes. This means that from any arbitrary state, there is at least a computation that reaches a valid $L$-coloring of the uni-ring for any $N>L$. Wlog, consider the case where $N=L+1$; i.e., the number of colors is one unit less than the number of processes, and processes that have a similar color to their predecessor simply choose the next color available by incrementing their value. Bernard et al. [8] show that the executions of any deterministic coloring protocol are isomorphic to a coloring protocol where all processes follow the rule of incrementing their value (i.e., choosing the next color in order). Now, consider an example state $\langle 0,0,1,2,3,\cdots,N-2\rangle$ for the uni-ring of size $N$. In this state, only the second process is enabled to change its color because it is the only processes that has the same color as that of its predecessor’s. The execution of the second process would get the protocol to the state $\langle 0,1,1,2,3,\cdots,N-2\rangle$, where the third process is now enabled. Following the same pattern, the uni-ring reaches the state $\langle 0,1,2,2,3,\cdots,N-2\rangle$, where the fourth process is the only process that is enabled. This sequence of states forms the livelock $\langle 0,0,1,2,3,\cdots,N-2\rangle$, $\langle 0,1,1,2,3,\cdots,N-2\rangle$, $\langle 0,1,2,2,3,\cdots,N-2\rangle$, $\cdots$, $\langle 0,1,2,3,4,\cdots,N-2,N-2\rangle$, $\langle 0,1,2,3,\cdots,N-2,0\rangle$. Notice that, the last state is actually the same as the initial state of this execution of the symmetric uni-ring. Moreover, this livelock is deterministic. Thus, by Corollary 2, even strong fairness will not resolve this deterministic livelock, which prevents convergence to $L$-coloring. A similar argument holds for weak fairness. ∎

Theorem 3.3**.**

Let $Q$ be a conjunctive state predicate $\forall i\in\mathbb{Z}_{N}:q(x_{i-1},x_{i})$. No symmetric uni-ring protocol exists that can converge to states where $Q$ holds through cyclic satisfaction of $q(c_{0},c_{1}),q(c_{1},c_{2}),\cdots,q(c_{L-2},c_{L-1}),q(c_{L-1},c_{0})$, for rings of $N>L$ processes and $L>1$. This result holds under any fairness assumption.

Proof.

By contradiction, let $p$ be a parameterized protocol that converges to states in $Q$ (under any fairness assumption) where $q(c_{0},c_{1}),q(c_{1},c_{2}),\cdots,q(c_{L-2},c_{L-1}),q(c_{L-1},c_{0})$ hold for some values $c_{0},c_{1},\cdots,c_{L-1}$, where $L>1$. Thus, the locality graph of $q(x_{i-1},x_{i})$ must include a cycle whose vertices are labeled with $c_{0},c_{1},\cdots,c_{L-1}$ in order. As a results, such states of $Q$ represent an ordered $L$-coloring. That is, $p$ converges to an ordered $L$-coloring protocol for $N>L$. This is a contradiction with Theorem 3.2 and Corollary 3. ∎

Theorem 3.4**.**

Let $R$ and $Q$ be non-empty conjunctive state predicates, $R\cap Q=\emptyset$ and $R\neq true$. No symmetric protocol exists on uni-rings that can satisfy $(R\leadsto Q)$ by reaching states where $Q$ holds through cyclic satisfaction of $q(c_{0},c_{1}),q(c_{1},c_{2}),\cdots,q(c_{L-2},c_{L-1}),q(c_{L-1},c_{0})$, for rings of $N>L$ processes.

Proof.

By contradiction, let $p$ be such a protocol whose computations reach states in $Q$ from states in $R$ through cyclic satisfaction of $q(c_{0},c_{1}),q(c_{1},c_{2}),\cdots,q(c_{L-2},c_{L-1}),q(c_{L-1},c_{0})$. Using the decidability of synthesizing self-stabilizing protocols (Theorem 2.7), we design a silent stabilizing protocol $p^{\prime}$ that converges to $R$ from any state, and once in $R$, $p^{\prime}$ becomes disabled. However, the actions of $p$ and $p^{\prime}$ may interfere by creating livelocks outside $R\vee Q$. Such livelocks include states where $p$ and $p^{\prime}$ both have enabled processes that can take some action. Thus, such livelocks are not deterministic livelocks. To ensure recovery from such livelocks, we assume strong fairness. As a result, we guarantee that $p^{\prime}$ will eventually converge to $R$, and from $R$, protocol $p$ can guarantee that we reach states in $Q$ through cyclic satisfaction of $q(c_{0},c_{1}),q(c_{1},c_{2}),\cdots,q(c_{L-2},c_{L-1}),q(c_{L-1},c_{0})$. Therefore, the net result is a protocol that converges to $Q$ through cyclic satisfaction of $q(c_{0},c_{1}),q(c_{1},c_{2}),\cdots,q(c_{L-2},c_{L-1}),q(c_{L-1},c_{0})$ under strong fairness. This is a contradiction with Theorem 3.3. ∎

4 Decidability of Synthesis

This section proves the decidability of synthesizing symmetric uni-ring protocols that satisfy the leads-to property $(R\leadsto Q)$, where $R$ and $Q$ denote non-empty conjunctive state predicates. We first establish a relation between self-stabilization and leads-to by the following lemma:

Lemma \thelemma.

Let $R$ and $Q$ be conjunctive state predicates specified on uni-rings. There is a symmetric protocol that satisfies $(R\leadsto Q)$ for unbounded (but finite) ring sizes iff there is a symmetric protocol that stabilizes to $Q$ for unbounded (but finite) ring sizes.

Proof.

Any protocol $p$ that is self-stabilizing to $Q$ ensures convergence to $Q$; i.e., $(true\leadsto Q)$. Since $R\subset true$, it follows that protocol $p$ satisfies $(R\leadsto Q)$. Now, if there is no protocol that stabilizes to $Q$, then Theorem 2.7 implies that there is no value $\gamma$ in the domain of $x_{i}$ for which $q(\gamma,\gamma)$ holds. Thus, for a protocol $p^{\prime}$ to satisfy $(R\leadsto Q)$, $p^{\prime}$ must converge to states where $Q$ holds through cyclic satisfaction of $q(c_{0},c_{1}),q(c_{1},c_{2}),\cdots,q(c_{L-2},c_{L-1}),q(c_{L-1},c_{0})$, which is impossible due to Theorem 3.4. ∎

Theorem 4.1**.**

Synthesizing a symmetric protocol on uni-rings that satisfies $(R\leadsto Q)$ (for unbounded ring sizes) is decidable.

To prove Theorem 4.1, we present a synthesis algorithm that takes two non-empty and disjoint conjunctive state predicates $R$ and $Q$, and generates a parameterized protocol that satisfies $R\leadsto Q$ on symmetric uni-rings, for unbounded ring sizes. Wlog, we assume that $R\cap Q=\emptyset$; even if $R$ and $Q$ intersect, $i.e.,(R\cap Q\neq\emptyset)$ , the synthesis problem is formulated for $(R-X)\leadsto(Q-X)$, where $X=R\cap Q$. (Note that $R\leadsto Q$ is vacuously true in $X$.) We later show that Algorithm 1 is sound and complete.

For a specific $\gamma$, Algorithm 1 performs Steps 3 to 8 in order to determine if there is a solution for that $\gamma$. In Steps 3 to 8, Algorithm 1 constructs the underlying structure of an action graph that will form the synthesized protocol $p$ after the labeling steps of 9 and 10. A correct protocol must meet certain constraints that are the minimum requirements for a protocol $p$ that satisfies $R\leadsto Q$. For instance, $p$ should only guarantee $R\leadsto Q$ starting in $R$. That is why Step 5 calculates the set of values in $\mathbb{Z}_{M}$ that do not appear in any state of $R$, and Step 6 removes them from the spanning tree of $G^{\prime}_{Q}$. Moreover, since we assume $R\cap Q=\emptyset$, the cycles of $G_{R}$ and $G_{Q}$ are arc-disjoint (due to Theorem 2.1). Thus, any correct protocol cannot include an arc $(a,c)\in A_{R}$ for which $r(a,c)$ holds and $c=\gamma$. Otherwise, the processes will include an action $x_{i-1}=a\wedge x_{i}=b\rightarrow x_{i}:=c$, for some $b$ where $\neg q(a,b)$. Such an action would set the locality of each process to a state (i.e., $x_{i-1}=a\wedge x_{i}=c$) where $R$ holds, thereby preventing reachability to $Q$. That is why Step 7 excludes such arcs. After eliminating such vertices and arcs through Steps 3 to 8, if we have a tree-like structure that has no leaves in common with the cycles in $G_{R}$, then we move to Step 2 and repeat the same process for a different $\gamma$. Algorithm 1 exits only if no valid action graph can be built for any $\gamma$.

Theorem 4.2** (Soundness).**

Algorithm 1 is sound.

Proof.

We show that if Algorithm 1 generates a parameterized protocol $p$ for two disjoint predicates $R$ and $Q$, then $p$ satisfies $R\leadsto Q$ for unbounded ring sizes. To prove this, we show that any computation of $p$ starting in a state $s\in R$ will be deadlock-free and livelock-free outside $Q$ and will eventually reach a state $s_{f}$ in $Q$.

Deadlock-freedom: Since the synthesized action graph, denoted $AG$, is a tree with a self-loop on its root $\gamma$, $AG$ must have some leaves. Step 8 of the algorithm ensures that any vertex $v\neq\gamma$ that participate in a cycle in the locality graph $G_{R}$ of the state predicate $R$ appears as a leaf in the tree. The labeling method of Step 9 guarantees that any leaf $a$ of $AG$ has an outgoing arc $(a,c)$ (to some vertex $c\in\mathbb{Z}_{M}$) with a label $b$ such that $r(a,b)$ holds. Step 11 would translate each labeled arcs $(a,b,c)$ to a parameterized action $x_{i-1}=a\wedge x_{i}=b\rightarrow x:=c$. By Theorem 2.1, we also know that cycles in locality graphs characterize global states of uni-rings. Thus, the guard condition of such an action evaluates to true in a state in $R$ because $r(a,b)$ holds. Thus, starting in $R$, there is at least one enabled action; i.e., deadlock-freedom in $R$. We now show that the computations of the synthesized protocol $p$ remain deadlock-free until reaching a state in $Q$. The only values in $\mathbb{Z}_{M}$ that are excluded from the synthesized action graph $AG$ include those values that do not participate in any cycle in $G_{R}$; i.e., those values do not appear in states in $R$. If computations of $p$ reach a state outside $R\vee Q$, the labeling method of Step 10 ensures that there is some enabled action; hence deadlock-freedom.

Livelock-freedom: The only type of propagation included in the synthesized action graph is $(\gamma,b,\gamma)$. Thus, there are no propagations that lead each other circularly. That is, based on Theorem 2.2, the synthesized protocol is livelock-free.

Reachability of $Q$: By deadlock-freedom and livelock-freedom, each process will eventually satisfy $q(\gamma,\gamma)$, which would result in a global state of the ring in $Q$. ∎

Theorem 4.3** (Completeness).**

Algorithm 1 is complete.

Proof.

Let $p$ be a parameterized protocol that satisfies $R\leadsto Q$ but Algorithm 1 fails to generate $p$. By Theorem 3.4, $p$ cannot satisfy $R\leadsto Q$ through cyclic satisfaction of some values; i.e., the action graph of $p$, denoted $A_{p}$, can include only cycles of length 1; i.e., self-loops. Further, if a node $v$ has a self-loop in $A_{p}$, then $v$ cannot have any other outgoing labeled arc; otherwise, $A_{p}$ will include either cycles of length greater than one, which contradicts Theorem 3.4, or ends in nodes without any outgoing arcs; i.e., deadlock. Thus, there must be a value $\gamma\in\mathbb{Z}_{M}$ for which $q(\gamma,\gamma)$ holds and there is some value $v\in\mathbb{Z}_{M}$, where $v\neq\gamma$ and $q(v,\gamma)$ holds too. That is, $A_{p}$ must include $\gamma$ as well as another labeled arc $(v,b,\gamma)$ for some $b\in\mathbb{Z}_{M}$, where $v\neq\gamma$ and $b\neq\gamma$. This means that Algorithm 1 would actually find such $\gamma$ in Step 2. The action graph $A_{p}$ must also include some source nodes without any incoming arcs. Otherwise, it would include cycles of length greater than one (which again contradicts Theorem 3.4). Such source nodes must also intersect with the vertices of some cycles in $V_{R}$ and have outgoing labeled arcs $(a,b,c)$ such that $r(a,b)$ holds and $a$ is a vertex in a cycle in $G_{R}$. Otherwise, $p$ deadlocks in $R$, which contradicts with $p$ satisfying $R\leadsto Q$. As such, Algorithm 1 would have included such labeled arcs in Steps 8 and 9, and would have created the action graph $A_{p}$ sinking towards $\gamma$. ∎

Theorem 4.4**.**

Algorithm 1 has an asymptotic polynomial time complexity in the domain size $M$.

Proof.

Other than Step 3, it is trivial to see that all the other steps would take polynomial amount of time (in $M=|V_{Q}|=$DomainSize$(x_{i})$) to compute. For Step 3, we first remove self-loops. Then, we start eliminating any vertex $v\neq\gamma$ in the locality graph $G_{Q}=(V_{Q},A_{Q})$ that has no outgoing arcs. This would result in removing the incoming arcs of $v$ too. We continue such vertex/arc removals until all remainig vertices have at least one outgoing arc, or no vertex remains. The remaining sub-graph that contains $\gamma$ would be used for subsequent steps of the algorithm. This process takes $O(M)$. Therefore, the asymptotic time complexity of Algorithm 1 is polynomial in $M$. ∎

Theorem 4.5**.**

Let $R_{i}$ and $Q$ be conjunctive state predicates, for $1\leq i\leq k$ and $k>1$. Synthesizing a parameterized protocol on symmetric uni-rings that satisfies $((R_{1}\vee R_{2}\cdots\vee R_{k})\leadsto Q)$ is decidable.

Proof.

One can apply Algorithm 1 $k$ times for each $R_{i}$ and decide if there is some $1\leq i\leq k$ for which there is a protocol that satisfies $R_{i}\leadsto Q$. Any such protocol is also a solution for $((R_{1}\vee R_{2}\cdots\vee R_{k})\leadsto Q)$. ∎

Theorem 4.6**.**

Let $R_{i}$ be conjunctive state predicates, for $1\leq i\leq k$ and $k>1$. Synthesizing a parameterized protocol on symmetric uni-rings that satisfies $((R_{1}\wedge R_{2}\cdots\wedge R_{k})\leadsto Q)$ is decidable.

Proof.

Since $R_{i}$ predicates are conjunctive, we apply Algorithm 1 while identifying cycles in the intersection of the locality graphs of $R_{i}$, for $1\leq i\leq k$. The rest of Algorithm 1 remains the same. ∎

Theorem 4.7**.**

Let $R,Q_{1}$ and $Q_{2}$ be conjunctive state predicates and $Q_{1}\cap Q_{2}\neq\emptyset$. Synthesizing a parameterized protocol on symmetric uni-rings that satisfies $(R\leadsto(Q_{1}\wedge Q_{2}))$ is decidable.

Proof.

We use Algorithm 1 by finding a value $\gamma$ in the domain of the variable $x_{i}$ (of the template process $P_{i}$) such that $q_{1}(\gamma,\gamma)\wedge q_{2}(\gamma,\gamma)$ holds. Moreover, it is straightforward to algorithmically find a common cycle in the locality graphs of $Q_{1}$ and $Q_{2}$ that contains $\gamma$ (e.g., by running a DFS algorithm starting at $\gamma$). There is a parameterized protocol that satisfies $(R\leadsto(Q_{1}\wedge Q_{2}))$ iff Algorithm 1 generates a protocol (due to its completeness). ∎

Theorem 4.8**.**

Let $R,Q_{1}$ and $Q_{2}$ be conjunctive state predicates. Synthesizing a parameterized protocol on symmetric uni-rings that satisfies $(R\leadsto(Q_{1}\vee Q_{2}))$ is decidable.

Proof.

It is straightforward to see that a protocol $p$ satisfies $(R\leadsto(Q_{1}\vee Q_{2}))$ iff $p$ satisfies $(R\leadsto Q_{1})$ or $(R\leadsto Q_{2})$. We execute Algorithm 1 once for $R\leadsto Q_{1}$ and another time for $R\leadsto Q_{2}$ in order to decide if a solution for $(R\leadsto(Q_{1}\vee Q_{2}))$ exists. ∎

5 Case Studies

This section presents four case studies of using Algorithm 1 for the synthesis of symmetric uni-rings. Section 5.1 discusses the synthesis of the Sum-Not-2 protocol, and Section 5.2 presents the dual of Sum-Not-2 protocol. Section 5.3 illustrates the synthesis of a symmetric uni-ring for solving the parity problem in distributed computing. Section 5.4 presents the synthesis of an agreement protocol on uni-rings. To increase our confidence in the proposed synthesis method, we have model checked all protocols synthesized in this section using SPIN [35] up to the extent our computational resources permit. The Promela models are available at http://asd.cs.mtu.edu/projects/ProTop/index.html.

5.1 Sum-Not-2

The Sum-Not-2 protocol is a simple but non-trivial example that can clearly demonstrate the complexity of synthesizing parameterized uni-rings that satisfy leadsto properties. In this protocol, we specify the set of initial states for even-size uni-rings where the summation of $x_{i-1}$ and $x_{i}$ is equal to two (modulo $M=4$) but $x_{i}\neq 1$. That is, $R=\forall i\in\mathbb{Z}_{N}:r(x_{i-1},x_{i})$, where $r(x_{i-1},x_{i})\equiv(x_{i}=2\wedge x_{i-1}=0)\vee(x_{i}=0\wedge x_{i-1}=2)$, and $N$ denotes the number of processes (i.e., ring size). The objective is to synthesize a protocol that eventually reaches states where the summation of $x_{i-1}$ and $x_{i}$ is no longer equal to two (for all processes), and it is not the case that all processes have a value of zero; i.e., $Q=\forall i\in\mathbb{Z}_{N}:q(x_{i-1},x_{i})$, where $q(x_{i-1},x_{i})\equiv((x_{i-1}\oplus_{4}x_{i})\neq 2)\wedge((x_{i-1}\neq 0)\vee(x_{i}\neq 0))$, and $\oplus_{4}$ denotes addition modulo $M=4$. We require that $R\leadsto Q$ is satisfied from $R$ for all even values of $N$.

Step 1: As the first step of Algorithm 1, we construct the locality graphs of $R$ and $Q$ illustrated in Figure 4. Each arc $(a,b)$ captures the fact that $r(a,b)$ (respectively, $q(a,b)$) holds. For example, the only arcs in Figure 4-(a) are between 0 and 2 because $r(x_{i-1},x_{i})$ does not hold for any other pairs of values in $\mathbb{Z}_{4}$. As another example, Figure 4-(b) lacks any arcs between 0 and 2 because their summation adds up to 2, which violates $Q$. Moreover, the only vertex that has a self-loop is 2 because the arc $(0,0)$ violates the second conjunct of $Q$ and arcs $(1,1)$ and $(3,3)$ violate the first conjunct of $Q$ (i.e., $1\oplus_{4}1=2$ and $3\oplus_{4}3=2$).

Step 2: Since $q(2,2)$ holds in $G_{Q}$ (see Figure 4-(b)), we set $\gamma$ to 2.

Step 3: Figure 5-(a) illustrates the induced subgraph $G^{\prime}_{Q}$ including simple cycles of $G_{Q}$ that contain $\gamma$ (e.g., the simple cycle $(0,3,2,1,0)$).

Step 4:  Figure 5-(b) illustrates a spanning tree $\tau$ rooted at $\gamma=2$, where each arc $(a,b)$ denotes that $b$ is the parent of $a$ in $\tau$. Notice that, there may be several spanning trees; i.e., the solution is not unique.

Step 5: Figure 4-(a) illustrates that vertices 1 and 3 do not participate in any cycles; hence $V^{\prime}_{R}=\{1,3\}$.

Step 6: Since $1$ is the only vertex of $V^{\prime}_{R}$ that is also a leaf of the spanning tree $\tau$, we eliminate its outgoing arc to $3$, illustrated by the dashed arrow in Figure 5-(b).

Step 7:  Since $V^{\prime}_{Q}=V_{Q}$, Step 7 does not make any changes.

Step 8: The only leaf of the tree $\tau^{\prime}$ for which $r(0,2)$ holds is [math]. Thus, we include just the self-loop $(2,2)$ to generate the tree $\tau^{\prime\prime}$ in Figure 6-(a).

Steps 9 and 10: Consider the arc $(3,2)$. The candidate labels of this arc include $0,1$ and $3$. We exclude $2$ because it is equal to the parent vertex of $3$. Since $q(3,0)$ and $q(3,1)$ are true and $q(3,3)$ is false, the only acceptable label for the arc $(3,2)$ is $3$ (see Figure 6-(a)). The arc $(0,3)$ has the label $2$ because $r(0,2)\wedge\neg q(0,2)$ holds. Likewise, the self-loop on $2$ gets [math] as its label.

Step 11: Figure 6-(b) illustrates the synthesized parameterized actions for any even-size uni-ring that satisfies $R\leadsto Q$.

5.2 SumTwo Protocol

We consider the dual of the previous example, which provides another interesting case. Let $R$ be $\forall i\in\mathbb{Z}_{N}:(x_{i}\oplus_{4}x_{i-1}\neq 2)\wedge(x_{i}\oplus_{4}1=x_{i-1})$, and $Q$ be $\forall i\in\mathbb{Z}_{N}:((x_{i-1}\oplus_{4}x_{i})=2)\wedge((x_{i-1}\neq 1)\vee(x_{i}\neq 1))$, where $N$ denotes the number of processes (i.e., ring size), and $\oplus_{4}$ represents addition modulo $M=4$. (Addition and subtraction in subscripts are done modulo $N$.) We would like to synthesize a protocol that eventually reaches states where the summation of $x_{i-1}$ and $x_{i}$ is equal to two (for all processes), and it is not the case that all processes have a value $1$. We require that $R\leadsto Q$ is satisfied from $R$ for all even values of $N$.

Step 1:  Figure 7 illustrates the locality graphs of the predicates $R$ and $Q$.

Steps 2, 3, 4:   Since $q(3,3)$, we have $\gamma=3$ (see Figure 7-(b)). The induced subgraph $G^{\prime}_{Q}$ includes the vertex $3$. Thus, the resulting spanning tree would include a single vertex; i.e., $3$.

Steps 5, 6:  Since all vertices of $G_{R}$ participate in a cycle (Figure 7-(a)), we have $V^{\prime}_{R}=\emptyset$. As such, there is nothing to be done in Step 6.

Steps 7 and 8:  Including arcs from vertices that are in $V_{Q}-V^{\prime}_{Q}$ to $\gamma$ would result in the spanning tree $\tau$ in Figure 8-(a). Since $r(0,3)$ holds, $\tau^{\prime}$ would look like the tree in Figure 8-(b) excluding the dashed arc and the self-loop. Including an arc from 0 to the leaf 1 as well as the self-loop $(3,3)$ would generate the tree $\tau^{\prime\prime}$ in Figure 8-(b).

Steps 9, 10, 11: The remaining steps of Algorithm 1 would generate the action graph of Figure 9-(a), which would be translated to the parameterized actions of the synthesized SumTwo protocol in Figure 9-(b).

5.3 Parity Protocol

The Parity protocol solves the problem of identifying a common parity amongst the nodes of a distributed system without a central coordinator dictating what the parity should be. In this case study, we synthesize a parameterized protocol for symmetric uni-rings that ensures reachability to an even parity in the entire ring from states where there is an odd parity. In fact, the synthesized protocol provides an algorithm for switching from odd to even parity amongst the nodes of a uni-ring. More precisely, we would like the protocol to satisfy $R\leadsto Q$, where $R=\forall i\in\mathbb{Z}_{N}:(((x_{i}\ominus_{4}x_{i-1}){}\textnormal{{\;mod\;}}{}2=0)\wedge(x_{i}{}\textnormal{{\;mod\;}}{}2\neq 0))$, $Q=\forall i\in\mathbb{Z}_{N}:(((x_{i}\ominus_{4}x_{i-1}){}\textnormal{{\;mod\;}}{}2=0)\wedge(x_{i}{}\textnormal{{\;mod\;}}{}2=0))$, $M=4$ and $\ominus_{4}$ denotes subtraction modulo 4.

Steps 1 and 2: We first construct the locality graphs $G_{R}$ and $G_{Q}$ (illustrated in Figure 10). Notice that both 0 and 2 can be considered as $\gamma$; we let $\gamma=2$.

Steps 3 and 4: We induce the subgraph $G^{\prime}_{Q}$ from $G_{Q}$ by considering the simple cycle between 0 and 2. We then compute the spanning tree of $G^{\prime}_{Q}$ rooted at $\gamma=2$.

Steps 5, 6: The set $V^{\prime}_{R}$ includes vertices 0 and 2, and the only vertex that is a leaf in $\tau$ is 0; hence $V^{\prime}_{Rleaf}=\{0\}$. Removing the outgoing arc $(0,2)$ will create the tree $\tau^{\prime}$ with the single vertex 2.

Steps 7 and 8: We now compute $V_{Q}-(V^{\prime}_{Q}\cup V^{\prime}_{Rleaf})$, which is equal to $\{1,3\}$. Thus, we include the arcs $(1,2)$ and $(3,2)$ to generate the tree $\tau^{\prime\prime}$. We also include the self-loop $(2,2)$ in $\tau^{\prime\prime}$ to generate the structure of the action graph of the synthesized protocol in Figure 12-(a). Notice that, $r(1,2)$ and $r(3,2)$ do not hold. Since the only leaf in $\tau^{\prime}$ is vertex 2, arc $(0,2)$ cannot be included in $\tau^{\prime\prime}$.

Steps 9, 10, 11: The remaining steps of the algorithm labels $\tau^{\prime\prime}$ (Figure 12-(a)), which would result in the action graph in Figure 12-(b). The synthesized parameterized actions of the parity protocol are as follows:

$\begin{aligned} &x_{i-1}{=}1&{}\land{}&x_{i}{=}3&{}\hskip 28.45274pt\longrightarrow{}\hskip 28.45274pt&x_{i}\mathrel{\mathop{:}}=2;\\ &x_{i-1}{=}3&{}\land{}&x_{i}{=}1&{}\hskip 28.45274pt\longrightarrow{}\hskip 28.45274pt&x_{i}\mathrel{\mathop{:}}=2;\\ &x_{i-1}{=}2&{}\land{}&(x_{i}{=}1\lor{}x_{i}{=}3)&{}\hskip 28.45274pt\longrightarrow{}\hskip 28.45274pt&x_{i}\mathrel{\mathop{:}}=2;\end{aligned}$

5.4 Agreement Protocol

Agreement is a fundamental problem in distributed computing. This section demonstrates how Algorithm 1 synthesizes a parameterized protocol on symmetric uni-rings that ensures agreement from a set of initial states. Specifically, we synthesize a protocol that meets $R\leadsto Q$, where $Q=\forall i\in\mathbb{Z}_{N}:x_{i-1}=x_{i}$, and $R=\forall i\in\mathbb{Z}_{N}:(((x_{i}\ominus x_{i-1}){}\textnormal{{\;mod\;}}{}2=0)\wedge(x_{i}\neq x_{i-1}))$.

Steps 1 and 2: Figure 13 illustrates the locality graphs $G_{R}$ and $G_{Q}$, respectively for predicates $R$ and $Q$. We have four possible values for $\gamma$. Wlog, we let $\gamma$ be 1.

Steps 3 and 4: Since $G_{Q}$ has only self-loops on its vertices, $G^{\prime}_{Q}$ would include just Vertex 1. Correspondingly, the spanning tree $\tau$ includes just a single vertex (i.e., 1).

Steps 5, 6: Since $V^{\prime}_{R}$ is empty, $V^{\prime}_{Rleaf}$ becomes empty too.

Steps 7 and 8: We have $V_{Q}-(V^{\prime}_{Q}\cup V^{\prime}_{Rleaf})=\{0,2,3\}$. As a result, $\tau^{\prime}$ would include arcs $(0,1)$ and $(2,1)$, but excludes $(3,1)$ because $r(3,1)$ holds (see Figure 14-(a)). Executing Step 8 would result in including arcs $(3,2)$ and $(1,1)$, resulting in tree $\tau^{\prime\prime}$ (Figure 14-(b)).

Steps 9, 10, 11: The remaining steps of the algorithm labels $\tau^{\prime\prime}$ (Figure 14-(b)), which would result in the action graph in Figure 15.

The synthesized parameterized actions of the agreement protocol are as follows:

$\begin{aligned} &x_{i-1}{=}0&{}\land{}&x_{i}{=}2&{}\longrightarrow{}&x_{i}\mathrel{\mathop{:}}=1;\\ &x_{i-1}{=}3&{}\land{}&x_{i}{=}1&{}\longrightarrow{}&x_{i}\mathrel{\mathop{:}}=2;\\ &x_{i-1}{=}2&{}\land{}&(x_{i}{=}0\lor{}x_{i}{=}3)&{}\longrightarrow{}&x_{i}\mathrel{\mathop{:}}=1;\\ &x_{i-1}{=}1&{}\land{}&(x_{i}{=}0\lor{}x_{i}{=}2\lor{}x_{i}{=}3)&{}\longrightarrow{}&x_{i}\mathrel{\mathop{:}}=1;\end{aligned}$

6 Related Work

There is a diverse set of methods for the synthesis of fixed-size and parameterized programs/protocols. For example, program sketching [55, 54] aims to automatically fill the holes in an incomplete program. Example-based synthesis [53] generates a program from a table of inputs and expected outputs. Syntax-guided program synthesis [3] constrains the search space of synthesis using a syntactic template of a program. Counterexample guided inductive synthesis [48, 1] generates abstract programs and a verifier provides counterexamples for refining the synthesized abstract programs. Techniques for automated completion of distributed protocols [59, 4, 58, 5] mainly extend program sketching and synthesis-by-examples for distributed programs under strong/weak fairness. Existing automated techniques [6, 43, 32, 17, 11, 19, 24, 22, 40, 23] for the addition of fault tolerance mainly enable the synthesis of fixed-size fault-tolerant protocols from their fault-intolerant versions.

Most existing methods for the verification of parameterized programs can be classified into abstraction methods [9, 36, 21], SMT-based verification [30, 13], parameterized visual diagrams [52], network invariants [61, 38, 34], compositional model checking [46], logic program transformations and inductive verification methods [49, 50, 51, 28], regular model checking [12, 57, 2], proof spaces [26] and topology-specific verification [45].

There are a variety of methods for the synthesis of parameterized programs. For example, Attie and Emerson [7] compose a pair of representative processes (under weak fairness) to reason about the global safety and local leads-to properties of a symmetric parameterized system. Some researchers [16, 10] present methods for generating parameterized protocols for specific problems (e.g., counting) on specific topologies (e.g., clique [16]). Verification and synthesis methods based on threshold automata [44] take a sketch automaton (whose transitions have incomplete guard conditions capturing the number of received messages), and complete the guards towards satisfying program specifications.

The closest work to this paper includes our previous work on the synthesis of self-stabilizing parameterized uni-rings [18], where a protocol is expected to recover to a set of states from any state. In the synthesis of self-stabilization, $R=true$ and $Q$ captures a set of legitimate states to which recovery is required. As such, we construct a spanning tree of the locality graph of $Q$ rooted at some $\gamma$. Such a spanning tree should include all values in the domain of $x_{i}$. By having just a self-loop on $\gamma$, we ensure that starting from any state in $\neg Q$, no livelocks will be reached (due to Theorem 2.2). However, when $R\subset true$, it is not trivial how the synthesis should be conducted so global computations of a parameterized ring guarantee reachability of $Q$ only from global states in $R$. To address this challenge, we would need to identify local characterization of states that are reachable from $R$ as well as ensuring livelock-freedom only in states reachable from $R$. Algorithm 1 succeeds in tackling these challenges. It is noteworthy to mention that a self-stabilizing solution may not be the best solution for $R\leadsto Q$ in cases where multiple leadsto properties must be satisfied. For example, consider the case of two leadsto properties $R_{1}\leadsto Q_{1}$ and $R_{2}\leadsto Q_{2}$, where $R_{1}\cap R_{2}=\emptyset$. If one synthesizes a self-stabilizing protocol $p$ that recovers to $Q_{1}$, then $p$ certainly satisfies $R_{1}\leadsto Q_{1}$ too. However, all hopes for revising $p$ towards satisfying $R_{2}\leadsto Q_{2}$ are lost because $p$ instead satisfies $R_{2}\leadsto Q_{1}$. Using Algorithm 1, we ensure that $R_{1}\leadsto Q_{1}$ is satisfied only from $R_{1}$, and not from states outside $R_{1}$. We are currently investigating conditions under which synthesis of parameterized uni-rings that satisfy two leadsto properties $R_{1}\leadsto Q_{1}$ and $R_{2}\leadsto Q_{2}$ becomes possible.

7 Conclusions and Future Work

We investigated the problems of verifying and synthesizing parameterized protocols on symmetric unidirectional rings for leadsto properties $R\leadsto Q$. We showed that the verification problem remains undecidable even for constant-space and deterministic processes and for global state predicates $R$ and $Q$ that are formed by the conjunction of symmetric local state predicates; i.e., conjunctive predicates. We then presented a somewhat surprising result that, synthesizing protocols that satisfy $R\leadsto Q$ on uni-rings is actually decidable! This is a significant result as both ring and leadsto are important aspects of distributed protocols. We are currently working on the implementation of our synthesis algorithm and conducting more interesting case studies such as cache coherence, leader election, etc. Moreover, we plan to study the synthesis of leadsto on bidirectional rings, and other elementary topologies (e.g., mesh, torus).

**Acknowledgment

**The author would like to thank Aly Farahat for fruitful discussions.