Mercurial > hg > Papers > 2018 > nozomi-master

<!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/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>

<style>
  .slide {page-break-after: always;}
</style>


</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 -&gt; B) -&gt; (B -&gt; C) -&gt; (A -&gt; C)</li>
          <li>(int -&gt; bool) -&gt; (bool -&gt; float) -&gt; (int -&gt; 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 -&gt; 構造体(複数の値と名前によって成り立つ)</li>
      <li>CodeSegment -&gt; 関数型(型を取って型を返す)</li>
      <li>Meta DataSegment -&gt; 構造体の共用体</li>
      <li>Meta CodeSegment -&gt; 関数型?</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 &lt;: T」で「S は T の部分型である」と読む</li>
      <li>全てのDataSegment に対して「MDS &lt;: 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>
author	atton <atton@cr.ie.u-ryukyu.ac.jp>
date	Sun, 12 Feb 2017 18:10:33 +0900
parents
children	5cca315b0230