Binary file Paper/main.pdf has changed

--- a/Paper/main.tex	Sat Dec 23 16:30:09 2017 +0900
+++ b/Paper/main.tex	Sat Dec 23 18:15:08 2017 +0900
@@ -67,10 +67,10 @@
 \maketitle
 
 % Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{OSの拡張性と信頼性の両立}
+\section{OS の拡張性と信頼性の両立}
 
-さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行うOSである。OSの信頼性を保証する事自体が難しいが、時代とともに進歩する
-ハードウェア、サービスに対応してOS自体が拡張される必要がある。OSは非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分
+さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩する。
+ハードウェア、サービスに対応して OS 自体が拡張される必要がある。OS は非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分
 であり、テストしきれない部分が残ってしまう。これに対処するためには、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法が
 ある。モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている
 図\ref{fig:verification}。
@@ -82,7 +82,7 @@
  \label{fig:verification}
 \end{figure}
 
-証明やモデル検査を用いてOSを検証する方法はさまざまなものが検討されている。検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しく
+証明やモデル検査を用いて OS を検証する方法はさまざまなものが検討されている。検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しく
 なることに検証をやり直す必要がある。つまり信頼性と拡張性を両立させることが重要である。
 
 コンピュータの計算はプログラミング言語で記述されるが、その言語の実行は操作的意味論の定義などで規定される。プログラミング言語で記述される部分を
@@ -91,32 +91,32 @@
 ノーマルレベルでの正当性を保証しつつ、新しく付け加えられたデバイスやプログラムを含む正当性を検証したい。
 
 本論文では、ノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C(以下CbC)\cite{cbc}を用いる。CbC は関数呼出時の暗黙の環境(Environment)
-を使わずに、コードの単位を行き来できる引数付きgoto文(parametarized goto)を持つCと互換性のある言語である。これを用いて、Code Gear と Data Gear、さらに
-そのMeta 構造を導入する。これらを用いて、検証されたGears OSを構築したい。
+を使わずに、コードの単位を行き来できる引数付き goto 文(parametarized goto)を持つ C と互換性のある言語である。これを用いて、Code Gear と Data Gear、さらに
+そのメタ構造を導入する。これらを用いて、検証された Gears OS を構築したい。
 図\ref{fig:MetaGear}。
 \begin{figure}[ht]
  \begin{center}
-  \includegraphics[width=70mm]{./pic/verification.pdf}
+  \includegraphics[width=70mm]{./pic/MetaGear.pdf}
  \end{center}
  \caption{Gearsのメタ計算}
  \label{fig:MetaGear}
 \end{figure}
 
-本論文では、Gears OSの要素である Code Gear、Data Gea、そして、Meta Code Gear 、Meta Data Gear の構成を示す。これらは、CbC に変換されて実行される。
-Gears OS は、Task Scheduler をCPUやGPU毎に持ち、一つのTaskに対応する Context というMeta Data Gear を使用しながら計算を実行する。
+本論文では、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を用いて直接に証明できるようにしたい。
+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}。
+従来の研究でメタ計算を用いる場合は、関数型言語では 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}。
 
-本研究で用いる Meta Gear は制限されたMonadに相当し、型つきアセンブラよりは大きな表現単位を提供する。
-Haskellなどの関数型プログラミング言語では実行環境が複雑であり、実行時の資源使用を明確にすることができない。CbC はスタック上に隠された
+本研究で用いる Meta Gear は制限された Monad に相当し、型つきアセンブラよりは大きな表現単位を提供する。
+Haskell などの関数型プログラミング言語では実行環境が複雑であり、実行時の資源使用を明確にすることができない。CbC はスタック上に隠された
 環境を持たないので、メタレベルで使用する資源を明確にできるという利点がある。ただし、Gear のプログラミングスタイルは、従来の関数呼出
-を中心としたものとはかなり異なる。本研究では、Gearsの記述をモジュールかするためにインターフェースを導入した。これにより、
+を中心としたものとはかなり異なる。本研究では、Gears の記述をモジュールかするためにインターフェースを導入した。これにより、
 見通しの良いプログラミングが可能になった。
 
 
@@ -143,7 +143,7 @@
 
 Continuation based C (CbC)\cite{cbc} はこの Code Gear 単位を用いたプログラミング言語として開発している。
 
-CbCは軽量継続による遷移を行うので、継続前の Code Gear に戻ることはなく、状態遷移ベースのプログラミングに適している。
+CbC は軽量継続による遷移を行うので、継続前の Code Gear に戻ることはなく、状態遷移ベースのプログラミングに適している。
 
 また、当研究室で開発している Gears OS\cite{gears} は Code Gear、 Data Gear の単位を用いて開発されており、CbC で記述されている。
 CbC での記述はメタ計算を含まないノーマルレベルでの記述と、 Code Gear、Data Gear の記述を含むメタレベルの記述の2種類がある。
@@ -170,15 +170,12 @@
 メタレベルでは Code Gear の引数は単一または複数の Data Gear として見ることができる。
 これは Context を直接操作することができることを意味する。
 この部分はノーマルレベルの Code Gear を呼び出す stub として生成される。
-ノーマルレベルでの goto 文はメタ計算への goto で置き換えられる。
+ノーマルレベルでの goto 文はメタ計算への goto で置き換えられる。                                                                                       
 Gears OS でのメタ計算は stub と goto のメタ計算の2箇所で実現される。
 
 メタ計算の例としては並列処理があり、Context を切り替えることによって複数のスレッドを実現している。
 Context を複数の CPU に割り当てることにより並列実行を可能にしている。
 
-
-本研究では CbC を用いての Gears OS の実装と Gears OS におけるメタ計算(Context と stub)の自動生成の実装について述べる。
-
 \section{Continuation based C (CbC)}
 CbC は Code Gear という処理の単位を用いて記述するプログラミング言語である。
 Code Gear は CbC における最も基本的な処理単位である。
@@ -370,41 +367,43 @@
 
 goto 文での引数は通常の関数呼出と異なり、スタック(環境)に積むことができない。引数に必要な情報を含むData Gearを
 持ち歩くスタイルとなる。一つのインタフェース内部では、これらは共通している。実際、これらはメタレベルでは、
-Context というMeta Data Gear にすべて格納されている。メタレベルは、Data Gearの詳細な型は使用されない。
+Context というMeta Data Gear にすべて格納されている。メタレベルは、Data Gear の詳細な型は使用されない。
 ノーマルレベルに移行する際に stub Code Gear を通して詳細な型が接続される。
 
 インタフェースを再利用する際には、呼び出すインタフェースが持つ引数は保存される必要がある。これらは、実際には
 Context 内にあるので自動的に保存されている。ノーマルレベルの記述では、... の部分にその意味が込めれている。
-これは、可変長引数の...と同じ意味だと考えても良い。ただ、LLVM/GCCレベルでそれを実装するのは比較的難しい。
+これは、可変長引数の...と同じ意味だと考えても良い。ただ、LLVM/GCC レベルでそれを実装するのは比較的難しい。
 なので、今回はScriptによる変換を採用している。
 
 ノーマルレベルの記述と関数型プログラミングの記述の比較。Gear は必ず継続を渡す必要がある。これは一段の
-関数呼出を許しているのと同等である。70年代のFortan の関数呼出は決まった場所に戻り先を格納するので
-再起呼出ができなかったのと同じである。例えばCode Gears 以下のような型を持つ。ここで t は継続の型である。
-Stack は Stack を受けとる Stack -> t というCode Gearを継続として引数で受けとる。popStack はこの引数を
+関数呼出を許しているのと同等である。70年代の Fortan の関数呼出は決まった場所に戻り先を格納するので
+再起呼出ができなかったのと同じである。例えば Code Gears 以下のような型を持つ。ここで t は継続の型である。
+Stack は Stack を受けとる Stack \verb|->| t という Code Gear を継続として引数で受けとる。popStack はこの引数を
 呼び出す。
 
-     popStack : {a t : Set} -> Stack -> (Stack -> t) -> t
+\verb|popStack : {a t : Set} -> Stack |
+
+\verb|           -> (Stack -> t) -> t|
 
 つまり、Code Gear は制限された関数の形式を持っている。Data Gear は、関数型言語の直積や排他的論理和(Sum)を含むデータ型に
-対応する。しかし、一つのContext で実行されるData Gear は、一つの巨大なSumに含まれるようになっている。これを
+対応する。しかし、一つの Context で実行される Data Gear は、一つの巨大なSumに含まれるようになっている。これを
 メタレベルでは、中の型の詳細に立ち入ることなく実行する。
 
-Context はノーマルレベルのData Gearの他に様々なメタ情報を持つ。例えば、メモリ管理情報や実行されるCPU、あるいは、Taskの
-状態、待ち合わせているData Gearなどである。これらの情報はCやアセンブラのレベルで実装されるのと同時に、通常のGearの
-プログラミングにも対応する。例えば、CPUをかそうてきにGearsで記述すればソフトウェア的な並列実行を実現し、実際の
-GPUを用いればGPUによる並列実行となる。この実行をモデル検査的な状態数え上げに対応させればモデル検査を実行できる。
+Context はノーマルレベル のData Gear の他に様々なメタ情報を持つ。例えば、メモリ管理情報や実行される CPU 、あるいは、Task の
+状態、待ち合わせている Data Gear などである。これらの情報は C やアセンブラのレベルで実装されるのと同時に、通常の Gear の
+プログラミングにも対応する。例えば、CPU をかそうてきに Gears で記述すればソフトウェア的な並列実行を実現し、実際の
+GPU を用いれば GPU による並列実行となる。この実行をモデル検査的な状態数え上げに対応させればモデル検査を実行できる。
 
-Haskell などを実行可能仕様記述として用いるOSの検証\cite{}と、Code Gearを用いる手法は類似しているが、Code Gearの場合は、
+Haskell などを実行可能仕様記述として用いる OS の検証\cite{Klein:2009:SFV:1629575.1629596,Chen:2015:UCH:2815400.2815402}と、Code Gear を用いる手法は類似しているが、Code Gear の場合は、
 記述を制限し、Code と仕様の対応、さらにCodeと資源の対応が明確になる利点がある。
 
-型つきアセンブラは、より低レベルの関数型の記述であると言える。アセンブラの記述自体は小さく扱いやすいが、
-OSレベルあるいはアプリケーションレベルからの距離が大きい。型の整合性を保証するだけではOSの検証としては
+型つきアセンブラ\cite{Yang:2010:SLI:1806596.1806610}は、より低レベルの関数型の記述であると言える。アセンブラの記述自体は小さく扱いやすいが、
+OS レベルあるいはアプリケーションレベルからの距離が大きい。型の整合性を保証するだけでは OS の検証としては
 不十分なので、証明やモデル検査を用いることになるが、記述量が多いのが、その際に欠点となる。
-Code Gearは、より大きな単位であり、プログラミングレベルの抽象化が可能になっているので、これらの記述の
+Code Gear は、より大きな単位であり、プログラミングレベルの抽象化が可能になっているので、これらの記述の
 大きさの欠点をカバーできる可能性がある。
 
-証明手法は、従来では Hoare Logic のような Post Condition / Pre Condition を用いる方法が使われている。
+証明手法は、従来では Hoare Logic \cite{Chen:2015:UCH:2815400.2815402}のような Post Condition / Pre Condition を用いる方法が使われている。
 現在のGearsは、Agda への変換は考えているが、その上の具体的な証明方法はまだ用意されていない。
 
 %従来の OS は、ユーザーレベルとシステムレベルを持っているが、