--- a/paper/introduction.tex	Tue Feb 06 06:52:42 2018 +0900
+++ b/paper/introduction.tex	Tue Feb 06 16:10:40 2018 +0900
@@ -1,12 +1,37 @@
 \chapter{メタ計算を使った並列処理}
-現代の OS では拡張性と信頼性を両立させることが要求されている。
-時代と主に進歩するハードウェア、サービスに対して OS 自体が拡張される必要がある。
-しかし、OSには非決定的な実行を持っており、その信頼性を保証するには従来のテストとデバッグでは不十分であり、テスト仕切れない部分が残ってしまう。
-これに対処するために証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
+並列処理は現代主流のマルチコアCPU の性能を発揮するには重要なものになっている。
+しかし、並列処理のプログラミングはスレッド間の共通資源の競合など非決定的な実行を持っており、その信頼性を保証するには従来のテストやデバッグでは不十分であり、テストしきれない部分が残ってしまう。
+
+また、マルチコア CPU 以外にも  GPU や CPU と GPU を複合したヘテロジニアスなプロセッサも並列処理をする上で無視できない。
+これらのプロセッサで性能を出すためにはアーキテクチャに合わせた並列プログラミングが必要になる。
+並列プログラミングフレームワークでは様々なプロセッサを抽象化し、CPU と同等に扱えるようにする柔軟性が求められる。
+
+本研究室では通常の計算をノーマルレベルとし、並列処理の信頼性をノーマルレベルの計算に対して保証し、拡張性をノーマルレベルとは別の階層のメタレベルの計算で実現することを目標に Gears OS を設計、開発中である。
+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 の継続の間に実行される。
 
-% これはryokka 向き
-証明やモデル検査を用いて OS の検証する方法は様々なものが検討されている。
-型付きアセンブラ\cite{Yang:2010:SLI:1806596.1806610}
-従来の研究ではPython\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596}による記述した OS を検証する研究も存在する。
-また SPIN などのモデル検査を OS の検証に用いた例もである。
-本研究室では信頼性をノーマルレベルの掲載に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を開発している。
+Gears OS でのプロセス、 スレッドは Context というすべての Code Gear と Data Gear の集合を持っている Meta Data Gear が担う。
+つまり、 並列実行する際は新しく Context を生成し、 それを CPU、 GPU に割り振る事によって実現される。
+生成された Context には実行される Code Gear と対応する Input/Output Data Gear が登録され、割り振られた先で Context に設定された Code Gear を実行する。
+このContext を用いた並列処理は新規に実行環境を作り、引数を設定するなどの煩雑なメタレベルの処理であり、ノーマルレベルでは Go 言語の goroutine のような簡潔な並列構文があることが望ましい。
+
+本研究では Gears OS の並列実行機構、 並列構文を実装し、 例題を用いて Gears OS の並列処理の評価を行う。
+
+% これはryokka 向きかなぁ
+
+%現代の OS では拡張性と信頼性を両立させることが要求されている。
+%時代と主に進歩するハードウェア、サービスに対して OS 自体が拡張される必要がある。
+%しかし、OSには非決定的な実行を持っており、その信頼性を保証するには従来のテストとデバッグでは不十分であり、テスト仕切れない部分が残ってしまう。
+%これに対処するために証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
+% 証明やモデル検査を用いて OS の検証する方法は様々なものが検討されている。
+% 型付きアセンブラ\cite{Yang:2010:SLI:1806596.1806610}
+% 従来の研究ではPython\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596}による記述した OS を検証する研究も存在する。
+% また SPIN などのモデル検査を OS の検証に用いた例もである。
+% 本研究室では信頼性をノーマルレベルの掲載に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を開発している。

Binary file paper/master_paper.pdf has changed