Binary file paper/vmpcbc.pdf has changed

--- a/paper/vmpcbc.tex	Wed Jul 06 14:56:42 2016 +0900
+++ b/paper/vmpcbc.tex	Wed Jul 06 16:04:51 2016 +0900
@@ -290,19 +290,73 @@
 通常の計算を保存するようメタ計算を定義することで、例外処理などを含む計算に拡張することができる\cite{cite:monad}。
 
 \section{CbC で記述した赤黒木}
-// TODO
+CbC で記述されたデータ構造に赤黒木がある。
+赤黒木とは木構造のデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。
+赤黒木は通常の二分探索木としての条件の他に以下の条件を持つ。
+
+\begin{itemize}
+    \item 各ノードは赤または黒の色を持つ。
+    \item ルートの色は黒である。
+    \item 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことはない)。
+    \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。
+\end{itemize}
+
+これらの条件により、木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる。
+
+赤黒木の実装として、当研究室で CbC を用いて開発している Gears OS \cite{cite:gears-os} における非破壊赤黒木がある。
+非破壊赤黒木とは木への挿入や削除を行なった際に一度構築した木構造を破壊することなく新しく木構造を生成する赤黒木である。
+非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、上に存在しないノードは変更前元の木構造と共有することで実現できる。
+
+%TODO figure
+
+関数呼び出しが可能な言語では戻り値で経路を辿ることか可能だが、CbC はgotoによる軽量継続のみで記述する必要があるため、経路を辿るにはノードに親への参照を持たせるか挿入・削除時に辿った経路を記憶するしかない。
+ノードが親への参照を持つ非破壊木構造は構築出来ないため、辿った経路を記憶する方法を用いる。
+辿った経路を記憶するため Meta Data Segment にスタックを持たせる。
+このスタックは軽量継続ではなく関数呼び出しで利用する。
+
+赤黒木の赤が続かないという制約をチェックする Code Segment は表\ref{src:rbtree}のようになる。
+まず、親の情報が必須なために経路を記憶しているスタックから親の情報を取得する。
+親の色が黒である場合は木が平衡であるために処理を終了し、ユーザ側のCode Segment へと \verb/goto/ する。
+親の色が赤である場合は経路情報を再現するためにスタックへと親を挿入し、次の条件判定へと \verb/goto/ する。
+
+\begin{table}
+\begin{lstlisting}
+
+// Meta Code Segment
+__code insertCase2(struct Context* context, struct Node* current) {
+    struct Node* parent;
+    stack_pop(context->node_stack, &parent);
+    if (parent->color == Black) {
+        stack_pop(context->code_stack, &context->next);
+        goto meta(context, context->next);
+    }
+    stack_push(context->node_stack, &parent);
+    goto meta(context, InsertCase3);
+}
+
+// Meta Meta Code Segment
+__code insert2_stub(struct Context* context) {
+    goto insertCase2(context, context->data[Traverse]->traverse.current);
+}
+\end{lstlisting}
+    \caption{赤黒木の赤が続かないという制約の判定}
+    \label{src:rbtree}
+\end{table}
+
+ここで、赤黒木に対する処理を Code Segment とした場合、赤黒木のメモリ管理などは Meta Code Segment である。
+赤黒木を利用する Code Segment からは赤黒木の処理は意識する必要がないため、赤黒木の処理はMeta Code Segment のように見え、赤黒木のメモリ管理は Meta Meta Code Segment と考えられる。
+このようにメタ計算は階層構造を持つため、任意の Code Segment に対してメタ計算を適用することが可能であり、検証機構の検証なども行なうことができる。
+
 
 \section{メタ計算を用いたデータ構造の性質の検証}
-CbC で記述されたデータ構造と、データ構造に対する処理の性質を実際に検証する。
-検証の対象として、当研究室で CbC を用いて開発している Gears OS \cite{cite:gears-os}における非破壊赤黒木を用いる。
-赤黒木とは木構造を持ったデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。
+CbC で記述された赤黒木と、それに対する処理の性質を実際に検証する。
 また、非破壊であるため木にデータを挿入、削除した際に過去の木は変更されない。
 非破壊赤黒木に求められる性質には、挿入したデータを参照できること、削除できること、値の更新ができること、操作を行なった後の木はバランスしていること、などが存在する。
 本論文では任意の順番で木に要素を挿入しても木がバランスしていることを検証する。
 
 まず、検証を行なうために満たすべき仕様を定義する。
 仕様はデータ構造が常に満たすべき論理式として表現し、CbC のコードで記述する。
-検証する仕様として、木を根から辿った際に最も長い経路は最も短い経路の高々2倍に収まることを CbC で定義する(Code\ref{src:specification})。
+検証する仕様として、とを CbC で定義する(Code\ref{src:specification})。
 
 \begin{lstlisting}[label=src:specification, caption=s]% 木の高さの仕様記述]
 
@@ -317,6 +371,7 @@
 また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。
 
 当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いてこの仕様を検証した。
+-
 akasha では検証用の仕様と検証用の処理をMeta Code Segmentに定義する。
 挿入順の数え上げには深さ優先探索を用いる。
 CbCには関数呼び出しが存在しないため、深さ優先探索を行なう際にスタックフレームに相当するMeta Data Segmentを自ら用意する。