I've created a bakery lock using Spin
1 int n=3;
2 int choosing[4] ; // initially 0
3 int number[4]; // initially 0
4
5 active [3] proctype p()
6 {
7
8 choosing[_pid] = 1;
9 int max = 0;
10 int i=0;
11
12 do
13 ::(number[i] > max) -> max=number[i];
14 ::i++;
15 :: (i == n) -> break;
16 od;
17
18 number[_pid] = max + 1;
19 choosing[_pid] = 0;
20
21 int j=0;
22
23 do
24 ::(j==n) -> break;
25 :: do
26 ::(choosing[j] == 0)-> break;
27 od;
28 :: if
29 ::(number[j] ==0) -> j++;
30 ::(number[j] > number[_pid]) -> j++;
31 ::((number[j] == number[_pid]) && ( j> _pid)) -> j++;
32 fi;
33 od;
34
35 number[_pid]=0
36
37 }
when I test it I get an error: pan:1: assertion violated - invalid array index (at depth 5)
when I run the trail I get this back
1: proc 2 (p) Bakery_lock.pml:8 (state 1) [choosing[_pid] = 1]
2: proc 2 (p) Bakery_lock.pml:10 (state 2) [max = 0]
2: proc 2 (p) Bakery_lock.pml:12 (state 3) [i = 0]
3: proc 2 (p) Bakery_lock.pml:14 (state 6) [i = (i+1)]
4: proc 2 (p) Bakery_lock.pml:14 (state 6) [i = (i+1)]
5: proc 2 (p) Bakery_lock.pml:14 (state 6) [i = (i+1)]
spin: indexing number[3] - size is 3
spin: Bakery_lock.pml:13, Error: indexing array 'number'
6: proc 2 (p) Bakery_lock.pml:13 (state 4) [((number[i]>max))]
Can anyone tell me why it skips this line (i == n) -> break; ?
It doesn't 'skip' that line. Spin executes every line that is executable. In your do
the line i++
is always executable and therefore, because Spin explores all possible executions, the i++
line will be executed even when (i == n)
. The fix is:
do
:: (number[i] > max) -> max=number[i];
:: (i < n) -> i++
:: (i == n) -> break;
od;