Mercurial > hg > Papers > 2016 > atton-ipsjpro
view presentation/slide.md @ 55:3d80db3be1b6
Update slides
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 04 Aug 2016 18:46:58 +0900 |
| parents | a0bffeced069 |
| children | c361708587eb |
line wrap: on
line source
title: Continuation based C を用いたプログラムの検証手法 author: 比嘉健太 profile: 琉球大学 大学院 理工学研究科 情報工学専攻 lang: Japanese # ソフトウェアの実装の信頼性の向上 * ソフトウェアの信頼性を向上させたい * 信頼性を向上させる手法には証明、モデル検査、テストなど様々な手法がある * ソフトウェアが定められた仕様を常に満たすか確認することで信頼性を保証する * 計算を拡張するメタ計算として検証機構を導入し、ソフトウェアの実装コードの検証を行なう # ソフトウェアの信頼性向上手法 * assert * 実行プログラム上で仕様が満たされているかチェックする * 網羅的にテストできない * ユニットテストと組み合わせて使う * 検証の計算システムで実行する(メタ計算) * Java Path Finder, Valgrind * 大規模システムは実行できない # ソフトウェアの信頼性向上手法 * アルゴリズムの正しさを証明する * Agda, Coq, Idris といった証明支援系でプログラムを記述する * 極めて難しい * 実装に対して適用できない * ソフトウェアの仕様を記述し、その反例が無いかをチェックする * Spin, NuSMV, CBMC といったモデルチェッカ * モデル検査用に特化した言語で実装を記述する必要がある # Akasha の目的 * 実装言語そのものを検査する * 実装に入り込むバグをする * 単語の打ち間違いによるバグ * 高速かつ網羅的に検査する * メタ計算の切り替えで様々な検証を行なう * 高速なメタ計算が行なえる言語(CbC) を用いる # Continuation based C (CbC) * 当研究室で開発している言語 * Code Segment, Data Segment という単位でソフトウェアを記述する * 関数呼び出しは末尾のみ、の制約を持ったC言語 * スタックは持たない * goto で飛んで戻ってこない * 保持すべき状態が明示的になっている * メタ計算は goto の間に計算を挟むことで実現できる # Code Segment and Data Segment * Code Segment は入出力である Input Data Segment と Output Data Segment を持つ * 単一 Code Segment はシンプル(purely functional)な処理のみを行なう * Code Segment どうしを接続してソフトウェア全体を構築していく * 依存のない Code Segment どうしは並列に実行することが可能 {:width="50%"} # Example of Code Segment in CbC * Code Segment は `__code` を付けた関数 * 次の Code Segment への接続は `goto` で表される ``` __code addTen(struct Count c) { struct Port p; p.port = c.x+10; goto twice(p); } __code twice(struct Port p) { p.x = p.x*2; goto showValue(p); } ``` # CbC のメタ計算 * Code Segment 間の接続はメタ計算レベルで行なわれる * Code Segment で使われる Data Segment は Meta Data Segment である Context に全て定義されている * ポインタの扱いや並列実行はメタ計算レベルで行なう * メタ計算も Code Segment と Data Segment で表現される * メタレベルではポインタを扱っても良い {:width="50%"} # CbC のメタ計算の実際 * プログラムで使用する Data Segment は Meta Data Segment で全て定義されている ``` union Data { struct Count { int x; } count; struct Port { int port; } port; } struct Context { union Data *data; // Data Segment unsigned int gotoCount; // メタ計算に必要なデータ unsigned int stepOfAddTen; }; ``` # CbC のメタ計算の実際 * Meta Code Segment では Data Segment は struct Data という形で一様に処理される * メタ計算と通常の計算は stub と meta によって接続される ``` __code addTen_stub(struct Context* context) { goto addTen(context, context->data[Count]); } __code addTen(struct Context* context, struct Count c) { struct Port p; p.port = c.x+10; goto meta(context, Twice); } __code twice_stub(struct Context* context) { goto twice(context, countext->data[Port]); } __code twice(struct Context* countext, struct Port p) { p.x = p.x*2; goto meta(context, ShowValue); } ``` # CbC のメタ計算の実際 * デフォルトの meta * meta を変更することで平行計算や例外処理やソフトウェア検証を行なう ``` __code meta(struct Context* context, enum Code next) { goto (context->code[next])(context); } ``` # Meta Code Segment を使った実際の検証 * goto する時に必ず通る Meta Code Segment `meta` を作る * `meta` を切り替えることでノーマルレベルの計算を拡張する ``` // Meta Data Segment struct Context { union Data *data; // Data Segment unsigned int gotoCount; // メタ計算に必要なデータ unsigned int stepOfAddTen; }; // Meta Code Segment __code meta(struct Context* context, enum Code next) { countext.gotoCount++; /* 接続時に行なうメタ計算を記述 */ switch (next) { case AddTen: // 特定のCode Segmentへのメタ計算 context.stepOfAddTen++; goto addTen_stub(context); case Twice: goto twice_stub(context); } } ``` # Verification Method of Programs Using Continuation based C * メタ計算として検証機構を導入する * 仕様はCbCで記述する * どのような状態でも成り立つべき式として定義 * 仕様を満たさない Input Data Segment が無いかチェックしていく * 検証の対象として CbC で記述された赤黒木を用いる # Red-Black Tree * 赤黒木とは木構造のデータ構造 * 赤黒木の条件: * 各ノードは赤または黒の色を持つ * ルートの色は黒である * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことはない) * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である * 仕様: 最も長い経路は最も短い経路の高々2倍に収まる {:width="35%"} # Verification Library Akasha * 本研究で作成した検証用メタ計算ライブラリ * 実装コードの `meta` を上書きするだけで検証を行なうことができる * どのような順番で要素が挿入されても常に仕様が満たされることを確認する * 仕様を満たさない挿入順番があればそれを表示 * 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙 * 挿入後の木はきちんとバランスしているかチェックする * CbC のメタ計算 Akasha では要素数13個までチェックできた * 実装にわざとバグを入れた場合にはバランスしない入力例を返した # C Bounded Model Checker * Carnegie Mellon University で開発されている記号実行モデルチェッカ * C, C++, Java に対応 * CbC は `__code` を `void` に、`goto` を `return` に変えると C Syntaxになる * コードを C に変換して検証 * 挿入順番は非決定的な入力 `nondet_int` を使う * 関数呼び出しやループは展開される * 展開可能な最大数まで展開しても赤黒木の仕様を検証できず # Conclusion * 動作するプログラムの記述を変更せず検証を行なえた * テストケースの自動生成+仕様の反例表示ができた * CBMC では検証できない範囲の検証を行なうことができた * 総当たりでチェックしているため扱えるサイズは小さい * CBMC に比べ高速 * ポインタアクセスに由来するバグなどは見付けられない # Comparison of tools | | akasha | cbmc | unit test | Spin | 証明 | JavaPathFinder | valgrind | |------------------------|:----------:|:--------------:|:----------:|:------------:|:------------:|:---------------:|:--------:| | 検証用に実装の変更 | 必要なし | 必要なし | 必要なし | 別に記述 | 別に記述 | 必要なし | 必要なし | | 検証用に記述する言語 | 実装と同じ | 実装とほぼ同じ | 実装と同じ | 実装と異なる | 実装と異なる | 必要なし | 必要なし | | 仕様の検証 | 可能 | 可能 | 不可能 | 可能 | 可能 | 不可能 | 不可能 | | メモリリークなどの検出 | 不可能 | 可能 | 不可能 | 不可能 | 不可能 | 不可能 | 可能 | | 状態の数え上げ | 可能 | 可能 | 不可能 | 可能 | 不可能 | 可能 | 不可能 | | 反例の表示 | 可能 | 可能 | 不可能 | 可能 | 不可能 | 不可能 | 不可能 | # Future Works * 挿入だけでなく削除を含む赤黒木の仕様検証 * 状態の抽象化による探索の効率化 * ポインタへの不正アクセス検出などの機能 * CbC コンパイラに検証を行ないやすくする機構の導入 # CBMC Informations * CBMC 5.4 * 実行オプション * cbmc --unwind 1 * cbmc --depth 400 --property verifySpecification.assertion.1 * 赤黒木のCbC実装 * 赤黒木部分のみ: 330行 * スタックやメモリのアロケータなどを含める: 640行 # 他の言語でのメタ計算 * 計算を実現するような計算 * プログラムを生成するようなプログラム * TemplateHaskell in Haskell, Template in C++, Generics * コンパイル時メタプログラミング * 言語が特別な API を提供する * method_missing, define_method in Ruby * プログラムがその言語処理系の挙動を変える * reflection in Java * 副作用などの言語処理系に依存した処理を表現する * Monad in Haskell * CbC では関数呼び出しが存在していないのでメタ計算を挟むことが容易になっている <!-- vim: set filetype=markdown.slide: -->