Go backward to Source CodeGo 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=>II=>_{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

(out_{j}(0).length = 0,out_{j}(1).length = 0,

~sent_{j},msg_{j}= null,state_{j}= 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

which is exactly the assertion implemented in the previous section. A subscripted variableI:<=>sent_{0}=>C(2)C(c) :<=> c = Sum_{j}(out_{j}(0).length +out_{j}(1).length +n_{j})

where

n_{j}= 0, ifmsg_{j}= null

n_{j}= 1, else

`v`

in program `j`

(`number`

). `out(``i`).getMessages()

in program For the purpose of verification, we need a couple of auxiliary propositions that describe the state at the beginning of each transition:

S_{j}^{0}:<=>state_{j}= 0 =>

msg_{j}= null, j=0 => (C(0), ~sent_{0}).S_{j}^{1}:<=>state_{j}= 1 =>

msg_{j}= null,j= 0,C(0), ~sent_{0}.S_{j}^{2}:<=>state_{j}= 2 =>

msg_{j}= null,j= 0,C(1), ~sent_{0},

out_{j}(1).length = 0.S_{j}^{3}:<=>state_{j}= 3 =>

msg_{j}= null.S_{j}^{4}:<=>state_{j}= 4 =>

msg_{j}= null.S_{j}^{5}:<=>state_{j}= 5 =>

msg_{j}= null,i_{j}< 5.S_{j}^{6}:<=>state_{j}= 6 =>

msg_{j}= null,i_{j}< 5,

index_{j}in {0, 1},in_{j}(index_{j}).length > 0.S_{j}^{7}:<=>state_{j}= 7 =>

msg_{j}/= null,i_{j}< 5,

index_{j}in {0, 1}.S_{j}^{8}:<=>state_{j}= 8 =>

msg_{j}= null.

We will prove a generalized invariant `I`' defined as

from whichI' :<=>I, forall j, k (S_{j}^{k})

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
(`S`_{j}^{0}) (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 `S`_{j}^{k};
it suffices to consider only those j, k where

- j is the index of the current node and k denotes a potential successor state of the transition, or
- j is the index of another node and
`S`_{j}^{k}is potentially affected by the transition.

`send`

operation).
We proceed by case distinction on the current state of node j, i.e., on the
value of `state`_{j}:

- Assume
`state`_{j}= 0:`I`is true after the transition, because`sent`_{0}remains false. Since the transition does not involve a`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:`state`_{j}= 1 =>`S`_{j}^{1}:`S`_{j}^{1}holds because the premise implies that the "then" path of the conditional was taken and thus j = 0 holds.`state`_{j}= 3 =>`S`_{j}^{3}:`S`_{j}^{3}follows from`S`_{j}^{0}and the code.

- Assume
`state`_{j}= 1:`I`is true after the transition, because`sent`_{0}remains false. From`S`_{j}^{2}we know j = 0 which implies that`S`_{j'}^{0},`S`_{j'}^{1},`S`_{j'}^{2}remain true for j' /=j. The only effect of the the`send`

operation to some node j' /=j might be the invalidation of`S`_{j'}^{6}. However, the statement

satisfies the transition rule`c`.send(`m`)`c`=`q`=>_{o}`c`=`q`:`m``m`to the message queue`q`of channel`c`), thus`in`_{j'}(`i`).length > 0 cannot become false.It remains to be shown that

`state`_{j}= 2 =>`S`_{j}^{2}after the transition. From`C`(0) at the beginning of the transition, we know`out`_{j}(1).length = 0, which remains true. Furthermore, by above transition rule, we can easily deduce`out`_{j}(0).length = 1 and thus`C`(1) after the transition. - Assume
`state`_{j}= 2: we have to show that`I`remains true. By same reasoning as for the previous case, we get`out`_{j}(1).length = 1 after the transition. Together with`C`(1) and`out`_{j}(1).length = 1 at the beginning of the transition, we can deduce`C`(2) after the transition.By same reasoning as for the previous case, no

`S`_{j'}^{k}is affected by the transition. That`S`_{j}^{3}holds after the transition follows directly from the code and from`S`_{j}^{2}. - Assume
`state`_{j}= 3: from the code, the truth of`I`is self-evident, no`S`_{j'}^{k}is affected and by`S`_{j}^{3}also`S`_{j}^{4}is clear. - Assume
`state`_{j}= 4: it suffices to prove that the following conditions hold after the transition:`state`_{j}= 5 =>`S`_{j}^{5}:`i`< 5 holds because the premise implies that the "then" part of the conditonal was taken.`state`_{j}= 8 =>`S`_{j}^{8}: this is self-evident.

- Assume
`state`_{j}= 5: the truth of`I`is clear and`index`_{j}is not referenced in any`S`_{j'}^{k}with j' /=j. Thus it suffices to show that`S`_{j}^{6}holds after the transition. The statement

satisfies the transition rule`i`=`s`.select()s.getSize() > 0 =>

and we know by network construction_{o}0 <=`i`< s.getSize(),`s`(`i`).length > 0`out`.getSize() = 2. Thus, using`S`_{j}^{5}, the truth of`S`_{j}^{6}is clear. - Assume
`state`_{j}= 6: first we show the truth of`I`after the transition. The statement

satisfies the transition rule`m`=`c`.receive()`c`=`n`:`q`=>_{o}`m`=`n`,`c`=`q``n`and message queue`q`). From this and`S`_{j}^{6}and knowing`out`.getSize() = 2 it is clear that, for some k in {0, 1} and non-negative l,`in`_{j}(k).length = 1+l`in`_{j}(k).length = l,`msg`_{j}/= null`index`_{j}(both before and after the transition). From this and from the overall relationship between input and output channelsSum

it is clear that_{j}(`in`_{j}(0).length +`in`_{j}(1).length) =

Sum_{j}(`out`_{j}(0).lenght +`out`_{j}(1).length)`I`holds after the transition.By above reasoning, it is also clear that

`S`_{j}^{7}holds after the transition.From

`S`_{j}^{6}and by above relationship between input and output channels we know before the transition`out`_{j'}(p).length > 0 for some j' /=j and p in {0, 1} (by network construction). Thus`state`_{0}/=0,`state`_{j'}/=1 (for all j' /= j) and the transition cannot invalidate`S`_{j'}^{0}and`S`_{j'}^{1}.`S`_{j'}^{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.`S`_{j'}^{6}remains true because the truth of`in`_{j'}(`index`_{j'}).length > 1 cannot be changed by a`receive`

operation in`j`. - Assume
`state`_{j}= 7: the truth of`I`is clear from the fact that`msg`_{j}is non-null before the transition but null after the transition using the transition rule for`send`

shown above.Similar reasoning as in the previous case also shows that

`S`_{0}^{j'},`S`_{j'}^{1}and`S`_{j'}^{2}remain true.`S`_{j'}^{6}remains true because the truth of`in`_{j'}(`index`_{j'}).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.

Maintained by: Wolfgang Schreiner

Last Modification: November 14, 1997