ASE 2011 Software Model Checking

Presentation on theme: "ASE 2011 Software Model Checking"— Presentation transcript:

1 ASE 2011 Software Model Checking
論文1 Identifying Future Field Accesses in Exhaustive State Space Traversal Pavel Parizek and Ondrej Lhotak

2 概要 内容 研究の対象 モデル検査の効率化 検証対象 モデル検査器 モデル検査：自動検証手法 Java のマルチスレッドプログラム
システムの取り得る状態を網羅的に探索 研究の対象 検証対象 Java のマルチスレッドプログラム モデル検査器 Java PathFinder (JPF)

3 Java PathFinder In-Situ モデルチェッカー 実装をそのまま検証 独自のVM上でプログラムを制御／実行
実装をそのまま検証　 独自のVM上でプログラムを制御／実行 考慮が必要なスケジューリングを実行 スレッドで共有しているオブジェクトが更新された場合、可能なスレッド切り替えをすべて考慮 A Thread 1 Thread 2 C B A, B, C: 命令列 C A C sharedObj.set(foo); A C B sharedObj.get(); B B sharedObj.set(foo);

4 状態削減のアイデア 観察 アプローチ 共有しているオブジェクトでも、将来、他のスレッドが実際にアクセスするとは限らない
現在のJPFでは、参照をたどってアクセス可能なオブジェクトは共有されていると判断 Conservative Approximation アプローチ 現状態で更新しようとしているオブジェクトのフィールドを、他のスレッドが将来アクセスする可能性があるかどうかを、静的解析をつかって調べる。 アクセスされないのであれば、ローカルな処理と見なせるので、コンテキストスイッチを考慮しなくてよい。

5 状態削減のアイデア A C B A, B, C: 命令列 C A C A C B B B A C A, B, C: 命令列 A B C C
Thread 1 Thread 2 C B A, B, C: 命令列 C A C sharedObj.set(foo); A C B sharedObj.get(); B B sharedObj.set(foo); Thread 1 Thread 2 A C A, B, C: 命令列 A B C C sharedObj.set(foo); A B C B sharedObj.set(foo);

6 静的解析手法 Field access analysis Pointer analysis
CFGを利用 Pointer analysis 同じインスタンスかどうかを判定 Immutable fields analysis フィールドがimmutableかどうかを判定

7 結果 実装 実験 結果 感想 様々な静的解析法をJPFに導入 WALA library を用いて実装 7つのプログラムへ適用
Field access analysis が有効 Pointer analysis はだめ ほとんど寄与しない Immutable fields analysisは効果が少ないが、コストも少ない 感想 JPFはJava Memory Modelを仮定していない。 Synchronizedでロックを取るような行儀のよいプログラムでも効果があるか？

8 ASE 2011 Software Model Checking
論文2 Model Checking Distributed Systems by Combining Caching and Process Checkpointing Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya Yoshinori Tanabe and Mitsuharu Yamamoto

9 概要 内容 基本方針 外部プロセスと相互作用するプログラムのモデル検査 JPFによる実装 SUTのみJPF上で実行 スケーラブル
Peerがjavaである必要 がない SUT: System Under Test Peer 1 SUT Peer 2

10 Checkpointing Environment
提案手法 Process Checkpointing 外部プロセス（peer）の応答が非決定的であった場合の取り扱い 例．鍵交換　（例. Diffie-Hellman） 乱数値を送信 IO Caching (ASE’09) SUTの非決定性の扱い SUTの状態がバックトラックした際、Peerをリスタートしてキャッシュした送信メッセージを再送し、Peerの状態もバックトラックする JPF Model Checker C a c h e Peer 1 Peer 2 SUT Checkpointing Environment

11 Process Checkpointing
プロセスの状態を二次記憶に保存し、その状態からのリスタートを可能にする チェックポイントをとるタイミング （1 or 2) 非決定性の原因となるシステムコール発生時 time (乱数のシード値となりうる), read (/dev/randomなどを読む) 必要なときだけチェックポイントをとるため、オーバーヘッド小 ネットワークIOオペレーション発生時 Peerのバックトラック時に、リスタート＋メッセージ再送の手間が不要

12 結果 実装 実験 実験結果 Process CheckpointingはDMTCPを利用 5種類のアプリケーションの検証を実行
Peerが決定的でcheckpointingを使わない場合とくらべて、実行時間が1分を超えるような例では、実行時間はそれほど遅くならない 多くて10%の増加 前頁の２つのチェックポイントのとり方による差はほとんどない

13 ASE 2011 Software Model Checking
論文3 Supporting Domain-Specific State Space Reductions through Local Partial-Order Reduction Peter Bokor, Johannes Kinder, Marco Serafini and Neeraj Suri

14 概要 半順序簡約（Partial Order Reduction）の新しい手法の提案 POR a b c
モデル検査における主要な状態削減手法 SPIN、LTSAなどのモデルチェッカーで実装 互いに依存していない並行トランジションがある場合に、検証に必要なものだけを考慮 1,1,1 a b c t1 t2 1 1 1 2,1,1 1,2,1 [c = 1] t1 t2 [a = 1 & b = 2] t3 t3 t2 t1 2 2 2 2,2,1 1,2,2

15 Partial Order Reduction
各状態で検証に必要なトランジションだけを考慮 どのトランジションを選ぶかが重要 正しい簡約 t1 t2 全体の遷移系 1,1,1 t3 t1 t2 t1 t2 誤った簡約 2,1,1 1,2,1 t1 t2 t3 t2 t1 2,2,1 1,2,2 t3 t2 t1

16 提案手法LPOR (Local POR) 単純な遷移選択方法 保存される性質 トランジションのローカルな情報だけで選択
言語、フォーマリズムに容易に適用可能 論文では分散システムのモデルへ適用 保存される性質 デッドロック インバリアント　(詳細はテクニカルレポート) 時相論理CTL*_x　(詳細はテクニカルレポート)

17 実験と結果 MP-Basset モデルチェッカーに適用 3種類のフォールトトレラント分散アルゴリズムに適用 結果
著者らによるJPFベースのモデルチェッカー 3種類のフォールトトレラント分散アルゴリズムに適用 プロセス数 5～7 結果 何もしない場合に比べて大幅に状態数・時間を削減（90%に達する場合も） Dynamic POR(別手法)よりも、モデルにエラーがない場合（全探索が必要な場合）は高速