Papers/2018/nozomi-master: paper/akasha.tex comparison

comparison paper/akasha.tex @ 77:50c2d2f1a186

Update chapter akasha

author	atton <atton@cr.ie.u-ryukyu.ac.jp>
date	Wed, 08 Feb 2017 14:27:06 +0900
parents	a9ed6a6dc1f2
children	897fda8e39c5

comparison

equal deleted inserted replaced

-:a9ed6a6dc1f2
+:50c2d2f1a186
 \lstinputlisting[label=src:akasha-meta, caption=検証を行なう CodeSegment の軽量継続] {src/akashaMeta.c}
 % }}}
+% {{{ モデル検査器 CBMC との比較
 \section{モデル検査器 CBMC との比較}
+akasha の比較対象として、 C言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いて赤黒木を検証した。
+CBMC は ANSI-C を記号実行し、仕様の否定となるような実行パターンが無いかを検証するツールである。
+比較のために全く同じ赤黒木のソースコードを用いたいが、CbCの構文は厳密にはCとは異なるために変換が必要である。
+具体的には、\verb/__code/ を \verb/void/ に、 \verb/goto/ を \verb/return/ に置換することで機械的にC言語に変換できる。
+CBMC における仕様は bool を返す式として記述するため、akashaと同様の仕様定義が利用できる(リスト\ref{src:cbmc-assert}。
+assert が true になるような実行パターンを CBMC が見付けると、その実行パターンが反例として出力される。
+\lstinputlisting[label=src:cbmc-assert, caption=CBMC における仕様記述] {src/cbmc-assert.c}
+挿入順の数え上げにはCBMCの機能に存在する非決定的な値 \verb/nondet_int()/ を用いた(リスト\ref{src:enumerate-inputs})。
+この \verb/nondet_int()/ 関数は int の持ちうる値の内から非決定的に値を取得する関数である。
+akasha では有限の要素個分の組み合わせを用いて挿入順の数え上げとしたが、CBMC では要素数回分だけランダムな値を入力させることで数え上げとする。
+\lstinputlisting[label=src:enumerate-inputs, caption= CBMC における挿入順の数え上げ] {src/enumerate-inputs.c}
+CBMCでは有限のステップ数だけC言語を記号実行し、その範囲内で仕様が満たされるかを確認する。
+条件分岐や繰り返しなどは展開されて実行される。
+基本的にはメモリの許す限り展開を行なうことができるが、今回の赤黒木の検証では411回まで展開することができた。
+この411回のうちの実行パスでは赤黒木の仕様は常に満たされる。
+しかし、この展開された回数は挿入された回数とは無関係であり、実際どの程度検証することができたか確認できない。
+実際、赤黒木に恣意的なバグを追加した際にも仕様の反例は得られず、CBMC で扱える範囲内では赤黒木の性質は検証できなかった。
+よって、CBMCでは検証できない範囲の検証を akasha で行なえることが確認できた。
+しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは言いづらい。
+より大きな数を扱っても現実的な速度で検証が行なえる必要がある。
+そのためには記号化なので状態の抽象化や、何らかの機構により状態の削減を行なう必要がある。
+CbC における状態の抽象化の内部表現や、状態を削減するための制約として、型に注目した。
+特に、型を値として利用できる
+% }}}

Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/akasha.tex @ 77:50c2d2f1a186