Binary file paper/master_paper.pdf has changed

--- a/paper/xv6.tex	Mon Feb 11 15:23:36 2019 +0900
+++ b/paper/xv6.tex	Mon Feb 11 17:10:33 2019 +0900
@@ -1,20 +1,29 @@
 \chapter{xv6 の CbC への書き換え}
-Gears OS をハードウェア上で実装するために、ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである Raspberry Pi 上で Gears OS 実装したい。
-ハードウェア上でのメタレベルの計算や並列実行を行うために、Linax 等に比べてシンプルである xv6 の機能の一部を Gears OS に置き換えることで実現させる。
-xv6 は UNIX V6 を x86 へ再実装したものであるが、
-ここでは xv6\cite{xv6} を Raspberry pi 用に移植した xv6-rpi を用いて実装する。
-
-Xv6 は 2006 年に MIT のオペレーティングシステムコースで教育用の目的として開発されたオペレーティングシステムである。
-Xv6 はプロセス、仮想メモリ、カーネルとユーザの分離、割り込み、ファイルシステムなどの基本的な Unix の構造を持つにも関わらず、
+xv6 は 2006 年に MIT のオペレーティングシステムコースで教育用の目的として開発されたオペレーティングシステムである。
+xv6 はプロセス、仮想メモリ、カーネルとユーザの分離、割り込み、
+ファイルシステムなどの基本的な Unix の構造を持つにも関わらず、
 シンプルで学習しやすい。
 
-\section{Raspberry Pi}
-Raspberry Pi は ARM プロセッサを搭載したシングルボードコンピュータである。
-教育用のコンピューターとして開発されたもので、低価格であり、小型であるため使い勝手が良い。
-ストレージにハードディスクや SSD を使用するのではなく、SD カードを用いる。
-HDMI 出力や USB ポートも備えており、開発に最適である。
+CbC は 継続を中心とした言語であるため状態遷移モデルに落とし込むことができる。
+xv6 を CbC で書き換えることにより、OS の機能の保証が可能となる。
+
+また、ハードウェア上でのメタレベルの計算や並列実行を行いたい。
+このため、xv6\cite{xv6} を ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである Raspberry pi 用に移植した xv6-rpi を用いて実装する。
+
+\section{xv6 のモジュール化}
 
-Raspberry Pi には Raspberry Pi 3、Raspberry Pi 2、Raspberry Pi 1、Raspberry Pi Zero といったバージョンが存在する。
+xv6 全体を CbC で書き換えるためには Interface を用いてモジュール化する必要がある。
+xv6 をモジュール化し、CbC で書き換えることができれば、Gears OS の機能を置き換えることもできる。
+図 \ref{fig:xv6Interface} は xv6 の構成図となる。
+
+\begin{figure}[ht]
+ \begin{center}
+  \includegraphics[width=150mm]{fig/xv6.pdf}
+ \end{center}
+ \caption{モジュール化した xv6 の構成}
+ \label{fig:xv6Interface}
+\end{figure}
+
 
 \section{xv6 の構成要素}
 xv6 はカーネルと呼ばれる形式をとっている。
@@ -163,27 +172,14 @@
 
 \lstinputlisting[label=readi, caption=readi の CbC 書き換えの例]{./src/readi.c}
 
-
+ソースコード \ref{consoleread} 11、50、行目 では sleep へ継続する際、戻るべき継続先を一緒に送ることで、
+sleep から consoleread に戻ってくることができる。
 
 \lstinputlisting[label=consoleread, caption=consoleread の CbC 書き換えの例]{./src/console.c}
 
 
 xv6 のシステムコールの関数を CbC で書き換え、QEMU 上で動作させることができた。
 
-\section{xv6 のモジュール化}
-
-xv6 全体を CbC で書き換えるためには Interface を用いてモジュール化する必要がある。
-xv6 をモジュール化し、CbC で書き換えることができれば、Gears OS の機能を置き換えることもできる。
-図 \ref{fig:xv6Interface} は xv6 の構成図となる。
-
-\begin{figure}[ht]
- \begin{center}
-  \includegraphics[width=150mm]{fig/xv6.pdf}
- \end{center}
- \caption{モジュール化した xv6 の構成}
- \label{fig:xv6Interface}
-\end{figure}
-
 \section{xv6 の CbC 書き換えによる考察}
 
 CbC は Code Gear 間の遷移は goto による継続で行われるため、
@@ -197,3 +193,11 @@
 これらのため、CbC で記述された実行可能な OS そのものがモデル検査と定理証明が可能となり、
 OS の信頼性が保証できる。
 
+\section{Raspberry Pi}
+Raspberry Pi は ARM\cite{arm}  プロセッサを搭載したシングルボードコンピュータである。
+教育用のコンピューターとして開発されたもので、低価格であり、小型であるため使い勝手が良い。
+ストレージにハードディスクや SSD を使用するのではなく、SD カードを用いる。
+HDMI 出力や USB ポートも備えており、開発に最適である。
+
+Raspberry Pi には Raspberry Pi 3、Raspberry Pi 2、Raspberry Pi 1、Raspberry Pi Zero といったバージョンが存在する。
+