Binary file paper/vmpcbc.pdf has changed

--- a/paper/vmpcbc.tex	Wed Jul 06 17:59:13 2016 +0900
+++ b/paper/vmpcbc.tex	Wed Jul 06 18:34:20 2016 +0900
@@ -499,7 +499,7 @@
 1つの挿入順を列挙後、前の深さの環状リストを再現し、環状リストの先頭を進めることで次の組み合わせを列挙していく。
 
 挿入順を列挙しつつ、木に要素を挿入する度に表\ref{src:specification}の仕様が満たされているか Code Segment を実行して確認する。
-仕様には木の高さが含まれるため、その値を取得する Meta Code Segment が必要である(表\ref{src:getMiHeight})。
+仕様には木の高さが含まれるため、その値を取得する Meta Code Segment が必要である(表\ref{src:getMinHeight})。
 
 % {{{ 木の最も低い高さを取得する Code Segment
 
@@ -559,41 +559,89 @@
 
 このように、Code Segment の検証に必要な仕様や処理は Code Segment で記述することができる。
 akasha におけるメタ計算を用いて、要素数13個まで任意の順で挿入を行なっても仕様が満たされることを検証した。
-
-% writing...
-\section{CBMC を用いた赤黒木の検証}
-C言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いてこの仕様を検証した。
-
-akasha では検証用の仕様と検証用の処理をMeta Code Segmentに定義する。
-挿入順の数え上げには深さ優先探索を用いる。
-CbCには関数呼び出しが存在しないため、深さ優先探索を行なう際にスタックフレームに相当するMeta Data Segmentを自ら用意する。
-各深さ毎の木を保存しておくことで、ある深さまでの探索が終了した際に木を再現ことができ、高速に探索を行なうことができる。
 また、赤黒木の処理内部にバグを追加した際にはakashaは反例を返した。
 
-同じ仕様をC言語の有限モデルチェッカCBMCで検証する。
-CbCは C とほぼ同様の構文を持つため、単純な置換でC言語に変換することができる。
-CbCで記述された赤黒木のコードを置換でC言語に変換し、CBMCで検証を行なった。
-CBMC における仕様は bool を返すコードとして記述するため、akashaと同じ仕様定義を用いることが可能である。
-また、ポインタへの不正アクセスといった一般的なバグへの検証コードが機能として存在する。
-挿入順の数え上げにはCBMCの機能に存在する非決定的な入力を用いた。
-しかし、CBMCで検証できる範囲内ではGearsの赤黒木の仕様を検証することはできなかった。
-有限モデルチェッカでは探索する状態空間を指定し、それを越える範囲は探索しない。
-CBMCで実行可能な最大の状態空間まで探索しても、バグを含んだ赤黒木に対する反例を得ることはできなかった。
+\section{CBMC を用いた赤黒木の検証}
+同様に赤黒木の仕様をC言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いて検証した。
+CBMC は C言語を記号実行し、仕様の否定となるような実行パターンが無いかを検証するツールである。
+
+比較のために全く同じ赤黒木のソースコードを用いたいが、CbCの構文はCとは異なるために変換が必要である。
+CbCはCと似た構文を持つため、\verb/__code/ を \verb/void/ に、 \verb/goto/ を \verb/return/ に置換することで機械的にC言語に変換した。
+
+CBMC における仕様は bool を返す式として記述するため、akashaと同様の仕様定義が利用できる(表\ref{src:specificationCBMC}。
+C では通常の再帰呼び出しができるため、木の高さは関数で確認している。
+assert が true になるような実行パターンを CBMC が見付けると、その実行パターンが反例として出力される。
+
+% {{{ CBMCにおける仕様記述
+
+\begin{table}[ht]
+\begin{lstlisting}
+void verifySpecification(struct Context* context,
+                         struct Tree* tree) {
+    assert(!(maxHeight(tree->root, 1) >
+             2*minHeight(tree->root, 1)));
+    return meta(context, EnumerateInputs);
+}
+\end{lstlisting}
+\caption{CBMCにおける仕様記述}
+\label{src:specificationCBMC}
+\end{table}
+
+% }}}
+
+挿入順の数え上げにはCBMCの機能に存在する非決定的な値 \verb/nondet_int()/ を用いた(表\ref{src:enumerateInputs})。
+検証する有限の要素数回分、ランダムな値を入力させることで挿入順の数え上げとする。
+
+% {{{ CBMCによる挿入順の数え上げ
 
-よって、CBMCでは検証できない範囲の検証をakashaで行なうことが確認できた。
+\begin{table}[ht]
+\begin{lstlisting}
+void enumerateInputs(struct Context* context,
+                     struct Node* node) {
+    if (context->loopCount > LIMIT_OF_VERIFICATION_SIZE) {
+        return meta(context, Exit);
+    }
+
+    node->key     = nondet_int();
+    node->value   = node->key;
+    context->next = VerifySpecification;
+    context->loopCount++;
+
+    return meta(context, Put);
+}
+\end{lstlisting}
+\caption{CBMCによる挿入順の数え上げ}
+\label{src:enumerateInputs}
+\end{table}
+
+% }}}
+
+CBMCでは有限のステップ数だけC言語を記号実行し、その範囲内で仕様が満たされるかを確認する。
+条件分岐や繰り返しなどは展開されて実行される。
+赤黒木検証時にCBMCが扱えた上限である 411 回まで展開を行なっても仕様は満たされていた。
+しかし、赤黒木にバグを追加した際にも仕様の反例を得られず、411回の展開では赤黒木を正しく検証できないことも分かった。
+
+よって、CBMCでは検証できない範囲の検証をakashaで行なえることが確認できた。
+
+% なお、CBMCで検証できなかった理由として、赤黒木がCでなくCbCで記述されていたコードの変換であることが考えられる。
+% CbCの軽量継続では元の環境を破棄するため、スタックフレームが増えない。
+% しかし、Cで記述した場合は末尾最適化をしない限りスタックフレームに関数呼び出し元の情報を残す必要がある。
+% CBMCにおける記号実行時に末尾最適化が行なわれない場合、CBMC内部での状態が非常に多くなってしまった可能性が考えられる。
 
 \section{まとめと今後の課題}
 CbC で記述したプログラムに対する仕様の検証を行なうことができた。
-CbC はCode SegmentとData Segmentを用いてプログラミングするため、検証用にコードを変更することなくメタ計算の切り替えで検証を行なうことができた。
+CbC はCode SegmentとData Segmentを用いてプログラミングすることで、検証用にコードを変更することなく検証を行なうことができた。
 
 今後の課題として、検証できる範囲の拡大や効率化、値の抽象化などがある。
-CBMCではポインタへの不正アクセスを行なう実行例を検出することができる。
+CBMCではポインタへの不正アクセスを行なう実行例を検出する機能が組込みで存在している。
 akashaでも一般的なエラーに対するメタ計算などを定義したい。
 本論文では入力の組み合わせを全探索するため、過去に探索した形状の木に対しても探索を行なっていた。
 木の形状を抽象化することで探索範囲を抑えて高速に検証ができると思われる。
 また、抽象度を上げることで有限回でなく無限回の操作も扱いたい。
 さらに、検証の際に証明を併用することで抽象化や状態数の削減が行なえると考えている。
 
+
+
 \begin{thebibliography}{9}
 
 \bibitem{cite:cbc-clang} 徳森海斗, 河野真治: Continuation based CのLLVM/clang 3.5上の実装について, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2014)