changeset 58:21c3332c2578

Update slides
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 05 Aug 2016 18:31:20 +0900
parents 728bbe91b6a2
children 1bd97f13e718
files presentation/slide.md
diffstat 1 files changed, 55 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/presentation/slide.md	Fri Aug 05 17:01:36 2016 +0900
+++ b/presentation/slide.md	Fri Aug 05 18:31:20 2016 +0900
@@ -15,7 +15,10 @@
     * 網羅的にテストできない
     * ユニットテストと組み合わせて使う
 * 検証の計算システムで実行する(メタ計算)
-    * Java Path Finder, Valgrind
+    * Java Path Finder
+        * JVM を切り替える
+    * Valgrind
+        * バイナリを動的解析
     * 大規模システムは実行できない
 
 # ソフトウェアの信頼性向上手法
@@ -24,7 +27,7 @@
     * 極めて難しい
     * 実装に対して適用できない
 * ソフトウェアの仕様を記述し、その反例が無いかをチェックする
-    * Spin, NuSMV, CBMC といったモデルチェッカ
+    * Spin, NuSMV といったモデルチェッカ
     * モデル検査用に特化した言語で実装を記述する必要がある
 
 # Akasha の目的
@@ -96,29 +99,30 @@
 ```
 
 # CbC のメタ計算の実際
-* Meta Code Segment では Data Segment は struct Data という形で一様に処理
+* Meta Code Segment では Data Segment は union Data という形で一様
 * メタ計算と通常の計算は stub と meta によって接続される
+    * stub では利用する Data Segment の指定などを行なう
 
 ```
 __code addTen_stub(struct Context* context) {
-    goto addTen(context, context->data[Count]);
+    goto addTen(context, &context->data[Count]->count);
 }
 __code addTen(struct Context* context, struct Count c) {
-    struct Port p;
-    p.port = c.x+10;
+    c.port = c.x+10;
     goto meta(context, Twice);
 }
 
 __code twice_stub(struct Context* context) {
-    goto twice(context, countext->data[Port]);
+    goto twice(context, &countext->data[Count]->count);
 }
-__code twice(struct Context* countext, struct Port p) {
-    p.x = p.x*2;
+__code twice(struct Context* countext, struct Count c) {
+    c.x = c.x*2;
     goto meta(context, ShowValue);
 }
 ```
 
 # CbC のメタ計算の実際
+* goto する時に必ず通る Meta Code Segment `meta` を作る
 * デフォルトの meta
     * Code Segment の接続先名から次に実行される Code Segment を決定する
 * meta を変更することで平行計算や例外処理やソフトウェア検証を行なう
@@ -130,10 +134,9 @@
 ```
 
 
-
 # Meta Code Segment を使った検証
-* goto する時に必ず通る Meta Code Segment `meta` を作る
 * `meta` を切り替えることでノーマルレベルの計算を拡張する
+    * `goto` した回数を数える
 
 ```
 // Meta Data Segment
@@ -160,7 +163,7 @@
 * 赤黒木とは木構造のデータ構造
 * 赤黒木の条件:
     * 各ノードは赤または黒の色を持つ
-    * ルートの色は黒である
+    * ルートと葉の色は黒である
     * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことはない)
     * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である
 * 仕様: 最も長い経路は最も短い経路の高々2倍に収まる
@@ -169,19 +172,20 @@
 
 # Verification Library Akasha
 * 本研究で作成した検証用メタ計算ライブラリ
-* 実装コードの `meta` を上書きするだけで検証を行なうことができる
 * どのような順番で要素が挿入されても常に仕様が満たされることを確認する
+    * 全ての順列組み合わせのテストケースを実行する
 * 仕様を満たさない挿入順番があればそれを表示
     * 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙
     * 挿入後の木はきちんとバランスしているかチェックする
 * CbC のメタ計算 Akasha では要素数13個までチェックできた
+    * 13の階乗で62億通りを1,2時間ほど
 * 実装にわざとバグを入れた場合にはバランスしない入力例を返した
 
 # C Bounded Model Checker
 * Carnegie Mellon University で開発されている記号実行モデルチェッカ
     * C, C++, Java に対応
 * CbC は `__code` を `void` に、`goto` を `return` に変えると C Syntaxになる
-    * コードを C に変換して検証
+    * 赤黒木のコードを機械的に置換で C に変換して検証
 * 挿入順番は非決定的な入力 `nondet_int` を使う
 * 関数呼び出しやループは展開される
     * 展開可能な最大数まで展開しても赤黒木の仕様を検証できず
@@ -192,27 +196,16 @@
 * CBMC では検証できない範囲の検証を行なうことができた
     * 総当たりでチェックしているため扱えるサイズは小さい
         * CBMC に比べ高速
-    * 有限の個数しか扱えない
+    * 記号実行しているわけではない
+        * 有限の個数しか扱えない
 * ポインタアクセスに由来するバグなどは見付けられない
 
-# Comparison of tools
-
-|                        | akasha         | cbmc           | unit test  | Spin         | 証明         | JavaPathFinder  | valgrind |
-|------------------------|:--------------:|:--------------:|:----------:|:------------:|:------------:|:---------------:|:--------:|
-| 検証用に実装の変更     | 必要なし       | 必要なし       | 必要なし   | 別に記述     | 別に記述     | 必要なし        | 必要なし |
-| 検証用に記述する言語   | 実装と同じ     | 実装とほぼ同じ | 実装と同じ | 実装と異なる | 実装と異なる | 必要なし        | 必要なし |
-| 仕様の検証             | 可能           | 可能           | 不可能     | 可能         | 可能         | 不可能          | 不可能   |
-| メモリリークなどの検出 | 不可能         | 可能           | 不可能     | 不可能       | 不可能       | 不可能          | 可能     |
-| 状態の数え上げ         | 可能           | 可能           | 不可能     | 可能         | 不可能       | 可能            | 不可能   |
-| 反例の表示             | 可能           | 可能           | 不可能     | 可能         | 不可能       | 不可能          | 不可能   |
-| 赤黒木の検証           | 有限個まで保証 | 検証できず     |            |              |              |                 |          |
-
-
 # Future Works
+* 状態の抽象化による探索の効率化
 * 挿入だけでなく削除を含む赤黒木の仕様検証
-* 状態の抽象化による探索の効率化
 * ポインタへの不正アクセス検出などの機能
 * 検証用APIを CbC コンパイラに導入
+* CBMC 側で検証できるよう赤黒木を書き換えて検証する
 
 # CBMC Informations
 * CBMC 5.4
@@ -234,5 +227,38 @@
     * reflection in Java
 * CbC では関数呼び出しが存在していないのでメタ計算を挟むことが容易
 
+# Red-Black Tree のコード例
+
+```
+__code insertCase2(struct Context* context, struct Node* current) {
+    struct Node* parent;
+    stack_pop(context->node_stack, &parent);
+
+    if (parent->color == Black) {
+        stack_pop(context->code_stack, &context->next);
+        goto meta(context, context->next);
+    }
+
+    stack_push(context->node_stack, &parent);
+    goto meta(context, InsertCase3);
+}
+
+__code insert2_stub(struct Context* context) {
+    goto insertCase2(context, context->data[Tree]->tree.current);
+}
+```
+
+# Akasha の検証コード例
+
+```
+__code verifySpecificationFinish(struct Context* context) {
+    if (context->data[AkashaInfo]->akashaInfo.maxHeight >
+        2*context->data[AkashaInfo]->akashaInfo.minHeight) {
+        context->next = Exit;
+        goto meta(context, ShowTrace);
+    }
+    goto meta(context, DuplicateIterator);
+}
+```
 
 <!-- vim: set filetype=markdown.slide: -->