J: Code Analysis J1: Partition-Based Regression Verification Marcel Böhme, Bruno C. d. S. Oliveira, Abhik Roychoudhury J2: Automated Diagnosis of Software Configuration Errors Sai Zhang, Michael D. Ernst J3: Detecting Deadlock in Programs with DataCentric Synchronization Daniel Marino, Christian Hammer, Julian Dolby, Mandana Vaziri, Frank Tip, Jan Vitek 情報処理学会 ソフトウェア工学研究会 国際的研究活動活性化WG ICSE’13 勉強会 ICSE’13勉強会 (2013年7月9日) 担当者： 野田 訓広@阿草研OB In Proc. of ICSE’13, pp.302--311. Outline 問題 • 全入力空間に対するRegression Verification(RV) は 時間・メモリが非常に多く必要で非実用的 提案 • 入力空間を分割①し，段階的に検証していく手法② (Partition-Based RV) を提案・実装③ (on JSlice) • テストケース生成の代替としても利用可能④ ①～④： Main Contributions 結果 • 既存手法よりも早くより多くのRegression Errorを 検出 • 長期間報告されなかったバグを即座に検出 J1: Partition-Based Regression Verification 3 Partition-Based RV ・RV： 全入力空間を検証 ・PRV： 入力空間を分割し段階的に検証 ・RT： 入力空間の特定の点に対し検査 同値空間は記号実行を基にした方法で計算． スライス・到達可能性・伝播状態などを 計算して，(1)同じ変更部分に到達するか (2)出力への影響が同じかを判定し求める． a. ランダムにテストケース選択・実行 b. 同値空間(differential partition)を計算 c. 隣接する空間のテストケースを選択・ 実行 d. b.に戻る 上図は “Böhne et. al., Partition-Based Regression Verification, In Proc. of ICSE‘13, pp.302-311” より引用 J1: Partition-Based Regression Verification 4 Experimental Evaluation 提案手法が関連手法よりもどれだけ有用かを評価 RQ1： Efficiency – Semantic Difference 41% 少ない時間で完了 21% 多くのregression differencesを検出 RQ2： Efficiency – Software Regression 5個のソフトウェア (20LOC～5,000LOC) 83個のバージョン 63% 少ない時間で完了 48% 多くのsoftware regression (≠semantic difference) を検出 RQ3： Practicability Apache CLIに対し，2ヶ月間も報告されなかったバグ を88秒で検出！ J1: Partition-Based Regression Verification 5 所感 Pros 実験結果が良い．関連研究と比較した際の有 用性がよく分かる． 実際に検出されづらいバグを検出できている (Apache CLIの例)点が良い． いかに良い例を見つけてくるかが重要？ 手法考案と例を見つけるのはどちらが先？ Cons Scalabilityについての議論は保留されている． 結局実用的なのか？ どのようなSemantic Difference/Software Regressionが見つかるのかよく分からない J1: Partition-Based Regression Verification 6 Automated Diagnosis of Software Configuration Errors Sai Zhang, Michael D. Ernst University of Washington, USA ICSE’13勉強会 (2013年7月9日) 担当者： 渥美 紀寿 (名古屋大学) In Proc. of ICSE’13, pp.312-321. 研究の目的と主要な貢献 目的 ソフトウェアの設定ミスによる不具合の原因を特定 特徴 テストオラクルが不要 クラッシュしている場合もしていない場合も自動的に 特定可能 主要な貢献 Java のソフトに対する診断ツールを実装 (http://config-errors.googlecode.com) 5つのソフトウェアに対する14の設定エラーに対して評 価したところ，根本の原因を上位に示すことができた J2: Automated Diagnosis of Software Configuration Errors 8 手法の概要 Configuration オプションの 値の設定からスライシング プログラム Configuration オプション エラー レポート 影響を 受ける 条件式 伝播解析 成功実行と大きく 異なる部分を検出 true と評価される 回数を計測するための コード埋め込み 計測 プログラム 実行 プロファイル 実行 エラー検出 成功実行における プロファイルを あらかじめ構築 原因となる Configuration オプションを Ranking プロファイル DB (成功実行) J2: Automated Diagnosis of Software Configuration Errors Configuration 入力 (エラー実行) 9 評価方法 対象 プロファイルDBの構築 ユーザマニュアル，FAQ，ML等から成功実行 既存技術との比較，利用技術の違い Randoop, Weka, JChord, Synoptic, Soot 5 non-crashing, 9 crashing ConfAnalyzer[1], Fault Localization (Tarantula[2], Daikon[3]), Slicing (Full Slicing, Thin Slicing) その他 確度，パフォーマンス [1] A. Rabkin and R. Katz. Precomputing possible configuration error diagnoses. In ASE, 2011. [2] J.A.Jones,M.J.Harrold,andJ.Stasko.Visualizationoftestinformation to assist fault localization. In ICSE, 2002. [3] M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. In ICSE, 1999. J2: Automated Diagnosis of Software Configuration Errors 10 評価結果 正しい実行におけるプロファイルに 大きく依存 既存技術との比較を 詳細に分析しているところが 論文の高評価に Fault Localiztion (Tarantula, Daikon) non-crashing では 原因を上位に出せた プロファイルが短かいので， うまくいかない 類似prof. / 全 prof. in DB Fig. 6. (S. Zhang, M. D. Ernst, Automated Diagnosis of Software Configuration Errors, In Proc. of ICSE’13, pp.312-321.) J2: Automated Diagnosis of Software Configuration Errors 11 Detecting Deadlock in Programs with Data-Centric Synchronization by Daniel Marino, Christian Hammer, Julian Dolby, Mandana Vaziri, Frank Tip, Jan Vitek @ ICSE 2013 ICSE’13勉強会 (2013年7月9日) 今井 敬吾 @ ITプランニング In Proc. of ICSE’13, pp.322--331. 概要 AJ (先行研究：Javaの並行拡張)：アトミックにアクセスすべきフィールド 群を宣言的に記述する atomic set 機能 (POPL’06, ICSE’08, ECOOP’10, TOPLAS’12, ICSE’13 ほか) AJ (Java+ atomic set) AJコンパイラは適切な位置に ロック命令を挿入した Javaのコードを生成する 競合が起こらない・データの一貫性を保持できる （オーバーヘッドも比較的小さい） compile lock Java （挿入したロックにより）デッドロックが起こってしまう… ⇒AJプログラムのデッドロックを検出する 型システム（というよりアノテーション＋プログラム解析アルゴリズム）を提案 J3: Detecting Deadlock in Programs with Data-Centric Synchronization 13 宣言的な同期制約 [1-3] AJ先行研究： tree1 Node root; int size; t atomic set t： rootとsizeにアクセスするメソッド呼び出し（ t のunit of workと呼ぶ）が （それらのアクセスに関して）アトミックになる The program code is from Fig. 2. of (D. Marino, et al., Detecting Deadlock in Programs with Data-Centric Synchronization, In Proc. of ICSE '13, pp. 322-331) J3: Detecting Deadlock in Programs with Data-Centric Synchronization 14 アトミックセットのエイリアス[1-3] AJ先行研究： tree1 Node root; int size; t root node1 Node left; Node right; n Aliasing annotation：複数のオブジェクトのアトミックセットを一つにする。 （単一のロックにより、tree1 と node1 の両方のフィールドが保護される） The program code is from Fig. 2. of (D. Marino, et al., Detecting Deadlock in Programs with Data-Centric Synchronization, In Proc. of ICSE '13, pp. 322-331) J3: Detecting Deadlock in Programs with Data-Centric Synchronization 15 検出可能なデッドロックの簡単な例 T 3 T 4 ② ② ① ① t tree1 t tree2 t < t (atomic set tのロックが循環する) デッドロック The program code is from Fig. 2 and Fig. 3. of (D. Marino, et al., Detecting Deadlock in Programs with Data-Centric Synchronization, In Proc. of ICSE '13, pp. 322-331) J3: Detecting Deadlock in Programs with Data-Centric Synchronization 16 貢献 AJのデッドロック検出アルゴリズムの提案と実装 ロックに半順序が付くことを示す、素朴なアルゴリズム AJのアノテーションはやや（かなり）重たいので、これくらいできて当然かも？ 再帰的データ構造を扱うためにアノテーション |a<this.a| をAJに追加 eclipseプラグイン(未公開)：WALAでCFG生成・データフロー解析 正当性の証明はごくインフォーマル([8]のtech. reportにある) 評価（解析対象のプログラム10個(一部公開)について） AJプログラムの修正はごくわずかで良い 2個：デッドロック誤検出を取り除くためのリファクタリング少し 1個：|a<this.a|のアノテーション4箇所 AJアノテーションは「筋が良い」か？わずかなアノテーションでデッドロックを検出できるならば良 いが、AJ自身に向き不向きがあるように思われる。例えば Java の collection フレームワークを AJ に書き換えるのに1ファイルあたり50近いエイリアスが必要（Table I参照）。他はそうでもない が… RQ3:実行時間は？→最大で75秒 (Core i5 1.8GHz RAM 4GB) J3: Detecting Deadlock in Programs with Data-Centric Synchronization 17 (補足)順序付けアノテーション |this.a<a| Node left; Node right; left n node1 right Node left; Node right; node2 Node left; Node right; n n node3 木全体をひとつのatomic setに属させる場合、子ノードのnを自身のnと 同じにすればよい The program code is from Fig. 2. of (D. Marino, et al., Detecting Deadlock in Programs with Data-Centric Synchronization, In Proc. of ICSE '13, pp. 322-331) J3: Detecting Deadlock in Programs with Data-Centric Synchronization 18 (補足)順序付けアノテーション |this.a<a| ノード毎に異なるatomic 細粒度lock:ノード毎に異なる set set にしたい atomic Node left; Node right; エイリアスを 削除 削除すると… left node1 right Node left; Node right; Error n node2 Node left; Node right; n n node3 left/right を全スレッドが同じ順でアクセスしていることを保証できない (デッドロックと判定される) The program code is from Fig. 2. of (D. Marino, et al., Detecting Deadlock in Programs with Data-Centric Synchronization, In Proc. of ICSE '13, pp. 322-331) J3: Detecting Deadlock in Programs with Data-Centric Synchronization 19 (補足)順序付けアノテーション |this.a<a| |this.n<n| Node left; Node right; 子ノードの atomic setは 自分より後に ロックする |this.n<n| left |this.n<n| |this.n<n| Ok n node1 right Node left; Node right; node2 Node left; Node right; n n node3 親→子の順にアクセスすることを保証できる The program code is from Fig. 2. of (D. Marino, et al., Detecting Deadlock in Programs with Data-Centric Synchronization, In Proc. of ICSE '13, pp. 322-331) J3: Detecting Deadlock in Programs with Data-Centric Synchronization 20
© Copyright 2024 ExpyDoc
