Mercurial > hg > Papers > 2019 > mitsuki-master

--- a/paper/gearsOS.tex	Thu Feb 07 17:11:07 2019 +0900
+++ b/paper/gearsOS.tex	Fri Feb 08 05:05:15 2019 +0900
@@ -25,8 +25,6 @@
  \label{fig:gearsos}
 \end{figure}

-%Context は Task でもあり、Taskは通常のOSのスレッドに対応する。
-%Task は実行する Code Gear と Data Gear をすべて持っている。
 TaskManager は Task を実行する Worker の生成、管理、Task の送信を行う。
 Gears OS における Task Queue は Synchronized Queue で実現される。
 Worker は TaskQueue から Task である Context を取得し、Task の Code Gear を実行し、Output Data Gear の書き出しを行っている。
@@ -64,6 +62,8 @@
 Context は、ソースコード \ref{enumCodeh} のように Code Gear の番号を持っており。
 初期化の際に Code Gear のアドレスと対応付けている。（ソースコード \ref{initContext}）

+\newpage
+
 \begin{lstlisting}[frame=lrbt,label=enumCodeh,caption={\footnotesize enum で定義された Code Gear の番号}]
 enum Code {
     C_popSingleLinkedStack,
--- a/paper/generate_code.tex	Thu Feb 07 17:11:07 2019 +0900
+++ b/paper/generate_code.tex	Fri Feb 08 05:05:15 2019 +0900
@@ -1,4 +1,4 @@
-\chapter{コードの自動生成}
+\chapter{メタレベルのコードの自動生成}

 stub Code Gear などの Meta Code Gear は通常ユーザーレベルからは見ることのできない Meta Data Gear である Context を扱うため、ユーザー自身が記述することは望ましくない。
 stub Code Gear は Code Gear 毎に記述する必要があるためユーザーの記述量が多くなる。
@@ -8,6 +8,9 @@
 また、このスクリプトによって Context の参照をユーザーレベルから隠すことができ、
 ユーザーレベルの Code Gear もシンプルになった。

+これらの Meta Code Gear は本来は OS が動的に生成するべきであるが、
+現在はコンパイル時に perl スクリプトによって静的に生成を行うことで実現している。
+
 \section{Meta Code Gear の生成}

 stub Code Gear は Code Gear 間の継続に挟まれる Meta Code Gear である。
@@ -18,27 +21,24 @@
 これにより Code Gear の記述量を約半分にすることができる。


-ソースコード \ref{Gears_code} は ユーザーレベルの Code Gear である。
+ソースコード \ref{StackPop} は ユーザーレベルの Code Gear である。
 この Code Gear を generate stub によって変換、
 stub Code Gear の生成を行なったコードがソースコード \ref{MetaCodeGear} である。

-生成された stub  Code Gear は、
-継続先の Code Gear が引数で指定した Input Data Gear、Output Data Gear を Context から参照している。
-Gearef は Context から Data Gear を参照するためのマクロである。
-ソースコード\ref{noref} はマクロを用いなかった場合の pop stack の stub Code Gear である。
-Context には Allocation 等で生成した Data Gear へのポインタが格納されている。
-Code Gear が Context にアクセスする際、
-ポインタを使用してデータを取り出すため煩雑なコードとなる。
-そこで Code Gear がデータを参照するための Gearef というマクロを定義した。
-Gearef は Context から Interface の引数格納用の Data Gear を取り出す。
-Gearef に Context と Interface の型を渡すことでデータの参照が行える。
+\begin{lstlisting}[frame=lrbt,label=StackPop,caption={\footnotesize 変換前の Stack pop}]
+__code popSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) {
+    if (stack->top) {
+        data = stack->top->data;
+        stack->top = stack->top->next;
+    } else {
+        data = NULL;
+    }
+    goto next(data, ...);
+}

-GearImpl マクロは Interface の型に包まれた Data Gear から
-実装の Data Gear を取り出すためのマクロである。
-実装の Data Gear を取り出す際も、ポインタでの記述が複雑になってしまうため 同様に GearImpl を定義した。
-GearImpl は Context と Interface の型、実装の Data Gear 名を指定することで参照する。
+\end{lstlisting}

-\begin{lstlisting}[frame=lrbt,label=MetaCodeGear,caption={\footnotesize Stack pop の変換}]
+\begin{lstlisting}[frame=lrbt,label=MetaCodeGear,caption={\footnotesize 変換後の Stack pop}]

 __code popSingleLinkedStack_stub(struct Context* context) {
         SingleLinkedStack* stack = (SingleLinkedStack*)GearImpl(context, Stack, stack);
@@ -58,12 +58,26 @@
         *O_data = data;
     goto meta(context, next);
 }
+\end{lstlisting}

-__code meta(struct Context* context, enum Code next) {
-    goto (context->code[next])(context);
-}

-\end{lstlisting}
+生成された stub  Code Gear は、
+継続先の Code Gear が引数で指定した Input Data Gear、Output Data Gear を Context から参照している。
+Gearef は Context から Data Gear を参照するためのマクロである。
+ソースコード\ref{noref} はマクロを用いなかった場合の pop stack の stub Code Gear である。
+Context には Allocation 等で生成した Data Gear へのポインタが格納されている。
+Code Gear が Context にアクセスする際、
+ポインタを使用してデータを取り出すため煩雑なコードとなる。
+そこで Code Gear がデータを参照するための Gearef というマクロを定義した。
+Gearef は Context から Interface の引数格納用の Data Gear を取り出す。
+Gearef に Context と Interface の型を渡すことでデータの参照が行える。
+
+GearImpl マクロは Interface の型に包まれた Data Gear から
+実装の Data Gear を取り出すためのマクロである。
+実装の Data Gear を取り出す際も、ポインタでの記述が複雑になってしまうため 同様に GearImpl を定義した。
+GearImpl は Context と Interface の型、実装の Data Gear 名を指定することで参照する。
+
+% 変換前のコードも入れる

 \begin{lstlisting}[frame=lrbt,label=noref,caption={マクロを用いない stub Code Gear}]
 __code popSingleLinkedStack_stub(struct Context* context) {
@@ -110,12 +124,74 @@
  \label{fig:gc}
 \end{figure}

-generate\_context は Context の定義が記述されている context.h を読み、宣言されている Data Gear を取得する。
-Code Gear の取得は指定された generate\_stub で生成されたコードから \_\_code 型を見て行う。
+generate\_context は Context の定義が記述されている context.h を読み、Data Gear を取得する。
+Code Gear の取得は generate\_stub で生成されたコードを読み、ソースコード内の \_\_code 型を見て行う。
 取得した Code Gear、Data Gear の enum の定義は enumCode.h、enumData.h に生成される。

-Code/Data Gear の名前とポインタの対応は generate\_context によって生成される enum Code、enum Data を指定することで接続を行う。
-また、generate context は取得した Code/Data Gear から initContext の生成も行う。
+Code Gear、Data Gear の名前とポインタの対応は generate\_context によって生成される enum Code、enum Data を指定することで接続を行う。
+generate context は、この Code Gear、Data Gear の初期化のコードの initContext の生成も行う。
+(ソースコード \ref{initContext})
+
+また、Gears OS のメタ計算に用いる \_\_code meta や main関数から継続する start\_code、
+終了処理を行う exit\_code も生成される。
+
+これらはまとめて target-context.c として生成される。
+
+\begin{lstlisting}[frame=lrbt,label=init_context,caption={\footnotesize 生成された target-context.c}]
+
+#include <stdlib.h>
+
+#include "../context.h"
+
+void initContext(struct Context* context) {
+    context->heapLimit = sizeof(union Data)*ALLOCATE_SIZE;
+    context->code = (__code(**) (struct Context*)) NEWN(ALLOCATE_SIZE, void*);
+    context->data = NEWN(ALLOCATE_SIZE, union Data*);
+    context->heapStart = NEWN(context->heapLimit, char);
+    context->heap = context->heapStart;
+
+    context->code[C_clearSingleLinkedStack]    = clearSingleLinkedStack_stub;
+    context->code[C_exit_code]    = exit_code_stub;
+    context->code[C_getSingleLinkedStack]    = getSingleLinkedStack_stub;
+    context->code[C_isEmptySingleLinkedStack]    = isEmptySingleLinkedStack_stub;
+    context->code[C_popSingleLinkedStack]    = popSingleLinkedStack_stub;
+    context->code[C_pushSingleLinkedStack]    = pushSingleLinkedStack_stub;
+    context->code[C_stack_test1]    = stack_test1_stub;
+    context->code[C_stack_test2]    = stack_test2_stub;
+    context->code[C_stack_test3]    = stack_test3_stub;
+    context->code[C_stack_test4]    = stack_test4_stub;
+    context->code[C_start_code]    = start_code_stub;
+
+#include "dataGearInit.c"
+
+}
+
+__code meta(struct Context* context, enum Code next) {
+    // printf("meta %d\n",next);
+    goto (context->code[next])(context);
+}
+
+__code start_code(struct Context* context) {
+    goto meta(context, context->next);
+}
+
+__code start_code_stub(struct Context* context) {
+    goto start_code(context);
+}
+
+__code exit_code(struct Context* context) {
+    free(context->code);
+    free(context->data);
+    free(context->heapStart);
+    goto exit(0);
+}
+
+__code exit_code_stub(struct Context* context) {
+    goto exit_code(context);
+}
+
+// end context_c
+\end{lstlisting}

 Context には Allocation 等で生成した Data Gear へのポインタが格納されている。
 Code Gear は Context を通して Data Gear へアクセスする。
--- a/paper/interface.tex	Thu Feb 07 17:11:07 2019 +0900
+++ b/paper/interface.tex	Fri Feb 08 05:05:15 2019 +0900
@@ -1,5 +1,6 @@
 \chapter{Interface}
 Interface は Gears OS のモジュール化の仕組みである。
+%java のインターフェースの話を入れる　モジュール化
 Interface は呼び出しの引数になる Data Gear の集合であり、そこで呼び出される Code Gear のエントリである。
 呼び出される Code Gear の引数となる Data Gear はここで全て定義される。
 Interface を定義することで複数の実装を持つことができる。
@@ -75,7 +76,7 @@
 Interface を記述することでデータ構造の API と Data Gear を結びつけることが出来る。
 これによりノーマルレベルとメタレベルの分離が可能となった。

-\section{Interface の実装}
+\section{Interface の実装の記述}
 ソースコード\ref{implement}は Stack の実装の例である。
 createImpl は実装の初期化を行う関数である。
 Interface の実装を呼び出す際、この関数を呼び出すことで ソースコード\ref{pushStack} 4 行目のように実装の操作を呼び出せるようになる。
--- a/paper/introduction.tex	Thu Feb 07 17:11:07 2019 +0900
+++ b/paper/introduction.tex	Fri Feb 08 05:05:15 2019 +0900
@@ -1,4 +1,4 @@
-\chapter{オペレーティングシステム}
+\chapter{OS の拡張性と信頼性の両立}

 コンピュータには CPU、ディスプレイ、キーボードやマウス、ハードディスクなど様々な機器が接続されている。
 プログラムの処理を行うとき、これらの様々なデバイスのアクセスや資源管理は複雑で容易ではない。
@@ -7,23 +7,21 @@

 ユーザーは OS のおかげで異なるハードウェアの違いを意識することなくプログラミングをすることができる。
 例えば同じプログラムで、異なる入力デバイスによる操作や、ディスプレイでの表示などは、
-デバイスへのアクセスなどの複雑な処理を OS が隠すことによってユーザーが意識せずにプログラミングを行える。
-%被ってる
+それぞれデバイスへのアクセスなどの複雑な処理を OS が隠すことによって可能となっている。

 CPU、メモリ、ディスク、などの本来ユーザーが意識しなければならない資源も、OS が資源管理を行うことで意識することなくプログ
 ラミングすることができる。

-1950年代におけるコンピューターがプログラムを実行する際には専門のオペレータが存在し、オペレーターがジョブの管理、コンパイ
-ラの選択などを行なっていた。
+1950年代におけるコンピューターがプログラムを実行する際には専門のオペレータが存在し、
+オペレーターがジョブの管理、コンパイラの選択などを行なっていた。
 しかし後に、ジョブの自動実行、やコンパイラのロードを行うプログラムができた。これが OS の祖先である。
 コンピュータには科学技術用のコンピューターと商用のコンピューターが開発されていたが、後に汎用コンピューターである System/360 が開発される。
-System/360 の OS/360 は強力なソフトウェア互換を持っていた。
+その OS/360 は強力なソフトウェア互換を持っていた。
 ソフトウェア互換により全てのソフトウェアが全てのマシンで動作するようになった。
-この頃の OS には、スプーリングやタイムシェアリングといった機能も導入されるようになった。
-その後、UNIX が開発され後に様々なバージョンが開発され、System V、BSD といった派生 OS なども開発され、現在に至る。
+その後、OS は、スプーリングやタイムシェアリングといった機能も導入されるようになった。
+1970年代には UNIX が開発され、後に様々なバージョンが開発され、System V、BSD といった派生 OS なども開発され、現在に至る。

-\chapter{OS の拡張性と信頼性の両立}
-さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。
+OS はさまざまなコンピュータの信頼性の基本である。
 OS の信頼性を保証する事自体が難しいが、
 時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。
 OS は非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分であり、
@@ -34,7 +32,7 @@
 (図\ref{fig:verification})
 \begin{figure}[ht]
  \begin{center}
-  \includegraphics[width=70mm]{./fig/verification.pdf}
+  \includegraphics[width=100mm]{./fig/verification.pdf}
  \end{center}
  \caption{証明とモデル検査によるOSの検証}
  \label{fig:verification}
@@ -80,9 +78,12 @@
 また、本研究では Gears の記述をモジュール化するために Interface を導入した。
 さらに並列処理の記述用にpar goto 構文を導入する。
 これらの機能は Agda 上で継続を用いた関数型プログラムに対応するようになっている。
+これにより Code Gear、Data Gear の Agda による証明が可能となり、
+モデル検査を入れられるように Gears OS の構築を行った。
+
 \begin{figure}[ht]
  \begin{center}
-  \includegraphics[width=100mm]{./fig/MetaGear.pdf}
+  \includegraphics[width=130mm]{./fig/MetaGear.pdf}
  \end{center}
  \caption{Gearsのメタ計算}
  \label{fig:MetaGear}
Binary file paper/master_paper.pdf has changed
--- a/paper/meta_computation.tex	Thu Feb 07 17:11:07 2019 +0900
+++ b/paper/meta_computation.tex	Fri Feb 08 05:05:15 2019 +0900
@@ -1,5 +1,4 @@
-\c:hapter{Gears におけるメタ計算}
-%
+\chapter{Gears におけるメタ計算}
 プログラムを記述する際、ノーマルレベルの処理の他に、メモリ管理、スレッド管理、CPU や GPU の資源管理等、記述しなければならない処理が存在する。
 これらの計算をメタ計算と呼ぶ。

@@ -23,6 +22,17 @@
 Gears OS は処理やデータの構造が Code Gear、Data Gear に閉じているため、
 これにより実行時間、メモリ使用量などを予測可能なものにすることが可能になる。

+Gears OS には Context と呼ばれる全ての Code Gear、Data Gear のリストを持つ Meta Data Gear が存在する。
+Gears OS ではこの Context を常に持ち歩いているが、これはノーマルレベルでは見えることはない。
+
+ノーマルレベルの処理とメタレベルを含む処理は同じ動作を行う。
+しかしメタレベルの計算を含むプログラムとノーマルレベルでは、Data Gear の扱いなどでギャップがある。
+ノーマルレベルでは Code Gear は Data Gear を引数の集合として引き渡しているが、
+メタレベルでは Context に格納されており、ここを参照することで Data Gear を扱っている。
+
+このギャップを解消するためにメタレベルでは stub Code Gear と呼ばれる Context から Data Gear の参照を行う
+Meta Code Gear が Code Gear 継続前に揷入されこれを解決する。
+
 \section{Continuation based C}
 CbC は処理を Code Gear とした単位を用いて記述するプログラミング言語である。
 Code Gear 間では軽量継続 (goto文) による遷移を行うので、継続前の Code Gear に戻ることはなく、
@@ -47,6 +57,8 @@
 関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。
 ソースコード \ref{code_simple} はCbC における Code Gear の一例である。

+\newpage
+
 \begin{lstlisting}[frame=lrbt,label=code_simple,caption={\footnotesize code segment の軽量継続}]
 __code cs0(int a, int b){
   goto cs1(a+b);
@@ -141,6 +153,8 @@
  \label{fig:meta_Code_Gear}
 \end{figure}

+\subsection{Context と stub Code Gear}
+
 Gears OS では Context と呼ばれる、使用されるすべての Code Gear、Data Gear を持つ Meta Data Gear を持っている。
 Gears OS は必要な Code Gear、Data Gear を参照したい場合、この Context を通す必要がある。
 しかし Context を通常の計算から直接扱うのはセキュリティ上好ましくない。
@@ -185,6 +199,8 @@
 Interface の操作に対応する Code Gear の引数は Interface に定義されている Data Gear を通して指定される。
 一つの実行スレッド内で使われる Interface の Code Gear と Data Gear は Context に格納される。

+%Context の概念のセクション
+
 Code Gear の継続は関数型プログラミングからみると継続先の Context を含む Closure となっている。
 これを記述するために継続に不定長引数を追加する構文をスクプリトの変換機能として用意した。
 メタ計算側ではこれらの Context を常に持ち歩いているので goto 文で引数を用いることはなく、
@@ -192,9 +208,15 @@

 これにより Interface 間の呼び出しを C++ のメソッド呼び出しのように記述することができる。
 Interface の実装は、Context 内に格納されているので、オブジェクトごとに実装を変える多様性を実現できている。
+%入れるのであれば
+%code gear の並列実行
+%ノーマルレベルでは複数の goto を持つ
+
+\subsection{Meta Gear を用いたメタレベルの処理}

 Context を複製して複数の CPU に割り当てることにより並列実行を可能になる。
 これによりメタ計算として並列処理を記述したことになる。
+
 Gears のスレッド生成は Agda の関数型プログラミングに対応して行われるのが望ましい。
 そこで、par goto 構文を導入し、Agda の継続呼び出しに対応させることにした。
 par goto では Context の複製、入力の同期、タスクスケジューラーへの Context の登録などが行われる。
--- a/paper/xv6.tex	Thu Feb 07 17:11:07 2019 +0900
+++ b/paper/xv6.tex	Fri Feb 08 05:05:15 2019 +0900
@@ -8,6 +8,8 @@
 Xv6 はプロセス、仮想メモリ、カーネルとユーザの分離、割り込み、ファイルシステムなどの基本的な Unix の構造を持つにも関わらず、
 シンプルで学習しやすい。

+\section{Raspberry Pi}
+
 \section{xv6 の構成要素}
 xv6 はカーネルと呼ばれる形式をとっている。
 カーネルは OS にとって中核となるプログラムである。