Binary file Paper/sigos.pdf has changed

--- a/Paper/sigos.tex	Tue May 07 23:25:05 2019 +0900
+++ b/Paper/sigos.tex	Wed May 08 17:36:46 2019 +0900
@@ -59,65 +59,55 @@
 \maketitle
 
 \section{はじめに}
-OS はさまざまなコンピュータの信頼性の基本である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。さらに非決定的な実行を持つ為、モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている。 xv6 はシンプルで扱いやすい基本的な構造を持つ OSである。このxv6 から Stack を排除することで OS の状態を有限化させることが可能となる。当研究室で開発している Continuation based C を用いてxv6 kernel を書き換えることでOSの状態を有限化可能であるかを検討する。
+
+現代の OS では拡張性と信頼性を両立させることが要求されている。
+信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。
+
+Gears OS は Continuation based C (CbC) によってアプリケーションと OS そのものを記述する。
+OS の下ではプログラムの記述は通常の処理の他に、メモリ管理、スレッドの待ち合わせやネットワークの管理、
+エラーハンドリング等の記述しなければならない処理が存在する。
+これらの計算をメタ計算と呼ぶ。
+メタ計算を通常の計算から切り離して記述するために、Code Gear、Data Gear という単位を提案している。
+CbC はこの Code Gear と Data Gear の単位でプログラムを記述する。
+
+OS は時代とともに複雑さが増し、OS の信頼性を保証することは難しい。
+そこで、基本的な OS の機能を揃えたシンプルな OS である xv6 を CbC で書き換え、OS の機能を保証する。
+
+Code Gear は goto による継続で処理を表すことができる。
+これにより、状態遷移による OS の記述が可能となり、複雑な OS のモデル検査を可能とする。
+また、CbC は 定理証明支援系 Agda に置き換えることができるように構築されている。
+これらを用いて OS の信頼性を保証したい。
+
+CbC でシステムやアプリケーションを記述するためには、Code Gear と Data Gear を柔軟に再利用する必要があり、
+機能を接続するAPIと実装の分離が可能であることが望ましい。
+Gears OS の信頼性を保証するために、形式化されたモジュールシステムを提供する必要がある。
+
+本論文では、Interface を用いたモジュールシステムの説明と、
+xv6 の CbC 書き換えについての考察を行う。
+
 
 \section{Continuation based C}
 \subsection{CbCの概要}
-CbC は処理を Code Gear とした単位を用いて記述するプログラミング言語である。 Code Gear 間では軽量継続 (goto 文) による遷移を行うので、継続前の Code Gear に戻 ることはなく、状態遷移ベースのプログラミングに適している。図1 は Code Gear 間 の処理の流れを表している。
+CbC は処理を Code Gear という単位を用いて記述するプログラミ
+ング言語である。 Code Gear 間では軽量継続 (goto 文) による
+遷移を行うので、継続前の Code Gear に戻 ることはない。この記述方法は
+図1のように状態
+遷移ベースのプログラミングに適している。
 
 \begin{figure}[ht]
  \begin{center}
-  \includegraphics[width=70mm]{codesegment.pdf}
+  \includegraphics[width=70mm]{fig/codesegment.pdf}
  \end{center}
  \caption{goto による code gear 間の継続}
  \label{fig:cbc}
 \end{figure}
 
-現在CbCはCコンパイラであるGCC及びLLVMをバックエンドとしたclang、MicroCコンパイラ上で実装されている。今回 xv6 のkernelの部分をこの CbC を
-用いて書き換える。
-
-\subsection{Code Gear}
-Code Gear は CbC における最も基本的な処理単位である。ソースコード \ref{codesegment} は CbC における Code Gear の一例である。
-\begin{lstlisting}[frame=lrbt,label=codesegment,caption={code segmentの軽量継続}]
-__code cs0(int a, int b){
-  goto cs1(a+b);
-}
-__code cs1(int c){
-  goto cs2(c);
-}
-\end{lstlisting}
-Code Gear は\_\_code Code Gear 名 (引数) の形で記述される。Code Gear は戻り値を持 たないので、関数とは異なり return 文は存在しない。次の Code Gear への遷移は goto Code Gear 名 (引数) で次の Code Gear への遷移を記述する。ソースコード\ref{codesegment} での goto cs1(a+b); がこれにあたる。この goto の行き先を継続と呼び、このときの a+b が次の Code Gear への出力となる。Scheme の継続と異なり CbC には呼び出し元の環境がない ので、この継続は単なる行き先である。したがってこれを軽量継続と呼ぶこともある。cs1 へ継続した後は cs0 へ戻ることはない。軽量継続により、並列化、ループ制御、関数コー ルとスタックの操作を意識した最適化がソースコードレベルで行えるようにする。
-CbC は軽量継続による遷移を行うので、継続前の Code Gear に戻ることはなく、状態 遷移ベースのプログラミングに適している。
-
-\subsection{Data Gear}
-Data Gear は CbC におけるデータの単位である。CbC では Code Gear は Input Data Gear、Output Data Gear を引数に持ち、任意の Input Data Gear を参照し、 Output Data Gear を書き出す。図 \ref{io}  Code Gear はこのとき渡された引数の Data Gear 以外を参照することはない。この Data Gear の対応から依存関係の解決を行う。
+現在CbCはCコンパイラであるGCC\cite{cbc-gcc}及びLLVM\cite{cbc-llvm}をバックエンドとしたclang
+% MicroCコンパイラ
+上で実装されている。今回 xv6 のkernelの部分をこの CbC を 用いて書き換える。
 
-\begin{figure}[ht]
- \begin{center}
- \includegraphics[width=70mm]{IO_DataGear.pdf}
- \end{center}
- \caption{CodeGearとDataGear}
- \label{io}
-\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 を通して参照する。
 
-\subsection{Context}
-Context は実行する Code Gear と Data Gear を全て持っており、通常 OS のプロセスに相当する。
-また Context は Data Gear を構造体で定義しており、その全てを union と定義している。
-Context 内で Code Gear と Data Gear は enumにより番号で管理されている。
 
-\subsection{Interface}
-Interface は Gears OS のモジュール化の仕組みである。Interface は呼び出しの引数になる Data Gear の集合であり、そこで呼び出される Code Gear のエントリである。呼び出される Code Gear の引数となる Data Gear はここで全て定義される。Interface を定義 することで複数の実装を持つことができる。
-CbC は関数呼び出しと異なり、goto による継続で遷移を行う。このため CbCの継続にはスタックフレームがなく引数を格納する場所がない。
-Context は初期化の際に引数格納用の Data Gear の領域を確保する。Code Gear が継
-続する際にはこの領域に引数の Data Gear を格納する。この領域に確保された Data Gear へのアクセスは Interface の情報から行われる。
-
-\section{xv6 のCbCへの書き換え}
-xv6 は 2006 年に MIT のオペレーティングシステムコースで教育用の目的として開発されたオペレーティングシステムである。xv6 はプロセス、仮想メモリ、カーネルとユーザ の分離、割り込み、ファイルシステムなどの基本的な Unix の構造を持つにも関わらず、シンプルで学習しやすい。
-CbC は 継続を中心とした言語であるため状態遷移モデルに落とし込むことができる。 xv6 を CbC で書き換えることにより、OS の機能の保証が可能となる。
-\subsection{書き換え}
 
 \section{結論}
 \subsection{現状}