# HG changeset patch # User atton # Date 1486890616 -32400 # Node ID 3ead244513d5038498ca9b0a97581b88b76f0119 # Parent 3ef3933dbd77f5bce95539c4f1cec7c6c665ac37 Writing slide ... diff -r 3ef3933dbd77 -r 3ead244513d5 presentation/slide.md --- /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る +* 赤黒木の挿入を証明する + + +