--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/presentation/slide.md	Sun Feb 12 18:10:16 2017 +0900
@@ -0,0 +1,223 @@
+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: -->
+