第 3 章 Qlock 相互排除プロトコルに対する無排斥性のモデル検査 28
3.3 EES クリプケ構造によるモデル検査
構造を模したクリプケ構造を用いる必要がある。次章では、Qlockを拡張し、公 平性の仮定を記述できるように修正し、再び無排斥性のモデル検査の実験をする。
24 pr PID . 25 s o r t Q u e u e .
26 op e m p t y : - > Q u e u e [ c t o r ] .
27 op _ | _ : Pid Q u e u e - > Q u e u e [ c t o r ] . 28 op enq : Q u e u e Pid - > Q u e u e .
29 op deq : Q u e u e - > Q u e u e . 30 var Q : Q u e u e .
31 v a r s X Y : Pid .
32 eq enq ( empty , X ) = X | e m p t y . 33 eq enq ( Y | Q , X ) = Y | enq ( Q , X ) . 34 eq deq ( e m p t y ) = e m p t y .
35 eq deq ( X | Q ) = Q . 36 e n d f m
37
38 fm o d S O U P is
39 pr PID .
40 pr L O C A T I O N . 41 pr Q U E U E . 42 pr L E V E N T .
43 s o r t s O C o m p S o u p . 44 s u b s o r t O C o m p < S o u p . 45 *** o b s e r v a b l e c o m p o n e n t s
46 op pc [ _ ] :_ : Pid L o c a t i o n - > O C o m p [ c t o r ] . 47 op q u e u e : _ : Q u e u e - > O C o m p [ c t o r ] .
48 op l e : _ : L E v e n t - > O C o m p [ c t o r ] . 49 *** s o u p
50 op __ : S o u p S o u p - > S o u p [ c t o r a s s o c c o m m ] . 51 e n d f m
52 *** S_ { ees , Q l o c k } END
Listing 3.8: Sees,Qlock
状態の集合Sees,Qlock = {(e, s)|e ∈ lE, s ∈ lS}は、前節で形式化したSQlockと 同様に、sは、プロセスの場所と、プロセス識別子の待ち行列とを示す観測可能 成分とを表す。違いは、モジュールLEVENTを追加したことである。LEVENTには、
ソートLEventと、その要素のラベル付きイベントeがnotran、dose、want、try、 exitとしてそれぞれ定義されている。notranはιを示す定数、それ以外はプロセ ス識別子を受け取ってラベル付きイベントを返す演算le: として定義される。こ れにより、ラベル付きイベントeは観測可能成分として表現され、状態(e, s)は観 測可能成分4つからなるスープとして表現される。
初期状態の集合Iees,QlockをMaudeコードで記述したものは以下の通りである。
53 *** I_ { ees , Q l o c k } 54 fm o d INIT - S O U P is 55 pr S O U P .
56 ops i n i t 2 i n i t 3 i n i t 4 i n i t 5 i n i t 6 i n i t 7 i n i t 8 : - > S o u p . 57 eq i n i t 2 = ( pc [ p1 ] : rs ) ( pc [ p2 ] : rs ) ( q u e u e : e m p t y ) ( le:
n o t r a n ) .
58 eq i n i t 3 = ( pc [ p1 ] : rs ) ( pc [ p2 ] : rs ) ( pc [ p3 ] : rs ) ( q u e u e : e m p t y ) ( le: n o t r a n ) .
59 eq i n i t 4 = ( pc [ p1 ] : rs ) ( pc [ p2 ] : rs ) ( pc [ p3 ] : rs ) ( pc [ p4 ] : rs ) ( q u e u e : e m p t y ) ( le: n o t r a n ) .
60 eq i n i t 5 = ( pc [ p1 ] : rs ) ( pc [ p2 ] : rs ) ( pc [ p3 ] : rs ) ( pc [ p4 ] : rs ) ( pc [ p5 ] : rs ) ( q u e u e : e m p t y ) ( le: n o t r a n ) .
61 eq i n i t 6 = ( pc [ p1 ] : rs ) ( pc [ p2 ] : rs ) ( pc [ p3 ] : rs ) ( pc [ p4 ] : rs ) ( pc [ p5 ] : rs ) ( pc [ p6 ] : rs ) ( q u e u e : e m p t y ) ( le:
n o t r a n ) .
62 eq i n i t 7 = ( pc [ p1 ] : rs ) ( pc [ p2 ] : rs ) ( pc [ p3 ] : rs ) ( pc [ p4 ] : rs ) ( pc [ p5 ] : rs ) ( pc [ p6 ] : rs ) ( pc [ p7 ] : rs ) ( q u e u e : e m p t y ) ( le: n o t r a n ) .
63 eq i n i t 8 = ( pc [ p1 ] : rs ) ( pc [ p2 ] : rs ) ( pc [ p3 ] : rs ) ( pc [ p4 ] : rs ) ( pc [ p5 ] : rs ) ( pc [ p6 ] : rs ) ( pc [ p7 ] : rs ) ( pc [ p8 ] : rs ) ( q u e u e : e m p t y ) ( le: n o t r a n ) .
64 e n d f m
Listing 3.9: Iees,Qlock
Iees,Qlock ={(ι, s)|s ∈lI}は、本節ではプロセスが２個から８個までの７通りを
定める。ιはnotranで、sは全てのプロセス識別子が場所rs、待ち行列emptyで 定義する。
遷移の集合Tees,Qlockは、以下のような書き換え規則で表現する。
65 *** T_ { ees , Q l o c k } 66 mod T R A N S I T I O N is 67 pr S O U P .
68 var Q : Q u e u e .
69 var I : Pid .
70 var E : L E v e n t .
71 rl [ d o s e ] : ( pc [ I ] : rs ) ( le: E )
72 = > ( pc [ I ] : rs ) ( le: d o s e ( I ) ) . 73 rl [ w a n t ] : ( pc [ I ] : rs ) ( q u e u e : Q ) ( le: E )
74 = > ( pc [ I ] : ws ) ( q u e u e : enq ( Q , I ) ) ( le: w a n t ( I ) ) . 75 rl [ try ] : ( pc [ I ] : ws ) ( q u e u e : ( I | Q ) ) ( le: E )
76 = > ( pc [ I ] : cs ) ( q u e u e : ( I | Q ) ) ( le: try ( I ) ) . 77 rl [ e x i t ] : ( pc [ I ] : cs ) ( q u e u e : Q ) ( le: E )
78 = > ( pc [ I ] : rs ) ( q u e u e : deq ( Q ) ) ( le: e x i t ( I ) ) . 79 en d m
Listing 3.10: Tees,Qlock
Tees,Qlock ={((e, s),(e′, s′))|e, e ∈lE, s, s′ ∈lS,(s, e′, s′)∈ lT)} は、前節と同様 に4つの書き換え規則が定められている。ただしそれぞれの遷移に対し、ラベル付 きイベントの観測成分の書き換えを加えている。例えば書き換え規則[dose]は、
プロセス識別子の位置には変化はないが、ラベル付きイベントの観測可能成分は
(le: dose(I))となり、直前の遷移が[dose]であることを状態として記録して いる。
原子状態命題の集合Pees,Qlockと、ラベリング関数Lees,QlockをMaudeコードで記 述したものは以下の通りである。
80 in model - c h e c k e r .
81 *** P_ { ees , Q l o c k } , L_ { ees , Q l o c k } 82 mod QLOCK - P R O P is
83 pr T R A N S I T I O N . 84 inc S A T I S F A C T I O N . 85 s u b s o r t S o u p < S t a t e . 86 *** P_ { ees , Q l o c k }
87 op w a i t : Pid - > P r o p . 88 op c r i t : Pid - > P r o p .
89 op e n a b l e d : L E v e n t - > P r o p . 90 op a p p l i e d : L E v e n t - > P r o p .
91 var I : Pid .
92 var Q : Q u e u e . 93 var S : S o u p . 94 var PR : P r o p . 95 var E : L E v e n t . 96 *** L_ { ees , Q l o c k }
97 eq ( pc [ I ] : ws ) S |= w a i t ( I ) = t r u e . 98 eq ( pc [ I ] : cs ) S |= c r i t ( I ) = t r u e .
99 eq ( pc [ I ] : rs ) S |= e n a b l e d ( d o s e ( I ) ) = t r u e . 100 eq ( pc [ I ] : rs ) S |= e n a b l e d ( w a n t ( I ) ) = t r u e .
101 eq ( pc [ I ] : ws ) ( q u e u e : ( I | Q ) ) S |= e n a b l e d ( try ( I ) ) = tr u e .
102 eq ( pc [ I ] : cs ) S |= e n a b l e d ( e x i t ( I ) ) = t r u e . 103 eq ( le: E ) S |= a p p l i e d ( E ) = t r u e .
104 eq S |= PR = f a l s e [ o w i s e ] . 105 en d m
Listing 3.11: Pees,QlockとLees,Qlock
Pees,Qlock =lP ∪lEのlP はプロセス識別子Pidを受け取ってラベル付き原子状
態命題Propを返す2つの演算子wait、critとして、lEはラベル付き遷移LEvent を受け取ってラベル付き原子状態命題Propを返す2つの演算子enabled、applied として定義する。
Lees,Qlock :lS → {e} ∪lL(s)はeqキーワードを用いて等式8行で定義する。3こ こで変数Pはプロセス識別子、Sは(観測可能成分の)スープ、Qは待ち行列、PR は原子状態命題、Eはラベル付きイベントである。
以上で、Qlockをクリプケ構造Kees,QlockとしてMaudeで形式化した。次に、これ
3ここで定まるラベリング関数Lees,Qlockは、例えばスープ(queue : (p1|p2|empty)) (pc[p1] : cs) (pc[p2] : ws) (le : try(p1))を受け取り、原子状態命題の集合{crit(p1),wait(p2),enabled(exit(p1)), enabled(try(p2)), applied(try(p1))} を返すような関数である。
に対し再び無排斥性のモデル検査をする。無排斥性のモデル検査は、以下のMaude コードで記述できる。
106 mod QLOCK - F O R M U L A is 107 pr INIT - S O U P . 108 inc QLOCK - P R O P . 109 inc MODEL - C H E C K E R . 110 inc LTL - S I M P L I F I E R . 111 var E : L E v e n t .
112 var I : Pid .
113 op wf : L E v e n t - > F o r m u l a .
114 eq wf ( E ) = ( < > [] e n a b l e d ( E ) ) - > ([] < > a p p l i e d ( E ) ) . 115 en d m
116
117 mod P R O C 2 M C is
118 pr QLOCK - F O R M U L A .
119 ops m u t e x 2 l o f r e e 2 f a i r 2 q f a i r 2 : - > F o r m u l a . 120 eq m u t e x 2 = [] ~( c r i t ( p1 ) /\ c r i t ( p2 ) ) .
121 eq l o f r e e 2 = ( w a i t ( p1 ) | - > c r i t ( p1 ) ) /\ ( w a i t ( p2 ) | - > c r i t ( p2 ) ) .
122 eq f a i r 2 = wf ( d o s e ( p1 ) ) /\ wf ( d o s e ( p2 ) ) /\
123 wf ( w a n t ( p1 ) ) /\ wf ( w a n t ( p2 ) ) /\
124 wf ( try ( p1 ) ) /\ wf ( try ( p2 ) ) /\
125 wf ( e x i t ( p1 ) ) /\ wf ( e x i t ( p2 ) ) . 126 en d m
127 red in P R O C 2 M C : m o d e l C h e c k ( init2 , f a i r 2 - > l o f r e e 2 ) . Listing 3.12: 無排斥性のモデル検査
QLOCK-FORMULAとPROC2MCは、モデル検査のために定義したモジュールである。
lofree2は、検査したい性質である無排斥性を形式化したLTL式である。wf(E)は、
ラベル付きイベントを受け取り、弱公平性の仮定を示すLTL式を返す。fair2は、
すべてのラベル付きイベントに対して弱公平性を仮定したLTL式である。wf(E) 内の->は論理包含を表す記号である。したがって、fair2 -> lofree2は、すべて のラベル付き遷移に対して弱公平性を仮定した無排斥性を記述したLTL式である。
modelCheck()関数に、第一引数に初期状態init2、第二引数にfair2 -> lofree2 を与えて実行した結果は以下の通り成功する。
r e d u c e in P R O C 2 M C : m o d e l C h e c k ( init2 , f a i r 2 - > l o f r e e 2 ) . r e w r i t e s : 1 6 3 6 6 in 3 1 4 9 6 ms cpu ( 4 6 1 4 3 ms r e a l ) ( 5 1 9 r e w r i t e s /
s e c o n d )
r e s u l t B o o l : t r u e
Listing 3.13: 弱公平性を仮定した無排斥性のモデル検査の実行結果
なお、本稿の実験環境ではプロセス３個の場合、一定時間を経過してもモデル
検査は停止しなかった。
次節では、この無排斥性のモデル検査に対して、DCAを適用することで効率化が 測れるかどうかについて再現する実験を行い、その効果について分析する。