--- a/paper/conclusion.tex	Tue Feb 06 18:09:49 2018 +0900
+++ b/paper/conclusion.tex	Wed Feb 07 17:46:49 2018 +0900
@@ -22,7 +22,7 @@
 今後の課題として、Gears OS の並列処理の信頼性の保証、 チューニングを行う。
 
 Gears OS では証明とモデル検査をメタレベルで実行することで信頼性を保証する。
-証明は CbC のプログラムを証明支援系の Agda\cite{agda} に対応させて証明を行う。
+証明は CbC のプログラムを証明支援系の Agda に対応させて証明を行う。
 現在は Gears OS の Interface 部分の動作の証明を行っており、Stack や Tree の動作の証明を行っている。
 Gears OS の並列処理の信頼性を証明するには Synchronized Queue の証明を行う必要がある。
 

--- a/paper/gearsOS.tex	Tue Feb 06 18:09:49 2018 +0900
+++ b/paper/gearsOS.tex	Wed Feb 07 17:46:49 2018 +0900
@@ -1,5 +1,5 @@
 \chapter{Gears OS の概念}
-Gears OS\cite{kkb-master} は信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に開発している OSである。
+Gears OS は信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に開発している OSである。
 
 Gears OS は処理の単位を Code Gear、データの単位を Data Gear と呼ばれる単位でプログラムを構成する。
 信頼性や拡張性はメタ計算として、通常の計算とは区別して記述する。

--- a/paper/interface.tex	Tue Feb 06 18:09:49 2018 +0900
+++ b/paper/interface.tex	Wed Feb 07 17:46:49 2018 +0900
@@ -21,7 +21,7 @@
 Gears OS は stub Code Gear という Meta Code Gear で Context という全ての Code Gear と Data Gear を持った Meta Data Gear から値を取りだし、ノーマルレベルの Code Gear に値を渡す。
 しかし、Gears OS を実際に実装するにつれて、メタレベルからノーマルレベルへの継続の記述が煩雑になることがわかり、Code Gear と Data Gear のモジュール化が必要になった。
 
-本章では Gears OS のモジュール化の仕組みである Interface について説明する。
+本章では Gears OS のモジュール化の仕組みである Interface\cite{mitsuki-prosym} について説明する。
 
 \section{Context を経由しての継続の問題点}
 Gears OS は Code Gear で必要な Input Data Gear を Context から番号を指定して取り出すことで処理を実行する。

--- a/paper/introduction.tex	Tue Feb 06 18:09:49 2018 +0900
+++ b/paper/introduction.tex	Wed Feb 07 17:46:49 2018 +0900
@@ -6,23 +6,32 @@
 これらのプロセッサで性能を出すためにはアーキテクチャに合わせた並列プログラミングが必要になる。
 並列プログラミングフレームワークでは様々なプロセッサを抽象化し、CPU と同等に扱えるようにする柔軟性が求められる。
 
-本研究室では通常の計算をノーマルレベルとし、並列処理の信頼性をノーマルレベルの計算に対して保証し、拡張性をノーマルレベルとは別の階層のメタレベルの計算で実現することを目標に Gears OS を設計、開発中である。
+本研究室では通常の計算をノーマルレベルとし、並列処理の信頼性をノーマルレベルの計算に対して保証し、拡張性をノーマルレベルとは別の階層のメタレベルの計算で実現することを目標に Gears OS\cite{kkb-master}を設計、開発中である。
 Gears OS では処理を Code Gear、 データを Data Gear という単位を用いてプログラムを記述する。
 Code Gear には実行するときに必要な Input Data Gear、出力するための Output Data Gear がある。
-この Code Gear と Data Gear の組で並列実行の Task を表現し、 Input/Output Data Gear によって依存関係が決定し、それにそって並列処理を行う。
 
 Gears OS のプログラムの信頼性の確保はモデル検査、検証を使用して行う。
 この信頼性のための計算はメタ計算として記述される。
 このメタ計算は信頼性の他に CPU、 GPU などのアーキテクチャに沿った実行環境の切り替え、データの拡張等の拡張性を提供する。
 メタ計算の処理は Meta Code Gear、 Meta Data Gear で表現する。
-Meta Code Gear は 通常の Code Gear の継続の間に実行される。
+Meta Code Gear は 通常の Code Gear 間に実行される。
 
-Gears OS でのプロセス、 スレッドは Context というすべての Code Gear と Data Gear の集合を持っている Meta Data Gear が担う。
+従来の研究では OS の実装言語として Python\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596} をノーマルレベルとして採用し、メタレベルで検証を行う研究や、メタ計算の実装を型付きアセンブラ(Typed Assembler)\cite{Yang:2010:SLI:1806596.1806610} を用いる例もある。
+Gears OS は ノーマルレベルとメタレベルを共通して表現出来る Continuation Based C(CbC) で実装を行い、 証明支援系 Agda\cite{agda} を用いて証明を行う。
+CbC は Code Gear の単位でプログラムを記述し、軽量継続を用いてコード間を移動する。
+軽量継続は関数呼び出しとは異なり、呼び出し元に戻らないため、呼び出し元の環境を覚えずに行き先のみを指定する。
+この CbC は C と互換性のある言語で、型付きアセンブラに比べると大きな表現力を提供する。また Haskell などに比べて関数呼び出しではなく軽量継続を採用しているため、スタック上に隠された環境を持たないため、メタレベルで使用する資源を明確にできる利点がある。
+
+Code Gear 間の継続は次の Code Gear の番号と Context という全ての Code Gear と Data Gear を参照できる Meta Data Gear で行われる。
+Context からノーマルレベルのCode Gear へ接続する際は stub Code Gear という Meta Code Gear を用いる。
+この stub Code Gear はメタレベルの計算であるため、継続先の Code Gear から自動的に生成されるのが望ましい。生成に必要な情報は Code Gear と Data Gear の集まりから得る。 この集まりを Interface として定義している。
+
+Gears OS でのプロセス、スレッドは Context が担う。
 つまり、 並列実行する際は新しく Context を生成し、 それを CPU、 GPU に割り振る事によって実現される。
 生成された Context には実行される Code Gear と対応する Input/Output Data Gear が登録され、割り振られた先で Context に設定された Code Gear を実行する。
 このContext を用いた並列処理は新規に実行環境を作り、引数を設定するなどの煩雑なメタレベルの処理であり、ノーマルレベルでは Go 言語の goroutine のような簡潔な並列構文があることが望ましい。
 
-本研究では Gears OS のマルチコアCPU と CUDA による GPUでの実行機構、 並列構文を実装し、 例題を用いて Gears OS の並列処理の評価を行う。
+本研究では Gears OS の基本設計、マルチコアCPU と CUDA による GPUでの実行機構、 並列構文を実装し、 例題を用いて Gears OS の並列処理の評価を行う。
 
 % これはryokka 向きかなぁ
 

Binary file paper/master_paper.pdf has changed

--- a/paper/parallelism_gears.tex	Tue Feb 06 18:09:49 2018 +0900
+++ b/paper/parallelism_gears.tex	Wed Feb 07 17:46:49 2018 +0900
@@ -11,7 +11,7 @@
 本章では、Gears OS の並列処理の構成、機能について説明する。
 
 \section{Task}
-Gears OS では 並列実行する Task を Context で表現する。
+Gears OS では 並列実行する Task を Context で表現する\cite{ikkun-sigos}。
 Context には Task 用の情報として、実行される Code Gear、Input/Output Data Gear の格納場所、待っている Input Data Gear のカウンタ等を持っている。
 Task の Input Data Gear が揃っているかを TaskManager で判断し、 実行可能な Task を Worker に送信する。
 Worker は送信された Task が指定した Code Gear を実行し、Output Data Gear を書き出す。

--- a/paper/reference.bib	Tue Feb 06 18:09:49 2018 +0900
+++ b/paper/reference.bib	Wed Feb 07 17:46:49 2018 +0900
@@ -104,7 +104,7 @@
 }
 
 @article{atton-ipsj,
-author="比嘉, 健太 and 河野, 真治",
+author="比嘉 健太 and 河野 真治",
 title="Verification Method of Programs Using Continuation based C",
 journal="情報処理学会論文誌プログラミング（PRO）",
 ISSN="1882-7802",