title: メタ計算を用いた Continuation based C の検証手法
author: Yasutaka Higa
profile:
lang: Japanese


# プログラミング言語とソフトウェアの信頼性
* 信頼性の高いソフトウェアを提供したい
* ソフトウェアの仕様を検証するには二つの手法がある
    * プログラムの持つ状態を数え上げ、仕様から外れた状態が無いかを確認するモデル検査
    * プログラムの性質を直接証明してしまう定理証明
* モデル検査も証明も行ないやすい言語として Continuation based C 言語を開発している

# 二つのアプローチを用いたソフトウェア検証
* モデル検査的アプローチ
    * メタ計算ライブラリ akasha による CbC の網羅的な実行
    * 非破壊赤黒木の仕様定義と検証
* 定理証明的なアプローチ
    * 依存型を持つ証明支援系言語 Agda による CbC の証明
    * 部分型を利用して Agda 上に型付きの CbC の項を記述する
    * 型システムを通して CbC の形式的な定義を得る
    * SingleLinkedStack の性質の証明

# モデル検査的アプローチについての流れ
* 既存のモデル検査器について
* Continuation based C (CbC) 言語について
* CbC における CodeSegment と DataSegment を用いたプログラミングスタイル
* CbC とメタ計算について
* CbC で記述された GearsOS とそのデータ構造である赤黒木
* 赤黒木の仕様の定義とその検証手法

# 既存のモデル検査器 spin
* spin
    * promela と呼ばれる言語でプログラムを記述
    * 並列に動作するプログラムの仕様を検証可能
    * 検証した promela から実行可能な C ソースを生成可能
    * 仕様は bool になる式を用いた assert
    * デメリット: promela は C とは記述が異なる

```
assert(x < 10);
```

# 既存のモデル検査器 CBMC
* CBMC
    * 検証対象のCソースを変更しないでも良い
    * C/C++ 言語の記号実行が可能
        * 条件分岐を網羅的に実行
    * 仕様は bool になる式を用いた assert
    * 有限ステップだけ検証する有界モデル検査器

```
assert(x < 10);
```

# Continuation based C
* 当研究室で開発しているプログラミング言語
* アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語
* OS や組み込みソフトウェアなどを対象にしている
* CodeSegment と DataSegment という単位を用いてプログラミングする
* モデル検査と証明の両検証手法をメタ計算として利用可能
    * CbC で CbC 自身を検証可能

# CodeSegment
* CodeSegment とは
    * 処理の単位であり、入力と出力を持つ
    * 結合や分割が容易
* CodeSegment どうしを接続することによりプログラム全体を作る
    * 関数呼び出しと違って戻ってこない(goto)

![cs](./images/cs.svg){:width="50%"}

```
__code cs0(int a, int b){
  goto cs1(a+b);
}
```


# DataSegment
* DataSegment とは
    * データの単位
    * CodeSegment の入出力にあたる
    * 接続元の Output DataSegment は接続先の Input DataSegment

![ds](./images/ds.svg){:width="50%"}

```
__code cs0(int a, int b){
  goto cs1(a+b);
}
```

# メタ計算
* とある計算を実現するための計算
* ネットワーク接続、例外処理、メモリ確保、並列処理など
* CbC は通常レベルの計算とメタ計算を分離して考える
    * 通常レベルではポインタは出てこない、など
* CodeSegment の接続部分に処理を追加することで実現

![meta](./images/meta.svg){:width="50%"}

# Meta CodeSegment
* メタ計算を行なう CodeSegment
* 通常の CodeSegment どうしの接続の間に入る

![mcs](./images/mcs.svg){:width="75%"}

# Meta DataSegment
* メタ計算用の DataSegment
* 通常の DataSegment を含むような DataSegment

![mds](./images/mds.svg){:width="75%"}

# 並列に信頼性高く動作する GearsOS
* CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある
* 並列実行やモデル検査をメタ計算として提供する
* 現在はメモリ管理、Synchronized Queue、非破壊赤黒木などが実装済み
* 今回はこの非破壊赤黒木の検証を行なう

# 赤黒木
* データの保存に用いる二分木
* 特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
    * ルートノードと葉ノードの色は黒
    * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)
    * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定

![rbtree](./images/rbtree.svg){:width="35%"}

# GearsOS における赤黒木の利用例(ノードの挿入)
* 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto
* goto する前に Meta CodeSegment が実行されて木に挿入する


![put](./images/put.svg){:width="50%"}

```
goto meta(context, Put);
```

# 仕様の記述とその確認
* 「バランスが取れている」とは何かを表現できる必要がある
    * 実行可能な CbC の条件式を使った assert になる
* そしてそれを保証したい
    * プログラムの全ての状態においてこれは常に成り立つのか?

# チェックする仕様
* 赤黒木の高さに関する仕様に以下のものがある
    * 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる
* 以下のような条件式を仕様として CbC で定義できる

```
__code verifySpecificationFinish(struct Context* context) {
    if (context->data[AkashaInfo]->akashaInfo.maxHeight >
        2*context->data[AkashaInfo]->akashaInfo.minHeight)
    {
        context->next = Exit;
        goto meta(context, ShowTrace);
    }
    goto meta(context, DuplicateIterator);
}
```

# メタ計算ライブラリ akasha
* メタ計算としてプログラムの状態を数え上げる
    * goto された時に挿入される要素の組み合わせを全て列挙して実行する
        * 赤黒木の状態の保存、挿入、チェック、次の状態の列挙、赤黒木の再現……
    * 挿入する度に仕様の式が成り立つかをチェック
* ノーマルレベルのコードを検証用に変更せず検証可能

![akashaPut](./images/akashaPut.svg){:width="50%"}

# akasha と CBMC の比較
* akasha は有限の要素数の組み合わせをチェックする
    * 要素数が13個までならどの順で木に挿入しても良い
* 比較対象として C Bounded Model Checker を使用した
    * C/C++ の記号実行を行なう
    * 実行可能なステップ数411だけ展開しても仕様は満たされる
    * が、恣意的にバグを入れ込んでも反例を返さない
    * akasha は返した
* 固定の要素数までの仕様検査で十分なのか?

# 定理証明を Continuation based C へ適用するには
* 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
* 直接プログラムの性質を証明
* Coq, Agda, ATS2 などのプログラミング言語で証明が可能
    * 本当は CbC で CbC 自身を証明したい
    * しかし CbC の形式的な定義が無いために今はできない
* Agda 上に CbC を定義することで形式的な定義を得る

# Agda における証明
* Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応
    * 自然演繹: 命題、ならば、かつ、または、で構成される証明システム
* 論理式は型に相当して、証明はその値の導出
* 三段論法の証明は以下のようになる
    * 「((A ならば B) かつ (B ならば C)) ならば (A ならば C)

```
f : {A B C : Set} -> ((A -> B) × (B -> C)) -> (A -> C)
f = \p x -> (snd p) ((fst p) x)
```

# Agda における等式の証明
* Agda では等式も証明できる
    * 依存型という型を変数として扱える型システムを持つ
    * 型を取って型を返す型などが定義可能
* 等式の証明は両方が同じ項に簡約されることを示せば良い
* 自然数の加法の交換法則は以下のようになる

```
addSym : (n m : Nat) -> n + m ≡ m + n
addSym O       O   = refl
addSym O    (S m)  = cong S (addSym O m)
addSym (S n)   O   = cong S (addSym n O)
addSym (S n) (S m) = begin
  (S n) + (S m)  ≡⟨ refl ⟩
  S (n + S m)    ≡⟨ cong S (addSym n (S m)) ⟩
  S ((S m) + n)  ≡⟨ addToRight (S m) n ⟩
  S (m + S n)    ≡⟨ refl ⟩
  (S m) + (S n)  ∎
```

# Agda と DataSegment
* CbC の DataSegment は Agda のレコード型
    * 名前付きの値が複数ある(C の構造体)

```
__code cs0(int a, int b){
  goto cs1(a+b);
}
```
```
record ds0 : Set where
  field
    a : Int
    b : Int
```

# Agda と CodeSegment
* CbC の CodeSegment は、Agda の関数型
    * Input を取って Output を返す

```
__code cs0(int a, int b){
  goto cs1(a+b);
}
```
```
data CodeSegment (A B : Set) : Set where
  cs : (A -> B) -> CodeSegment A B

cs0 : CodeSegment ds0 ds1
cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
```

# メタレベルの型付け
* メタ計算とは通常のレベルとは区別された計算
* 任意の通常のレベルの計算を扱えなくてはならない
    * ライブラリが呼び出されるプログラムは無数にあるようなイメージ
* メタレベルを使うための制約を満たしていれば良い、ということを表現できれば良い
* 部分型を使う
    * Java におけるインターフェース、Haskell における型クラス
    * 「このフィールドXがあればデータ型Tとみなして良い」

# Agda 上のメタ計算
* ノーマルレベルの型を保持したままメタレベルの計算を利用できる
    * cs0 の定義はメタ計算用に変更しなくても良い

```
cs0 : CodeSegment ds0 ds1
cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
```

```
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)})
```

# Agda 上で証明できた性質
* CodeSegment の合成則

```
comp-associative : > (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)
                   -> csComp  c (csComp b a) ≡ csComp  (csComp c b) a
comp-associative (cs _) (cs _) (cs _) = refl
-- c . (b . a) ≡ (c . b) . a
```

* スタックの操作についての性質

```
push-pop-type : ℕ -> ℕ  -> ℕ -> Element ℕ -> Set₁
push-pop-type n e x s = M.exec (M.csComp (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
-- goto (pop . push) mds ≡ mds

n-push-pop-type : ℕ ->  ℕ  -> ℕ -> SingleLinkedStack ℕ -> Set₁
n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop  n) (n-push n)) meta ≡ meta
-- goto (pop*n . push*n) mds ≡ mds
```


# Agda 上に CbC を記述した成果
* 部分型で CbC の型付けができた
* メタ計算をきちんと階層化できた
    * メタ計算にもメタ計算が適用可能
* 赤黒木で利用しているデータ構造スタックの性質を証明できた
    * 任意の回数だけ値を積んで同じだけ取り出すとスタックは変化しない

# まとめ
* Continuation based C 言語を対象にした二種類の検証アプローチ
* モデル検査的なアプローチ
    * 継続を上書きして可能な状態を数え上げるメタ計算ライブラリ akasha を実装
    * 有限の要素数まで検証できた
* 証明的なアプローチ
    * 証明支援系 Agda 上で CbC のプログラムを定義して直接証明
    * 部分型を利用して CbC を型付け
    * データ構造 SingleLinkedStack の証明ができた

# 今後の課題
* より大きなサイズの赤黒木の検証
* 赤黒木の挿入に関する性質を証明する
* 部分型を利用してCbCを型付け
* 依存型をCbC に導入して自身を証明可能にする

# 発表履歴
* Agda 入門.
    * オープンソースカンファレンス 2014 Okinawa, May 2014.
* 形式手法を学び始めて思うことと、形式手法を広めるには(2p).
    * 情報処理学会ソフトウェア工学研究会 (IPSJ SIGSE) ウィンターワークショップ 2015・ イン・宜野湾 (WWS2015), Jan 2015.
* Continuation based C を用いたプログラムの検証手法(6p).
    * 2016 年並列/分散/協調処理に関する『松本』サマー・ワークショップ (SWoPP2016)
    * 情報処理学会・プログラミング研究会 第 110 回プログラミング研究会 (PRO-2016-2) Aug 2016.

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