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


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

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

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

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

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

# メタ計算
* とある計算を実現するための計算
* ネットワーク接続、例外処理、メモリ確保、並列処理など
* 時に本来行ないたい処理よりも複雑になる
* CbC は通常レベルの計算とメタ計算を分離して考える
    * 通常レベルではポインタは出てこない、など
* TODO: 図

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

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

# C言語との対応
* CodeSegment は C 言語における返り値の無い関数
* DataSegment は C 言語における構造体
* Meta CodeSegment は CodeSegment の前後にある CodeSegment
* Meta DataSegment は全ての DataSegment の共用体を持つ構造体
* CodeSegment の接続は goto における軽量継続
    * 末尾のみで行なうスタックを保持しない関数呼び出し

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

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

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

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

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

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

# メタ計算ライブラリ akasha
* メタ計算としてプログラムの状態を数え上げる
* goto された時に挿入される要素の組み合わせを全て列挙して実行する
* その度に仕様の式は成り立つかをチェックする
* TODO: 図

# チェックする仕様
* TODO: たかさについて

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

# 定理証明
* 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
* そのままプログラムの性質を保証してやる
* プログラムと証明は Curry-Howard Isomorphism により、自然演繹と型付ラムダ計算が対応
    * プログラムにおける命題は型であり、証明はその導出が存在するかどうか
    * 例えば三段論法が書ける
        * (A -> B) -> (B -> C) -> (A -> C)
        * (int -> bool) -> (bool -> float) -> (int -> float)

# 証明支援系 Agda
* 依存型を持つ言語
    * 型が第一級(型が値である)
    * 「型を取って型を返す型」などが定義可能
* 定理証明が記述可能
    * この言語の上に CbC の項を表現する
    * Agda 経由で CbC の形式的な定義を得る

# Agda 上に CbC を記述するには?
* CbC と CbC の対応で書ける?
    * DataSegment -> 構造体(複数の値と名前によって成り立つ)
    * CodeSegment -> 関数型(型を取って型を返す)
    * Meta DataSegment -> 構造体の共用体
    * Meta CodeSegment -> 関数型?
* Meta CodeSegment の階層構造をどう定義するか
    * 構造体に相当するレコード型はAgdaにある
    * 共用体に相当する直和型も定義可能

# メタレベルの型付け
* Meta CodeSegment が持っているべき性質
    * メタレベルは階層構造を持つ
        * メタ計算は組み合わせられる
    * ノーマルレベルの DataSegment を一様に扱える
    * ノーマルレベルの CodeSegment へと goto できる
        * どんなプログラムからもライブラリとして使える
* 構造体では融通が効かない
    * 完全にマッチしなくてはいけない
* TODO: ソース

# 部分型
* DataSegment が持つべき制約を表現できる型
* 型 T が期待される文脈で S を用いても良い、というようなことができる
    * 「S <: T」で「S は T の部分型である」と読む
    * 全てのDataSegment に対して「MDS <: DS」となるような MDS を用意する
* DataSegment X が期待される CodeSegment に Meta DataSegment を渡してやる

# 入力の部分型
# 出力の部分型

# 部分型で何ができたか?
* Meta CodeSegment を部分型とすることで
    * ノーマルレベルの CodeSegment の前後に処理を入れても型は整合する
    * Meta CodeSegment を CodeSegment とすることで階層構造を作れる
* Meta DataSegment を部分型とすることで
    * ノーマルレベルからはアクセスできないデータを保持してもOK
    * ノーマルレベルに Meta DataSegment を渡しても良い
    * こちらも階層構造を取ることができる

# SingleLinkedStack の証明
* 証明支援系 Agda に GearsOS のデータ構造 SingleLinkedStack を定義
    * スタックは赤黒木に用いられている
* その性質を証明する
    * 性質もいくつか考えられる
    * 「push して pop するとスタックは元に戻る」

# Agda を用いた証明手法
* 基本的にはデータの構造に関する帰納法
    * スタックは内部に SingleLinkedList を持つ
    * SingleLinkedList は NULL か値と次のノードを持つ
    * 値がある場合と無い場合との場合分け
* 挿入する要素を指定せずに push を呼ぶとどうなるのか?
    * 実装依存のコード
    * 証明には表れる
        * TODO: かく...

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

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

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