changeset 14:784913eb2902

Wrote section 3
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 04 Jul 2016 13:59:34 +0900
parents fccf91d337c3
children aab1f02f16e8
files paper/vmpcbc.tex
diffstat 1 files changed, 27 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/paper/vmpcbc.tex	Fri Jul 01 19:36:48 2016 +0900
+++ b/paper/vmpcbc.tex	Mon Jul 04 13:59:34 2016 +0900
@@ -109,22 +109,43 @@
 メタコードセグメントの切り替えは \verb/meta/ の切り替えで表現できる。
 メタデータセグメントはデータセグメントをフィールドに持つ構造体として表現できる。
 
-CbC におけるメタ計算の例にメモリの管理がある。
-メモリの確保やポインタの演算をメタコードセグメントで行なうことで、コードセグメント側ではメモリに由来するエラーを排除することができる。
+CbC におけるメタ計算の例にメモリ管理がある。
+メモリの確保やポインタ演算をメタコードセグメントのみで行なうことで、コードセグメント側ではメモリに由来するエラーを排除することができる。
 また、メタ計算を切り替えることでメモリの管理方法も切り替えることができるため、不要な領域の開放するよう拡張することも容易である。
 
 \section{メタ計算を用いたデータ構造の性質の検証}
-CbC で記述されさデータ構造と、それに対する処理の性質を実際に検証する。
+CbC で記述されさデータ構造と、データ構造に対する処理の性質を実際に検証する。
 検証の対象として、当研究室で CbC を用いて開発している Gears OS における非破壊赤黒木を用いる。
 赤黒木とは木構造を持ったデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。
 また、非破壊であるため木にデータを挿入、削除した際に過去の木は変更されない。
 非破壊赤黒木に求められる性質には、挿入したデータを参照できること、削除できること、値の更新ができること、操作を行なった後の木はバランスしていること、などが存在する。
-本論文ではどのような順番で木に要素を挿入してもバランスしていることを検証する。
+本論文では任意の順番で木に要素を挿入しても木がバランスしていることを検証する。
+
+まず、検証を行なうために満たすべき仕様を定義する。
+仕様はデータ構造が常に満たすべき論理式として表現し、CbC のコードで記述する。
+検証する仕様として、木を根から辿った際に最も長い経路は最も短い経路の高々2倍に収まることを CbC で定義する。
+% TODO code
+定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。
+また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。
 
-% メタ計算で実現するために必要なこと
-% cbmc じゃだめなこと
+当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ cbmc を用いてこの仕様を検証した。
+akasha では検証用の仕様をメタコードセグメントに定義する。
+検証に必要な木の状態の保持や挿入順番の数え上げといった状態の保持はメタデータセグメントが行なう。
+akasha を用いて要素数12個までは任意の順で挿入を行なっても仕様が満たされることを検証した。 % todo: だっけか
+また、赤黒木の処理に恣意的にバグを追加した際には反例をきちんとと返した。
+
+CbCは C とほぼ同じ構文を持つため、単純な置換でC言語に変換することができる。
+CbCで記述された赤黒木のコードを置換でC言語に変換し、cbmcで検証する。
+cbmc における仕様は bool を返すコードとして記述するため、akashaと同じ仕様定義を用いることができる。
+任意の順番での挿入の検証にはcbmcの機能に存在する非決定的な入力を用いた。
+しかし、cbmcで検証できる範囲内では赤黒木の仕様を検証することはできなかった。
+有限モデルチェッカでは探索する状態空間を有限の数で指定し、それを越える範囲は探索しない。
+cbmcで実行可能な最大の状態空間まで探索しても、バグを含んだ赤黒木に対する反例を得ることはできなかった。
 
 \section{まとめと今後の課題}
+% unbounded にする
+% 状態の抽象化
+% 証明を使った空間削減
 
 \begin{thebibliography}{9}
 \bibitem{okumura}