LTL model checking using Spin and Promela syntax

Question

I'm trying to reproduce ALGOL 60 code written by Dijkstra in the paper titled "Cooperating sequential processes", the code is the first attempt to solve the mutex problem, here is the syntax:

begin integer turn; turn:= 1;
      parbegin
      process 1: begin Ll: if turn = 2 then goto Ll;
                           critical section 1;
                           turn:= 2;
                           remainder of cycle 1; goto L1
                 end;
      process 2: begin L2: if turn = 1 then goto L2;
                           critical section 2;
                           turn:= 1;
                           remainder of cycle 2; goto L2
                  end
      parend
end 

So I tried to reproduce the above code in Promela and here is my code:

#define true    1
#define Aturn true
#define Bturn false

bool turn, status;

active proctype A()
{   
    L1: (turn == 1); 
    status = Aturn;
    goto L1;
    /* critical section */
    turn = 1;

}

active proctype B()
{   
    L2: (turn == 2); 
    status = Bturn;
    goto L2;
    /* critical section */
    turn = 2;
}

never{ /* ![]p */ 
    if
    :: (!status) -> skip
    fi;
}

init
{   turn = 1;
    run A(); run B();
}

What I'm trying to do is, verify that the fairness property will never hold because the label L1 is running infinitely.

The issue here is that my never claim block is not producing any error, the output I get simply says that my statement was never reached..

here is the actual output from iSpin

spin -a  dekker.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000 
Pid: 46025

(Spin Version 6.2.3 -- 24 October 2012)
    + Partial Order Reduction

Full statespace search for:
    never claim             - (not selected)
    assertion violations    +
    cycle checks        - (disabled by -DSAFETY)
    invalid end states  +

State-vector 44 byte, depth reached 8, errors: 0
       11 states, stored
        9 states, matched
       20 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001   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


unreached in proctype A
    dekker.pml:13, state 4, "turn = 1"
    dekker.pml:15, state 5, "-end-"
    (2 of 5 states)
unreached in proctype B
    dekker.pml:20, state 2, "status = 0"
    dekker.pml:23, state 4, "turn = 2"
    dekker.pml:24, state 5, "-end-"
    (3 of 5 states)
unreached in claim never_0
    dekker.pml:30, state 5, "-end-"
    (1 of 5 states)
unreached in init
    (0 of 4 states)

pan: elapsed time 0 seconds
No errors found -- did you verify all claims?

I've read all the documentation of spin on the never{..} block but couldn't find my answer (here is the link), also I've tried using ltl{..} blocks as well (link) but that just gave me syntax error, even though its explicitly mentioned in the documentation that it can be outside the init and proctypes, can someone help me correct this code please?

Thank you

Answer 1

You've redefined 'true' which can't possibly be good. I axed that redefinition and the never claim fails. But, the failure is immaterial to your goal - that initial state of 'status' is 'false' and thus the never claim exits, which is a failure.

Also, it is slightly bad form to assign 1 or 0 to a bool; assign true or false instead - or use bit. Why not follow the Dijkstra code more closely - use an 'int' or 'byte'. It is not as if performance will be an issue in this problem.

You don't need 'active' if you are going to call 'run' - just one or the other.

My translation of 'process 1' would be:

proctype A ()
{
L1: turn !=2 ->
  /* critical section */
  status = Aturn;
  turn = 2
  /* remainder of cycle 1 */
  goto L1;
}

but I could be wrong on that.