| << Chapter < Page | Chapter >> Page > |
How can we test for the possibility of
A looping forever
without executing
B ?
Remove the progress label from
B ,
and add one to thecorresponding place within
A .
Of course, the faulty behavior we'd really like
to have SPIN alert us to is
A
or
B is being starved,
instead of having to choose one and name it.
Why does putting
progress labels in both
A
and
B
not achieve what we want?
Putting in two progress labels, and getting a
green light from SPIN's verifier, would only meanIt is verified that in every trace,
either
A or
B is making progress.But we want to confirm
A
and
B are making progress.
In this toy example,
where
A and
B are
identical (up to differing in progress labels),we can argue by symmetry that
lack of non-progress-for-
A is enough to implylack of non-progress-for-
B .
But in general, SPIN makes us run two separateverifications (though we will see some possible
code
contortions later).
Process scheduling software is usually written so as to avoid starvation. For example, a simple scheduler could simply pickprocesses in a round-robin fashion, executing some of each process 0, 1, 2,, 0, 1, 2,forever. However, this scheme inappropriately schedules time for blockedthreads, doesn't allow the processes to be prioritized, and doesn't allow the set of running processes to change dynamically.Real schedulers manage not only the order, but also the frequencyof context switches.
So far, we have considered verification with an arbitrary scheduler. Since we know nothing about the scheduler, we mustconsider all possible traces. ( Remember that the scheduler might sometimes be nature,or even an adversary.) But, SPIN also allows you to specifysome more restricted scheduling behaviors, thus reducing the state space.We will look at one of these mechanisms in SPINenforcingweak fairness.
Let us return to our
starvation example ,
but this time we will have SPIN enforce weak fairness.To turn this feature on in
xspin ,
select it from the verification options.
-f for
fairness, as well as
-l for loop-checking.
prompt>spin -a
filename .pml
prompt>gcc -DNP pan.c -o
filename prompt>
filename -f -l 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 }
In this code, each process is always enabled, since each guard is
just
true . Thus, a weakly fair
scheduler guarantees that at each point in the trace,each process will eventually be scheduled
in the future.
Now verify there are no non-progress cycles when weak
fairness is guaranteed.
B again and verify that no errors are reported.
Repeat with the progress label in
A .
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|