Mercurial > hg > Papers > 2021 > anatofuz-master
changeset 155:6f940582768f
...
author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 16 Feb 2021 15:21:11 +0900 |
parents | 90419bf3386e |
children | 951d8499d773 |
files | paper/chapter/01-introduction.tex paper/chapter/02-cbc.tex paper/chapter/03-gears.tex paper/chapter/04-interface.tex paper/master_paper.pdf |
diffstat | 5 files changed, 17 insertions(+), 16 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/chapter/01-introduction.tex Tue Feb 16 15:02:05 2021 +0900 +++ b/paper/chapter/01-introduction.tex Tue Feb 16 15:21:11 2021 +0900 @@ -3,7 +3,7 @@ コンピューター上では様々なアプリケーションが常時動作している。 動作しているアプリケーションは信頼性が保証されていてほしい。 信頼性の保証には、 実行してほしい一連の挙動をまとめた仕様と、 それを満たしているかどうかの確認である検証が必要となる。 -アプリケーション開発では検証に関数や一連の動作をテストを行う方法や、デバッグを通して信頼性を保証する手法が広く使われている。 +アプリケーション開発では関数や一連の動作をテストで検証する方法や、デバッグを通して信頼性を保証する手法が広く使われている。 実際にアプリケーションを動作させるOSは、アプリケーションよりさらに高い信頼性が保証される必要がある。 OSはCPUやメモリなどの資源管理と、 ユーザーにシステムコールなどのAPIを提供することで抽象化を行っている。 @@ -43,8 +43,8 @@ OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。 その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。 -OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。 -範囲が限られているため、有限時間でモデル検査などで検証することが可能である。 +OSを巨大な状態遷移マシンと考えると、 巨大なOSの処理の状態遷移の一部分を切り出すことができる。 +状態を切り出すと範囲が限られているため、有限時間でモデル検査などで検証することが可能である。 この為にはOSの処理を証明しやすくする表現で実装する必要がある\cite{hyperkernel}。 証明しやすい表現の例として、 状態遷移ベースでの実装がある。
--- a/paper/chapter/02-cbc.tex Tue Feb 16 15:02:05 2021 +0900 +++ b/paper/chapter/02-cbc.tex Tue Feb 16 15:21:11 2021 +0900 @@ -1,7 +1,8 @@ \chapter{Continuation Based C} Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。 CbCでは通常の関数呼び出しの他に、 関数呼び出し時のスタックの操作を行わず、次のコードブロックに\texttt{jmp}命令で移動する継続が導入されている。 -この継続はSchemeのcall/ccなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である為に軽量である事から軽量継続と呼べる。 +この継続はSchemeのcall/ccなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である。 +call/ccの継続と比較して軽量である事から軽量継続と呼べる。 またCbCではこの軽量継続を用いて\texttt{for}文などのループの代わりに再起呼び出しを行う。 これは関数型プログラミングでのTail callスタイルでプログラミングすることに相当する。 Agda よる関数型のCbCの記述も用意されている。
--- a/paper/chapter/03-gears.tex Tue Feb 16 15:02:05 2021 +0900 +++ b/paper/chapter/03-gears.tex Tue Feb 16 15:21:11 2021 +0900 @@ -42,7 +42,7 @@ GearsOSでのデータの単位から見ると、 MetaDataGearに相当する。 Contextの概要図を図\ref{fig:context}に、実際のCbC上での定義をソースコード\ref{src:structContext}に示す。 -ContextはMetaDataGearである為に、 ノーマルレベルのCodeGearからはcontextは直接参照しない。 +ContextはMetaDataGearである為に、 ノーマルレベルのCodeGearからはcontextを直接参照しない。 contextの操作をしてしまうと、メタレベルとノーマルレベルの分離をした意味がなくなってしまう為である。 Contextはプロセスに相当するので、ユーザープログラムごとにCotnextが存在する。 @@ -67,7 +67,7 @@ ContextはGearsOSの計算で使用されるすべてのDataGearとCodeGearを持つ。 つまりGearsOSで使われるCodeGearとDataGearは、 誰かのContextに必ず書き込まれている。 -各CodeGear、DataGearはContextはそれぞれ配列形式でContextにデータを格納する場所が用意されている。 +各CodeGear、DataGearは、それぞれ配列形式でContextにデータを格納する場所が用意されている。 CodeGearが保存されている配列はソースコード\ref{src:structContext}の6行目で定義している\texttt{code}である。 StubCodeGearはContextのみを引数で持つため、 \texttt{\_\_code stub(struct Context*)}の様なCodeGearの関数ポインタのポインタ、つまりCodeGearの配列としての定義されている。 これは前述したStubCodeGearの関数ポインタが格納されており、 \texttt{\_\_code meta}でのディスパッチに利用される。 @@ -101,7 +101,7 @@ ソースコード\ref{src:StackPush}に示すノーマルレベルで記述したCodeGearを、Perlスクリプトによって変換した結果をソースコード\ref{src:StackPushStub}に示す。 常に自分自身のContextをCodeGearは入力の形で受け取る為、変換後の\texttt{pushSingleLinkedStack}は、 第1引数にContextが加わっている。 -pushSingleLinkedStackは引数は3つ要求していた。 +pushSingleLinkedStackは引数を3つ要求していた。 これらの引数は生成された\texttt{pushSingleLinkedStack\_stub}がContextの特定の場所から取り出す。 このCodeGearはGearsOSのInterfaceを利用しており、 Stack Interaceの実装となっている。 マクロ\texttt{Gearef}は、 contextのInterface用のDataGearの置き場所にアクセスするマクロであり、 Stack Interfaceの置き場所から、引数情報を取得している。 @@ -228,7 +228,7 @@ Interface宣言時には具体的にどの型が来るかは不定であるため、 キーワードを利用している。 ImplはInterfaceのAPI呼び出し時に、メタレベルの処理であるStubCodeGearで自動で入力される。 その為ユーザーはInterfaceのAPIを呼び出す際は、 このImplに対応する引数は設定しない。 -すなわち実際にいれるべき引数は、 Implを抜いたものになる。 +すなわち実際に設定すべき引数は、 Implを抜いたものになる。 第1引数にImplが来ないCodeGearとして\texttt{whenEmpty}と\texttt{next}がQueueの例で存在している。 これらはAPIの呼び出し時に継続として渡されるCodeGearであるため、 Interfaceの定義時には不定である。 @@ -280,7 +280,7 @@ \subsection{goto時のContextとInterfaceの関係} Interfaceはモジュール化の仕組みとしてでなく、 メタレベルでは一時的な変数の置き場所としても利用している。 -ソースコード\ref{src:queueTake}で呼び出しているtakeは、 OutputDataGearがあるAPIである。 +ソースコード\ref{src:queueTake}で呼び出しているtakeは、 OutputDataGearが存在するAPIである。 このOutputDataGearは、 context内のDataGearの置き場所であるdata配列の、 Interfaceのデータ格納場所に書き込まれる。 OutputDataGearを取得する場合は、 継続先でなく、APIのInterfaceから取得しないといけない。 @@ -365,7 +365,7 @@ CMake自身はコンパイルに必要なコマンドを実行することはなく、ビルドツールであるmakeやninja-buildに処理を移譲している。 CMakeはmakeやninja-buildが実行時に必要とするファイルであるMakefile、 build.ninjaの生成までを担当する。 -\lstinputlisting[label=src:cmakeGearsMacro, caption=CMakeList.txt内でのプロジェクト定義]{src/GearsMacroCMake.txt} +\lstinputlisting[label=src:cmakeGearsMacro, caption=CMakeLists.txt内でのプロジェクト定義]{src/GearsMacroCMake.txt} GearsOSのビルドでは直接CbCコンパイラがソースコードをコンパイルすることはなく、 間にPerlスクリプトが2種類実行される。 @@ -393,7 +393,7 @@ これらのPerlスクリプトはプログラマが自分で動かすことはない。 Perlスクリプトの実行手順はCMakeLists.txtに記述しており、 makeやninja-buildでのビルド時に呼び出される(ソースコード \ref{src:cmake1})。 -\lstinputlisting[label=src:cmake1, caption=CMakeList.txt内でのPerlの実行部分]{src/cmakefile.1.txt} +\lstinputlisting[label=src:cmake1, caption=CMakeLists.txt内でのPerlの実行部分]{src/cmakefile.1.txt} 従来のGearsOSではPerlスクリプトを利用した変換時には、厳格なエラーチェックを行っていなかった。 例えばContextへの値の代入の式が正常に生成できなくても、 Perlスクリプトは正常に動作を終了したことにしてしまう。 @@ -424,7 +424,7 @@ これらの処理で、 1つのGearsOSのファイル自身と、 呼び出しているInterfaceの定義ファイルに実装されているCodeGearとDataGearの組を取得する。 データの収集は、入力で与えられたファイルを1行ずつ読み込み、 あらかじめ設定した正規表現にパターンマッチすることで処理を行っている。 ソースコード\ref{src:generateExampleInterface}は、GearsOSのソースコード中でInterfaceの使用宣言部分のパターンマッチ処理である。 -\lstinputlisting[label=src:generateExampleInterface, caption=CMakeList.txt内でのPerlの実行部分]{src/generateStubInterfaceExample.pl} +\lstinputlisting[label=src:generateExampleInterface, caption=Interfaceの使用宣言部分のパターンマッチ]{src/generateStubInterfaceExample.pl} ここでは使用しているInterfaceの名前を変数\texttt{\$interfaceHeader}にキャプチャし、 Interfaceの読み込み処理を8行目の\texttt{includeInterface}関数で実行している。 includeInterface関数の中ではgetDataGearを呼び出し、CodeGear、DataGearの情報を取得している。
--- a/paper/chapter/04-interface.tex Tue Feb 16 15:02:05 2021 +0900 +++ b/paper/chapter/04-interface.tex Tue Feb 16 15:21:11 2021 +0900 @@ -23,7 +23,7 @@ これをユーザーに強く意識させる必要がある。 golangにもInterfaceの機能が実装されている。 -golangの場合はInterfaceは関数の宣言部分のみを記述するルールになっている。 +golangでは、 Interfaceは関数の宣言部分のみを記述するルールになっている。 変数名は含まれていても含まなくても問題ない。 \begin{lstlisting}[frame=lrbt,label=src:golang_interface,caption={golangのinterface宣言}] @@ -236,7 +236,7 @@ Implementの宣言の構文では、 まず\texttt{\#impl}の後ろに実装したいIntefaceの名前を入れる。 続く\texttt{as}キーワードの後ろに、 Implementの型名を記述する。 宣言はgenerate\_stub.plが読み取り、 変換した後のCbCファイルからは該当する行が削除される。 -\lstinputlisting[label=src:implHeader, caption=DataGearの使用の宣言]{src/implHeader.h} +\lstinputlisting[label=src:implHeader, caption=Interface実装の宣言]{src/implHeader.h} @@ -253,14 +253,14 @@ これは使用したいDataGearの定義ファイルを\texttt{\#data}の後ろに記述する。 SingleLinkedStackの場合の例をソースコード\ref{src:implStackdef}に示す。 この例ではNodeとElementを使用している。 -\lstinputlisting[label=src:implStackdef, caption=DataGearの使用の宣言]{src/implStackDef.cbc} +\lstinputlisting[label=src:implStackdef, caption=DataGearを使用する宣言]{src/implStackDef.cbc} この宣言は、使用しているDataGearを調査しcontext.hを作製するgenerate\_context.plが発見できなければならない。 しかしgenerate\_context.plは、メタ情報を含む形にgenerate\_stub.plはトランスパイルした後に実行される。 GearsOSで拡張したマクロの用なInterface関連の宣言はここで消されてしまう。 DataGearの使用の宣言は、コメントの形で変換後のファイルに書き出すようにし、generate\_context.plでも参照可能にした。 SingleLinkedStackの例題に対応する変換後のコードを、ソースコード\ref{src:implStackdefAfter}に示す。 -\lstinputlisting[label=src:implStackdefAfter, caption=DataGearの使用の宣言のPerlによる変換後]{src/IncludeNode.cbc} +\lstinputlisting[label=src:implStackdefAfter, caption=DataGearを使用する宣言のPerlによる変換後]{src/IncludeNode.cbc} \section{Interface APIに対応したCodeGearの名前の自動変換} \label{sec:autoCodeGearName}