--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/presentation/slide.md	Tue Jul 26 17:33:52 2016 +0900
@@ -0,0 +1,205 @@
+title: Continuation based C を用いたプログラムの検証手法
+author: 比嘉健太
+profile: 琉球大学 大学院 理工学研究科
+lang: Japanese
+
+# 研究目的
+* ソフトウェアの信頼性を向上させたい
+* ソフトウェアが仕様を常に満たすことを保証することで信頼性を確保する
+* 特に動作するソフトウェアを検証したい
+* 計算を拡張するメタ計算として検証機構を導入し、ソフトウェアの記述を変更せずに検証を行なう
+
+# 研究内容
+* Code Segment と Code Segment を用いるプログラミングスタイルを提案する
+* Code Segment とは処理の単位であり、相互に接続することでプログラムを構成していく
+* メタ計算による処理の拡張は接続部分に Meta Code Segment を挟むことで実現できる
+* Continuation based C 言語で記述された赤黒木を検証していく
+
+# Code Segment
+* Code Segment は処理の単位
+* ループを含まないシンプルな処理のみを単一 Code Segment で行なう
+* Code Segment どうしを接続することで複雑な処理も実現できる
+* 依存のない Code Segment どうしは並列に実行することが可能
+
+# Data Segment
+* Data Segment はデータの単位
+* Code Segment は入出力である Input Data Segment と Output Data Segment を持つ
+* Code Segment 内部で扱うデータは Data Segment に格納される
+* Output Data Segment は次の Code Segment の Input Data Segment
+* TODO: figure of code segments
+
+# Meta Computations
+* 計算を実現する計算をメタ計算とする
+* メモリ管理や例外処理、並列実行など
+* 一つレベルが上の計算と考える
+* ノーマルレベルとメタレベル
+* ノーマルレベルの計算を保存するメタ計算を定義して、プログラムを変えずに全体の挙動を変える
+* 例:
+    * 直列に実行される想定でプログラムを記述する
+    * 並列に実行するメタ計算で拡張する
+    * ノーマルレベルのプログラムを変更せずに並列で動作するプログラムになる
+
+# Meta Code Segment
+* メタ計算は Code Segment と Code Segment の間に Code Segment を入れることで追加できる
+* Code Segment に対する Meta Code Segment
+* Code Segment に必要な Data Segment を用意したり
+* メモリ管理の例:
+    * Code Segment に必要な変数にメモリを割り当て、 Code Segment に Data Segment として渡す
+    * ノーマルレベルの Code Segment からはポインタが見えないのでポインタに由来するバグを減らせる
+
+# Meta Data Segment
+* Meta Code Segment に必要なデータを格納する
+* Data Segment を内包する Data Segment
+* メモリ管理の例:
+    * Data Segment は Code Segment に必要な変数を持つ
+    * Meta Data Segment は変数の割り当てに使用可能なメモリアドレスを保持
+* メモリのアロケータの変更が容易
+
+# Continuation based C (CbC)
+* Code Segment と Data Segment をサポートした言語
+* 関数呼び出しは末尾のみ、の制約を持ったC言語
+    * goto で飛んで戻ってこない
+    * C とアセンブラの中間のようなもの
+* 組込みシステムの記述やOSの記述を目的としている
+
+# Example of Code Segment in CbC
+* Code Segment は ``__code`` を付けた関数
+* 次の Code Segment への接続は ``goto`` で表される
+
+```
+__code addTen(int a) {
+    int b = a+10;
+    goto twice(b);
+}
+
+__code twice(int x) {
+    int y = 2*x;
+    goto showValue(y);
+}
+```
+
+# Example of Data Segment in CbC
+* 各 Code Segment で使うデータの構造体の共用体
+
+```
+union Data {
+    struct Count {
+        int x;
+    } count;
+    struct Port {
+        int port;
+    } port;
+};
+```
+
+# Meta Computation in Continuation based C
+* メタ計算は Code Segment の間に挟まれた Code Segment で行なう
+* 例は Data Segment を指定する Meta Code Segment `twice_stub`
+* ノーマルレベルからはポインタは見えないものとする
+
+```
+// Code Segment
+__code addTen(union Data* ds, int a) {
+    int b = a+10;
+    goto twice_stub(ds);
+}
+
+// Meta Code Segment
+__code twice_stub(union Data* ds) {
+    goto twice(ds->count.x);
+}
+
+// Code Segment
+__code twice(int x) {
+    int y = 2*x;
+    goto showValue(y);
+}
+```
+
+# Meta Computation Hook in CbC
+* 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);
+    }
+}
+
+// Code Segment
+__code addTen(struct Context* context, int a) {
+    x = x+10;
+    goto meta(context, Twice);
+}
+
+// Code Segment
+__code twice(struct Context* context, int x) {
+    x = x*2;
+    goto meta(context, ShowValue);
+}
+```
+
+# Verification Method of Programs Using Continuation based C
+* メタ計算として検証機構を導入する
+* 仕様は CbC で記述し、恒真の式として定義する
+* 仕様を満たさない Input Data Segment が無いかチェックしていく
+* 検証の対象として CbC で記述された赤黒木を用いる
+
+# Red-Black Tree
+* 赤黒木とは木構造のデータ構造
+* 各ノードに赤と黒の色を割り当て、その色を用いて木のバランスを取る
+* 赤黒木の条件:
+    * 各ノードは赤または黒の色を持つ
+    * ルートの色は黒である
+    * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことはない)
+    * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である
+
+# Verification of Red-Black Tree
+* 仕様: 最も長い経路は最も短い経路の高々2倍に収まる
+* どのような順番で要素が挿入されても常に仕様が満たされることを確認する
+* 仕様を満たさないような挿入順番があればそれを表示する
+* 木への挿入は有限の個数だけ行なわれる
+
+# Verification Library Akasha
+* CbC のメタ計算として高さをチェックしていく
+* 深さ優先探索で挿入順番を総当たりでチェック
+* Data Segment に木が入っている
+* Meta Data Segment に挿入順番や実行履歴を記憶させる
+
+# C Bounded Model Checker
+* ANSI-C の記号実行モデルチェッカ
+* CbC は `__code` を `void` に、`goto` を `return` に変えると C Syntaxになる
+* Red-Black Tree を C に変換して検証
+* 挿入順番は非決定的な入力 `nondet_int` を使う
+
+# Result of Verification
+* CbC のメタ計算 Akasha では要素数13個までチェックできた
+* CBMC ではチェックできなかった
+* TODO: 表でまとめておく
+
+# Conclusion and Future Works
+* CBMC では検証できない範囲の検証を行なうことができた
+* 動作するプログラムの記述を変更することなく検証を行なえた
+* 今後の課題
+    * 挿入だけでなく削除を含む赤黒木の仕様検証
+    * 状態の抽象化による探索の効率化
+    * ポインタへの不正アクセス検出などのプログラムに依存しない仕様チェック機能
+
+<!-- vim: set filetype=markdown.slide: -->