Go backward to 4 Correctness of the AlgorithmGo up to TopGo forward to References

# 5 Progress of the Algorithm

#### Fairness

In the previous section, we have shown a so called safety property of the termination detection algorithm: if the variable `term` is set, then the system has terminated. We have not yet shown the crucial progress property of the algorithm: if the system has terminated, then the algorithm eventually sets `term`. In fact, this property is not true for the current specification, because there is a system behavior where the algorithm never sets `term`: the behavior where none of the system variables changes any more (i.e., only stuttering steps are performed after termination).

Of course, we consider this behavior very "unfair" because in a termination state, also either Start or Forward is continously enabled. We therefore have to augment our algorithm by a condition that prevents such an unfair behavior. We therefore introduce

Definition 2 (Weak Fairness) An action is weakly fair if it is not possible that the action is continuously enabled but never executed:

WF(A) :<=> (<>[]Enabled < A > ) => []<> < A > .

This notion of fairness is called "weak" because it allows an action to be continuedly enabled and disabled without ever being executed. In those cases where the enabling condition of an action continues to be true (as for those of Signal or Forward), this notion of fairness is however sufficient. The fairness requirements of the termination detection algorithm are then added to our specification as shown in Specification 3.

Specification 3: Termination Detection with Fairness

SystemTFn in N(`act` in Zn->B, `chan` in Zn x Zn->Seq(MSG), `term` in B) :<=>
(A system that eventually detects its termination)
...
/\
• ...
• forall i in Zn: WF(Starti(`run`, `sig`, `mark`, `tval`, `tmark`))
• forall i in Zn: WF(Forwardi(`act`i, `cnt`i, `sig`, `mark`, `tval`, `tmark`, `term`))

The new specification is equivalent to the original system:

Proposition 9 (Equivalence) SystemTF implements System and vice versa, i.e., for all n, `act`, and `chan`:

(var `term` in B: SystemTFn(`act`, `chan`, `term`)) <=> Systemn(`act`,`chan`).

Proof: Analogous to the Proof of Proposition 1. []

By construction, for all n, `act`, `chan` and `term`, also SystemTFn(`act`, `chan`, `term`) => Systemn(`act`, `chan` `term`) holds, but because of the additional fairness constraints the converse is not true.

The crucial progress property of the new specification is then stated by

Proposition 10 (Progress) If the system is terminated, it will eventually detect so, i.e., for all n, `act`, `chan`, `term`:

SystemTFn in N(`act`, `chan`, `term`) =>
[](terminated_n(`act`, `chan`) => <>`term`).

#### Proving Progress

In order to show a formula of the form <>A, it suffices to show that there exists an "induction term" t depending on the system variables (a state function) such that under the assumption ~A/\ ~A`'`

1. t is not increased by any system action,
2. there is some "helpful" system action that decreases t,
3. the helpful action is enabled.

Provided that the denoted ordering does not allow infinitely decreasing sequences of values (i.e., that it is well-founded), above conditions ensure that A is eventually executed.

#### Virtual Variables

As already discussed in Section 3, if the system terminates during a termination detection round, it may be necessary to first complete this round and perform two more rounds until termination can be concluded. The induction term therefore depends on the information in which round the termination detection algorithm is. Unfortunately, this information is not yet captured in any of the existing program variables. We therefore introduce a "virtual" variable

`trun` in Z3

which is initialized to 2

Init(...) :<=>

/\
• ...
• `trun` = 2,

and decreased by Process 0 at the end of a termination detection round, if the system has terminated: the variable is set to 1, if some other process in the system is still marked and to 0, otherwise. Thus `trun` describes an upper bound for the number of detection rounds to be performed until termination can be definitely concluded.

Forwardi(...) :<=>

/\
• ...
• `trun``'` =
if i != 0\/ ~terminatedn(`act`, `chan`) then trun
else if exists j in Zn: j > 0/\ `mark`j then 1 else 0

Of course, this behavior cannot be implemented (otherwise it would already solve the termination detection problem!); however, the only purpose of this variable is to give us some means for expressing the induction term to be constructed for proving progress of the algorithm. See Specification 4 for a complete description of the extension.

Specification 4: Introduction of A Virtual Variable

SystemTFVn in N(`act` in Zn->B, `chan` in Zn x Zn->Seq(MSG), `term` in B) :<=>
(A system that eventually detects its termination)
let
• Init(in `act`, in `chan`, in `term`, in `run`, in `cnt`, in `sig`, in `mark`, in `trun`) :<=>

/\
• ...
• `trun` = 2,
• ...
• Forwardi(in `a`, in `c`, io `sig`, io `mark`, io `tval`, io `tmark`, io `term`, io `trun`) :<=>

/\
• ...
• `trun``'` = if i != 0\/ ~terminatedn(`act`, `chan`) then trun
else if exists j in Zn: j > 0/\ `mark`j then 1 else 0
• Actionn, i(io `act`, io `chan`, io `term`, io `run`, io `cnt`, io `sig`, io `mark`, io `tval`, io `tmark`, io `trun`) :<=>

\/
• ...
• Forwardi(`act`i, `cnt`i, `sig`, `mark`, `tval`, `tmark`, `term`, `trun`):
var
• ...
• `trun` in Z3:

/\
• Init(`act`, `chan`, `term`, `run`, `cnt`, `sig`, `mark`, `trun`)
• [][exists i in Zn: Actionn, i(`act`, `chan`, `term`, `run`, `cnt`, `sig`, `mark`, `tval`, `tmark`, `trun`)]
• ...

We have to check that the new variable is indeed virtual, i.e., does not at all influence the original program behavior:

Proposition 11 (Equivalence) SystemTFV implements SystemTF and vice versa, i.e., for all n, `act`, `chan`, and `term`:

SystemTFVn(`act`, `chan`, `term`)) <=> SystemTFn(`act`, `chan`, `term`).

Proof: `trun` is not used except for computing `trun``'`. []

As in the previous section, we assume fixed n, `act`, `chan`, `term` and all internal variables such that all conditions in the specification hold. The following propositions are therefore only true for behaviors of SystemTFV ("the system").

As usual, we immediately assert some type condition for the new variable `trun`.

Proposition 12 (Type Correctness) The system preserves the type of `trun`.

[](`trun` in Z3).

Proof: Init implies `trun` = 2. Only Forward sets `trun` by assigining 1 or 0. []

#### Induction Term

Based on `trun`, we now define the induction term that we expect to decrease with every action of the terminated system.

Definition 3 (Induction Term) We define the induction term

numn(`sig`, `trun`) := (`trun`, tposn(`sig`))
where
tposn(`sig`) :=
such i in Zn+1:

\/
• forall j in Zn: ~`sig`j/\ i = n
• exists j in Zn: `sig`j/\ i = j.

The first component of num denotes the number of detection rounds to be performed, the second component the number of processes that the token still has to pass in the current round.

The domain of the induction term is stated by

Proposition 13 (Type Correctness) num is well typed:

[](numn(`sig`, `trun`) in Z3 x Zn+1).

Proof: By definition and Proposition 12. []

We then have to assert that num is indeed a suitable induction term.

Proposition 14 (Well Foundedness) The domain (Z3 x Zn+1, < ) with

(t0, p0) < (t1, p1) :<=>

\/
• t0 < t1

• /\
• t0 = t1
• p0 < p1
has not infinitely decreasing sequences of elements.

Proof: Obvious. []

#### System Invariants

The following invariants characterize `trun`.

Proposition 15 (Invariant) If `trun` has been decreased, the system has terminated:

[](`trun` < 2 => terminated_n(`act`, `chan`)).

Proof: Init implies `trun` = 2. Assume `trun` < 2 => terminated_n(`act`, `chan`) and `trun``'` < 2. If `trun` < 2, we have terminated_n(`act`, `chan`) and Proposition 2 implies terminated_n(`act``'`, `chan``'`). If `trun` = 2, we have Forward0(`act`i, `cnt`i, `sig`, `mark`, `tval`, `tmark`, `term`, `trun`) and, by the action, terminated_n(`act`, `chan`). Proposition 2 then implies terminated_n(`act``'`, `chan``'`). []

Proposition 16 (Invariant) If `trun` has been decreased, the token value reflects the actual message count:

[](`trun` < 2 => (forall k in Zn: `sig`k => `tval` = sumj in Z_n, j > k`cnt`j)).

Proof: Init implies `trun` = 2. Assume `trun` < 2 => ... and `trun``'` < 2. If `trun` = 2, we have Forward0(`act`0, `cnt`i, `sig`, `mark`, `tval`, `tmark`, `term`, `trun`) and thus ~`sig``'`k for all k in Zn. Assume `trun` < 2 and take k in Znwith `sig``'`k. By Proposition 15, we have terminated_n(`act`, `chan`), thus Send and Receive are not enabled and Inactivate has no effect. Start`i`(`run`, `sig`, `mark`, `tval`, `tmark`) implies `tval``'` = 0; Proposition 7 gives k = n-1. Forwardi(`act`i, `cnt`i, `sig`, `mark`, `tval`, `tmark`, `term`, `trun`) implies `tval``'` = `tval`+`cnt`i. If i > 0, Proposition 7 yields k = i-1; otherwise, we have ~`sig``'`k for every k in Zn. []

Proposition 17 (Invariant) If `trun` has been decreased once, all processes that previously held the token are unmarked:

[](`trun` = 1 => (forall k in Zn: `sig`k => (forall j in Zn: j > k => ~`mark`j))).

Proof: Init implies `trun` = 2. Assume `trun` = 1 => ... and `trun``'` = 1. If `trun` != 1, we have Forward0(`act`0, `cnt`i, `sig`, `mark`, `tval`, `tmark`, `term`, `trun`) and thus ~`sig``'`k for all k in Zn. Assume `trun` = 1 and take k in Znwith `sig``'`k. By Proposition 15, we have terminated_n(`act`, `chan`), thus Send and Receive are not enabled and Inactivate has no effect. Start`i`(`run`, `sig`, `mark`, `tval`, `tmark`) and Proposition 7 imply k = n-1. Forwardi(`act`i, `cnt`i, `sig`, `mark`, `tval`, `tmark`, `term`, `trun`) implies ~`mark``'`i. If i > 0, Proposition 7 yields k = i-1, otherwise we have ~`sig``'`k for every k in Zn. []

Proposition 18 (Invariant) If `trun` has been decreased twice, all processes are unmarked and the token is unmarked in a detection run:

[](`trun` = 0 =>

/\
• forall k in Zn: ~`mark`k
• `run` => ~`tmark`).

Proof: Init implies `trun` = 2. Assume `trun` = 0 => ... and `trun``'` = 0. If `trun` != 0, we have Forward0(`act`0, `cnt`i, `sig`, `mark`, `tval`, `tmark`, `term`, `trun`), which implies ~`run``'` and (by the definition of `trun``'` and of `mark``'`) ~`mark``'`k for every k in Zn. Assume `trun` = 0 and take k in Zn. By Proposition 15, we have terminated_n(`act`, `chan`), thus Send and Receive are not enabled and Inactivate has no effect. As well Start`i`(`run`, `sig`, `mark`, `tval`, `tmark`) as Forwardi(`act`i, `cnt`i, `sig`, `mark`, `tval`, `tmark`, `term`, `trun`) imply with the hypothesis ~`tmark``'` and ~`mark``'`k for every k in Zn. []

#### Conclusion

Finally we combine all our knowledge to the

Proof of Proposition 10 (Progress): Assume terminated_n(`act`, `chan`) and ~`term` and ~`term``'`. We show that

1. numn(`sig`, `term`) is not increased (with respect to < ) by any action,
2. numn(`sig`, `term`) is decreased by the helpful action

\/
• Start`i`(`run`, `sig`, `mark`, `tval`, `tmark`)
• Forwardi(`act`i, `cnt`i, `sig`, `mark`, `tval`, `tmark`, `term`, `trun`),
3. this action is enabled.
From the weak fairness condition of the decreasing action and Propositions 13 and 14 we can then conclude <>`term`.
1. The only actions that affect `sig` and `trun` are Start and Forward.
2. Case Start`i`(`run`, `sig`, `mark`, `tval`, `tmark`)
The action implies ~`run`;Proposition 6 gives us numn(`sig`, `trun`) = (`trun`, n). The action implies numn(`sig``'`, `trun``'`) = (`trun`, n-1).
Case Forwardi(`act`i, `cnt`i, `sig`, `mark`, `tval`, `tmark`, `term`, `trun`)
We have `sig`i; Proposition 7 implies numn(`sig`, `trun`) = (`trun`, i). If i != 0, we have `trun``'` = `trun` and `sig``'`i-1; Proposition 7 then yields numn(`sig``'`, `term``'`) = (`trun`, i-1). If i = 0, ~`term``'` implies

\/
• `tmark`\/ `mark`0
• `tval`+`cnt`0 != 0
By terminated_n(`act`, `chan`), Proposition 5, and Proposition 16, we then have `tval`+`cnt`0 = 0. Above disjunction and Proposition 18 thus give `trun` != 0.
Case `trun` = 1
By Proposition 17, forall j in Zn: j > 0 => ~`mark`j. Therefore we have `trun``'` = 0.
Case `trun` = 2
By terminated_n(`act`, `chan`), we have `trun``'` < 2.
3. If `run`, then terminated_n(`act`, `chan`) and Proposition 6 ensure that Forwardi(`act`i, `cnt`i, `sig`, `mark`, `tval`, `tmark`, `term`, `trun`) is enabled for some i in Zn. If ~`run`, then Start0(`run`, `sig`, `mark`, `tval`, `tmark`, `t`) is enabled. []

Maintainer: Wolfgang Schreiner
Last Modification: August 20, 1998