Promela (ispin) stucks at the end of loop

Question

well, i have this (it is part of code):

20  proctype Main(byte myID) {
21    do
22    ::int J=0;
23      int K=0;
24    
25      atomic{
26        requestCS[myID]=true;
27        myNum[myID]=highestNum[myID]+1;
28    }
29  
30      do
31      :: J <= NPROCS-1 ->
32        if
33          :: J != myID -> ch[J] ! request, myID, myNum[myID];
34        fi;
35        J++;
36      :: else break;
37      od;//////////////////////////////////
38  
39    
40    do
41    :: K <= NPROCS-2 ->
42      ch[myID] ?? reply, _, _;
43      K++;
44    :: else break;
45    od;
46    
47    
48    cs: critical++;
49    assert (critical==1);
50    critical--;
51    requestCS[myID]=false;
52  
53    byte N;
54       do
55       :: empty(deferred[myID]) -> break;
56          deferred [myID] ? N -> ch[N] ! reply, 0, 0;
57       od;
58    od;
59  }

on ///////////// it stucks (writing timeout), and there is no way forward, to step 40, for example.

it is the part of Ricart-Agrawala algoritm, here it is et al:

1   #define  NPROCS 2
2   int critical = 0;
3   byte myNum[NPROCS];
4   byte highestNum[NPROCS];
5   bool requestCS[NPROCS];
6   chan deferred[NPROCS] = [NPROCS] of {byte};
7   mtype={request, reply};
8   chan ch[NPROCS]=[NPROCS] of {mtype, byte, byte};
9   
10  init {  
11    atomic {
12      int i;
13      for (i : 0 .. NPROCS-1){
14        run Main(i);
15        run Receive(i);
16      }
17    }
18  }
19  
20  proctype Main(byte myID) {
21    do
22    ::int J=0;
23      int K=0;
24    
25      atomic{
26        requestCS[myID]=true;
27        myNum[myID]=highestNum[myID]+1;
28    }
29  
30      do
31      :: J <= NPROCS-1 ->
32        if
33          :: J != myID -> ch[J] ! request, myID, myNum[myID];
34        fi;
35        J++;
36      :: else break;
37      od;
38  
39    
40    do
41    :: K <= NPROCS-2 ->
42      ch[myID] ?? reply, _, _;
43      K++;
44    :: else break;
45    od;
46    
47    
48    cs: critical++;
49    assert (critical==1);
50    critical--;
51    requestCS[myID]=false;
52  
53    byte N;
54       do
55       :: empty(deferred[myID]) -> break;
56          deferred [myID] ? N -> ch[N] ! reply, 0, 0;
57       od;
58    od;
59  }
60  
61  proctype Receive(byte myID){
62    byte reqNum, source;
63    do
64     :: ch[myID] ?? request, source, reqNum;
65  
66       highestNum[myID] = ((reqNum > highestNum[myID]) -> reqNum : highestNum[myID]);
67  
68       atomic {
69        if
70        :: requestCS[myID] && ((myNum[myID] < reqNum) || ((myNum[myID] == reqNum) && (myID < source))) -> deferred[myID] ! source
71        :: else -> ch[source] ! reply, 0, 0;
72        fi;
73    }
74    od;
75  }

what i doing wrong? Thank You in advance

P.S. critical - is a critical section "simulator", 'cause this algoritm is for distributed systems...

Answer 1

The verification can be stuck at line 37/40 for a couple of reasons. Your code just prior to then is:

32        if
33          :: J != myID -> ch[J] ! request, myID, myNum[myID];
34        fi;

This if statement will block forever if: J == myID or if ch[J] is full and never empties. You can 'fix' this problem by adding an else to the if and being careful to handle the 'queue is full' case. Of course, the 'fix' might not be consistent with what you are trying to model.