Go backward to 4 Correctness of the Algorithm Go up to Top Go 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

• ...
• forall i in Z_n: WF(Start_i(run, sig, mark, tval, tmark))
• forall i in Z_n: WF(Forward_i(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: SystemTF_n(act, chan, term)) <=> System_n(act,chan).

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

By construction, for all n, act, chan and term, also SystemTF_n(act, chan, term) => System_n(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:

SystemTF_{n 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 Z₃

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.

Forward_i(...) :<=>

/\

• ...
• trun' =
  if i != 0\/ ~terminated_n(act, chan) then trun
  else if exists j in Z_n: 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

• Init(in act, in chan, in term, in run, in cnt, in sig, in mark, in trun) :<=>
  
  /\
  • ...
  • trun = 2,
• ...
• Forward_i(in a, in c, io sig, io mark, io tval, io tmark, io term, io trun) :<=>
  
  /\
  • ...
  • trun' = if i != 0\/ ~terminated_n(act, chan) then trun
    else if exists j in Z_n: j > 0/\ mark_j then 1 else 0
• Action_{n, i}(io act, io chan, io term, io run, io cnt, io sig, io mark, io tval, io tmark, io trun) :<=>
  
  \/
  • ...
  • Forward_i(act_i, cnt_i, sig, mark, tval, tmark, term, trun):

• ...
• trun in Z₃:

• Init(act, chan, term, run, cnt, sig, mark, trun)
• [][exists i in Z_n: Action_{n, 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:

SystemTFV_n(act, chan, term)) <=> SystemTF_n(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 Z₃).

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

num_n(sig, trun) := (trun, tpos_n(sig))

tpos_n(sig) :=
such i in Z_n+1:

\/

• forall j in Z_n: ~sig_j/\ i = n
• exists j in Z_n: 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:

[](num_n(sig, trun) in Z₃ x Z_n+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 (Z₃ x Z_n+1, < ) with

(t₀, p₀) < (t₁, p₁) :<=>

\/

• t₀ < t₁
• 
  /\
  • t₀ = t₁
  • p₀ < p₁

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 Forward₀(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 Z_n: sig_k => tval = sum_{j in Z_n, j > k}cnt_j)).

Proof: Init implies trun = 2. Assume trun < 2 => ... and trun' < 2. If trun = 2, we have Forward₀(act₀, cnt_i, sig, mark, tval, tmark, term, trun) and thus ~sig'_k for all k in Z_n. Assume trun < 2 and take k in Z_nwith 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. Forward_i(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 Z_n. []

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

[](trun = 1 => (forall k in Z_n: sig_k => (forall j in Z_n: j > k => ~mark_j))).

Proof: Init implies trun = 2. Assume trun = 1 => ... and trun' = 1. If trun != 1, we have Forward₀(act₀, cnt_i, sig, mark, tval, tmark, term, trun) and thus ~sig'_k for all k in Z_n. Assume trun = 1 and take k in Z_nwith 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. Forward_i(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 Z_n. []

 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 Z_n: ~mark_k
• run => ~tmark).

Proof: Init implies trun = 2. Assume trun = 0 => ... and trun' = 0. If trun != 0, we have Forward₀(act₀, 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 Z_n. Assume trun = 0 and take k in Z_n. 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 Forward_i(act_i, cnt_i, sig, mark, tval, tmark, term, trun) imply with the hypothesis ~tmark' and ~mark'_k for every k in Z_n. []

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. num_n(sig, term) is not increased (with respect to < ) by any action,
2. num_n(sig, term) is decreased by the helpful action

   
   \/

   • Start_i(run, sig, mark, tval, tmark)
   • Forward_i(act_i, cnt_i, sig, mark, tval, tmark, term, trun),

3. this action is enabled.

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 num_n(sig, trun) = (trun, n). The action implies num_n(sig', trun') = (trun, n-1).

   Case Forward_i(act_i, cnt_i, sig, mark, tval, tmark, term, trun)

   We have sig_i; Proposition 7 implies num_n(sig, trun) = (trun, i). If i != 0, we have trun' = trun and sig'_i-1; Proposition 7 then yields num_n(sig', term') = (trun, i-1). If i = 0, ~term' implies

   
   \/

   • tmark\/ mark₀
   • tval+cnt₀ != 0

   By terminated_{_n}(act, chan), Proposition 5, and Proposition 16, we then have tval+cnt₀ = 0. Above disjunction and Proposition 18 thus give trun != 0.

   Case trun = 1

   By Proposition 17, forall j in Z_n: 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 Forward_i(act_i, cnt_i, sig, mark, tval, tmark, term, trun) is enabled for some i in Z_n. If ~run, then Start₀(run, sig, mark, tval, tmark, t) is enabled. []