自旋隨機誤差，麪包店鎖

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;