--- a/Paper/sigos.tex	Fri Apr 13 19:59:33 2018 +0900
+++ b/Paper/sigos.tex	Sun Apr 22 17:29:14 2018 +0900
@@ -121,11 +121,15 @@
 この二つのレベルを同じ言語で記述できるようにして、ノーマルレベルの計算の信頼性をメタレベルから保証できるようにしたい。
 ノーマルレベルでの正当性を保証しつつ、新しく付け加えられたデバイスやプログラムを含む正当性を検証したい。
 
-本論文では、ノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C(以下CbC)\cite{cbc}を用いる。
+ノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C(以下CbC)\cite{cbc}を用いる。
 CbC は関数呼出時の暗黙の環境(Environment)を使わずに、コードの単位を行き来できる引数付き goto 文(parametarized goto)を持つ C と互換性のある言語である。
 これを用いて、Code Gear と Data Gear、さらにそのメタ構造を導入する。
 これらを用いて、検証された Gears OS を構築したい。
 図\ref{fig:MetaGear}。
+検証には定理証明支援系である Agda を用いる。
+Gears の記述をモジュール化するために Interface を導入した。
+さらに並列処理の記述用にpar goto 構文を導入する。
+これらの機能は Agda 上で継続を用いた関数型プログラムに対応するようになっている。
 \begin{figure}[ht]
  \begin{center}
   \includegraphics[width=70mm]{./pic/MetaGear.pdf}
@@ -134,79 +138,56 @@
  \label{fig:MetaGear}
 \end{figure}
 
-本論文では、Gears OS の要素である Code Gear、Data Gear、そして、Meta Code Gear 、Meta Data Gear の構成を示す。
-これらは、CbC に変換されて実行される。
-Gears OS は、Task Scheduler を CPU や GPU 毎に持ち、一つの Task に対応する Context という Meta Data Gear を使用しながら計算を実行する。
-
-Meta Gear を入れかえることにより、ノーマルレベルの Gear をモデル検査することができるようにしたい。
-ノーマルレベルでの Code Gear と Data Gear は継続を基本とした関数型プログラミング的な記述に対応する。
-この記述を定理証明支援系である Agda を用いて直接に証明できるようにしたい。
-
-従来の研究でメタ計算を用いる場合は、関数型言語では Monad を用いる\cite{Moggi:1989:CLM:77350.77353}。
-これは Hakell では実行時の環境を記述する構文として使われている。
-OS の研究では、メタ計算の記述に型つきアセンブラ(Typed Assembler)を用いることがある\cite{Yang:2010:SLI:1806596.1806610}。
-Python や Haskell による記述をノーマルレベルとして
-採用した OS の検証の研究もある\cite{Klein:2009:SFV:1629575.1629596,Chen:2015:UCH:2815400.2815402}。
-SMIT などのモデル検査を OS の検証に用いた例もある\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}。
+本論文では Interface と par goto の実装の詳細を記述し評価を行った。
+マルチ CPU と GPU 上での par goto 文の実行を確認した。
+%Go言語に比べて並列構文 par goto が遅いことがわかった。
 
-本研究で用いる Meta Gear は制限された Monad に相当し、型つきアセンブラよりは大きな表現単位を提供する。
-Haskell などの関数型プログラミング言語では実行環境が複雑であり、実行時の資源使用を明確にすることができない。
-CbC はスタック上に隠された環境を持たないので、メタレベルで使用する資源を明確にできるという利点がある。
-ただし、Gear のプログラミングスタイルは、従来の関数呼出を中心としたものとはかなり異なる。
-本研究では、Gears の記述をモジュール化するために Interface を導入した。
-これにより、見通しの良いプログラミングが可能になった。
-
-\section{メタ計算の重要性}
-従来の OS では、メタ計算はシステムコールやライブラリーコールの単位で行われる。
-実行時にメタ計算の変更を行う場合には、OS 内部のパラメータの変更を使用し、
-実行されるユーザープログラム自体への変更は限定的である。
-しかし、メタ計算は性能測定あるいはプログラム検証、さらに並列分散計算のチューニングなど細かい処理が必要で
-実際のシステムコール単位では不十分である。
-例えば、モデル検査ではアセンブラあるいはバイトコード、インタプリタレベルでのメタ計算が必要になる。
-しかし、バイトコードレベルでは粒度が細かすぎて扱いが困難になっている。
-具体的にはメタ計算の実行時間が大きくなってしまう。
-
-メタ計算を通常の計算から切り離して記述するためには処理を細かく分割する必要がある。しかし、関数やクラスなどの単位は容易に分割できない。
-そこで当研究室ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を提案している。
-これによりシステムコードよりも細かくバイトコードよりも大きなメタ計算の単位を提供できる。
-
-Code Gear は処理の単位である。
-関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。
+\section{Gears におけるメタ計算}
+Gears OS ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を用いる。
 Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、これらを用いてメタ計算を実現する。
 
-CbC はこの Code Gear 単位を用いたプログラミング言語として開発している。
-
-CbC は軽量継続による遷移を行うので、継続前の Code Gear に戻ることはなく、状態遷移ベースのプログラミングに適している。
-
-CbC での記述はメタ計算を含まないノーマルレベルでの記述と、Meta Code Gear、Meta Data Gear の記述を含むメタレベルの記述の2種類がある。
-メタレベルでもさらに、メタ計算を用いることが可能になっている。
-この2つのレベルはプログラミング言語レベルでの変換として実現される。
-CbC は LLVM\cite{llvm} 上で実装されており、メタレベルでの変換系は本論文では、Perl による変換スクリプトにより実装されている。
+CbC は軽量継続 (goto文) による遷移を行うので、継続前の Code Gear に戻ることはなく、状態遷移ベースのプログラミングに適している。
+CbC は LLVM\cite{llvm} と GCC\cite{gcc} 上で実装されている。
+メタレベルの記述は Perl スクリプトによって生成される stub と goto meta によって Code Gear で記述される。
 
 Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される。
 Interface は使用される Data Gear の定義と、それに対する操作を行う Code Gear の集合である。
-Interface は複数の実装を持つことができ、Meta Data Gear によって定義される。
-Interface の操作に対応する Code Gear の引数は Interface に定義されている Data Gear を通して行われる。
+Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。
+Interface の操作に対応する Code Gear の引数は Interface に定義されている Data Gear を通して指定される。
+一つの実行スレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。
+この Meta Data Gear を Context という。
+ノーマルレベルでは Context を直接見ることはできない。
 
-従来の関数呼び出しでは引数をスタック上に構成し、関数の実装アドレスを Call する。
-Gears OS では引数は Context 上に用意された Interface の Data Gear に格納され、
-操作に対応する Code Gear に goto する。
-Context とは使用される Code Gear と Data Gear を全て格納している Meta Data Gear である。
-これは従来のスレッド構造体に対応する。
-つまり Gears OS では従来はコンパイラが定義する ABI(Application Binary Interface)
-を Meta Data Gear として CbC で表現し、メタ計算として操作することができる。
+Code Gear の継続は関数型プログラミングからみると継続先の Context を含む Closure となっている。
+これを記述するために継続に不定長引数を追加する構文をスクプリトの変換機能として用意した図。\ref{fig:varargnext}
+メタ計算側ではこれらの Context を常に持ち歩いているので goto 文で引数を用いることはなく、
+行き先は Code Gear の番号のみで指定される。
+\begin{figure}[ht]
+ \begin{center}
+%  \includegraphics[width=70mm]{./pic/MetaGear.pdf}
+ \end{center}
+ \caption{不定長引数を持つ継続}
+ \label{fig:varargnext}
+\end{figure}
 
-ノーマルレベルでは Context を直接見ることはできず、引数は Code Gear の引数を明示する必要がある。
-この時に呼び出し側の引数を不定長引数として追加する構文を CbC に追加した。
-これにより Interface 間の呼び出しを簡潔に記述することが出来るようになった。
-メタレベルでは Code Gear の引数は単一または複数の Data Gear として見ることができる。
-これは Context を直接操作することができることを意味する。
-この部分はノーマルレベルの Code Gear を呼び出す stub として生成される。
-ノーマルレベルでの goto 文はメタ計算への goto で置き換えられる。
+
+これにより Interface 間の呼び出しを C++ のメソッド呼び出しのように記述することができる。
+Interface の実装は、Context 内に格納されているので、オブジェクトごとに実装を変える多様性を実現できている。
+呼び出された Code Gear は必要な引数を Context から取り出す必要がある。
+これは スクリプトで生成された stub Meta Code Gear で行われる。
 Gears OS でのメタ計算は stub と goto のメタ計算の2箇所で実現される。
 
-メタ計算の例としては並列処理があり、Context を切り替えることによって複数のスレッドを実現している。
-Context を複数の CPU に割り当てることにより並列実行を可能にしている。
+Context を複製して複数の CPU に割り当てることにより並列実行を可能になる。
+これによりメタ計算として並列処理を記述したことになる。
+Gears のスレッド生成は Agda の関数型プログラミングに対応して行われるのが望ましい。
+そこで、par goto 構文を導入し、Agda の継続呼び出しに対応させることにした。
+par goto では Context の複製、入力の同期、タスクスケジューラーへの Context の登録などが行われる。
+par goto 文の継続として、スレッドの join に相当する \_\_exit を用意した。
+\_\_exit により par goto で分岐した Code Gear の出力を元のスレッドで受け取ることができる。 
+
+関数型プログラムではメモリ管理は GC などを通して暗黙に行われる。
+Gears OS ではメモリ管理は stub などのメタ計算部分で処理される。
+例えば、寿命の短いスレッドでは使い捨ての線形アロケーションを用いる。 
 
 \section{Continuation based C (CbC)}
 CbC は Code Gear という処理の単位を用いて記述するプログラミング言語である。