第 4 章 TAS 相互排除プロトコルに対する無排斥性のモデル検査 47
4.3 DCA を適用したモデル検査
る。一方のプロセスがwsに止まり続け、もう片方のプロセスのみ何度もcsを通 過する結果となる。全ての遷移に対して弱公平性を仮定したmodelCheck(init2, wfair2 -> lofree2)も、反例を得て失敗する。同様に一方のプロセスがws に 止まり続け、もう片方のプロセスのみ何度もcsを通過する結果となる。これは、
弱公平性では仮定が弱いためである。全ての遷移に対して強公平性を仮定した modelCheck(init2, sfair2 -> lofree2)は、成功する。結果は、CPU時間にし て691799ミリ秒で、195666回の書き換えとなった。プロセス３個に増やした場 合は、半日経っても停止しない結果となった。
次節では、この無排斥性のモデル検査に対して、DCAを適用することで効率化が 測れるかどうかについて実験を行い、その効果について分析する。
上記４式中、上から３つまでの式のlofree(pi) は、擬公平性を表しており、
lofree(pi) = wait(pi) ⇝ crit(pi)である。今回の分割では、上記の４番目の LTL式から確認できるように恒真式であり、全体として真であることが見て取れる ため、モデル検査は省略することとする。Kees,TASに対して、DCAを適用したMaude コードと、実行結果は以下の通りである。
r e d u c e in TAS - F O R M U L A : m o d e l C h e c k ( init3 , wf ( e x i t ( p3 ) ) /\ ( wf ( e x i t ( p2 ) ) /\ sf ( try ( p1 ) ) ) - > l o f r e e ( p1 ) ) .
r e w r i t e s : 1 9 2 6 in 18 ms cpu (21 ms r e a l ) ( 1 0 2 2 1 8 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
= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =
r e d u c e in TAS - F O R M U L A : m o d e l C h e c k ( init3 , wf ( e x i t ( p1 ) ) /\ ( wf ( e x i t ( p3 ) ) /\ sf ( try ( p2 ) ) ) - > l o f r e e ( p2 ) ) .
r e w r i t e s : 1 9 2 6 in 19 ms cpu (22 ms r e a l ) ( 9 6 9 0 5 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
= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =
r e d u c e in TAS - F O R M U L A : m o d e l C h e c k ( init3 , wf ( e x i t ( p2 ) ) /\ ( wf ( e x i t ( p1 ) ) /\ sf ( try ( p3 ) ) ) - > l o f r e e ( p3 ) ) .
r e w r i t e s : 1 9 2 6 in 20 ms cpu (22 ms r e a l ) ( 9 3 5 7 2 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 4.8: DCAを適用したプロセス３個の場合のモデル検査実行結果
公平性⇒擬公平性のモデル検査は、それぞれ20ミリ秒程度で検査が成功。今 回は、擬公平性⇒活性のモデル検査は、恒真のため不要であった。DCAを適用し ない場合、すなわち公平性⇒活性のモデル検査は、半日経っても停止しなかった ため、大幅に効率化が果たされたと言える。
改めて、プロセス2個の場合からプロセス８個までの、公平性⇒擬公平性のモ デル検査を、各プロセスにつき１つずつ検査した結果は以下の通りである。2
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 , wf ( e x i t ( p2 ) ) /\ sf ( try ( p1 ) ) - > l o f r e e ( p1 ) ) .
r e w r i t e s : 738 in 5 ms cpu (6 ms r e a l ) ( 1 2 6 7 8 2 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
= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =
r e d u c e in TAS - F O R M U L A : m o d e l C h e c k ( init3 , wf ( e x i t ( p3 ) ) /\ ( wf ( e x i t ( p2 ) ) /\ sf ( try ( p1 ) ) ) - > l o f r e e ( p1 ) ) .
r e w r i t e s : 1 9 2 6 in 15 ms cpu (18 ms r e a l ) ( 1 2 4 3 2 2 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
= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =
r e d u c e in TAS - F O R M U L A : m o d e l C h e c k ( init4 , wf ( e x i t ( p4 ) ) /\ (
2公平性⇒活性のモデル検査は、恒真のため不要である。
wf ( e x i t ( p3 ) ) /\ ( wf ( e x i t ( p2 ) ) /\ sf ( try ( p1 ) ) ) ) - > l o f r e e ( p1 ) ) .
r e w r i t e s : 4 9 3 5 in 50 ms cpu (62 ms r e a l ) ( 9 7 5 9 5 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
= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =
r e d u c e in TAS - F O R M U L A : m o d e l C h e c k ( init5 , wf ( e x i t ( p5 ) ) /\ ( wf ( e x i t ( p4 ) ) /\ ( wf ( e x i t ( p3 ) ) /\ ( wf ( e x i t ( p2 ) ) /\ sf ( try ( p1 ) ) ) ) ) - > l o f r e e ( p1 ) ) .
r e w r i t e s : 1 2 6 3 4 in 210 ms cpu ( 2 7 3 ms r e a l ) ( 6 0 1 1 7 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
= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =
r e d u c e in TAS - F O R M U L A : m o d e l C h e c k ( init6 , wf ( e x i t ( p6 ) ) /\ ( wf ( e x i t ( p5 ) ) /\ ( wf ( e x i t ( p4 ) ) /\ ( wf ( e x i t ( p3 ) ) /\ ( wf ( e x i t ( p2 ) ) /\ sf ( try ( p1 ) ) ) ) ) ) - > l o f r e e ( p1 ) ) .
r e w r i t e s : 3 2 4 0 5 in 811 ms cpu ( 1 0 9 8 ms r e a l ) ( 3 9 9 4 8 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
= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =
r e d u c e in TAS - F O R M U L A : m o d e l C h e c k ( init7 , wf ( e x i t ( p7 ) ) /\ ( wf ( e x i t ( p6 ) ) /\ ( wf ( e x i t ( p5 ) ) /\ ( wf ( e x i t ( p4 ) ) /\ ( wf ( e x i t ( p3 ) ) /\ ( wf ( e x i t ( p2 ) ) /\ sf ( try ( p1 ) ) ) ) ) ) ) - > l o f r e e ( p1 ) ) .
r e w r i t e s : 8 3 0 4 6 in 3 8 7 3 ms cpu ( 5 5 4 1 ms r e a l ) ( 2 1 4 4 0 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
= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =
r e d u c e in TAS - F O R M U L A : m o d e l C h e c k ( init8 , wf ( e x i t ( p8 ) ) /\ ( wf ( e x i t ( p7 ) ) /\ ( wf ( e x i t ( p6 ) ) /\ ( wf ( e x i t ( p5 ) ) /\ ( wf ( e x i t ( p4 ) ) /\ ( wf ( e x i t ( p3 ) ) /\ ( wf ( e x i t ( p2 ) ) /\ sf ( try ( p1 ) ) ) ) ) ) ) ) - > l o f r e e ( p1 ) ) .
r e w r i t e s : 2 1 1 8 5 5 in 2 0 8 0 3 ms cpu ( 3 0 1 1 5 ms r e a l ) ( 1 0 1 8 3 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 4.9: DCAを適用したプロセス２から８個までのモデル検査実行結果
今回のTASのDCAの実験では、プロセス数の場合毎に１つずつ検査してある。し たがって、CPU実行時間を比較する場合は、実行時間をプロセス数で乗じたものが 分割統治全体の結果となる。以上までの結果をまとめたものは、図??である。
DCA適用前では、実験環境ではプロセス２個までしか結果を得ることができな かった。対して、DCA適用後は、プロセス８個に拡張しても一定時間内に結果を得 ることができた。
図 4.2: TASのDCA適用前後の比較