Structural Invariants for Parameterized Architectures
231
Intuitively, the transitions of the system with n dining philosophers and n forks are
given by the minimal models of the disjuncts of Γ philo with universe {0, 1,..., n − 1}, and
succ interpreted as “successor modulo n’. In particular, for each 0 ≤ k ≤ n − 1 the first
disjunct has a minimal model that interprets the predicates g and t as the sets {k} and
{k, (k + 1) mod n}. This model describes the interaction in which the k-th philosopher
takes a g-transition (from waiting to eating), while, simultaneously, the k-th and (k + 1)th forks take t-transitions (from free to busy). This is graphically represented by one of
the dashed lines in Fig. 1. Observe that the ring topology of the system is implicit in the
modulo-n interpretation of the successor function.
Since philosophers can only grab their two forks simultaneously, the system is
deadlock-free for any number n ≥ 2 of philosophers. An automatic proof requires to
compute an invariant, and prove that it has an empty intersection with the set of deadlock configurations defined by the WSκS formula
deadlock(X w , X e , X f , X b ) = ∀i . [¬X w (i) ∨ ¬X f (i) ∨ ¬X f (succ(i))] ∧
[¬X e (i) ∨ ¬X b (i) ∨ ¬X b (succ(i))]
(2)
where X w , X e , X f , X b are set variables, the intended meaning of X w (i) resp. X e (i) is that
the i-th philosopher is waiting, resp. eating, and the intended meaning of X f (i) resp.
X b (i) is that the i-th fork is free, resp. busy. Our method automatically computes from
Γ philo a formula trap-invariant S which formalizes an inductive invariant of the system.
Moreover, we express the consistency requirement that every component is in one of
its state at all times in a formula marking S and derive the deadlock-freeness for any
number of philosophers by the unsatisfiability of the formula
deadlock ∧ trap-invariant S ∧ marking S .
2 Parameterized Component-based Systems
A component type is a tuple C = P, S, s 0 ,Δ, where P = {p, q, r,...} is a finite set of
ports, S is a finite set of states, s 0 ∈ S is an initial state and Δ ⊆ S × P × S is a set of
transitions denoted s
p
−
→ s , for s, s ∈ S and p ∈ P. We assume there are no two different
transitions with the same port.
A component-based system S = C
1
,..., C
N
,Γ consists of a fixed number N ≥ 1
of component types C
k
= P
k
, S
k
, s 0
k
,Δ
k
and an interaction formula Γ. In the dining
philosophers there are two component types, Philosopher and Fork, each with two
states and two transitions, as shown in Fig. 1. We assume that P
i
∩P
j
= ∅ and S
i
∩S
j
= ∅,
for all 1 ≤ i < j ≤ N. We denote the component type of a port p or a state s by type(p)
and type(s), respectively. For instance, in Fig. 1 we have type(p) = type(g) = type(w) =
type(e) = Philosopher and type(t) = type() = type( f ) = type(b) = Fork.
The interaction formula Γ determines the family of systems we can construct out
of these components. It does so by specifying, for each possible number of replicated
instances (for example, 3 philosophers and 3 forks), which are the possible interactions between them. An interaction consists of a set of transitions that are executed
simultaneously. For example, in an interaction philosopher 3 executes a g(et) transition
simultaneously with t(ake) transitions of the forks 2 and 3. Before formalizing this, we
introduce the syntax and semantics of Interaction Logic.
231
Intuitively, the transitions of the system with n dining philosophers and n forks are
given by the minimal models of the disjuncts of Γ philo with universe {0, 1,..., n − 1}, and
succ interpreted as “successor modulo n’. In particular, for each 0 ≤ k ≤ n − 1 the first
disjunct has a minimal model that interprets the predicates g and t as the sets {k} and
{k, (k + 1) mod n}. This model describes the interaction in which the k-th philosopher
takes a g-transition (from waiting to eating), while, simultaneously, the k-th and (k + 1)th forks take t-transitions (from free to busy). This is graphically represented by one of
the dashed lines in Fig. 1. Observe that the ring topology of the system is implicit in the
modulo-n interpretation of the successor function.
Since philosophers can only grab their two forks simultaneously, the system is
deadlock-free for any number n ≥ 2 of philosophers. An automatic proof requires to
compute an invariant, and prove that it has an empty intersection with the set of deadlock configurations defined by the WSκS formula
deadlock(X w , X e , X f , X b ) = ∀i . [¬X w (i) ∨ ¬X f (i) ∨ ¬X f (succ(i))] ∧
[¬X e (i) ∨ ¬X b (i) ∨ ¬X b (succ(i))]
(2)
where X w , X e , X f , X b are set variables, the intended meaning of X w (i) resp. X e (i) is that
the i-th philosopher is waiting, resp. eating, and the intended meaning of X f (i) resp.
X b (i) is that the i-th fork is free, resp. busy. Our method automatically computes from
Γ philo a formula trap-invariant S which formalizes an inductive invariant of the system.
Moreover, we express the consistency requirement that every component is in one of
its state at all times in a formula marking S and derive the deadlock-freeness for any
number of philosophers by the unsatisfiability of the formula
deadlock ∧ trap-invariant S ∧ marking S .
2 Parameterized Component-based Systems
A component type is a tuple C = P, S, s 0 ,Δ, where P = {p, q, r,...} is a finite set of
ports, S is a finite set of states, s 0 ∈ S is an initial state and Δ ⊆ S × P × S is a set of
transitions denoted s
p
−
→ s , for s, s ∈ S and p ∈ P. We assume there are no two different
transitions with the same port.
A component-based system S = C
1
,..., C
N
,Γ consists of a fixed number N ≥ 1
of component types C
k
= P
k
, S
k
, s 0
k
,Δ
k
and an interaction formula Γ. In the dining
philosophers there are two component types, Philosopher and Fork, each with two
states and two transitions, as shown in Fig. 1. We assume that P
i
∩P
j
= ∅ and S
i
∩S
j
= ∅,
for all 1 ≤ i < j ≤ N. We denote the component type of a port p or a state s by type(p)
and type(s), respectively. For instance, in Fig. 1 we have type(p) = type(g) = type(w) =
type(e) = Philosopher and type(t) = type() = type( f ) = type(b) = Fork.
The interaction formula Γ determines the family of systems we can construct out
of these components. It does so by specifying, for each possible number of replicated
instances (for example, 3 philosophers and 3 forks), which are the possible interactions between them. An interaction consists of a set of transitions that are executed
simultaneously. For example, in an interaction philosopher 3 executes a g(et) transition
simultaneously with t(ake) transitions of the forks 2 and 3. Before formalizing this, we
introduce the syntax and semantics of Interaction Logic.