| << Chapter < Page | Chapter >> Page > |
Now we want to verify this code. From the "Run" menu,select "Set Verification Parameters" and then turn on "Liveness" checking and "Non-Progress Cycles".
-a to have SPIN generate a verifier.
Then, when compiling
pan.c ,
we must include a flag to check for non-progress,
-DNP .
Finally, when running the resulting executable, we must alsospecify loop-checking via the flag
-l .
prompt>spin -a
filename .pml
prompt>gcc -DNP pan.c -o
filename prompt>
filename -l (With all the varying flag names,
you can begin to appreciate
xspin 's interface!)pan: non-progress cycle (at depth 6)
pan: wrote pan_in.trail
Now run the guided simulation. In the "Simulation Output" window, the start of the cycle is so labeled, and the end of the cycleis the last step displayed. Pictorially, the trace is as follows.
Whereas livelock is when computation continues but no process makes actual progress, starvation is whencomputation continues, and some processes make progress but others don't.
Consider the following code.
(Clearly, it does not compute anything interesting.)
1 show int x = 0;
23 active proctype A()
4 {5 do
6 :: true ->x = 1 - x;
7 od8 }
910 active proctype B()
11 {12 do
13 :: true ->x = 1 - x;
14 od15 } Our nave expectation and desire is
that
A and
B each get executed infinitely often
(though not necessarily exactly alternating).The problem is that we could get unluckyvery
A to get all the processor time,
while
B never even gets executed once, ever.
More generally, maybe
B gets its fair share of processor time for a while,
but later priority is always given to
A ,
and
B never runs again.
This is simply another instance of a lack of progress.
For example, if we consider only
B 's
loop to be progress, then there is a non-progress cycle.
Modify the code to test for this non-progress cycle, and then run SPIN's verifier.
Since we are currently considering only
B 's loop to be progress,
we only add a progress label in
B .
1 show int x = 0;
23 active proctype A()
4 {5 do
6 :: true ->x = 1 - x;
7 od8 }
910 active proctype B()
11 {12 progress_B:
13 do14 :: true ->x = 1 - x;
15 od16 }
Now we want to verify this code
First, run a syntax check. Partly, this is just anotherreminder of a good habit. But, it also forces
xspin to re-scan your code and recognize
the progress label. After doing this,re-run the verifier, and indeed it will find a non-progress
cycleThe following are two of the possible traces it could find,
one minimal, and one not.
A and
a nonminimal trace thatexecutes
B a little first.
Progress states are depicted with red borders.The next figure shows the entire state space, which has
a bit of a surprise. Some of the states are duplicated,differing
only in their status as progress states or not.
To see why that is necessary, contrast the following.
Entering line 14, as in the first
transition of the above nonminimal trace, entails progress.This corresponds to each of the red progress states.
However, say that
B execute for one step, long enough to pass the guard, but
not yet execute the assignment.Now, if only
A executes,
B never makes further progress.
This corresponds to the black non-progress states with
B 's line counter at 14.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|