I have written the following model of Peterson's algorithm:
bool want[2], turn
ltl { []<>P[0]@cs }
active [2] proctype P() {
pid me = _pid
pid you = 1 - me
do
:: want[me] = true
turn = you
!want[you] || turn == me
cs: want[me] = false
od
}
It is my understanding that this algorithm provides freedom from starvation, as expressed in the linear temporal logic claim. Then why do I get an error when I analyze the model?
ltl ltl_0: [] (<> ((P[0]@cs)))
pan:1: acceptance cycle (at depth 2)
pan: wrote peterson.pml.trail
(Spin Version 6.4.8 -- 2 March 2018)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (ltl_0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 36 byte, depth reached 9, errors: 1
5 states, stored
0 states, matched
5 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.291 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
pan: elapsed time 0 seconds
You are right, the Peterson algorithm should be free of starvation and, indeed, it is.
Starvation occurs when a process requested some resources but it is perpetually denied them. Thus, a better encoding of the progress formula would be:
where
req
is a label placed as follows:Unfortunately, the previous formula is still found to be
false
.The reason for this is that the process scheduler of the system you are model checking is not, generally speaking, fair. In fact, it admits executions in which the process with
_pid
equal to0
is forever not selected for execution.The
spin
model-checker gives you a counter-example that falls exactly in this situation:Workarounds.
There are basically two workarounds for this problem:
the first is to merely ask that, if some process tries to enter the critical section, then some process eventually enters it:
This ensures that there is progress in the system as a whole, but it doesn't guarantee that either one among
P[0]
andP[1]
specifically doesn't incur in starvation.the second is to introduce a fairness condition which requests to focus the model-checking only on those executions in which a process is scheduled for execution infinitely often:
where
_last
is a predefined internal variable, described in the docs as follows:Unfortunately, this approach is not that great when checking for absence of starvation on your model. This is because requiring
[] <> _last == 0
would not only remove any execution in whichP[0]
is not scheduled infinitely often for execution due to the unfairness of the scheduler, but also those situations in whichP[0]
is not scheduled due to an actual problem of starvation.An appropriate solution.
I would suggest to change your model so that
P[0]
performs busy waiting instead of blocking while waiting for its own turn. This makes the use of_last
less problematic when trying to prove absence of starvation. The final model would be:And the property is indeed verified without throwing away any potentially interesting execution trace:
Note that we require both
P[0]
andP[1]
to be allowed to execute infinitely often, because otherwise another spurious counter-example would be found.So to answer your question more directly, your model is not functionally incorrect but to appropriately verify absence of starvation it is necessary to perform some minor changes.