Local Reasoning for Parameterized First Order Protocols

TL;DR

This paper introduces a FOL-based framework for specifying and verifying distributed protocols locally, using an oracle for topology to simplify reasoning and enable scalable verification of properties like leader election.

Contribution

It presents a novel process-local specification framework with an oracle-based proof rule that simplifies reasoning about implicit network topologies in distributed protocols.

Findings

Framework effectively models protocols with local reasoning.

Proof rule reduces verification to a fixed number of processes.

Demonstrated on leader election in a ring topology.

Abstract

First Order Logic (FOL) is a powerful reasoning tool for program verification. Recent work on Ivy shows that FOL is well suited for verification of parameterized distributed systems. However, specifying many natural objects, such as a ring topology, in FOL is unexpectedly inconvenient. We present a framework based on FOL for specifying distributed multi-process protocols in a process-local manner together with an implicit network topology. In the specification framework, we provide an auto-active analysis technique to reason about the protocols locally, in a process-modular way. Our goal is to mirror the way designers often describe and reason about protocols. By hiding the topology behind the FOL structure, we simplify the modelling, but complicate the reasoning. To deal with that, we use an oracle for the topology to develop a sound and relatively complete proof rule that reduces reasoning about the implicit topology back to pure FOL. This completely avoids the need to axiomatize the topology. Using the rule, we establish a property that reduces verification to a fixed number of processes bounded by the size of local neighbourhoods. We show how to use the framework on two examples, including leader election on a ring.

Equations

$$\forall x,y,z$$

$$\forall w,x,y,z$$

$$\forall w,x,y$$

$$\forall a,b$$

$$\Sigma$$

$$\tau$$

$$Init:$$

$$Tr:$$

$$red\Rightarrow right.var:=b$$

$$Bad:$$

$$Const$$

$$Pred$$

$$Init(p)$$

$$Mod(p)$$

$$t_r(p)$$

$$t_b(p)$$

$$TrLoc(p)$$

$$\begin{array}{rlrl}{\phi }_0& \triangleq \forall \vec{p}\cdot Init(\vec{p})& \tau & \triangleq \exists p\cdot TrLoc(p)\wedge Frame(p)\end{array}$$

$$\begin{array}{rl}Frame(p)& \triangleq UnMod\wedge \left(\forall y\cdot y\notin Mod(p)\Rightarrow Unch(y))\right)\\ Unch(y)& \triangleq \left(\underset{P\in Pre{d}_S}{\bigwedge }\forall \vec{v}\cdot P(y,\vec{v})⟺P^{\prime }(y,\vec{v})\right)\wedge \left(\underset{f\in Fun{c}_S}{\bigwedge }\forall \vec{v}\cdot f(y,\vec{v})=f^{\prime }(y,\vec{v})\right)\\ UnMod& \triangleq \left(\underset{P\in Pre{d}_B}{\bigwedge }\forall \vec{v}\cdot P(\vec{v})⟺P^{\prime }(\vec{v})\right)\wedge \left(\underset{f\in Fun{c}_B}{\bigwedge }\forall \vec{v}\cdot f(\vec{v})=f^{\prime }(\vec{v})\right)\end{array}$$

$$InvOk\triangleq ((\forall \vec{p}\cdot Init(\vec{p}))\Rightarrow (\forall \vec{p}\cdot Inv(\vec{p})))\wedge ((\forall \vec{p}\cdot Inv(\vec{p}))\wedge \tau \Rightarrow (\forall \vec{p}\cdot {Inv}^{\prime }(\vec{p})))$$

$$\forall \vec{q}\cdot ({CrossInit}_{Top}(\vec{q})\Rightarrow {Inv}_{Top}(\vec{q}))$$

$$\forall p,\vec{q}\cdot (({CrossInv}_{Top}(Mod(p),\vec{q})\wedge \tau )\Rightarrow {Inv}_{Top}^{\prime }(\vec{q}))$$

$${\chi }_{Red}($$

$$((Red(left(p))\wedge Black(p)\wedge Red(right(p))\wedge p\ne q)\vee$$

$$(Black(left(p))\wedge Red(p)\wedge Black(right(p))\wedge distinct(left(p),right(p),q)))$$

$${Inv}_{red}(p)$$

$$\forall p\cdot {Init}_{red}(p)\Rightarrow {Inv}_{red}(p)$$

$$\forall p,q\cdot (Red(q)\wedge {Inv}_{red}(q)\wedge Red(left(p))\wedge {Inv}_{red}(left(p))\wedge$$

$$Black(p)\wedge {Inv}_{black}(p)\wedge Red(right(p))\wedge {Inv}_{red}(right(p))\wedge$$

$$p\ne q\wedge distinct(left(p),p,right(p)))\Rightarrow {Inv}_{red}^{\prime }(q)$$

$$\forall p,q\cdot (Red(q)\wedge {Inv}_{red}(q)\wedge Black(left(p))\wedge {Inv}_{black}(left(p))\wedge$$

$$Red(p)\wedge {Inv}_{red}(p)\wedge Black(right(p))\wedge {Inv}_{black}(right(p))\wedge$$

$$distinct(left(p),right(p),q)\wedge distinct(left(p),p,right(p)))\Rightarrow {Inv}_{red}^{\prime }(q)$$

$$V{C}_{P,1}({Inv}_{red},{Inv}_{black})\triangleq \text{eqref}eq:initred\wedge \text{eqref}eq:black\wedge \text{eqref}eq:vcExEnd$$

$$\begin{array}{rlrlrlrl}Const& \triangleq \{0_{/0}\}& Func& \triangleq \{{next}_{/1},{id}_{/1},{comp}_{/1}\}& Pred& \triangleq \{{\le }_{/2},{=}_{/2},{btw}_{/3}\}& \mathcal{C}& \triangleq \mathcal{B}\mathcal{T}\mathcal{W}\end{array}$$

$$\begin{array}{rlrlrl}\Sigma & \triangleq (Const,Func,Pred)& {LO}_0(\le )& \triangleq LO(\le )\wedge \forall x\cdot 0\le x& Mod(p)& \triangleq \{p,next(p)\}\end{array}$$

$$\begin{array}{rl}Init(p)& \triangleq \left({LO}_0(\le )\wedge btw(x,y,z)\Rightarrow (distinct(id(x),id(y),id(z))\wedge 0<id(x)\wedge comp(x)=0\right))\\ {\tau }_1(p)& \triangleq \left(id(p)\le comp(p)\Rightarrow \left({comp}^{\prime }(next(p))=comp(p)\right)\right)\\ {\tau }_2(p)& \triangleq \left(comp(p)\le id(p)\Rightarrow \left({comp}^{\prime }(next(p))=id(p)\right)\right)\\ TrLoc(p)& \triangleq \left(id(p)={id}^{\prime }(p)\wedge comp(p)={comp}^{\prime }(p)\wedge {id}^{\prime }(next(p))=id(next(p))\wedge {\tau }_1(p)\wedge {\tau }_2(p)\right)\end{array}$$

$$(btw(x,y,z)\wedge id(y)=comp(x))\Rightarrow (id(z)\le id(y))$$

$$(btw(x,y,z)\wedge id(x)=comp(x))\Rightarrow (id(y)\le id(x)\wedge id(z)\le id(x))$$

$$(btw(x,y,z)\wedge id(x)=comp(x)\wedge id(y)=comp(y))\Rightarrow x=y$$

Full text

1 Introduction

Auto-active[6] and automated verification engines are now commonly used to analyze the behavior of safety- and system-critical multi-process distributed systems. Applying the analysis techniques early in the design cycle has the added advantage that any errors or bugs found are less costly to fix than if one waits until the system is deployed. Therefore, it is typical to seek a proof of safety for parametric designs, where the number of participating program components is not yet determined, but the inter-process communciation fits a given pattern, as is common in routing or communication protocols, and other distributed systems.

Recently, Ivy [15] has been introduced as a novel auto-active verification technique (in the style of Dafny [6] for reasoning about parameterized systems. Ivy models protocols in First Order Logic (FOL). The verification conditions are compiled (with user help) to a decidable fragment of FOL, called Effectively Propositional Reasoning (EPR) [16]. Ivy is automatic in the sense that the verification engineer only provides an inductive invariant. Furthermore, unlike Dafny, it guarantees that the verification is never stuck inside the decision procedure (verification conditions are decidable).

One of the disadvantages of Ivy is that an engineer must formally specify the entire protocol, including the topology. For instance, in verifying the leader election on a ring, Ivy requires an explicit axiomatization of the ring topology, as shown in Fig. 1. The predicate $\mathit{btw}(x,y,z)$ means that a process $y$ is between processes $x$ and $z$ in the ring; similarly, $\mathit{next}(a,b)$ means that $b$ is an immediate neighbour of $a$ on the ring. All (finite) rings satisfy the axioms in Fig. 1. The converse is not true in general. For instance, take the rationals $\mathbb{Q}$ and let $\mathit{btw}(x,y,z)$ be defined as $x<y<z\vee y<z<x\vee z<x<y$. All axioms of $btw$ are satisfied, but the only consistent interpretation of $\mathit{next}$ is an empty set. This satisfies all the axioms, but does not define a ring. For the axioms in Fig. 1, all finite models of $\mathit{btw}$ and $\mathit{next}$ describe rings. This is not an issue for Ivy, since infinite models do not need to be considered for EPR. Such reasoning is non-trivial and is a burden on the verification engineer. As another example, we were not able to come up with an axiomatization of rings of alternating red and black nodes (shown in Fig. 2(a)) within EPR. In general, a complete axiomatization of the topology might be hard to construct.

In this paper, we propose to address this problem by specifying the topology independently of process behaviour. We present a framework which separates the two and provides a clean way to express the topology. We then specify our transitions locally, as this is a natural and common way to define protocols. Once these preliminaries are done, we provide a process-local proof rule to verify properties of the system. To generate the proof rule, we offload topological knowledge to an oracle that can answer questions about the topology. Finally, we prove various properties of the proof rule.

In summary, the paper makes the following contributions. First, in Sec. 3, we show how to model protocols locally in FOL. This is an alternative to the global modelling used in Ivy. Second, in Sec. 4, we show a proof rule with verification conditions (VC) in FOL, which are often in EPR. When the VC is in EPR, this gives an engineer a mechanical check of inductiveness. This allows reasoning about topology without axiomatizing it. Third, in Sec. 5, we show that our proof rule (a) satisfies a small model property, and (b) is relatively complete. The first guarantees the verification can be done on small process domains; the second ensures that our proof rule is fairly expressive.

We illustrate our approach on two examples. First, as a running example, motivated by [12], is a protocol on rings of alternating red and black nodes. These rings have only rotational symmetry, however, they have substantial local symmetry [7, 11, 12] consisting of two equivalence classes, one of red nodes, and one of black nodes. Second, in Sec. 6, we consider a modified version of the leader election protocol from Ivy [15]. This is of particular interest, since the local symmetry of [7, 11, 12] has not been applied to leader election. We thus extend [7, 11, 12] by both allowing more symmetries and infinite-state systems.

2 Preliminaries

FOL syntax and semantics.

We assume some familiarity with the standard concepts of many sorted First Order Logic (FOL). A signature $\Sigma$ consists of sorted predicates, functions, and constants. Terms are variables, constants, or (recursively) $k$-ary functions applied to $k$ other terms of the correct sort. For every $k$-ary predicate $P$ and $k$ terms $t_{1},\ldots,t_{k}$ of the appropriate sort for $P$, the formula $P(t_{1},\dots,t_{k})$ is a well-formed formula (wff). Wffs are then boolean combinations of formulae and universally or existentially quantified formulae. Namely, if $\psi$ and $\varphi$ are wffs, then so are $(\psi\wedge\varphi)$, $(\psi\vee\varphi)$,$(\neg\psi)$, $(\psi\Rightarrow\varphi)$,$(\psi\iff\varphi)$, $(\forall x\cdot\psi)$, and $(\exists x\cdot\psi)$. A variable $x$ in a formula $\psi$ is bound if it appears under the scope of a quantifier. A variable not bound is free. A wff with no free variables is called a sentence. For convenience, we often drop unnecessary parenthesis, and use $\top$ to denote true and $\bot$ to denote false.

An FOL interpretation $\mathcal{I}$ over a domain $D$ assigns every $k$-ary predicate $P$ a sort-appropriate semantic interpretation $\mathcal{I}(P):D^{k}\to\{T,F\}$; to every $k$-ary function $f$ a sort-appropriate interpretation $\mathcal{I}(f):D^{k}\to D$, and to every constant $c$ an element $\mathcal{I}(c)\in D$. Given an interpretation $\mathcal{I}$ and a sentence $\psi$, then either $\psi$ is true in $\mathcal{I}$ (denoted, $\mathcal{I}\models\psi$), or $\psi$ is false in $\mathcal{I}$ (denoted $\mathcal{I}\not\models\psi$). The definition of the models relation is defined on the structure of the formula as usual, for example, $\mathcal{I}\models(\varphi\land\psi)$ iff $\mathcal{I}\models\varphi$ and $\mathcal{I}\models\psi$.

We write $\mathcal{I}(\Sigma^{\prime})$ to denote a restriction of an interpretation $\mathcal{I}$ to a signature $\Sigma^{\prime}\subseteq\Sigma$. Given disjoint signatures $\Sigma$,$\Sigma^{\prime}$ and corresponding interpretations $\mathcal{I}$, $\mathcal{I}^{\prime}$ over a fixed domain $D$, we define $\mathcal{I}\oplus\mathcal{I}^{\prime}$ to be an interpretation of $\Sigma\cup\Sigma^{\prime}$ over domain $D$ defined such that $(\mathcal{I}\oplus\mathcal{I}^{\prime})(t)=\mathcal{I}(t)$ if $t\in\Sigma$, and $(\mathcal{I}\oplus\mathcal{I}^{\prime})(t)=\mathcal{I}^{\prime}(t)$ if $t\in\Sigma^{\prime}$. Given interpretation $\mathcal{I}$ and sub-domain $D^{\prime}\subseteq D$ where $D^{\prime}$ contains all constants, we let $\mathcal{I}(D^{\prime})$ be the interpretation restricted to domain $D^{\prime}$.

FOL modulo structures

We use an extension of FOL to describe structures, namely graphs. In this case, the signature $\Sigma$ is extended with some pre-defined functions and predicates, and the interpretations are restricted to particular intended interpretations of these additions to the signature. We identify a structure class $\mathcal{C}$ with its signature $\Sigma_{\mathcal{C}}$ and an intended interpretation. We write $\mathit{FOL}^{\mathcal{C}}$ for First Order Logic over the structure class $\mathcal{C}$. Common examples are FOL over strings, FOL over trees, and other finite structures.

A structure $\mathcal{S}=(D,\mathcal{I})$ is an intended interpretation $\mathcal{I}$ for structural predicates/functions $\Sigma_{\mathcal{C}}$ over an intended domain $D$. A set of structures is denoted $\mathcal{C}$. The syntax of $\mathit{FOL}^{\mathcal{C}}$ is given by the syntax for FOL with signature $\Sigma\uplus\Sigma_{\mathcal{C}}$ (where $\Sigma$ is an arbitrary disjoint signature). For semantics, any $FOL$ interpretation $\mathcal{I}$ of signature $\Sigma$ leads to an $FOL^{\mathcal{C}}$ interpretation $\mathcal{I}\oplus\mathcal{I}_{S}$ of the signature $\Sigma\uplus\Sigma_{\mathcal{C}}$. We write $\models_{\mathcal{C}}\varphi$ iff every $FOL^{\mathcal{C}}$ interpretation $\mathcal{I}$ satisfies $\mathcal{I}\models\varphi$. We introduce a process sort $\mathit{Proc}$ and require the intended domain $D$ to be exactly the set of $\mathit{Proc}$-sorted elements, so that we put our intended structure on the processes.

First Order Transition Systems.

We use First Order Transitions Systems from Ivy [15, 14]. While the original definition was restricted to the EPR fragment of FOL, we do not require this. A transition system is a tuple $Tr=(S,S_{0},R)$, where $S$ is a set of states, $S_{0}\subseteq S$ is a set of initial states, and $R\subseteq S\times S$ is a transition relation. A trace $\pi$ is a (finite or infinite) sequence of states $\pi=s_{0}\cdots s_{i}\cdots$ such that $s_{0}\in S_{0}$ and for every $0\leq i<|\pi|$, $(s_{i},s_{i+1})\in R$, where $|\pi|$ denotes the length of $\pi$, or $\infty$ if $\pi$ is infinite. A transition system may be augmented with a set $B\subseteq S$ of “bad” states. The system is safe iff all traces contain no bad states. A set of states $I$ is inductive iff $S_{0}\subseteq I$ and if $s\in I$ and $(s,s^{\prime})\in R$, then $s^{\prime}\in I$. Showing the existence of an inductive set $I$ that is disjoint from bad set $B$ suffices to show a transition system is safe.

A First-Order Transition System Specification (FOTSS) is a tuple $(\Sigma,\varphi_{0},\tau)$ where $\Sigma$ is an FOL signature, $\varphi_{0}$ is a sentence over $\Sigma$ and $\tau$ is a sentence over $\Sigma\uplus\Sigma^{\prime}$, where $\uplus$ denotes disjoint union and $\Sigma^{\prime}=\{t^{\prime}\mid t\in\Sigma\}$. The semantics of a FOTSS are given by First Order Transition Systems (FOTS). Let $D$ be a fixed domain. A FOTSS $(\Sigma,\varphi_{0},\tau)$ defines a FOTS over $D$ as follows: $S=\{\mathcal{I}\mid\mathcal{I}\text{ is an FOL interpretation over }D\}$, $S_{0}=\{\mathcal{I}\in S\mid\mathcal{I}\models\varphi_{0}\}$, and $R=\{(\mathcal{I}_{1},\mathcal{I}_{2})\in S\times S\mid\mathcal{I}_{1}\oplus\mathcal{I}^{\prime}_{2}\models\tau\}$, where $\mathcal{I}^{\prime}$ interprets $\Sigma^{\prime}$. We may augment a FOTSS with a FOL sentence $\mathit{Bad}$, giving bad states in the FOTS by $\mathcal{I}\in B$ iff $\mathcal{I}\vDash\mathit{Bad}$. A FOTSS is safe if all of its corresponding FOTS $Tr$ are safe, and is unsafe otherwise. That is, an FOTSS is unsafe if there exists at least one FOTS corresponding to it that has at least one execution that reaches a bad state. A common way to show a FOTSS is safe is to give a formula $\mathit{Inv}$ such that $\models\varphi_{0}\Rightarrow\mathit{Inv}$ and $\models\mathit{Inv}\wedge\tau\Rightarrow\mathit{Inv}^{\prime}$. Then for any FOTS over domain $D$, the set $I\subseteq S$ given by $I=\{\mathcal{I}\in S\mid\mathcal{I}\models\mathit{Inv}\}$ is an inductive set, and $\models\mathit{Inv}\Rightarrow\neg\mathit{Bad}$ then suffices to show that the state sets $I,B$ in the FOTS are disjoint. Finding an invariant $\mathit{Inv}$ satisfying the above proves the system safe.

Example 1

Consider the following FOTSS:

[TABLE]

where $Unch(Even,+,1)$ means that $Even$, $+$, and $1$ have identical interpretations in the pre- and post-states of $\tau$.

Our intention is to model a program that starts with an even number in a variable $var$ and increments $var$ by $2$ at every transition. It is an error if $var$ ever becomes odd. A natural invariant to conjecture is $\mathit{Inv}\triangleq Even(var)$. However, since the signature is uninterpreted, the FOTSS does not model our intention.

For example, let $D=\{0,1,2\}$, $\mathcal{I}_{0}(Even)=\{1,2\}$, $\mathcal{I}_{0}(1)=1$, $\mathcal{I}_{0}(+)(a,b)=a+b\mod 3$, and $\mathcal{I}_{0}(var)=1$. Thus, $\mathcal{I}_{0}\models\varphi_{0}$. Let $\mathcal{I}_{1}$ be the same as $\mathcal{I}_{0}$, except $\mathcal{I}_{1}(var)=0$. Then, $\mathcal{I}_{0}\oplus\mathcal{I}^{\prime}_{1}\models\tau$ and $\mathcal{I}_{1}\models\mathit{Bad}$. Thus, this FOTSS is unsafe.

One way to explicate our intention in Example 1 is to axiomatize the uninterpreted functions and relations in FOL as part of $\varphi_{0}$ and $\tau$. Another alternative is to restrict their interpretation by restricting the interpretation of FOL to a particular structure. This is the approach we take in this paper. We define a First-Order (relative to $\mathcal{C}$) Transition System Specification (FOCTSS).

We need to be able to talk about the structural objects in $\Sigma_{\mathcal{C}}$, and so we require that every FOCTSS $(\Sigma,\varphi_{0},\tau)$ be an FOTSS with $\Sigma_{\mathcal{C}}\subseteq\Sigma$. Once we have these structural objects, any structure $(D,\mathcal{I})\in\mathcal{C}$ gives a FOCTS with states $\mathcal{I}$ where $\mathcal{I}(\Sigma_{\mathcal{C}})=\mathcal{I}_{\mathcal{C}}$, initial states $\mathcal{I}$ where $\mathcal{I}\models\varphi_{0}$, transitions $(\mathcal{I}_{1},\mathcal{I}_{2})$ where $\mathcal{I}_{1}\oplus\mathcal{I}_{2}^{\prime}\models\tau$, and bad states $\mathcal{I}$ for which $\mathcal{I}\models\mathit{Bad}$.

3 First-Order Protocols

We introduce the notion of a First-Order Protocol (FOP) to simplify and restrict specifications in a FOTS. We choose restrictions to make our protocols asynchronous compositions of processes over static network topologies. Each process description is relative to its process neighbourhood. For example, a process operating on a ring has access to its immediate left and right neighbours, and transitions are restricted to these processes. This simplifies the modelling.

We begin with formalizing the concept of a network topology. As a running example, consider a Red-Black-Ring (RBR) topology, whose instance with 4 processes is shown in Fig. 2(a). Processes are connected in a ring of alternating Red and Black processes. Each process is connected to two neighbours using two links, labelled $\mathit{left}$ and $\mathit{right}$, respectively. From the example it is clear how to extend this topology to rings of arbitrary even size.

To formalize this, we assume that there is a unique sort $\mathit{Proc}$ for processes. Define $\Sigma^{\mathcal{C}}=\Sigma_{E}^{\mathcal{C}}\uplus\Sigma_{T}^{\mathcal{C}}$ to be a topological signature, where $\Sigma_{E}^{\mathcal{C}}$ is a set of unary $\mathit{Proc}$-sorted functions and $\Sigma_{T}^{\mathcal{C}}$ is a set of distinct $k$-ary $\mathit{Proc}$-sorted predicates ($k$ fixed). Functions in $\Sigma_{E}^{\mathcal{C}}$ correspond to communication edges, such as $\mathit{left}$ and $\mathit{right}$ in our example. Predicates in $\Sigma_{T}^{\mathcal{C}}$ correspond to classes of processes, such as $\mathit{Red}$ and $\mathit{Black}$ in our example. For simplicity, we assume that all classes have the same arity $k$. We often omit $k$ from the signature when it is contextually clear. We are now ready to define the concept of a network topology:

Definition 1

A network topology $\mathcal{C}$ over a topological signature $\Sigma^{\mathcal{C}}$ is a collection of directed graphs $G=(V,E)$ augmented with an edge labelling $\mathit{dir}:E\to\Sigma^{\mathcal{C}}_{E}$ and $k$-node labelling $\mathit{kind}:V^{k}\to\Sigma^{\mathcal{C}}_{T}$. Given a node $p$ in a graph $G=(V,E)$ from a network topology $\mathcal{C}$, the neighbourhood of $p$ is defined as $\mathit{nbd}(p)=\{p\}\cup\{q\mid(p,q)\in E\}$, and a neighbourhood of a tuple $\vec{p}=(p_{1},\dots,p_{k})$ is defined as $\mathit{nbd}(\vec{p})=\bigcup_{i=1}^{k}\mathit{nbd}(p_{i})$. A network topology is deterministic if for every distinct pair $q,r\in\mathit{nbd}(p)\setminus\{p\}$, $\mathit{dir}(p,q)\neq\mathit{dir}(p,r)$. That is, each neighbour of $p$ corresponds to a distinct name in $\Sigma_{E}$.

Given the signatures $\Sigma_{T}^{\mathcal{C}}$ and $\Sigma_{E}^{\mathcal{C}}$, the intended interpretation of a predicate $P\in\Sigma_{T}^{\mathcal{C}}$ is the set of all nodes in the network topology labelled by $P$, and the intended interpretation of a function $f\in\Sigma_{E}^{\mathcal{C}}$ is such that $f(p)=q$ if an edge $(p,q)$ is labelled by $f$ and $f(p)=p$, otherwise.

Each graph $G$ in a network topology $\mathcal{C}$ provides a possible intended interpretation for the sort of processes $\mathit{Proc}$, and the edge and node labelling provide the intended interpretation for predicates and functions in $\Sigma^{\mathcal{C}}$.

Example 2

For our running example, consider an informal description of the protocol shown in Fig. 2(b) described by a set of guarded commands. The protocol is intended to be executed on the RBR topology shown in Fig. 2(a). Initially, all processes start with their state variable $var$ set to a special constant $null$. Then, at each step, a non-deterministically chosen process, sends a color to its right. Every black process sends a red color $r$, and every red process sends a black color $b$. It is bad if a Red process ever gets a black color.

To formalize the topology, for each $n>1$, let $G_{n}=(V_{n},E_{n})$, where $V_{n}=\{p^{n}_{i}\mid 0\leq i<2n\}$, and $E_{n}=\{(p^{n}_{i},p^{n}_{j})\mid|i-j|\bmod 2n=1\}$. The edge labelling is given by $\mathit{dir}(p^{n}_{i},p^{n}_{j})=\mathit{right}$ if $j=(i+1)\mod n$ and $\mathit{left}$ if $j=(i-1)\mod n$. Processes have colour $\mathit{kind}(p^{n}_{i})=\mathit{Red}$ if $i$ is even, and $\mathit{Black}$ if $i$ is odd. Finally, we define $\mathcal{RBR}=\{G_{n}\mid n\geq 2\}$ as the class of Red-Black Rings (RBR). ∎

Note that any set of graphs $\mathcal{G}$ with an upper bound on the out-degree of any vertex can be given a finite labelling according to the above.

First-Order Protocols.

Once we have specified the topology, we want to establish how processes transition. We define the syntax and semantics of a protocol.

A protocol signature $\Sigma$ is a disjoint union of a topological signature $\Sigma_{\mathcal{C}}$, a state signature $\Sigma_{S}$, and a background signature $\Sigma_{B}$. Recall that all functions and relations in $\Sigma_{\mathcal{C}}$ are of sort $\mathit{Proc}$. All elements of $\Sigma_{S}$ have arity of at least $1$ with the first and only the first argument of sort $\mathit{Proc}$. Elements of $\Sigma_{B}$ do not allow arguments of sort $\mathit{Proc}$ at all. Intuitively, elements of $\Sigma_{\mathcal{C}}$ describe how processes are connected, elements of $\Sigma_{S}$ describe what is true in the current state of some process, and elements of $\Sigma_{B}$ provide background theories, such as laws of arithmetic and uninterpreted functions.

For an interpretation $\mathcal{I}$, and a set of processes $P\subseteq\mathcal{I}(Proc)$, we write $\mathcal{I}(\Sigma_{S})(P)$ for the interpretation $\mathcal{I}(\Sigma_{S})$ restricted to processes in $P$. Intuitively, we look only at the states of $P$ and ignore the states of all other processes.

Definition 2

A First-Order Protocol (FO-protocol) is a tuple $P=(\Sigma,Init(\vec{p}),$ $Mod(p),\mathit{TrLoc}(p),\mathcal{C})$, where $\Sigma$ is a protocol signature; $p$ is a free variable of sort $\mathit{Proc}$, $Init(\vec{p})$ is a formula with $k$ free variables $\vec{p}$ of sort $\mathit{Proc}$; $Mod(p)$ is a set of terms $\{t(p)\mid t\in\mathit{dir}(E)\}\cup\{p\}$; $TrLoc(p)$ is a formula over the signature $\Sigma\cup\Sigma^{\prime}$, and $\mathcal{C}$ is a network topology. Furthermore, $Init(\vec{p})$ is of the form $\bigwedge_{P\in\Sigma_{T}}\left(P(\vec{p})\Rightarrow Init_{P}(\vec{p})\right)$, where the arity of $P$ is $|\vec{p}|$, and each $Init_{P}$ is a formula over $\Sigma\setminus\Sigma_{\mathcal{C}}$ (an initial state described without reference to topology for each relevant topological class); and terms of sort $\mathit{Proc}$ occurring in $\mathit{TrLoc}(p)$ are a subset of $\mathit{Mod}(p)$.

A formal description of our running example is given in Figure 3 as a FO-protocol. We define the signature including $\Sigma_{\mathcal{C}}=\{\mathit{left},\mathit{right},\mathit{Red},\mathit{Black}\}$, the initial states $\mathit{Init}(p)$ in the restricted form, and modification set $\mathit{Mod}(p)$, where we allow processes to only write to their local neighbourhood. Next we specify two kinds of transitions, a red $t_{r}$ and a black $t_{b}$ transition. Each writes to their right neighbour the colour they expect that process to be. Each process $p$ does not change the var states of $p,\mathit{left}(p)\in\mathit{Mod}(p)$. Finally, we specify our local transitions $\mathit{TrLoc}(p)$ by allowing each of the sub-transitions. Note that all process-sorted terms in $\mathit{TrLoc}(p)$ are in $\mathit{Mod}(p)=\{\mathit{left}(p),p,\mathit{right}(p)\}$, and we are allowed to call on topological predicates in $\mathit{TrLoc}$, finishing our specification.

Furthermore, note that the semantic local neighbourhood $\mathit{nbd}(p)$ and the set of syntactic terms in $Mod(p)$ have been connected. Namely, for every edge $(p,q)\in E$, there is a term $t(p)\in Mod(p)$ to refer to $q$, and for every term $t(p)\in Mod(p)$, we will refer to some process in the neighbourhood of $p$.

The semantics of a protocol $P$ are given be an FOCTSS as shown in Fig. 4. The protocol signature $\Sigma$ is the same in the FOCTSS as in the FOP. Initially, $\varphi_{0}$ requires that all $k$-tuples of a given topology satisfy a topology-specific initial state. Finally, to take a transition $\tau$, some process takes a local transition $\mathit{TrLoc}(p)$ modifying states of processes that can be described using the terms in $\mathit{Mod}(p)$. $Unch(y)$ guarantees that the transition does not affect local state of processes that are outside of $\mathit{Mod}(p)$. Finally, $UnMod$ makes all functions and predicates in the background signature retain their interpretation during the transition. Overall, this describes a general multiprocess asynchronous protocol.

This definition of a FO-protocol places some added structure on the notion of FOTSS. It restricts how transition systems can be specified, which might seem like a drawback. On the contrary, the added structure provides two benefits. First, it removes the need for axiomatizing the network topology, since the topology is given semantically by $\mathcal{C}$. Second, the system guarantees to model asynchronous composition of processes whose local transition relation is given by $\mathit{TrLoc}$ – a common framework for specifying and reasoning about protocols.

To show safety of such a system, we will be concerned with invariants which only discuss a few processes, say $\mathit{Inv}(\vec{p})$ where $\vec{p}=p_{1},\dots,p_{k}$. Then our FO-invariants will be of the form $\forall\vec{p}\cdot\mathit{Inv}(\vec{p})$, and substituting $\varphi_{0}$ into our background, we find a natural check for when a given formula is inductive:

[TABLE]

Indeed, by unpacking definitions, one sees that $\models_{\mathcal{C}}\mathit{InvOk}$ means that every state on any trace of a FOCTS satisfies $\forall\vec{p}\cdot\mathit{Inv}(\vec{p})$, and thus it suffices to check that $\models_{\mathcal{C}}\forall\vec{p}\cdot\mathit{Inv}(\vec{p})\Rightarrow\neg\mathit{Bad}$ to prove safety. We, however, will focus on the task of verifying a candidate formula as inductive or not.

To decide if a candidate is inductive or not requires reasoning in $\mathit{FOL}^{\mathcal{C}}$. However, reasoning about FOL extended with an arbitrary topology is difficult (or undecidable in general). We would like to reduce the verification problem to pure FOL. One solution is to axiomatize the topology in FOL – this is the approach taken by Ivy[15]. Another approach is to use properties of the topology to reduce reasoning about FO-protocols to FOL. This is similar to the use of topology to reduce reasoning about parameterized finite-state systems to reasoning about finite combinations of finite-state systems in [11]. In the next section, we show how this approach can be extended to FO-protocols.

4 Verifying FO-Protocols using First Order Logic

In this section, we present a technique for reducing verification of FO-protocols over a given topology $\mathcal{C}$ to a decision problem in pure FOL. We assume that we are given a (modular) inductive invariant $\forall\vec{q}\cdot\mathit{Inv}(\vec{q})$ of the form $\left(\forall\vec{q}\cdot\bigwedge_{\mathit{Top}\in\Sigma^{\mathcal{C}}_{T}}\mathit{Top}(\vec{q})\Rightarrow\mathit{Inv}_{\mathit{Top}}(\vec{q})\right)$. That is, $\mathit{Inv}$ has a local inductive invariant $\mathit{Inv}_{\mathit{Top}(\vec{q})}$ for each topological class $\mathit{Top}$.

Given a First-Order Protocol and candidate invariant, we want to know if $\models_{\mathit{FOL}_{\mathcal{C}}}\mathit{InvOk}$. But deciding this is hard, and so we show that deciding validity of $\mathit{InvOk}$ can be done in pure FOL using modular verification conditions in the style of Owicki-Gries [13] and Paramaterized Compositional Model Checking [11].

The input to our procedure is a formula $\mathit{Inv}_{\mathit{Top}}$ over signature $\Sigma_{B}\uplus\Sigma_{S}$ for each topological class $\mathit{Top}\in\Sigma^{\mathcal{C}}_{T}$. The VC is a collection of sentences ensuring that for each tuple of processes $\vec{q}$ in a topological class $\mathit{Top}$, $\mathit{Inv}_{\mathit{Top}}(\vec{q})$ is true initially, is stable under a transition of one process in $\vec{q}$, and is stable under interference by any other process $p$ whose execution might affect some $q_{i}\in\vec{q}$. If the VC is FOL-valid, an inductive invariant has been found. If not, there will be a local violation to inductiveness, which may correspond to a global violation.

Formally, the VC is a collection of statements of the following two forms:

[TABLE]

Statements of the first form require that every local neighbourhood of $\vec{q}$ that satisfies all appropriate initial states also satisfies $\vec{q}$’s invariant. Statements of the second form capture both transitions where $p=q_{i}$ for some $i$, or process $p$ acts and modifies $q_{i}\in\mathit{nbd}(p)$, since $p$ is quantified universally. All that remains is to formally construct the statements $\mathit{CrossInit},\mathit{CrossInv}$. In order to do so, we will construct a characteristic local neighbourhood of a process tuple $\vec{q}$. We will want to use a similar construction for both, and so generalize to the characteristic that $\vec{q}$ must satisfy in addition to other processes given by an arbitrary set $A$.

We will say that formula $\psi$ is a valid candidate for $\chi_{\mathit{Top}}(A,\vec{q})$ when it is (1) over signature $\Sigma_{T}\cup\Sigma_{E}\cup\{=\}$, (2) contains only terms $A\cup\{q_{i}\mid q_{i}\in\vec{q}\}$, and (3) is in CNF and all literals from $\Sigma_{T}$ appear in positive form. Intuitively, we will want to capture when elements of $A,\vec{q}$ satisfy various topological notions given by signature $\Sigma_{E}\cup\{=\}$. We also never want to force some processes to be outside of some topological class. We let $\chi_{\mathit{Top}}(A,\vec{q})$ be the strongest candidate that satisfies $\models_{\mathcal{C}}\forall\vec{q}\cdot\mathit{Top}(\vec{q})\Rightarrow\chi_{\mathit{Top}}(A,\vec{q})$. Intuitively, $\chi$ is a formula that captures all topological knowledge derivable from the topology given that we know that $\mathit{Top}(\vec{q})$ holds. For instance, in $\mathcal{RBR}$, we have $\chi_{\mathit{Red}}(\emptyset,q)=\mathit{Red}(q)$, while expanding this for $A=\{\mathit{left}(p),p,\mathit{right}(p)\}$ results in the following formula.

[TABLE]

These characteristics are illustrated in Figure 5. When we just look at $\chi_{\mathit{Red}}(\emptyset,q)$, we find $q$ is red. However, if we expand our local reasoning to the characteristic $\chi_{\mathit{Red}}(\mathit{Mod}(p),q)$, we find that there are two options given by $\mathcal{RBR}$. One option is $p$ is red, and $q=p$ is optional (dotted lines), while $q\neq\mathit{left}(p),\mathit{right}(p)$. Alternatively, $p$ is black, and $q\neq p$, but $q$ could be $\mathit{left}(p),\mathit{right}(p)$, or neither.

Once we have $\chi_{\mathit{Top}}(A,\vec{q})$, we can define our statements $\mathit{CrossInit}_{\mathit{Top}},$ $\mathit{CrossInv}_{\mathit{Top}}$. First, $\mathit{CrossInit}_{\mathit{Top}}(\vec{q})$ is obtained from $\chi_{\mathit{Top}}(\emptyset,\vec{q})$ by replacing every instance of $\mathit{Top}_{i}^{\prime}(\vec{q})$ with $\mathit{Init}_{\mathit{Top}_{i}}^{\prime}(\vec{q})$. We build our interference constraints in a similar way. We construct $\mathit{CrossInv}_{\mathit{Top}}(\vec{q})$ by modifying $\chi_{\mathit{Top}}(\mathit{Mod}(p),\vec{q})$. Namely, we obtain $\mathit{CrossInv}_{\mathit{Top}}(\mathit{Mod}(p),\vec{q})$ from $\chi_{\mathit{Top}}(\mathit{Mod}(p),\vec{q})$ by replacing every instance of $\mathit{Top}_{i}^{\prime}(\vec{q})$ with $\mathit{Top}_{i}^{\prime}(\vec{q})\wedge\mathit{Inv}_{\mathit{Top}_{i}}^{\prime}(\vec{q})$.

Example 3

The VC generated by the $\mathcal{RBR}$ topology may be partitioned into $\mathit{VC}_{\mathit{Red}}$ and $\mathit{VC}_{\mathit{Black}}$, each consisting of the statements whose conclusions are $\mathit{Inv}_{\mathit{Red}},\mathit{Inv}_{\mathit{Red}}^{\prime}$ and $\mathit{Inv}_{\mathit{black}},\mathit{Inv}_{\mathit{black}}^{\prime}$, respectively. $\mathit{VC}_{\mathit{Red}}$ is shown in Fig. 6. The conditions for $\mathit{VC}_{\mathit{Black}}$ are symmetric. One can check that

[TABLE]

is an inductive invariant for the protocol in Fig. 2. ∎

In practice, the role of the oracle can be filled by a verification engineer. A description of local neighbourhoods starts by allowing all possible neighbourhoods, and as counter-examples disallowed by the topology occur, a verifier may dismiss local configurations that cannot occur on the topology.

5 Soundness and Completeness

In this section, we present soundness and relative completeness of our verification procedure from Section 4.

Soundness.

To show soundness, we present a model-theoretic argument to show that whenever the verification condition from Section 4 is valid in FOL, then the condition $\mathit{InvOk}$ is valid in FOL extended with the given topology $\mathcal{C}$.

Theorem 5.1

Given a FO-protocol $P$ and a local invariant per topological class* $\mathit{Inv}_{\mathit{Top}_{1}}(\vec{p}),\ldots,\mathit{Inv}_{\mathit{Top}_{n}}(\vec{p})$, if $\vDash VC(\mathit{Inv})$, then $\vDash_{\mathcal{C}}InvOk(\mathit{Inv})$.*

Proof

We show that $\mathit{InvOk}(\mathit{Inv})$ is valid in $\mathit{FOL}^{\mathcal{C}}$ by showing that any pair of $\mathit{FOL}^{\mathcal{C}}$ interpretations $\mathcal{I}$ and $\mathcal{I}^{\prime}$ satisfy $VC(\mathit{Inv})$ as FOL interpretations, and this is strong enough to guarantee $\mathcal{I}\oplus\mathcal{I}^{\prime}\models\mathit{InvOk}(\mathit{Inv})$.

Let $\mathcal{I},\mathcal{I}^{\prime}$ be $FOL^{\mathcal{C}}$ interpretations over some $G=(V,E)\in\mathcal{C}$. Then $\mathcal{I}\oplus\mathcal{I}^{\prime}\models VC(\mathit{Inv})$ because $VC(\mathit{Inv})$ is valid and $\mathcal{I}\oplus\mathcal{I}^{\prime}$ is an FOL interpretation.

We first show that $\mathcal{I}\models(\forall\vec{p}\cdot\mathit{Init}(\vec{p})\Rightarrow\forall\vec{p}\cdot\mathit{Inv}(\vec{p}))$. Suppose that $\mathcal{I}\vDash\forall\vec{p}\cdot\mathit{Init}(\vec{p})$. Let $\vec{p}$ be an aribtrary tuple in $G$. If $\mathcal{I}\models\neg\mathit{Top}_{i}(\vec{p})$ for every $\mathit{Top}_{i}\in\Sigma_{T}$, then $\mathit{Inv}(\vec{p})$ follows vacuously. Otherwise, suppose $\mathcal{I}\models\mathit{Top}_{i}(\vec{p})$. Then by definition of $\chi$, we obtain $\mathcal{I}\models\chi_{\mathit{Top}_{i}}(\emptyset,\vec{p})$ since $\mathcal{I}\models\mathit{Top}_{i}(\vec{p})\Rightarrow\chi_{\mathit{Top}_{i}}(\vec{p})$. Since $\mathcal{I}\models\forall\vec{p}\cdot\mathit{Init}(\vec{p})$, this gives us that $\mathcal{I}\models\mathit{CrossInit}(\vec{p})$ (for any $\mathit{Top}_{j}(\vec{p}^{\prime})$ in $\chi_{\mathit{Top}_{i}}(\vec{p})$, find that $\mathit{Init}(\vec{p}^{\prime})$, and thus $\mathit{Top}_{j}(\vec{p}^{\prime})$ implies $\mathit{Init}_{\mathit{Top}_{j}}(\vec{p}^{\prime})$, giving $\mathit{CrossInit}$). Since $\mathcal{I}\models\mathit{CrossInit}_{\mathit{Top}_{i}}(\vec{p})$ and $\mathcal{I}\models VC$, we get $\mathcal{I}\models\mathit{CrossInit}_{\mathit{Top}_{i}}(\vec{p})\Rightarrow\mathit{Inv}_{\mathit{Top}_{i}}(\vec{p})$, finally giving us $\mathcal{I}\models\mathit{Inv}_{\mathit{Top}_{i}}(\vec{p})$, as desired.

Second, we show that $\mathcal{I}\oplus\mathcal{I}^{\prime}\models(\forall\vec{p}\cdot\mathit{Inv}(\vec{p}))\wedge\tau\Rightarrow(\forall\vec{p}\cdot\mathit{Inv}(\vec{p}))$. Suppose that $\mathcal{I}\models\forall\vec{p}\cdot\mathit{Inv}(\vec{p})$ and $\mathcal{I}\oplus\mathcal{I}^{\prime}\models\mathit{TrLoc}(p)\wedge\mathit{Frame}(p)$ for some $p\in V$. We show that $\mathcal{I}^{\prime}\models\forall\vec{q}\cdot\mathit{Inv}^{\prime}(\vec{q})$. Let $\vec{q}\in V^{k}$ be an arbitrary process tuple. If $\mathcal{I}^{\prime}\not\models\mathit{Top}_{i}(\vec{q})$ for all $1\leq i\leq n$, then $\mathcal{I}^{\prime}\models\mathit{Inv}^{\prime}(\vec{q})$ vacuously. Suppose $\mathcal{I}^{\prime}\models\mathit{Top}_{i}(\vec{q})$ for some $\mathit{Top}_{i}\in\Sigma_{T}$. Then $\mathcal{I}\models\mathit{Top}_{i}(\vec{q})\Rightarrow\chi_{\mathit{Top}_{i}}(\mathit{Mod}(p),\vec{q})$, and so $\mathcal{I}\models\chi_{\mathit{Top}_{i}}(\mathit{Mod}(p),\vec{q})$. Again by instantiating $\forall\vec{p}\cdot\mathit{Inv}(\vec{p})$ on terms in $\mathit{Mod}(p),\vec{q}$, we may obtain that $\mathcal{I}\models\mathit{CrossInv}(\mathit{Mod}(p),\vec{q})$. Combined, we have $\mathcal{I}\oplus\mathcal{I}^{\prime}\models\mathit{CrossInv}(\mathit{Mod}(p),\vec{q})\wedge\tau$. Applying $VC$ finally gives $\mathit{Inv}_{\mathit{Top}_{i}}(\vec{q})$.∎

Intuitively, the correctness of Theorem 5.1 follows from the fact that any interpretation under $\mathit{FOL}^{\mathcal{C}}$ is also an interpretation under $\mathit{FOL}$, and all preconditions generated for VC are true under $\mathit{FOL}^{\mathcal{C}}$ interpretation.

Small model property.

Checking validity of universally quantified statements in FOL is in the fragment EPR, and thus we obtain a result saying that we only need to consider models of a given size. This means that a FOL solver needs to only reason about finitely many elements of sort $\mathit{Proc}$. It further means that topologies such as $\mathcal{RBR}$ may be difficult to compile to EPR in Ivy, but our methodology guarantees our verifications will be in EPR.

Theorem 5.2

If $\models VC(\mathit{Inv})$ for all process domains of size at most $|\mathit{Mod}(p)|+k$, then $\models_{\mathcal{C}}\mathit{InvOk}(\mathit{Inv})$.

Proof

By contrapositive, suppose $\not\vDash_{\mathcal{C}}InvOk(\mathit{Inv})$. Then, by Theorem 5.1, $\not\models VC(\mathit{Inv})$. Let $\mathcal{I}\oplus\mathcal{I}^{\prime}$ be a falsifying interpretation. It contains an assignment to $\mathit{Mod}(p)$ and $\vec{q}$, or to $\vec{p}$ that makes at least one statement in $VC(\mathit{Inv})$ false. Then, $(\mathcal{I}\oplus\mathcal{I}^{\prime})(\mathit{Mod}(p)\cup\vec{q})$ or $\mathcal{I}(\vec{p})$ $\mathit{Mod}(p),\vec{q}$ or $\vec{p}$ to make some statement in $VC$ unsatisfiable. Then $\mathcal{I}\oplus\mathcal{I}^{\prime}(\mathit{Mod}(p)\cup\vec{q})$ or $\mathcal{I}(\vec{p})$ is also a counter-model to $VC(\mathit{Inv})$, but with at most $|Mod(p)|+k$ elements of sort $\mathit{Proc}$.

Relative Completeness.

We show that our method is relatively complete for local invariants that satisfy the completability condition. Let $\varphi(\vec{p})$ be a formula of the form $\bigwedge^{n}_{i=1}(\mathit{Top}_{i}(\vec{p})\Rightarrow\varphi_{\mathit{Top}_{i}}(\vec{p}))$ with $\varphi_{\mathit{Top}_{i}}(\vec{p})$ over the signature $\Sigma_{S}\cup\Sigma_{B}$. Intuitively, $\varphi(\vec{p})$ is completable if every interpretation $\mathcal{I}$ that satisfies $\forall\vec{p}\cdot\varphi(\vec{p})$ and is consistent with some $\mathcal{C}$-interpretation $\mathcal{I}_{G}$ can be extended to a full $\mathcal{C}$-interpretation (not necessarily $\mathcal{I}_{G}$) that satisfies $\forall\vec{p}\cdot\varphi(\vec{p})$. Formally, $\varphi$ is completable relative to topology $\mathcal{C}$ iff for every interpretation $\mathcal{I}$ with domain $U\subseteq V$ for $G=(V,E)\in\mathcal{C}$ with an intended interpretation $\mathcal{I}_{G}$ such that $(\mathcal{I}\uplus\mathcal{I}_{G})(U)\models\forall\vec{p}\cdot\varphi(\vec{p})$, there exists an interpretation $\mathcal{J}$ with domain $V$ s.t. $(\mathcal{J}\uplus\mathcal{I}_{G})\models\forall\vec{p}\cdot\varphi$ and $\mathcal{I}(U)=\mathcal{J}(U)$. Furthermore, we need a lemma expressing that the chacteristic formula $\chi_{\mathit{Top}}(A,\vec{q})$ captures all the information we care about for a given topological neighbourhood of $A,\vec{q}$.

Lemma 1

If FOL interpretation $\mathcal{I}$ of signature $\Sigma_{\mathcal{C}}$ satisfies $\mathcal{I}\models\chi_{\mathit{Top}}(A,\vec{q})$, then there exists a $\mathcal{C}$ interpretation $\mathcal{J}$ of the same signature with $\mathcal{J}\models\chi_{\mathit{Top}}(A,\vec{q})$ and $\mathcal{I}\models t_{i}=t_{j}$ iff $\mathcal{J}\models t_{i}=t_{j}$ for terms $t_{i},t_{j}\in A\cup\vec{q}$.

Proof

Let $\mathcal{I}\models\chi_{\mathit{Top}}(A,\vec{q})$. Let $\varphi(A,\vec{q})$ be the conjunction of all atomic formulae over the signature $\{=\}$ and statements $\neg\mathit{Top}_{j}(\vec{q}^{\prime})$ that is true of elements of $A,\vec{q}$ in interpretation $\mathcal{I}$. If no $\mathcal{C}$ interpretation $\mathcal{J}\models\mathit{Top}(\vec{q})\wedge\varphi(A,\vec{q})$, then we can add the clause $\neg\varphi(A,\vec{q})$ to $\chi_{\mathit{Top}}(A,\vec{q})$, thus strengthening it (this is stronger since $\mathcal{I}\models\mathit{Top}(\vec{q}),\not\models\neg\varphi(A,\vec{q})$, and is true of every interpretation modelling $\mathit{Top}(\vec{q})$). However, this violates the assumptions that $\chi_{\mathit{Top}}$ is as strong as possible. Thus, some $\mathcal{J}\models\mathit{Top}(\vec{q})\wedge\varphi(A,\vec{q})$. Note that $\mathcal{J}$ already satisfies $t_{i}=t_{j}$ iff $\mathcal{I}$ satisfies $t_{i}=t_{j}$ since every statement of $=,\neq$ is included in $\varphi(A,\vec{q})$. Finally, since $\mathcal{J}$ is a $\mathcal{C}$ interpretation and $\mathcal{I}^{\prime}\models\mathit{Top}(\vec{q})$, then $\mathcal{I}^{\prime}\models\chi_{\mathit{Top}}(A,\vec{q})$ by definition.∎

Theorem 5.3

Given an FO-protocol $P$, if $\models_{\mathcal{C}}InvOk(\mathit{Inv})$ and both $Inv(\vec{p})$ and $Init(\vec{p})$ are completable relative to $\mathcal{C}$, then $\models VC(\mathit{Inv})$.

Proof

By contra-positive, we show that given a completable local invariant $\mathit{Inv}(\vec{p})$, if $VC(\mathit{Inv})$ is falsifiable in $\mathit{FOL}$, then $\mathit{InvOk}(\mathit{Inv})$ is falsifiable in $\mathit{FOL}^{\mathcal{C}}$. Suppose $VC(\mathit{Inv})$ is not valid, and let $\mathcal{I}\oplus\mathcal{I}^{\prime}$ by such that $\mathcal{I}\oplus\mathcal{I}^{\prime}\not\models VC(\mathit{Inv})$. We consider two cases – a violation initially or inductively.

Case 1: Initialization: For some processes $\vec{p}=\langle p_{1},\ldots,p_{k}\rangle$ and $1\leq i\leq|\Sigma^{\mathcal{C}}_{T}|$, $\mathcal{I}\models\mathit{CrossInit}_{\mathit{Top}_{i}}(\vec{p})$ and $\mathcal{I}\not\models\mathit{Inv}_{\mathit{Top}_{i}}(\vec{p})$. Modify $\mathcal{I}(\Sigma_{T})$ for every $\vec{q}$ so that $\mathit{Top}_{j}(\vec{q})$ is interpreted to be true iff $\mathit{Init}_{\mathit{Top}_{j}}(\vec{q})$ is true. Noting that all invariants and initial conditions are outside of the signature $\Sigma_{T}$, we observe that this is done without loss of generality. Since $\mathcal{I}\models\mathit{CrossInit}_{\mathit{Top}_{i}}(\vec{p})$, we conclude now that $\mathcal{I}\models\chi_{\emptyset,\mathit{Top}_{i}}(\vec{p})$. Applying Lemma 1 to $\mathcal{I}(\Sigma_{\mathcal{C}})$, we get a $\mathcal{C}$ interpretation $\mathcal{J}\models\chi_{\mathit{Top}_{i}}(\emptyset,\vec{p}^{\mathcal{C}})$. Since this model has the same equalities of terms $\vec{p}^{\mathcal{C}}$ in $\mathcal{J}$ as $\vec{p}$ in $\mathcal{I}$, we may copy the states $\mathcal{I}(\Sigma_{S})(p_{i})$ to $\mathcal{J}(\Sigma_{S})(p_{i})$. Set $\mathcal{J}(\Sigma_{B})=\mathcal{I}(\Sigma_{B})$. Since $\mathit{Init}$ is completable by assumption, we complete $\mathcal{J}(\Sigma_{S}\cup\Sigma_{B})(\vec{p})$ to $\mathcal{J}(\Sigma_{S}\cup\Sigma_{B})$, completing our construction of $\mathcal{J}$ interpreting $\Sigma_{\mathcal{C}}\cup\Sigma_{S}\cup\Sigma_{B}$. Note that $\mathcal{J}\models\forall\vec{p}\cdot\mathit{Init}(\vec{p})$, but $\mathcal{J}\models\neg\mathit{Top}_{i}(\vec{p}^{\mathcal{C}})\wedge\mathit{Inv}_{\mathit{Top}_{i}}(\vec{p}^{\mathcal{C}})$, thus showing that $\mathit{InvOk}(\mathit{Inv})$ is falsifable in $\mathit{FOL}^{\mathcal{C}}$.

Case 2: Inductiveness: For some $p,\vec{q}$, and $1\leq i\leq|\Sigma^{\mathcal{C}}_{T}|$, we have $\mathcal{I}\models\mathit{CrossInv}_{\mathit{Top}_{i}}(\mathit{Mod}(p),\vec{q})$, $(\mathcal{I}\oplus\mathcal{I}^{\prime})\models\mathit{TrLoc}(p)\wedge\mathit{Frame}(p)$, and $\mathcal{I}^{\prime}\not\models\mathit{Inv}_{\mathit{Top}_{i}}(\vec{q})$. By construction, $\models\mathit{CrossInv}(\mathit{Mod}(p),\vec{q})\Rightarrow\chi_{\mathit{Top}_{i}}(\mathit{Mod}(p),\vec{q})$. Applying Lemma 1 to $\mathcal{I}(\Sigma_{\mathcal{C}})\models\chi_{\mathit{Top}_{i}}(\mathit{Mod}(p),\vec{q})$, we get a $\mathcal{C}$ interpretation of $\Sigma^{\mathcal{C}}_{T}$ which $\mathcal{J}\models\chi_{\mathit{Top}_{i}}(\mathit{Mod}(p^{\mathcal{C}}),\vec{q}^{\mathcal{C}})$. We extend this to a full model $\mathcal{J}$ of signature $\Sigma_{\mathcal{C}}\cup\Sigma_{S}\cup\Sigma_{B}$. We set $\mathcal{J}^{\prime}(\Sigma_{\mathcal{C}})=\mathcal{J}(\Sigma_{\mathcal{C}})$. Then, since $\mathcal{J}$ and $\mathcal{I}$, and $\mathcal{J}^{\prime}$ and $\mathcal{I}^{\prime}$ share equalties across terms in $\mathit{Mod}(p)\cup\vec{q}$ and $\mathit{Mod}(p^{\mathcal{C}})\cup\vec{q}^{\mathcal{C}}$, we can lift states from terms $t\in\mathit{Mod}(p)\cup\vec{q}$ by $\mathcal{J}(\Sigma_{S}\cup\Sigma_{B})(t^{\mathcal{C}})\triangleq\mathcal{I}(\Sigma_{S}\cup\Sigma_{B})(t)$ and $\mathcal{J}^{\prime}(\Sigma_{S})(t^{\mathcal{C}})\triangleq\mathcal{I}^{\prime}(\Sigma_{S})(t)$. Since $\mathit{Inv}$ is completable, we complete this interpretation with $\mathcal{J}(\Sigma_{S}\cup\Sigma_{B})$ and clone the completion to $\mathcal{J}^{\prime}(\Sigma_{S}\cup\Sigma_{B})(V\setminus(\mathit{Mod}(p)\cup\vec{q}))$. Overall, this completes the interpretations $\mathcal{J}\oplus\mathcal{J}^{\prime}$.

Note that $\mathcal{J}\models\forall\vec{p}\cdot\mathit{Inv}(\vec{p})$ by construction. Similarly, $\mathcal{J}\oplus\mathcal{J}^{\prime}\models\tau$ since $\mathcal{I}\oplus\mathcal{I}^{\prime}\models\tau(p)$ and $\mathit{Mod}(p)$ terms are lifted directly from $\mathcal{I}$ and $\mathcal{I}^{\prime}$ to $\mathcal{J}$ and $\mathcal{J}^{\prime}$. Finally, $\mathcal{J}^{\prime}\models\neg\mathit{Inv}_{\mathit{Top}_{i}}(\vec{q})$ since $\mathcal{J}^{\prime}(\Sigma_{S})$ is lifted directly from $\mathcal{I}^{\prime}(\Sigma_{S})$, which is the language of invariants. Thus, we have shown that $\mathit{InvOk}(\mathit{Inv})$ is falsifiable in $\mathit{FOL}^{\mathcal{C}}$ in this case as well.∎

How restrictive is the requirement of completability? Intuitively, if a protocol is very restrictive about how processes interact, then the system is likely sufficiently intricate that trying to reason locally may be difficult independant of our methodology. For instance, the invariant we later find for leader election is not completable. However, if equivalence classes are small, then most reasonable formulae satisfy the completability condition.

Theorem 5.4

If $\mathit{Inv}_{\mathit{Top}_{i}}(p)$ is satisfiable over any domain for each $1\leq i\leq n$ and topological predicates are of arity $k=1$, then $\mathit{Inv}(p)$ is completable.

Proof

Let $\mathit{Inv}_{i}(p)$ be satisfiable for each $1\leq i\leq n$. Then let $\mathcal{I}(V^{\prime})$ be an interpretation of $\Sigma_{B}\uplus\Sigma_{S}$ over domain $V^{\prime}\subseteq V$ for $G=(V,E)\in\mathcal{C}$. For each $p\in V\setminus V^{\prime}$, suppose $\mathcal{I}_{G}\models\mathit{Top}_{i}(p)$ for some $1\leq i\leq n$. Then choose $\mathcal{J}(p)\models\mathit{Inv}_{\mathit{Top}_{i}}(p)$ since $\mathit{Inv}_{\mathit{Top}_{i}}(p)$ is satisfiable. Otherwise, if $\mathcal{I}_{G}\not\models\mathit{Top}_{i}(p)$ for all $1\leq i\leq n$, then $\mathcal{J}(p)$ is chosen arbitrarily. In either case, $\mathcal{J}\models\mathit{Inv}(p)$. Finally, define $\mathcal{J}(p)=\mathcal{I}(p)$ for $p\in V^{\prime}$. Then $\mathcal{J}$ completes the partial interpretation $\mathcal{I}$.

Theorem 5.4 can be generalized to the case where the topological kinds $\Sigma_{T}$ are non-overlapping, and individually completable, where by individually completable, we mean that if $\mathit{Top}(\vec{p})$ and process states of $\vec{p}^{\prime}\subset\vec{p}$ are given, then there is a way to satisfy $\mathit{Inv}(\vec{p})$ without changing the states of $\vec{p}^{\prime}$.

6 Example: Leader Election Protocol

In this section, we illustrate our approach by applying it to the well-known leader election protocol [2]. This is essentially the same protocol used to illustrate Ivy in [15]. The goal of the protocol is to choose a leader on a ring. Each process sends messages to its neighbour on one side and receives messages from a neighbour on the other side. Initially, all processes start with distinct identifiers, $\mathit{id}$, that are totally ordered. Processes pass $\mathit{id}$s around the ring and declare themselves the leader if they ever receive their own $\mathit{id}$.

We implement this behaviour by providing each process a comparison variable $\mathit{comp}$. Processes then pass the maximum between $\mathit{id}$ and $\mathit{comp}$ to the next process. A process whose $\mathit{id}$ and $\mathit{comp}$ have the same value is the leader. The desired safety property is that there is never more than one leader in the protocol.

In [15], the protocol is modelled by a global transition system. The system maintains a bag of messages for each process. At each step, a currently waiting message is selected and processed according to the program of the protocol. The network topology is axiomatized, as shown in Section 1. Here, we present a local model of the protocol and its corresponding verification condition.

Network topology.

The leader election protocol operates on a ring of size at least 3. For $n\geq 3$, let $G_{n}=(V_{n},E_{n})$, where $V_{n}=\{p^{n}_{i}\mid 0\leq i<n\}$ and $E_{n}=\{(p^{n}_{i},p^{n}_{j})\mid 0\leq i<n,j=i+1\bmod n\}$. Let $\Sigma_{E}=\{\mathit{next}\}$ and $\Sigma_{T}=\{\mathit{btw}\}$, where $\mathit{btw}$ is a ternary relation such that $\mathit{btw}(p^{n}_{i},p^{n}_{j},p^{n}_{k})$ iff $i<j<k$, $j<k<i$, or $k<i<j$. Finally, the network topology is $\mathcal{BTW}=\{G_{n}\mid n\geq 3\}$. Note that while $\mathcal{BTW}$ can be axiomatized in FOL, we do not require such an axiomatization. The definition is purely semantic, no theorem prover sees it.

A formal specification of the leader election as an FO-protocol is shown in Fig. 7, where $LO(\leq)$ is an axiomatization of total order from [15], and $x<y$ stands for $x\leq y\land x\neq y$. The model follows closely the informal description of the protocol given above. The safety property is $\neg Bad$, where $Bad=btw(x,y,z)\land id(x)=comp(x)\land id(y)=comp(y)$. That is, a bad state is reached when two processes that participate in the $\mathit{btw}$ relation are both leaders.

A local invariant $Inv_{\textit{lead}}$ based on the invariant from [15] is shown in Fig. 8. The invariant first says if an $\mathit{id}$ passes from $y$ to $x$ through $z$, then it must witness $\mathit{id}(y)\geq\mathit{id}(z)$ to do so. Second, the invariant says that if a process is a leader, then it has a maximum id. Finally, the invariant asserts our safety property.

This invariant was found interactively with Ivy by seeking local violations to the invariant. Our protocol’s $\mathit{btw}$ is uninterpreted, while Ivy’s $\mathit{btw}$ is explicitly axiomatized. The inductive check assumes that the processes $p,\mathit{next}(p),\vec{q}$ all satisfy a finite instantiation of the ring axioms (this could be done by the developer as needed if an axiomatization is unknown, and this is guaranteed to terminate as there are finitely many relevant terms), and $\mathit{btw}(\vec{q})$. Once the invariants are provided, the check of inductiveness is mechanical. Overall, this presents a natural way to model protocols for engineers that reason locally.

An uncompletable invariant

The invariant for the leader election is not completable. To see this, we present a partial interpretation $\mathcal{I}$ over $\{p^{3}_{0},p^{3}_{2}\}\subseteq V_{3}$ from $G_{3}$ with no extension. We choose $\mathcal{I}(\leq)$ to be $\leq$ over $\mathbb{N}$, as intended. Then we choose $\mathcal{I}(\mathit{id})$ to map $p^{3}_{0}\mapsto 1$ and $p^{3}_{2}\mapsto 2$. We also choose $\mathcal{I}(\mathit{comp})$ to map $p^{3}_{0}\mapsto 0$ and $p^{3}_{2}\mapsto 1$. Since no tuple satisfies $btw$, this vacuously satisfies all invariants thus far. Let $\mathcal{J}$ be an $\mathcal{BTW}$ interpretation agreeing on $p^{3}_{0},p^{3}_{2}$. Consider $\mathit{id}(p^{3}_{1})$. We know $\mathit{id}(p^{3}_{1})\neq 0,1,2$ since we require distinct ids across the new $\mathit{btw}$ relation. But we also have $\mathit{id}(p^{3}_{0})=\mathit{comp}(p^{3}_{2})$ and thus to satisfy $\mathit{Inv}$ we must have $\mathit{id}(p^{3}_{0})\geq\mathit{id}(p^{3}_{1})$. Thus we seek an $n\in\mathbb{N}$ such that $1\geq n$, but $n\neq 0,1$, which cannot exist. Thus $\mathit{Inv}$ is uncompletable.

7 Related Work

We have shown how analysis techniques for parametric distributed systems composed of several components running on locally symmetric topologies, introduced in [7, 8, 9, 11, 12], can be generalized and applied within a First Order Logic based theorem proving engine. The key steps are showing how the local neighbourhoods of network nodes can be encoded and reasoned about separately from FOL based reasoning about safety properties of the reachable states of a parametric family of programs. Using separate decision procedures, one for answering questions about the topology and one for answering questions about local similarity between topological structures, and processes, one can then reason compositionally within an FOL-based theorem prover. We have used the framework to reason about the correctness of a version of the leader election protocol [2].

We based our description of leader election on that presented in the Ivy framework [15]. The distinction being that the analysis carried out in Ivy [15] is global, while the analysis given in the current paper is local, where the local structures reason about triples of processes in the the ring.

There has been extensive work on proving properties of parametric, distributed protocols. In particular the work in [1] offers an alternative approach to parametric program analysis based on “views”. In that work, cut off points are calculated during program analysis. As another example, in [7, 11, 12] the “cut-offs” are based on the program topology and the local structural symmetries amongst the nodes of the process interconnection networks.

The notion of a “cutoff” proof of safety for a parametric family of programs was first introduced by [4]. For example, in [4], if a ring of 3 processes satisfies a parametric property then the property must hold for all rings with at least three nodes. The technique used here is somewhat different; rather than needing to check a ring of 3 processes, we check all pseudo-rings of a given size.

Local symmetry reduction for multi-process networks and parametric families of networks generalizes work on “global” symmetry reduction introduced by [5] and [3]. Local symmetry is, in general, an abstraction technique that can offer exponentially more reduction than global symmetry. In particular, ring structures are globaly rotationally symmetric, but for isomorphic processes may be fully-locally symmetric [11, 12].

Recent work [17] has focused on modular reasoning in the proof or analysis of distributed systems. In the current work, the modularity in the proof is driven by a natural modularity in the program structures. In particular, for programs of several processes proofs are structured by modules that are local to a neighborhood of one or more processes [7, 11, 12].

8 Conclusion

We have presented a framework for specifying protocols in a process-local manner with topology factored out. We show that verification is reducible to FOL with an oracle to answer local questions about the topology. This reduction results in a decidable VC when the background theories are decidable. This cleanly separates the reasoning about the topology from that of the states of the processes.

Many open questions remain. We plan to investigate our methodology on other protocols and topologies, implement oracles for common topologies, and explore complexity of the generated characteristic formulae. Finally, we restricted ourselves to static topologies of bounded degree. Handling dynamic or unbounded topologies, for example in the AODV protocol [10], is left open.

Acknowledgements

Richard Trefler was supported, in part, by an Individual Discovery Grant from the Natural Sciences and Engineering Research Council of Canada.