ASE 2011 Software Model Checking • 論文1 – Identifying Future Field Accesses in Exhaustive State Space Traversal Pavel Parizek and Ondrej Lhotak 1 概要 • 内容 – モデル検査の効率化 • モデル検査:自動検証手法 – システムの取り得る状態を網羅的に探索 • 研究の対象 – 検証対象 • Java のマルチスレッドプログラム – モデル検査器 • Java PathFinder (JPF) 2 Java PathFinder • In-Situ モデルチェッカー – 実装をそのまま検証 • 独自のVM上でプログラムを制御/実行 • 考慮が必要なスケジューリングを実行 – スレッドで共有しているオブジェクトが更新された場合、可能 なスレッド切り替えをすべて考慮 Thread 1 A, B, C: 命令列 A sharedObj.set(foo); sharedObj.set(foo); C B C C sharedObj.get(); B A Thread 2 C A B B 3 状態削減のアイデア • 観察 – 共有しているオブジェクトでも、将来、他のスレッドが 実際にアクセスするとは限らない • 現在のJPFでは、参照をたどってアクセス可能なオブジェクト は共有されていると判断 – Conservative Approximation • アプローチ – 現状態で更新しようとしているオブジェクトのフィール ドを、他のスレッドが将来アクセスする可能性がある かどうかを、静的解析をつかって調べる。 – アクセスされないのであれば、ローカルな処理と見な せるので、コンテキストスイッチを考慮しなくてよい。 4 状態削減のアイデア Thread 1 A, B, C: 命令列 A sharedObj.set(foo); A Thread 2 C B C C sharedObj.get(); C A B B B sharedObj.set(foo); Thread 1 A, B, C: 命令列 A sharedObj.set(foo); B sharedObj.set(foo); Thread 2 C A B C C A C B 5 静的解析手法 • Field access analysis – CFGを利用 • Pointer analysis – 同じインスタンスかどうかを判定 • Immutable fields analysis – フィールドがimmutableかどうかを判定 6 結果 • 実装 – 様々な静的解析法をJPFに導入 – WALA library を用いて実装 • 実験 – 7つのプログラムへ適用 • 結果 – Field access analysis が有効 – Pointer analysis はだめ • ほとんど寄与しない – Immutable fields analysisは効果が少ないが、コストも少ない • 感想 – JPFはJava Memory Modelを仮定していない。 – Synchronizedでロックを取るような行儀のよいプログラムでも効果が あるか? 7 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 8 概要 • 内容 – 外部プロセスと相互作用するプログラムのモデル 検査 – JPFによる実装 • 基本方針 – SUTのみJPF上で実行 • スケーラブル • Peerがjavaである必要 がない SUT: System Under Test Peer 1 SUT Peer 2 9 提案手法 • Process Checkpointing – 外部プロセス(peer)の応答が非決定的であった場合の 取り扱い • 例.鍵交換 (例. Diffie-Hellman) – 乱数値を送信 • IO Caching (ASE’09) – SUTの非決定性の扱い • SUTの状態がバックトラックした際、Peerをリスタートしてキャッシュ した送信メッセージを再送し、Peerの状態もバックトラックする JPF Model Checker SUT C a c h e Peer 1 Peer 2 Checkpointing Environment 10 Process Checkpointing • Checkpointing – プロセスの状態を二次記憶に保存し、その状態 からのリスタートを可能にする – チェックポイントをとるタイミング (1 or 2) 1. 非決定性の原因となるシステムコール発生時 – time (乱数のシード値となりうる), read (/dev/randomなどを読 む) – 必要なときだけチェックポイントをとるため、オーバーヘッド小 2. ネットワークIOオペレーション発生時 – Peerのバックトラック時に、リスタート+メッセージ再送の手間 が不要 11 結果 • 実装 – Process CheckpointingはDMTCPを利用 • 実験 – 5種類のアプリケーションの検証を実行 • 実験結果 – Peerが決定的でcheckpointingを使わない場合とくら べて、実行時間が1分を超えるような例では、実行時 間はそれほど遅くならない • 多くて10%の増加 – 前頁の2つのチェックポイントのとり方による差はほと んどない 12 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 13 概要 • 半順序簡約(Partial Order Reduction)の新しい手法 の提案 – POR • モデル検査における主要な状態削減手法 – SPIN、LTSAなどのモデルチェッカーで実装 • 互いに依存していない並行トランジションがある場合に、検証に 必要なものだけを考慮 a 1 b [c = 1] t1 2 c 1 t2 [a = 1 & b = 2] t3 2,1,1 t2 2 t1 1 1,1,1 2 1,2,1 t1 t2 2,2,1 t3 1,2,2 14 Partial Order Reduction • 各状態で検証に必要なトランジションだけを 考慮 • どのトランジションを選ぶかが重要 正しい簡約 t1 t2 全体の遷移系 t1 1,1,1 t2 t2 2,1,1 t1 2,2,1 t3 誤った簡約 1,2,1 t2 t1 t3 1,2,2 t1 t2 t2 t1 t3 15 提案手法LPOR (Local POR) • 単純な遷移選択方法 – トランジションのローカルな情報だけで選択 – 言語、フォーマリズムに容易に適用可能 • 論文では分散システムのモデルへ適用 • 保存される性質 – デッドロック – インバリアント (詳細はテクニカルレポート) – 時相論理CTL*_x (詳細はテクニカルレポート) 16 実験と結果 • MP-Basset モデルチェッカーに適用 – 著者らによるJPFベースのモデルチェッカー • 3種類のフォールトトレラント分散アルゴリズムに 適用 – プロセス数 5~7 • 結果 – 何もしない場合に比べて大幅に状態数・時間を削減 (90%に達する場合も) – Dynamic POR(別手法)よりも、モデルにエラーがない 場合(全探索が必要な場合)は高速 17
© Copyright 2024 ExpyDoc