Mercurial > hg > Papers > 2018 > nozomi-master
diff presentation/slide.html @ 103:76769fd0995e
Generate slide
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 12 Feb 2017 18:10:33 +0900 |
parents | |
children | 5cca315b0230 |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presentation/slide.html Sun Feb 12 18:10:33 2017 +0900 @@ -0,0 +1,590 @@ +<!DOCTYPE html> +<html> +<head> + <meta http-equiv="content-type" content="text/html;charset=utf-8"> + <title>メタ計算を用いた Continuation based C の検証手法</title> + +<meta name="generator" content="Slide Show (S9) v2.5.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]"> +<meta name="author" content="Yasutaka Higa" > + +<!-- style sheet links --> +<link rel="stylesheet" href="s6/themes/projection.css" media="screen,projection"> +<link rel="stylesheet" href="s6/themes/screen.css" media="screen"> +<link rel="stylesheet" href="s6/themes/print.css" media="print"> +<link rel="stylesheet" href="s6/themes/blank.css" media="screen,projection"> + +<!-- JS --> +<script src="s6/js/jquery-1.11.3.min.js"></script> +<script src="s6/js/jquery.slideshow.js"></script> +<script src="s6/js/jquery.slideshow.counter.js"></script> +<script src="s6/js/jquery.slideshow.controls.js"></script> +<script src="s6/js/jquery.slideshow.footer.js"></script> +<script src="s6/js/jquery.slideshow.autoplay.js"></script> + +<!-- prettify --> +<link rel="stylesheet" href="scripts/prettify.css"> +<script src="scripts/prettify.js"></script> + +<script> + $(document).ready( function() { + Slideshow.init(); + + $('code').each(function(_, el) { + if (!el.classList.contains('noprettyprint')) { + el.classList.add('prettyprint'); + } + }); + prettyPrint(); + } ); + + +</script> + +<!-- Better Browser Banner for Microsoft Internet Explorer (IE) --> +<!--[if IE]> +<script src="s6/js/jquery.microsoft.js"></script> +<![endif]--> + + + +</head> +<body> + +<div class="layout"> + <div id="header"></div> + <div id="footer"> + <div align="right"> + <img src="s6/images/logo.svg" width="200px"> + </div> + </div> +</div> + +<div class="presentation"> + + <div class='slide cover'> + <table width="90%" height="90%" border="0" align="center"> + <tr> + <td> + <div align="center"> + <h1><font color="#808db5">メタ計算を用いた Continuation based C の検証手法</font></h1> + </div> + </td> + </tr> + <tr> + <td> + <div align="left"> + Yasutaka Higa + + <hr style="color:#ffcc00;background-color:#ffcc00;text-align:left;border:none;width:100%;height:0.2em;"> + </div> + </td> + </tr> + </table> + </div> + +<div class='slide '> +<!-- === begin markdown block === + + generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16] + on 2017-02-12 18:10:22 +0900 with Markdown engine kramdown (1.13.0) + using options {} + --> + +<!-- _S9SLIDE_ --> +<h1 id="section">プログラミング言語とソフトウェアの信頼性</h1> +<ul> + <li>信頼性の高いソフトウェアを提供したい</li> + <li>ソフトウェアの仕様を検証するには二つの手法がある + <ul> + <li>プログラムの持つ状態を数え上げ、仕様から外れた状態が無いかを確認するモデル検査</li> + <li>プログラムの性質を直接証明してしまう定理証明</li> + </ul> + </li> + <li>モデル検査も証明も行ないやすい言語として Continuation based C 言語を開発している</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="section-1">二つのアプローチを用いたソフトウェア検証</h1> +<ul> + <li>モデル検査的アプローチ + <ul> + <li>メタ計算ライブラリ akasha による網羅的な実行</li> + <li>非破壊赤黒木の仕様定義と検証</li> + </ul> + </li> + <li>定理証明的なアプローチ + <ul> + <li>依存型を持つ証明支援系言語 Agda による CbC の証明</li> + <li>部分型を利用して Agda 上に型付きの CbC の項を記述する</li> + <li>型システムを通して CbC の形式的な定義を得る</li> + <li>SingleLinkedStack の性質の証明</li> + </ul> + </li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="continuation-based-c">Continuation based C</h1> +<ul> + <li>当研究室で開発しているプログラミング言語</li> + <li>アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語</li> + <li>OS や組み込みソフトウェアなどを対象にしている</li> + <li>CodeSegment と DataSegment という単位を用いてプログラミングする</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="codesegment">CodeSegment</h1> +<ul> + <li>CodeSegment とは + <ul> + <li>処理の単位</li> + <li>結合や分割が容易</li> + <li>入力と出力を持つ</li> + </ul> + </li> + <li>CodeSegment どうしを接続することによりプログラム全体を作る</li> + <li>TODO: 図</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="datasegment">DataSegment</h1> +<ul> + <li>DataSegment とは + <ul> + <li>データの単位</li> + <li>CodeSegment の入出力にあたる</li> + <li>接続元の Output DataSegment は接続先の Input DataSegment</li> + </ul> + </li> + <li>TODO: 図</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="section-2">メタ計算</h1> +<ul> + <li>とある計算を実現するための計算</li> + <li>ネットワーク接続、例外処理、メモリ確保、並列処理など</li> + <li>時に本来行ないたい処理よりも複雑になる</li> + <li>CbC は通常レベルの計算とメタ計算を分離して考える + <ul> + <li>通常レベルではポインタは出てこない、など</li> + </ul> + </li> + <li>TODO: 図</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="meta-codesegment">Meta CodeSegment</h1> +<ul> + <li>メタ計算を行なう CodeSegment</li> + <li>通常の CodeSegment どうしの接続の間に入る</li> + <li>TODO: 図</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="meta-datasegment">Meta DataSegment</h1> +<ul> + <li>メタ計算用の DataSegment</li> + <li>通常の DataSegment を含むような DataSegment</li> + <li>TODO: 図</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="c">C言語との対応</h1> +<ul> + <li>CodeSegment は C 言語における返り値の無い関数</li> + <li>DataSegment は C 言語における構造体</li> + <li>Meta CodeSegment は CodeSegment の前後にある CodeSegment</li> + <li>Meta DataSegment は全ての DataSegment の共用体を持つ構造体</li> + <li>CodeSegment の接続は goto における軽量継続 + <ul> + <li>末尾のみで行なうスタックを保持しない関数呼び出し</li> + </ul> + </li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="gearsos">並列に信頼性高く動作する GearsOS</h1> +<ul> + <li>CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある</li> + <li>並列実行やモデル検査をメタ計算として提供する</li> + <li>現在はメモリ管理、Synchronized Queue、非破壊赤黒木などが実装済み</li> + <li>今回はこの非破壊赤黒木の検証を行なう</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="section-3">赤黒木</h1> +<ul> + <li>データの保存に用いる二分木</li> + <li>特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る + <ul> + <li>ルートノードと葉ノードの色は黒</li> + <li>赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)</li> + <li>ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定</li> + </ul> + </li> + <li>TODO: 図</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="gearsos-">GearsOS における赤黒木の利用例(ノードの挿入)</h1> +<ul> + <li>挿入したい要素を DataSegment に格納して次の CodeSegment へ goto</li> + <li>goto する前に Meta CodeSegment が実行されて木に挿入する</li> + <li>GearsOS では木の実装のためにスタックを用いて経路情報を保持している</li> + <li>TODO: 図</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="section-4">仕様の記述とその確認</h1> +<ul> + <li>「バランスが取れている」とは何かを表現できる必要がある + <ul> + <li>実行可能な CbC の式を使った assert になる</li> + </ul> + </li> + <li>そしてそれを保証したい + <ul> + <li>プログラムの全ての状態においてこれは常に成り立つのか?</li> + </ul> + </li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="spin">既存のモデル検査器 spin</h1> +<ul> + <li>spin + <ul> + <li>promela と呼ばれる言語でプログラムを記述</li> + <li>並列に動作するプログラムの仕様を検証可能</li> + <li>検証した promela から実行可能な C ソースを生成可能</li> + <li>仕様は bool になる式を用いた assert</li> + <li>promela は C とは記述が異なる</li> + </ul> + </li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="cbmc">既存のモデル検査器 CBMC</h1> +<ul> + <li>CBMC + <ul> + <li>検証対象のCソースを変更しないでも良い</li> + <li>C/C++ 言語の記号実行が可能 + <ul> + <li>条件分岐を網羅的に実行</li> + </ul> + </li> + <li>仕様は bool になる式を用いた assert</li> + <li>有限ステップ検証する有界モデル検査器</li> + </ul> + </li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="akasha">メタ計算ライブラリ akasha</h1> +<ul> + <li>メタ計算としてプログラムの状態を数え上げる</li> + <li>goto された時に挿入される要素の組み合わせを全て列挙して実行する</li> + <li>その度に仕様の式は成り立つかをチェックする</li> + <li>TODO: 図</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="section-5">チェックする仕様</h1> +<ul> + <li>TODO: たかさについて</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="akasha--cbmc-">akasha と CBMC の比較</h1> +<ul> + <li>akasha は有限の要素数の組み合わせをチェックする + <ul> + <li>要素数が13個までならどの順で木に挿入しても良い</li> + </ul> + </li> + <li>比較対象として C Bounded Model Checker を使用した + <ul> + <li>C/C++ の記号実行を行なう</li> + <li>実行可能なステップ数411だけ展開しても仕様は満たされる</li> + <li>が、恣意的にバグを入れ込んでも反例を返さない</li> + <li>akasha は返した</li> + </ul> + </li> + <li>固定の要素数までの仕様検査で十分なのか?</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="section-6">定理証明</h1> +<ul> + <li>任意の回数だけ木の操作を行なっても大丈夫なことを保証したい</li> + <li>そのままプログラムの性質を保証してやる</li> + <li>プログラムと証明は Curry-Howard Isomorphism により、自然演繹と型付ラムダ計算が対応 + <ul> + <li>プログラムにおける命題は型であり、証明はその導出が存在するかどうか</li> + <li>例えば三段論法が書ける + <ul> + <li>(A -> B) -> (B -> C) -> (A -> C)</li> + <li>(int -> bool) -> (bool -> float) -> (int -> float)</li> + </ul> + </li> + </ul> + </li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="agda">証明支援系 Agda</h1> +<ul> + <li>依存型を持つ言語 + <ul> + <li>型が第一級(型が値である)</li> + <li>「型を取って型を返す型」などが定義可能</li> + </ul> + </li> + <li>定理証明が記述可能 + <ul> + <li>この言語の上に CbC の項を表現する</li> + <li>Agda 経由で CbC の形式的な定義を得る</li> + </ul> + </li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="agda--cbc-">Agda 上に CbC を記述するには?</h1> +<ul> + <li>CbC と CbC の対応で書ける? + <ul> + <li>DataSegment -> 構造体(複数の値と名前によって成り立つ)</li> + <li>CodeSegment -> 関数型(型を取って型を返す)</li> + <li>Meta DataSegment -> 構造体の共用体</li> + <li>Meta CodeSegment -> 関数型?</li> + </ul> + </li> + <li>Meta CodeSegment の階層構造をどう定義するか + <ul> + <li>構造体に相当するレコード型はAgdaにある</li> + <li>共用体に相当する直和型も定義可能</li> + </ul> + </li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="section-7">メタレベルの型付け</h1> +<ul> + <li>Meta CodeSegment が持っているべき性質 + <ul> + <li>メタレベルは階層構造を持つ + <ul> + <li>メタ計算は組み合わせられる</li> + </ul> + </li> + <li>ノーマルレベルの DataSegment を一様に扱える</li> + <li>ノーマルレベルの CodeSegment へと goto できる + <ul> + <li>どんなプログラムからもライブラリとして使える</li> + </ul> + </li> + </ul> + </li> + <li>構造体では融通が効かない + <ul> + <li>完全にマッチしなくてはいけない</li> + </ul> + </li> + <li>TODO: ソース</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="section-8">部分型</h1> +<ul> + <li>DataSegment が持つべき制約を表現できる型</li> + <li>型 T が期待される文脈で S を用いても良い、というようなことができる + <ul> + <li>「S <: T」で「S は T の部分型である」と読む</li> + <li>全てのDataSegment に対して「MDS <: DS」となるような MDS を用意する</li> + </ul> + </li> + <li>DataSegment X が期待される CodeSegment に Meta DataSegment を渡してやる</li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="section-9">入力の部分型</h1> +<p># 出力の部分型</p> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="section-10">部分型で何ができたか?</h1> +<ul> + <li>Meta CodeSegment を部分型とすることで + <ul> + <li>ノーマルレベルの CodeSegment の前後に処理を入れても型は整合する</li> + <li>Meta CodeSegment を CodeSegment とすることで階層構造を作れる</li> + </ul> + </li> + <li>Meta DataSegment を部分型とすることで + <ul> + <li>ノーマルレベルからはアクセスできないデータを保持してもOK</li> + <li>ノーマルレベルに Meta DataSegment を渡しても良い</li> + <li>こちらも階層構造を取ることができる</li> + </ul> + </li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="singlelinkedstack-">SingleLinkedStack の証明</h1> +<ul> + <li>証明支援系 Agda に GearsOS のデータ構造 SingleLinkedStack を定義 + <ul> + <li>スタックは赤黒木に用いられている</li> + </ul> + </li> + <li>その性質を証明する + <ul> + <li>性質もいくつか考えられる</li> + <li>「push して pop するとスタックは元に戻る」</li> + </ul> + </li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="agda-">Agda を用いた証明手法</h1> +<ul> + <li>基本的にはデータの構造に関する帰納法 + <ul> + <li>スタックは内部に SingleLinkedList を持つ</li> + <li>SingleLinkedList は NULL か値と次のノードを持つ</li> + <li>値がある場合と無い場合との場合分け</li> + </ul> + </li> + <li>挿入する要素を指定せずに push を呼ぶとどうなるのか? + <ul> + <li>実装依存のコード</li> + <li>証明には表れる + <ul> + <li>TODO: かく…</li> + </ul> + </li> + </ul> + </li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="section-11">まとめ</h1> +<ul> + <li>Continuation based C 言語を対象にした二種類の検証アプローチ</li> + <li>モデル検査的なアプローチ + <ul> + <li>継続を上書きして可能な状態を数え上げるメタ計算ライブラリ akasha を実装</li> + <li>有限の要素数まで保証できた</li> + </ul> + </li> + <li>証明的なアプローチ + <ul> + <li>証明支援系 Agda 上で CbC のプログラムを定義して直接証明</li> + <li>部分型を利用して CbC を型付け</li> + <li>データ構造 SingleLinkedStack の証明ができた</li> + </ul> + </li> +</ul> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h1 id="section-12">今後の課題</h1> +<ul> + <li>部分型を利用してCbCを型付け</li> + <li>依存型をCbC に導入して自身を証明可能にする</li> + <li>型情報から stub を自動生成すkる</li> + <li>赤黒木の挿入を証明する</li> +</ul> + +<!-- vim: set filetype=markdown.slide: --> + +<!-- === end markdown block === --> +</div> + + +</div><!-- presentation --> +</body> +</html>