\chapter{メタ計算ライブラリ akasha における検証}
\label{chapter:akasha}
第~\ref{chapter:cbc}章では Continuation based C 言語の概要と、CbC で記述された GearsOS について述べた。
GearsOS の持つメタ計算として、モデル検査的なアプローチで CodeGear の仕様を検証していく。

% {{{ モデル検査
\section{モデル検査}
モデル検査とは、ソフトウェアの全ての状態において仕様が満たされるかを確認するものである。
このモデル検査を行なうソフトウェアをモデル検査器と呼ぶ。
モデルは検査器は、仕様の定義と確認ができる。
加えて、仕様を満たさない場合にはソフトウェアがどのような状態であったか反例を返す。

モデル検査器には Spin\cite{spin} やCBMC\cite{cbmc} などが存在する。

Spin は Promela と呼ばれる言語でモデルを記述し、その中に論理式として仕様を記述する。
論理式は assert でモデルの内部に埋め込まれ、並列に実行してもその仕様が満たされるかをチェックする。
また、Promela で記述されたモデルからC言語を生成することができる。
しかし、Promela で記述されたモデルは元のC言語とはかなり異なる構文をしており、ユーザが記述する難易度が高い。

そこで、モデルを個別に記述せずに実装そのものを検査するアプローチがある。
例えばモデル検査器 CBMC は C言語を直接検証できる。
CBMC でも仕様は論理式で記述され、 assert と組み合わせる。
C 言語の実行は通常の実行とは異なり、記号実行という形で実行される。
プログラム上の変数は記号として処理され、\verb/a < b/ といった条件式により分岐が行なわれたのなら、その条件を持つ場合の経路、持たない場合の経路、と分岐していくのである。

GearsOS におけるモデル検査的なアプローチはCBMC のように実装言語をそのまま検証できるようにしたい。
そのために、assert を利用した仕様の定義と、その検査、必要なら反例を提出するようなメタ計算を定義する。
このメタ計算をメタ計算ライブラリ akasha として実装した。

この章では、メタ計算ライブラリ akasha を用いて GearsOS のデータ構造を検証していく。
% }}}

% {{{ GearsOS における非破壊赤黒木
\section{GearsOS における非破壊赤黒木}
現状の GearsOS に実装されているメタ計算として、非破壊赤黒木が存在する。
非破壊赤黒木はユーザがデータを保存する際に利用することを想定している。
メタ計算として定義することで、ノーマルレベルからは木のバランスを考慮せず木への操作が行なえる。

なお、赤黒木とは二分探索木の一種であり、木のバランスを取るための情報として各ノードは赤か黒の色を持っている。

二分探索木の条件は以下である。

\begin{itemize}
    \item 左の子孫の値は親の値より小さい
    \item 右の子孫の値は親の値より大きい
\end{itemize}

加えて、赤黒木が持つ具体的な条件は以下のものである。

\begin{itemize}
    \item 各ノードは赤か黒の色を持つ。
    \item ルートノードの色は黒である。
    \item 葉ノードの色は黒である。
    \item 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)。
    \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。
\end{itemize}


数値を要素に持つ赤黒木の例を図\ref{fig:rbtree}に示す。
条件に示されている通り、ルートノードは黒であり、赤ノードは連続していない。
加えて各最下位ノードへの経路に含まれる黒ノードの個数は全て2である。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=0.5]{fig/rbtree.pdf}
        \caption{赤黒木の例}
        \label{fig:rbtree}
    \end{center}
\end{figure}

赤黒木の持つ条件を言い変えるのなら、「木をルートから辿った際に最も長い経路は最も短い経路の高々二倍に収まる」とも言える。
この言い換えは「赤が続くことはない」という条件と「ルートから最下位への経路の黒ノードはどの最下位ノードでも同じ」であることから導ける。
具体的には、最短経路は「黒のみの経路」であり、最長経路は「黒と赤が交互に続く経路」となる。
この条件を言い変えた性質を仕様とし、検証していく。

GearsOS で実装されている赤黒木は特に非破壊赤黒木であり、一度構築した木構造は破壊される操作ごとに新しい木構造が生成される。
非破壊の性質を付与した理由として、並列実行時のデータの保存がある。
同じ赤黒木をロックせずに同時に更新した場合、ノードの値は実行順に依存したり、競合したりする。
しかし、ロックを行なって更新した場合は同じ木に対する処理に待ち合わせが発生し、全体の並列度が下がる。
この問題に対し GearsOS では、各スレッドは処理を行なう際には非破壊の木を利用することで並列度は保ち、値の更新が発生する時のみ木をアトミックな操作で置き換えることで競合を回避する。
具体的には木の操作を行なった後はルートのノードを元に CAS で置き換え、失敗した時は木を読み込み直して処理を再実行する。
CAS(Check and Set) とは、アトミックに値を置き換える操作であり、使う際は更新前の値と更新後の値を渡す。
CAS で渡された更新前の値が、保存している値と同じであれば競合していないために値の更新に成功し、異なる場合は他に書き込みがあったことを示すために値の更新が失敗する操作のことである。

非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、変更後に新たなルートノードとする。
この際に変更が行なわれていない部分は変更前の木と共有する(図\ref{fig:non-destructive-rbtree})。
これは一度構築された木構造は破壊されないという非破壊の性質を用いたメモリ使用量の最適化である。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[scale=0.5]{fig/non-destructive-rbtree}
        \caption{非破壊赤黒木の編集}
        \label{fig:non-destructive-rbtree}
    \end{center}
\end{figure}

CbC を用いて赤黒木を実装する際の問題として、関数の呼び出しスタックが存在しないことがある。
C における実装では関数の再帰呼び出しによって木が辿るが、それが行なえない。
経路を辿るためには、ノードに親への参照を持たせるか、挿入や削除の際に辿った経路を記憶する必要がある。
ノードが親への参照を持つ非破壊木構造は共通部分の共有が行なえないため、経路を記憶する方法を使う。
経路の記憶にはスタックを用い、スタックは Meta DataSegment に保持する。

赤黒木を格納する DataSegment と Meta DataSegment の定義をリスト\ref{src:rbtree-context}に示す。
経路の記憶に用いるスタックは Meta DataSegment である Context 内部の \verb/node_stack/ である。
DataSegment は各ノード情報を持つ \verb/Node/構造体と、赤黒木を格納する \verb/Tree/構造体、挿入などで操作中の一時的な木を格納する \verb/Traverse/共用体などがある。

\lstinputlisting[label=src:rbtree-context, caption=赤黒木の DataSegment と Meta DataSegment] {src/rbtreeContext.h}

Meta DataSegment を初期化する Meta CodeSegment initLLRBContext をリスト\ref{src:init-rbtree-context}に示す。
この Meta CodeSegment ではメモリ領域の確保、CodeSegment 名と CodeSegment の実体の対応表の作成などを行なう。
メモリ領域はプログラムの起動時に一定数のメモリを確保し、ヒープとして \verb/heap/ フィールドに保持させる。
CodeSegment 名と CodeSegment の実体との対応は、enum で定義された CodeSegment 名の添字へと CodeSegment の関数ポインタを代入することにより持つ。
例えば \verb/Put/ の実体は \verb/put_stub/ である。
他にも DataSegment の初期化(リスト\ref{src:init-rbtree-context} 34-48)とスタックの初期化(リスト\ref{src:init-rbtree-context} 50-51)を行なう。

\lstinputlisting[label=src:init-rbtree-context, caption=赤黒木の Meta DataSegment の初期化を行なう Meta CodeSegment ] {src/initLLRBContext.c}

実際の赤黒木の実装に用いられている Meta CodeSegment の一例をリスト\ref{src:rbtree-insert-case-2}に示す。
Meta CodeSegment \verb/insertCase2/ は要素を挿入した場合に呼ばれる Meta CodeSegment の一つであり、親ノードの色によって処理を変える。
まず、色を確認するために経路を記憶しているスタックから親の情報を取り出す。
親の色が黒ならば処理を終了し、次の CodeSegment へと軽量継続する(リスト\ref{src:rbtree-insert-case-2} 5-8)。
親の色が赤であるならばさらに処理を続行して \verb/InsertCase3/ へと軽量継続する。
ここで、経路情報を再現するためにスタックへと親を再代入してから軽量継続を行なっている。
なお、Meta CodeSegment でも Context から DataSegment を展開する処理は stub によって行なわれる(リスト\ref{src:rbtree-insert-case-2} 14-16)。

\lstinputlisting[label=src:rbtree-insert-case-2, caption=赤黒木の実装に用いられている Meta CodeSegment例] {src/insertCase2.c}

% }}}

% {{{ メタ計算ライブラリ akasha を用いた赤黒木の実装の検証

\section{メタ計算ライブラリ akasha を用いた赤黒木の実装の検証}
赤黒木の仕様の定義とその確認を CbC で行なっていく。
仕様には赤黒木の利用方法などによっていくつかのものが考えられる。
赤黒木に対する操作の仕様と、その操作によって保証されるべき赤黒木の状態を示すと以下のようになる。

\begin{itemize}
    \item 挿入したデータは参照できること
    \item 削除したデータは参照できないこと
    \item 値を更新した後は更新された値が参照されること
    \item 操作を行なった後の木はバランスしていること
\end{itemize}

今回はバランスに関する仕様を確認する。
操作を挿入に限定し、どのような順番で要素を挿入しても木がバランスすることを検証する。
検証には当研究室で開発しているメタ計算ライブラリ akasha を用いる。

akasha では仕様は常に成り立つべき CbC の条件式として定義される。
具体的には Meta CodeSegment に定義した assert が仕様に相当する。
仕様の例として「木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる」という式を定義する(リスト\ref{src:assert})。

\lstinputlisting[label=src:assert, caption=木の高さに関する仕様記述] {src/assert.c}

リスト\ref{src:assert} で定義した仕様がプログラムの持つ全ての状態に成り立つかを確認する。
また、成り立たない場合には仕様に反する状態を反例として提出する。

まずは最も単純な検証として要素数を有限に固定し、その挿入順番を数え上げる。
最初に、検証の対象となる赤黒木と、検証に必要な DataSegment を含む Meta DataSegment を定義する(リスト\ref{src:akasha-context})。
これが akasha のレベルで利用する Meta DataSegment である。
赤黒木自体はユーザから見るとメタレベル計算であるが、今回はその実装の検証するため、赤黒木がノーマルレベルとなる。
よって akasha はメタメタレベルの計算とも考えられる。

% TODO: meta meta の図

akasha が使う DataSegment は データの挿入順を数え上げるためには使う環状リスト \verb/Iterator/ とその要素 \verb/IterElem/、検証に使う情報を保持する \verb/AkashaInfo/、木をなぞる際に使う \verb/AkashaNode/ がある。

\lstinputlisting[label=src:akasha-context, caption=検証を行なうための Meta DataSegment] {src/akashaContext.h}

挿入順番の数え上げには環状リストを用いた深さ優先探索を用いる。
最初に検証する要素を全て持つ環状リストを作成し、木に挿入した要素を除きながら環状リストを複製していく。
環状リストが空になった時が組み合わせを一つ列挙し終えた状態となる。
列挙し終えた後、前の深さの環状リストを再現してリストの先頭を進めることで異なる組み合わせを列挙する。

仕様には木の高さが含まれるので、高さを取得する Meta CodeSegment が必要となる。
リスト\ref{src:get-min-height}に木の最も低い経路の長さを取得する Meta CodeSegment を示す。

木を辿るためのスタックに相当する \verb/AkshaNode/を用いて経路を保持しつつ、高さを確認している。
スタックが空であれば全てのノードを確認したので次の CodeSegment へと軽量継続を行なう。
空でなければ今辿っているノードが葉であるか確認し、葉ならば高さを更新して次のノードを確認するため自身へと軽量継続する。
葉でなければ高さを1増やして左右の子をスタックに積み、自身へと軽量継続を行なう。

\lstinputlisting[label=src:get-min-height, caption=木の最も短かい経路の長さを確認する Meta CodeSegment] {src/getMinHeight.c}

同様に最も高い高さを取得し、仕様であるリスト\ref{src:assert}の assert を挿入の度に実行する。
assert は CodeSegment の結合を行なうメタ計算である \verb/meta/ を上書きすることにより実現する。

% TODO: 図

\verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。
検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続である(リスト\ref{src:meta})。

\lstinputlisting[label=src:meta, caption=通常の CodeSegment の軽量継続] {src/meta.c}

これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。
検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。
実際の検証部分は \verb/PutAndGoToNextDepth/ の後に行なわれるため、直接は記述されていない。
この \verb/meta/ が行なうのは検証用にメモリの管理である。
状態の数え上げを行なう際に状態を保存したり、元の状態に戻す処理が行なわれる。
このメタ計算を用いた検証では、要素数13個までの任意の順で挿入の際に仕様が満たされることを確認できた。
また、赤黒木の処理内部に恣意的なバグを追加した際には反例を返した。

\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 における状態の抽象化の内部表現や、状態を削減するための制約として、型に注目した。
特に、型を値として利用できる

% }}}