--- a/paper/chapter/02-cbc.tex	Mon Feb 01 15:15:41 2021 +0900
+++ b/paper/chapter/02-cbc.tex	Mon Feb 01 17:16:24 2021 +0900
@@ -38,3 +38,34 @@
 実際に\texttt{cbc\_ret}に継続が行われるのは、 \texttt{read}などのシステムコールの一連の処理の継続が終わったタイミングである。
 
 \lstinputlisting[label=src:cbc_syscall_example, caption=CbCを利用したシステムコールのディスパッチ]{src/xv6_syscall.cbc}
+
+軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。
+その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
+CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
+CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。
+CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。\cite{gears}
+現在のGearsOSは並列フレームワークとして実装されており、 実用的なOSのプロトタイプ実装として既存のOS上への実装を目指している。
+
+\section{MetaCodeGear}
+
+GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。
+遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。
+このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。
+また、 対象のCodeGearの直前で実行されるMetaCodeGearをStubCodeGearと呼ぶ。
+MetaCodeGearやMetaDataGearは、プログラマが直接実装することはなく、 現在はPerlスクリプトによってGearsOSのビルド時に生成される。
+CodeGearから別のCodeGearに遷移する際のDataGearなどの関係性を、図\ref{meta-cg-dg}に示す。
+
+\begin{figure}[tb]
+    \begin{center}
+        \includegraphics[width=150mm]{./fig/meta-cg-dg.pdf}
+    \end{center}
+    \caption{CodeGearとMetaCodeGear}
+    \label{meta-cg-dg}
+\end{figure}
+
+通常のコード中では入力のDataGearを受け取りCodeGearを実行、 結果をDataGearに書き込んだ上で別のCodeGearに継続する様に見える。
+この流れを図\ref{meta-cg-dg}の上段に示す。
+しかし実際はCodeGearの実行の前後に実行されるMetaCodeGearや入出力のDataGearをMetaDataGearから取り出すなどのメタ計算が加わる。
+これは図\ref{meta-cg-dg}の下段に対応する。
+
+\section{MetaDataGear}

Binary file paper/fig/Context_ref.pdf has changed

Binary file paper/fig/cbc_syscall_Trap.pdf has changed

Binary file paper/fig/cgdg.pdf has changed

Binary file paper/fig/factorial_cbc.pdf has changed

Binary file paper/fig/meta-cg-dg.pdf has changed

Binary file paper/fig/readsyscall.pdf has changed

Binary file paper/fig/readsyscall_state.pdf has changed

Binary file paper/fig/syscall_dispatch.pdf has changed

Binary file paper/master_paper.pdf has changed