Mercurial > hg > Papers > 2016 > atton-ipsjpro

--- a/presentation/slide.md	Tue Aug 02 17:56:27 2016 +0900
+++ b/presentation/slide.md	Wed Aug 03 17:53:25 2016 +0900
@@ -10,67 +10,73 @@
 * 計算を拡張するメタ計算として検証機構を導入し、ソフトウェアの実装コードの検証を行なう

 # ソフトウェアの信頼性向上手法
+* assert
+    * 実行プログラム上で仕様が満たされているかチェックする
+    * 網羅的にテストできない
+    * ユニットテストと組み合わせて使う
+* 検証の計算システムで実行する(メタ計算)
+    * Java Path Finder, Valgrind
+    * 大規模システムは実行できない
 * アルゴリズムの正しさを証明する
     * Agda, Coq, Idris といった証明支援系でプログラムを記述する
-    * TeX: アルゴリズムの証明をドキュメントとして記述している
+    * 極めて難しい
+    * 実装に対して適用できない
 * ソフトウェアの仕様を記述し、その反例が無いかをチェックする
     * Spin, NuSMV, CBMC といったモデルチェッカ
-* テストデータを入力して正しい出力を返すか
-    * ユニットテスト
-* assert や型システム、検証用の実行処理系
-    * Java Path Finder, Virtual VM, Valgrind
+    * モデル検査用に特化した言語で実装を記述する必要がある

-# ソフトウェアの実装を検証したい
-* アルゴリズムの正しさが証明できても実装する際にバグが入ることがある
+# Akasha の目的
+* 実装言語そのものを検査する
+    * 実装に入り込むバグをする
     * 単語の打ち間違いによるバグ
-    * 同じアルゴリズムを検証と実装で二度記述する
-    * 検証と実装で言語も違うことも
-* 実際に動作するソフトウェアの実装をチェックしたい
-    * 実装コードを変更せずに仕様を保証する
-    * 実装部分と検証部分も同じ言語で記述したい
+* 高速かつ網羅的に検査する
+* メタ計算の切り替えで様々な検証を行なう
+* 高速なメタ計算が行なえる言語(CbC) を用いる

 # Continuation based C (CbC)
 * 当研究室で開発している言語
+* Code Segment, Data Segment という単位でソフトウェアを記述する
 * 関数呼び出しは末尾のみ、の制約を持ったC言語
-    * Tail Call を言語仕様として持つ
     * スタックは持たない
     * goto で飛んで戻ってこない
-    * アーキテクチャに依存しないアセンブラ
-    * C function を呼ぶこともできる
-* 組込みシステムやOSの記述を目的としている
-* Code Segment, Data Segment という単位でソフトウェアを記述する
+    * 保持すべき状態が明示的になっている
+    * メタ計算は goto の間に計算を挟むことで実現できる

-# Code Segment: 処理の単位
-* 単一 Code Segment ではループを含まないシンプルな処理のみを行なう
+# Code Segment and Data Segment
+* Code Segment は入出力である Input Data Segment と Output Data Segment を持つ
+* 単一 Code Segment はシンプル(purely functional)な処理のみを行なう
 * Code Segment どうしを接続してソフトウェア全体を構築していく
 * 依存のない Code Segment どうしは並列に実行することが可能
-![cs](./images/code_segments.svg){:width="50%"}
+![csds](./images/code_segment_data_segment.svg){:width="50%"}

-# Data Segment: データの単位
-* Code Segment は入出力である Input Data Segment と Output Data Segment を持つ
-* Output Data Segment は接続先の Code Segment の Input になる
-* Code Segment 内部で扱う変数は Data Segment に格納される
-![csds](./images/code_segment_data_segment.svg){:width="50%"}

 # Example of Code Segment in CbC
 * Code Segment は `__code` を付けた関数
 * 次の Code Segment への接続は `goto` で表される

 ```
-__code addTen(int a) {
-    int b = a+10;
-    goto twice(b);
+__code addTen(struct Count c) {
+    struct Port p;
+    p.port = c.x+10;
+    goto twice(p);
 }

-__code twice(int x) {
-    int y = 2*x;
-    goto showValue(y);
+__code twice(struct Port p) {
+    p.x = p.x*2;
+    goto showValue(p);
 }
 ```

-# Example of Data Segment in CbC
-* 各 Code Segment で使うデータの構造体の共用体で表現される
+# CbC のメタ計算
+* Code Segment 間の接続はメタ計算レベルで行なわれる
+* Code Segment で使われる Data Segment は Meta Data Segment である Context に全て定義されている
+* ポインタの扱いや並列実行はメタ計算レベルで行なう
+* メタ計算も Code Segment と Data Segment で表現される
+    * メタレベルではポインタを扱っても良い
+* TODO メタ計算の図

+# CbC のメタ計算の実際
+* プログラムで使用する Data Segment は Meta Data Segment で全て定義されている
 ```
 union Data {
     struct Count {
@@ -79,27 +85,49 @@
     struct Port {
         int port;
     } port;
+}
+
+struct Context {
+    union Data *data;  // Data Segment
+    unsigned int gotoCount; // メタ計算に必要なデータ
+    unsigned int stepOfAddTen;
 };
 ```

+* Meta Code Segment では Data Segment は struct Data という形で一様に処理される
+* メタ計算と通常の計算は stub と meta によって接続される
+```
+__code addTen_stub(struct Context* context) {
+    goto addTen(context, context->data[Count]);
+}
+
+__code addTen(struct Context* context, struct Count c) {
+    struct Port p;
+    p.port = c.x+10;
+    goto meta(context, Twice);
+}
+
+__code twice_stub(struct Context* context) {
+    goto twice(context, countext->data[Port]);
+}
+
+__code twice(struct Context* countext, struct Port p) {
+    p.x = p.x*2;
+    goto meta(context, ShowValue);
+}
+```
+
+* デフォルトの meta
+    * meta を変更することで平行計算や例外処理やソフトウェア検証を行なう
+
+```
+__code meta(struct Context* context, enum Code next) {
+    goto (context->code[next])(context);
+}
+```
+

-# メタ計算による階層化
-* CbC で書いた実装を CbC で検証していく
-    * 仕様記述も CbC で行なう
-    * 仕様のチェックも CbC で行なう
-    * 実装の記述は変更したくない
-    * どこまでがソフトウェア本体でどこまでが実装コード?
-* メタ計算で計算を階層化することで解決する
-    * 実装はノーマルレベル、検証はメタレベル
-    * メタからノーマルは見えて、ノーマルからメタは見えない
-
-# 階層化のメリット
-* メモリ管理などの検証が難しい部分もメタレベルで行なう
-    * 検証するべきノーマルレベルはシンプルになる
-    * ノーマルレベルではポインタが出てこない
-* メモリ管理アルゴリズムの切り替えも楽になる
-
-# Examples of Meta Computation
+# 他の言語でのメタ計算
 * 計算を実現するような計算
 * プログラムを生成するようなプログラム
     * TemplateHaskell in Haskell, Template in C++, Generics
@@ -110,50 +138,18 @@
     * reflection in Java
 * 副作用などの言語処理系に依存した処理を表現する
     * Monad in Haskell
-
-# Meta Code Segment
-* メタ計算は Code Segment の接続部分に Meta Code Segment を入れることで表現できる
-* 仕様定義、仕様検証は Meta Code Segment に記述
-* 実装である Code Segment の検証を行なえば良い
-    * Input Data Segment を作成して正しい Output Data Segment を出すかチェックする
-
-# Meta Data Segment
-* Meta Code Segment に必要なデータを格納する
-* Data Segment より上位の Data Segment
+* CbC では関数呼び出しが存在していないのでメタ計算を挟むことが容易になっている


-# Code of Meta Computation in Continuation based C
-* メタ計算は Code Segment の間に挟まれた Code Segment で行なう
-* 例: Data Segment を指定する Meta Code Segment `twice_stub`
-* ノーマルレベルからはポインタは見えないものとする

-```
-// Code Segment
-__code addTen(union Data* ds, int a) {
-    int b = a+10;
-    goto twice_stub(ds);
-}
-
-// Meta Code Segment
-__code twice_stub(union Data* ds) {
-    goto twice(ds->count.x);
-}
-
-// Code Segment
-__code twice(int x) {
-    int y = 2*x;
-    goto showValue(y);
-}
-```
-
-# Meta Computation Hook in CbC
+# Meta Code Segment を使った実際の検証
 * goto する時に必ず通る Meta Code Segment `meta` を作る
 * `meta` を切り替えることでノーマルレベルの計算を拡張する

 ```
 // Meta Data Segment
 struct Context {
-    union Data *data;  // Data Segment
+    union Data *data;       // Data Segment
     unsigned int gotoCount; // メタ計算に必要なデータ
     unsigned int stepOfAddTen;
 };
@@ -172,18 +168,6 @@
             goto twice_stub(context);
     }
 }
-
-// Code Segment
-__code addTen(struct Context* context, int a) {
-    x = x+10;
-    goto meta(context, Twice);
-}
-
-// Code Segment
-__code twice(struct Context* context, int x) {
-    x = x*2;
-    goto meta(context, ShowValue);
-}
 ```

 # Verification Method of Programs Using Continuation based C
@@ -200,9 +184,10 @@
     * ルートの色は黒である
     * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことはない)
     * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である
+* 仕様: 最も長い経路は最も短い経路の高々2倍に収まる
+* todo 図を入れておこう

 # Verification of Red-Black Tree
-* 仕様: 最も長い経路は最も短い経路の高々2倍に収まる
 * どのような順番で要素が挿入されても常に仕様が満たされることを確認する
 * 仕様を満たさないような挿入順番があればそれを表示する
 * 木への挿入は有限の個数だけ行なわれる