--- a/paper/cbc.tex	Mon Feb 06 20:23:42 2017 +0900
+++ b/paper/cbc.tex	Wed Feb 08 13:50:52 2017 +0900
@@ -101,25 +101,30 @@
 
 % {{{ Continuation based C におけるメタ計算の例: GearsOS
 \section{Continuation based C におけるメタ計算の例: GearsOS}
-CbC におけるメタ計算は軽量継続を行なう際に Meta CodeSegment を挟むことで実現できる。
 CbC を用いてメタ計算を実現した例として、GearsOS\cite{weko_142109_1}が存在する。
-GearsOS とはマルチコアCPUやGPU環境での動作を対象としたOSであり、現在OSの設計と並列処理部分の実装が行なわれている。
-GearsOS におけるメタ計算はMonadによって形式化されている\cite{Moggi:1991:NCM:116981.116984}。
-現在存在するメタ計算としてメモリの確保と割り当て、並列に書き込むことが可能な Synchronized Queue、データの保存に用いる非破壊赤黒木がある。
+GearsOS は並列に、信頼性高く動作することを目標としたOS であり、 マルチコアCPUやGPU環境での動作を対象としている。
+現在OSの設計と並列処理部分の実装が行なわれている。
+GearsOS におけるメタ計算はMonad\cite{Moggi:1991:NCM:116981.116984}を用いている。 %TODO: kkb さんの修論
+現在実装済みのメタ計算はメモリの管理、並列に書き込むことが可能な Synchronized Queue、データの保存用の非破壊赤黒木がある。
 
 GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。
 マルチコアCPU環境では CodeGear と CodeSegment は同一だが、GPU 環境では CodeGear には OpenCL~\cite{opencl}/CUDA~\cite{cuda} における kernel も含まれる。
-kernel とは GPU で実行される関数のことであり、GPU上のメモリに配置されたデータ群に対して並列に実行されるものである。
-通常 GPU でデータの処理を行なう場合はデータの転送、転送終了を同期で確認、 kernel 実行、kernel の終了を同期で確認する、という手順が必要である。
-CPU/GPU での処理をメタ計算で行なうことにより、ノーマルレベルでは CodeGear が実行されるデバイスや DataGear の位置を意識する必要が無いというメリットがある。
+kernel とは GPU で実行される関数のことであり、GPU上のメモリに配置されたデータ群に対して並列に実行される。
+通常 GPU でデータの処理を行なう場合は
 
-GearsOS においては軽量継続の呼び出し部分もメタ計算として実現されている。
-ある CodeGear から次の CodeGear へと継続する際には、次に実行される CodeGear の名前を指定する。
-その名前を Meta CodeGear が解釈し、対応する CodeGear へと処理を引き渡す。
-これは従来の OS の Dynamic Loading Libary や Command の呼び出しに相当する。
-CodeGear と名前の対応は Meta DataGear に格納されており、従来の OS の Process  や Thread に相当する。
+\begin{itemize}
+    \item データをメインメモリから GPUのメモリへ転送
+    \item 転送終了を同期で確認
+    \item kernel 起動(GPUメモリ上のデータに対して並列に処理)
+    \item 処理終了を同期で確認
+    \item 計算結果であるデータを GPU のメモリからメインメモリへ転送
+    \item 転送終了を同期で確認
+\end{itemize}
 
-具体的には Meta DataGear には以下のようなものが格納される。
+といった手順が必要であり、ユーザは処理したいデータの位置などを意識しながらプログラミングする必要がある。
+GearsOS では CPU/GPU での処理をメタ計算としてユーザから隠すことにより、 CodeGear が実行されるデバイスや DataGear の位置を意識する必要がなくなる。
+
+GearsOS で利用する Meta DataGear には以下のものが含まれる。
 
 \begin{itemize}
     \item DataGear の型情報
@@ -130,9 +135,12 @@
 
 実際の GearsOS におけるメモリ管理を含むメタ計算用の Meta DataGear の定義例をリスト\ref{src:context}に示す。
 Meta DataGear は Context という名前の構造体で定義されている。
+通常レベルの DataGear も構造体で定義されているが、メタ計算側から見た DataGear はそれぞれの構造体の共用体となっており、一様に扱える。
 
 \lstinputlisting[label=src:context, caption=GearsOS における Meta DataGearの定義例] {src/context.h}
 
+リスト~\ref{src:context}のソースコードは以下のように対応している。
+
 \begin{itemize}
     \item DataGear の型情報
 
@@ -162,164 +170,33 @@
         取り出す必要がある DataGear は enum を用いて定義し(リスト\ref{src:context} 11-14行)、 CodeGear を実行する際に data フィールドから取り出す。
 \end{itemize}
 
-なお、この Context から DataGear を取り出す Meta CodeSegment を stub と呼ぶ。
-stub の例をリスト\ref{src:stub}に示す。
-stub は Context が持つ DataGear のポインタ data に対して enum を用いてアクセスしている。
-現在、この stub は全ての CodeGear に対してユーザが1つずつ定義する必要がある。
-この作業は非常に煩雑であり、CodeGear の定義から生成するスクリプトを用いて定義の簡易化を行なっているが、コンパイラ側でのサポートは入っていない。
-この stub を型情報から自動生成するために Continuation based C における型システムを定義する必要がある。
-
-\lstinputlisting[label=src:stub, caption=GearsOS における stub Meta CodeSegment] {src/stub.cbc}
-
-% }}}
-
-% {{{ 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}
-
-これらの条件より、木をルートから辿った際に最も長い経路は最も短い経路の高々二倍に収まる。
-
-\newpage % for layout
-
-GearsOS で実装されている赤黒木は特に非破壊赤黒木であり、一度構築した木構造は破壊される操作ごとに新しい木構造が生成される。
-非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、変更後に新たなルートノードとする。
-この際に変更が行なわれていない部分は変更前の木と共有する(図\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 を用いて赤黒木を実装する際の問題として、関数の呼び出しスタックが存在しないため、関数の再帰呼び出しによって木が辿れないことがある。
-経路を辿るためにはノードに親への参照を持たせるか、挿入・削除時に辿った経路を記憶する必要がある。
-ノードが親への参照を持つ非破壊木構造は共通部分の共有が行なえないため、辿った経路を記憶する方法を使う。
-経路の記憶にはスタックを用い、スタックは Meta DataSegment に保持させる。
+Meta CodeGear は定義された Meta DataGear を処理する CodeGear である。
+メモリ管理や並列処理の待ち合わせといった処理はこのメタレベルにしか表れない。
 
-赤黒木を格納する 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 を用いた赤黒木の実装の検証}
-GearsOS の赤黒木の仕様の定義とその確認を 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})。
-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/ を上書きすることにより実現する。
-\verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。
-検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続である(リスト\ref{src:meta})。
+GearsOS においては軽量継続もメタ計算として実現されている。
+とある CodeGear から次の CodeGear へと軽量継続する際には、次に実行される CodeGear の名前を指定する。
+その名前を Meta CodeGear が解釈し、対応する CodeGear へと処理を引き渡す(リスト~\ref{src:meta}の \verb/meta/)。
 
 \lstinputlisting[label=src:meta, caption=通常の CodeSegment の軽量継続] {src/meta.c}
 
-これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。
-検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。
-実際の検証部分は \verb/PutAndGoToNextDepth/ の後に行なわれるため、直接は記述されていない。
-この \verb/meta/ が行なうのは検証用にメモリの管理である。
-状態の数え上げを行なう際に状態を保存したり、元の状態に戻す処理が行なわれる。
-このメタ計算を用いた検証では、要素数13個までの任意の順で挿入の際に仕様が満たされることを確認できた。
-また、赤黒木の処理内部に恣意的なバグを追加した際には反例を返した。
+CodeGear と名前の対応は Meta DataGear に格納されており、従来の OS の Process  や Thread に相当する。
+名前の対応を動的に切り替えたり、Thread ごとに切り替えることにより、通常レベルのプログラムを変更せず実行を上書きできる。
+これは従来の OS の Dynamic Loading Libary や Command の呼び出しに相当する。
+
+また、通常レベルの CodeGear から Meta DataGear を操作できてしまうと、ユーザがメタレベル操作を自由に記述できてしまい、メタ計算を分離した意味が無くなってしまう。
+これを防ぐために、CodeGear を実行する際は Meta DataGear から必要な DataGear だけを渡す。
+このように、 Meta DataGear から DataGear を取り出す Meta CodeGear を stub と呼ぶ。
+stub の例をリスト\ref{src:stub}に示す。
+\lstinputlisting[label=src:stub, caption=GearsOS における stub Meta CodeSegment] {src/stub.cbc}
 
-\lstinputlisting[label=src:akasha-meta, caption=検証を行なう CodeSegment の軽量継続] {src/akashaMeta.c}
+stub は Context が持つ DataGear のポインタ data に対して enum を用いてアクセスしている。
+なお、現在はメタレベルの計算とノーマルレベルの分離はコンパイラ側がサポートしていないため、引数に Meta DataGear である Context が渡されているが、本来はノーマルレベルではアクセスできない。
+% また、stub は全ての CodeGear に対してユーザが1つずつ定義する必要があるため、 CodeGear の定義が煩雑になっている。
+% レベルの分離と stub の自動生成を行なうスクリプトも存在しているが、コンパイラ側のサポートはまだ行なわれていない。
+% 型情報を用いたコンパイル時 stub 生成や、軽量継続時の型チェックを行なうために本研究では CbC の型システムを定義する。
+
+また、GearsOS におけるメタ計算として CodeGear のモデル検査がある。
+通常レベルの CodeGear を変更することなく、その仕様を検証するものである。
+個々の CodeGear の仕様を検証することにより、より信頼性の高いOSを目指す。
 
 % }}}