20090610

修士研究紹介：強連結成分ベースの
グラフ分割による分散並列LTL
モデル検査の高速化
2009/06/10
三輪真弘
1
研究の背景と目的
 LTLモデル検査とは，システムの振る舞いをオートマトンでモデル化し，その
状態空間を網羅的に探索することにより，線形時間時相論理 LTL（Linear
Temporal Logic）で記述された性質が満たすか判定する手法
 状態空間が巨大になることが多く，単体マシンではリソース不足
⇒ PCクラスタでの並列LTLモデル検査
 分散並列LTLモデル検査では、状態空間の分割による通信時間が実行時間
の大半を占める
 既存の分割手法であるHash-Based分割法とProperty-Driven分割法ではそれぞ
れ欠点を抱えている
 既存手法の問題点を緩和するグラフ分割により，分散並列LTLモデル検査の
高速化
2
LTLモデル検査
システムオートマトン
性質（LTL：線形時相論理）
[]<> a : いずれ（<>）aになるという状態が常に
（[]）成り立つ
c
￢[]<>aを表すオートマトン（性質オートマトン）
1
a
b
1
￢a
￢a
受理状態
2
 システムを表すオートマトンとLTLの否定を表すオートマトンの積オー
トマトングラフの探索問題（到達性検査，サイクル探索）に帰着
1c
1a
2c
1b
2a
2b
 状態空間が巨大になることが多く，単体マシンでは資源不足
⇒ PCクラスタでの並列LTLモデル検査
3
DiVinE-Cluster
 Distributed Verification Environment（チェコの
Masaryk大学で開発）
分散並列LTLモデル検査ツール
 MPIによる通信
 複数の並列LTLモデル検査アルゴリズム
 グラフ分割法
Hash-Based分割法
頂点をランダムに分割
Property-Driven分割法
（次スライド）
4
Property-Driven分割法
性質
システム
[]<> a :いずれaになるという状態が常に成り立つ
c
￢[]<> aを表すオートマトン
a
1
b
1
同期積
1c
1a
SCC（強連
結成分）
SCC数は少ない
ことがほとんど！
￢a
￢a
2
2c
1b
2a
2b
SCCでない
5
Hash On SCC分割法（提案手法）
既存グラフ分割法の問題点
Hash-Based分割法・・・通信オーバーヘッド
Property-Driven分割法・・・実行PE数が少数
Property-Driven分割法を行ってからHashBased分割法を行う
局所性と多数PEでの実行を活かす
6
Hash On SCC分割法（提案手法）
性質オートマトンのSCC ID ： 0
性質オートマトンのSCC ID ： 1
・・・・・・・
・・・・・・・
・・・・・・・
・
・
・
・・・・・・・
・・・・・・
SCC ID ： 1
を担当
SCC ID：0を
担当
・・・
・・・
7
Hash On SCC分割法の評価実験
（内容）
 LTLモデル検査向けベンチマークを利用（全10問）
 デフォルトのHash-Based分割法と比較
 性質オートマトンの各SCCには，等しいPE数を割り当てる
（適用アルゴリズム）
 OWCTYアルゴリズム
（環境）
 Core2Duo 2.13GHz，4GBメモリ，16ノード，GigE
 DiVinE-Cluster version 0.7.1
（測定方法）
 5回測定し，上位3位（実行時間の短い順）の平均を取る
 1200秒で打ち切り
8
One-Way-Catch-Them-Young (OWCTY)
受理サイクル上には存在し得ない頂点をグラフから繰り返し取
り除く
 頂点集合が空になればサイクルが存在しない
 削除する頂点（2つの削除ルール）
 入次数が0の頂点
 受理頂点から到達不可能な頂点
 グラフを全構築してから探索（not on-the-fly）
 頂点集合をHash-Based関数で分け，各計算ノードはlocalな
頂点に削除ルールを適用することで並列化
9
実験結果
473.2%
提案手法
の適用
10
負荷分散の最適化
SCCに等しいPE数を割り当てても最適でない
デフォルトでは，SCC2個の問題において，16PEごと
PE数の割り当ての変更による適切な負荷分散
16x2
16x2 HoS
16x2 HoS 最適化
elevator.5.prop3（28, 4）
100（%）
473.2
98.8
lamport.7.prop4（17, 15）
100
89.9
82.2
rether.5.prop5（17, 15）
100
83.5
77.6
reher.7.prop5（17, 15）
100
92.8
88.7
11
適切な割り当ての自動化に向けて
短時間の到達可能性検査による強連結成分
毎の処理状態数の差異情報を利用
表：elevator.5.prop3のSCC毎の処理状態数
scc 0
（scc 0）/（scc 1）
scc 1
3秒
52,194
7,204
7.25
5秒
150,721
24,340
6.19
10秒
347,942
49,649
7.00
184,925,888
20,630,544
8.96
（完全展開）
12
関連研究
Alberto L. L. :”Simplified Distributed LTL
Model Checking by Localizing Cycles”
（本研究との違い）
LTLモデル検査アルゴリズムは，二段階深さ
優先探索
システムオートマトンもSCCに分解する（重た
くないか）
この手法が適用されて動作するシステムがな
い
13
補足：SCC2個の問題を考えることの妥当性
実験で用いた問題10問中8問で性質オートマ
トンの形が同じ（強連結成分数 etc）
SCCが2個になるLTLは以下の2種類である
[] (a -> <> b)
応答性
[]<> a
再発性
これら2つは、LTLモデル検査でよく利用され
る（参考文献：Gerald J. Holzmann :”The Spin Model
Checker”）
14
まとめと今後の課題
（まとめ）
Hash On SCC分割法によって分散並列LTL
モデル検査の高速化を行った
負荷分散の最適化によるさらなる高速化
負荷分散のためのプロファイリング
（課題）
プロファイリングを利用した自動割り当て
15
既出の質問事項、コメント
台数増やしたら同じ
提案手法＋プロファイリング時間＜既存手法
か？
見つかるサイクルの大きさによる影響
16

Download Report