自旋随机误差，面包店锁

Question

我使用自旋

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 } 

创建了一家面包店锁定当我测试它，我得到一个错误：锅：1：断言侵犯 - 无效的数组索引（在深度5）

当我运行的踪迹，我得到这个回

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))] 

谁能告诉我，为什么它会跳过这一行（我== N） - >突破; ？

Answer 1

它不'跳过'该行。自旋执行可执行的每一行。在您的do行i++是总是可执行文件，因此，因为Spin探索所有可能的执行，所以i++行即使在(i == n)时也会执行。修复方法是：

do  
:: (number[i] > max) -> max=number[i]; 
:: (i < n) -> i++ 
:: (i == n) -> break; 
od;