<<もくじ:Formal Verification Memo
次に、Murphi で同じモデルの検証をしてみたいと思います。 Murphi におけるモデルの記述は、Promela の場合とは少し違った感じになります。
(ご注意:前ページの promela モデルは、Basic Spin Manual に書いてあったものなので、 おそらく間違っていないと思いますが、本ページのモデルは、さっき海野が書いたものなので、 嘘っぱちである可能性大です。バグってたり、嘘っぱちだったりする箇所を見つけたら、 おしえてください。 uDiary の方につっこんでもらえるとありがたいです。)
コーディングに先だって、検証対象の状態遷移図を書いてみます。
上図は、先ほどの promela によるコードを見ながら書いたものです。 状態遷移の形にできてしまえば、murphi で記述するのは簡単です。
-- Filename: dek0.m -- Version: Murphi 3.1 -- Content: Bad Example for mutual exclusion. type proc_idx_t: 0..1; want_t: enum {T, F}; state_t: enum {S0, S1, S2, S3, C}; var turn: proc_idx_t; var want: Array [ proc_idx_t ] of want_t; var stat: Array [ proc_idx_t ] of state_t; procedure goto(p: proc_idx_t; s: state_t); begin stat[p] := s; end; ruleset p: proc_idx_t do rule "S0 -> S1 always" stat[p] = S0 ==> begin want[p] := T; goto(p, S1); end; rule "S1 -> S2 if other's turn" stat[p] = S1 & turn != p ==> begin goto(p, S2); end; rule "S2 -> S3 if another is not wanting" stat[p] = S2 & want[1-p] = F ==> begin goto(p, S3); end; rule "S2 -> S1 if another is wanting" stat[p] = S2 & want[1-p] = T ==> begin goto(p, S1); end; rule "S3 -> S1 always" stat[p] = S3 ==> begin turn := p; goto(p, S1); end; rule "S1 -> C (Critical) if its turn" stat[p] = S1 & turn = p ==> begin goto(p, C); end; rule "Critical Session" stat[p] = C ==> begin want[p] := F; goto(p, S0); end; end; startstate begin for p : proc_idx_t do goto(p, S0); want[p] := F; end; turn := 0; end; invariant !(stat[0] = C & stat[1] = C);
muphi モデルを実行するには、まず mu で murphi モデル (今回のファイル名は dek0.m) をコンパイルして、さらに出来た C++ プログラムを (g++ などで) コンパイルします。
% mu dek0.m % g++ -I ${Murphi3.1path}/include -o dek0 dek0.C % ./dek0 This program should be regarded as a DEBUGGING aid, not as a certifier of correctness. Call with the -l flag or read the license file for terms and conditions of use. Run this program with "-h" for the list of options. Bugs, questions, and comments should be directed to "murphi@verify.stanford.edu". Murphi compiler last modified date: Jan 29 1999 Include files last modified date: Jan 29 1999 ========================================================================== ========================================================================== Murphi Release 3.1 Finite-state Concurrent System Verifier. Copyright (C) 1992 - 1999 by the Board of Trustees of Leland Stanford Junior University. ========================================================================== Protocol: dek0 Algorithm: Verification by breadth first search. with symmetry algorithm 3 -- Heuristic Small Memory Normalization with permutation trial limit 10. Memory usage: * The size of each state is 40 bits (rounded up to 8 bytes). * The memory allocated for the hash table and state queue is 8 Mbytes. With two words of overhead per state, the maximum size of the state space is 476219 states. * Use option "-k" or "-m" to increase this, if necessary. * Capacity in queue for breadth-first search: 47621 states. * Change the constant gPercentActiveStates in mu_prolog.inc to increase this, if necessary. Warning: No trace will not be printed in the case of protocol errors! Check the options if you want to have error traces. ========================================================================== Result: Invariant "Invariant 0" failed. State Space Explored: 203 states, 202 rules fired in 0.10s. Analysis of State Space: There are rules that are never fired. If you are running with symmetry, this may be why. Otherwise, please run this program with "-pr" for the rules information.
やはり、Invariant (不変な表明) 違反が検出されました。
失敗ケースのトレースは、-tv オプション付きで実行することで得られます。
% ./dek0 -tv ... (略) ... Startstate Startstate 0 fired. turn:0 want[0]:F want[1]:F stat[0]:S0 stat[1]:S0 ---------- Rule S0 -> S1 always, p:1 fired. want[1]:T stat[1]:S1 ---------- Rule S1 -> S2 if other's turn, p:1 fired. stat[1]:S2 ---------- Rule S2 -> S3 if another is not wanting, p:1 fired. stat[1]:S3 ---------- Rule S0 -> S1 always, p:0 fired. want[0]:T stat[0]:S1 ---------- Rule S1 -> C (Critical) if its turn, p:0 fired. stat[0]:C ---------- Rule S3 -> S1 always, p:1 fired. turn:1 stat[1]:S1 ---------- Rule S1 -> C (Critical) if its turn, p:1 fired. The last state of the trace (in full) is: turn:1 want[0]:T want[1]:T stat[0]:C stat[1]:C ---------- End of the error trace. ... (略) ...
検出された失敗ケースは、前ページ (Dekker0 by Spin) のモデルで検出されたものと同じですね。 turn != p & want[1-p] = T を確認してから、turn := p の操作の間に、 相手プロセスが割り込んでしまうことで、意図しない動作となってしまっていました。