Binary file Paper/sigos.pdf has changed

--- a/Paper/sigos.tex	Tue May 07 20:33:06 2019 +0900
+++ b/Paper/sigos.tex	Tue May 07 21:12:29 2019 +0900
@@ -58,12 +58,8 @@
 
 \maketitle
 
-\section{OS の拡張性と信頼性の両立}
-OS はさまざまなコンピュータの信頼性の基本である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要があり、さらに非決定的な実行を持つ為、モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている。
-証明やモデル検査を用いて OS を検証する方法はさまざまなものが検討されている。検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しくなること に検証をやり直す必要がある。つまり信頼性と拡張性を両立させることが重要である。
-コンピュータの計算はプログラミング言語で記述されるが、その言語の実行は操作的意 味論の定義などで規定される。プログラミング言語で記述される部分をノーマルレベル の計算と呼ぶ。実際にコードが実行される時には、処理系の詳細や使用する資源、あるい は、コードの仕様や型などの言語以外の部分が服属する。これをメタレベルの計算とい う。この二つのレベルを同じ言語で記述できるようにして、ノーマルレベルの計算の信頼 性をメタレベルから保証できるようにしたい。ノーマルレベルでの正当性を保証しつつ、 新しく付け加えられたデバイスやプログラムを含む正当性を検証したい。
-ノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C(以 下 CbC) を用いる。CbC は関数呼出時の暗黙の環境 (Environment) を使わずに、コー ドの単位を行き来できる引数付き goto 文 (parametarized goto) を持つ C と互換性のある 言語である。これを用いて、Code Gear と Data Gear、さらにそのメタ構造を導入する。 これらを用いて、検証された Gears OS を構築したい。
-Meta Gear を入れかえることにより、ノーマルレベルの Gear をモデル検査することが できるようにしたい。ノーマルレベルでの Code Gear と Data Gear は継続を基本とした 関数型プログラミング的な記述に対応する。この記述を定理証明支援系である Agda を用 いて直接に証明できるようにしたい。Gears OS の記述はそのまま Agda に落ちる。Code Gear、Data Gear を用いた言語である CbC で記述することによって検証された OS を実 装することができる。
+\section{OS }
+OS はさまざまなコンピュータの信頼性の基本である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。さらに非決定的な実行を持つ為、モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている。現段階で動作する OS として xv6 を採用し、 CbCで書き換えることにより stackを排除し状態遷移化することができる。状態遷移化することにより状態を有限化させることが可能となるため、評価が容易になる。よって評価を容易にするためにxv6 kernel をCbC で書き換え状態遷移に落とし込むことを目的とする。
 
 
 \section{Continuation based C}
@@ -106,15 +102,19 @@
 \end{figure}
 
 \section{Gears OSの概要}
-Gears OS は Code Gear、Data Gear の単位を用いて開発されており、CbC で記述されて いる。Gears OS は Context と呼ばれる使用されるすべての Code Gear、Data Gear 持っ ている Meta Data Gear を持つ。Gears OS は継続の際この Context を常に持ち歩き、必要な Code Gear、Data Gear を参照したい場合、この Context を通して参照する。
+Gears OS は Code Gear、Data Gear の単位を用いて開発されており、CbC で記述されている。Gears OS は Context と呼ばれる使用されるすべての Code Gear、Data Gear 持っ ている Meta Data Gear を持つ。Gears OS は継続の際この Context を常に持ち歩き、必要な Code Gear、Data Gear を参照したい場合、この Context を通して参照する。
+
+\subsection{Context}
+Context は実行する Code Gear と Data Gear を全て持っている Meta Data Gear で ある。Context は通常の OS のスレッドに対応する。
+
+\subsection{Interface}
 
 \section{xv6 のCbCへの書き換え}
-\subsection{現状}
 
 \subsection{書き換え}
 
 \section{結論}
-\subsection{評価}
+\subsection{現状}
 
 \subsection{今後}
 \subsection{}