title: Verification of programs using Code Segments and Data Segments
author: Yasutaka Higa
profile:
lang: Japanese


# 研究目的
* コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
* プログラムはコードセグメントという処理の集合として表され、相互に接続される
* 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する

# 研究内容
* コードセグメントとデータセグメントを用いたプログラムに対し、自動で検証する機構を提案する
* 検証機構には可能な状態を列挙できるモデルチェッカーや、型システムを用いた証明を用いる
* 検証をメタ計算として定義し、通常のプログラムから検証を含んだプログラムを導出する
* メタ計算の形式化には Monad を用い、通常の計算とメタ計算間の一対一対応を保証する

# 近況報告
* atsuki さんの DPP 動くようになりました
* sakura の方から100VMどうですか? って連絡が来てます

# DPP について
* CVS から持ってきて変換しました
* hg/CbC/DPP に mercurial repository を置いています

# DPP in LLVM 3.7
* cbc-clang の 98:88e6d15e811d で動作確認
    * brew install --HEAD ie-developers/ie/cbc
    * export CbC_Clang=/usr/local/Cellar/cbc/HEAD/bin
* くらいです

# 変更点
* code を __code に
* return を __return に
* goto 先が構造体の attribute だと TCE できなくて落ちてた
* 一旦 enum で受けてその先で switch するとできました

# before

```
typedef struct phils {
    int id;
    struct fork *right_fork;
    struct fork *left_fork;
    struct phils *right;
    struct phils *left;
    __code (*next)(struct phils *);
} Phils, *PhilsPtr;
```

```
goto list->phils->next(list->phils,list);
```

* error: tableau : Tail call elimination was failed on codesegment which is accessed by pointer!

# after

```
goto do_action(list->phils, list);
```

```
typedef struct phils {
    int id;
    struct fork *right_fork;
    struct fork *left_fork;
    struct phils *right;
    struct phils *left;
    enum Action next;
} Phils, *PhilsPtr;
```

```
enum Action {
    PutDownLeftFork,
    PutDownRightFork,
    /* ...... */
    PutDownFork
};
```

```
__code do_action(PhilsPtr phils, TaskPtr list)
{
    switch (phils->next) {
        case PutDownLeftFork:
            goto putdown_lfork(phils, list);
        case PutDownRightFork:
            goto putdown_rfork(phils, list);
        /* ....... */
        default:
            printf("invalid action\n");
            exit(1);
    }
    __code (*action) (PhilsPtr, TaskPtr) = thinking;
    goto action(phils, list);
}
```

* で動きました
* Gears がこんな感じで enum で一旦受けて meta で next を決める形

# DPP について
* 実行ファイルが5つできました
    * dpp
        * 1つの philosopher のみが行動(スケジューラなし)
        * 停止しない
    * dpp2
        * 全ての philosopher が順番に行動(スケジューラなし)
        * デッドロックが発生する
    * tableau
        * スケジューラがいて遷移を管理している
        * 乱数の seed が固定値(555)。この値だとデッドロックが発生
    * tableau2
        * tableau に LTL がついてるっぽい
        * デッドロックするので p は満たされないと出る
    * tableau3
        * tableau2 で philosopher に行動が足されてるっぽい
        * 同時にフォークを両方ともおろす
        * p は not valid とのこと

# これから
* Gears の llrb に対して random な値を insert して木のバランスをチェックするように
    * 状態の抽象化?
    * 反例の短縮?

# sakura について
* 「講義用のクラウドについて」
    * date 2016/01/05
    * from nishiura@sakura.ad.jp (Toru Nishiura)
* 先生の提案とかあれば

# sakura についての案とか
* 講義用テンプレートのコピー
* イメージの削除

<!-- vim: set filetype=markdown.slide: -->