SPIN:2プロセスからのメッセージ受信順序確認
前回(SPIN:LTLを使った2プロセスの実行順序確認 - プログラミングなどなど)の内容と似ていますが、今度は2つのプロセスA,BがプロセスCにメッセージ送信する例を考えてみました。前回の内容とほぼ同じなので、同じオプションで結果が得られると考えていましたが、Bが先に送信するケースだけが検出されトライ&エラーを繰り返すこととなりました。
結果として、最適化オプションの無効化-o1または-o2を行うことで欲しいケースを得ることができました。(結果以上のことは理解していません。)
モデル
$ cat -n 2msg.pml 1 mtype = { msgA, msgB } 2 3 chan ch = [2] of { mtype } 4 5 bool isRcvA = false; 6 bool isRcvB = false; 7 8 active proctype A() 9 { 10 ch ! msgA 11 } 12 13 active proctype B() 14 { 15 ch ! msgB 16 } 17 18 active proctype C() 19 { 20 mtype msg; 21 do 22 :: ch ? msg -> 23 if 24 :: msg == msgA -> isRcvA = true; 25 :: msg == msgB -> isRcvB = true; 26 fi 27 od 28 }
プロセスAとBが、プロセスCに向けてメッセージを送信するモデルです。実行の制約は無いので、22行目:プロセスCのch ? msg では、msgAを先に受信する場合とmsgBを先に受信する場合があるはずです。
ランダムシミュレーション
ランダムシミュレーションを何度か行ってみると、確かに上記の2ケースが結果として出てきます。
msgAを先に受信するケース
$ spin -r 2msg.pml 3: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) 8: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) timeout #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 12: proc 2 (C:1) 2msg.pml:21 (state 8) 12: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 12: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 3 processes created
msgBを先に受信するケース
$ spin -r 2msg.pml 3: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) 8: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) timeout #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 12: proc 2 (C:1) 2msg.pml:21 (state 8) 12: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 12: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 3 processes created
LTLでの確認
確認したい性質としては先の例と同じなので同様の式を追加して検証してみます。
検証式
以下の検証式をモデルに追加します。
検証したい性質
ltl a01 { <>[](isRcvA == true && isRcvB == true) }
検証したい性質の否定
ltl c01 { !<>[](isRcvA == true && isRcvB == true) }
実行
検証したい性質の確認
$ spin -run -ltl a01 2msg.pml pan: ltl formula a01 (Spin Version 6.5.0 -- 17 July 2019) + Partial Order Reduction Full statespace search for: never claim + (a01) assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 44 byte, depth reached 17, errors: 0 43 states, stored (83 visited) 83 states, matched 166 transitions (= visited+matched) 0 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.003 equivalent memory usage for states (stored*(State-vector + overhead)) 0.289 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 (0 of 2 states) unreached in proctype B (0 of 2 states) unreached in proctype C 2msg.pml:28, state 11, "-end-" (1 of 11 states) unreached in claim a01 _spin_nvr.tmp:10, state 13, "-end-" (1 of 13 states) unreached in claim c02 _spin_nvr.tmp:19, state 10, "(((isRcvA==1)&&(isRcvB==1)))" _spin_nvr.tmp:21, state 13, "-end-" (2 of 13 states) pan: elapsed time 0 seconds
検証したい性質がどのように成り立ったかの確認
$ spin -run -ltl c01 -c0 -e 2msg.pml pan: ltl formula c01 pan:1: acceptance cycle (at depth 18) pan: wrote 2msg.pml1.trail pan: wrote 2msg.pml2.trail (Spin Version 6.5.0 -- 17 July 2019) + Partial Order Reduction Full statespace search for: never claim + (c01) assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 44 byte, depth reached 18, errors: 2 23 states, stored (24 visited) 8 states, matched 32 transitions (= visited+matched) 0 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.002 equivalent memory usage for states (stored*(State-vector + overhead)) 0.289 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 (0 of 2 states) unreached in proctype B (0 of 2 states) unreached in proctype C 2msg.pml:28, state 11, "-end-" (1 of 11 states) unreached in claim c01 _spin_nvr.tmp:21, state 13, "-end-" (1 of 13 states) pan: elapsed time 0 seconds
エラートレイルの確認
エラートレイルを確認すると検出された2件ともmsgBを先に受信したケースとなっています。
1件目
$ spin -t1 -r 2msg.pml ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1)))) ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1))))) starting claim 4 Never claim moves to line 15 [(1)] 4: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) 12: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) Never claim moves to line 14 [(((isRcvA==1)&&(isRcvB==1)))] Never claim moves to line 19 [(((isRcvA==1)&&(isRcvB==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 19 steps #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 19: proc 2 (C:1) 2msg.pml:21 (state 8) 19: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 19: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 19: proc - (c01:1) _spin_nvr.tmp:18 (state 10)
2件目
$ spin -t2 -r 2msg.pml ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1)))) ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1))))) starting claim 4 Never claim moves to line 15 [(1)] 4: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) 12: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) Never claim moves to line 14 [(((isRcvA==1)&&(isRcvB==1)))] Never claim moves to line 19 [(((isRcvA==1)&&(isRcvB==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 19 steps #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 19: proc 2 (C:1) 2msg.pml:21 (state 8) 19: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 19: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 19: proc - (c01:1) _spin_nvr.tmp:18 (state 10) 3 processes created
トライ&エラー
検証式はあっているだろうとの考えから、今回はオプションが関係していないかと思い--helpオプションで出力される内容から該当しそうなものを試していきました。
試した結果、詳しい理由はわかりませんが以下のオプションを使用することで、msgAから受信するケースとmsgBから受信するケースの両方を検出させることができました。
オプション -o1 turn off dataflow-optimizations in verifier
$ spin -o1 -run -ltl c01 -c0 -e 2msg.pml : State-vector 44 byte, depth reached 18, errors: 4 25 states, stored (27 visited) 10 states, matched 37 transitions (= visited+matched) 0 atomic steps hash conflicts: 0 (resolved)
msgBから受信するケース
$ spin -t1 -r 2msg.pml ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1)))) ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1))))) starting claim 4 Never claim moves to line 15 [(1)] 4: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) 12: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) Never claim moves to line 14 [(((isRcvA==1)&&(isRcvB==1)))] Never claim moves to line 19 [(((isRcvA==1)&&(isRcvB==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 19 steps #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 19: proc 2 (C:1) 2msg.pml:21 (state 8) 19: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 19: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 19: proc - (c01:1) _spin_nvr.tmp:18 (state 10) 3 processes created
msgBから受信するケース
$ spin -t3 -r 2msg.pml ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1)))) ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1))))) starting claim 4 Never claim moves to line 15 [(1)] 4: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) 12: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) Never claim moves to line 14 [(((isRcvA==1)&&(isRcvB==1)))] Never claim moves to line 19 [(((isRcvA==1)&&(isRcvB==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 19 steps #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 19: proc 2 (C:1) 2msg.pml:21 (state 8) 19: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 19: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 19: proc - (c01:1) _spin_nvr.tmp:18 (state 10) 3 processes created
オプション -o2 don't hide write-only variables in verifier
$ spin -o2 -run -ltl c01 -c0 -e 2msg.pml : State-vector 44 byte, depth reached 18, errors: 4 25 states, stored (27 visited) 10 states, matched 37 transitions (= visited+matched) 0 atomic steps hash conflicts: 0 (resolved)
msgBから受信するケース
$ spin -t1 -r 2msg.pml ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1)))) ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1))))) starting claim 4 Never claim moves to line 15 [(1)] 4: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) 12: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) Never claim moves to line 14 [(((isRcvA==1)&&(isRcvB==1)))] Never claim moves to line 19 [(((isRcvA==1)&&(isRcvB==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 19 steps #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 19: proc 2 (C:1) 2msg.pml:21 (state 8) 19: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 19: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 19: proc - (c01:1) _spin_nvr.tmp:18 (state 10) 3 processes created
msbAから受信するケース
$ spin -t3 -r 2msg.pml ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1)))) ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1))))) starting claim 4 Never claim moves to line 15 [(1)] 4: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) 12: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) Never claim moves to line 14 [(((isRcvA==1)&&(isRcvB==1)))] Never claim moves to line 19 [(((isRcvA==1)&&(isRcvB==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 19 steps #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 19: proc 2 (C:1) 2msg.pml:21 (state 8) 19: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 19: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 19: proc - (c01:1) _spin_nvr.tmp:18 (state 10) 3 processes created