5

ダイクストラが「シーケンシャルプロセスの協調」というタイトルの論文で書いたALGOL60コードを再現しようとしています。このコードは、ミューテックス問題を解決する最初の試みです。構文は次のとおりです。

begin integer turn; turn:= 1;
      parbegin
      process 1: begin Ll: if turn = 2 then goto Ll;
                           critical section 1;
                           turn:= 2;
                           remainder of cycle 1; goto L1
                 end;
      process 2: begin L2: if turn = 1 then goto L2;
                           critical section 2;
                           turn:= 1;
                           remainder of cycle 2; goto L2
                  end
      parend
end

だから私はPromelaで上記のコードを再現しようとしました、そしてここに私のコードがあります：

#define true    1
#define Aturn true
#define Bturn false

bool turn, status;

active proctype A()
{   
    L1: (turn == 1); 
    status = Aturn;
    goto L1;
    /* critical section */
    turn = 1;

}

active proctype B()
{   
    L2: (turn == 2); 
    status = Bturn;
    goto L2;
    /* critical section */
    turn = 2;
}

never{ /* ![]p */ 
    if
    :: (!status) -> skip
    fi;
}

init
{   turn = 1;
    run A(); run B();
}

私がやろうとしているのは、ラベルL1が無限に実行されているため、公平性プロパティが保持されないことを確認することです。

ここでの問題は、neverclaimブロックがエラーを生成していないことです。取得した出力は、単に私のステートメントに到達しなかったことを示しています。

これがiSpinからの実際の出力です

spin -a  dekker.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000 
Pid: 46025

(Spin Version 6.2.3 -- 24 October 2012)
    + Partial Order Reduction

Full statespace search for:
    never claim             - (not selected)
    assertion violations    +
    cycle checks        - (disabled by -DSAFETY)
    invalid end states  +

State-vector 44 byte, depth reached 8, errors: 0
       11 states, stored
        9 states, matched
       20 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001   equivalent memory usage for states (stored*(State-vector + overhead))
    0.291   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage


unreached in proctype A
    dekker.pml:13, state 4, "turn = 1"
    dekker.pml:15, state 5, "-end-"
    (2 of 5 states)
unreached in proctype B
    dekker.pml:20, state 2, "status = 0"
    dekker.pml:23, state 4, "turn = 2"
    dekker.pml:24, state 5, "-end-"
    (3 of 5 states)
unreached in claim never_0
    dekker.pml:30, state 5, "-end-"
    (1 of 5 states)
unreached in init
    (0 of 4 states)

pan: elapsed time 0 seconds
No errors found -- did you verify all claims?

ブロックのスピンに関するすべてのドキュメントを読みましたnever{..}が、答えが見つかりませんでした（ここにリンクがあります）。また、ltl{..}ブロックを使用してみました（リンク）が、明示的には構文エラーが発生しました。ドキュメントに、initおよびの外部にある可能性があると記載されていますがproctypes、誰かがこのコードを修正するのを手伝ってもらえますか？

ありがとうございました

4

1 に答える 1

1

'true'を再定義しましたが、これはおそらく良いことではありません。私はその再定義を斥けました、そして決して主張は失敗しません。ただし、失敗は目標にとって重要ではありません。「status」の初期状態は「false」であるため、決して終了しないという主張は失敗です。

また、ブール値に1または0を割り当てるのは少し悪い形式です。代わりにtrueまたはfalseを割り当てます-またはビットを使用します。ダイクストラコードにもっと厳密に従ってみませんか？「int」または「byte」を使用してください。この問題でパフォーマンスが問題になるわけではありません。

'run'を呼び出す場合は、'active'は必要ありません。どちらか一方だけです。

'プロセス1'の私の翻訳は次のようになります：

proctype A ()
{
L1: turn !=2 ->
  /* critical section */
  status = Aturn;
  turn = 2
  /* remainder of cycle 1 */
  goto L1;
}

しかし、私はそれについて間違っている可能性があります。

于 2013-03-06T00:38:01.740 に答える