Go backward to 4 Correctness of the Algorithm Go up to Top Go 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
in Zn->B,
chan
in Zn x Zn->Seq(MSG),
term
in B) :<=>
run
, sig
, mark
,
tval
, tmark
))
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
:
(varterm
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
).
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'
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
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
act
in Zn->B,
chan
in Zn x Zn->Seq(MSG),
term
in B) :<=>
act
, in chan
, in term
, in run
,
in cnt
, in sig
, in mark
, in trun
) :<=>
trun
= 2,
a
, in c
, io sig
,
io mark
, io tval
, io tmark
, io term
, io trun
) :<=>
trun
'
= if i != 0\/ ~terminatedn(act
,
chan
) then trun
mark
j then 1 else 0
act
, io chan
,
io term
, io run
,
io cnt
, io sig
, io mark
, io tval
,
io tmark
, io trun
) :<=>
act
i,
cnt
i, sig
,
mark
, tval
, tmark
, term
,
trun
):
trun
in Z3:
act
, chan
, term
, run
,
cnt
, sig
, mark
, trun
)
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. []
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(wheresig
,trun
) := (trun
, tposn(sig
))
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) :<=>has not infinitely decreasing sequences of elements.
\/
- t0 < t1
/\
- t0 = t1
- p0 < p1
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
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 > kcnt
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.
Starti
(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.
Starti
(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
krun
=> ~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 Starti
(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. []
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
sig
, term
) is not increased
(with respect to < ) by any action,
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
),
term
.
sig
and trun
are
Start and Forward.
i
(run
, sig
,
mark
, tval
, tmark
)run
;Proposition 6 gives
us numn(sig
, trun
) = (trun
, n).
The action implies numn(sig
'
,
trun
'
) = (trun
, n-1).
act
i,
cnt
i, sig
, mark
, tval
, tmark
,
term
, trun
)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
By terminated_n(
\/
tmark
\/mark
0tval
+cnt
0 != 0
act
, chan
),
Proposition 5, and Proposition 16, we then have
tval
+cnt
0 = 0.
Above disjunction and Proposition 18 thus give
trun
!= 0.
trun
= 1mark
j.
Therefore we have trun
'
= 0.
trun
= 2act
, chan
), we have
trun
'
< 2.
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. []