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

Strong fairness states that if a statement is enabled infinitely often, it will eventually be executed.That would be sufficient to guarantee the third option is eventually chosen. SPIN does not have a built-in switchfor enforcing strong fairness.

Some unexpected progress (optional)

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.

Get Jobilize Job Search Mobile App in your pocket Now!

Get it on Google Play Download on the App Store Now




Source:  OpenStax, Model checking concurrent programs. OpenStax CNX. Oct 27, 2005 Download for free at http://cnx.org/content/col10294/1.3
Google Play and the Google Play logo are trademarks of Google Inc.

Notification Switch

Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?

Ask