Binary file Paper/sigos.pdf has changed

--- a/Paper/sigos.tex	Tue May 07 13:21:36 2019 +0900
+++ b/Paper/sigos.tex	Tue May 07 20:33:06 2019 +0900
@@ -2,26 +2,55 @@
 %\usepackage[dvips]{graphicx}
 \usepackage{latexsym}
 \usepackage[dvipdfmx]{graphicx} 
+\usepackage{listings}
+\usepackage{caption}
 
 \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
 \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
 \def\|{\verb|}
+\def\lstlistingname{ソースコード}
+
+\newcommand\coderef[1]{ソースコード \ref{code:#1}}
+
+\lstset{
+  frame=single,
+  keepspaces=true,
+  stringstyle={\ttfamily},
+  commentstyle={\ttfamily},
+  identifierstyle={\ttfamily},
+  keywordstyle={\ttfamily},
+  basicstyle={\ttfamily},
+  breaklines=true,
+  xleftmargin=0zw,
+  xrightmargin=0zw,
+  framerule=.2pt,
+  columns=[l]{fullflexible},
+  numbers=left,
+  stepnumber=1,
+  numberstyle={\scriptsize},
+  numbersep=1em,
+  language={},
+  tabsize=4,
+  lineskip=-0.5zw,
+  escapechar={@},
+}
+
 
 \begin{document}
 
 \title{継続を用いたxv6 kernelの書き換え}
 
-\paffiliate{JU1}{琉球大学工学部情報工学科\\
+\paffiliate{IPSJ}{琉球大学工学部情報工学科\\
 Information Engineering, University of the Ryukyus.}
-\paffiliate{JU2}{琉球大学大学院理工学研究科情報工学専攻\\
+\paffiliate{JU}{琉球大学大学院理工学研究科情報工学専攻\\
 Interdisciplinary Information Engineering, Graduate School of Engineering and Science, University of the Ryukyus.}
 
-\author{坂本昂弘}{Takahiro SAKAMOTO}{JU1}
-\author{桃 原 優}{Yu TTOBARU}{JU2}
-\author{河野真治}{Shinji KONO}{JU1}
+\author{坂本昂弘}{Takahiro SAKAMOTO}{IPSJ}
+\author{桃 原 優}{Yu TTOBARU}{IPSJ}
+\author{河野真治}{Shinji KONO}{IPSJ}
 
 \begin{abstract}
-xv6 は MIT で教育用の目的で開発されたオペレーティングシステムで基本的な Unix の構造を持っている。当研究室で開発している Continuation based C (CbC) は継続を中心とした言語で、状態遷移モデルに落とし込むことで検証を行いたい。xv6 を CbC で書き換えることで、 オペレーティングシステムの基本的な機能に対する検証を行う。
+xv6 は MIT で教育用の目的で開発されたオペレーティングシステムで基本的な Unix の構造を持っている。当研究室で開発している Continuation based C (CbC) は継続を中心とした言語で、用いることにより検証しやすくなる。xv6 を CbC で書き換えることで、 オペレーティングシステムの基本的な機能に対する検証を行うために書き換えを行う。
 \end{abstract}
 
 
@@ -29,15 +58,17 @@
 
 \maketitle
 
-\section{はじめに}
-
+\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{Continuation based C}
-CbC は処理をCode Gear とした単位を用いて記述するプログラミング言語である。
-Code Gear 間では軽量継続（goto 文）による遷移を行うので、継続前の Code Gearに
-戻ることなく、状態遷移ベースのプログラミングに適している。 図1はCode Gear 間の
-処理の流れを表している。
+\subsection{CbCの概要}
+CbC は処理を Code Gear とした単位を用いて記述するプログラミング言語である。 Code Gear 間では軽量継続 (goto 文) による遷移を行うので、継続前の Code Gear に戻 ることはなく、状態遷移ベースのプログラミングに適している。図1 は Code Gear 間 の処理の流れを表している。
 
 \begin{figure}[ht]
  \begin{center}
@@ -47,29 +78,49 @@
  \label{fig:cbc}
 \end{figure}
 
-現在CbCはLLVM[11]とGCC[12]上で実装されている。今回 xv6 のkernelも部分をこの CbC を
+現在CbCはCコンパイラであるGCC及びLLVMをバックエンドとしたclang、MicroCコンパイラ上で実装されている。今回 xv6 のkernelの部分をこの CbC を
 用いて書き換える。
 
-\section{xv6 の概要}
+\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 の対応から依存関係の解決を行う。
 
 \begin{figure}[ht]
  \begin{center}
-  \includegraphics[width=70mm]{xv6.pdf}
+ \includegraphics[width=70mm]{IO_DataGear.pdf}
  \end{center}
- \caption{xv6 の構成図}
- \label{fig:cbc}
+ \caption{CodeGearとDataGear}
+ \label{io}
 \end{figure}
 
-\section{xv6 kernel のCbCによる書き換え}
+\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 を通して参照する。
+
+\section{xv6 のCbCへの書き換え}
 \subsection{現状}
 
 \subsection{書き換え}
 
 \section{結論}
+\subsection{評価}
+
+\subsection{今後}
+\subsection{}
 
 \begin{thebibliography}{9}
-\bibitem{latex} 宮城光希: \textbf{}. 琉球大学理工学研究科修士論文、2019
+\bibitem{latex} 宮城光希: \textbf{継続を基本とした言語によるOSのモジュール化}. 琉球大学理工学研究科修士論文、2019
 
 \end{thebibliography}
-
 \end{document}