Mercurial > hg > Papers > 2021 > anatofuz-master
changeset 152:c9fb8f47a921
...
author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 16 Feb 2021 14:52:49 +0900 |
parents | 9ae59ed5c53a |
children | db92350dc65f |
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, 12 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/chapter/01-introduction.tex Tue Feb 16 14:33:25 2021 +0900 +++ b/paper/chapter/01-introduction.tex Tue Feb 16 14:52:49 2021 +0900 @@ -45,7 +45,7 @@ その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。 OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。 範囲が限られているため、有限時間でモデル検査などで検証することが可能である。 -この為にはOSの処理を証明しやすくする表現で実装する必要がある。\cite{hyperkernel} +この為にはOSの処理を証明しやすくする表現で実装する必要がある\cite{hyperkernel}。 証明しやすい表現の例として、 状態遷移ベースでの実装がある。 @@ -102,4 +102,4 @@ これらのメタレベルの計算はコンパイル時に決定するために、自動化を行いたい。 本研究ではGearsOSの信頼性と拡張性の保証につながる、メタ計算に関するAPIについて考察する。 -GearsOSがメタ計算を自動生成しているPerlトランスパイラで従来のGearsOSのシステムよりさらに拡張性の充実と、信頼性の保証を図る。 \ No newline at end of file +GearsOSがメタ計算を自動生成しているPerlトランスパイラで従来のGearsOSのシステムよりさらに拡張性の充実と、信頼性の保証を図る。
--- a/paper/chapter/02-cbc.tex Tue Feb 16 14:33:25 2021 +0900 +++ b/paper/chapter/02-cbc.tex Tue Feb 16 14:52:49 2021 +0900 @@ -44,7 +44,7 @@ \lstinputlisting[label=src:cbcexample_test, caption=CbCの例題]{src/cbc_example_test.cbc} \lstinputlisting[label=src:cbcexample_test_c, caption=ソースコード\ref{src:cbcexample_test}のCでの実装]{src/cbc_example_test.c} CbCの場合は継続で進んでいくが、 C言語での実装はvoid型の返り値を持つ関数呼び出しで表現される。 -\texttt{codegear3}に遷移したタイミングで、 CbCはmain関数のスタックしか持たないが、 C言語ではcodegear1、codegear2のスタックをそれぞれ持つ違いがある。(図\ref{fig:cbc_vs_c}) +\texttt{codegear3}に遷移したタイミングで、 CbCはmain関数のスタックしか持たないが、 C言語ではcodegear1、codegear2のスタックをそれぞれ持つ違いがある(図\ref{fig:cbc_vs_c})。 \begin{figure}[tb] \begin{center}
--- a/paper/chapter/03-gears.tex Tue Feb 16 14:33:25 2021 +0900 +++ b/paper/chapter/03-gears.tex Tue Feb 16 14:52:49 2021 +0900 @@ -189,9 +189,10 @@ すべてのDataGearを管理する、Contextは計算で使うすべてのDataGearの型定義を持っている。 各DataGearは当然ではあるが別の型である。 例えばStack DataGearとQueue DataGearは、それぞれstruct Stackとstruct Queueで表現されるが、 C言語のシステム上別の型とみなされる。 -メタレベルで見れば、 この型定義は\texttt{union Data}型にすべて書かれている。 -しかしContextはこれらの型をすべてDataGearとして等しく扱う必要がある。 +メタレベルで見れば、 これらDataGearの型はcontext.hの中に構造体の形で型定義されている。 +Contextはこれらの型をすべてDataGearとして等しく扱う必要がある。 この為にC言語の共用体を使用し、汎用的なDataGearの型であるunion Data型を定義している。 +すべてのDataGearの型定義は、このunion Data型の中で定義されている。 共用体とは、構成するメンバ変数で最大の型のメモリサイズと同じメモリサイズになる特徴があり、複数の異なる型をまとめて管理することができる。 構造体と違い、1度に一つの型しか使うことができない。 @@ -231,7 +232,9 @@ 第1引数にImplが来ないCodeGearとして\texttt{whenEmpty}と\texttt{next}がQueueの例で存在している。 これらはAPIの呼び出し時に継続として渡されるCodeGearであるため、 Interfaceの定義時には不定である。 -その為\texttt{...}を用いて、不定なCodeGearとDataGearのClosureが来ると仮定している。 +GearsOSはCbCで実装されているため、 goto文で継続してきた場合、次の継続に使われる引数はスタック以外の場所から取り出す必要がある。 +\texttt{...}を用いて、不定なCodeGearとDataGearの組であるClosureが来ると仮定している。 +このClosureは実際にはContextであり、 GearsOSがContextからすべての値を取り出していることを意味している。 8行目で定義している\texttt{whenEmpty}はQueueの状態を確認し、空でなければ\texttt{next}、空であれば\texttt{whenEmpty}に継続する。 これらは呼び出し時にCodeGearを入力して与えることになる。 @@ -415,7 +418,7 @@ \end{figure} generate\_stub.plはGearsOSのソースコードを2回読む。 -1度目の読み込みは関数getDataGearが担当する。(図\ref{fig:aboutDataGear}) +1度目の読み込みは関数getDataGearが担当する(図\ref{fig:aboutDataGear})。 ソースコード中に登場するCodeGearと、CodeGearの入出力を検知する。 この際に\texttt{\#interface}構文でInterfaceの利用が確認された場合、 Interfaceの定義ファイルを開き、getDataGearをさらに呼び出す。 これらの処理で、 1つのGearsOSのファイル自身と、 呼び出しているInterfaceの定義ファイルに実装されているCodeGearとDataGearの組を取得する。 @@ -440,7 +443,7 @@ \end{figure} 1度ファイルを完全に読み込み、 CodeGear、DataGearの情報を取得し終わると、以降はその情報をもとに変換したファイルを書き出す。 -この書き出しはgenerateDataGear関数で行われる。(図\ref{fig:aboutgenerateDataGear}) +この書き出しはgenerateDataGear関数で行われる(図\ref{fig:aboutgenerateDataGear})。 ファイルを書き出す際は、 元のCbCファイルを再読み込みし、 変換する必要があるキーワードが出現するまでは、変換後のファイルに転記を行う。 例えば各CodeGearの最後に実行される\texttt{goto}文は、 GearsOSの場合はMetaCodeGearに継続するように、 対象を切り替える必要がある。 この為にgenerate\_stub.plは、goto文を検知するとcontext経由で引数のやりとりをするメタ処理を付け加える。
--- a/paper/chapter/04-interface.tex Tue Feb 16 14:33:25 2021 +0900 +++ b/paper/chapter/04-interface.tex Tue Feb 16 14:52:49 2021 +0900 @@ -82,7 +82,7 @@ Implementの型定義ファイルも、 Interfaceの型定義ファイルと似たシンタックスにしたい。 Implementの型定義ファイルで持たなければいけないのは、 どのInterfaceを実装しているかの情報である。 この情報は他言語ではInterfaceの実装を持つ型の宣言時に記述するケースと、型名の記述はせずに言語システムが実装しているかどうかを確認するケースが存在する。 -Javaでは\texttt{implements}キーワードを用いてどのInterfaceを実装しているかを記述する。\cite{javaimpl} +Javaでは\texttt{implements}キーワードを用いてどのInterfaceを実装しているかを記述する\cite{javaimpl}。 ソースコード\ref{src:javaimpl}では、\texttt{Pig}クラスは\texttt{Animal} Interfaceを実装している。 \lstinputlisting[label=src:javaimpl, caption=JavaのImplementキーワード]{src/java-interface-implements.java} golangではInterfaceの実装は特にキーワードを指定せずに、 そのInterfaceで定義しているメソッドを、Implementに相当する構造体がすべて実装しているかどうかでチェックされる。