model-checkingpromelaspin

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:


    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.