--- a/Paper/sigos.tex	Thu Apr 12 20:15:23 2018 +0900
+++ b/Paper/sigos.tex	Thu Apr 12 21:49:46 2018 +0900
@@ -104,9 +104,10 @@
 \section{OS の拡張性と信頼性の両立}
 
 さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩する。
-ハードウェア、サービスに対応して OS 自体が拡張される必要がある。OS は非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分
-であり、テストしきれない部分が残ってしまう。これに対処するためには、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法が
-ある。モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている
+ハードウェア、サービスに対応して OS 自体が拡張される必要がある。
+OS は非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分であり、テストしきれない部分が残ってしまう。
+これに対処するためには、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
+モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている
 図\ref{fig:verification}。
 \begin{figure}[ht]
  \begin{center}
@@ -116,17 +117,21 @@
  \label{fig:verification}
 \end{figure}
 
-証明やモデル検査を用いて OS を検証する方法はさまざまなものが検討されている。検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しく
-なることに検証をやり直す必要がある。つまり信頼性と拡張性を両立させることが重要である。
+証明やモデル検査を用いて OS を検証する方法はさまざまなものが検討されている。
+検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しくなることに検証をやり直す必要がある。
+つまり信頼性と拡張性を両立させることが重要である。
 
-コンピュータの計算はプログラミング言語で記述されるが、その言語の実行は操作的意味論の定義などで規定される。プログラミング言語で記述される部分を
-ノーマルレベルの計算と呼ぶ。コードが実行される時には、処理系の詳細や使用する資源、あるいは、コードの仕様や型などの言語以外の部分が服属する。
-これをメタレベルの計算という。この二つのレベルを同じ言語で記述できるようにして、ノーマルレベルの計算の信頼性をメタレベルから保証できるようにしたい。
+コンピュータの計算はプログラミング言語で記述されるが、その言語の実行は操作的意味論の定義などで規定される。
+プログラミング言語で記述される部分をノーマルレベルの計算と呼ぶ。
+コードが実行される時には、処理系の詳細や使用する資源、あるいは、コードの仕様や型などの言語以外の部分が服属する。
+これをメタレベルの計算という。
+この二つのレベルを同じ言語で記述できるようにして、ノーマルレベルの計算の信頼性をメタレベルから保証できるようにしたい。
 ノーマルレベルでの正当性を保証しつつ、新しく付け加えられたデバイスやプログラムを含む正当性を検証したい。
 
-本論文では、ノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C(以下CbC)\cite{cbc}を用いる。CbC は関数呼出時の暗黙の環境(Environment)
-を使わずに、コードの単位を行き来できる引数付き goto 文(parametarized goto)を持つ C と互換性のある言語である。これを用いて、Code Gear と Data Gear、さら>に
-そのメタ構造を導入する。これらを用いて、検証された Gears OS を構築したい。
+本論文では、ノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C(以下CbC)\cite{cbc}を用いる。
+CbC は関数呼出時の暗黙の環境(Environment)を使わずに、コードの単位を行き来できる引数付き goto 文(parametarized goto)を持つ C と互換性のある言語である。
+これを用いて、Code Gear と Data Gear、さらにそのメタ構造を導入する。
+これらを用いて、検証された Gears OS を構築したい。
 図\ref{fig:MetaGear}。
 \begin{figure}[ht]
  \begin{center}
@@ -136,29 +141,29 @@
  \label{fig:MetaGear}
 \end{figure}
 
-本論文では、Gears OS の要素である Code Gear、Data Gear、そして、Meta Code Gear 、Meta Data Gear の構成を示す。これらは、CbC に変換されて実行される。
+本論文では、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 による記述をノ
-ーマルレベルとして
+従来の研究でメタ計算を用いる場合は、関数型言語では 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 はスタック上に隠された
-環境を持たないので、メタレベルで使用する資源を明確にできるという利点がある。ただし、Gear のプログラミングスタイルは、従来の関数呼出
-を中心としたものとはかなり異なる。本研究では、Gears の記述をモジュールかするためにインターフェースを導入した。これにより、
-見通しの良いプログラミングが可能になった。
+Haskell などの関数型プログラミング言語では実行環境が複雑であり、実行時の資源使用を明確にすることができない。
+CbC はスタック上に隠された環境を持たないので、メタレベルで使用する資源を明確にできるという利点がある。
+ただし、Gear のプログラミングスタイルは、従来の関数呼出を中心としたものとはかなり異なる。
+本研究では、Gears の記述をモジュールかするためにインターフェースを導入した。
+これにより、見通しの良いプログラミングが可能になった。
 
 \section{メタ計算の重要性}
-プログラムを記述する際、ノーマルレベルの処理の他に、メモリ管理、スレッド管理、CPU や GPU の資源管理等、記述しなければならない処理が存在する。
-これらの計算をメタ計算と呼ぶ。
-
 従来の OS では、メタ計算はシステムコールやライブラリーコールの単位で行われる。
 実行時にメタ計算の変更を行う場合には、OS 内部のパラメータの変更を使用し、
 実行されるユーザープログラム自体への変更は限定的である。
@@ -176,12 +181,11 @@
 関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。
 Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、これらを用いてメタ計算を実現する。
 
-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種類がある。
+CbC での記述はメタ計算を含まないノーマルレベルでの記述と、Meta Code Gear、Meta Data Gear の記述を含むメタレベルの記述の2種類がある。
 メタレベルでもさらに、メタ計算を用いることが可能になっている。
 この2つのレベルはプログラミング言語レベルでの変換として実現される。
 CbC は LLVM\cite{llvm} 上で実装されており、メタレベルでの変換系は本論文では、Perl による変換スクリプトにより実装されている。