--- a/paper/abstract.tex	Tue Feb 12 15:01:58 2019 +0900
+++ b/paper/abstract.tex	Tue Feb 12 15:19:09 2019 +0900
@@ -18,8 +18,8 @@
 また、CbC は 定理証明支援系 Agda に置き換えることができるように構築されている。
 これらを用いて OS の信頼性を保証したい。
 
-CbC でシステムやアプリケーションを記述するためには、Code Gear と Data Gear を柔軟に再利用する必要がある。
-このときに機能を接続するAPIと実装の分離が可能であることが望ましい。
+CbC でシステムやアプリケーションを記述するためには、Code Gear と Data Gear を柔軟に再利用する必要があり、
+機能を接続するAPIと実装の分離が可能であることが望ましい。
 Gears OS の信頼性を保証するために、形式化されたモジュールシステムを提供する必要がある。
 
 本論文では、Interface を用いたモジュールシステムの説明と、
@@ -37,13 +37,17 @@
 In order to describe the meta computation separately from normal computation, we propose a unit called Code Gear, Data Gear.
 CbC describes the program in units of Code Gear and Data Gear.
 
-It is necessary to flexibly reuse Code Gear and Data Gear to describe systems and applications.
-At this time it is desirable that it is possible to separate API and implementation connecting functions.
+As the OS increases in complexity with the times, it is difficult to guarantee the reliability of the OS.
+Therefore, xv6 which is a simple OS with basic OS functions is rewritten with CbC to guarantee the function of OS.
+
+Code Gear can express processing in continuation by goto.
+This makes it possible to describe the OS by state transition and to enable model checking of complex OS.
+In addition, CbC is constructed so that it can be replaced by the theorem proving support system Agda.
+I want to guarantee the reliability of the OS using these.
+
+In order to describe systems and applications with CbC, it is necessary to flexibly reuse Code Gear and Data Gear,
+It is desirable that it is possible to separate API and implementation that connect functions.
 In order to guarantee the reliability of the Gears OS, it is necessary to provide a formatted module system.
 
 In this paper, we describe the module system using Interface,
-In order to enable meta computation and parallel execution on hardware,
-We also consider the implementation of Gears OS on Raspberry Pi.
-
-In order to meta computation on hardware and execute it in parallel, basic OS functions are aligned,
-It is realized by replacing simple xv 6 with Gears OS.
+Consideration about CbC rewriting of xv6.

--- a/paper/conclusion.tex	Tue Feb 12 15:01:58 2019 +0900
+++ b/paper/conclusion.tex	Tue Feb 12 15:19:09 2019 +0900
@@ -31,4 +31,4 @@
 今後の課題は、
 現在は xv6 のシステムコールの一部のみの書き換えと、設計のみしか行っていないので、カーネル全ての書き換えと、
 Gears OS の TaskManager の置き換えを行い、Gears OS の機能を xv6 に組み込む必要がある。
-また、xv6-rpi は QEMU のみの動作でしか確認してないため、実機上での動作を行う必要がある。
+また、xv6-rpi は QEMU のみの動作でしか確認してないため、実機上での動作が可能なように実装する必要がある。

--- a/paper/evaluation.tex	Tue Feb 12 15:01:58 2019 +0900
+++ b/paper/evaluation.tex	Tue Feb 12 15:19:09 2019 +0900
@@ -94,14 +94,6 @@
 元の C のソースコードからの大きな変更をすることなしに、
 図 \ref{fig:state} のように状態遷移ベースの実行可能なプログラムへと落とし込むことができた。
 
-\begin{figure}[ht]
- \begin{center}
-  \includegraphics[width=150mm]{fig/state.pdf}
- \end{center}
- \caption{read システムコールの遷移図}
- \label{fig:state}
-\end{figure}
-
 また、CbC は C 言語との互換があるため、システムコールのみ CbC へと書き換えるといったことも可能であるため、
 信頼性を保証したい機能のみを CbC で記述することもできる。
 

Binary file paper/master_paper.pdf has changed

--- a/paper/xv6.tex	Tue Feb 12 15:01:58 2019 +0900
+++ b/paper/xv6.tex	Tue Feb 12 15:19:09 2019 +0900
@@ -10,7 +10,7 @@
 また、ハードウェア上でのメタレベルの計算や並列実行を行いたい。
 このため、xv6 を ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである Raspberry pi 用に移植した xv6-rpi を用いて実装する。
 
-\section{xv6 のモジュール化}
+\section{xv6 の構成要素}
 
 xv6 全体を CbC で書き換えるためには Interface を用いてモジュール化する必要がある。
 xv6 をモジュール化し、CbC で書き換えることができれば、Gears OS の機能を置き換えることもできる。
@@ -25,8 +25,6 @@
 \end{figure}
 
 \newpage
-
-\section{xv6 の構成要素}
 xv6 はカーネルと呼ばれる形式をとっている。
 カーネルは OS にとって中核となるプログラムである。
 xv6 ではカーネルとユーザープログラムは分離されており、カーネルはプログラムにプロセス管理、メモリ管理、I/O やファイルの管理などのサービスを提供する。
@@ -104,11 +102,6 @@
 
 オリジナルの xv6 は x86 アーキテクチャで実装されたものだが、xv6-rpi は Raspberry Pi 用に実装されたものである。
 
-xv6-rpi を CbC で書き換えるために、
-GCC 上で実装した CbC コンパイラを ARM 向けに build し xv6-rpi をコンパイルした。
-これにより、 xv6-rpi を CbC で書き換えることができるようになった。
-
-\section{Raspberry Pi}
 Raspberry Pi は ARM\cite{arm}  プロセッサを搭載したシングルボードコンピュータである。
 教育用のコンピューターとして開発されたもので、低価格であり、小型であるため使い勝手が良い。
 ストレージにハードディスクや SSD を使用するのではなく、SD カードを用いる。
@@ -116,6 +109,10 @@
 
 Raspberry Pi には Raspberry Pi 3、Raspberry Pi 2、Raspberry Pi 1、Raspberry Pi Zero といったバージョンが存在する。
 
+xv6-rpi を CbC で書き換えるために、
+GCC 上で実装した CbC コンパイラを ARM 向けに build し xv6-rpi をコンパイルした。
+これにより、 xv6-rpi を CbC で書き換えることができるようになった。
+
 \section{CbC によるシステムコールの書き換え}
 CbC によるシステムコールの書き換えは、従来の xv6 のシステムコールの形から、
 大きく崩すことなく可能である。