プログラミングなどなど

プログラミングに関係しそうな内容を

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