\chapter{Continuation Based C}
Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。
CbCでは通常の関数呼び出しの他に、 関数呼び出し時のスタックの操作を行わず、次のコードブロックに\texttt{jmp}命令で移動する継続が導入されている。
この継続はSchemeのcall/ccなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である為に軽量である事から軽量継続と呼べる。
またCbCではこの軽量継続を用いて\texttt{for}文などのループの代わりに再起呼び出しを行う。
これは関数型プログラミングでのTail callスタイルでプログラミングすることに相当する。
Agda よる関数型のCbCの記述も用意されている。
実際のOSやアプリケーションを記述する場合には、GCC及びLLVM/clang上のCbC実装を用いる。

\section{CodeGear}
CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。
CodeGearは通常のCの関数宣言の返り値の型の代わりに\texttt{\_\_code}で宣言を行う。
各CodeGearはDataGearと呼ばれるデータの単位で入力を受け取り、 その結果を別のDataGearに書き込む。
入力のDataGearをInputDataGearと呼び、 出力のDataGearをOutputDataGearと呼ぶ。
CodeGearがアクセスできるDataGearは、 InputDataGearとOutputDataGearに限定される。



CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。
しかしCodeGearを呼び出す直前のスタックは保存される。
部分的にCbCを適用する場合はCodeGearを呼び出す\texttt{void}型などの関数を経由することで呼び出しが可能となる。

この他にCbCからCへ復帰する為のAPIとして、 環境付きgotoという機能がある。
これは呼び出し元の関数を次のCodeGearの継続対象として設定するものである。
これはGCCでは内部コードを生成を行う。
LLVM/clangでは\texttt{setjmp}と\texttt{longjmp}を使い実装している。
したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。

\section{DataGear}


\section{CbCを使ったシステムコールディスパッチの例題}
CbCを用いてMITが開発した教育用のOSであるxv6\cite{xv6}の書き換えを行った。
CbCを利用したシステムコールのディスパッチ部分をソースコード\ref{src:cbc_syscall_example}に示す。
この例題では特定のシステムコールの場合、 CbCで実装された処理に\texttt{goto}文をつかって継続する。
例題ではCodeGearへのアドレスが配列\texttt{cbccodes}に格納されている。
引数として渡している\texttt{cbc\_ret}は、 システムコールの返り値の数値をレジスタに代入するCodeGearである。
実際に\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{メタ計算}

関数型プログラミングの見方では、 メタ計算はモナドの形で表現されていた。\cite{moggi-monad}

\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}