Is this model of Peterson's algorithm incorrect?

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

Solution

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:

ltl p1 { [] (P[0]@req -> <> (P[0]@cs) }

where req is a label placed as follows:

    do
    :: true ->
req:   want[me] = true
       turn = you
       !want[you] || turn == me
cs:    want[me] = false
    od

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 to 0 is forever not selected for execution.

The spin model-checker gives you a counter-example that falls exactly in this situation:

~$ spin -t -g -l -p t.pml
ltl ltl_0: [] (<> ((P[0]@cs)))
starting claim 1
using statement merging
Never claim moves to line 3 [(!((P[0]._p==cs)))]
  2:    proc  1 (P:1) t.pml:10 (state 1)    [want[me] = 1]
        want[0] = 0
        want[1] = 1
  <<<<<START OF CYCLE>>>>>
Never claim moves to line 8 [(!((P[0]._p==cs)))]
  4:    proc  1 (P:1) t.pml:11 (state 2)    [turn = you]
  6:    proc  1 (P:1) t.pml:12 (state 3)    [((!(want[you])||(turn==me)))]
  8:    proc  1 (P:1) t.pml:13 (state 4)    [want[me] = 0]
        want[0] = 0
        want[1] = 0
 10:    proc  1 (P:1) t.pml:10 (state 1)    [want[me] = 1]
        want[0] = 0
        want[1] = 1
spin: trail ends after 10 steps
#processes: 2
        want[0] = 0
        want[1] = 1
        turn = 0
        cs = 0
 10:    proc  1 (P:1) t.pml:11 (state 2)
 10:    proc  0 (P:1) t.pml:9 (state 5)
 10:    proc  - (ltl_0:1) _spin_nvr.tmp:7 (state 10)
2 processes created

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:
```
ltl p2 { [] ((P[0]@req || P[1]@req) -> <> (P[0]@cs || P[1]@cs) }
```
This ensures that there is progress in the system as a whole, but it doesn't guarantee that either one among P[0] and P[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:
```
ltl p3 { ([]<> (_last == 0)) -> [] (P[0]@req -> <> (P[0]@cs)) }
```
where _last is a predefined internal variable, described in the docs as follows:

DESCRIPTION _last is a predefined, global, read-only variable of type pid that holds the instantiation number of the process that performed the last step in the current execution sequence. The initial value of _last is zero.

The _last variable can only be used inside never claims. It is an error to assign a value to this variable in any context.

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 which P[0] is not scheduled infinitely often for execution due to the unfairness of the scheduler, but also those situations in which P[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:

bool flag[2], turn

active [2] proctype P() {
    pid i = _pid;
    pid j = 1 - i;

    do
    :: true ->
req:    flag[i] = true
        turn = j;
        do
            :: (flag[j] && (turn == j)) -> skip
            :: else -> break;
        od;
cs:     skip;
        flag[i] = false;
    od
}

ltl p1 { (
            ([]<> (_last == 0)) &&
            ([]<> (_last == 1))
         ) ->
            ([] (P[0]@req -> <> (P[0]@cs)))
       }

And the property is indeed verified without throwing away any potentially interesting execution trace:

~$ spin -a t.pml
ltl p1: (! (([] (<> ((_last==0)))) && ([] (<> ((_last==1)))))) || ([] ((! ((P[0]@req))) || (<> ((P[0]@cs)))))
~$ gcc pan.c
~$ ./a.out -a 

(Spin Version 6.4.8 -- 2 March 2018)

Full statespace search for:
    never claim             + (p1)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 40 byte, depth reached 97, errors: 0
      269 states, stored (415 visited)
      670 states, matched
     1085 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.017   equivalent memory usage for states (stored*(State-vector + overhead))
    0.287   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


unreached in proctype P
    t.pml:18, state 16, "-end-"
    (1 of 16 states)
unreached in claim p1
    _spin_nvr.tmp:23, state 33, "-end-"
    (1 of 33 states)

pan: elapsed time 0 seconds

Note that we require both P[0] and P[1] to be allowed to execute infinitely often, because otherwise another spurious counter-example would be found.

Is this model of Peterson's algorithm incorrect?

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.