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

\section{DataGear}
DataGearはCbCでのデータの単位である。
CbC上では構造体の形で表現される。
各CodeGearの入力として受けるDataGearをInputDataGearと呼ぶ。
逆に次の継続に渡すDataGearをOutputDataGearと呼ぶ。

メタレベルではDataGearはポインタを扱っているが、 ノーマルレベルのDataGearはポインタを扱っていないと仮定している。
例えばリストのDataGearを考えると、 Cの実装の場合はポインタを使った単方向リストが考えられる。
リストのそれぞれの要素には、メタレベルでは次の要素を指し示すポインタが含まれている。
ノーマルレベルのDataGearとして見る場合は、 リストそのものや、 リストの中の値そのものとして判断するために、より抽象化された単位として見える。
これは関数型プログラミングにおける末尾再起呼び出し時の値のやりとりに似た概念である。

\section{CbCを使った例題}
ソースコード\ref{src:cbcexample_test}にCbCを使った例題を、 ソースコード\ref{src:cbcexample_test_c}に通常のCで実装した例題を示す。
この例では構造体\texttt{struct test}をcodegear1に渡し、その次にcodegear2に継続している。
codegear2からはcodegear3にgotoし、 最後にexitする。
\lstinputlisting[label=src:cbcexample_test, caption=CbCの例題]{src/cbc_example_test.cbc}
\lstinputlisting[label=src:cbcexample_test_c, caption=ソースコード\ref{src:cbcexample_test}のCでの実装]{src/cbc_example_test.c}
CbCの場合は継続で進んでいくが、 C言語での実装はvoid型の返り値を持つ関数呼び出しで表現される。
\texttt{codegear3}に遷移したタイミングで、 CbCはmain関数のスタックしか持たないが、 C言語ではcodegear1、codegear2のスタックをそれぞれ持つ違いがある。(図\ref{fig:cbc_vs_c})

\begin{figure}[tb]
    \begin{center}
        \includegraphics[width=150mm]{./drawio/cbc_vs_c.pdf}
    \end{center}
    \caption{CbCとCの処理の差}
    \label{fig:cbc_vs_c}
\end{figure}


実際に軽量継続になっているかを、この例題をアセンブラに変換した結果を見比べて確認する。
\lstinputlisting[label=src:cbcexample_test_asm, caption=CbCの例題をコンパイルしたアセンブラの一部]{src/cbc_example_test.s}
\lstinputlisting[label=src:cbcexample_test_asm_void, caption=C言語の例題をコンパイルしたアセンブラの一部]{src/cbc_example_test_void.s}
codegear1からcodegear2への移動の際に、CbCとCで発行されるアセンブラの命令を比較する。
CbCの例題の場合のアセンブラのソースコード\ref{src:cbcexample_test_asm}はcodegear2へ25行目でjmp命令を使って遷移している。
対してC言語での実装の場合(ソースコード\ref{src:cbcexample_test_asm_void})は21行目でcallqを使っている。
jmp命令はプログラムカウンタを切り替えるのみの命令であり、 callは関数呼び出しの命令であるためにスタックの操作が行われる。
CbCでのgoto文はすべてこのjmp命令に変換されるため、 関数呼び出しより軽量に実行することが可能である。


\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も重要であることが解ってきた。

\section{メタ計算}
メタ計算のメタとは、高次元などの意味を持つ言葉であり、特定の物の上位に位置するものである。
メタ計算の場合は計算に必要な計算や、 計算を行うのに必要な計算を指す。
GearsOSでのメタ計算は、 通常の計算を管理しているOSレベルの計算などを指す。
OSから見たメタ計算は、自分自身を検証する計算などになる。

ノーマルレベルの計算からすると、メタ計算は通常隠蔽される。
これはUNIXのプログラムを実行する際に、 OSのスケジューラーのことを意識せずに実行可能であることなどから分かる。
新しいプロセスを作製する場合は\texttt{fork}システムコールを実行する必要がある。
システムコールの先はOSが処理を行う。
forkシステムコールの処理をOSが計算するが、 この計算はユーザープログラムから見るとメタ計算である。
システムコールの中で何が起こっているかはユーザーレベルでは判断できず、 返り値などのAPIを経由して情報を取得する。
現状のUNIXではメタ計算はこの様なシステムコールの形としても表現される。


メタデータなどはデータのデータであり、 データを扱う上で必要なデータ情報を意味する。
プログラムの中でプログラムを生成するものをメタプログラミングなどと呼ぶ。
メタ計算やメタプログラムは、プログラム自身の検証などにとって重要な機能である。
しかしメタレベルの計算をノーマルレベルで自在に記述してしまうと、 ノーマルレベルでの信頼性に問題が発生する。
メタレベルではポインタ操作や資源管理を行うため、メモリオーバーフローなどの問題を簡単に引き起こしてしまう。
メタレベルの計算とノーマルレベルの計算を適切に分離しつつ、 ノーマルレベルから安全にメタレベルの計算を呼び出す手法が必要となる。


プログラミング言語からメタ計算を取り扱う場合、 言語の特性に応じて様々な手法が使われてきた。
関数型プログラミングの見方では、 メタ計算はモナドの形で表現されていた。\cite{moggi-monad}
OSの研究ではメタ計算の記述に型付きアセンブラを用いることもある。\cite{Yang:2010:SLI:1806596.1806610}

通常ユーザーがメタレベルのコードを扱う場合は特定のAPIを経由することになる。
プログラム実行中のスタックの中には、 プログラムが現在実行している関数までのフレームや、各関数でアロケートされた変数などの情報が入る。
これらを環境と呼ぶ。
現状のプログラミング言語やOSでは、 この環境を常に持ち歩かなければならない。
ノーマルレベルとメタレベルを分離しようとすると、 環境の保存について考慮しなければならず、 結果的にシステムコールなどのAPIを使わなければならない。
システムコールを利用しても、 保存されている環境が常に存在する。
また関数単位での分離を行っても、 呼び出す関数の数が細かくなってしまい、スタックの容量を容易に消費してしまう。
既存言語ではメタ計算の分離が困難である。


CbCではgoto文による軽量継続によって、 スタックをgotoの度に捨てていく。
そもそもスタックが存在しないため、 暗黙の環境も存在せずに自由にプログラミングが可能となる。
またCodeGearをどれだけ呼び出しても、関数呼び出し時に伴うスタックの消費も存在しない。
メタ計算の単位で細かくCodeGearを切り分けても、実行の問題が生じない。
その為従来のプログラミング言語ではできなかった、ノーマルレベルとメタレベルのコードの分離が容易に行える。

CbCでのメタ計算はCodeGear、 DataGearの単位がそのまま使用できる。
メタ計算を行うCodeGearや、 メタな情報を持つDataGearが存在する。
これらの単位はそれぞれ、 MetaCodeGear、 MetaDataGearと呼ばれる。
\section{MetaCodeGear}
遷移する各CodeGearの実行に必要なデータの整合性の確認などはメタ計算である。
この計算はMetaCodeGearと呼ばれる各CodeGearごと実装されたメタなCodeGearで計算を行う。

特に対象のCodeGearの直前で実行されるMetaCodeGearをStubCodeGearと呼ぶ。
ユーザーからするとノーマルレベルのCodeGear間の移動に見えるが、実際にはStubCodeGearが挿入される。
MetaCodeGearやMetaDataGearは、プログラマが直接実装せず、 PerlスクリプトによってGearsOSのビルド時に生成される。
ただしPerlスクリプトはすでに書かれていたStubCodeGearは上書きしない。
スクリプトに問題がある場合や、 細かな調整をしたい場合はプログラマが直接実装可能である。
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}
基本はC言語の構造体そのものであるが、 DataGearの場合はデータに付随するメタ情報も取り扱う。
これはデータ自身がどういう型を持っているかなどの情報である。
ほかに計算を実行するCPU、 GPUの情報や、 計算に必要なすべてのDataGearの管理などの実行環境のメタデータもDataGearの形で表現される。
このメタデータを扱うDataGearをMetaDataGearと呼ぶ。


またCbCはスタックを持たないため、 データを保存したい場合はスタック以外の場所に値を書き込む必要がある。
このスタック以外の場所はDataGearであり、 メタなデータを扱っているためにMetaDataGearと言える。
具体的にMetaDataGearがどのように構成されているかは、CbCを扱うプロジェクトによって異なる。