Mercurial > hg > Papers > 2021 > anatofuz-master
changeset 40:66b32f3ec7fa
rename
| author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Feb 2021 08:32:58 +0900 |
| parents | 4f4d3f1fc568 |
| children | e25a073180de |
| files | paper/chapter/01-cbc.tex paper/chapter/01-introduction.tex paper/chapter/02-cbc.tex paper/chapter/02-interface.tex paper/chapter/02-perl.tex paper/chapter/03-gears.tex paper/chapter/04-interface.tex paper/chapter/04-perl.tex paper/chapter/gears.tex paper/chapter/introduction.tex paper/master_paper.pdf paper/master_paper.tex |
| diffstat | 12 files changed, 469 insertions(+), 469 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/chapter/01-cbc.tex Sun Jan 31 22:42:23 2021 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -\chapter{Continuation Based C} - -Continuation Based Cとは、 C言語から関数呼び出しとループ処理を取り除いた言語である。 -Cの下位言語と言え、 C言語とアセンブラの中間のような言語として利用することが出来る。 \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/chapter/01-introduction.tex Mon Feb 01 08:32:58 2021 +0900 @@ -0,0 +1,80 @@ +\chapter{OSとアプリケーションの信頼性} + +コンピューター上では様々なアプリケーションが常時動作している。 +動作しているアプリケーションは信頼性が保証されていてほしい。 +信頼性の保証には、 実行してほしい一連の挙動をまとめた仕様と、 それを満たしているかどうかの確認である検証が必要となる。 +アプリケーション開発では検証に関数や一連の動作をテストを行う方法や、デバッグを通して信頼性を保証する手法が広く使われている。 + +実際にアプリケーションを動作させるOSは、アプリケーションよりさらに高い信頼性が保証される必要がある。 +OSはCPUやメモリなどの資源管理と、 ユーザーにシステムコールなどのAPIを提供することで抽象化を行っている。 +OSの信頼性の保証もテストコードを用いて証明することも可能ではあるが、 アプリケーションと比較するとOSのコード量、 処理の量は膨大である。 +またOSはCPU制御やメモリ制御、 並列・並行処理などを多用する。 +テストコードを用いて処理を検証する場合、テストコードとして特定の状況を作成する必要がある。 +実際にOSが動作する中でバグやエラーを発生する条件を、 並列処理の状況などを踏まえてテストコードで表現するのは困難である。 +非決定的な処理を持つOSの信頼性を保証するには、 テストコード以外の手法を用いる必要がある。 + + +テストコード以外の方法として、 形式手法的と呼ばれるアプローチがある。 +形式手法の具体的な検証方法の中で、 証明を用いる方法\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402}とモデル検査を用いる方法がある。 +証明を用いる方法ではAgda\cite{agda}やCoq\cite{coq}などの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。 +Curry-Howard同型対応則により、型と論理式の命題が対応する。 +この型を導出するプログラムと実際の証明が対応する。 +証明には特定の型を入力として受け取り、証明したい型を生成する関数を作成する。 +整合性の確認は、記述した関数を元に定理証明支援系が検証する。 +証明を使う手法の場合、 実際の証明を行うのは定理証明支援系であるため、 定理証明支援系が理解できるプログラムで実装する必要がある。 +AgdaやCoqの場合はAgda、 Cow自身のプログラムで記述する必要がある。 +しかしAgdaで証明ができてもAgdaのコードを直接OSのソースコードとしてコンパイルすることはできない。 +Agda側でCのソースコードを吐き出せれば可能ではあるが、 現状は検証したコードと実際に動作するコードは分離されている。 +検証されたアルゴリズムをもとにCで実装することは可能であるが、 この場合移植時にバグが入る可能性がある。 +検証ができているソースコードそのものを使ってOSを動作させたい。 + + +他の形式手法にモデル検査がある。 +モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。 +例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。 +モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。 +OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。 +しかしOSの処理は膨大である。 +すべての存在可能な状態を数え上げるモデル検査では状態爆発が問題となる。 +状態を有限に制限したり抽象化を行う必要がある。 + + +OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。 +その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。 +OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。 +範囲が限られているため、有限時間でモデル検査などで検証することが可能である。 +この為にはOSの処理を証明しやすくする表現で実装する必要がある。\cite{hyperkernel} +証明しやすい表現の例として、 状態遷移ベースでの実装がある。 + + +証明を行う対象の計算は、 その意味が大きく別けられる。 +OSやプログラムの動作においては本来したい計算がまず存在する。 +これはプログラマが通常プログラミングするものである。 +これら本来行いたい処理のほかに、 CPU、メモリ、スレッドなどの資源管理なども必要となる。 +前者の計算をノーマルレベルの計算と呼び、後者をメタレベルの計算と呼ぶ。 +OSはメタ計算を担当していると言える。 +ユーザーレベルから見ると、データの読み込みなどは資源へのアクセスが必要であるため、システムコールを呼ぶ必要がある。 +システムコールを呼び出すとOSが管理する資源に対して何らかの副作用が発生するメタ計算と言える。 +副作用は関数型プログラムの見方からするとモナドと言え、 モナドもメタ計算ととらえることができる。 +OS上で動くプログラムはCPUにより並行実行される。この際の他のプロセスとの干渉もメタレベルの処理である。 +実装のソースコードはノーマルレベルであり検証用のソースコードはメタ計算だと考えると、OSそのものが +検証を行ない、システム全体の信頼を高める機能を持つべきだと考える。 +ノーマルレベルの計算を確実に行う為には、メタレベルの計算が重要となる。 + + +プログラムの整合性の検証はメタレベルの計算で行いたい。 +ユーザーが実装したノーマルレベルの計算に対応するメタレベルの計算を、自由にメタレベルの計算で証明したい。 +またメタレベルで検証ががすでにされたプログラムがあった場合、都度実行ユーザーの環境で検証が行われるとパフォーマンスに問題が発生する。 +この場合はメタレベルの計算を検証をするもの、しないものと切り替えられる柔軟なAPIが必要となる。 +メタレベルの計算をノーマルレベルの計算と同等にプログラミングできると、動作するコードに対して様々なアプローチが掛けられる。 +この為にはノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。 + +プログラムのノーマルレベルの計算とメタレベルの計算を一貫して行う言語として、 Continuation Based C(CbC)を用いる。 +CbCは基本\texttt{goto文}で\texttt{CodeGaar}というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と呼ばれる隠れた状態を持たない。 +このため、計算のための情報は\texttt{CodeGear}の入力にすべてそろっている。 +そのうちのいくつかはメタ計算、つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(\texttt{DataGear})である。 +メタ計算とノーマルレベルの区別は入力のどこを扱うかの差に帰着される。 +CbCはCと互換性のあるCの下位言語である。 +CbCは\texttt{GCC}\cite{gcc}\cite{weko_82695_1}あるいは\texttt{LLVM}\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。 +Cのコンパイルシステムを使える為に、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。 +またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{agda-ryokka}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/chapter/02-cbc.tex Mon Feb 01 08:32:58 2021 +0900 @@ -0,0 +1,4 @@ +\chapter{Continuation Based C} + +Continuation Based Cとは、 C言語から関数呼び出しとループ処理を取り除いた言語である。 +Cの下位言語と言え、 C言語とアセンブラの中間のような言語として利用することが出来る。 \ No newline at end of file
--- a/paper/chapter/02-interface.tex Sun Jan 31 22:42:23 2021 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,112 +0,0 @@ -\section{GearsOSのInterfaceの構文の改良} -GearsOSのInterfaceでは、 従来はDataGearとCodeGearを分離して記述していた。 -CodeGearの入出力をDataGearとして列挙する必要があった。 -CodeGearの入出力として\texttt{\_\_code()}の間に記述したDataGearの一覧と、Interface上部で記述したDataGearの集合が一致している必要がある。 - -従来の分離している記法の場合、 このDataGearの宣言が一致していないケースが多々発生した。 -またInterfaceの入力としてのDataGearではなく、 フィールド変数としてDataGearを使うようなプログラミングスタイルを取ってしまうケースも見られた。 -GearsOSでは、 DataGearやフィールド変数をオブジェクトに格納したい場合、 Interface側ではなくImpl側に変数を保存する必要がある。 -Interface側に記述してしまう原因は複数考えられる。 -GearsOSのプログラミングスタイルに慣れていないことも考えられるが、構文によるところも考えられる。 -CodeGearとDataGearはInterfaceの場合は密接な関係性にあるが、 分離して記述してしまうと「DataGearの集合」と「CodeGearの集合」を別個で捉えてしまう。 -あくまでInterfaceで定義するCodeGearとDataGearはInterfaceのAPIである。 -これをユーザーに強く意識させる必要がある。 - -golangにもInterfaceの機能が実装されている。 -golangの場合はInterfaceは関数の宣言部分のみを記述するルールになっている。 -変数名は含まれていても含まなくても問題ない。 - -\begin{lstlisting}[frame=lrbt,label=src:golang_interface,caption={golangのinterface宣言}] -type geometry interface { - area() float64 - perim() float64 -} -\end{lstlisting} - -\section{Implementの型をいれたことによる間違ったGearsプログラミング} -Implementの型を導入したが、 GearsOSのプログラミングをするにつれていくつかの間違ったパターンがあることがわかった。 -自動生成されるStubCodeGearは、 goto metaから遷移するのが前提であるため、 引数をContextから取り出す必要がある。 -Contextから取り出す場合は、 実装しているInterfaceに対応している置き場所からデータを取り出す。 -この置き場所は\texttt{data}配列であり、 配列の添え字は\texttt{enum Data}と対応している。 -また各CodeGearからgotoする際に、 遷移先のInterfaceに値を書き込みに行く。 - - -Interfaceで定義したCodeGearと対応しているImplementのCodeGearの場合はこのデータの取り出し方で問題はない。 -しかしImplementのCodeGearから内部でgotoするCodeGearの場合は事情が異なる。 -内部でgotoするCodeGearは、 Javaなどのプライベートメソッドのように使うことを想定している。 -このCodeGearのことをprivate CodeGearと呼ぶ。 -privateCodeGearにgotoする場合、 goto元のCodeGearからは\texttt{goto meta}経由で遷移する。 -goto metaが発行されるとStub Code Gearに遷移するが、現在のシステムではInterfaceから値をとってくることになってしまう。 - - -\section{メタ計算部分の入れ替え} -GearsOSでは次のCodeGearに移行する前のMetaCodeGearとして、 デフォルトでは\texttt{\_\_code meta}が使われている。 -\texttt{\_\_code meta}はcontextに含まれているCodeGearの関数ポインタを、 enumからディスパッチして次のStub CodeGearに継続するものである。 - -例えばモデル検査をGearsOSで実行する場合、 通常のStub CodeGearのほかに状態の保存などを行う必要がある。 -この状態の保存に関する一連の処理は明らかにメタ計算であるので、 ノーマルレベルのCodeGearではない箇所で行いたい。 -ノーマルレベル以外のCodeGearで実行する場合は、 通常のコード生成だとStubCodeGearの中で行うことになる。 -StubCodeGearは自動生成されてしまうため、 値の取り出し以外のことを行う場合は自分で実装する必要がある。 -しかしモデル検査に関する処理は様々なCodeGearの後に行う必要があるため、 すべてのCodeGearのStubを静的に実装するのは煩雑である。 - -ノーマルレベルのCodeGearの処理の後に、StubCodeGear以外のMeta Code Gearを実行したい。 -Stub Code Gearに直ちに遷移してしまう\texttt{\_\_code meta}以外のMeta CodeGearに、 特定のCodeGearの計算が終わったら遷移したい。 -このためには、特定のCodeGearの遷移先のMetaCodeGearをユーザーが定義できるAPIが必要となる。 -このAPIを実装すると、ユーザーが柔軟にメタ計算を選択することが可能となる。 - -GearsOSのビルドシステムのAPIとして\texttt{meta.pm}を作製した。 -これはPerlのモジュールファイルとして実装した。 -meta.pmはPerlで実装されたGearsOSのトランスコンパイラであるgenerate\_stub.plから呼び出される。 -meta.pmの中のサブルーチンである\texttt{replaceMeta}に変更対象のCodeGearと変更先のMetaCodeGearへのgotoを記述する。 -ユーザーはmeta.pmのPerlファイルをAPIとしてGearsOSのトランスコンパイラにアクセスすることが可能となる。 - -具体的な使用例をコード\ref{src:metapm}に示す。 -meta.pmはサブルーチン\texttt{replaceMeta}が返すリストの中に、特定のパターンで配列を設定する。 -各配列の0番目には、goto metaを置換したいCodeGearの名前を示すPerl正規表現リテラルを入れる。 -コード\ref{src:metapm}の例では、\texttt{PhilsImpl}が名前に含まれるCodeGearを指定している。 -すべてのCodeGearのgotoの先を切り替える場合は\texttt{qr/.*\//}などの正規表現を指定する。 - -\lstinputlisting[label=src:metapm, caption=meta.pm]{src/meta.pm} - -generate\_stub.plはGears CbCファイルの変換時に、 CbCファイルがあるディレクトリにmeta.pmがあるかを確認する。 -meta.pmがある場合はモジュールロードを行う。 -meta.pmがない場合はmeta Code Gearにgotoするものをデフォルト設定として使う。 -各Gode Gearが\texttt{goto文}を呼び出したタイミングでreplaceMetaを呼び出し、 ルールにしたがってgoto文を書き換える。 -変換するCodeGearがルールになかった場合は、 デフォルト設定が呼び出される。 - -\section{別Interfaceからの書き出しを取得する必要があるCodeGear} - -従来のMetaCodeGearの生成では、 別のInterfaceからの入力を受け取るCodeGearのStubの生成に問題があった。 -具体的なこの問題が発生する例題をソースコード\ref{src:insertTest1}に示す。 -この例では\texttt{pop2Test}Code Gearから \texttt{stack->pop2}を呼び出し、 継続として\texttt{pop2Test1}を渡している。 -\texttt{pop2Test}自体はStackTest Interfaceであり、 \texttt{stack->pop2}の\texttt{stack}はStack Interfaceである。 - -\lstinputlisting[label=src:insertTest1, caption=別Interfaceからの書き出しを取得するCodeGearの例]{src/pop2test.cbc} - -当初Perlスクリプトが生成した\texttt{pop2Test1}のstub CodeGearはソースコード\ref{src:pop2stub-origin}のものである。 -\lstinputlisting[label=src:pop2stub-origin, caption=生成されたStub]{src/pop2stub-origin.cbc} -\texttt{\_\_code pop2Test}で遷移する先のCodeGearはStackInterfaceであり、 呼び出しているAPIは\texttt{pop2}である。 -pop2はスタックから値を2つ取得するAPIである。 -取得したAPIはGearsOSのInterfaceの処理ルールにより、 Context中のStack Interfaceのデータ格納場所に書き込まれる。 -しかしソースコード\ref{src:pop2stub-origin}の例では\texttt{Gearef(context, StackTest)}でContext中の\texttt{StackTest} Interfaceのdataの置き場所から値を取得している。 -これではpop2でせっかく取り出した値を取得できない。 -ここで必要となってくるのは、 呼び出し元のStack Interfaceからの値の取得である。 -どのInterfaceから呼び出されているかは、 コンパイルタイムには確定できるのでPerlのトランスコンパイラでStub Codeを生成したい。 - - -別Interfaceから値を取得するには別の出力があるCodeGearの継続で渡されたCodeGearをまず確定させる。 -今回の例では\texttt{pop2Test1}が該当する。 -このCodeGearの入力の値と、 出力があるCodeGearの出力を見比べ、 出力をマッピングすれば良い。 -Stack Interfaceのpop2はdataとdata1に値を書き込む。 -pop2Test1の引数はdata, data1, stackであるので、前2つにpop2の出力を代入したい。 - -Contextから値を取り出すのはメタ計算であるStub CodeGearで行われる。 -別Interfaceから値を取り出そうとする場合、 すでにPerlトランスコンパイラが生成しているStubを書き換えてしまう方法も取れる。 -しかしStubCodeGearそのものを、 別Interfaceから値を取り出すように書き換えてはいけない。 -これは別Interfaceの継続として渡されるケースと、 次のgoto先として遷移するケースがあるためである。 -前者のみの場合は書き換えで問題ないが、 後者のケースで書き換えを行ってしまうとStubで値を取り出す先が異なってしまう。 -どのような呼び出し方をしても対応できるようにするには工夫が必要となる。 - - -GearsOSでは継続として渡す場合や、 次のgoto文で遷移する先のCodeGearはノーマルレベルではenumの番号として表現されていた。 -今回のような次に実行するStub CodeGear、つまりメタCodeGearを切り替えたい場合は、ノーマルレベルからメタレベルへの変換時にenumの番号を切り替えることで実現可能である。
--- a/paper/chapter/02-perl.tex Sun Jan 31 22:42:23 2021 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,183 +0,0 @@ -\chapter{GearsOSのトランスコンパイラ} - -GearsOSはCbCで実装を行う。 -CbCはC言語よりアセンブラに近い言語であるため、 すべてを純粋なCbCで記述しようとすると記述量が膨大になってしまう。 -またノーマルレベルの計算とメタレベルの計算を、全てプログラマが記述する必要が発生してしまう。 -メタ計算では値の取り出しなどを行うが、 これはノーマルレベルのCodeGearのAPIが決まれば一意に決定される。 -したがってノーマルレベルのみ記述すれば、 機械的にメタ部分の処理は概ね生成可能となる。 -また、メタレベルのみ切り替えたいなどの状況が存在する。 -ノーマルレベル、メタレベル共に同じコードの場合は記述の変更量が膨大であるが、 メタレベルの作成を分離するとこの問題は解消される。 - -GearsOSではメタレベルの処理の作成にPerlスクリプトを用いており、 ノーマルレベルで記述されたCbCから、 メタ部分を含むCbCへと変換する。 -変換前のCbCをGearsCbCと呼ぶ。 - -\section{トランスコンパイラ} -プログラミング言語から実行可能ファイルやアセンブラを生成する処理系のことを、一般的にコンパイラと呼ぶ。 -特定のプログラミング言語から別のプログラミング言語に変換するコンパイラのことを、 トランスコンパイラと呼ぶ。 -トランスコンパイラとしてはJavaScriptを古い規格のJavaScriptに変換するBabel\cite{babel}がある。 - -またトランスコンパイラは、変換先の言語を拡張した言語の実装としても使われる。 -JavaScriptに強い型制約をつけた拡張言語であるTypeScriptは、 TypeScriptから純粋なJavaScriptに変換を行うトランスコンパイラである。 -すべてのTypeScriptのコードはJavaScriptにコンパイル可能である。 -JavaScriptに静的型の機能を取り込みたい場合に使われる言語であり、 JavaScriptの上位の言語と言える。 - -GearsOSはCbCを拡張した言語となっている。 -ただしこの拡張自体はCbCコンパイラであるgcc、 llvm/clangには搭載されていない。 -その為GearsOSの拡張部分を、等価な純粋なCbCの記述に変換する必要がある。 -現在のGearsOSでは、 CMakeによるコンパイル時にPerlで記述された\texttt{generate\_stub.pl}と\texttt{generate\_context.pl}の2種類のスクリプトで変換される。 - - - -\begin{itemize} - \item \texttt{generate\_stub.pl} - \begin{itemize} - \item 各CbCファイルごとに呼び出されるスクリプト - \item 対応するメタ計算を導入したCbCファイル(拡張子はc)に変換する - \begin{itemize} - \item 図\ref{fig:generate_stub_pl_1}に処理の概要を示す - \end{itemize} - \end{itemize} - \item \texttt{generate\_context.pl} - \begin{itemize} - \item 生成したCbCファイルを解析し、使われているCodeGearを確定する - \item context.hを読み込み、使われているDataGearを確定する - \item Context関係の初期化ルーチンやCodeGear、 DataGearの番号であるenumを生成する - \begin{itemize} - \item 図\ref{fig:generate_context_1}に処理の概要を示す - \end{itemize} - \end{itemize} -\end{itemize} - -これらのPerlスクリプトはプログラマが自分で動かすことはない。 -Perlスクリプトの実行手順はCMakeLists.txtに記述しており、 makeやninja-buildでのビルド時に呼び出される。(ソースコード \ref{src:cmake1}) - -\lstinputlisting[label=src:cmake1, caption=CMakeList.txt内でのPerlの実行部分]{src/cmakefile.1.txt} - -\begin{figure}[htp] - \begin{center} - \includegraphics[width=160mm]{drawio/gears_os_build_flow.pdf} - \end{center} - \caption{generate\_sub.plを使ったトランスコンパイル} - \label{fig:generate_stub_pl_1} - \end{figure} - -\begin{figure}[htp] - \begin{center} - \includegraphics[width=130mm]{drawio/old_generate_context.pdf} - \end{center} - \caption{generate\_context.plを使ったファイル生成} - \label{fig:generate_context_1} - \end{figure} - - - -\section{GearsCbCのInterfaceの実装時の問題} - -Interfaceとそれを実装するImplの型が決定すると、最低限満たすべきCodeGearのAPIは一意に決定する。 -ここで満たすべきCodeGearは、Interfaceで定義したCodeGearと、 Impl側で定義した privateなCodeGearとなる。 -例えばStack Interfaceの実装を考えると、各Implで\texttt{pop}, push, shift, isEmptyなどを実装する必要がある。 - -従来はプログラマが手作業でヘッダーファイルの定義を参照しながら\texttt{.cbc}ファイルを作成していた。 -手作業での実装のため、 コンパイル時に次のような問題点が多発した。 - -\begin{itemize} - \item CodeGearの入力のフォーマットの不一致 - \item Interfaceの実装のCodeGearの命名規則の不一致 - \item 実装を忘れているCodeGearの発生 -\end{itemize} - - -特にGearsOSの場合はPerlスクリプトによって純粋なCbCに一度変換されてからコンパイルが行われる。 -実装の状況とトランスコンパイラの組み合わせによっては、 CbCコンパイラレベルでコンパイルエラーを発生させないケースがある。 -この場合は実際に動作させながら、gdb, lldbなどのCデバッガを用いてデバッグをする必要がある。 -またCbCコンパイラレベルで検知できても、すでに変換されたコード側でエラーが出てしまうので、トランスコンパイラの挙動をトレースしながらデバッグをする必要がある。 -Interfaceの実装が不十分であることのエラーは、 GearsOSレベル、最低でもCbCコンパイラのレベルで完全に検知したい。 - -\section{Interfaceを満たすコード生成の他言語の対応状況} - -Interfaceを機能として所持している言語の場合、Interfaceを完全に見たいしているかどうかはコンパイルレベルか実行時レベルで検知される。 -例えばJavaの場合はInterfaceを満たしていない場合はコンパイルエラーになる。 - - -InterfaceのAPIを完全に実装するのを促す仕組みとして、Interfaceの定義からエディタやツールが満たすべき関数と引数の組を自動生成するツールがある。 - -Javaでは様々な手法でこのツールを実装している。 -Microsoftが提唱しているIDEとプログラミング言語のコンパイラをつなぐプロトコルにLanguage Serverがある。 -Language Serverはコーディング中のソースコードをコンパイラ自身でパースし、 型推論やエラーの内容などをIDE側に通知するプロトコルである。 -主要なJavaのLanguage Serverの実装であるeclipse.jdt.ls\cite{eclipse.jdt.ls}では、 LanguageServerの機能として未実装のメソッドを検知する機能が実装されている。\cite{eclipse_pull322} -この機能を応用してvscode上から未実装のメソッドを特定し、 雛形を生成する機能がある。 -他にもIntelliJ IDEなどの商用IDEでは、 IDEが独自に未実装のメソッドを検知、雛形を生成する機能を実装している。 - - -golangの場合は主に\texttt{josharian/impl}\cite{golang_impl}が使われている。 -これはインストールすると\texttt{impl}コマンドが使用可能になり、 実装したいInterfaceの型と、 Interfaceを実装するImplの型(レシーバ)を与えることで雛形が生成される。 -主要なエディタであるvscodeのgolangの公式パッケージである\texttt{vscode-go}\cite{vscode-go}でも導入されており、 vscodeから呼び出すことが可能である。 -vscode以外にもvimなどのエディタから呼び出すことや、 シェル上で呼び出して標準出力の結果を利用することが可能である。 - -\section{GearsOSでのInterfaceを満たすCbCの雛形生成} -GearsOSでも同様のInterfaceの定義から実装するCodeGearの雛形を生成したい。 -LanguageServerの導入も考えられるが、 今回の場合はC言語のLanguageServerをCbC用にまず改良し、 さらにGearsOS用に書き換える必要がある。 -現状のGearsOSが持つシンタックスはCbCのシンタックスを拡張しているものではあるが、これはCbCコンパイラ側には組み込まれていない。 -LanguageServerをGearsOSに対応する場合、 CbCコンパイラ側にGearsOSの拡張シンタックスを導入する必要がある。 -CbCコンパイラ側への機能の実装は、 比較的難易度が高いと考えらる。 -CbCコンパイラ側に手をつけず、 Interfaceの入出力の検査は既存のGearsOSのビルドシステム上に組み込みたい。 - -対してgolangの\texttt{impl}コマンドのように、 シェルから呼び出し標準出力に結果を書き込む形式も考えられる。 -この場合は実装が比較的容易かつ、 コマンドを呼び出して標準出力の結果を使えるシェルやエディタなどの各プラットフォームで使用可能となる。 -先行事例を参考に、コマンドを実行して雛形ファイルを生成するコマンド\texttt{impl2cbc.pl}をGearsOSに導入した。 -\texttt{impl2cbc.pl}の処理の概要を図\ref{fig:impl2cbc}に示す。 - - -\begin{figure}[hp] - \begin{center} - \includegraphics[width=130mm]{drawio/impl2cbc.pdf} - \end{center} - \caption{impl2cbcの処理の流れ} - \label{fig:impl2cbc} - \end{figure} - -\subsection{雛形生成の手法} - - -Interfaceでは入力の引数がImplと揃っている必要があるが、 第一引数は実装自身のインスタンスがくる制約となっている。 -実装自身の型は、Interface定義時には不定である。 -その為、 GearsOSではInterfaceのAPIの宣言時にデフォルト型変数\texttt{Impl}を実装の型として利用する。 -デフォルト型\texttt{Impl}を各実装の型に置換することで自動生成が可能となる。 - - -実装すべきCodeGearはInterfaceとImpl側の型を見れば定義されている。 -\texttt{\_\_code}で宣言されているものを逐次生成すればよいが、 継続として呼び出されるCodeGearは具体的な実装を持たない。 -GearsOSで使われているInterfaceには概ね次の継続である\texttt{next}が登録されている。 -\texttt{next}そのものはInterfaceを呼び出す際に、入力として与える。 -その為各Interfaceに入力として与えられた\texttt{next}を保存する場所は存在するが、 nextそのものの独自実装は各Interfaceは所持しない。 -したがってこれをInterfaceの実装側で明示的に実装することはできない。 -雛形生成の際に、入力として与えられるCodeGearを生成してしまうと、プログラマに混乱をもたらしてしまう。 - -入力として与えられているCodeGearは、Interfaceに定義されているCodeGearの引数として表現されている。 -コードに示す例では、\texttt{whenEmpty}は入力して与えられているCodeGearである。 -雛形を生成する場合は、入力として与えられたCodeGearを除外して出力を行う。 -順序はInterfaceをまず出力した後に、 Impl側を出力する。 - - -\subsection{コンストラクタの自動生成} -雛形生成では他にコンストラクタの生成も行う。 -GearsOSのInterfaceのコンストラクタは、 メモリの確保及び各変数の初期化を行う。 -メモリ上に確保するのは主にInterfaceとImplのそれぞれが基本となっている。 -Interfaceによっては別のDataGearを内包しているものがある。 -その場合は別のDataGearの初期化もコンストラクタ内で行う必要があるが、 自動生成コマンドではそこまでの解析は行わない。 - - -コンストラクタのメンバ変数はデフォルトでは変数は0、ポインタの場合はNULLで初期化するように生成する。 -このスクリプトで生成されたコンストラクタを使う場合、 CbCファイルから該当する部分を削除すると、\texttt{generate\_stub.pl}内でも自動的に生成される。 -自動生成機能を作成すると1CbCファイルあたりの記述量が減る利点がある。 - - - -明示的にコンストラクタが書かれていた場合は、 Perlスクリプト内での自動生成は実行しないように実装した。 -これはオブジェクト指向言語のオーバーライドに相当する機能と言える。 -現状のGearsOSで使われているコンストラクタは、 基本は\texttt{struct Context*}型の変数のみを引数で要求している。 -しかしオブジェクトを識別するためにIDを実装側に埋め込みたい場合など、 コンストラクタ経由で値を代入したいケースが存在する。 -この場合はコンストラクタの引数を増やす必要や、 受け取った値をインスタンスのメンバに書き込む必要がある。 -具体的にどの値を書き込めば良いのかまではPerlスクリプトでは判定することができない。 -このような細かな調整をする場合は、 generate\_stub.pl側での自動生成はせずに、 雛形生成されたコンストラクタを変更すれば良い。 -あくまで雛形生成スクリプトはプログラマ支援であるため、 いくつかの手動での実装は許容している。
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/chapter/03-gears.tex Mon Feb 01 08:32:58 2021 +0900 @@ -0,0 +1,85 @@ +\chapter{GearsOS} + +GearsOSとはContinuation Based Cを用いて実装しているOSプロジェクトである。 +CodeGearとDataGearを基本単位として実行する。 +GearsOSはOSとして実行する側面と、 CbCのシンタックスを拡張した言語フレームワークとしての側面がある。 + +\section{GearsOSのビルドシステム} +GearsOSではビルドツールにCMakeを利用している。 +ビルドフローを図\ref{fig:gearsbuild1}に示す。 +CMakeはautomakeなどのMakeファイルを作成するツールに相当するものである。 +GearsOSでプログラミングする際は、ビルドしたいプロジェクトをCMakeLists.txtに記述する。 +CMakeは自身がコンパイルをすることはなく、ビルドツールであるmakeやninja-buildに処理を移譲している。 +CMakeはmakeやninja-buildが実行可能なMakefile、 build.ninjaの生成までを担当する。 + + +GearsOSのビルドでは直接CbCコンパイラがソースコードをコンパイルすることはなく、 間にPerlスクリプトが2種類実行される。 +Perlスクリプトはビルド対象のGearsOSで拡張されたCbCファイルを、純粋なCbCファイルに変換する。 +ほかにGearsOSで動作する例題ごとに必要な初期化関数なども生成する。 +Perlスクリプトで変換されたCbCファイルなどをもとにCbCコンパイラがコンパイルを行う。 +ビルドの処理は自動化されており、 CMake経由でmakeやninjaコマンドを用いてビルドする。 + +\begin{figure}[hp] + \begin{center} + \includegraphics[width=120mm]{drawio/geasflow1.pdf} + \end{center} + \caption{GearsOSのビルドフロー} + \label{fig:gearsbuild1} + \end{figure} + +\section{pmake} +GearsOSをビルドする場合は、x86アーキテクチャのマシンからビルドするのが殆どである。 +この場合ビルドしたバイナリはx86向けのバイナリとなる。 +これはビルドをするホストマシンに導入されているCbCコンパイラがx86アーキテクチャ向けにビルドされたものである為である。 + +CbCコンパイラはGCCとllvm/clang上に構築した2種類が主力な処理系である。 +LVM/clangの場合はLLVM側でターゲットアーキテクチャを選択することが可能である。 +GCCの場合は最初からjターゲットアーキテクチャを指定してコンパイラをビルドする必要がある。 + +時にマシンスペックの問題などから、 別のアーキテクチャ向けのバイナリを生成したいケースがある。 +教育用マイコンボードであるRaspberry Pi\cite{rpi}はARMアーキテクチャが搭載されている。 +Raspberry Pi上でGearsOSのビルドをする場合、 ARM用にビルドされたCbCコンパイラが必要となる。 +Raspberry Pi自体は非力なマシンであるため、 GearsOSのビルドはもとよりCbCコンパイラの構築をRaspberry Pi上でするのは困難である。 +マシンスペックが高めのx86マシンからARM用のバイナリをビルドして、 Raspberry Piに転送し実行したい。 +ホストマシンのアーキテクチャ以外のアーキテクチャ向けにコンパイルすることをクロスコンパイルと呼ぶ。 + + +GearsOSはビルドツールにCMakeを利用しているので、 CMakeでクロスコンパイル出来るように工夫をする必要がある。 +ビルドに使用するコンパイラやリンカはCMakeが自動探索し、 決定した上でMakefileやbuild.ninjaファイルを生成する。 +しかしCMakeは今ビルドしようとしている対象が、自分が動作しているアーキテクチャかそうでないか、クロスコンパイラとして使えるかなどはチェックしない。 +つまりCMakeが自動でクロスコンパイル対応のGCCコンパイラを探すことはない。 +その為そのままビルドするとx86用のバイナリが生成されてしまう。 + + +CMakeを利用してクロスコンパイルする場合、CMakeの実行時に引数でクロスコンパイラを明示的に指定する必要がある。 +この場合x86のマシンからARMのバイナリを出力する必要があり、 コンパイラやリンカーなどをARMのクロスコンパイル対応のものに指定する必要がある。 +また、 xv6の場合はリンク時に特定のリンカスクリプトを使う必要がある。 +これらのリンカスクリプトもCMake側に、 CMakeが提供しているリンカ用の特殊変数を使って自分で組み立てて渡す必要がある。 +このようなCMakeの処理を手打ちで行うことは難しいので、 \texttt{pmake.pl}を作成した。 +\texttt{pmake.pl}の処理の概要を図\ref{fig:pmake}に示す。 +\texttt{pmake.pl}はPerlスクリプトで、 シェルコマンドを内部で実行しクロスコンパイル用のオプションを組み立てる。 +\texttt{pmake.pl}を経由してCMakeを実行すると、 makeコマンドに対応するMakefile、 ninja-buildに対応するbuild.ninjaが生成される。 +以降はcmakeではなくmakeなどのビルドツールがビルドを行う。 + +\begin{figure}[h] + \begin{center} + \includegraphics[width=160mm]{drawio/pmake.pdf} + \end{center} + \caption{pmake.plの処理フロー} + \label{fig:pmake} + \end{figure} + + + + + \section{Interfaceの取り扱い方法の検討} + + GearsOSのInterfaceはモジュール化の仕組みと\texttt{goto}文での引数の一時保管場所としての機能を持っている。 +InterfaceのImplementのヘッダーファイルを実装したことで、 GearsOS上でInterfaceを実装する際に新たな方法での実装を検討した。 +ImplementのCodeGearは今まではInterfaceで定義したCodeGearと1対1対応していた。 +ImplementのCodeGearからgotoする先は、 入力として与えられたCodeGearか、 Implement内で独自に定義したCodeGearにgotoするケースとなっていた。 +後者の独自に定義したCodeGearにgotoするケースも、 実装のCbCファイルの中に記述されているCodeGearに遷移していた。 + +GearsOSを用いてxv6 OSを再実装した際に、 実装側のCodeGearを細かく別けて記述した。 +細分化によって1つのCbCファイルあたりのCodeGearの記述量が増えてしまうという問題が発生した。 +見通しをよくする為に、 Interfaceで定義したCodeGearと直接対応するCodeGearの実装と、 それらからgotoするCodeGearで実装ファイルを分離することを試みた。
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/chapter/04-interface.tex Mon Feb 01 08:32:58 2021 +0900 @@ -0,0 +1,112 @@ +\section{GearsOSのInterfaceの構文の改良} +GearsOSのInterfaceでは、 従来はDataGearとCodeGearを分離して記述していた。 +CodeGearの入出力をDataGearとして列挙する必要があった。 +CodeGearの入出力として\texttt{\_\_code()}の間に記述したDataGearの一覧と、Interface上部で記述したDataGearの集合が一致している必要がある。 + +従来の分離している記法の場合、 このDataGearの宣言が一致していないケースが多々発生した。 +またInterfaceの入力としてのDataGearではなく、 フィールド変数としてDataGearを使うようなプログラミングスタイルを取ってしまうケースも見られた。 +GearsOSでは、 DataGearやフィールド変数をオブジェクトに格納したい場合、 Interface側ではなくImpl側に変数を保存する必要がある。 +Interface側に記述してしまう原因は複数考えられる。 +GearsOSのプログラミングスタイルに慣れていないことも考えられるが、構文によるところも考えられる。 +CodeGearとDataGearはInterfaceの場合は密接な関係性にあるが、 分離して記述してしまうと「DataGearの集合」と「CodeGearの集合」を別個で捉えてしまう。 +あくまでInterfaceで定義するCodeGearとDataGearはInterfaceのAPIである。 +これをユーザーに強く意識させる必要がある。 + +golangにもInterfaceの機能が実装されている。 +golangの場合はInterfaceは関数の宣言部分のみを記述するルールになっている。 +変数名は含まれていても含まなくても問題ない。 + +\begin{lstlisting}[frame=lrbt,label=src:golang_interface,caption={golangのinterface宣言}] +type geometry interface { + area() float64 + perim() float64 +} +\end{lstlisting} + +\section{Implementの型をいれたことによる間違ったGearsプログラミング} +Implementの型を導入したが、 GearsOSのプログラミングをするにつれていくつかの間違ったパターンがあることがわかった。 +自動生成されるStubCodeGearは、 goto metaから遷移するのが前提であるため、 引数をContextから取り出す必要がある。 +Contextから取り出す場合は、 実装しているInterfaceに対応している置き場所からデータを取り出す。 +この置き場所は\texttt{data}配列であり、 配列の添え字は\texttt{enum Data}と対応している。 +また各CodeGearからgotoする際に、 遷移先のInterfaceに値を書き込みに行く。 + + +Interfaceで定義したCodeGearと対応しているImplementのCodeGearの場合はこのデータの取り出し方で問題はない。 +しかしImplementのCodeGearから内部でgotoするCodeGearの場合は事情が異なる。 +内部でgotoするCodeGearは、 Javaなどのプライベートメソッドのように使うことを想定している。 +このCodeGearのことをprivate CodeGearと呼ぶ。 +privateCodeGearにgotoする場合、 goto元のCodeGearからは\texttt{goto meta}経由で遷移する。 +goto metaが発行されるとStub Code Gearに遷移するが、現在のシステムではInterfaceから値をとってくることになってしまう。 + + +\section{メタ計算部分の入れ替え} +GearsOSでは次のCodeGearに移行する前のMetaCodeGearとして、 デフォルトでは\texttt{\_\_code meta}が使われている。 +\texttt{\_\_code meta}はcontextに含まれているCodeGearの関数ポインタを、 enumからディスパッチして次のStub CodeGearに継続するものである。 + +例えばモデル検査をGearsOSで実行する場合、 通常のStub CodeGearのほかに状態の保存などを行う必要がある。 +この状態の保存に関する一連の処理は明らかにメタ計算であるので、 ノーマルレベルのCodeGearではない箇所で行いたい。 +ノーマルレベル以外のCodeGearで実行する場合は、 通常のコード生成だとStubCodeGearの中で行うことになる。 +StubCodeGearは自動生成されてしまうため、 値の取り出し以外のことを行う場合は自分で実装する必要がある。 +しかしモデル検査に関する処理は様々なCodeGearの後に行う必要があるため、 すべてのCodeGearのStubを静的に実装するのは煩雑である。 + +ノーマルレベルのCodeGearの処理の後に、StubCodeGear以外のMeta Code Gearを実行したい。 +Stub Code Gearに直ちに遷移してしまう\texttt{\_\_code meta}以外のMeta CodeGearに、 特定のCodeGearの計算が終わったら遷移したい。 +このためには、特定のCodeGearの遷移先のMetaCodeGearをユーザーが定義できるAPIが必要となる。 +このAPIを実装すると、ユーザーが柔軟にメタ計算を選択することが可能となる。 + +GearsOSのビルドシステムのAPIとして\texttt{meta.pm}を作製した。 +これはPerlのモジュールファイルとして実装した。 +meta.pmはPerlで実装されたGearsOSのトランスコンパイラであるgenerate\_stub.plから呼び出される。 +meta.pmの中のサブルーチンである\texttt{replaceMeta}に変更対象のCodeGearと変更先のMetaCodeGearへのgotoを記述する。 +ユーザーはmeta.pmのPerlファイルをAPIとしてGearsOSのトランスコンパイラにアクセスすることが可能となる。 + +具体的な使用例をコード\ref{src:metapm}に示す。 +meta.pmはサブルーチン\texttt{replaceMeta}が返すリストの中に、特定のパターンで配列を設定する。 +各配列の0番目には、goto metaを置換したいCodeGearの名前を示すPerl正規表現リテラルを入れる。 +コード\ref{src:metapm}の例では、\texttt{PhilsImpl}が名前に含まれるCodeGearを指定している。 +すべてのCodeGearのgotoの先を切り替える場合は\texttt{qr/.*\//}などの正規表現を指定する。 + +\lstinputlisting[label=src:metapm, caption=meta.pm]{src/meta.pm} + +generate\_stub.plはGears CbCファイルの変換時に、 CbCファイルがあるディレクトリにmeta.pmがあるかを確認する。 +meta.pmがある場合はモジュールロードを行う。 +meta.pmがない場合はmeta Code Gearにgotoするものをデフォルト設定として使う。 +各Gode Gearが\texttt{goto文}を呼び出したタイミングでreplaceMetaを呼び出し、 ルールにしたがってgoto文を書き換える。 +変換するCodeGearがルールになかった場合は、 デフォルト設定が呼び出される。 + +\section{別Interfaceからの書き出しを取得する必要があるCodeGear} + +従来のMetaCodeGearの生成では、 別のInterfaceからの入力を受け取るCodeGearのStubの生成に問題があった。 +具体的なこの問題が発生する例題をソースコード\ref{src:insertTest1}に示す。 +この例では\texttt{pop2Test}Code Gearから \texttt{stack->pop2}を呼び出し、 継続として\texttt{pop2Test1}を渡している。 +\texttt{pop2Test}自体はStackTest Interfaceであり、 \texttt{stack->pop2}の\texttt{stack}はStack Interfaceである。 + +\lstinputlisting[label=src:insertTest1, caption=別Interfaceからの書き出しを取得するCodeGearの例]{src/pop2test.cbc} + +当初Perlスクリプトが生成した\texttt{pop2Test1}のstub CodeGearはソースコード\ref{src:pop2stub-origin}のものである。 +\lstinputlisting[label=src:pop2stub-origin, caption=生成されたStub]{src/pop2stub-origin.cbc} +\texttt{\_\_code pop2Test}で遷移する先のCodeGearはStackInterfaceであり、 呼び出しているAPIは\texttt{pop2}である。 +pop2はスタックから値を2つ取得するAPIである。 +取得したAPIはGearsOSのInterfaceの処理ルールにより、 Context中のStack Interfaceのデータ格納場所に書き込まれる。 +しかしソースコード\ref{src:pop2stub-origin}の例では\texttt{Gearef(context, StackTest)}でContext中の\texttt{StackTest} Interfaceのdataの置き場所から値を取得している。 +これではpop2でせっかく取り出した値を取得できない。 +ここで必要となってくるのは、 呼び出し元のStack Interfaceからの値の取得である。 +どのInterfaceから呼び出されているかは、 コンパイルタイムには確定できるのでPerlのトランスコンパイラでStub Codeを生成したい。 + + +別Interfaceから値を取得するには別の出力があるCodeGearの継続で渡されたCodeGearをまず確定させる。 +今回の例では\texttt{pop2Test1}が該当する。 +このCodeGearの入力の値と、 出力があるCodeGearの出力を見比べ、 出力をマッピングすれば良い。 +Stack Interfaceのpop2はdataとdata1に値を書き込む。 +pop2Test1の引数はdata, data1, stackであるので、前2つにpop2の出力を代入したい。 + +Contextから値を取り出すのはメタ計算であるStub CodeGearで行われる。 +別Interfaceから値を取り出そうとする場合、 すでにPerlトランスコンパイラが生成しているStubを書き換えてしまう方法も取れる。 +しかしStubCodeGearそのものを、 別Interfaceから値を取り出すように書き換えてはいけない。 +これは別Interfaceの継続として渡されるケースと、 次のgoto先として遷移するケースがあるためである。 +前者のみの場合は書き換えで問題ないが、 後者のケースで書き換えを行ってしまうとStubで値を取り出す先が異なってしまう。 +どのような呼び出し方をしても対応できるようにするには工夫が必要となる。 + + +GearsOSでは継続として渡す場合や、 次のgoto文で遷移する先のCodeGearはノーマルレベルではenumの番号として表現されていた。 +今回のような次に実行するStub CodeGear、つまりメタCodeGearを切り替えたい場合は、ノーマルレベルからメタレベルへの変換時にenumの番号を切り替えることで実現可能である。
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/chapter/04-perl.tex Mon Feb 01 08:32:58 2021 +0900 @@ -0,0 +1,183 @@ +\chapter{GearsOSのトランスコンパイラ} + +GearsOSはCbCで実装を行う。 +CbCはC言語よりアセンブラに近い言語であるため、 すべてを純粋なCbCで記述しようとすると記述量が膨大になってしまう。 +またノーマルレベルの計算とメタレベルの計算を、全てプログラマが記述する必要が発生してしまう。 +メタ計算では値の取り出しなどを行うが、 これはノーマルレベルのCodeGearのAPIが決まれば一意に決定される。 +したがってノーマルレベルのみ記述すれば、 機械的にメタ部分の処理は概ね生成可能となる。 +また、メタレベルのみ切り替えたいなどの状況が存在する。 +ノーマルレベル、メタレベル共に同じコードの場合は記述の変更量が膨大であるが、 メタレベルの作成を分離するとこの問題は解消される。 + +GearsOSではメタレベルの処理の作成にPerlスクリプトを用いており、 ノーマルレベルで記述されたCbCから、 メタ部分を含むCbCへと変換する。 +変換前のCbCをGearsCbCと呼ぶ。 + +\section{トランスコンパイラ} +プログラミング言語から実行可能ファイルやアセンブラを生成する処理系のことを、一般的にコンパイラと呼ぶ。 +特定のプログラミング言語から別のプログラミング言語に変換するコンパイラのことを、 トランスコンパイラと呼ぶ。 +トランスコンパイラとしてはJavaScriptを古い規格のJavaScriptに変換するBabel\cite{babel}がある。 + +またトランスコンパイラは、変換先の言語を拡張した言語の実装としても使われる。 +JavaScriptに強い型制約をつけた拡張言語であるTypeScriptは、 TypeScriptから純粋なJavaScriptに変換を行うトランスコンパイラである。 +すべてのTypeScriptのコードはJavaScriptにコンパイル可能である。 +JavaScriptに静的型の機能を取り込みたい場合に使われる言語であり、 JavaScriptの上位の言語と言える。 + +GearsOSはCbCを拡張した言語となっている。 +ただしこの拡張自体はCbCコンパイラであるgcc、 llvm/clangには搭載されていない。 +その為GearsOSの拡張部分を、等価な純粋なCbCの記述に変換する必要がある。 +現在のGearsOSでは、 CMakeによるコンパイル時にPerlで記述された\texttt{generate\_stub.pl}と\texttt{generate\_context.pl}の2種類のスクリプトで変換される。 + + + +\begin{itemize} + \item \texttt{generate\_stub.pl} + \begin{itemize} + \item 各CbCファイルごとに呼び出されるスクリプト + \item 対応するメタ計算を導入したCbCファイル(拡張子はc)に変換する + \begin{itemize} + \item 図\ref{fig:generate_stub_pl_1}に処理の概要を示す + \end{itemize} + \end{itemize} + \item \texttt{generate\_context.pl} + \begin{itemize} + \item 生成したCbCファイルを解析し、使われているCodeGearを確定する + \item context.hを読み込み、使われているDataGearを確定する + \item Context関係の初期化ルーチンやCodeGear、 DataGearの番号であるenumを生成する + \begin{itemize} + \item 図\ref{fig:generate_context_1}に処理の概要を示す + \end{itemize} + \end{itemize} +\end{itemize} + +これらのPerlスクリプトはプログラマが自分で動かすことはない。 +Perlスクリプトの実行手順はCMakeLists.txtに記述しており、 makeやninja-buildでのビルド時に呼び出される。(ソースコード \ref{src:cmake1}) + +\lstinputlisting[label=src:cmake1, caption=CMakeList.txt内でのPerlの実行部分]{src/cmakefile.1.txt} + +\begin{figure}[htp] + \begin{center} + \includegraphics[width=160mm]{drawio/gears_os_build_flow.pdf} + \end{center} + \caption{generate\_sub.plを使ったトランスコンパイル} + \label{fig:generate_stub_pl_1} + \end{figure} + +\begin{figure}[htp] + \begin{center} + \includegraphics[width=130mm]{drawio/old_generate_context.pdf} + \end{center} + \caption{generate\_context.plを使ったファイル生成} + \label{fig:generate_context_1} + \end{figure} + + + +\section{GearsCbCのInterfaceの実装時の問題} + +Interfaceとそれを実装するImplの型が決定すると、最低限満たすべきCodeGearのAPIは一意に決定する。 +ここで満たすべきCodeGearは、Interfaceで定義したCodeGearと、 Impl側で定義した privateなCodeGearとなる。 +例えばStack Interfaceの実装を考えると、各Implで\texttt{pop}, push, shift, isEmptyなどを実装する必要がある。 + +従来はプログラマが手作業でヘッダーファイルの定義を参照しながら\texttt{.cbc}ファイルを作成していた。 +手作業での実装のため、 コンパイル時に次のような問題点が多発した。 + +\begin{itemize} + \item CodeGearの入力のフォーマットの不一致 + \item Interfaceの実装のCodeGearの命名規則の不一致 + \item 実装を忘れているCodeGearの発生 +\end{itemize} + + +特にGearsOSの場合はPerlスクリプトによって純粋なCbCに一度変換されてからコンパイルが行われる。 +実装の状況とトランスコンパイラの組み合わせによっては、 CbCコンパイラレベルでコンパイルエラーを発生させないケースがある。 +この場合は実際に動作させながら、gdb, lldbなどのCデバッガを用いてデバッグをする必要がある。 +またCbCコンパイラレベルで検知できても、すでに変換されたコード側でエラーが出てしまうので、トランスコンパイラの挙動をトレースしながらデバッグをする必要がある。 +Interfaceの実装が不十分であることのエラーは、 GearsOSレベル、最低でもCbCコンパイラのレベルで完全に検知したい。 + +\section{Interfaceを満たすコード生成の他言語の対応状況} + +Interfaceを機能として所持している言語の場合、Interfaceを完全に見たいしているかどうかはコンパイルレベルか実行時レベルで検知される。 +例えばJavaの場合はInterfaceを満たしていない場合はコンパイルエラーになる。 + + +InterfaceのAPIを完全に実装するのを促す仕組みとして、Interfaceの定義からエディタやツールが満たすべき関数と引数の組を自動生成するツールがある。 + +Javaでは様々な手法でこのツールを実装している。 +Microsoftが提唱しているIDEとプログラミング言語のコンパイラをつなぐプロトコルにLanguage Serverがある。 +Language Serverはコーディング中のソースコードをコンパイラ自身でパースし、 型推論やエラーの内容などをIDE側に通知するプロトコルである。 +主要なJavaのLanguage Serverの実装であるeclipse.jdt.ls\cite{eclipse.jdt.ls}では、 LanguageServerの機能として未実装のメソッドを検知する機能が実装されている。\cite{eclipse_pull322} +この機能を応用してvscode上から未実装のメソッドを特定し、 雛形を生成する機能がある。 +他にもIntelliJ IDEなどの商用IDEでは、 IDEが独自に未実装のメソッドを検知、雛形を生成する機能を実装している。 + + +golangの場合は主に\texttt{josharian/impl}\cite{golang_impl}が使われている。 +これはインストールすると\texttt{impl}コマンドが使用可能になり、 実装したいInterfaceの型と、 Interfaceを実装するImplの型(レシーバ)を与えることで雛形が生成される。 +主要なエディタであるvscodeのgolangの公式パッケージである\texttt{vscode-go}\cite{vscode-go}でも導入されており、 vscodeから呼び出すことが可能である。 +vscode以外にもvimなどのエディタから呼び出すことや、 シェル上で呼び出して標準出力の結果を利用することが可能である。 + +\section{GearsOSでのInterfaceを満たすCbCの雛形生成} +GearsOSでも同様のInterfaceの定義から実装するCodeGearの雛形を生成したい。 +LanguageServerの導入も考えられるが、 今回の場合はC言語のLanguageServerをCbC用にまず改良し、 さらにGearsOS用に書き換える必要がある。 +現状のGearsOSが持つシンタックスはCbCのシンタックスを拡張しているものではあるが、これはCbCコンパイラ側には組み込まれていない。 +LanguageServerをGearsOSに対応する場合、 CbCコンパイラ側にGearsOSの拡張シンタックスを導入する必要がある。 +CbCコンパイラ側への機能の実装は、 比較的難易度が高いと考えらる。 +CbCコンパイラ側に手をつけず、 Interfaceの入出力の検査は既存のGearsOSのビルドシステム上に組み込みたい。 + +対してgolangの\texttt{impl}コマンドのように、 シェルから呼び出し標準出力に結果を書き込む形式も考えられる。 +この場合は実装が比較的容易かつ、 コマンドを呼び出して標準出力の結果を使えるシェルやエディタなどの各プラットフォームで使用可能となる。 +先行事例を参考に、コマンドを実行して雛形ファイルを生成するコマンド\texttt{impl2cbc.pl}をGearsOSに導入した。 +\texttt{impl2cbc.pl}の処理の概要を図\ref{fig:impl2cbc}に示す。 + + +\begin{figure}[hp] + \begin{center} + \includegraphics[width=130mm]{drawio/impl2cbc.pdf} + \end{center} + \caption{impl2cbcの処理の流れ} + \label{fig:impl2cbc} + \end{figure} + +\subsection{雛形生成の手法} + + +Interfaceでは入力の引数がImplと揃っている必要があるが、 第一引数は実装自身のインスタンスがくる制約となっている。 +実装自身の型は、Interface定義時には不定である。 +その為、 GearsOSではInterfaceのAPIの宣言時にデフォルト型変数\texttt{Impl}を実装の型として利用する。 +デフォルト型\texttt{Impl}を各実装の型に置換することで自動生成が可能となる。 + + +実装すべきCodeGearはInterfaceとImpl側の型を見れば定義されている。 +\texttt{\_\_code}で宣言されているものを逐次生成すればよいが、 継続として呼び出されるCodeGearは具体的な実装を持たない。 +GearsOSで使われているInterfaceには概ね次の継続である\texttt{next}が登録されている。 +\texttt{next}そのものはInterfaceを呼び出す際に、入力として与える。 +その為各Interfaceに入力として与えられた\texttt{next}を保存する場所は存在するが、 nextそのものの独自実装は各Interfaceは所持しない。 +したがってこれをInterfaceの実装側で明示的に実装することはできない。 +雛形生成の際に、入力として与えられるCodeGearを生成してしまうと、プログラマに混乱をもたらしてしまう。 + +入力として与えられているCodeGearは、Interfaceに定義されているCodeGearの引数として表現されている。 +コードに示す例では、\texttt{whenEmpty}は入力して与えられているCodeGearである。 +雛形を生成する場合は、入力として与えられたCodeGearを除外して出力を行う。 +順序はInterfaceをまず出力した後に、 Impl側を出力する。 + + +\subsection{コンストラクタの自動生成} +雛形生成では他にコンストラクタの生成も行う。 +GearsOSのInterfaceのコンストラクタは、 メモリの確保及び各変数の初期化を行う。 +メモリ上に確保するのは主にInterfaceとImplのそれぞれが基本となっている。 +Interfaceによっては別のDataGearを内包しているものがある。 +その場合は別のDataGearの初期化もコンストラクタ内で行う必要があるが、 自動生成コマンドではそこまでの解析は行わない。 + + +コンストラクタのメンバ変数はデフォルトでは変数は0、ポインタの場合はNULLで初期化するように生成する。 +このスクリプトで生成されたコンストラクタを使う場合、 CbCファイルから該当する部分を削除すると、\texttt{generate\_stub.pl}内でも自動的に生成される。 +自動生成機能を作成すると1CbCファイルあたりの記述量が減る利点がある。 + + + +明示的にコンストラクタが書かれていた場合は、 Perlスクリプト内での自動生成は実行しないように実装した。 +これはオブジェクト指向言語のオーバーライドに相当する機能と言える。 +現状のGearsOSで使われているコンストラクタは、 基本は\texttt{struct Context*}型の変数のみを引数で要求している。 +しかしオブジェクトを識別するためにIDを実装側に埋め込みたい場合など、 コンストラクタ経由で値を代入したいケースが存在する。 +この場合はコンストラクタの引数を増やす必要や、 受け取った値をインスタンスのメンバに書き込む必要がある。 +具体的にどの値を書き込めば良いのかまではPerlスクリプトでは判定することができない。 +このような細かな調整をする場合は、 generate\_stub.pl側での自動生成はせずに、 雛形生成されたコンストラクタを変更すれば良い。 +あくまで雛形生成スクリプトはプログラマ支援であるため、 いくつかの手動での実装は許容している。
--- a/paper/chapter/gears.tex Sun Jan 31 22:42:23 2021 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,85 +0,0 @@ -\chapter{GearsOS} - -GearsOSとはContinuation Based Cを用いて実装しているOSプロジェクトである。 -CodeGearとDataGearを基本単位として実行する。 -GearsOSはOSとして実行する側面と、 CbCのシンタックスを拡張した言語フレームワークとしての側面がある。 - -\section{GearsOSのビルドシステム} -GearsOSではビルドツールにCMakeを利用している。 -ビルドフローを図\ref{fig:gearsbuild1}に示す。 -CMakeはautomakeなどのMakeファイルを作成するツールに相当するものである。 -GearsOSでプログラミングする際は、ビルドしたいプロジェクトをCMakeLists.txtに記述する。 -CMakeは自身がコンパイルをすることはなく、ビルドツールであるmakeやninja-buildに処理を移譲している。 -CMakeはmakeやninja-buildが実行可能なMakefile、 build.ninjaの生成までを担当する。 - - -GearsOSのビルドでは直接CbCコンパイラがソースコードをコンパイルすることはなく、 間にPerlスクリプトが2種類実行される。 -Perlスクリプトはビルド対象のGearsOSで拡張されたCbCファイルを、純粋なCbCファイルに変換する。 -ほかにGearsOSで動作する例題ごとに必要な初期化関数なども生成する。 -Perlスクリプトで変換されたCbCファイルなどをもとにCbCコンパイラがコンパイルを行う。 -ビルドの処理は自動化されており、 CMake経由でmakeやninjaコマンドを用いてビルドする。 - -\begin{figure}[hp] - \begin{center} - \includegraphics[width=120mm]{drawio/geasflow1.pdf} - \end{center} - \caption{GearsOSのビルドフロー} - \label{fig:gearsbuild1} - \end{figure} - -\section{pmake} -GearsOSをビルドする場合は、x86アーキテクチャのマシンからビルドするのが殆どである。 -この場合ビルドしたバイナリはx86向けのバイナリとなる。 -これはビルドをするホストマシンに導入されているCbCコンパイラがx86アーキテクチャ向けにビルドされたものである為である。 - -CbCコンパイラはGCCとllvm/clang上に構築した2種類が主力な処理系である。 -LVM/clangの場合はLLVM側でターゲットアーキテクチャを選択することが可能である。 -GCCの場合は最初からjターゲットアーキテクチャを指定してコンパイラをビルドする必要がある。 - -時にマシンスペックの問題などから、 別のアーキテクチャ向けのバイナリを生成したいケースがある。 -教育用マイコンボードであるRaspberry Pi\cite{rpi}はARMアーキテクチャが搭載されている。 -Raspberry Pi上でGearsOSのビルドをする場合、 ARM用にビルドされたCbCコンパイラが必要となる。 -Raspberry Pi自体は非力なマシンであるため、 GearsOSのビルドはもとよりCbCコンパイラの構築をRaspberry Pi上でするのは困難である。 -マシンスペックが高めのx86マシンからARM用のバイナリをビルドして、 Raspberry Piに転送し実行したい。 -ホストマシンのアーキテクチャ以外のアーキテクチャ向けにコンパイルすることをクロスコンパイルと呼ぶ。 - - -GearsOSはビルドツールにCMakeを利用しているので、 CMakeでクロスコンパイル出来るように工夫をする必要がある。 -ビルドに使用するコンパイラやリンカはCMakeが自動探索し、 決定した上でMakefileやbuild.ninjaファイルを生成する。 -しかしCMakeは今ビルドしようとしている対象が、自分が動作しているアーキテクチャかそうでないか、クロスコンパイラとして使えるかなどはチェックしない。 -つまりCMakeが自動でクロスコンパイル対応のGCCコンパイラを探すことはない。 -その為そのままビルドするとx86用のバイナリが生成されてしまう。 - - -CMakeを利用してクロスコンパイルする場合、CMakeの実行時に引数でクロスコンパイラを明示的に指定する必要がある。 -この場合x86のマシンからARMのバイナリを出力する必要があり、 コンパイラやリンカーなどをARMのクロスコンパイル対応のものに指定する必要がある。 -また、 xv6の場合はリンク時に特定のリンカスクリプトを使う必要がある。 -これらのリンカスクリプトもCMake側に、 CMakeが提供しているリンカ用の特殊変数を使って自分で組み立てて渡す必要がある。 -このようなCMakeの処理を手打ちで行うことは難しいので、 \texttt{pmake.pl}を作成した。 -\texttt{pmake.pl}の処理の概要を図\ref{fig:pmake}に示す。 -\texttt{pmake.pl}はPerlスクリプトで、 シェルコマンドを内部で実行しクロスコンパイル用のオプションを組み立てる。 -\texttt{pmake.pl}を経由してCMakeを実行すると、 makeコマンドに対応するMakefile、 ninja-buildに対応するbuild.ninjaが生成される。 -以降はcmakeではなくmakeなどのビルドツールがビルドを行う。 - -\begin{figure}[h] - \begin{center} - \includegraphics[width=160mm]{drawio/pmake.pdf} - \end{center} - \caption{pmake.plの処理フロー} - \label{fig:pmake} - \end{figure} - - - - - \section{Interfaceの取り扱い方法の検討} - - GearsOSのInterfaceはモジュール化の仕組みと\texttt{goto}文での引数の一時保管場所としての機能を持っている。 -InterfaceのImplementのヘッダーファイルを実装したことで、 GearsOS上でInterfaceを実装する際に新たな方法での実装を検討した。 -ImplementのCodeGearは今まではInterfaceで定義したCodeGearと1対1対応していた。 -ImplementのCodeGearからgotoする先は、 入力として与えられたCodeGearか、 Implement内で独自に定義したCodeGearにgotoするケースとなっていた。 -後者の独自に定義したCodeGearにgotoするケースも、 実装のCbCファイルの中に記述されているCodeGearに遷移していた。 - -GearsOSを用いてxv6 OSを再実装した際に、 実装側のCodeGearを細かく別けて記述した。 -細分化によって1つのCbCファイルあたりのCodeGearの記述量が増えてしまうという問題が発生した。 -見通しをよくする為に、 Interfaceで定義したCodeGearと直接対応するCodeGearの実装と、 それらからgotoするCodeGearで実装ファイルを分離することを試みた。
--- a/paper/chapter/introduction.tex Sun Jan 31 22:42:23 2021 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,80 +0,0 @@ -\chapter{OSとアプリケーションの信頼性} - -コンピューター上では様々なアプリケーションが常時動作している。 -動作しているアプリケーションは信頼性が保証されていてほしい。 -信頼性の保証には、 実行してほしい一連の挙動をまとめた仕様と、 それを満たしているかどうかの確認である検証が必要となる。 -アプリケーション開発では検証に関数や一連の動作をテストを行う方法や、デバッグを通して信頼性を保証する手法が広く使われている。 - -実際にアプリケーションを動作させるOSは、アプリケーションよりさらに高い信頼性が保証される必要がある。 -OSはCPUやメモリなどの資源管理と、 ユーザーにシステムコールなどのAPIを提供することで抽象化を行っている。 -OSの信頼性の保証もテストコードを用いて証明することも可能ではあるが、 アプリケーションと比較するとOSのコード量、 処理の量は膨大である。 -またOSはCPU制御やメモリ制御、 並列・並行処理などを多用する。 -テストコードを用いて処理を検証する場合、テストコードとして特定の状況を作成する必要がある。 -実際にOSが動作する中でバグやエラーを発生する条件を、 並列処理の状況などを踏まえてテストコードで表現するのは困難である。 -非決定的な処理を持つOSの信頼性を保証するには、 テストコード以外の手法を用いる必要がある。 - - -テストコード以外の方法として、 形式手法的と呼ばれるアプローチがある。 -形式手法の具体的な検証方法の中で、 証明を用いる方法\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402}とモデル検査を用いる方法がある。 -証明を用いる方法ではAgda\cite{agda}やCoq\cite{coq}などの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。 -Curry-Howard同型対応則により、型と論理式の命題が対応する。 -この型を導出するプログラムと実際の証明が対応する。 -証明には特定の型を入力として受け取り、証明したい型を生成する関数を作成する。 -整合性の確認は、記述した関数を元に定理証明支援系が検証する。 -証明を使う手法の場合、 実際の証明を行うのは定理証明支援系であるため、 定理証明支援系が理解できるプログラムで実装する必要がある。 -AgdaやCoqの場合はAgda、 Cow自身のプログラムで記述する必要がある。 -しかしAgdaで証明ができてもAgdaのコードを直接OSのソースコードとしてコンパイルすることはできない。 -Agda側でCのソースコードを吐き出せれば可能ではあるが、 現状は検証したコードと実際に動作するコードは分離されている。 -検証されたアルゴリズムをもとにCで実装することは可能であるが、 この場合移植時にバグが入る可能性がある。 -検証ができているソースコードそのものを使ってOSを動作させたい。 - - -他の形式手法にモデル検査がある。 -モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。 -例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。 -モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。 -OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。 -しかしOSの処理は膨大である。 -すべての存在可能な状態を数え上げるモデル検査では状態爆発が問題となる。 -状態を有限に制限したり抽象化を行う必要がある。 - - -OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。 -その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。 -OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。 -範囲が限られているため、有限時間でモデル検査などで検証することが可能である。 -この為にはOSの処理を証明しやすくする表現で実装する必要がある。\cite{hyperkernel} -証明しやすい表現の例として、 状態遷移ベースでの実装がある。 - - -証明を行う対象の計算は、 その意味が大きく別けられる。 -OSやプログラムの動作においては本来したい計算がまず存在する。 -これはプログラマが通常プログラミングするものである。 -これら本来行いたい処理のほかに、 CPU、メモリ、スレッドなどの資源管理なども必要となる。 -前者の計算をノーマルレベルの計算と呼び、後者をメタレベルの計算と呼ぶ。 -OSはメタ計算を担当していると言える。 -ユーザーレベルから見ると、データの読み込みなどは資源へのアクセスが必要であるため、システムコールを呼ぶ必要がある。 -システムコールを呼び出すとOSが管理する資源に対して何らかの副作用が発生するメタ計算と言える。 -副作用は関数型プログラムの見方からするとモナドと言え、 モナドもメタ計算ととらえることができる。 -OS上で動くプログラムはCPUにより並行実行される。この際の他のプロセスとの干渉もメタレベルの処理である。 -実装のソースコードはノーマルレベルであり検証用のソースコードはメタ計算だと考えると、OSそのものが -検証を行ない、システム全体の信頼を高める機能を持つべきだと考える。 -ノーマルレベルの計算を確実に行う為には、メタレベルの計算が重要となる。 - - -プログラムの整合性の検証はメタレベルの計算で行いたい。 -ユーザーが実装したノーマルレベルの計算に対応するメタレベルの計算を、自由にメタレベルの計算で証明したい。 -またメタレベルで検証ががすでにされたプログラムがあった場合、都度実行ユーザーの環境で検証が行われるとパフォーマンスに問題が発生する。 -この場合はメタレベルの計算を検証をするもの、しないものと切り替えられる柔軟なAPIが必要となる。 -メタレベルの計算をノーマルレベルの計算と同等にプログラミングできると、動作するコードに対して様々なアプローチが掛けられる。 -この為にはノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。 - -プログラムのノーマルレベルの計算とメタレベルの計算を一貫して行う言語として、 Continuation Based C(CbC)を用いる。 -CbCは基本\texttt{goto文}で\texttt{CodeGaar}というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と呼ばれる隠れた状態を持たない。 -このため、計算のための情報は\texttt{CodeGear}の入力にすべてそろっている。 -そのうちのいくつかはメタ計算、つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(\texttt{DataGear})である。 -メタ計算とノーマルレベルの区別は入力のどこを扱うかの差に帰着される。 -CbCはCと互換性のあるCの下位言語である。 -CbCは\texttt{GCC}\cite{gcc}\cite{weko_82695_1}あるいは\texttt{LLVM}\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。 -Cのコンパイルシステムを使える為に、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。 -またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{agda-ryokka}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
--- a/paper/master_paper.tex Sun Jan 31 22:42:23 2021 +0900 +++ b/paper/master_paper.tex Mon Feb 01 08:32:58 2021 +0900 @@ -94,11 +94,11 @@ \lstlistoflistings %chapters -\input{chapter/introduction.tex} -\input{chapter/01-cbc.tex} -\input{chapter/gears.tex} -\input{chapter/02-perl.tex} -\input{chapter/02-interface.tex} +\input{chapter/01-introduction.tex} +\input{chapter/02-cbc.tex} +\input{chapter/03-gears.tex} +\input{chapter/04-perl.tex} +\input{chapter/04-interface.tex} \input{chapter/conclusion.tex}