Binary file Paper/sigos.pdf has changed

--- a/Paper/sigos.tex	Thu May 09 17:42:06 2019 +0900
+++ b/Paper/sigos.tex	Thu May 09 18:26:22 2019 +0900
@@ -39,7 +39,7 @@
 
 \begin{document}
 
-\title{継続を用いたxv6 kernelの書き換え}
+\title{継続を用いたx.v6 kernelの書き換え}
 
 \paffiliate{IPSJ}{琉球大学工学部情報工学科\\
 Information Engineering, University of the Ryukyus.}
@@ -51,15 +51,42 @@
 \author{河野真治}{Shinji KONO}{IPSJ}
 
 \begin{abstract}
-xv6 は MIT で教育用の目的で開発されたオペレーティングシステムで基本的な Unix の構造を持っている．当研究室で開発している Continuation based C (CbC) は継続を中心とした言語で，用いることにより検証しやすくなる．xv6 を CbC で書き換えることで，オペレーティングシステムの基本的な機能に対する検証を行うために書き換えを行う．
+x.v6 は MIT で教育用の目的で開発されたオペレーティングシステ
+ムで基本的な Unix の構造を持っている．当研究室で開発してい
+る Continuation based C (CbC) は継続を中心とした言語で，
+継続を用いることにより適切なプログラミング単位を提供し, 検証しやすくなると考えている．
+x.v6 を CbC で書き換えることで，オペレーティングシステムの基本的な機能を stack 抜きで
+実現することができると考えれる. また, CbC では Interface という module 化を提供しており,
+これにより実装とAPIそして, メタ計算APIを分離することができる.
+実際に書き換えを行なったが, 現状での書き換えは x.v6 の基本的な構造は変更していない.
+また, 未変換の部分と両立するように作られている. 
+現在の書き換え手法について述べ, その有効性, 将来の書き換えの方針について考察する.
+
 \end{abstract}
 
+\begin{eabstract}
+x.v6 is an operating system developed at MIT for educational
+purposes and has a basic Unix structure. Continuation based
+C (CbC), developed by our laboratory, is a continuation-oriented
+language, and we believe that using continuation will provide
+an appropriate programming unit and make it easier to verify.
+By rewriting x.v6 with CbC, it is thought that the basic functions
+of the operating system can be realized without stack. In addition,
+CbC provides a modularization called Interface, and this makes
+it possible to implement, API, and The meta-calculation API
+can be separated. 
+The current rewriting does not change the basic structure of x.v6, 
+and it is made to be compatible with the unconverted part.
+This paper describes the current rewriting method and discusses
+its effectiveness and future rewriting policy. 
+
+\end{eabstract}
 
 
 
 \maketitle
 
-\section{はじめに}
+\section{x.v6を継続で書き換える意味}
 
 現代の OS では拡張性と信頼性を両立させることが要求されている．
 信頼性をノーマルレベルの計算に対して保証し，拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である．
@@ -70,21 +97,24 @@
 これらの計算をメタ計算と呼ぶ．
 メタ計算を通常の計算から切り離して記述するために，Code Gear，Data Gear という単位を提案している．
 CbC はこの Code Gear と Data Gear の単位でプログラムを記述する．
+% OS は時代とともに複雑さが増し，OS の信頼性を保証することは難しい．
 
-OS は時代とともに複雑さが増し，OS の信頼性を保証することは難しい．
-そこで，基本的な OS の機能を揃えたシンプルな OS である xv6 を CbC で書き換え，OS の機能を保証する．
 
 Code Gear は goto による継続で処理を表すことができる．
 これにより，状態遷移による OS の記述が可能となり，複雑な OS のモデル検査を可能とする．
 また，CbC は 定理証明支援系 Agda に置き換えることができるように構築されている．
+
 これらを用いて OS の信頼性を保証したい．
+CbCの有効性を示すために，基本的な機能を揃えた OS である xv6 を CbC で書き換える.
+これにより，OS の個々のシステムコールの持つ状態を明確にすることができると考えている.
 
 CbC でシステムやアプリケーションを記述するためには，Code Gear と Data Gear を柔軟に再利用する必要があり，
 機能を接続するAPIと実装の分離が可能であることが望ましい．
-Gears OS の信頼性を保証するために，形式化されたモジュールシステムを提供する必要がある．
+CbC では形式化されたモジュールシステムが提供されている. 
+xv6 の CbC 書き換えでは, このモジュールシステムを用いる.
 
-本論文では，Interface を用いたモジュールシステムの説明と，
-xv6 の CbC 書き換えについての考察を行う．
+書き換えはまだ部分的であるが, 既存の部分と両立するように設計されている. 従って, x.v6 の基本的な
+動作には変更はない. 実際に実行速度などはほとんど差がない. 逆に言えばオーバヘッドが存在しないことが確認できた.
 
 
 \section{Continuation based C}
@@ -490,12 +520,16 @@
 比較的シンプルな OS である xv6 を CbC に書き換えることにした．
 
 xv6 を CbC で書き換えることによって，実行可能な CbC プログラムで記述された OS がそのまま，
-状態遷移モデルによるモデル検査，Agda による定理証明が可能となる． 
+抽象的な
+状態遷移モデルになる. それによりモデル検査，Agda による定理証明が可能となると考えている． 
 
-今後の課題は，
-現在は xv6 のシステムコールの一部のみの書き換えと，設計のみしか行っていないので，カーネル全ての書き換えと，
-Gears OS の TaskManager の置き換えを行い，Gears OS の機能を xv6 に組み込む必要がある．
+現在は xv6 のシステムコールの一部のみの書き換えと，設計のみしか行っていないので，カーネル全ての書き換え
+をおこなう.
+
+Gears OS にはメタ計算を実装する context は par goto の機能がある. これらの機能を xv6 に組み込む方法に
+ついて考察する必要がある.
 また，xv6-rpi は QEMU のみの動作でしか確認してないため，実機上での動作が可能なように実装する必要がある．
+
 \nocite{*}
 \bibliographystyle{ipsjunsrt}
 \bibliography{reference}