<<もくじ:Formal Verification Memo
この例は、Basic Spin Manualで取り上げられているもの*1で、 もともとは 1966 年に H. Hyman が Communication of the ACM で発表したものだそうです。 また、これは、Dekker の初期の解としてしられているそうですが、 いわゆる Dekker's algorithm ではありません。
いわゆる Dekker's algorithm と違い、この方法には欠陥があります。 その欠陥をいかにして検出するかというのが、この例題の趣旨です。
bool want[2]; bool turn; byte cnt; proctype P(bool i) { want[i] = 1; do :: (turn != i) -> (!want[1-i]); turn = i :: (turn == i) -> break od; /* critical section */ cnt = cnt + 1; assert(cnt == 1); cnt = cnt - 1; want[i] = 0; } init { run P(0); run P(1); }
グローバル変数、want[n], turn は排他制御のためのものです。 各プロセスは、これらの変数を用いて、排他制御を行います。
cnt は、排他が実現されているかどうかをチェックするためのグローバル変数です。
では、前述のソースファイルで表現された検証モデルを実行してみましょう。
% spin -a hyman1 % gcc -DSAFETY -o pan pan.c % ./pan pan: assertion violated (cnt==1) (at depth 12) pan: wrote hyman1.trail (Spin Version 5.1.4 -- 27 January 2008) Warning: Search not completed + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 36 byte, depth reached 23, errors: 1 60 states, stored 16 states, matched 76 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) 4.653 memory usage (Mbyte)
検証プログラムは、assert 違反があったことを報告しています。 エラーシーケンスの追跡は以下のようにして得られます。
% spin -t -p hyman1 Starting :init: with pid 0 Starting P with pid 1 1: proc 0 (:init:) line 22 "hyman1" (state 1) [(run P(0))] Starting P with pid 2 2: proc 0 (:init:) line 22 "hyman1" (state 2) [(run P(1))] 3: proc 2 (P) line 7 "hyman1" (state 1) [want[i] = 1] 4: proc 2 (P) line 9 "hyman1" (state 2) [((turn!=i))] 5: proc 2 (P) line 9 "hyman1" (state 3) [(!(want[(1-i)]))] 6: proc 1 (P) line 7 "hyman1" (state 1) [want[i] = 1] 7: proc 1 (P) line 10 "hyman1" (state 5) [((turn==i))] 8: proc 2 (P) line 9 "hyman1" (state 4) [turn = i] 9: proc 2 (P) line 10 "hyman1" (state 5) [((turn==i))] 10: proc 2 (P) line 15 "hyman1" (state 10) [cnt = (cnt+1)] 11: proc 2 (P) line 16 "hyman1" (state 11) [assert((cnt==1))] 12: proc 1 (P) line 15 "hyman1" (state 10) [cnt = (cnt+1)] spin: line 16 "hyman1", Error: assertion violated spin: text of failed assertion: assert((cnt==1)) 13: proc 1 (P) line 16 "hyman1" (state 11) [assert((cnt==1))] spin: trail ends after 13 steps #processes: 3 want[0] = 1 want[1] = 1 turn = 1 cnt = 2 13: proc 2 (P) line 18 "hyman1" (state 12) 13: proc 1 (P) line 18 "hyman1" (state 12) 13: proc 0 (:init:) line 22 "hyman1" (state 3) <valid end state> 3 processes created
なるほど、なるほど。 グローバル変数 turn, want[1-i] を確認するのと、turn の更新がアトミックじゃないので、 期待どおりにいかない場合があるんですね。
上のコーディング例では、assert 文を各プロセスのクリティカル・セッション内に書きましたが、 独立の監視プロセスにまかせることもできます。
bool want[2]; bool turn; byte cnt; proctype P(bool i) { want[i] = 1; do :: (turn != i) -> (!want[1-i]); turn = i :: (turn == i) -> break od; cnt = cnt+1; /* critical section */ cnt = cnt-1; want[i] = 0 } proctype monitor() { assert(cnt == 0 || cnt == 1) } init { run P(0); run P(1); run monitor() }
>>次のページ:Dekker0 by Murphi