計算機言語システム論 10/02 論文サーベイ 吉野　寿宏 (米澤研究室 D1)

今回の論文 M. Naik, A. Aiken, J. Whaley. Effective Static Race Detection for Java. PLDI ’06. Race detection を行うシステム Chord を実装した http://www.stanford.edu/~mhn/chord.html にて入手可 Chord を用いて実際のアプリケーションの race condition を発見し、バグの修正につながった

背景: Race Detection Race (競合) とは何か？ Race はバグの元である マルチスレッドのプログラムが同一のメモリ領域に対して同時に(同期なしに)参照を行うこと しかも少なくとも一つが書き込みアクセスである ような場合 Race はバグの元である プログラムの invariant (常に成り立っているべき 条件)を壊すおそれがある スケジューリングなどの状況により発生し、再現が難しい

2 スレッドがConnection を持ってしまう！ An Example of Race JdbF からの例 public class ConnectionSource { private Connection conn; private boolean used; 　　 public Connection getConnection() throws SQLException { if (!used) { used = true; return conn; } throw new SQLException(...); }; ロックをかけていない スレッド 1　　　　2 2 スレッドがConnection を持ってしまう！

既存研究 (1) 動的な検出 既存研究の多くはほとんどこちらの手法 Happens-before relation[L. Lamport 1978] 時間順に起こらなければならない制約を表す半順序 False negative が非常に多い(検出精度が悪い) Lockset algorithm スレッドの保持しているロックを動的に管理 lock/unlock 以外の同期手法を使うと false positive が出る

既存研究 (2) 静的な検出 本論文はこちらの手法に分類される 型検査器によるシステム モデル検査器によるシステム 同期に関する挙動を型などで表す方式 しかし型を自動的に推論することは非常に難しい モデル検査器によるシステム Path sensitive な解析をするのでさまざまな同期機構に対応できる しかし open program には対応できない 静的 Lockset algorithm

Static Race Detection はどうあるべきか？ 5 つの指標を掲げている 正確さ False positive (誤検知) の確率は十分に低いか？ スケーラビリティ 大規模なプログラムも現実的な時間で解析できるか？ 幅広い同期機構への対応 現実に用いられている同期機構に対応できるか？ それ自身で閉じていないプログラム(ライブラリや デバイスドライバ等)への対応 (デバッグのための)反例生成の枠組み

Chord 中核は k-object sensitivity[Whaley, Lam 2004] による エリアス解析 BDD (Binary Decision Diagram) を用いて効率化 bddbddb[Lam, Whaley 2005] による実装 全体として 4 つのステージ Reachable-/Aliasing-/Escaping-/Unlocked-Pairs Computation いずれも実行箇所のペア(別スレッドで同時に実行される箇所を抽出したいことに注意)を扱う 各ステージで、race にならないものを枝狩りしていく Flow-insensitive な解析 ⇒ Unsound な手法 False positive/false negative が出る可能性がある

Chord: システム構成図

Open Program の扱い それ自体では完結しないプログラムは、補完してから検証の必要がある ライブラリ等は、自身がどのように呼び出されるかわからない (missing caller) テスト用の harness を生成してやる必要 またプログラムが依存するライブラリの挙動が不明な場合もある (missing callee) Java の native method など Chord では一部をモデル化し、それ以外は nop と等価として扱っている (このあたりも unsoundness の要因)

Test Harness Synthesis プログラムを解析するにあたって、エントリ ポイント(main)を自動生成 チェックしたいインターフェイス(I とする)に含まれるメソッドの引数をローカル変数として準備 参照型の変数に、非決定的に同じ型の値を代入 I のそれぞれのメソッドを、上で準備した値を用いて非決定的に呼び出し、結果を型の合う変数に代入 詳細は後ほど例を出します

Synchronization Idioms Java にはいくつかの同期手法がある synchronized(expr) { … } 自然に扱うことができる fork/join synchronization Flow sensitive な(プログラムの場所を考慮する)解析が必要 Chord は flow insensitive なので、ユーザが annotation をつけてやる必要がある オブジェクトのモニタ (Object#wait/notify) あまり重要ではない、と著者らは書いている

Stage 1: Reachable-Pairs Computation

Original-Pairs Computation まず最初に、プログラムの中で同じ変数を 使う可能性のある場所をすべて列挙する インスタンス変数 f、static 変数 g、配列 a への read/write アクセスを行う場所の組 Soot framework[R. Vallée-Rai et al. 1999] により求める インスタンス変数は、同一インスタンスの中のみを考慮すればよい しかしこれはものすごく大雑把な解析 ⇒ 後段の解析により refine していく

Original-Pairs Computation

Original-Pairs Computation: 例 public class A { int f; public A() { this.f = 0; } private int rd() { return this.f; } private int wr(int x) { this.f = x; return x; } public int get() { return this.rd(); } public synchronized int inc() { int t = this.rd() + (new A()).wr(1); return this.wr(t); } write read OriginalPairs = {(fr, fw), (fw, fw), (fr, f’w), (f’w, f’w), (fw, f’w)}

Reachable-Pairs Computation プログラムのエントリポイントから到達可能でなければ race は起こらない Race を起こす組は、main からどこかスレッドを 立ち上げる箇所を経由して到達可能なはず 到達可能性により Original-Pairs を枝狩り コールグラフ(呼び出し-呼び出されの関係をグラフにしたもの)の解析による

Call Graph 遷移関係の定義 →n、⇒n も帰納的に定義できる 　　は call site と context から、そこで呼ばれる メソッドと context の組を与える関数 Ifork は、スレッドを立ち上げる(thread-spawning) call site の集合 → と ⇒ の違いは、スレッドの起動が起こりうるかどうか →n、⇒n も帰納的に定義できる

Computation of Reachable Pairs Call Graph の関係(の反射推移閉包)を 用いて、次のように計算される 　　は main から到達可能な thread-spawning call site とコンテクストの集合 　　 は call site (またはメモリアクセス)からそれが含まれるメソッドを返す関数 ReachablePairs が求める集合

Reachable-Pairs Computation: 例 public class A { public int get() { return this.rd(); } public synchronized int inc() { int t = this.rd() + (new A()).wr(1); return this.wr(t); } static public void main() { A a; if(*) a = new A(); if(*) a.get(); if(*) a.inc(); Test Harness コンストラクタの race は検出しないので消える ReachablePairs = {(fr, fw), (fw, fw), (fr, f’w), (f’w, f’w), (fw, f’w)}

Reachable-Pairs Computation: 例 public class A { public int get() { return this.rd(); } public synchronized int inc() { int t = this.rd() + (new A()).wr(1); return this.wr(t); } static public void main() { A a; if(*) a = new A(); if(*) a.get(); if(*) a.inc(); ReachablePairs = {(fr, fw), (fw, fw), (fr, f’w), (f’w, f’w), (fw, f’w)} ReachablePairs = {(fr, fw), (fw, fw), (fr, f’w), (f’w, f’w), (fw, f’w)} ReachablePairs = {(fr, fw), (fw, fw), (fr, f’w), (f’w, f’w), (fw, f’w)}

Stage 2: Aliasing-Pairs Computation

Aliasing-Pairs Computation 同じ変数実体に同時にアクセスしていない限り race は起こらない あるオブジェクトの異なるインスタンスにある同一名の変数 エリアスしていない配列へのアクセス エリアスしていてもインデックスが異なれば race にはならないが、ここでは保守的にインデックスは省いて考えている Reachable-Pairs として計算されたものから エリアス解析により枝狩り k-object sensitive alias analysis[Milanova et al. 2002] の手法をここでは用いる Flow insensitive, context/object/field sensitive analysis Inclusion-base analysis

エリアス解析 (Alias Analysis) オブジェクトへの参照が同じ場所を指して いるかどうかを静的に解析する手法 参照 = ポインタ(C, C++)、参照(C++, Java, C# ...) たとえば、次のコードは安全か？ void swap(int* x, int* y) { *x ^= *y ^= *x ^= *y; } x == y だったら *x も *y も 0 になってしまう！ そうならないことを保証するために、エリアス解析が有効

Stage 3: Escaping-Pairs Computation

Escaping-Pairs Computation 複数のスレッドに共有されていないデータは race を引き起こさない Aliasing-Pairs をさらに枝狩りできる データ共有のためには 2 つの場合がある メソッド呼び出し(thread-spawning)における引数 explicit な呼び出し(java.lang.Runnable#start) implicit な呼び出し(main から) オブジェクトのフィールドとしての共有

Stage 4: Unlocked-Pairs Computation

Unlocked-Pairs Computation (共通の)ロックをとっている組は race を引き起こさない Call graph と alias analysis から導出できる しかし計算量等の観点から、いくつか unsound な仮定が必要になる 次で説明

Unlocked-Pairs Computation UnlockedPairs’’ ⊆ UnlockedPairs’ になっている (証明済) つまり、false positive が出る可能性がある May-alias の解析しかしていない 「正しく」やるためには、must-alias (True と判断された場合は必ず alias)の解析が必要 ⇒ Chord が race-free と結論づけた場合でも、ひょっとすると別のオブジェクトに対して同期しているかもしれない False negative が出る可能性がある しかし実験中にそのような不都合は起きなかった、とのこと

後処理 最後まで残った変数アクセスの組を race の可能性があるものとして報告 そこに至るまでのパスを反例として出力 どの変数、またはオブジェクトが race を起こして いるのかを表示する しかし最終的に本当のバグによるものかを 判断するには人手が必要

Unlocked-Pairs Computation: 例 public class A { int f; public A() { this.f = 0; } private int rd() { return this.f; } private int wr(int x) { this.f = x; return x; } public int get() { return this.rd(); } public synchronized int inc() { int t = this.rd() + (new A()).wr(1); return this.wr(t); } inc() は synchronized メソッドなので、同時に到達することはない Escaping-Pairs = {(fr, fw), (fw, fw)}

Chord の評価実験 実際に広く使われているプログラムを検証

実験結果 (1) 速度 アノテーションはほとんど 必要なかった 646KLoC を 30 分弱で検査完了 大規模プロジェクトでも使用に耐える 手動でつけてもそれほど 苦にはならない

実験結果 (2) 発見された race 実際開発者に報告して修正がされたケースも False alarm が出ている箇所はさほど多くない Apache commons-pool における 17 箇所のバグの指摘に対し、実際に 5 箇所に修正パッチが出た

まとめ 静的解析により race を見つけ出すための 画期的な手法を提案した bddbddb を用いてシステムを実装した 広く使われている(マルチスレッド)プログラムを 用いてベンチマークを行った かなり巨大なプログラムでも現実的時間内で解析可能であることが確かめられた False positive の数が少ないことが確かめられた 実際にバグの解決に役立った事例もある