Mercurial > hg > Papers > 2019 > mitsuki-master
changeset 5:94ac73bc7829
update
author | mir3636 |
---|---|
date | Mon, 21 Jan 2019 14:31:36 +0900 |
parents | aeabc8477ec1 |
children | 7d9441dd343e |
files | paper/gearsOS.tex paper/introduction.tex paper/meta_computation.tex |
diffstat | 3 files changed, 56 insertions(+), 33 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/gearsOS.tex Sun Jan 20 21:14:08 2019 +0900 +++ b/paper/gearsOS.tex Mon Jan 21 14:31:36 2019 +0900 @@ -12,7 +12,7 @@ \begin{figure}[ht] \begin{center} - \includegraphics[width=70mm]{./fig/gears_structure} + \includegraphics[width=120mm]{./fig/gears_structure} \end{center} \caption{Gears OS の構成図} \label{fig:gearsos}
--- a/paper/introduction.tex Sun Jan 20 21:14:08 2019 +0900 +++ b/paper/introduction.tex Mon Jan 21 14:31:36 2019 +0900 @@ -34,7 +34,7 @@ CbC は関数呼出時の暗黙の環境(Environment)を使わずに、コードの単位を行き来できる引数付き goto 文(parametarized goto)を持つ C と互換性のある言語である。 これを用いて、Code Gear と Data Gear、さらにそのメタ構造を導入する。 これらを用いて、検証された Gears OS を構築したい。 -%図\ref{fig:MetaGear}。 +図\ref{fig:MetaGear}。 検証には定理証明支援系である Agda を用いる。 Gears OS の記述はそのまま Agda に落ちる。 CbC で記述することによって検証された OS を実装することができる。 @@ -42,13 +42,13 @@ また、Gears の記述をモジュール化するために Interface を導入した。 さらに並列処理の記述用にpar goto 構文を導入する。 これらの機能は Agda 上で継続を用いた関数型プログラムに対応するようになっている。 -%\begin{figure}[ht] -% \begin{center} -% \includegraphics[width=70mm]{./fig/MetaGear.pdf} -% \end{center} -% \caption{Gearsのメタ計算} -% \label{fig:MetaGear} -%\end{figure} +\begin{figure}[ht] + \begin{center} + \includegraphics[width=70mm]{./fig/MetaGear.pdf} + \end{center} + \caption{Gearsのメタ計算} + \label{fig:MetaGear} +\end{figure} 本論文では Interface と par goto の実装を行なった。 %実際の修正は考えてない
--- a/paper/meta_computation.tex Sun Jan 20 21:14:08 2019 +0900 +++ b/paper/meta_computation.tex Mon Jan 21 14:31:36 2019 +0900 @@ -1,8 +1,10 @@ \chapter{Gears におけるメタ計算} Gears OS ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を用いる。 プログラムの処理の単位を Code Gear、データの単位を Data Gear と呼ぶ。 + Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、 これらを用いてメタ計算を実現する。 + Gears OS は処理やデータの構造が Code Gear、Data Gear に閉じているため、 これにより実行時間、メモリ使用量などを予測可能なものにすることが可能になる。 @@ -85,9 +87,6 @@ } __code assert3(struct Node* node, struct Stack* stack) { - /* - assert in normal level - */ assert(node->color == Red); goto exit_code(0); } @@ -97,15 +96,6 @@ \section{Meta Code Gear、Meta Data Gear} Gears OS ではメタ計算 を Meta Code Gear、Meta Data Gear で表現する。 Meta Code Gear は通常の Code Gear の直後に遷移され、メタ計算を実行する。 -これを図示したものが図\ref{fig:metaCS}である。 - -\begin{figure}[ht] - \begin{center} - \includegraphics[width=70mm]{fig/metaCS.pdf} - \end{center} - \caption{Gears でのメタ計算} - \label{fig:metaCS} -\end{figure} Gears OS では Context と呼ばれる、使用されるすべての Code Gear、Data Gear を持つ Meta Data Gear を持っている。 Gears OS は必要な Code Gear、Data Gear を参照したい場合、この Context を通す必要がある。 @@ -121,6 +111,46 @@ メタレベルの記述は Perl スクリプトによって生成される。 stub Code Gear と meta によって Code Gear で記述される。 +リスト \ref{MetaCodeGear} は生成された Meta Code Gear のコードである。 + +\begin{lstlisting}[frame=lrbt,label=Gears_code,caption={\footnotesize MetaCodeGear}] + +__code popSingleLinkedStack_stub(struct Context* context) { + SingleLinkedStack* stack = (SingleLinkedStack*)GearImpl(context, Stack, stack); + enum Code next = Gearef(context, Stack)->next; + Data** O_data = &Gearef(context, Stack)->data; + goto popSingleLinkedStack(context, stack, next, O_data); +} + +__code popSingleLinkedStack(struct Context *context,struct SingleLinkedStack* stack, enum Code next,union Data **O_data) { + Data* data = *O_data; + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + *O_data = data; + goto meta(context, next); +} + +__code meta(struct Context* context, enum Code next) { + goto (context->code[next])(context); +} + +\end{lstlisting} + +Gears OS では継続先の Code Gear へと継続する前に Meta Code Gear である +stub Code Gear へと継続する。 + +stub Code Gear では、継続先が求める Input Code Gear、Output Code Gear を Context から参照している。 +Gearef は Context から Data Gear を参照するためのマクロである。 +stub Code Gear は自動生成されるため、ユーザーレベルでは Context を直接触ることなくプログラミングできる。 + +また、Code Gear は継続の際 meta へと goto する。 +Context はすべての Code Gear のリストを持っており、継続先の Code Gear のアドレスは +enum で対応付けられた Code Gear のアドレスのリストを参照して継続を行う。 + Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される。 Interface は使用される Data Gear の定義と、それに対する操作を行う Code Gear の集合である。 @@ -128,18 +158,14 @@ Interface の操作に対応する Code Gear の引数は Interface に定義されている Data Gear を通して指定される。 一つの実行スレッド内で使われる Interface の Code Gear と Data Gear は Context に格納される。 -%Code Gear の継続は関数型プログラミングからみると継続先の Context を含む Closure となっている。 -%これを記述するために継続に不定長引数を追加する構文をスクプリトの変換機能として用意した。Code \ref{varargnext} -%メタ計算側ではこれらの Context を常に持ち歩いているので goto 文で引数を用いることはなく、 -%行き先は Code Gear の番号のみで指定される。 - -%\lstinputlisting[label=varargnext, caption=不定長引数を持つ継続]{./src/varargnext.cbc} +Code Gear の継続は関数型プログラミングからみると継続先の Context を含む Closure となっている。 +これを記述するために継続に不定長引数を追加する構文をスクプリトの変換機能として用意した。 +メタ計算側ではこれらの Context を常に持ち歩いているので goto 文で引数を用いることはなく、 +行き先は Code Gear の番号のみで指定される。 これにより Interface 間の呼び出しを C++ のメソッド呼び出しのように記述することができる。 Interface の実装は、Context 内に格納されているので、オブジェクトごとに実装を変える多様性を実現できている。 -呼び出された Code Gear は必要な引数を Context から取り出す必要がある。 -これは スクリプトで生成された stub Meta Code Gear で行われる。 -Gears OS でのメタ計算は stub と goto のメタ計算の2箇所で実現される。 + Context を複製して複数の CPU に割り当てることにより並列実行を可能になる。 これによりメタ計算として並列処理を記述したことになる。 @@ -153,6 +179,3 @@ Gears OS ではメモリ管理は stub などのメタ計算部分で処理される。 例えば、寿命の短いスレッドでは使い捨ての線形アロケーションを用いる。 -%Meta Code Gear は通常の Code Gear の直後に遷移され、メタ計算を実行する。 - -%これを図示したものが図\ref{fig:metaCS}である。