Declarative Parameterized Verification of Topology-Sensitive Distributed Protocols

Abstract

We show that Cubicle [9], an SMT-based infinite-state model checker, can be applied as a verification engine for GLog, a logic-based specification language for topology-sensitive distributed protocols with asynchronous communication. Existential coverability queries in GLog can be translated into verification judgements in Cubicle by encoding relational updates rules as unbounded array transitions. We apply the resulting framework to automatically verify a distributed version of the Dining Philosopher mutual exclusion protocol formulated for an arbitrary number of nodes and communication buffers.

1 Introduction

Automated verification of distributed systems is a difficult task for standard model checkers [7, 8]. Protocols designed to operate in distributed systems are often defined for an arbitrary number of nodes, arbitrary connection topology, and asynchronous communication. protocol rules typically depend on the current network configuration (e.g., presence of a communication link, state of all connections, etc.). Several formal languages have been proposed to specify this class of systems, e.g., communicating state machines, automata, process algebraic languages, (graph) rewriting, etc. In this setting safety properties can be nicely formulated by lifting decision problems based on reachability and coverability, in which the initial configuration is typically fixed a priory, to formulations that are existentially quantified over an infinite set of initial configurations. Existentially quantified coverability problems have been considered in [5, 6, 14,15,16] in order to reason on parameterized formulation of distributed protocols with broadcast communication. The coverability decision problem [1] is typically used to formulate reachability of bad configurations independently from the number of components of a system. Therefore, a constructive way to solve an existentially quantified coverability problem for a formal specification of a distributed algorithm provides a characterization of initial configurations from which it is possible to reach a bad configuration (e.g. an anomaly in the protocol). Existentially quantified coverability problems turn out to be undecidable even for systems with a static communication topology and very basic interaction primitives like atomic broadcast communication [1, 7, 13,14,15]. As mentioned before, communicating state machine (automata), adopted e.g. in [11, 14,15,16], and graph rewriting, adopted in [5], are two examples of formal description languages for this kind of systems. communicating state machines can be considered a standard design and protocol specification language adopted in several verification tools like Uppaal and Spin. Graph rewriting systems are well-suited for representing topology-sensitive rules as shown by the examples of the Groove tool suite. In several case-studies, protocol rules require complex guards that require the inspection of the state of nodes, links, paths, vicinity etc. and tables to store information collected during the execution of protocol phases. The combination of these features seems to require more general specification formalisms. To this aim, in [12] we proposed to adopt a logic-based declarative language, named GLog, a fragment of both DCDCs [12] and MSR [23]. GLog can be viewed as a logic-based presentation of graph update rules with global conditions expressed using quantified first order formulas. GLog is based on a quantified predicate logic in a finite relational signature with no function symbols. Configurations are represented here as sets of ground atomic formulas (instances of unary and binary predicates). Update rules consist of a guard and two sets of first order predicates that define resp. deletion and addition of state components. Differently from specification languages based on extension of Petri nets like transfer and broadcast protocols, guards are checked atomically but update transitions have only local effect. In other words, we forbid simultaneously update of the state of all nodes in a graph. Update rules can be applied to update a global configuration node by node and to operate on the vicinity of a node by restricting updates to given predicates. Termination of an update subprotocol can then be checked via a global condition. Similar specification patterns have been applied to model non-atomic consistency protocol and mutual exclusion protocols with non-atomic global conditions. GLog has been applied to manually analyze distributed protocols in [12]. In the present paper we show that Cubicle [9, 18], an SMT-based infinite-state model checker based on previous work by Ghilardi et al. [3], can be applied as automated verification engine for existentially quantified coverability queries in GLog. In Cubicle parameterized systems can be specified as unbounded arrays in which individual components can be referred to via an array index. The Cubicle verification engine performs a symbolic backward reachability analysis using an SMT solver for computing intermediate steps (preimage computation, entailment and termination test) and applies overapproximates predecessors using upward closed sets as in monotone abstractions [2]. A peculiar feature of Cubicle w.r.t. MCMT [3] is that the tool can handle unbounded matrices. This is particularly relevant when modeling topology-sensitive protocols as done in GLog using binary relations defined over component identifiers. Furthermore, existentially quantified coverability decision problems in GLog can directly be mapped into Cubicle. More specifically, the encoding transforms GLog update rules into array-based update formulas in Cubicle. Classes of initial configurations are specified by using partial specifications of initial configurations in Cubicle verification judgements. Infinite sets of bad configurations can be expressed using unsafe configurations in Cubicle verification judgements.

As a case-study, we consider the distributed version of the Dining Philosopher mutual exclusion protocol (DDP) recently studied in [12, 17, 20]. The protocol deals with an arbitrary, finite number of nodes and buffers that act as single-place communication channels, and arbitrary link topology between nodes and buffers. Ownership of buffers is specified using asynchronous rules. Global conditions over linked buffers are used as enabling conditions for acquiring access to resources shared among neighbors. The GLog formal specification of DDP is mapped to a Cubicle verification problem in a natural way. In our preliminary experiments, Cubicle verified the correctness of the protocols in negligible time. Furthermore, as expected it reports potential error traces when introducing network reconfiguration rules (e.g. dynamic link creation and deletion) unrelated to the state of the corresponding involved nodes. The application of declarative specification languages and SMT-based engine seems a very promising research line for dealing for a larger class of distributed algorithms.

Contents. The paper is organized as follows: we first present the GLog declarative language and, in that context, the existential coverabiliity problem; we then introduce Cubicle and exhibit a general encoding of existential coverability into Cubicle; we then discuss the experimental evaluation on the DDP case-study, and, finally, discuss other examples and future directions.

2 GLog

GLog [12] formulas are based on a simple relational calculus that can be used to express updates of sets of ground atoms. A set of ground atoms can be interpreted as the current state or configuration of the system we are modeling. Update rules contain a formula working as a condition and deletion and addition sets that specify ground atoms to be deleted and added to the current state. More formally, let P be a finite set of names of (unary and binary) predicate names, $\mathcal{N}$ a denumerable set of node identifiers equipped with a total order <, V be a denumerable set of variables. Predicates in P are used to model current configurations. In addition to predicates in P, we interpret the binary relation lt as the total order < in our model. Our logic has no function symbols but can be instantiated with elements from $\mathcal{N}$. An atomic formula is either a formula p(x), lt(x, y) or p(x, y), where $p\in P$, $x,y\in V\cup \mathcal{N}$ A ground atom is a either a p(n), lt(n, m), or p(n, m), where $n,m\in \mathcal{N}$. A literal is either an atomic formula or the negation $\lnot A$ of an atomic formula A. A formula is a first order formula built on literals, namely, any literal is a formula, conjunctions, disjunctions, universally and existentially quantified formulas are still formulas. Multiple occurrences of the same variable implicitly model equality constraints. The set of free variables of a formula F, namely FV(F), is the minimal set satisfying $FV(p(x,y))=\{x,y\}$, $FV(A\vee B)=FV(A)\cup FV(B)$, $FV(A\wedge B)=FV(A)\cap FV(B)$, $FV(\lnot A)=FV(A)$, $FV(\forall v.A)=FV(A)\setminus \{v\}$, and $FV(\exists v.A)=FV(A)\setminus \{v\}$. Given $S=\{F_1,\ldots ,F_n\}$, we define $FV(S)=FV(F_1)\cup \ldots \cup FV(F_n)$. Quantified formulas we will be used as application conditions of rules.

Configurations, Interpretations and Update Rules. As mentioned before a set of ground atoms will be used to model a configuration. Formally, a configuration is a finite set $\varDelta$ of ground atomic formulas with predicates in P. A configuration implicitly defines a graph in which directed edges are represented by atomic formulas whose predicate name acts as edge label. Configurations can also be viewed as models in which to evaluate a conditions. An interpretation is a mapping $\sigma$ from V to $\mathcal{N}$. We use here a fixed interpretation of variables. The interpretation domain however consists of a denumerable set of node identifiers. For a formula F we use $F\sigma$ as an abbreviation for $\hat{\sigma }(F)$, where $\hat{\sigma }$ is the natural extension of $\sigma$ to terms. For a set $S=\{A_1,\ldots ,A_n\}$, we use $S\sigma$ to denote the set $\{A_1\sigma ,\ldots ,A_n\sigma \}$. Update rules consists of conditions defined by quantified formulas with no function symbols, a deletion and an addition set. The deletion (resp. addition) set defines the set of ground atoms that have to be cancelled from (resp. added to) the current configuration. A rule has the following form $\langle {C,D,A}\rangle$, where C is a quantified formula, D and A are two sets of atomic formulas with variables in V and predicates in P, and such that $FV(A)\cup FV(D)\subseteq FV(C)$. A protocol $\mathcal{P}$ is defined as a set of rules.

Operational Semantics. To fix an operational semantics for our language we need a support for the interpretation of relations and variables. We use $\varDelta \models A$ to define the satisfiability relation of a quantified formula A s.t. $FV(A)=\emptyset$. Let A[n / X] denote the formula obtained by replacing each free occurrence of X with n. The relation is defined by induction as follows. $\varDelta \models p(n)$, if $p(n)\in \varDelta$, $\varDelta \models lt(n,m)$, if $n<m$, $\varDelta \models p(n,m)$ for $p\in P$, if $p(n,m)\in \varDelta$, $\varDelta \models A\wedge B$, if $\varDelta \models A$ and $\varDelta \models B$, $\varDelta \models \lnot A$, if $\varDelta \not \models A$, $\varDelta \models \forall X.A$, if $\varDelta \models A[n/X]$ for each $n\in \mathcal{N}$, and $\varDelta \models \exists X.A$, if $\varDelta \models A[n/X]$ for some $n\in \mathcal{N}$. Given a configuration $\varDelta$, we say that the quantified formula A is satisfied in $\varDelta$, if there exists an interpretation $\sigma$ s.t. $A\sigma$ is satisfiable. In order to apply a rule $\langle {C,D,A}\rangle$ to $\varDelta$, there must be an interpretation $\sigma$ that satisfies the quantified formula C. The same interpretation $\sigma$ is then applied to the atomic formulas in D and A. The resulting sets of atoms, say $D'$ and $A'$ respectively, are deleted from and added to $\varDelta$, respectively.

The operational semantics of a protocol $\mathcal{P}$ is given by a transition system $T_\mathcal{P}=\langle {\mathcal{C},\rightarrow }\rangle$, where $\mathcal{C}$ is the set of possible configurations, i.e., finite subsets of ground atoms with predicates in P, and $\rightarrow \subseteq \mathcal{C}\times \mathcal{C}$ is a relation defined as follows. For $\varDelta ,\varDelta '\in \mathcal{C}$ and a rule ${\langle {C,D,A}\rangle \in \mathcal{P}}$, $\varDelta \rightarrow \varDelta '$ if there exists $\sigma$ s.t. $\varDelta \models C\sigma$ and $\varDelta '=(\varDelta \setminus D\sigma )\cup A\sigma$. A computation is a sequence of configurations $\varDelta _0\varDelta _1\ldots$ s.t. $\varDelta _i\rightarrow \varDelta _{i+1}$ for $i\ge 0$. We use $\rightarrow ^*$ to denote the reflexive and transitive closure of $\rightarrow$. In a single step of the operational semantics a rule is evaluated in the current configuration by taking a sort of closed-world assumption, i.e., ground atomic formulas that do not occur in a configuration are evaluated to false. Furthermore, ground atomic formulas that are not deleted are transferred from the current to the successor configuration. The latter property can be viewed then as a sort of frame axiom. It is important to notice that, in general, a configuration $\varDelta$ has several possible successors. Indeed, depending of the chosen interpretation of free variables the same rule can be applied to different subsets of ground atoms contained in the same configuration. Furthermore, the choice of the rules to be applied at a given step is non-deterministic.

As an example, we consider possible application of GLog to the specification of distributed protocols. The key ingredient of the specification language is the combination of complex conditions and update rules to reason on graphs in which predicates can be viewed as labels of links between agents and communication buffers. We have shown that we can also add labels to individual agents and buffers, e.g., to represent their current state. Update rules can be used to dynamically reconfigure the graph, i.e., change labels, topology and add or delete agents. The separation between agents and buffers is convenient to model asynchronous communication. For instance, let us consider a protocol in which two agents need to establish a connection via a shared buffer.

• An agent $n_1$ of type A connects to a buffer $e_1$ in idle state (the buffer is free) and sets the state of the buffer to ready.

• An agent $n_2$ of type B connects to $e_1$ in state ready and changes the state to ack.

• Agent $n_1$ sends message m by changing the state of $e_1$ to $msg_m$.

• Agent $n_2$ receives message m and updates the state of the channel to ack for further communications.

The protocol can be specified as follows. We use unary predicates to associate states to edges. send messages are non-deterministically generated. An initial configuration has the form $idle(b_1),\ldots ,idle(b_k)$, where $b_i<b_j$ for $i\ne j$, $i,j:1,\ldots ,k$. For the sake of simplicity, we do not model the state of agents but only their capabilities (req, rec, send).

R	C	D	A
1	$idle(B)\wedge \lnot req(A,B)$	$\{idle(B)\}$	$\{ready(B),req(A,B)\}$
2	$ready(B)\wedge \lnot rec(A,B)$	$\{ready(B)\}$	$\{ack(B),rec(A,B)\}$
3	true	$\{\}$	$\{send(A,B,M)\}$
4	$ack(B)\wedge send(A,B)$	$\{ack(B),send(A,B)\}$	$\{msg(B,M)\}$
5	$msg(B,M)\wedge rec(A,B)$	$\{msg(B,M),rec(A,B)\}$	$\{idle(B)\}$

In rule 1 a buffer B is locked by a non-deterministically generated request req(A, B) from sender agent A (a variable). In rule 2 a buffer B is locked by a non-deterministically generated request rec(A, B) from receiver agent A (a variable). Rule 3 nondeterministically generates a send action from agent A. Rule 4 synchronizes a send action from agent A with a buffer locked by the same agent. The (non deterministically generated) message M is stored in the buffer. Rule 5 synchronizes and consumes a message in the buffer with the receiver agent, releasing the buffer.

The model provides other form of interactions. For instance, we can model ordered buffers by forming lists of messages attached to a given edge as in the representation of the tape of the Turing machine.

We can also model synchronous communication as in the following example

C	$link(A,B)\wedge s_1(A)\wedge link(E,B)\wedge s_2(E)$
D	$\{s_1(A),link(A,B), link(E,B),s_2(E)\}$
A	$\{link(A,B),s_1'(A),link(E,B),s_2'(E)\}$

Here s(A) and $s'(A)$ denote agent A resp. in state s and $s'$, $s_1(E)$ and $s_1'(E)$ denote agent E resp. in state $s_1$ and $s_1'$, and link(A, B) and link(Y, B) denote links to a common buffer B.

2.1 Existential Coverability

We consider here decision problems that generalize the standard notion of reachability between configurations. The key point is to reason about an infinite set of initial configurations in order to prove properties for protocol instances with an arbitrary number of nodes. For a set S of configurations, we first define the Post and Pre operators as follows $Post(S)=\{\varDelta '\ \mid \exists \varDelta \in S,\ \varDelta \rightarrow \varDelta '\}$ and $Pre(S)=\{\varDelta '\ \mid \exists \varDelta \in S,\ \varDelta '\rightarrow \varDelta \}$. We use $Post^*(S)$ (resp. $Pre^*(S)$) to denote the reflexive-transitive closure of Post (resp. Pre).

We now introduce the $\exists$-coverability problem as follows.

Definition 1

($\exists$-coverability). Given a protocol $\mathcal{P}$, a set of target configurations T and a possibly infinite set of initial configurations I, $\exists$-coverability is satisfied for $\mathcal{P}$, I and T, written ${\exists }Reach(\mathcal{P},I,T)$, if there exists $\varDelta \in T$ and a configuration $\varDelta _1$ s.t. $\varDelta _1\in Post^*(I)$ and $\varDelta \subseteq \varDelta _1$.

By expanding the definition of $Post^*$, ${\exists }Reach(\mathcal{P},I,T)$ holds if there exists a configuration $\varDelta _0\in I$ s.t. $\varDelta _0\rightarrow ^*\varDelta _1$ and $\varDelta \subseteq \varDelta _1$ for some $\varDelta \in T$. The target T can be interpreted as a pattern to match or avoid in computations starting from initial configurations. If the set I consists of configurations consisting of an arbitrary, finite number of components than $\exists$-coverability formally describes a parameterized verification decision problem for specifications given in GLog. The $\exists$-coverability problem turns out to be undecidable [12].

3 From GLog to Cubicle

Cubicle is a model checker that can be applied to verify safety properties of array-based systems, a syntactically restricted class of parametrized transition systems with states represented as arrays indexed by an arbitrary number of processes [9, 18]. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems. Cubicle model-checks by a symbolic backward reachability analysis on infinite sets of states represented by specific simple formulas, called cubes. Cubicle is written in OCaml. The SMT solver is a tightly integrated, lightweight and enhanced version of Alt-Ergo [21]; and its parallel implementation relies on the Functory library [22]. Cubicle input language is a typed version of Murphi similar to the one of Uclid. A system is described in Cubicle by: (1) a set of type, variable, and array declarations; (2) a formula for the initial states; and (3) a set of transitions. It is parametrized by a set of process identifiers, denoted by the built-in type proc. Standard types int, real, and bool are also built in. Additionally, the user can specify abstract types and enumerations with simple declarations like and . As an example consider the following declaration.

The system state is defined by a set of global variables and arrays. The initial states are defined by a universal conjunction of literals characterizing the values for some variables and array entries.

A state of our example consists of a process identifier Turn and two boolean arrays Want and Crit; a state is initial iff every cell of both arrays are set to false Transitions are given in the usual guard/action form and may be parameterized by (one or more) process identifiers. Guards are expressed via expressions. They are quantified formulas. Quantification is defined only over variables of type proc. As an example, consider the following rule.

The transition is enabled if there exists index (a process) such that . Its effect is to set to true for index and leave the array unchanged in all other positions. A system execution is defined by an infinite loop that at each iteration: (1) non-deterministically chooses a transition instance whose guard is true in the current state; and (2) updates state variables according to the action of the fired transition instance.

Infinite sets of unsafe states (bad configurations) are defined by using unsafe constraints. For instance, the judgement

specifies the infinite set of arrays Crit (with any size) in which there exist two cells with value True.

The Cubicle verification engine is based on symbolic backward exploration. Cubicle operates over sets of existentially quantified formulas called cubes. Formulas containing universally quantified formulas (generated during the computation of predecessors) are over-approximated by existentially quantified formulas. The class of formulas manipulated by the backward reachability loop of Cubicle in not closed by pre-image in presence of universally quantified guards. To handle such formulas, Cubicle implements a safe but over-approximate pre-image computation. Given a cube $\exists \bar{i}. \varPhi$ and a guard G of the form $\forall \bar{j}. \varPsi (\bar{j})$, the pre-image replaces G by the conjunction $\bigwedge _{\sigma \in \varSigma (\bar{j},\bar{i})} \varPsi (\bar{j})\sigma$ of instances over the permutation of $\varSigma (\bar{j}, \bar{i})$. In other words, in order to handle universally quantified guards, Cubicle applies monotone abstraction [2] and over-approximates predecessors via upward-closed sets of configurations. The search procedure maintains a set V and a priority queue Q resp. of visited and unvisited cubes. Initially, let V be empty and let Q contain the cubes representing bad states. At each iteration, the procedure selects the highest-priority cube $\varPhi$ from Q and checks for intersection with the formula denoting the initial configurations (satisfiability of conjunction of $\varPhi$ and formulas in the initial conditions). If the test fails, it terminates reporting a possibile error trace. If the test passes, the procedure proceeds to the subsumption check, i.e., implication between formulas. If subsumption fails, then add $\varPhi$ to V, compute all cubes in $pred_t$ (for every t), add them to Q, and move on to the next iteration. If the subsumption check succeeds, then drop $\varPhi$ from consideration and move on. The algorithm terminates when a safety check fails or Q becomes empty. When an unsafe cube is found, Cubicle actually produces a counterexample trace. Safety checks, being ground satisfiability queries, are easy for SMT solvers. The challenge is in the subsumption check because of their size and the existential implies existential logical form. Cubicle applies the heuristics described in [9] to handle subsumption. The BRAB algorithm introduce in [10] automatically computes over-approximations of backward reachable states that are checked to be unreachable in a finite instance of the system (using Mur$\phi$). The resulting approximations (candidate invariants) are model checked together with the original safety properties. Completeness of the approach is ensured by a mechanism for backtracking on spurious traces introduced by too coarse approximations.

Encoding GLog in Cubicle

In this section we present an encoding of GLog into an array-based specification language. The encoding is quite natural. The interpretation domain of variables is that of process indexes. For each unary predicate $p\in P$, we introduce a corresponding Boolean array variable .

For each binary predicate q, we introduce a two-dimensional Boolean array

Encoding of guards is straightforward. Free variables occurring in GLog update rules become parameters of transition definitions. A literal q(x, y) [resp. q(x)] is mapped to the formula $q(x,y)=true$ [resp. $q(x)=true$]. A literal $\lnot q(x,y)$ [resp. $\lnot q(x)$] is mapped to the formula $q(x,y)=false$ [resp. $q(x)=false$]. Compound/quantified require conditions are mapped to compound/quantified formulas over literals.

Some care has to be taken in the encoding of GLog update rules. Transitions in Cubicle operate simultaneously on every cell of an array to provide support for global operations like reset and transfer. This kind of operations are not provided in GLog since the focus is on asynchronous behavior, i.e., we assume that global operations are split into several asynchronous operations equipped with guards that can be used to check for the current state of the protocol phase under consideration.

To encode a deletion rule, operating on the atomic formula A(x, y), we use auxiliary variables u, t and a case analysis on indexes: for the case $x=u,y=t$ we add the action $A[x,y]:=false$, and $A[x,y]:=A[x,y]$ in all other cases. To encode an addition rule, operating on the atomic formula A(x, y), we use again auxiliary variables u, t and a case analysis on indexes: for $x=u,y=t$ we add the action $A[x,y]:=true$, and $A[x,y]:=A[x,y]$ in all other cases.

To encode $\exists$-coverability, we also need to specify initial and unsafe configurations. Unsafe configurations can be described as in Cubicle using an existentially quantified formula over array cells. To select classes of initial states, we can use declarations in which we specify only partial conditions on array cells.

4 Case Study: Distributed Dining Philosophers

We consider here a distributed version of the dining philosopher mutual exclusion problem presented in [19]. Agents are distributed on an arbitrary graph and communicate asynchronously via point-to-point channels. Channels are viewed as buffers with state. Distributed Dining Philosophers (DDP) is defined as follows. The goal is to ensure that agents can access a resource shared in common with their neighbors in mutual exclusion. The protocol from the perspective a single agent consists of the following steps:

• Initially, all agents are in idle state.

• When an agent A wants to get a resource, A has to acquire the control of each buffer shared with his/her neighbors.

• To acquire a channel, A marks the channel with its identifier. If the channel is already marked, A has to wait.

• A acquires the resources when all channels shared with neighbors are marked with his/her identifier.

• To release a resource, A first resets each buffer. When all buffers are reset, A moves back to idle state.

In a statically defined topology, agent A gets access to a resource when all neighbors are either idle or are waiting for acquiring some channel. Communication between two neighbors is asynchronous. Indeed, they interact by reading and writing on the shared channel. The protocol should guarantee that two agents that share the same channel cannot acquire and use a resource simultaneously. The protocol should be robust under dynamic reconfigurations of the network.

4.1 Formal Specification of DDP

In this section we present a formal specification of the DDP protocol. Network configurations are expressed as GLog configurations. The dynamics in a protocol interaction is expressed via a finite set of update rules. We use a predicate link to represent connections from an agent to a possibly shared buffer. We model buffers with states using unary predicates. Asynchronous communication is modeled as in the previous example, i.e., agents interact only via a common buffer. Communication between two agents is not atomic. Instead of modeling identifiers and buffers with data, we introduce a special relation own that is used to model ownership of a given buffer to which a agent is linked. Ownership is normed in the same way as the labeling of buffers in the original protocol, i.e., an agent can acquire ownership only if the buffer is not owned by other agents. Ownership can be released when in idle state. We also model non-deterministic creation (in idle state) and deletion of links. We model this behavior using the following predicates and rules (rules have the form $(C_i,D_i,A_i)$ for $i:1,\ldots ,6$):

R	C	D	A
getE	$link(X,E)\wedge \forall Z. \lnot own(Z,E)$	$\emptyset$	$\{own(X,E)\}$
relE	$\{idle(X),own(X,E)\}$	$\{own(X,E)\}$	$\emptyset$
acquire	$idle(X)\wedge \forall E. (link(X,E)\supset own(X,E))$	$\{idle(X)\}$	$\{busy(X)\}$
release	$\{busy(X)\}$	$\{busy(X)\}$	$\{idle(X)\}$

An initial state configuration has the following form $idle(n_1),\ldots ,idle(n_k)$, where $n_i\ne n_j$ for $i\ne j$, $i,j:1,\ldots ,k$ and $k\ge 1$.

4.2 Encoding in Cubicle

Following the encoding rules specified for GLog, we can now obtain a Cubicle specification for DDP. To simplify a little bit the specification, we introduce an enumeration type over node states.

This way, we can use a single array with cell type instead of two Boolean arrays. We also need a array and a array to specify link and ownership relations between nodes and buffers.

The initial configuration consists of all possible topologies in which nodes are in idle state. We also enforce the ownership relation to be false for each pair of node and buffer.

This way we do not put any constraints on link topology. The bad configuration are defined by graphs of the following form.

Two node are in mutex state while pointing to at the same buffer. The transitions are obtained via the encoding of the GLog specification into Cubicle input language shown in Appendix A. When applying Cubicle to the above described problem, the tool proves the model correct in few seconds without need to apply multicore optimizations via the Functory library. More specifically, Cubicle visits 19 nodes with at most 3 process indexes, 529 fixpoint checks, and 176 calls to the Alter-Ego SMT solver. Since Cubicle operates over unbounded arrays, the above result provides a formal correctness proof of the considered model for any number of nodes and links and any topology. The proof certificate can be obtained by taking the set of assertions (formulas) collected during the fixpoint computation. By applying the BRAB algorithm with parameter 3, the number of visited nodes reduces to 10 with 312 fixpoint tests, and 88 calls to the Alter-Ego solver. Furthermore, the BRAB algorithm infers the invariant $\lnot (Own[\#1, \#3] = True \wedge Own[\#2,\#3] = True)$.

4.3 Dynamic Reconfiguration

To model dynamic reconfigurations, we can non-deterministically add and remove link predicates between pairs of agents and buffers. We first consider the non-deterministic rules link and unlink defined below.

R	C	D	A
Link	$\lnot link(X,E)$	$\emptyset$	$\{link(X,E)\}$
Unlink	link(X, E)	$\{link(X,E)\}$	$\emptyset$

When the model extended with the above rules is checked with Cubicle (see Appendix B), the tool reports the error trace $acquire(\#1) \rightarrow link(\#1,\#3) \rightarrow get(\#2, \#3) \rightarrow acquire(\#2) \rightarrow unsafe[1]$. This trace is a real error trace. Indeed, process $p_1$ can acquire ownership when there are no links to buffer $b_3$. Since the link rule has no condition on $p_1$, a link can then be added from $p_1$ to $b_3$. However, Process $p_2$ can now become owner of $b_3$ and then move to state Busy. Two processes are linked to the same buffer $b_3$ while in state Busy.

Fig. 1.

Experimental results: V = visited nodes, F = fixpoint tests, S = solver calls, M = max process number, D = deleted node, I = number of invariants (brab), C = property checked (Yes/No).

We can modify the model and restrict addition of new link connected to node X only when X is in state Idle as follows.

R	C	D	A
iLink	$idle(X),\lnot link(X,E)$	$\emptyset$	$\{link(X,E)\}$
Unlink	link(X, E)	$\{link(X,E)\}$	$\emptyset$

In this model we assume that nodes have some form of control over connections with buffers (i.e. a new link is detected by a node in state Idle). When the model extended with the $link'$ and unlink rules is checked with Cubicle (see Appendix B), the tool verifies correctness by visiting 28 nodes with at most 3 process indexes, invoking 261 times the SMT solver, performs 1449 fixpoint tests, and deletes 6 redundant nodes. The above result provides a formal correctness proof of the considered model for any number of nodes and links and any topology. Using dfs search, the tool verifies the property but the number of visited nodes is 39 with 414 calls to the SMT solver and 1996 fixpoint checks. Using the BRAB algorithm with parameter 3, the number of visited nodes reduces to 14 with 735 fixpoint tests, and 153 calls to the Alter-Ego solver. As for static topologies, the BRAB algorithm infers the invariant $\lnot (Own[\#1, \#3] = True \wedge Own[\#2,\#3] = True)$. A summary of the results with the considered models and heuristics are shown in Fig. 1.

5 Conclusions

We have studied a possible application of SMT-based infinite-state model checker to the verification of topology-sensitive distributed protocols, i.e., protocols defined over network graphs and in which rules have guards and effects that depend on communication links. Starting from a logic-based presentation of distributed protocols based on the GLog relational update language, we have shown how to encode existential coverability queries in GLog as Cubicle verification judgements. As a case-study, we have shown that the declarative approach supported by GLog + Cubicle provides a very effective way to verify protocols operating on graphs. For instance, in previous work DDP required complex verification methodologies like assume-guarantee reasoning or ad hoc algorithms for graph rewriting systems. In the present paper DDP is verified using a very simple declarative specification and a general purpose model checker. Cubicle verifies correctness in negligible execution time (without need of multicore optimizations via the Functory library).

The proposed methodology can be applied to other types of distributed protocols. More specifically, we are currently studying how to deal with routing protocols for arbitrary topologies and hierarchical protocols for reference counting (e.g. garbage collections disciplines etc.). Another interesting direction is related to the possible application of Cubicle for verification of protocol specifications in parameterized multi-agent systems [4].

Appendices

A DDP in Cubicle

B Dynamic Reconfiguration in Cubicle