| << Chapter < Page | Chapter >> Page > |
Weak fairness is defined not in terms of processes,
but of individual statements. This example illustrateshow it applies to situations other than avoiding starvation,
and in particular, when there is only one process.
show int x = 0;
active proctype loop(){
do:: true ->x = 1;
:: x==1 ->x = 2;
:: x==2 ->x = 3;
od;}
Without any kind of fairness enforced, it is possible to repeatedly execute only the first option.
Verify the previous statement. Where would you add progress labels?
We want a progress label within the second option.
Although that is not allowed before the guard, it is sufficientfor this example to add it after the guard.
active proctype loop()
{do
:: true ->x = 1;
:: x==1 ->progress_2: x = 2;
:: x==2 ->progress_3: x = 3;
od;}
The
progress_3 label is unnecessary
since it would only be encountered after the second optionis executed. However, it is arguably a good idea not to reason
through such arguments, and instead let the tool formallydo the reasoning.
After the first execution of the first option, the second one
is continously enabled, since
x==1 .
With weak fairness enforced, we are thus guaranteed that
x eventually becomes 2.
Now verify again with weak fairness enforced.
After
x becomes 2,
both the first and third options are enabled.Weak fairness is not sufficient to guarantee that the third will be
ever be picked, as
x could
alternate between the values 1 and 2forever. Since it wouldn't have the value 2 continuously, the weak
fairness guarantee doesn't apply to the third option.
Verify this claim. Where are progress labels needed now?
Only the previous
progress_3 label should be used.
Does the following code have a non-progress loop?
1 int x = 0;
23 active proctype A()
4 {5 progressA:
6 /* Consider: A reaches this line, but never executes it. */7 x = 1;
8 }9
10 active proctype B()11 {
12 do13 :: x == 0 ->skip;
14 :: x == 1 ->15 progressB: skip;16 od;
17 }
It does if
A never runs, and
B runs forever
with
x being zero.
(Of course, this only happens if fairness is not being enforced.)But surprisingly,
SPIN does not report any non-progress cycles! It views
A as forever sitting in the
state
progressA , and thus feels that progress is
always happening (even though that statement is never executed).
This mismatch isn't due to the fact that
SPIN associates labels with the state just
before executing the labeled statement;
even if they were associated with the statement precedingthe label,
we could still construct a situationwhere SPIN views
A as making progress even
though it is doing nothing at all (just idlingin a state tagged as a progress).
The fundamental mismatch is that to you and me, the idea ofmaking progresscorresponds to making certain transitions . But SPIN views labels only as relating to states. If there are transitions which don't correspond to progress,yet arrive at a labeled-progress-state (in particular: self-loops, possibly introduced for stutter-extension ), then the state-based and transition-based approaches differ.
We'll see in the next section a way to still capture our transition-based notion with SPIN . Nevertheless, beware that sometimes a particular tool mighthave some surprising notions.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|