Go backward to Program Properties Go up to B.5 Verification Go forward to Time Complexity

Termination

For proving termination, it is necessary to introduce the following assumptions:

1. The network is fully connected.
2. Node 0 eventually generates a snap message.
3. The operation s.select() is fair, i.e., it eventually returns the index of every non-empty channel in s.

The first assumption is true by construction. The second assumption is only probabilistically true (because the random generator might never trigger the generation of the snap message). The third assumption is not true in DAJ. If the first channel of s not empty, other channels in s are not considered. In order to guarantee termination, one thus has to implement fairness using e.g. a counter f initialized as 0:

  InChannelSet s;
  s.addChannel(in(f));
  f++; if (f == in().getSize()) f = 0;
  index = s.select(random(5))

Let us assume that all requirements are actually met. Then node 0 eventually triggers a snap message which, by connectivity and fairness, eventually reaches every other node and is forwarded to every output channel and thus to every channel of the network. Thus in every node eventually missingSnaps drops to 0 and a result message is generated which, again by connectivity and fairness, eventually reaches every other node. Thus in every node missingResults eventually drops to 0 and mode TERMINATED is reached, which lets the node terminate.