=Paper=
{{Paper
|id=Vol-1645/paper28
|storemode=property
|title=A Logic-based Approach to Verify Distributed Protocols
|pdfUrl=https://ceur-ws.org/Vol-1645/paper_28.pdf
|volume=Vol-1645
|authors=Giorgio Delzanno
|dblpUrl=https://dblp.org/rec/conf/cilc/Delzanno16
}}
==A Logic-based Approach to Verify Distributed Protocols==
https://ceur-ws.org/Vol-1645/paper_28.pdf
A Logic-based Approach to Verify Distributed
Protocols
Giorgio Delzanno
DIBRIS, University of Genova, Italy
Abstract. We present a framework for the specification of distributed
protocols based on a logic-based presentation of bipartite graphs. For
the considered language, we define assertions that can be applied to
arbitrary configurations. We apply the language to model the distributed
version of the Dining Philosopher Protocol. The protocol is defined for
asynchronous processes distributed over a graph with arbitrary topology.
To validate the protocol, we apply permutation schemes, transformation
rules, and inductive verification.
1 Introduction
Verification of distributed systems with parametric dimension is a challenging
task. In this setting protocols are defined on generic configurations of a network,
e.g., for an arbitrary number of nodes and arbitrary connection topology. Proto-
col rules may depend on the current network configuration. For instance, in [14]
Namjoshi and Trefler introduced a distributed variant of the dining philosopher
protocol in which individual nodes interact asynchronously via shared buffers.
Global conditions formulated on the state of visible buffers are used to regulate
the access to resources shared between adjacent nodes.
In this paper we present a formalization of distributed protocols with all
above mentioned features based on a logic-based presentation of bipartite graphs
defined over two classes of nodes: agent and edges. A agent corresponds to a net-
work agent. An edge corresponds to a potential link between multiple agents.
We use bipartite graphs in order to model both complex topologies and asyn-
chronous operations in a more natural way with respect to standard transition
systems. Point-to-point links can be obtained by using conditions defined on
update rules. Our specification language is based on a predicated logic with
quantification defined over a finite set of typed relations without function sym-
bols. The interpretation domain of relations is defined over an infinite set of
agents and edges. In this setting we can model handshaking between two agents
via intermediate steps in which agents first connect to edges and then, by up-
dating the relations connecting them, start an interaction between them. In our
model we admit multiple connections to the same edge.
The technical contribution of the paper is as follows. We first define the
syntax and formal semantics of the BLog specification language. The language
is based on conditional update rules. Conditions are expressed as first order
quantified formulas defined over binary predicates without function symbols.
Update rules are defined by sets of atomic formulas that specify the ground atoms
that have to be removed from the current configuration and those that have to be
added to the new one. BLog can be viewed as a fragment of richer languages for
representing evolving databases like DCDS [8]. Differently from DCDS, designed
for updates of relational databases, we are interested here in a minimal fragment
of relational logic to reason about evolving bipartite graphs. Furthermore, we
focus our attention on a special class of decision problems that can be viewed
as parametric versions of reachability problems. More specifically, in order to
reason about families of distributed systems we consider reachability problems
existentially quantified over initial configurations as in previous work on formal
verification of parameterized systems. Furthermore, we isolate a fragment of
BLog in which we show that the considered decision problem is undecidable.
The proof is based on an encoding of Turing machines on a special type of
bipartite graphs in which we used special links to order the representation of
tape cells.
We apply our language to model the distributed version of the Dining Philoso-
pher Protocol proposed in [15]. The protocol is defined for asynchronous pro-
cesses distributed over a graph with arbitrary topology. We model the protocol
by considering dynamic reconfigurations of the topology. To verify the correct-
ness of our model, we apply a proof method that combines two kinds of reasoning.
We first apply source to source transformations based on permutation schemes
that lead to derived rules. Permutation schemes are obtained via a proof theo-
retic analysis of computations. Permutation rules can be applied to derive meta
rules obtained by composing sequences of rule applications of the original pro-
tocol. We use deductive reasoning to prove mutual exclusion on the resulting
model. Invariants are expressed using parametric formulas, an extension of the
assertional language used in BLog needed to express properties like parametric
reachability. The resulting method is based on proof techniques that are com-
plementary to compositional reasoning [15] and symbolic backward exploration
[7].
1.1 Related Work
We focus our attention on a class of formal models for concurrent and dis-
tributed systems in which synchronization is achieved by using broadcast com-
munication, a less standard communication primitive than rendez-vous or point-
to-point communication. Rendez-vous communication involves a fixed a priori
number of agents (e.g. a sender and a receiver in point-to-point communica-
tion). Properties of rendez-vous communication have been investigated deeply
in the field of automated verification, see e.g. [6]. Interactions in models with
broadcast communication are usually defined by allowing a finite but arbitrary
number of agents to react to a given message or signal. This type of communi-
cation is particularly useful to define protocols for replicated systems, e.g. cache
coherence protocols, algorithms with global conditions, e.g., simultaneous resets
of local variables, and communication in an open environment like an Ad Hoc or
Wireless network. Algorithmic verification of models with broadcast communi-
cation started receiving more attention after the introduction of the Broadcast
Protocols of Emerson and Namjoshi [3]. FAST [2,24], TRex [23], LASH [25],
and MIST [17] are tools that can handle counter abstractions of network models
given in formal of vector addition systems and their extensions. MAP [4] is a
tool based on transformations of constraint logic programs that can be applied
to infinite-state systems with linear configurations and relations over data vari-
ables. MCMT [18] is a symbolic backward reachability engine based on SMT
solvers that can handle parameterized systems with linear configurations. The
MCMT tool is based on the EPR fragment of first order logic with arrays and
applies different types of heuristics including invariant generation to reduce the
state space. PFS [21] and UNDIP [22] are tool specifically devised to handle pa-
rameterized systems. AUGUR 2 [11] is a tool devised for the analysis of Graph
Transformation Systems using approximated unfoldings based on Petri nets. The
approximated systems can then be verified using regular expressions, first order
logic and coverability checking techniques. AUGUR 2 does not handle global
operations like those needed for modeling broadcast communication. PETRU-
CHIO [13] is a tool that extracts a Petri net representation from specifications
of dynamic networks based on the π-calculus. Boom [20] is a tool that applies
symbolic algorithms, see, e.g., [10,12,1,9], to verify counter abstractions of multi-
threaded programs. The algorithms behind the tool go beyond backward search.
Indeed they combine several types of heuristics like those based on dynamic
generation and refinement of over-approximations (defined in terms of upward
closed set of states). PCW [19] is a tool that applies ordered counter abstraction
[5], a refinement of monotonic abstraction with CEGAR, for the verification of
parameterized systems. In this setting over-approximations are refined by us-
ing stronger and stronger orderings that can be used to define upward closed
sets that ”forbid” specific patterns (e.g. they forbid sets of points defined by
a given equation). UNCOVER [16,26] is a tool that performs a symbolic back-
ward reachability analysis for GTS with universally quantified conditions. The
tool exploits a generalization of monotonic abstraction to quantifications over
graph patterns as a heuristic to manipulate infinite sets of configurations using
minimal constraints (given in form of graphs) only. UNCONVER can be viewed
as the counterpart of UNDIP and PFS for systems in which configurations have
a graph structure.
Differently from [16,26] and [14], our specification logic can be applied to
define invariants involving an arbitrary but fixed number of nodes. For this
purpose, we use assertions with parametric formulas. Global conditions can be
defined using universally quantified formulas. The use of SMT solvers for graph-
based specification is an interesting direction to explore.
2 BLog
In this section we will define a logic-based presentation of evolving bipartite
graphs called BLog.
BLog formulas are based on a simple relational calculus that can be used to
express updates of configurations defined by sets of ground atoms. Ground atoms
define relations, i.e., labelled links, between agents and edges. More formally, let
P be a finite set of names of binary relations, and V be a denumerable set of
variables partitioned in two sets Va and Ve , namely variables ranging over agents
and edges, respectively. Furthermore, let N and E be denumerable sets of agent
and edge identifiers. We consider here typed binary predicates in which the first
argument is of agent type and the second one is of edge type. Our logic has no
function symbols but can be instantiated with elements froN and E.
Definition 1. An atomic formula is a formula p(x, y), where p ∈ P , x ∈ Va ,
and y ∈ Ve . A ground formula is a formula p(n, e), where n ∈ N , and e ∈ E. A
literal is either an atomic formula or the negation ¬A of an atomic formula A.
A formula is a Boolean combination of atomic formulas.
Definition 2. The set of free variables of a formula F , namely F V (F ), is the
minimal set satisfying F V (p(x, y)) = {x, y}, F V (A ∨ B) = F V (A) ∪ F V (B),
F V (A ∧ B) = F V (A) ∩ F V (B), F V (¬A) = F V (A), F V (∀v.A) = F V (A) \ {v},
and F V (∃v.A) = F V (A) \ {v}. Given S = {F1 , . . . , Fn }, we define F V (S) =
F V (F1 ) ∪ . . . ∪ F V (Fn ).
Quantified formulas will be used as application conditions of rules. 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. We will consider free variables occurring in conditions to restrict
the range of identifiers of a configuration.
Definition 3. A rule has the following form hC, D, Ai, where C is a quantified
formula, D and A are two sets of predicates with variables in V , and such that
F V (A) ∪ F V (D) ⊆ F V (C).
Configurations can be viewed as models in which to evaluate a formula.
Definition 4. A configuration is a set ∆ of ground atomic formulas.
Definition 5. We use ∆ |= A to define the satisfiability relation of a quantified
formula A s.t. F V (A) = ∅. The relation is defined by induction as follows.
– ∆ |= A, if A ∈ ∆;
– ∆ |= A ∧ B, if ∆ |= A and ∆ |= B;
– ∆ |= ¬A, if ∆ 6|= A;
– ∆ |= ∀X.A (resp. ∀E.A), if ∆ |= A[n/X] (resp. A[e/X]) for each n ∈ N
(resp. e ∈ E);
– ∆ |= ∃X.A (resp. ∃E.A), if ∆ |= A[n/X] (resp. A[e/X]) for some n ∈ N
(resp. e ∈ E).
To define instantiations of free variables, we consider injective mappings. We
use injective mappings in order to give a unique interpretation of a formula like
p(X, E) ∧ p(Y, F ), i.e., X and Y refer to distinct agents and E and F to distinct
edges. We allow multiple occurrences of the same variable to implicitly model
equality constraints.
Definition 6. An interpretation is an injective mapping σ from Va ∪Ve to N ∪E
s.t. σ(Va ) ⊆ N and σ(Ve ) ⊆ E.
Definition 7. Given a configuration ∆, we say that the quantified formula A is
satisfied in ∆, if there exists an interpretation σ s.t. ∆ |= Aσ is satisfiable.
Example 1. The condition ∀X. p(X, E) ⊃ q(X, E), when evaluated on a con-
figuration ∆, is satisfiable if there exists an edge e such that for all instances
p(n, e) ∈ ∆, there exists an atom q(n, e) ∈ ∆. Based on these considerations, the
rule
hlink(X, Y ) ∧ ∀Z.link(Z, Y ) ⊃ ¬own(Z, Y ), ∅, {own(X, Y )}i
defines a transition in which for a pair n, e such that link(n, e) occurs in the
current configuration and such that there are not other agents n0 s.t. own(n0 , e)
is in the current configuration, own(n, e) is added to the successor configuration.
In the operational semantics we assume that all atomic formulas that are not
deleted are transferred to the successor configuration.
For a set S = {A1 , . . . , An }, we use Sσ to denote the set {A1 σ, . . . , An σ}.
2.1 Transition System
A protocol P is a set of rules. The operational semantics of P is given by a
transition system TP = hC, →i, where C is the set of possible configurations, i.e.,
finite subsets of ground atoms, and →⊆ C × C is a relation defined as follows.
For ∆, ∆0 ∈ C and a rule hC, D, Ai ∈ P, ∆ → ∆0 if there exists σ s.t. ∆ |= Cσ
and ∆0 = (∆ \ Dσ) ∪ Aσ.
Definition 8. A computation is a sequence of configurations ∆0 ∆1 . . . s.t. ∆i →
∆i+1 for i ≥ 0.
We use →∗ to denote the reflexive and transitive closure of →.
Example 2. Let P be a protocol that contains the rule ∀X. link(X, E) ⊃ own(X, E).
Consider ∆ = {link(n1 , e1 ), link(n2 , e1 ), link(n3 , e3 ), own(n3 , e3 )}, we first no-
tice that ∆ does not satisfy the condition
link(X, Y ) ∧ ∀Z.link(Z, Y ) ⊃ ¬own(Z, Y )
with the interpretation σ = [n3 /X, e3 /Y ]. Indeed, we have that
– ∆ 6|= link(n3 , e3 ) ∧ ∀Z.link(Z, e3 ) ⊃ ¬own(Z, e3 );
– ∆ |= link(n3 , e3 ) and ∆ 6|= ∀Z.link(Z, e3 ) ⊃ ¬own(Z, e3 );
– ∆ 6|= ∀Z.link(Z, e3 ) ⊃ ¬own(Z, e3 );
– ∆ |= link(n1 , e3 ) ⊃ ¬own(n1 , e3 ), since own(n1 , e3 ) 6∈ ∆, link(n1 , e3 ) ∈ ∆;
– ∆ |= link(n2 , e3 ) ⊃ ¬own(n2 , e3 ), since own(n2 , e3 ) 6∈ ∆, link(n2 , e3 ) ∈ ∆;
– ∆ 6|= link(n3 , e3 ) ⊃ ¬own(n3 , e3 ), since own(n3 , e3 ), link(n3 , e3 ) ∈ ∆.
However, ∆ satisfies the condition link(X, Y ) ∧ ∀Z.link(Z, Y ) ⊃ ¬own(Z, Y )
with the interpretation σ = [n1 /X, e1 /Y ]. Indeed, we have that
– ∆ 6|= link(n1 , e1 ) ∧ ∀Z.link(Z, e1 ) ⊃ ¬own(Z, e1 );
– ∆ |= link(n1 , e1 ) and ∆ 6|= ∀Z.link(Z, e1 ) ⊃ ¬own(Z, e1 );
– ∆ 6|= ∀Z.link(Z, e1 ) ⊃ ¬own(Z, e1 );
– ∆ |= link(n1 , e1 ) ⊃ ¬own(n1 , e1 ), since own(n1 , e1 ) 6∈ ∆, link(n1 , e1 ) ∈ ∆;
– ∆ |= link(n2 , e1 ) ⊃ ¬own(n2 , e1 ), since own(n2 , e1 ) 6∈ ∆, link(n2 , e1 ) ∈ ∆;
– ∆ |= link(n3 , e3 ) ⊃ ¬own(n3 , e1 ), since own(n3 , e1 ) 6∈ ∆, link(n3 , e1 ) ∈ ∆.
Starting from ∆0 = ∆ we obtain then a successor configuration
∆1 = ∆0 ∪ {own(n3 , e3 )}
Now, let P be a protocol that contains the rule
hlink(X, Y ), {own(X, Y )}, ∅i
Starting from ∆1 , we can reach ∆0 . Indeed, we have that ∆0 |= link(n3 , e3 ), and
that ∆1 = ∆0 \ {own(n3 , e3 )}.
In a single step of the operational semantics a rule is evaluated in the current
configuration by taking a sort of closed-word assumption, i.e., ground atoms
that do not occur in a configuration are evaluated to false. Furthermore, 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 ∆ 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.
For a set S of configurations, we define the following sets:
P ost(S) = {∆0 | ∃∆ ∈ S, ∆ → ∆0 }
P re(S) = {∆0 | ∃∆ ∈ S, ∆0 → ∆}
We use P ost∗ (S) (resp. P re∗ (S)) to denote the reflexive-transitive closure of
P ost (resp. P re).
2.2 Derived and Unary Predicates
In the rest of the section we will introduce formulas that define special condi-
tions on agents and edges. The formula isoN (n) = ¬∃X.(∨r∈P r(n, X)) specifies
an isolated agent n, i.e., that is not involved in any relation in P . Similarly, the
formula isoE(e) = ¬∃X.(∨r∈P r(X, e)) specifies an edge that is not involved in
any relation in P . Conditions like isoN (n) and isoE(e) are building blocks for
the definition of other types of derived predicates. This pattern can be applied
anytime it is necessary to avoid interference when constructing new predicates
and relations. For instance, if isoE(e) holds, then we define rules to add predi-
cates like q(n, e) that associate a state/label q to agent n. Similarly, if isoN (n)
holds, then we can add predicates like q(n, e) to associate a state/label to edge
e. For the sake of simplicity, in the rest of the paper we use unary predicates,
e.g. q(X) and q(E), instead of binary predicate in which one of the arguments
is used only as placeholder (e.g. associated to an isolated agent/edge) as in the
previous examples.
3 Decision Problem
We consider decision problems that generalize the standard notion of reacha-
bility 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 agents and edges. For this purpose, we introduce the
∃-reachability problem defined as follows.
Definition 9. Given a protocol P, a set of target configurations T and a possibly
infinite set of initial configurations I, ∃-reachability is satisfied for P, I and
T , written ∃Reach(P, I, T ), if there exists ∆ ∈ T and a configuration ∆1 s.t.
∆1 ∈ P ost∗ (I) and ∆ ⊆ ∆1 .
In other words ∃Reach(P, I, T ) holds if there exists a configuration ∆0 ∈ I s.t.
∆0 →∗ ∆1 and ∆ ⊆ ∆1 for some ∆ ∈ T .
In the rest of the paper we will generalize the problem by considering patterns
defined via existentially quantified formulas. Generalized ∃-reachability is defined
as follows.
Definition 10. Given a protocol P and a formula Φ with free variables in S
and a set of initial configurations I, generalized ∃-reachability is satisfied for P,
I, and Φ, written ∃Reach(P, I, Φ), if there exists an interpretation σ, a configu-
ration ∆ s.t. ∆ |= Φσ, and a configuration ∆1 s.t. ∆1 ∈ P ost∗ (I) and ∆ ⊆ ∆1 .
3.1 Undecidability
The ∃-Reachability problem turns out to be undecidable. A proof can be con-
structed by reducing the halting problem for Turing machines to ∃-reachability.
The idea of the construction is as follows. Let M = hΣ, Q, δ, q0 , F i be a Turing
machine in which Q is the set of control states, Σ is the tape alphabet that
includes the special blank symbol B, F ⊆ Q is the set of final states, q0 is the
initial state, and δ : Q × Σ → Q × Σ × {L, R} is the transition relation. Given
an input word w ∈ Σ ∗ without blanks, we first define a bipartite graph that
encodes w. We use here three types of relations:
– The atomic formula q(n1 , e1 ) is used to represent the state of the head point-
ing to cell n1 .
– The atomic formula `(n1 , e1 ) is used to represent a cell n1 containing symbol
`.
– The atomic formula next(n2 , e1 ) is used to link, via edge e1 , a cell to its
successor cell identified by agent n2 .
Creation of the word w = a1 . . . an and initialization of the tape head are defined
by the rule (∧ni=1 isoN (Xi ) ∧ isoE(Ei ), ∅, A), where
A = {q0 (X1 , E1 ), a1 (X1 , E1 ), next(X2 , E1 ), a2 (X2 , E2 ), . . . , an (Xn , En )}
This rule selects n isolated agents and edges and defines a zig-zag graph in which
we keep the information about letters and pointers to the adjacent cells.
To simulate a transition δ(q1 , a) = hq2 , b, Ri we use the rules r1 = hC1 , D1 , A1 i
and r2 = hC2 , D2 , A2 i, where
W
– C1 = q1 (X1 , E1 ) ∧ a(X1 , E1 ) ∧ next(X2 , E1 ) ∧ `∈Σ `(X2 , E2 ),
– D1 = {q1 (X1 , E1 ), a(X1 , E1 )} and A1 = {q2 (X2 , E2 ), b(X2 , E2 )}.
– C2 = q1 (X1 , E1 ) ∧ a(X1 , E1 ) ∧ isoN (X2 ) ∧ isoE(E2 ) ∧ ¬∃Z.next(Z, E1 ),
– D2 = {q1 (X1 , E1 ), a(X1 , E1 )},
– A2 = {next(X2 , E1 ), q2 (X2 , E2 ), b(X2 , E2 )}.
The former rule updates the relation associated to the encoding of the cell
pointed to by the head assuming that there exists another cell at its right. If
there are no representations of cells at its right, i.e., the relation next is not de-
fined, the latter rule can be applied to generate a representation of a blank cell.
To simulate a transition δ(q1 , a) = hq2 , b, Li we use the rules r3 = hC3 , D3 , A3 i
and r4 = hC4 , D4 , A4 i where
W
– C3 = q1 (X2 , E2 ) ∧ a(X2 , E2 ) ∧ next(X2 , E1 ) ∧ `∈Σ `(X1 , E1 ),
– D3 = {q1 (X2 , E2 ), a(X2 , E2 )} and A3 = {q1 (X1 , E1 ), b(X2 , E2 )}.
– C4 = q1 (X1 , E1 ) ∧ a(X1 , E1 ) ∧ isoN (X2 ) ∧ isoE(E2 ) ∧ ¬∃F.next(X1 , F ),
– D4 = {q1 (X1 , E1 ), a(X1 , E1 )},
– A4 = {next(X1 , E2 ), q2 (X2 , E2 ), b(X1 , E1 ), B(X2 , E2 )}.
The former rule updates the relation associated to the encoding of the cell
pointed to by the head assuming that there exists another cell at its left. If
there are no representations of cells at its left, the latter rule can be applied to
generate a representation of a blank cell.
The set of initial configurations I consists of an arbitrary number of isolated
agents and edges, i.e., it contains a configuration ∆n,m for each possible number
n of agents and m of edges. Let us indicate with ∆ the configuration of the
Turing machine represented by ∆.
Namely, if
∆ = {a1 (n1 , e1 ), next(n2 , e1 ), a2 (n2 , e2 ), . . . , ak (nk , ek ), qi (nj , ej )}
then ∆ = a1 . . . aj−1 qi aj . . . ak . By construction, the application of a rule pro-
duced by the encoding preserve the well-formedness of the encoding of configu-
rations. The following properties then holds.
Proposition 1. Let PM be the encoding of the Turing machine M and ∆0 ∈ I.
If ∆0 →∗ ∆1 , then there exists a computation in M from ∆0 to ∆1 .
Indeed, by construction, each step of a computation in PM mimics the applica-
tion of transitions in M . ∆0 contains finitely many agents and edges, the size of
visited part of tape in the computation in M is bounded by the cardinality of
∆0 .
Proposition 2. Let PM be the encoding of the Turing machine M and γ0 = q0 w
an initial configuration of M on input w. If γ1 is reachable from γ0 , then there
exists ∆0 ∈ I and ∆1 s.t. ∆0 = γ0 , ∆1 = γ1 , and ∆0 →∗ ∆1 .
If γ1 is reachable from γ0 , then there is a finite upperbound k on the number
of cells visited by the machine. Let ∆0 be an initial configuration with at least
n (isolated) agents and edges. By applying a creation rule, we can generate a
configuration ∆00 that represents the initial configuration γ0 . By construction of
PM , a step from γi to γi+1 can be simulated by the application of a rule in PM .
The choice of ∆0 ensures us that we can always select isolated agents and edges
when needed, i.e., when the machine moves to a blank cell to the left or right of
the visited part of the tape.
The following property then holds.
Theorem 1. Let PM be the encoding of the Turing machine M . The Halting
W for M can be reduced to ∃-Reachability in PM by taking the formula
problem
Φ = q∈F q(X, Y ) as representation of subconfigurations denoting a final state.
4 Modelling
In this section we consider possible application of BLog to the specification of
distributed protocols. The key ingredient of the specification language is the com-
bination of complex conditions and update rules to reason on bipartite graphs
in which predicates can be viewed as labels of links between agents and edges.
We have shown that we can also add labels to individual agents and edges, e.g.,
to represent their current state. Update rules can be used to dynamically re-
configure the graph, i.e., change labels, topology and add or delete agents. The
separation between agents and edges is convenient to model asynchronous com-
munication. For instance, let us consider a protocol in which two agents need to
establish a connection via a shared buffer.
– An agent n1 of type A connects to an edge e1 in idle state (the buffer is free)
and sets the state of the buffer to ready.
– An agent n2 of type B connects to e1 in state ready and changes the state
to readyack.
– Agent n1 sends message m by changing the state of e1 to msgm .
– Agent n2 receive message m and updates the state of the channel to readyack
for further communications.
The protocol can be specified as follows. We use unary predicates to associate
states to edges.
1
Rule reqA = (C1 , D1 , A1 ) is s.t. C1 = idle(E) ∧ ¬send(X, E),
D1 = {idle(E)}, A1 = {ready(E), req(X, E)}
1
Rule reqB = (C2 , D2 , A2 ) is s.t. C2 = ready(E) ∧ ¬rec(X, E),
D2 = {ready(E)}, A2 = {readyack(E), rec(X, E)}.
2
Rule reqA = (C3 , D3 , A3 ) is s.t. C3 = readyack(E) ∧ send(X, E),
D3 = {readyack(E), send(X, E)}, A3 = {msgm (E)}
3
Rule reqA = (C4 , D4 , A4 ) is s.t. C4 = msgm (E) ∧ rec(X, E),
D4 = {msgm (E), rec(X, E)}, A4 = {idle(E)}
An initial state consists of a bipartite graph defined by the configuration of
the following form idle(e1 ), . . . , idle(ek ), where ei 6= ej for i 6= j, i, j : 1, . . . , k.
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 by using rules like (C, D, A) defined as:
– C = link(X, E) ∧ s1 (X, F ) ∧ link(Y, E) ∧ s2 (Y, G)
– D = {s1 (X, F ), link(X, E), link(Y, E), s2 (Y, G)}
– A = {link(X, E), s01 (X, F ), link(Y, E), s02 (Y, G)}
where s1 (X, F ) is a relation used to denote state of agent X, link(X, E), link(Y, E)
is a relation used to share a common buffer E, and s2 (Y, G) is a relation used
to denote state of agent Y , etc.
5 Distributed Dining Philosophers
We consider here a distributed version of the dining philosopher mutual exclusion
problem presented in [14]. 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 neigh-
bors 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 simultaneosly.
The protocol should be robust under dynamic reconfigurations of the network.
5.1 Formal Specification of DDP
In this section we present a formal specification of the DPP protocol. Network
configurations are expressed as BLog 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 a agent to a possibly shared buffer. To model dynamic
reconfigurations, we can non-deterministically add and remove link predicates
between pairs of agents and edges. To model buffers with states, we use special
relations in which agents are initially isolated. Asynchronous communication is
modelled as in the previous example, i.e., agents interact only via a common
edge. Communication between two agents is not atomic. Instead of modelling
identifiers and buffers with data, we introduce a special relation own that is
used to model ownership of a given edge to which a agent is linked. Ownership
is normed in the same way as the labelling of buffers in the original protocol, i.e.,
an agent can acquire ownership only if the edge is not owned by other agents.
In our framework we model this behavior using the following predicates and
rules.
Rule link = (C1 , D1 , A1 ) is defined s.t. C1 = ¬link(X, E), D1 = ∅, A1 =
{link(X, E)}.
Rule unlink = (C2 , D2 , A2 ) is defined s.t. C2 = link(X, E), D2 = {link(X, E)},
A2 = ∅.
Rule getE = (C3 , D3 , A3 ) is s.t. C3 = link(X, E) ∧ ∀Z.¬own(Z, E), D3 = ∅,
A3 = {own(X, E)}.
Rule relE = (C4 , D4 , A4 ) is s.t.: C4 = D4 = {own(X, E)}, A4 = ∅.
Rule acquire = (C5 , D5 , A5 ) is s.t. C5 = idle(X)∧∀E.(link(X, E) ⊃ own(X, E)),
D5 = {idle(X)}, A5 = {busy(X)}.
Rule release = (C6 , D6 , A6 ) is defined s.t. C6 = D6 = {busy(X)}, A6 =
{idle(X)}.
An initial state consists of a bipartite graph defined by a configuration of the
following form idle(n1 ), . . . , idle(nk ), where ni 6= nj for i 6= j, i, j : 1, . . . , k and
k ≥ 1.
Correctness Mutual exclusion for the considered protocol can be formulated
in its more general form, i.e., for any number of agents, as the negation of an
∃-reachability problem. More specifically, let Φ be the formula
busy(N ) ∧ busy(M ) ∧ link(N, G) ∧ link(M, G)
that denotes a configurations in which two agents share the same channel. We
have that ∃Reach(PM , I, Φ) holds if and only if mutual exclusion does not hold
for DDP.
6 Verification via Transformation Rules
In this section we define a sort of canonical form for computations in Pddp
obtained via permutation and deletion schemes that we can be uses to synthesize
derived rules that are equivalent w.r.t. our correctness criteria.
6.1 Permutation and Deletion Schemes
We first consider deletion and permutation properties of rule applications within
a given computation. We focus our attention on link and unlink rules, i.e., dy-
namic reconfigurations of the graph topology. Let θ = ∆0 ∆1 ∆2 be a computation
in Pddp and let r1 , r2 be the transitions applied in each step.
– We first observe that if r2 is an instance of the unlink rule applied to n1 , e1 ,
and r1 is an instance of rule link applied to the same pair, they can be
eliminated since ∆0 = ∆2 .
– If r1 is an instance of the getE rule applied to agent n1 , e1 , and r2 is an
application of relE applied to the same pair, then they can be eliminated
since ∆0 = ∆2 .
– We now observe that unlink can be permuted with every other rule applied
to different pairs to its left in a computation. Namely, if r2 is an instance
of the unlink rule applied to n1 , e1 , and r1 is a rule that is not applied to
n1 , e1 , then we can permute the application of the two rules and obtain a
new computation leading to the same configuration.
– If r1 is an instance of the link rule applied to n1 , e1 , and r2 is an application of
any other rule on a different pair, then we can permute the applications of the
two rules and obtain a new computation leading to the same configuration.
We can now reason on the previous properties in order to consider sets of equiv-
alent computations and infer derived blocks of rules and new permutation rules.
More specifically, given a computation θ we can obtain an equivalent, w.r.t. our
correctness criteria, computation θ0 by applying the following steps:
– We can eliminate all applications of reconfigurations, i.e., link and unlink,
performed on the same pair n, e, if in between their occurrences in a compu-
tation there are no occurrences of instances of getE on the same pair. The
property can be obtained by repeatedly applying permutation rules so as to
push applications of link towards the first occurrence of unlink and then
apply the corresponding deletion rules.
– We can eliminate all applications of acquire getE and relE on the same pair
n, e, if there are no occurrences of acquire involving n in between. Again,
the property can be obtained by repeatedly applying permutation rules so
as to push applications of relE towards the first occurrence of getE to its
left.
– We can push the application of link rules close to the first occurrence of a
corresponding getE rule to its left.
Following from the previous properties, from any computation we can extract
a subcomputation in which occurrences of relE occur only after occurrences
of acquire on the same pair. Similarly, we can push occurrences of unlink so
as to occur only after occurrences of acquire. In other words we can derive
rules obtained by combining link and reqE. The resulting pattern, link reqE,
is used to simultaneously link an agent to an edge and acquire its ownership.
Similarly, since computations in which relE and unlink on specific pairs occur
after acquire, we can use permutations in order to cluster all occurrences of
patterns relE unlink occurring before an acquire. In other words, we can use
permutations of patterns link reqE with other rules or patterns operating on
different agents, in order to push all their occurrences close to the first acquire on
their right involving the same agent. This properties leads to patterns of the form
(link reqE)∗ acquire. We now observe that the pattern can be used by agent n
to simultaneously acquire the ownership of a given set of edges e1 , . . . , en , and
update the local state to busy. We can reason on permutations of unlink, relE
and release in a similar way, i.e., apply permutations to cluster the sequence
of applications of these rules involving the same agent after an acquire. The
resulting sequence can be represented by the pattern (relE unlink)∗ release. In
other words in the resulting patterns the link relation is updated in parallel with
the own relation.
6.2 Derived Rules
The pattern (link reqE)∗ acquire cannot be represented via a single rule in our
specification language, since it may involve an arbitrary number of edges. To ex-
press this pattern, we can use a family {rk }k≥0 of rules, where rk = (Ck , Dk , Ak )
is defined as:
Vk Vk
– Ck = idle(X) ∧ i=1 ¬link(X, Ei ) ∧ ∀Z. i=1 ¬own(Z, Ei ),
– Dk = {idle(X)},
– Ak = {busy(X), link(X, E1 ), own(X, E1 ), . . . , link(X, Ek ), own(X, Ek )}.
The rule associates agent X to an arbitrary subset of edges. The association is
defined via the ownership predicate.
The pattern (relE unlink)∗ release is expressed by the infinite family {sk }k≥0
of rules. Rule sk = (Ck , Dk , Ak ) is defined as:
Vk
– Ck = busy(X) ∧ i=1 link(X, Ei ) ∧ own(X, Ei ),
– Dk = {busy(X), link(X, E1 ), own(X, E1 ), . . . , link(X, Ek ), own(X, Ek )},
– Ak = {idle(X)}.
This rule can be applied to a subset of all edges connected to a given agent. This
corresponds to a sequence of applications on release and relE.
6.3 Deductive Reasoning
To verify correctness, we have to prove that the formula
Ψ = ¬∃X, Y.busy(N ) ∧ busy(M ) ∧ link(N, G) ∧ link(M, G)
is an invariant for our system. To prove the property, we will strenghten the
invariant proving that
Ψ0 = Υ ∧ Ψ
where Υ = (∀Z, E.link(Z, E) ⊃ own(Z, E)), is still an invariant of the resulting
rule. By definition Ψ 0 holds in any initial configuration ∆m,n , since initial con-
figurations only contain agents in state idle. The key point is to show that Ψ 0 is
preserved by applications of rule rk and sk for any k ≥ 0.
Consider a configuration ∆ with cardinality n and assume that ∆ |= Ψ 0 . Now
consider rk s.t. k ≤ n. If rk can be appliedVk to ∆, there exists V an interpretation σ
k
s.t. ∆ |= Ck σ where Ck = (idle(X)∧ i=1 ¬link(X, Ei )∧∀Z. i=1 ¬own(Z, Ei )).
This implies that there exists an agent n s.t. idle(n) ∈ ∆, and there exist
e1 , . . . , en s.t. link(m, ei ), own(m, ei ) 6∈ ∆ for i : 1, . . . , k and for any m oc-
curring in ∆. The application of the rule yields a configuration ∆0 defined as
∆0 = ∆ ∪ {link(n, e1 ), . . . , link(n, ek ), own(n, e1 ), . . . , own(n, ek ), busy(n)}
Since by assumption own(m, ei ), link(m, ei ) 6∈ ∆ for any m occurring in ∆ and
i : 1, . . . , k, we have that ∆0 |= Ψ 0 .
Now consider a configuration ∆ with cardinality n and assume that ∆ |= Ψ 0 .
Now consider sk s.t. k ≤ n. If sk can be applied Vk to ∆, there exists an interpreta-
tion σ s.t. ∆ |= Ck σ where Ck = (busy(X)∧ i=1 link(X, Ei )∧own(X, Ei )). This
implies that there exists an agent n s.t. busy(n) ∈ ∆, and there exist e1 , . . . , en
s.t. link(n, ei ), own(n, ei ) ∈ ∆ for i : 1, . . . , k. The application of the rule yields
a configuration ∆0 defined as
∆0 = ∆ \ {link(n, e1 ), . . . , link(n, ek ), own(n, e1 ), . . . , own(n, ek )} ∪ {idle(n)}
Although the rule might remove a strict subset of link and own predicates
involving n, the resulting configuration still satisfies Ψ 0 .
Since ∆, k, and σ are chosen in arbitrary way, we have that the considered
invariant Φ0 is an invariant for the whole family of rules of type sk and rk with
k ≥ 0.
Finally, we observe that for any ∆ we have that if ∆ |= Ψ 0 then ∆ |= Ψ . This
prove that Ψ is still an invariant for the model resulting from the transformation
described in the previous sections.
7 Conclusions and Related Work
We have presented a formal language for the specification of asynchronous dis-
tributed systems based on logic-based update rules for bipartite graphs. For
the considered language, we have presented a verification approach that com-
bines transformation schemes based on permutation properties and inductive
verification. The proposed approach can be applied to verify the correctness
of a distributed version of the dining philosopher protocol regardless the net-
work topology and the number of nodes. Mechanization of the considered proof
method could be an interesting direction for future work.
References
1. P. Liu andT. Wahl. Infinite-state backward exploration of boolean broadcast pro-
grams. In Formal Methods in Computer Aided Design, FMCAD ’14, pages 155–162,
2014.
2. Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Laure Petrucci. FAST: accel-
eration from theory to practice. STTT, 10(5):401–424, 2008.
3. E. A. Emerson and K. S. Namjoshi. On model checking for non-deterministic
infinite-state systems. In Thirteenth Annual IEEE Symposium on Logic in Com-
puter Science, Indianapolis, Indiana, USA, June 21-24, 1998, pages 70–80, 1998.
4. F. Fioravanti, A. Pettorossi, M. Proietti, and V. Senni. Improving reachability
analysis of infinite state systems by specialization. Fundam. Inform., 119(3-4):281–
300, 2012.
5. P. Ganty and A. Rezine. Ordered counter-abstraction - refinable subword relations
for parameterized verification. In Language and Automata Theory and Applications
- 8th International Conference, LATA 2014, Madrid, Spain, March 10-14, 2014.
Proceedings, pages 396–408, 2014.
6. S. M. German and A. P. Sistla. Reasoning about systems with many processes. J.
ACM, 39(3):675–735, 1992.
7. S. Ghilardi and S. Ranise. Backward reachability of array-based systems by SMT
solving: Termination and invariant synthesis. Logical Methods in Computer Sci-
ence, 6(4), 2010.
8. B. Bagheri Hariri, D. Calvanese, G. De Giacomo, A. Deutsch, and M. Montali.
Verification of relational data-centric dynamic systems with external services. In
Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGART Symposium on Princi-
ples of Database Systems, PODS 2013, New York, NY, USA - June 22 - 27, 2013,
pages 163–174, 2013.
9. A. Kaiser, D. Kroening, and T. Wahl. Lost in abstraction: Monotonicity in multi-
threaded programs. In CONCUR 2014 - Concurrency Theory - 25th International
Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, pages
141–155, 2014.
10. A. Kaiser, D. Kroening, and Thomas Wahl. A widening approach to multithreaded
program verification. ACM Trans. Program. Lang. Syst., 36(4):14, 2014.
11. B. König and V. Kozioura. Augur 2 - A new version of a tool for the analysis of
graph transformation systems. Electr. Notes Theor. Comput. Sci., 211:201–210,
2008.
12. D. Kroening. Automated verification of concurrent software. In Reachability Prob-
lems - 7th International Workshop, RP 2013, Uppsala, Sweden, September 24-26,
2013 Proceedings, pages 19–20, 2013.
13. R. Meyer and T. Strazny. Petruchio: From dynamic networks to nets. In Computer
Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK,
July 15-19, 2010. Proceedings, pages 175–179, 2010.
14. K. S. Namjoshi and R. J. Trefler. Uncovering symmetries in irregular process
networks. In VMCAI, pages 496–514, 2013.
15. Kedar S. Namjoshi and Richard J. Trefler. Analysis of dynamic process networks.
In Tools and Algorithms for the Construction and Analysis of Systems - 21st Inter-
national Conference, TACAS 2015, Held as Part of the European Joint Conferences
on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015.
Proceedings, pages 164–178, 2015.
16. J. Stückrath. Uncover: Using coverability analysis for verifying graph transfor-
mation systems. In Graph Transformation - 8th International Conference, ICGT
2015, Held as Part of STAF 2015, L’Aquila, Italy, July 21-23, 2015. Proceedings,
pages 266–274, 2015.
17. https://github.com/pierreganty/mist.
18. http://users.mat.unimi.it/users/ghilardi/mcmt/.
19. http://www.ahmedrezine.com/tools/.
20. http://www.ccs.neu.edu/home/wahl/Research/boom-and-cutoffs.html.
21. http://www.it.uu.se/research/docs/fm/apv/tools/pfs/.
22. http://www.it.uu.se/research/docs/fm/apv/tools/undip/.
23. http://www.liafa.jussieu.fr/~sighirea/trex/.
24. http://www.lsv.ens-cachan.fr/Software/fast/.
25. http://www.montefiore.ulg.ac.be/~boigelot/research/lash/.
26. http://www.ti.inf.uni-due.de/de/research/tools/uncover/.