Program Abstractions for Behaviour Validation

Presentation on theme: "Program Abstractions for Behaviour Validation"— Presentation transcript:

1 Program Abstractions for Behaviour Validation
FCEyN, UBA Guido de Caso FCEyN, UBA Victor Braberman Imperial College Diego Garbervetsky Imperial College Sebastian Uchitel 早稲田大学　鷲崎研究室　坂本一憲

2 Inrtoduction プログラムの振る舞いを検証するための抽象化 ソースコードと仕様を与えてモデルを自動生成
情報量が少ない仕様 エンジニアのメンタルモデル ソースコードと仕様を与えてモデルを自動生成 無限の状態に対応 比較的低コストで生成 エンジニアはモデルと仕様を比較してバグ発見

3 Overview 振る舞いモデルを自動抽出 状態遷移図のような モデル上で誤りを検出 S5：空，S7：非空，S0：解放済み
01 typedef struct node 02 { int data; struct node next; } node; 03 typedef struct list 04 { int size; node first; } list; list *l; int inv() { return l==NULL || 09 l->size >=0; } 10 int List() { 11 l = (list*) malloc(sizeof(list)); 12 i f (l == NULL) return 0; 13 l->size = 0; l->first = NULL; 14 return 1; 15 } 16 … 振る舞いモデルを自動抽出 状態遷移図のような モデル上で誤りを検出 S5：空，S7：非空，S0：解放済み S5 -> S0 に addで遷移がおかしい S7 -> S5 に戻れないのはおかしい

4 Enabledness Abstractions
関数にInvariantとRequires clausesを記述 契約プログラミングに おける不変/事前条件 幅優先探索によって 状態を探索 得られた状態が上記の条件を満たすか検査 満たす状態のみで構築 到達性をモデル検査でチェック

5 Evaluation Java PipedOutputStream Java Signature Java List Iterator
Javadocと比較 Java Signature Java List Iterator PCCR Framework SMTPProtocol 人手でおこしたモデルと比較

6 Programs, Tests, and Oracles: The Foundations of Testing Revisited (Distinguished paper)
University of Minnesota Matt Staats University of Minnesota Michael W. Whalen University of Minnesota Mats P.E. Heimdahl 早稲田大学　鷲崎研究室　坂本一憲

7 Inrtoduction Test oracleに関する形式的な土台を築く その上で，過去の研究を見直す Programs
プログラムの意味論は エラー伝搬を決定する オラクルはプログラムの観測点を限定する プログラムの構造情報は テストの選択を支援する プログラムは 仕様を実装する Specifications 仕様はテストの 選択を支援する オラクルは仕様を近似する Oracles テストは仕様とプログラムの相違点を検出 Tests

8 Extension of Gourlay’s framework
p：プログラム，s：仕様，t：テスト，o：Test oracle 「pがsを満たす => pがsを満たすとtで判断」 問題1：Test oracleを選択する余地がない パラメータp, s, tについてのみ議論可能 問題2： Test oracleについて言及がない 常にsを満たすと判断するTest oracle：上式が常に真 pがsを満たさないケースについて言及がない 完全性：「pがsを満たすとtで判断⇒oはpが正しいとtで判断」 健全性：「oはpが正しいとtで判断⇒pがsを満たすとtで判断」

9 Test oracle comparison
Power：Gourlay’s frameworkの定義を改良 要約：pが正しいと判断する程度が低いほど強い o1 >TS o2：o1はo2より強い i.e. o1(p, t) => o2(p, t) カバレッジの強さ：PROBBETTER [Weyuker et al.] C1 PB C2： C1の方がC2よりバグを検出する確率が高い 同様に， O1 PBTS O2を定義（TS：テスト集合） o1 >TS o2 => O1 PBTS O2 Test oracle同士の比較からメトリクスへ

10 Applications to previous work
Comparing Coverage Criteria Test oracleに言及せずカバレッジの強さを定義 Test oracleを変えれば発見可能な欠陥が変化 e.g. Assert文のないテストケース vs あるテストケース Mutation Testing Testとtest oracleの両方を評価 少ないtestで強いtest oracleで満たす場合も Testability Test oracleが検査する値に関するエラーの伝搬 Test selectionのみならずoracle selectionへ応用

11 RACEZ: A Lightweight and Non-Invasive Race Detection Tool for Production Applications
Tsinghua University Tianwei Sheng Google, Inc. Neil Vachharajani Google, Inc. Stephane Eranian Google, Inc. Robert Hundt Tsinghua University Wenguang Chen 早稲田大学　鷲崎研究室　坂本一憲

12 Inrtoduction and problem
Data races：並列プログラミングにおけるバグ 共有変数を複数のスレッドで読み書きする Race detectionの既存研究 静的な検出手法：False positiveが多すぎる ⇒現在は動的な検出手法が主流 問題1：検査時間（最新研究でも元より28%増加） 実際に稼動しているサーバーへの適用が困難 問題2：侵略的（Invasive） コード埋め込みによりコードサイズが2倍増加

13 Solution(S) and contribution(C)
検出手法: lockset algorithm S1: 検査するコード位置（メモリアクセス）をサンプリング S2: Performance monitoring unit(PMU)の利用：世界初 C1: 検出と検出通知のタイミングのずれへの対処 C2: 検査位置が離散的と，偏ったサンプリングへの対処 2行目をサンプリングによって PMUが情報収集する場合 01: Lock(排他制御) 02: shared_memory = 1; 03: Unlock (排他制御) 04: other = 1; 連続的に 情報収集 離散的に 情報収集 ×悪いケース： 検査したタイミング 以外でPMUが通知 ○良いケース ： 検査したタイミング でPMUが通知 既存手法（非PMU） 提案手法（PMU）

14 Detection in detail 排他制御（コード挿入）とメモリアクセス（PMU）を検知
同アドレスに排他制御外で複数スレッドからアクセス⇒警告 サンプリング周波数の自動調整：パフォーマンス向上 C1: 検出と検出通知のタイミングのずれへの対処 Lock/Unlock（排他制御）の直前にNOPを挿入 C2: 検査位置が離散的と,偏ったサンプリングへの対処 アセンブリを解析して情報収集した周辺について調査 mov %rcx,0x38(%rax); mov 0x28(%rdx),%rcx; mov %rcx,0x40(%rax) 片方のアドレスが分かればもう片方も解析可能

15 Data raceを発見可能な サンプリング位置
Evaluation サンプル周波数：200,000 周波数×数 = メモリアクセス数 Data raceを発見可能な サンプリング位置 Bugs サンプル数 検出結果（確率） メモリ アクセス1 メモリ アクセス2 Base OS Sample Offline Ext. Extend Test 10,000 1% 4% 7% 1 3 httpd-1 80,000 3% 5 httpd-2 6% httpd-3 X httpd-4 8,000 5% 2 httpd-5 6,000 2% 10 mysqld-1 20,000 9% 18 mysqld-2 0% 6 mysqld-3 mysqld-4 4 mysqld-5 8%