title: メタ計算を用いた Continuation based C の検証手法
author: Yasutaka Higa
profile:
lang: Japanese


# プログラミング言語とソフトウェアの信頼性
* 信頼性の高いソフトウェアを提供したい
* ソフトウェアの仕様を検証するには二つの手法がある
    * プログラムの持つ状態を数え上げ、仕様から外れた状態が無いかを確認するモデル検査
    * プログラムの性質を直接証明してしまう定理証明
* モデル検査も証明も行ないやすい言語として Continuation based C 言語を開発している

# 二つのアプローチを用いたソフトウェア検証
* モデル検査的アプローチ
    * メタ計算ライブラリ akasha による網羅的な実行
    * 非破壊赤黒木の仕様定義と検証
* 定理証明的なアプローチ
    * 依存型を持つ証明支援系言語 Agda による CbC の証明
    * 部分型を利用して Agda 上に型付きの CbC の項を記述する
    * 型システムを通して CbC の形式的な定義を得る
    * SingleLinkedStack の性質の証明

# モデル検査的アプローチについての流れ
* Continuation based C (CbC) 言語について
* CbC における CodeSegment と DataSegment を用いたプログラミングスタイル
* CbC とメタ計算について
* CbC で記述された GearsOS とそのデータ構造である赤黒木
* 赤黒木の仕様の定義とその検証手法

# Continuation based C
* 当研究室で開発しているプログラミング言語
* アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語
* OS や組み込みソフトウェアなどを対象にしている
* CodeSegment と DataSegment という単位を用いてプログラミングする
* 両検証手法をメタ計算として利用可能

# CodeSegment
* CodeSegment とは
    * 処理の単位
    * 結合や分割が容易
    * 入力と出力を持つ
* CodeSegment どうしを接続することによりプログラム全体を作る

![goto](./images/goto.svg){:width="50%"}


# DataSegment
* DataSegment とは
    * データの単位
    * CodeSegment の入出力にあたる
    * 接続元の Output DataSegment は接続先の Input DataSegment

![csds](./images/csds.svg){:width="50%"}

# メタ計算
* とある計算を実現するための計算
* ネットワーク接続、例外処理、メモリ確保、並列処理など
* CbC は通常レベルの計算とメタ計算を分離して考える
    * 通常レベルではポインタは出てこない、など
* CodeSegment の接続部分に処理を追加することで実現

![meta](./images/meta.svg){:width="50%"}

# Meta CodeSegment
* メタ計算を行なう CodeSegment
* 通常の CodeSegment どうしの接続の間に入る
* TODO: 図

# Meta DataSegment
* メタ計算用の DataSegment
* 通常の DataSegment を含むような DataSegment
* TODO: 図

# 並列に信頼性高く動作する GearsOS
* CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある
* 並列実行やモデル検査をメタ計算として提供する
* 現在はメモリ管理、Synchronized Queue、非破壊赤黒木などが実装済み
* 今回はこの非破壊赤黒木の検証を行なう

# 赤黒木
* データの保存に用いる二分木
* 特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
    * ルートノードと葉ノードの色は黒
    * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)
    * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定
* TODO: 図

# GearsOS における赤黒木の利用例(ノードの挿入)
* 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto
* goto する前に Meta CodeSegment が実行されて木に挿入する
* GearsOS では木の実装のためにスタックを用いて経路情報を保持している

![put](./images/put.svg){:width="50%"}

# 仕様の記述とその確認
* 「バランスが取れている」とは何かを表現できる必要がある
    * 実行可能な CbC の式を使った assert になる
* そしてそれを保証したい
    * プログラムの全ての状態においてこれは常に成り立つのか?

# 既存のモデル検査器 spin
* spin
    * promela と呼ばれる言語でプログラムを記述
    * 並列に動作するプログラムの仕様を検証可能
    * 検証した promela から実行可能な C ソースを生成可能
    * 仕様は bool になる式を用いた assert
    * promela は C とは記述が異なる

# 既存のモデル検査器 CBMC
* CBMC
    * 検証対象のCソースを変更しないでも良い
    * C/C++ 言語の記号実行が可能
        * 条件分岐を網羅的に実行
    * 仕様は bool になる式を用いた assert
    * 有限ステップ検証する有界モデル検査器

# メタ計算ライブラリ akasha
* メタ計算としてプログラムの状態を数え上げる
    * goto された時に挿入される要素の組み合わせを全て列挙して実行する
    * その度に仕様の式は成り立つかをチェックする
* ノーマルレベルのコードを検証用に変更せず検証可能

![akashaPut](./images/akashaPut.svg){:width="51%"}

# チェックする仕様
* 赤黒木のの高さに関する仕様に以下のものがある
    * 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる
* 以下のように assert を用いて CbC で定義できる
* この仕様が満たされるかをチェックする

```
void verifySpecification(struct Context* context, struct Tree* tree) {
    assert(!(maxHeight(tree->root, 1) > 2*minHeight(tree->root, 1)));
        goto meta(context, EnumerateInputs);
    }
```

# akasha と CBMC の比較
* akasha は有限の要素数の組み合わせをチェックする
    * 要素数が13個までならどの順で木に挿入しても良い
* 比較対象として C Bounded Model Checker を使用した
    * C/C++ の記号実行を行なう
    * 実行可能なステップ数411だけ展開しても仕様は満たされる
    * が、恣意的にバグを入れ込んでも反例を返さない
    * akasha は返した
* 固定の要素数までの仕様検査で十分なのか?

# 定理証明的なアプローチの流れ
* プログラムを証明するにはどうするのか
* 証明支援系 Agda における証明
* Agda による CbC の定義
* Agda を用いて CbC のコードを証明する

# 定理証明を Continuation based C へ適用するには
* 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
* そのままプログラムの性質を保証してやる
* Coq, Agda, ATS2 などのプログラミング言語で証明が可能
    * 本当は CbC で CbC 自身を証明したい
    * しかし CbC の形式的な定義が無いために今はできない
* Agda 上に CbC を定義することで形式的な定義を得る

# Agda と DataSegment
* CbC の DataSegment は Agda のレコード型

```
__code cs0(int a, int b){
  goto cs1(a+b);
}
```
```
record ds0 : Set where
  field
    a : Int
    b : Int
```

# Agda と CodeSegment
* CbC の CodeSegment は、Agda の関数型(Input を取って Output を返す)

```
__code cs0(int a, int b){
  goto cs1(a+b);
}
```
```
cs0 : CodeSegment ds0 ds1
cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
```

# メタレベルの型付け
* メタ計算とは通常のレベルとは区別された計算
* 任意の通常のレベルの計算を扱えなくてはならない
    * ライブラリが呼び出されるプログラムは無数にあるようなイメージ
* メタレベルを使うための制約を満たしていれば良い、ということを表現できれば良い
* 部分型を使う
    * Java におけるインターフェース、Haskell における型クラス
    * 「このデータにはこのフィールドさえあれば良い」

# Agda 上のメタ計算
* ノーマルレベルの型を保持したままメタレベルの計算を利用できる
    * cs0 の定義はメタ計算用に変更しなくても良い

```
main : ds1
main = goto cs0 (record {a = 100 ; b = 50})
```
```
main : Meta
main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)})
```

# Agda 上に CbC を記述した成果
* 部分型で CbC の型付けができた
* メタ計算をきちんと階層化できた
    * メタ計算にもメタ計算が適用可能
* 赤黒木で利用しているデータ構造スタックの性質を証明できた
    * 任意の回数だけ値を積んで同じだけ取り出すとスタックは変化しない

# まとめ
* Continuation based C 言語を対象にした二種類の検証アプローチ
* モデル検査的なアプローチ
    * 継続を上書きして可能な状態を数え上げるメタ計算ライブラリ akasha を実装
    * 有限の要素数まで保証できた
* 証明的なアプローチ
    * 証明支援系 Agda 上で CbC のプログラムを定義して直接証明
    * 部分型を利用して CbC を型付け
    * データ構造 SingleLinkedStack の証明ができた

# 今後の課題
* 部分型を利用してCbCを型付け
* 依存型をCbC に導入して自身を証明可能にする
* 型情報から stub を自動生成すkる
* 赤黒木の挿入に関する性質を証明する

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