title: Continuation based C を用いたプログラムの検証手法
author: 比嘉健太
profile: 琉球大学 大学院 理工学研究科 情報工学専攻
lang: Japanese

# ソフトウェアの実装の信頼性の向上
* ソフトウェアの信頼性を向上させたい
* 信頼性を向上させる手法には証明、モデル検査、テストなど様々な手法がある
* ソフトウェアが定められた仕様を常に満たすか確認することで信頼性を保証する
* 計算を拡張するメタ計算として検証機構を導入し、ソフトウェアの実装コードの検証を行なう

# ソフトウェアの信頼性向上手法
* アルゴリズムの正しさを証明する
    * Agda, Coq, Idris といった証明支援系でプログラムを記述する
    * TeX: アルゴリズムの証明をドキュメントとして記述している
* ソフトウェアの仕様を記述し、その反例が無いかをチェックする
    * Spin, NuSMV, CBMC といったモデルチェッカ
* テストデータを入力して正しい出力を返すか
    * ユニットテスト
* assert や型システム、検証用の実行処理系
    * Java Path Finder, Virtual VM, Valgrind

# ソフトウェアの実装を検証したい
* アルゴリズムの正しさが証明できても実装する際にバグが入ることがある
    * 単語の打ち間違いによるバグ
    * 同じアルゴリズムを検証と実装で二度記述する
    * 検証と実装で言語も違うことも
* 実際に動作するソフトウェアの実装をチェックしたい
    * 実装コードを変更せずに仕様を保証する
    * 実装部分と検証部分も同じ言語で記述したい

# Continuation based C (CbC)
* 当研究室で開発している言語
* 関数呼び出しは末尾のみ、の制約を持ったC言語
    * Tail Call を言語仕様として持つ
    * スタックは持たない
    * goto で飛んで戻ってこない
    * アーキテクチャに依存しないアセンブラ
    * C function を呼ぶこともできる
* 組込みシステムやOSの記述を目的としている
* Code Segment, Data Segment という単位でソフトウェアを記述する

# Code Segment: 処理の単位
* 単一 Code Segment ではループを含まないシンプルな処理のみを行なう
* Code Segment どうしを接続してソフトウェア全体を構築していく
* 依存のない Code Segment どうしは並列に実行することが可能
![cs](./images/code_segments.svg){:width="50%"}

# Data Segment: データの単位
* Code Segment は入出力である Input Data Segment と Output Data Segment を持つ
* Output Data Segment は接続先の Code Segment の Input になる
* Code Segment 内部で扱う変数は Data Segment に格納される
![csds](./images/code_segment_data_segment.svg){:width="50%"}

# 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;
};
```


# メタ計算による階層化
* CbC で書いた実装を CbC で検証していく
    * 仕様記述も CbC で行なう
    * 仕様のチェックも CbC で行なう
    * 実装の記述は変更したくない
    * どこまでがソフトウェア本体でどこまでが実装コード?
* メタ計算で計算を階層化することで解決する
    * 実装はノーマルレベル
    * 検証はメタレベル
    * メタからノーマルは見えて、ノーマルからメタは見えない

# Examples of Meta Computation
* 計算を実現するような計算
* プログラムを生成するようなプログラム
    * TemplateHaskell in Haskell, Template in C++, Generics
    * コンパイル時メタプログラミング
* 言語が特別な API を提供する
    * method_missing, define_method in Ruby
* プログラムがその言語処理系の挙動を変える
    * reflection in Java
* 副作用などの言語処理系に依存した処理を表現する
    * Monad in Haskell

# Meta Code Segment
* メタ計算は Code Segment の接続部分に Meta Code Segment を入れることで表現できる
* 仕様定義、仕様検証は Meta Code Segment に記述
* 実装である Code Segment の検証を行なえば良い
    * Input Data Segment を作成して正しい Output Data Segment を出すかチェックする

# Meta Data Segment
* Meta Code Segment に必要なデータを格納する
* Data Segment より上位の Data Segment


# Code of 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
* 本研究で作成した検証用メタ計算ライブラリ
* 実装コードの ``meta`` を上書きするだけで検証を行なうことができる
* 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙
* 挿入後の木はきちんとバランスしているかチェックする
* Meta Data Segment に挿入順番や実行履歴を記憶させる

# C Bounded Model Checker
* Carnegie Mellon University で開発されている ANSI-C の記号実行モデルチェッカ
* CbC は `__code` を `void` に、`goto` を `return` に変えると C Syntaxになる
* Red-Black Tree を C に変換して検証
* 挿入順番は非決定的な入力 `nondet_int` を使う

# Result of Verification
* CbC のメタ計算 Akasha では要素数13個までチェックできた
* CBMC ではチェックできなかった
* TODO: 表でまとめておく

# Comparison of tools
* valgrind, cbmc, akasha, valgrind, manual unit test
* TODO

# Conclusion and Future Works
* CBMC では検証できない範囲の検証を行なうことができた
* 動作するプログラムの記述を変更することなく検証を行なえた
* 今後の課題
    * 挿入だけでなく削除を含む赤黒木の仕様検証
    * 状態の抽象化による探索の効率化
    * ポインタへの不正アクセス検出などの機能


<!-- vim: set filetype=markdown.slide: -->