1

さて、私はこれを持っています（これはコードの一部です）：

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  }

/////////////でスタックし（書き込みタイムアウト）、たとえばステップ40に進む方法はありません。

これは、Ricart-Agrawala アルゴリズムの一部です。ここでは次のようになります。

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  }

私は何を間違っていますか？前もって感謝します

PS クリティカル - クリティカル セクションの「シミュレーター」です。このアルゴリズムは分散システム用です...

4

1 に答える 1

1

いくつかの理由により、検証が 37/40 行目で停止することがあります。その直前のコードは次のとおりです。

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

このifステートメントは、次の場合に永久にブロックされます:J == myIDまたはch[J]がいっぱいで空にならない場合。elseに を追加しif、「キューがいっぱい」の場合を慎重に処理することで、この問題を「修正」できます。もちろん、「修正」は、モデル化しようとしているものと一致しない場合があります。

于 2014-04-25T19:54:06.693 に答える