Mercurial > hg > Papers > 2018 > nozomi-master

diff presentation/slide.html @ 114:5cca315b0230

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Writing slide...
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 13 Feb 2017 16:01:38 +0900
parents 76769fd0995e
children d731f2d0947d
line wrap: on
line diff
--- a/presentation/slide.html	Mon Feb 13 15:44:45 2017 +0900
+++ b/presentation/slide.html	Mon Feb 13 16:01:38 2017 +0900
@@ -86,7 +86,7 @@
 <!-- === 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)
+                on 2017-02-13 16:01:12 +0900 with Markdown engine kramdown (1.13.0)
                   using options {}
   -->
 
@@ -129,12 +129,26 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="section-2">モデル検査的アプローチについての流れ</h1>
+<ul>
+  <li>Continuation based C (CbC) 言語について</li>
+  <li>CbC における CodeSegment と DataSegment を用いたプログラミングスタイル</li>
+  <li>CbC とメタ計算について</li>
+  <li>CbC で記述された GearsOS とそのデータ構造である赤黒木</li>
+  <li>赤黒木の仕様の定義とその検証手法</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>
+  <li>両検証手法をメタ計算として利用可能</li>
 </ul>
 
 
@@ -151,9 +165,10 @@
     </ul>
   </li>
   <li>CodeSegment どうしを接続することによりプログラム全体を作る</li>
-  <li>TODO: 図</li>
 </ul>
 
+<p><img src="./images/goto.svg" alt="goto" width="50%" /></p>
+
 
 </div>
 <div class='slide '>
@@ -167,26 +182,28 @@
       <li>接続元の Output DataSegment は接続先の Input DataSegment</li>
     </ul>
   </li>
-  <li>TODO: 図</li>
 </ul>
 
+<p><img src="./images/csds.svg" alt="csds" width="50%" /></p>
+
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-2">メタ計算</h1>
+<h1 id="section-3">メタ計算</h1>
 <ul>
   <li>とある計算を実現するための計算</li>
   <li>ネットワーク接続、例外処理、メモリ確保、並列処理など</li>
-  <li>時に本来行ないたい処理よりも複雑になる</li>
   <li>CbC は通常レベルの計算とメタ計算を分離して考える
     <ul>
       <li>通常レベルではポインタは出てこない、など</li>
     </ul>
   </li>
-  <li>TODO: 図</li>
+  <li>CodeSegment の接続部分に処理を追加することで実現</li>
 </ul>
 
+<p><img src="./images/meta.svg" alt="meta" width="50%" /></p>
+
 
 </div>
 <div class='slide '>
@@ -213,23 +230,6 @@
 </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>
@@ -242,7 +242,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-3">赤黒木</h1>
+<h1 id="section-4">赤黒木</h1>
 <ul>
   <li>データの保存に用いる二分木</li>
   <li>特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
@@ -264,14 +264,15 @@
   <li>挿入したい要素を DataSegment に格納して次の CodeSegment へ goto</li>
   <li>goto する前に Meta CodeSegment が実行されて木に挿入する</li>
   <li>GearsOS では木の実装のためにスタックを用いて経路情報を保持している</li>
-  <li>TODO: 図</li>
 </ul>
 
+<p><img src="./images/put.svg" alt="put" width="50%" /></p>
+
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-4">仕様の記述とその確認</h1>
+<h1 id="section-5">仕様の記述とその確認</h1>
 <ul>
   <li>「バランスが取れている」とは何かを表現できる必要がある
     <ul>
@@ -328,21 +329,38 @@
 <!-- _S9SLIDE_ -->
 <h1 id="akasha">メタ計算ライブラリ akasha</h1>
 <ul>
-  <li>メタ計算としてプログラムの状態を数え上げる</li>
-  <li>goto された時に挿入される要素の組み合わせを全て列挙して実行する</li>
-  <li>その度に仕様の式は成り立つかをチェックする</li>
-  <li>TODO: 図</li>
+  <li>メタ計算としてプログラムの状態を数え上げる
+    <ul>
+      <li>goto された時に挿入される要素の組み合わせを全て列挙して実行する</li>
+      <li>その度に仕様の式は成り立つかをチェックする</li>
+    </ul>
+  </li>
+  <li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
 </ul>
 
+<p><img src="./images/akashaPut.svg" alt="akashaPut" width="50%" /></p>
+
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-5">チェックする仕様</h1>
+<h1 id="section-6">チェックする仕様</h1>
 <ul>
-  <li>TODO: たかさについて</li>
+  <li>赤黒木のの高さに関する仕様に以下のものがある
+    <ul>
+      <li>木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる</li>
+    </ul>
+  </li>
+  <li>以下のように assert を用いて CbC で定義できる</li>
+  <li>この仕様が満たされるかをチェックする</li>
 </ul>
 
+<pre><code>void verifySpecification(struct Context* context, struct Tree* tree) {
+    assert(!(maxHeight(tree-&gt;root, 1) &gt; 2*minHeight(tree-&gt;root, 1)));
+        goto meta(context, EnumerateInputs);
+    }
+</code></pre>
+
 
 </div>
 <div class='slide '>
@@ -369,61 +387,84 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-6">定理証明</h1>
+<h1 id="section-7">定理証明的なアプローチの流れ</h1>
+<ul>
+  <li>プログラムを証明するにはどうするのか</li>
+  <li>証明支援系 Agda における証明</li>
+  <li>Agda による CbC の定義</li>
+  <li>Agda を用いて CbC のコードを証明する</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="continuation-based-c-">定理証明を Continuation based C へ適用するには</h1>
 <ul>
   <li>任意の回数だけ木の操作を行なっても大丈夫なことを保証したい</li>
   <li>そのままプログラムの性質を保証してやる</li>
-  <li>プログラムと証明は Curry-Howard Isomorphism により、自然演繹と型付ラムダ計算が対応
+  <li>Coq, Agda, ATS2 などのプログラミング言語で証明が可能
     <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>
+      <li>本当は CbC で CbC 自身を証明したい</li>
+      <li>しかし CbC の形式的な定義が無いために今はできない</li>
     </ul>
   </li>
+  <li>Agda 上に CbC を定義することで形式的な定義を得る</li>
 </ul>
 
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="agda">証明支援系 Agda</h1>
+<h1 id="agda--datasegment">Agda と DataSegment</h1>
 <ul>
-  <li>依存型を持つ言語
-    <ul>
-      <li>型が第一級(型が値である)</li>
-      <li>「型を取って型を返す型」などが定義可能</li>
-    </ul>
-  </li>
-  <li>定理証明が記述可能
-    <ul>
-      <li>この言語の上に CbC の項を表現する</li>
-      <li>Agda 経由で CbC の形式的な定義を得る</li>
-    </ul>
-  </li>
+  <li>CbC の DataSegment は Agda のレコード型</li>
 </ul>
 
+<pre><code>__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+</code></pre>
+<pre><code>record ds0 : Set where
+  field
+    a : Int
+    b : Int
+</code></pre>
+
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="agda--cbc-">Agda 上に CbC を記述するには?</h1>
+<h1 id="agda--codesegment">Agda と CodeSegment</h1>
 <ul>
-  <li>CbC と CbC の対応で書ける?
+  <li>CbC の CodeSegment は、Agda の関数型(Input を取って Output を返す)</li>
+</ul>
+
+<pre><code>__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+</code></pre>
+<pre><code>cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -&gt; goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section-8">メタレベルの型付け</h1>
+<ul>
+  <li>メタ計算とは通常のレベルとは区別された計算</li>
+  <li>任意の通常のレベルの計算を扱えなくてはならない
     <ul>
-      <li>DataSegment -&gt; 構造体(複数の値と名前によって成り立つ)</li>
-      <li>CodeSegment -&gt; 関数型(型を取って型を返す)</li>
-      <li>Meta DataSegment -&gt; 構造体の共用体</li>
-      <li>Meta CodeSegment -&gt; 関数型?</li>
+      <li>ライブラリが呼び出されるプログラムは無数にあるようなイメージ</li>
     </ul>
   </li>
-  <li>Meta CodeSegment の階層構造をどう定義するか
+  <li>メタレベルを使うための制約を満たしていれば良い、ということを表現できれば良い</li>
+  <li>部分型を使う
     <ul>
-      <li>構造体に相当するレコード型はAgdaにある</li>
-      <li>共用体に相当する直和型も定義可能</li>
+      <li>Java におけるインターフェース、Haskell における型クラス</li>
+      <li>「このデータにはこのフィールドさえあれば良い」</li>
     </ul>
   </li>
 </ul>
@@ -432,71 +473,19 @@
 </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>
+<h1 id="agda-">Agda 上のメタ計算</h1>
 <ul>
-  <li>DataSegment が持つべき制約を表現できる型</li>
-  <li>型 T が期待される文脈で S を用いても良い、というようなことができる
+  <li>ノーマルレベルの型を保持したままメタレベルの計算を利用できる
     <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>
+      <li>cs0 の定義はメタ計算用に変更しなくても良い
+~~~
+main : ds1
+main = goto cs0 (record {a = 100 ; b = 50})
+~~~
+~~~
+main : Meta
+main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c’ = 0 ; next = (N.cs id)})
+~~~</li>
     </ul>
   </li>
 </ul>
@@ -505,17 +494,17 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="singlelinkedstack-">SingleLinkedStack の証明</h1>
+<h1 id="agda--cbc-">Agda 上に CbC を記述した成果</h1>
 <ul>
-  <li>証明支援系 Agda に GearsOS のデータ構造 SingleLinkedStack を定義
+  <li>部分型で CbC の型付けができた</li>
+  <li>メタ計算をきちんと階層化できた
     <ul>
-      <li>スタックは赤黒木に用いられている</li>
+      <li>メタ計算にもメタ計算が適用可能</li>
     </ul>
   </li>
-  <li>その性質を証明する
+  <li>赤黒木で利用しているデータ構造スタックの性質を証明できた
     <ul>
-      <li>性質もいくつか考えられる</li>
-      <li>「push して pop するとスタックは元に戻る」</li>
+      <li>任意の回数だけ値を積んで同じだけ取り出すとスタックは変化しない</li>
     </ul>
   </li>
 </ul>
@@ -524,32 +513,7 @@
 </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>
+<h1 id="section-9">まとめ</h1>
 <ul>
   <li>Continuation based C 言語を対象にした二種類の検証アプローチ</li>
   <li>モデル検査的なアプローチ
@@ -571,12 +535,12 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-12">今後の課題</h1>
+<h1 id="section-10">今後の課題</h1>
 <ul>
   <li>部分型を利用してCbCを型付け</li>
   <li>依存型をCbC に導入して自身を証明可能にする</li>
   <li>型情報から stub を自動生成すkる</li>
-  <li>赤黒木の挿入を証明する</li>
+  <li>赤黒木の挿入に関する性質を証明する</li>
 </ul>
 
 <!-- vim: set filetype=markdown.slide: -->