Mercurial > hg > Papers > 2021 > anatofuz-master

comparison paper/chapter/02-cbc.tex @ 62:45395005373f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
update
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Wed, 03 Feb 2021 13:00:02 +0900
parents 1ce43db7c038
children eaa7a127027b
comparison
equal deleted inserted replaced
61:e1dbf6e648ad 62:45395005373f
29 DataGearはCbCでのデータの単位である。 29 DataGearはCbCでのデータの単位である。
30 CbC上では構造体の形で表現される。 30 CbC上では構造体の形で表現される。
31 各CodeGearの入力として受けるDataGearをInputDataGearと呼ぶ。 31 各CodeGearの入力として受けるDataGearをInputDataGearと呼ぶ。
32 逆に次の継続に渡すDataGearをOutputDataGearと呼ぶ。 32 逆に次の継続に渡すDataGearをOutputDataGearと呼ぶ。
33 33
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
34 47
35 \section{CbCを使ったシステムコールディスパッチの例題} 48 \section{CbCを使ったシステムコールディスパッチの例題}
36 CbCを用いてMITが開発した教育用のOSであるxv6\cite{xv6}の書き換えを行った。 49 CbCを用いてMITが開発した教育用のOSであるxv6\cite{xv6}の書き換えを行った。
37 CbCを利用したシステムコールのディスパッチ部分をソースコード\ref{src:cbc_syscall_example}に示す。 50 CbCを利用したシステムコールのディスパッチ部分をソースコード\ref{src:cbc_syscall_example}に示す。
38 この例題では特定のシステムコールの場合、 CbCで実装された処理に\texttt{goto}文をつかって継続する。 51 この例題では特定のシステムコールの場合、 CbCで実装された処理に\texttt{goto}文をつかって継続する。
46 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。 59 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
47 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。 60 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
48 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。 61 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。
49 62
50 \section{メタ計算} 63 \section{メタ計算}
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
51 プログラミング言語からメタ計算を取り扱う場合、 言語の特性に応じて様々な手法が使われてきた。 86 プログラミング言語からメタ計算を取り扱う場合、 言語の特性に応じて様々な手法が使われてきた。
52 関数型プログラミングの見方では、 メタ計算はモナドの形で表現されていた。\cite{moggi-monad} 87 関数型プログラミングの見方では、 メタ計算はモナドの形で表現されていた。\cite{moggi-monad}
53 OSの研究ではメタ計算の記述に型付きアセンブラを用いることもある。\cite{Yang:2010:SLI:1806596.1806610} 88 OSの研究ではメタ計算の記述に型付きアセンブラを用いることもある。\cite{Yang:2010:SLI:1806596.1806610}
54 89
90 通常ユーザーがメタレベルのコードを扱う場合は特定のAPIを経由することになる。
91 プログラム実行中のスタックの中には、 プログラムが現在実行している関数までのフレームや、各関数でアロケートされた変数などの情報が入る。
92 これらを環境と呼ぶ。
93 現状のプログラミング言語やOSでは、 この環境を常に持ち歩かなければならない。
94 ノーマルレベルとメタレベルを分離しようとすると、 環境の保存について考慮しなければならず、 結果的にシステムコールなどのAPIを使わなければならない。
95 システムコールを利用しても、 保存されている環境が常に存在する。
96 この暗黙の環境のことを常に意識しなければならず、 既存言語でノーマルレベルとメタレベルの分離を完全に行うのは難しい。
97
98
99 CbCではgoto文による軽量継続によって、 スタックをgotoの度に捨てていく。
100 そもそもスタックが存在しないため、 暗黙の環境も存在せずに自由にプログラミングが可能となる。
101 その為従来のプログラミング言語ではできなかった、ノーマルレベルとメタレベルのコードの分離が容易に行える。
102
55 CbCでのメタ計算はCodeGear、 DataGearの単位がそのまま使用できる。 103 CbCでのメタ計算はCodeGear、 DataGearの単位がそのまま使用できる。
56 メタ計算で使われるこれらの単位はそれぞれ、 MetaCodeGear、 MetaDataGearと呼ばれる。 104 メタ計算を行うCodeGearや、 メタな情報を持つDataGearが存在する。
57 105 これらの単位はそれぞれ、 MetaCodeGear、 MetaDataGearと呼ばれる。
58 106
59 \section{MetaCodeGear} 107 \section{MetaCodeGear}
60 108
61 GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。 109 遷移する各CodeGearの実行に必要なデータの整合性の確認などはメタ計算である。
62 遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。 110 この計算はMetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。
63 このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。 111
64 また、 対象のCodeGearの直前で実行されるMetaCodeGearをStubCodeGearと呼ぶ。 112 特に対象のCodeGearの直前で実行されるMetaCodeGearをStubCodeGearと呼ぶ。
65 MetaCodeGearやMetaDataGearは、プログラマが直接実装することはなく、 現在はPerlスクリプトによってGearsOSのビルド時に生成される。 113 MetaCodeGearやMetaDataGearは、プログラマが直接実装せず、 PerlスクリプトによってGearsOSのビルド時に生成される。
114 ただしPerlスクリプトはすでに書かれていたStubCodeGearは上書きしない。
115 スクリプトに問題がある場合や、 細かな調整をしたい場合はプログラマが直接実装可能である。
66 CodeGearから別のCodeGearに遷移する際のDataGearなどの関係性を、図\ref{meta-cg-dg}に示す。 116 CodeGearから別のCodeGearに遷移する際のDataGearなどの関係性を、図\ref{meta-cg-dg}に示す。
67 117
68 \begin{figure}[tb] 118 \begin{figure}[tb]
69 \begin{center} 119 \begin{center}
70 \includegraphics[width=150mm]{./fig/meta-cg-dg.pdf} 120 \includegraphics[width=150mm]{./fig/meta-cg-dg.pdf}