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

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

`act`

`chan`

`term`

...

- ...
**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`

inB: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`

).

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``'`

`t`is not increased by any system action,- there is some "helpful" system action that decreases
`t`, - 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.

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`

inZ_{3}

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`

`'`

=

ifi!= 0\/ ~terminated_{n}(`act`

,`chan`

)thentrun

elseifexistsjinZ_{n}:j> 0/\`mark`

_{j}then1else0

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

`act`

`chan`

`term`

`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**_{3}:

`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`

inZ_{3}).

**Proof:** `Init` implies `trun`

`=` 2. Only
`Forward` sets `trun`

by assigining 1 or 0. []

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

wherenum_{n}(`sig`

,`trun`

) := (`trun`

,tpos_{n}(`sig`

))

tpos_{n}(`sig`

) :=

suchiinZ_{n+1}:

\/

foralljinZ_{n}: ~`sig`

_{j}/\i=nexistsjinZ_{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`

)inZ_{3}xZ_{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**_{3} `x` **Z**_{n+1},
**<** ) with

(has not infinitely decreasing sequences of elements.t_{0},p_{0})<(t_{1},p_{1}) :<=>

\/

t_{0}<t_{1}/\

t_{0}=t_{1}p_{0}<p_{1}

**Proof:** Obvious. []

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`_{0}(`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 => (forallkinZ_{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`_{0}(`act`

_{0},
`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**_{n}with
`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 => (forallkinZ_{n}:`sig`

_{k}=> (foralljinZ_{n}:j>k=> ~`mark`

_{j}))).

**Proof:** `Init` implies `trun`

`=` 2.
Assume
`trun`

`=` 1 => ... and
`trun`

`'`

`=` 1.
If `trun`

!= 1, we have
`Forward`_{0}(`act`

_{0},
`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**_{n}with
`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 =>

/\

forallkinZ_{n}: ~`mark`

_{k}`run`

=> ~`tmark`

).

**Proof:** `Init` implies `trun`

`=` 2.
Assume `trun`

`=` 0 => ... and
`trun`

`'`

`=` 0.
If `trun`

!= 0, we have
`Forward`_{0}(`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` **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}. []

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

`num`_{n}(`sig`

,`term`

) is not increased (with respect to**<**) by any action,`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`

),

- this action is enabled.

`term`

.
- The only actions that affect
`sig`

and`trun`

are`Start`and`Forward`. **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`

_{0}`tval`

+`cnt`

_{0}!= 0

`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`**Z**_{n}:`j`> 0 => ~`mark`

_{j}. Therefore we have`trun`

`'`

`=`0. **Case**`trun`

`=`2- By
`terminated`_{_n}(`act`

,`chan`

), we have`trun`

`'`

< 2.

- 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`_{0}(`run`

,`sig`

,`mark`

,`tval`

,`tmark`

,`t`

) is enabled. []

Maintainer: Wolfgang Schreiner

Last Modification: August 20, 1998