A05

ASE2011
Session05: Analysis, Verification and Validation
1. Scalable and Precise Symbolic Analysis for Atomicity
Violations
2. DC2: A Framework for Scalable, Scope-Bounded Software
Verification
3. Formalizing HW/SW Interface Specifications
4. Safe Asynchronous Multicore Memory Operations
担当者：横川智教 (岡山県立大学)
12/03/21
FSE/ASE2011勉強会
1
A05-1
Scalable and Precise
Symbolic Analysis for
Atomicity Violation
Malay K. Ganai
(NEC Labs America)
12/03/21
FSE/ASE2011勉強会
2
Background
コンカレントシステムにおけるバグの原因の45.7％は
原子性(Atomicity)の違反に関するもの [1]
バグの原因
割合(件数)
Atomicity violation
45.7%(48)
Deadlocks
29.5%(31)
Order violation
22.8%(24)
Others
2.0%(2)
原子性の違反を検出するツールBESTの開発
[1] S. Lu et al., “Learning from mistakes: A comphrensive study on real world
concurrency bug characteristics,” In Architectural Support for Programming
Languages and Operating Systems, 2008.
12/03/21
FSE/ASE2011勉強会
3
BEST(Binary instrumentation-based Error-directed Symbolic
Testing)
Target Binary
Test Harness
Stage2:Simplify CTM
• ローカル処理を合成
• 実行不能/冗長なコンテクス
トスイッチを削除
Stage1:Trace Generalization
• バイナリを実行し，メモリアクセス等
のイベントを記録
• Concurrent Trace Model(CTM)を作成
Stage3:Inferring Atomic Specification
• CTMからAtomic Regionを抽出
• atomicと証明済/non-atomicと既知のも
のを削除
• Atomic Propertyを生成
Stage4:Property-specific Symbolic Analysis
• Atomic Violation(NAV)とFeasible Schedule(Ωsched)を記号表現
• NAV∧Ωschedの充足可能性判定
12/03/21
FSE/ASE2011勉強会
Stage5:
Debug
Traces
4
Contributions
Generalization:
扱えるスケジュールに制約がない
Precision:
実行可能なスケジュールの全てかつそれのみを記号表現
Scalability:
CTMの簡単化により問題のサイズを削減
制約ベースの検証 → 明示的なスケジュールの列挙が不要
Feasibility:
Causal AtomicityやCausal Mutual Atomicityなどの
様々なAtomicity Propertyを検証することが可能
12/03/21
FSE/ASE2011勉強会
5
Evaluation
9種のマルチスレッドアプリケーション(C/C++/Java)
に対してBESTツールを適用
A. Atomicity Analysis (Tab. 4)
スレッド数に対する問題サイズの変化の測定
• 17個のバグを検出
• CAと比較して，CMAの検出コストは小さい
B. Reduction Step (Tab. 5)
削減手法の組み合わせに関する効果の測定
• 削減効果は大きい(最大で2×106倍)
• CAと比較して，CMAに関する削減の度合いが大きい
12/03/21
FSE/ASE2011勉強会
6
A05-2
DC2: A Framework for Scalable,
Scope-Bounded Software
Verification
Franjo Ivancic, Gogul Balakrishnan, Aarti Gupta
(NEC Labs America)
Sriram Sankaranarayanan
(University of Colorado)
Naoto Maeda, Hiroki Tokuoka, Takashi Imoto, Yoshiaki Miyazaki
(NEC Corporation)
12/03/21
FSE/ASE2011勉強会
7
Background
Software Model Checkingへの要求
Scalability:
1MLOC以上のソースコードが扱えなければならない
Performance:
与えられた時間内に検証を完了しなければならない
Accuracy:
誤検出が多くてはならない
ソフトウェア検証フレームワークDC2の開発
12/03/21
FSE/ASE2011勉強会
8
DC2(Depth-Cutoff with Design Constraints)
Scope bounding:
ネストの深い関数を排除することでモデルサイズを制限
Automatic specification inference:
関数の外部環境(グローバル変数，呼び出し等)の制約を推測
スタブ関数の推測
プログラム解析ツールSpecTackleの開発
Environment refinement:
反例を元に抽象モデルを詳細化
CEGER(CounterExample-Guided Environment Refineme
NECが開発したソフトウェア検証ツールVARVELの一部として実
12/03/21
FSE/ASE2011勉強会
9
Depth Cutoff in DC2
fun. f()
assume(pre_f)
call g1();
call g2();
fun. g1()
assert(pre_g1)
call h();
call h_stub();
fun. h()
…
fun. g2()
assert(pre_g2)
…
fun. h_stub()
assert(pre_h)
inferred stub
assume(post_h)
(本文Fig.3より抜粋)
12/03/21
FSE/ASE2011勉強会
10
Evaluation
A. DC2の適用 (Tab. 4)
DC2適用前後のSuccess Ratioと#Likely Bugsを測定
• 定められた期間で検証が完了した割合が増加
• 検出数の増加および誤検出の減少
B. CEGERの適用
Zister Benchmark (Tab. 6)
• 検出率が向上(7/90→10/13)
• 検出数も増加
Industrial Benchmark (Tab. 7)
• より少ない検出数でバグを発見
• 被験者は非専門家であったが効果があった
12/03/21
FSE/ASE2011勉強会
11
A05-3
Formalizing Hardware/Software
Interface Specifications
Juncao Li, Thomas Ball, Vladimir Levin, Con McGarvey
(Microsoft Corporation)
Fei Xie
(Portland State University)
12/03/21
FSE/ASE2011勉強会
12
Background
ドライバ(SW)とデバイス(HW)の依存性
ドライバを開発時にはデバイスが完成している必要がある
開発サイクルの長期化
HW/SWインタフェースのモデル化
ドライバ(SW)開発
Software
Inter
face
Hardware
デバイス(HW)開発
HW/SWを並行して開発することが可能
12/03/21
FSE/ASE2011勉強会
13
Contributions
Relative atomicity:
トランザクションの優先度を相対的な原子性として表現
Specification of HW/SW interface protocols:
仕様記述言語modelCを開発
C言語のセマンティクスに3つの制約(範囲付き整数，再帰
呼出回数の制限，動的メモリ割り当ての禁止)と2つの拡張
(Relative atomicityおよびnon-determinism)
Protocols coverage:
HW/SWインタフェースのプロトコルを厳密にモデル化
Application and evaluation criteria:
MODEL-DOC rationを始めとし，4つの評価基準を提示
12/03/21
FSE/ASE2011勉強会
14
Formal specification framework
atWritePortA()
atWritePortB()
Σ={{wr_a},{wr_b},{no_evt},..}
Output2PortA()
Output2PortB()
Isr()
Software
Model
(LPDS)
Hardware
Model
(BA)
atRun_DIO()
I={{intr},{no_intr},..}
RunIsr()
(本文Fig.5より抜粋)
12/03/21
FSE/ASE2011勉強会
15
Evaluation
提案するモデル4つの評価基準をもとに評価
Correctness assurance:
仕様の不整合をCコンパイラで検出
Manual effort:
仕様化するプロトコルの複雑さをドキュメントの規模を元に測
False positives:
over abstractionに起因する偽陽性
Comparison with the English specification:
モデルとドキュメントの関係解析のためMODEL-DOC ratioを導
モデルを記述するmodelCの行数
MODEL-DOC =
ドキュメントのページ数
12/03/21
FSE/ASE2011勉強会
16
A05-4
Safe Asynchronous Multicore
Memory Operations
Matko Botincan, Mike Dodds
(University of Cambridge)
Alastair F. Donaldson
(Imperial College London)
Matthew J. Parkinson
(Microsoft Reseach Cambridge)
12/03/21
FSE/ASE2011勉強会
17
Background
マルチコアシステムにおいて非同期メモリ操作は非常に重要な技
Cell，CUDA，OpenCLなどでも利用される
不正な非同期操作に起因するバグは検出・分析が非常に困難
ある環境では正しく動作し，他では重大な障害を引き起こす
形式的検証が必要とされる
マルチコアプログラムの安全性検証手法の提案
ツールasyncStarとしての実装
12/03/21
FSE/ASE2011勉強会
18
Contributions
マルチコアプログラムを対象としたプログラム論理の構築
スレッドのfork/joinと非同期メモリ操作を考慮
マルチコアプログラム論理の自動証明
SMTソルバの利用
ツールasyncStarの実装
Industrial Benchmarkによる評価
12/03/21
FSE/ASE2011勉強会
19
asyncStar
coreStar
Theorem prover
SMT solver
Abstraction
APRON
Symbolic execution
asyncStar
Pre/post conditions
Loop invariants
VMC program
(Verified Multicore C)
coreStarIL program
VMC frontend
(本文Fig.5より抜粋)
12/03/21
FSE/ASE2011勉強会
20
Evaluation
Cell Broadband Engine SDKのベンチマークを用いて評価
バグを含まないもの(Correct)と含むもの*(Buggy)に対して
asyncStarを適用した結果を測定
*Wait命令を取り除くことで作成
証明および反証は現実的な時間で終了(～8416秒程度)
要素数の変化は検証コストに影響を与えない
本質的なボトルネックではない
12/03/21
FSE/ASE2011勉強会
21

Download Report