annotate paper/chapter/02-cbc.tex @ 47:24f6f068ddbb

from sigos
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Mon, 01 Feb 2021 17:16:24 +0900 (2021-02-01)
parents 8d779a8c8029
children f72ef87a5139
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
17
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \chapter{Continuation Based C}
41
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
2 Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
3 CbCでは通常の関数呼び出しの他に、 関数呼び出し時のスタックの操作を行わず、次のコードブロックに\texttt{jmp}命令で移動する継続が導入されている。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
4 この継続はSchemeのcall/ccなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である為に軽量である事から軽量継続と呼べる。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
5 またCbCではこの軽量継続を用いて\texttt{for}文などのループの代わりに再起呼び出しを行う。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
6 これは関数型プログラミングでのTail callスタイルでプログラミングすることに相当する。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
7 Agda よる関数型のCbCの記述も用意されている。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
8 実際のOSやアプリケーションを記述する場合には、GCC及びLLVM/clang上のCbC実装を用いる。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
9
42
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
10 \section{CodeGear}
41
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
11 CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
12 CodeGearは通常のCの関数宣言の返り値の型の代わりに\texttt{\_\_code}で宣言を行う。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
13 各CodeGearはDataGearと呼ばれるデータの単位で入力を受け取り、 その結果を別のDataGearに書き込む。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
14 入力のDataGearをInputDataGearと呼び、 出力のDataGearをOutputDataGearと呼ぶ。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
15 CodeGearがアクセスできるDataGearは、 InputDataGearとOutputDataGearに限定される。
17
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
41
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
17
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
18
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
19 CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
20 しかしCodeGearを呼び出す直前のスタックは保存される。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
21 部分的にCbCを適用する場合はCodeGearを呼び出す\texttt{void}型などの関数を経由することで呼び出しが可能となる。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
22
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
23 この他にCbCからCへ復帰する為のAPIとして、 環境付きgotoという機能がある。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
24 これは呼び出し元の関数を次のCodeGearの継続対象として設定するものである。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
25 これはGCCでは内部コードを生成を行う。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
26 LLVM/clangでは\texttt{setjmp}と\texttt{longjmp}を使い実装している。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
27 したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。
e25a073180de add file
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
28
42
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
29 \section{DataGear}
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
30
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
31
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
32 \section{CbCを使ったシステムコールディスパッチの例題}
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
33 CbCを用いてMITが開発した教育用のOSであるxv6\cite{xv6}の書き換えを行った。
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
34 CbCを利用したシステムコールのディスパッチ部分をソースコード\ref{src:cbc_syscall_example}に示す。
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
35 この例題では特定のシステムコールの場合、 CbCで実装された処理に\texttt{goto}文をつかって継続する。
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
36 例題ではCodeGearへのアドレスが配列\texttt{cbccodes}に格納されている。
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
37 引数として渡している\texttt{cbc\_ret}は、 システムコールの返り値の数値をレジスタに代入するCodeGearである。
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
38 実際に\texttt{cbc\_ret}に継続が行われるのは、 \texttt{read}などのシステムコールの一連の処理の継続が終わったタイミングである。
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
39
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
40 \lstinputlisting[label=src:cbc_syscall_example, caption=CbCを利用したシステムコールのディスパッチ]{src/xv6_syscall.cbc}
47
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
41
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
42 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
43 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
44 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
45 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
46 CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。\cite{gears}
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
47 現在のGearsOSは並列フレームワークとして実装されており、 実用的なOSのプロトタイプ実装として既存のOS上への実装を目指している。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
48
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
49 \section{MetaCodeGear}
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
50
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
51 GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
52 遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
53 このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
54 また、 対象のCodeGearの直前で実行されるMetaCodeGearをStubCodeGearと呼ぶ。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
55 MetaCodeGearやMetaDataGearは、プログラマが直接実装することはなく、 現在はPerlスクリプトによってGearsOSのビルド時に生成される。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
56 CodeGearから別のCodeGearに遷移する際のDataGearなどの関係性を、図\ref{meta-cg-dg}に示す。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
57
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
58 \begin{figure}[tb]
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
59 \begin{center}
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
60 \includegraphics[width=150mm]{./fig/meta-cg-dg.pdf}
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
61 \end{center}
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
62 \caption{CodeGearとMetaCodeGear}
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
63 \label{meta-cg-dg}
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
64 \end{figure}
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
65
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
66 通常のコード中では入力のDataGearを受け取りCodeGearを実行、 結果をDataGearに書き込んだ上で別のCodeGearに継続する様に見える。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
67 この流れを図\ref{meta-cg-dg}の上段に示す。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
68 しかし実際はCodeGearの実行の前後に実行されるMetaCodeGearや入出力のDataGearをMetaDataGearから取り出すなどのメタ計算が加わる。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
69 これは図\ref{meta-cg-dg}の下段に対応する。
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
70
24f6f068ddbb from sigos
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
71 \section{MetaDataGear}