Go backward to Source Code Go up to Top |
We are going to formally verify the assertion stated by the program: as soon
as node 0 has signalled by its variable sent
the initialization of the
network, there must be exactly two messages in the network.
For the purpose of verification, we rewrite the method main
as follows:
public void main() { int i; int state = 0; while (state != 8) { switch (state) { case 0: { if (number = 0) state = 1; else state = 3; } case 1: { out(0).send(new Msg(0)); state = 2; } case 2: { out(1).send(new Msg(0)) sent = true; state = 3; } case 3: { i = 0; state = 4; } case 4: { if (i < 5) state = 5; else state = 8; } case 5: { index = in().select(); state = 6; } case 6: { msg = in(index).receive(); state = 7; } case 7: { out(index).send(msg); msg = null; i = i+1; state = 4; } } } }
This program implements the same behavior as the original one presented in the
previous subsection by a sequence of state transitions such that the only
interaction with other nodes (send
, receive
, select
)
occurs as the first statement of some transition. A node program may be
interrupted only immediately before such a communication operation takes
place. Network execution can be therefore considered as an interleaving of
such transitions from the programs of different nodes.
To establish the truth of a global invariant, it thus suffices to prove
A => I
I =>o I
where A describes the initial state of the network (immediately before the transition loop is entered) and the implication I =>o I denotes the invariance of I on every state transition (i.e., if I holds immediately before the transition, it must also hold after the transition).
The initial condition A of our network is defined as
A :<=>
forall j
(outj(0).length = 0, outj(1).length = 0,
~sentj, msgj = null, statej = 0)
i.e., all channels are empty, the local variables are initialized as described by the program constructor, and programs start with initial state 0.
We want to prove invariant I defined as
I :<=> sent0 => C(2)which is exactly the assertion implemented in the previous section. A subscripted variable vj denotes the content of variable
C(c) :<=> c = Sumj (outj(0).length + outj(1).length + nj)
where
nj = 0, if msgj = null
nj = 1, else
v
in program j
(j is represented in the program by the
variable number
). outj(i) denotes the array of messages
out(i).getMessages()
in program j.
For the purpose of verification, we need a couple of auxiliary propositions that describe the state at the beginning of each transition:
Sj0 :<=> statej = 0 =>
msgj = null, j=0 => (C(0), ~sent0).
Sj1 :<=> statej = 1 =>
msgj = null, j = 0, C(0), ~sent0.
Sj2 :<=> statej = 2 =>
msgj = null, j = 0, C(1), ~sent0,
outj(1).length = 0.
Sj3 :<=> statej = 3 =>
msgj = null.
Sj4 :<=> statej = 4 =>
msgj = null.
Sj5 :<=> statej = 5 =>
msgj = null, ij < 5.
Sj6 :<=> statej = 6 =>
msgj = null, ij < 5,
indexj in {0, 1}, inj(indexj).length > 0.
Sj7 :<=> statej = 7 =>
msgj /= null, ij < 5,
indexj in {0, 1}.
Sj8 :<=> statej = 8 =>
msgj = null.
We will prove a generalized invariant I' defined as
I' :<=> I, forall j, k (Sjk)from which I trivially follows.
We are now going to prove
A => I'
I' =>o I'
For proving A => I', it suffices to prove A => I and A => forall j (Sj0) (both of which are direct consequences of A).
For proving I' =>o I', we have to establish the truth of I after the transition and to show Sjk; it suffices to consider only those j, k where
send
operation).
We proceed by case distinction on the current state of node j, i.e., on the value of statej:
send
or an assigment operation, nodes other than j are not
affected. There are two potential successor states; it thus suffices to prove
that the following conditions hold after the transition:
send
operation to some node j' /=j
might be the invalidation of Sj'6. However, the statement
satisfies the transition rulec.send(m)
c = q =>o c = q:m(i.e., it appends one element m to the message queue q of channel c), thus inj'(i).length > 0 cannot become false.
It remains to be shown that statej = 2 => Sj2 after the transition. From C(0) at the beginning of the transition, we know outj(1).length = 0, which remains true. Furthermore, by above transition rule, we can easily deduce outj(0).length = 1 and thus C(1) after the transition.
By same reasoning as for the previous case, no Sj'k is affected by the transition. That Sj3 holds after the transition follows directly from the code and from Sj2.
satisfies the transition rulei = s.select()
s.getSize() > 0 =>o 0 <= i < s.getSize(), s(i).length > 0and we know by network construction out.getSize() = 2. Thus, using Sj5, the truth of Sj6 is clear.
satisfies the transition rulem = c.receive()
c = n:q =>o m = n, c = q(for some non-null message n and message queue q). From this and Sj6 and knowing out.getSize() = 2 it is clear that, for some k in {0, 1} and non-negative l,
inj(k).length = 1+lholds before the transition, and that
inj(k).length = l, msgj /= nullholds after the transition and that k = indexj (both before and after the transition). From this and from the overall relationship between input and output channels
Sumj (inj(0).length + inj(1).length) =it is clear that I holds after the transition.
Sumj (outj(0).lenght + outj(1).length)
By above reasoning, it is also clear that Sj7 holds after the transition.
From Sj6 and by above relationship between input and output channels
we know before the transition outj'(p).length > 0 for some
j' /=j and p in {0, 1} (by network construction). Thus
state0 /=0, statej' /=1 (for all j'
/= j) and the transition cannot invalidate Sj'0 and
Sj'1. Sj'2 remains true because
out
j'(1).length() = 0 cannot be changed by a receive
operation; furthermore I and C(1) at the beginning of the
transition implies by the code and above rule also
C(1) at the end of the transition.
Sj'6 remains true because the truth of
inj'(indexj').length > 1 cannot be changed by a
receive
operation in j.
send
shown above.
Similar reasoning as in the previous case also shows that S0j',
Sj'1 and Sj'2 remain true. Sj'6 remains
true because the truth of inj'(indexj').length > 1
cannot be changed by a send
operation.
Thus we have established the invariance of I'.
Since each program loops through a bounded number of iterations, it is clear that the execution of the network will not run forever. It is however less clear whether all node programs actually reach the termination state. In fact, this is not guarantueed: two network programs may terminate in a state where both messages are captured in the channels between them; the third node will thus wait forever on its input channels.