|
17
|
1 \chapter{Continuation Based C}
|
|
41
|
2 Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。
|
|
|
3 CbCでは通常の関数呼び出しの他に、 関数呼び出し時のスタックの操作を行わず、次のコードブロックに\texttt{jmp}命令で移動する継続が導入されている。
|
|
|
4 この継続はSchemeのcall/ccなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である為に軽量である事から軽量継続と呼べる。
|
|
|
5 またCbCではこの軽量継続を用いて\texttt{for}文などのループの代わりに再起呼び出しを行う。
|
|
|
6 これは関数型プログラミングでのTail callスタイルでプログラミングすることに相当する。
|
|
|
7 Agda よる関数型のCbCの記述も用意されている。
|
|
57
|
8 実際のOSやアプリケーションを記述する場合には、GCC\cite{cbcgcc}及びLLVM/clang上\cite{cbcllvm}のCbC実装を用いる。
|
|
41
|
9
|
|
55
|
10
|
|
42
|
11 \section{CodeGear}
|
|
41
|
12 CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。
|
|
|
13 CodeGearは通常のCの関数宣言の返り値の型の代わりに\texttt{\_\_code}で宣言を行う。
|
|
|
14 各CodeGearはDataGearと呼ばれるデータの単位で入力を受け取り、 その結果を別のDataGearに書き込む。
|
|
|
15 入力のDataGearをInputDataGearと呼び、 出力のDataGearをOutputDataGearと呼ぶ。
|
|
|
16 CodeGearがアクセスできるDataGearは、 InputDataGearとOutputDataGearに限定される。
|
|
17
|
17
|
|
58
|
18 CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移すると元の処理に戻ってこれない。
|
|
41
|
19 しかしCodeGearを呼び出す直前のスタックは保存される。
|
|
|
20 部分的にCbCを適用する場合はCodeGearを呼び出す\texttt{void}型などの関数を経由することで呼び出しが可能となる。
|
|
|
21
|
|
58
|
22 この他にCbCからCへ復帰する為のAPIとして、 環境付きgotoがある。
|
|
41
|
23 これは呼び出し元の関数を次のCodeGearの継続対象として設定するものである。
|
|
|
24 これはGCCでは内部コードを生成を行う。
|
|
|
25 LLVM/clangでは\texttt{setjmp}と\texttt{longjmp}を使い実装している。
|
|
60
|
26 環境付きgotoを使うと、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。
|
|
41
|
27
|
|
60
|
28 \section{DataGear}
|
|
55
|
29 DataGearはCbCでのデータの単位である。
|
|
60
|
30 CbC上では構造体の形で表現される。
|
|
|
31 各CodeGearの入力として受けるDataGearをInputDataGearと呼ぶ。
|
|
|
32 逆に次の継続に渡すDataGearをOutputDataGearと呼ぶ。
|
|
42
|
33
|
|
62
|
34 \section{CbCを使った例題}
|
|
|
35 ソースコード\ref{src:cbcexample_test}にCbCを使った例題を示す。
|
|
|
36 \lstinputlisting[label=src:cbcexample_test, caption=CbCの例題]{src/cbc_example_test.cbc}
|
|
|
37
|
|
|
38
|
|
|
39 この例では構造体\texttt{struct Test}をcodegear1に渡し、その次にcodegear2に継続している。
|
|
|
40 codegear2からはcodegear3にgotoし、 最後にexitする。
|
|
|
41 この例題をアセンブラに変換した結果を示す。
|
|
|
42 初回のmainからcodeGear1への継続は、 CbCコンパイラの仕様上関数呼び出しが行われる。
|
|
|
43 それ以外のcodegear2からcodegear3などのgotoは、jmp命令が実行される。
|
|
|
44 jmp命令はプログラムカウンタを切り替えるのみの命令であるため、 callと違いスタックの操作をしていないことが分かる。
|
|
|
45
|
|
|
46
|
|
42
|
47
|
|
|
48 \section{CbCを使ったシステムコールディスパッチの例題}
|
|
|
49 CbCを用いてMITが開発した教育用のOSであるxv6\cite{xv6}の書き換えを行った。
|
|
|
50 CbCを利用したシステムコールのディスパッチ部分をソースコード\ref{src:cbc_syscall_example}に示す。
|
|
|
51 この例題では特定のシステムコールの場合、 CbCで実装された処理に\texttt{goto}文をつかって継続する。
|
|
|
52 例題ではCodeGearへのアドレスが配列\texttt{cbccodes}に格納されている。
|
|
|
53 引数として渡している\texttt{cbc\_ret}は、 システムコールの返り値の数値をレジスタに代入するCodeGearである。
|
|
|
54 実際に\texttt{cbc\_ret}に継続が行われるのは、 \texttt{read}などのシステムコールの一連の処理の継続が終わったタイミングである。
|
|
|
55
|
|
|
56 \lstinputlisting[label=src:cbc_syscall_example, caption=CbCを利用したシステムコールのディスパッチ]{src/xv6_syscall.cbc}
|
|
47
|
57
|
|
|
58 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。
|
|
|
59 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
|
|
|
60 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
|
|
|
61 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。
|
|
|
62
|
|
50
|
63 \section{メタ計算}
|
|
62
|
64 メタ計算のメタとは、高次元などの意味を持つ言葉であり、特定の物の上位に位置するものである。
|
|
|
65 メタ計算の場合は計算に必要な計算や、 計算を行うのに必要な計算を指す。
|
|
|
66 GearsOSでのメタ計算は、 通常の計算を管理しているOSレベルの計算などを指す。
|
|
|
67 OSから見たメタ計算は、自分自身を検証する計算などになる。
|
|
|
68
|
|
|
69 ノーマルレベルの計算からすると、メタ計算は通常隠蔽される。
|
|
|
70 これはUNIXのプログラムを実行する際に、 OSのスケジューラーのことを意識せずに実行可能であることなどから分かる。
|
|
|
71 新しいプロセスを作製する場合は\texttt{fork}システムコールを実行する必要がある。
|
|
|
72 システムコールの先はOSが処理を行う。
|
|
|
73 forkシステムコールの処理をOSが計算するが、 この計算はユーザープログラムから見るとメタ計算である。
|
|
|
74 システムコールの中で何が起こっているかはユーザーレベルでは判断できず、 返り値などのAPIを経由して情報を取得する。
|
|
|
75 現状のUNIXではメタ計算はこの様なシステムコールの形としても表現される。
|
|
|
76
|
|
|
77
|
|
|
78 メタデータなどはデータのデータであり、 データを扱う上で必要なデータ情報を意味する。
|
|
|
79 プログラムの中でプログラムを生成するものをメタプログラミングなどと呼ぶ。
|
|
|
80 メタ計算やメタプログラムは、プログラム自身の検証などにとって重要な機能である。
|
|
|
81 しかしメタレベルの計算をノーマルレベルで自在に記述してしまうと、 ノーマルレベルでの信頼性に問題が発生する。
|
|
|
82 メタレベルではポインタ操作や資源管理を行うため、メモリオーバーフローなどの問題を簡単に引き起こしてしまう。
|
|
|
83 メタレベルの計算とノーマルレベルの計算を適切に分離しつつ、 ノーマルレベルから安全にメタレベルの計算を呼び出す手法が必要となる。
|
|
|
84
|
|
|
85
|
|
55
|
86 プログラミング言語からメタ計算を取り扱う場合、 言語の特性に応じて様々な手法が使われてきた。
|
|
|
87 関数型プログラミングの見方では、 メタ計算はモナドの形で表現されていた。\cite{moggi-monad}
|
|
56
|
88 OSの研究ではメタ計算の記述に型付きアセンブラを用いることもある。\cite{Yang:2010:SLI:1806596.1806610}
|
|
50
|
89
|
|
62
|
90 通常ユーザーがメタレベルのコードを扱う場合は特定のAPIを経由することになる。
|
|
|
91 プログラム実行中のスタックの中には、 プログラムが現在実行している関数までのフレームや、各関数でアロケートされた変数などの情報が入る。
|
|
|
92 これらを環境と呼ぶ。
|
|
|
93 現状のプログラミング言語やOSでは、 この環境を常に持ち歩かなければならない。
|
|
|
94 ノーマルレベルとメタレベルを分離しようとすると、 環境の保存について考慮しなければならず、 結果的にシステムコールなどのAPIを使わなければならない。
|
|
|
95 システムコールを利用しても、 保存されている環境が常に存在する。
|
|
|
96 この暗黙の環境のことを常に意識しなければならず、 既存言語でノーマルレベルとメタレベルの分離を完全に行うのは難しい。
|
|
|
97
|
|
|
98
|
|
|
99 CbCではgoto文による軽量継続によって、 スタックをgotoの度に捨てていく。
|
|
|
100 そもそもスタックが存在しないため、 暗黙の環境も存在せずに自由にプログラミングが可能となる。
|
|
|
101 その為従来のプログラミング言語ではできなかった、ノーマルレベルとメタレベルのコードの分離が容易に行える。
|
|
|
102
|
|
55
|
103 CbCでのメタ計算はCodeGear、 DataGearの単位がそのまま使用できる。
|
|
62
|
104 メタ計算を行うCodeGearや、 メタな情報を持つDataGearが存在する。
|
|
|
105 これらの単位はそれぞれ、 MetaCodeGear、 MetaDataGearと呼ばれる。
|
|
60
|
106
|
|
47
|
107 \section{MetaCodeGear}
|
|
|
108
|
|
62
|
109 遷移する各CodeGearの実行に必要なデータの整合性の確認などはメタ計算である。
|
|
|
110 この計算はMetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。
|
|
|
111
|
|
|
112 特に対象のCodeGearの直前で実行されるMetaCodeGearをStubCodeGearと呼ぶ。
|
|
|
113 MetaCodeGearやMetaDataGearは、プログラマが直接実装せず、 PerlスクリプトによってGearsOSのビルド時に生成される。
|
|
|
114 ただしPerlスクリプトはすでに書かれていたStubCodeGearは上書きしない。
|
|
|
115 スクリプトに問題がある場合や、 細かな調整をしたい場合はプログラマが直接実装可能である。
|
|
47
|
116 CodeGearから別のCodeGearに遷移する際のDataGearなどの関係性を、図\ref{meta-cg-dg}に示す。
|
|
|
117
|
|
|
118 \begin{figure}[tb]
|
|
|
119 \begin{center}
|
|
|
120 \includegraphics[width=150mm]{./fig/meta-cg-dg.pdf}
|
|
|
121 \end{center}
|
|
|
122 \caption{CodeGearとMetaCodeGear}
|
|
|
123 \label{meta-cg-dg}
|
|
|
124 \end{figure}
|
|
|
125
|
|
|
126 通常のコード中では入力のDataGearを受け取りCodeGearを実行、 結果をDataGearに書き込んだ上で別のCodeGearに継続する様に見える。
|
|
|
127 この流れを図\ref{meta-cg-dg}の上段に示す。
|
|
|
128 しかし実際はCodeGearの実行の前後に実行されるMetaCodeGearや入出力のDataGearをMetaDataGearから取り出すなどのメタ計算が加わる。
|
|
|
129 これは図\ref{meta-cg-dg}の下段に対応する。
|
|
|
130
|
|
|
131 \section{MetaDataGear}
|
|
60
|
132 基本はC言語の構造体そのものであるが、 DataGearの場合はデータに付随するメタ情報も取り扱う。
|
|
|
133 これはデータ自身がどういう型を持っているかなどの情報である。
|
|
|
134 ほかに計算を実行するCPU、 GPUの情報や、 計算に必要なすべてのDataGearの管理などの実行環境のメタデータもDataGearの形で表現される。
|
|
62
|
135 このメタデータを扱うDataGearをMetaDataGearと呼ぶ。
|
