Binary file paper/vmpcbc.pdf has changed

--- a/paper/vmpcbc.tex	Wed Jul 06 18:58:49 2016 +0900
+++ b/paper/vmpcbc.tex	Wed Jul 06 19:40:01 2016 +0900
@@ -39,39 +39,15 @@
 \begin{document}
 
 % ipsjpro
-%     llrb の実装を書いても良い
-%         stack の話とか
-%     どうやって akasha で検証しているか
 %     cbmc でできなかった理由とかも書く
 %         実際はフェアじゃないし
 %
 % --- たけだくんから ---
 % Attonさん
 %
-% オブジェクトレベルがないとのだれも論文はわからない
-% meta levelの話がいきなり来ている
-% stub
-%
-% どれがメタでどれがオブジェクトがちゃんと書いたほうがいい
-%
-% メタとstubの関係
-% 今のred black treeがあんまり綺麗に書かれてないのがそもそも問題
-% sm
-% new smvとかちゃんと知ってますよと書いたほうがいいかも・・・
-%
-% 同じようなことをやってる人の論文を見るといいかも
-% 背景などもわかるかも
-%
 % Treeの大きさがどれくらいなのかという図
 % CBCで書かれたRed black Treeも書いた方がいい
 %
-% 検証できる範囲を検証できなかったというのはおかしい
-%
-% うりとしては実コードで検証できる
-% 挿入する要素数がある程度あれば
-%
-% Treeeをランダムに生成する
-%
 % なぜswitchを入れている？
 % セグフォした時に前のコードがわからない
 % ー＞デバッグ用のコード
@@ -79,8 +55,6 @@
 % 次のためにみたいなので
 % const struct Node* node = akashaInfo -> akashaNode-> Node;の go toの部分
 %
-% red black treeで2ページぐらいでスタックの部分ももりもり書いてもいい
-%
 % なぜcbcで苦労して書くのか？
 % toy program的なのを書きたい
 %
@@ -137,13 +111,14 @@
 \section{ソフトウェアの検証}
 ソフトウェアの規模が大きくなるにつれ、バグは発生しやすくなる。
 バグとはソフトウェアが期待される動作とは異なる動作を行なうことである。
-また、ソフトウェアの期待される動作を定義したものは仕様と呼ばれ、自然言語や論理で記述される。
+ソフトウェアの期待される動作は仕様と呼ばれ、自然言語や論理で記述される。
 検証とは、ソフトウェアが定められた環境下において仕様を満たすことを保証するものである。
-ソフトウェアが仕様を満たすことを保証する手法として、定理証明とモデル検査がある。
-定理証明はプログラムが満たすべき仕様を論理式で記述し、その式が常に真であることを証明する。
-定理証明を行なう言語には Agda\cite{cite:agda} や Coq\cite{cite:coq} などが存在する。
-モデル検査を行なうモデル検査器には、 promela と呼ばれる言語でモデルを記述する spin\cite{cite:spin} やモデルを状態遷移系で記述する NuSMV\cite{cite:nusmv} 、C言語を記号実行することができる CBMC\cite{cite:cbmc} などが存在する。
-証明やモデル検査器で検証を行なう際、実際に動作するコードでなく証明用にコードを書き直す必要があるなど、実際の実装との乖離が存在する。
+ソフトウェアの検証手法には、定理証明とモデル検査がある。
+定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その式が常に真であることを証明する。
+定理証明を行なう言語には依存型で証明を行なう Agda\cite{cite:agda} や Coq\cite{cite:coq} などが存在する。
+モデル検査はソフトウェアのモデルの全ての状態において仕様が満たされるかを確認するものである。
+モデル検査を行なうモデル検査器には、 promela と呼ばれる言語でモデルを記述する spin\cite{cite:spin} やモデルを状態遷移系で記述する NuSMV\cite{cite:nusmv} 、ANSI-Cを記号実行することができる CBMC\cite{cite:cbmc} などが存在する。
+証明やモデル検査器で検証を行なう際、実際に動作するコードでなく検証用にコードを書き直す必要があるなど、実際の実装との乖離が存在する。
 よって、検証した環境では仕様が満たされていても、実装にバグが入り込み信頼性を保証できない可能性がある。
 本研究は実際に動作するプログラムの信頼性を保証することを目的とする。
 
@@ -179,7 +154,7 @@
 プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたCode Segmentを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。
 
 \section{Continuation based C}
-Code SegmentとData Segmentを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cite:cbc-clang} 言語が存在する。
+Code SegmentとData Segmentを用いたプログラミングスタイルで記述する言語に Continuation based C\cite{cite:cbc-clang} 言語が存在する。
 Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。
 CbC におけるCode SegmentはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。
 Code Segmentどうしの接続は goto による軽量継続で表される(表\ref{src:simpleCs})。
@@ -207,7 +182,7 @@
 
 CbCにおけるCode Segmentは、C言語の関数宣言の返り値の型の部分に \verb/__code/ を記述して定義する。
 Code Segment内部には変数の宣言やif文による分岐といったC言語の文法を用いて処理を記述する。
-表\ref{src:simpleCs}の例では、2つのCode Segment \verb/addTen/ と \verb/twice/を定義している。
+表\ref{src:simpleCs}の例では、\verb/addTen/ と \verb/twice/という2つのCode Segmentを定義している。
 \verb/addTen/では int の値を受けとり、10加算して \verb/twice/ を実行する。
 \verb/twice/ では受けとったintの値を2倍して \verb/showValue/ を実行する。
 
@@ -232,7 +207,8 @@
 % }}}
 
 表\ref{src:simpleDs}ではData Segmentとして int を持つ count と unsigned int を持つ port の2つを定義している。
-Code Segment 内部では演算やポインタ演算は行なわず、メタ計算部分でポインタへの演算を行なう。
+
+Code Segment 内部では演算やポインタ演算は行なわず、メタ計算でポインタへの演算を行なう。
 これにはメモリ管理をメタ計算部分に分離することで、プログラムを検証しやすくするねらいがある。
 Code Segment がどの Data Segment にアクセスするかといった指定も Meta Code Segment で行なう(表\ref{src:stub} における \verb/twice_stub/)。
 CbC における Meta Code Segment は Code Segment と Code Segment 間に存在する Code Segment である。
@@ -263,11 +239,11 @@
 
 % }}}
 
-CbC における Meta Data Segment は Data Segment を内包する構造体として定義できる(表\ref{src:meta} における Context)。
-また、goto する際に必ず通る Meta Code Segment を定義することで、 Code Segment どうしの接続もメタ計算として定義できる(表\ref{src:meta} における \verb/meta/)。
+CbC における Meta Data Segment は Data Segment を内包する構造体として定義できる(表\ref{src:meta} の Context)。
+また、goto する際に必ず通る Meta Code Segment を定義することで、 Code Segment どうしの接続もメタ計算として定義できる(表\ref{src:meta} の \verb/meta/)。
 \verb/meta/ を切り替えることで Code Segment を変更することなくメタ計算のみを変更することができる。
 
-% {{{ Code Segment を接続するメタ計算メタ計算として接続した例
+% {{{ メタ計算を用いてCode Segment を接続する例
 
 \begin{table}[ht]
 \begin{lstlisting}
@@ -303,16 +279,16 @@
     goto meta(context, ShowValue);
 }
 \end{lstlisting}
-\caption{Code Segment を接続するメタ計算メタ計算として接続した例}
+\caption{メタ計算を用いてCode Segment を接続する例}
 \label{src:meta}
 \end{table}
 
 % }}}
 
-メタ計算の例として、メモリ管理の他にも例外処理や並列実行やネットワークアクセスなどがある。
+メタ計算の例として、メモリ管理の他にも例外処理や並列実行、ネットワークアクセスなどがある。
 通常の計算を保存するようメタ計算を定義することで、例外処理などを含む計算に拡張することができる\cite{cite:monad}。
 
-\section{CbC で記述した赤黒木}
+\section{CbC で記述した非破壊赤黒木}
 CbC で記述されたデータ構造に赤黒木がある。
 赤黒木とは木構造のデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。
 赤黒木は通常の二分探索木としての条件の他に以下の条件を持つ。
@@ -326,9 +302,9 @@
 
 これらの条件により、木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる。
 
-赤黒木の実装として、当研究室で CbC を用いて開発している Gears OS \cite{cite:gears-os} における非破壊赤黒木がある。
-非破壊赤黒木とは木への挿入や削除を行なった際に一度構築した木構造を破壊することなく新しく木構造を生成する赤黒木である。
-非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、上に存在しないノードは変更前元の木構造と共有することで実現できる(図\ref{fig:tree})。
+赤黒木の実装として、当研究室で CbC を用いて開発している Gears OS \cite{cite:gears-os} における非破壊赤黒木\cite{cite:rbtree}がある。
+非破壊赤黒木とは木への挿入や削除を行なった際、一度構築した木構造を破壊せず新しく木構造を生成する赤黒木である。
+非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、上に存在しないノードは変更前元の木構造と共有することである(図\ref{fig:tree})。
 
 \begin{figure}[ht]
     \begin{center}
@@ -338,9 +314,9 @@
     \end{center}
 \end{figure}
 
-関数呼び出しが可能な言語では戻り値で経路を辿ることか可能だが、CbC はgotoによる軽量継続のみで記述する必要があるため、経路を辿るにはノードに親への参照を持たせるか挿入・削除時に辿った経路を記憶するしかない。
+関数呼び出しが可能な言語では戻り値で経路を辿ることか可能だが、CbC は \verb/goto/による軽量継続のみで記述する必要があるため、経路を辿るにはノードに親への参照を持たせるか挿入・削除時に辿った経路を記憶するしかない。
 ノードが親への参照を持つ非破壊木構造は構築出来ないため、辿った経路を記憶する方法を用いる。
-辿った経路を記憶するため Meta Data Segment にスタックを持たせる(表\ref{src:stack}における Context)。
+辿った経路を記憶するため Meta Data Segment にスタックを持たせる(表\ref{src:stack}における Context 内部の \verb/node_stack/)。
 なお、このスタックは軽量継続ではなく関数呼び出しで利用している。
 赤黒木で利用する Data Segment を表\ref{src:stack}に表す。
 Data Segment は各ノードの情報を持つ \verb/Node/ と赤黒木を格納する \verb/Tree/と、挿入などの操作中の一時的な木を持つ\verb/Traverse/の共用体で表される。
@@ -382,10 +358,10 @@
 
 % }}}
 
-赤黒木の赤が続かないという制約をチェックする Code Segment は表\ref{src:rbtree}のようになる。
-まず、親の情報が必須なために経路を記憶しているスタックから親の情報を取得する。
+CbCによる赤黒木実装の例として、赤が続かないという制約をチェックする Code Segment を表\ref{src:rbtree}に示す。
+まず、赤が連続するか判定するために親の情報が必須なため、経路を記憶しているスタックから親の情報を取得する。
 親の色が黒である場合は木が平衡であるために処理を終了し、ユーザ側のCode Segment へと \verb/goto/ する。
-親の色が赤である場合は経路情報を再現するためにスタックへと親を挿入し、次の条件判定へと \verb/goto/ する。
+親の色が赤である場合は次の条件判定へと \verb/goto/ するが、経路情報を再現するためにスタックへと親を再度挿入しつつ \verb/goto/ する。
 
 % {{{ 赤黒木で赤のノードが続かないという制約の判定
 
@@ -420,7 +396,8 @@
 
 \section{メタ計算を用いた赤黒木の検証}
 CbC で記述された赤黒木と、それに対する処理の性質を実際に検証していく。
-非破壊赤黒木に求められる性質には以下のようなものがある
+赤黒木に求められる性質には以下のようなものがある
+
 \begin{itemize}
     \item 挿入したデータを参照できるこ
     \item 挿入したデータを削除できること
@@ -430,7 +407,7 @@
 
 本論文では操作を挿入に限定し、任意の順で木に要素を挿入しても木がバランスすることを検証する。
 検証には当研究室で開発している検証用メタ計算ライブラリ akasha を用いる。
-akasha では仕様を Meta Code Segment として記述するため、CbCで常に真となるべき式として定義する
+akasha では仕様を Meta Code Segment に記述するため、CbCで常に真となる式として定義する
 赤黒木の性質である、 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まることをCbCのコードで記述する(表\ref{src:specification})。
 
 % {{{ 木の高さの仕様記述
@@ -448,10 +425,10 @@
 
 % }}}
 
-表\ref{src:specification}で定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。
+表\ref{src:specification}で定義した仕様が常に成り立つか、全ての挿入順の組み合わせを列挙しながら確認していく。
 無限回の挿入順番を数え上げることは状態の抽象化無しには不可能なので、限られた要素数の挿入を検証する。
-検証の対象である赤黒木を内包する Meta Data Segment を定義し、挿入順の検証に必要なデータを追加で定義する(表\ref{src:akashaDs})。
-必要なデータには挿入順の数え上げに使う環状リスト \verb/Iterator/ とその要素 \verb/IterElem/、検証に使う情報を保持する \verb/AkashaInfo/、木をなぞる際に使う \verb/AkashaNode/がある。
+検証の対象である赤黒木を内包する Meta Data Segment を定義し、挿入順の列挙に必要なデータを追加で定義する(表\ref{src:akashaDs})。
+検証に必要なデータには挿入順の数え上げに使う環状リスト \verb/Iterator/ とその要素 \verb/IterElem/、検証に使う情報を保持する \verb/AkashaInfo/、木をなぞる際に使う \verb/AkashaNode/がある。
 
 % {{{ akasha の Data Segment
 \begin{table}[ht]
@@ -493,12 +470,12 @@
 
 % }}}
 
-挿入順の数え上げには深さ優先探索を用いるが、CbCスタックフレームが無いために再帰では記述できず、データ構造に今の状態を保持させながら探索する必要がある。
-検証する要素を全て持つ環状リストを作成し、木に一度挿入する度に環状リストを複製する。
-複製を行なった際に挿入した要素を削除し、全ての要素が無くなることで1つの挿入順の探索を終了する。
-1つの挿入順を列挙後、前の深さの環状リストを再現し、環状リストの先頭を進めることで次の組み合わせを列挙していく。
+挿入順の数え上げには深さ優先探索を用いるが、CbCスタックフレームが無いために再帰では記述できず、データ構造に今の状態を保持させながら探索する。
+検証する要素を全て持つ環状リストを作成し、木に一度挿入する度に挿入した要素を排除した環状リストを複製していく。
+環状リストに全ての要素が無くなった時、1つの組み合わせを列挙したことになる。
+1つの挿入順を列挙後、前の深さの環状リストを再現し、環状リストの先頭を進めることで組み合わせの列挙を続ける。
 
-挿入順を列挙しつつ、木に要素を挿入する度に表\ref{src:specification}の仕様が満たされているか Code Segment を実行して確認する。
+挿入順を列挙しつつ、木に要素を挿入する度に表\ref{src:specification}の仕様が成り立つか Code Segment を実行して確認する。
 仕様には木の高さが含まれるため、その値を取得する Meta Code Segment が必要である(表\ref{src:getMinHeight})。
 
 % {{{ 木の最も低い高さを取得する Code Segment
@@ -553,8 +530,9 @@
 % }}}
 
 木をなぞるためのスタックに相当する \verb/AkashaNode/ を用いてノードを保持しつつ、高さを確認している。
-スタックが空であれば全てのノードをなぞったので最も高い高さを取得するために \verb/goto/する。
-空でなければ今なぞっているノードが葉であるか確認し、葉ならば高さを更新し、スタックからノードを1つ破棄して自身に \verb/goto/する。
+スタックが空であれば全てのノードをなぞったので、次の処理へと \verb/goto/する。
+空でなければ今なぞっているノードが葉であるか確認する。
+葉ならば高さを更新し、スタックからノードを1つ破棄して自身に \verb/goto/する。
 葉でなければ高さを1つ増やしながらスタックに左右の子供を積み、自身に \verb/goto/ する。
 
 このように、Code Segment の検証に必要な仕様や処理は Code Segment で記述することができる。
@@ -563,13 +541,13 @@
 
 \section{CBMC を用いた赤黒木の検証}
 同様に赤黒木の仕様をC言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いて検証した。
-CBMC は C言語を記号実行し、仕様の否定となるような実行パターンが無いかを検証するツールである。
+CBMC は ANSI-C を記号実行し、仕様の否定となるような実行パターンが無いかを検証するツールである。
 
 比較のために全く同じ赤黒木のソースコードを用いたいが、CbCの構文はCとは異なるために変換が必要である。
-CbCはCと似た構文を持つため、\verb/__code/ を \verb/void/ に、 \verb/goto/ を \verb/return/ に置換することで機械的にC言語に変換した。
+CbCはCと似た構文を持つため、\verb/__code/ を \verb/void/ に、 \verb/goto/ を \verb/return/ に置換することで機械的にC言語に変換できる。
 
 CBMC における仕様は bool を返す式として記述するため、akashaと同様の仕様定義が利用できる(表\ref{src:specificationCBMC}。
-C では通常の再帰呼び出しができるため、木の高さは関数で確認している。
+C では再帰呼び出しができるため、木の高さは再帰関数で確認している。
 assert が true になるような実行パターンを CBMC が見付けると、その実行パターンが反例として出力される。
 
 % {{{ CBMCにおける仕様記述
@@ -623,11 +601,6 @@
 
 よって、CBMCでは検証できない範囲の検証をakashaで行なえることが確認できた。
 
-% なお、CBMCで検証できなかった理由として、赤黒木がCでなくCbCで記述されていたコードの変換であることが考えられる。
-% CbCの軽量継続では元の環境を破棄するため、スタックフレームが増えない。
-% しかし、Cで記述した場合は末尾最適化をしない限りスタックフレームに関数呼び出し元の情報を残す必要がある。
-% CBMCにおける記号実行時に末尾最適化が行なわれない場合、CBMC内部での状態が非常に多くなってしまった可能性が考えられる。
-
 \section{まとめと今後の課題}
 CbC で記述したプログラムに対する仕様の検証を行なうことができた。
 CbC はCode SegmentとData Segmentを用いてプログラミングすることで、検証用にコードを変更することなく検証を行なうことができた。
@@ -640,13 +613,11 @@
 また、抽象度を上げることで有限回でなく無限回の操作も扱いたい。
 さらに、検証の際に証明を併用することで抽象化や状態数の削減が行なえると考えている。
 
-
-
 \begin{thebibliography}{9}
 
 \bibitem{cite:cbc-clang} 徳森海斗, 河野真治: Continuation based CのLLVM/clang 3.5上の実装について, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2014)
 \bibitem{cite:gears-os} 伊波立樹, 東恩納琢偉, 河野真治: Code Gear、 Data Gear に基づく OS のプロトタイプ, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2016)
-\bibitem{cite:llrb} 小久保 翔平, 河野真治: Code Segment と Data Segment を持つ Gears OS の 設計 (2016)
+\bibitem{cite:rbtree} 小久保 翔平, 河野真治: Code Segment と Data Segment を持つ Gears OS の 設計 (2016)
 \bibitem{cite:monad} Moggi, Eugenio: Notions of Computation and Monads, Inf. Comput (1991).
 \bibitem{cite:cbmc} Clarke, Edmund and Kroening, Daniel and Lerda, Flavio: A Tool for Checking {ANSI-C} Programs, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004)
 \bibitem{cite:agda} \verb/The Agda Wiki - Agda/ \urlj{http://wiki.portal.chalmers.se/agda/pmwiki.php} \refdatej{2016-07-05}.