Program Abstractions for Behaviour Validation FCEyN, UBA Guido de Caso FCEyN, UBA Victor Braberman Imperial College Diego Garbervetsky Imperial College Sebastian Uchitel 早稲田大学鷲崎研究室坂本一憲 Inrtoduction • プログラムの振る舞いを検証するための抽象化 – 情報量が少ない仕様 – エンジニアのメンタルモデル • ソースコードと仕様を与えてモデルを自動生成 – 無限の状態に対応 – 比較的低コストで生成 • エンジニアはモデルと仕様を比較してバグ発見 Overview 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 typedef struct node { int data; struct node next; } node; typedef struct list { int size; node first; } list; list *l; int inv() { return l==NULL || • 振る舞いモデルを自動抽出 l->size >=0; } int List() { – 状態遷移図のような l = (list*) malloc(sizeof(list)); • モデル上で誤りを検出 i f (l == NULL) return 0; l->size = 0; l->first = NULL; – S5：空，S7：非空，S0：解放済み return 1; – S5 -> S0 に addで遷移がおかしい } – S7 -> S5 に戻れないのはおかしい … Enabledness Abstractions • 関数にInvariantと Requires clausesを記述 – 契約プログラミングにおける不変/事前条件 • 幅優先探索によって状態を探索 • 得られた状態が上記の条件を満たすか検査 – 満たす状態のみで構築 • 到達性をモデル検査でチェック Evaluation • Java PipedOutputStream – Javadocと比較 • • • • Java Signature Java List Iterator PCCR Framework SMTPProtocol – 人手でおこしたモデルと比較 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 早稲田大学鷲崎研究室坂本一憲 Inrtoduction • Test oracleに関する形式的な土台を築く – その上で，過去の研究を見直す Programs オラクルはプログラムの観測点を限定するプログラムは仕様を実装する Specifications Oracles プログラムの意味論はエラー伝搬を決定するオラクルは仕様を近似するプログラムの構造情報はテストの選択を支援する仕様はテストの選択を支援するテストは仕様とプログラムの相違点を検出 Tests 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で判断」 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同士の比較からメトリクスへ 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へ応用 RACEZ: A Lightweight and NonInvasive 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 早稲田大学鷲崎研究室坂本一憲 Inrtoduction and problem • Data races：並列プログラミングにおけるバグ – 共有変数を複数のスレッドで読み書きする • Race detectionの既存研究 – 静的な検出手法：False positiveが多すぎる ⇒現在は動的な検出手法が主流 – 問題1：検査時間（最新研究でも元より28%増加） • 実際に稼動しているサーバーへの適用が困難 – 問題2：侵略的（Invasive） • コード埋め込みによりコードサイズが2倍増加 Solution(S) and contribution(C) 検出手法: lockset algorithm S1: 検査するコード位置（メモリアクセス）をサンプリング S2: Performance monitoring unit(PMU)の利用：世界初 C1: 検出と検出通知のタイミングのずれへの対処 C2: 検査位置が離散的と，偏ったサンプリングへの対処 2行目をサンプリングによって PMUが情報収集する場合 01: 02: 03: 04: Lock(排他制御) shared_memory = 1; Unlock (排他制御) other = 1; ×悪いケース：検査したタイミング以外でPMUが通知 ○良いケース：検査したタイミングでPMUが通知連続的に情報収集離散的に情報収集既存手法（非PMU）提案手法（PMU） Detection in detail • 排他制御（コード挿入）とメモリアクセス（PMU）を検知 • PMUによる解析：排他制御内か否か，メモリアドレス – 同アドレスに排他制御外で複数スレッドからアクセス⇒警告 • サンプリング周波数の自動調整：パフォーマンス向上 • C1: 検出と検出通知のタイミングのずれへの対処 – Lock/Unlock（排他制御）の直前にNOPを挿入 • C2: 検査位置が離散的と,偏ったサンプリングへの対処 – アセンブリを解析して情報収集した周辺について調査 mov %rcx,0x38(%rax); mov 0x28(%rdx),%rcx; mov %rcx,0x40(%rax) 片方のアドレスが分かればもう片方も解析可能サンプル周波数：200,000 周波数×数 = メモリアクセス数 Bugs サンプル数 Data raceを発見可能なサンプリング位置 Evaluation 検出結果（確率） Base OS Sample メモリアクセス1 Offline Ext. メモリアクセス2 Base Extend Base Extend Test 10,000 1% 4% 7% 1 3 1 3 httpd-1 80,000 1% 3% 4% 1 3 1 5 httpd-2 80,000 4% 4% 6% 1 3 1 3 httpd-3 80,000 X X X X X X X httpd-4 8,000 1% 3% 5% 1 2 1 2 httpd-5 6,000 2% 4% 4% 1 10 1 10 mysqld-1 20,000 2% 4% 9% 1 3 1 18 mysqld-2 20,000 0% 1% 1% 1 3 1 6 mysqld-3 20,000 X X X X X X X mysqld-4 10,000 1% 2% 3% 1 4 1 4 mysqld-5 10,000 3% 6% 8% 1 6 1 6