--- a/paper/anatofuz-sigos.tex	Thu May 07 16:33:47 2020 +0900
+++ b/paper/anatofuz-sigos.tex	Thu May 07 19:04:11 2020 +0900
@@ -83,11 +83,9 @@
 テスト以外の方法でOSの信頼性を高めたい。
 
 そこで数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
-OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、Agda定理証明支援系\cite{}を利用した証明ベースでの信頼性の確保などの手法が考えられる。
-形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。
-% これに適した形として、 状態遷移モデルが挙げられる。
+OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、定理証明支援系Agda\cite{agda}を利用した証明ベースでの信頼性の確保などの手法が考えられる。\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}
+形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。\cite{hyperKernel}
 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。
-% 既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析し、仕様記述言語などによる再実装が必要となる。
 しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。
 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。
 
@@ -97,18 +95,16 @@
 実装のソースコードはノーマルレベルであり検証用のソースコードはメタ計算だと考えると、OSそのものが
 検証を行ない、システム全体の信頼を高める機能を持つべきだと考える。
 ノーマルレベル上でのバグを例えばモデル検査のようなメタ計算によって発見し信頼性を向上させたい。
-% プログラマからはノーマルレベルの計算のみ実装するが、整合性の確認や拡張を行う際にノーマルレベルと同様の記述力でメタ計算も実装できる必要がある。
 
 ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。
-CbCは基本 goto で CodeGaar というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と
-呼ばれる隠れた状態を持たない。このため、計算のための情報は CodeGearの入力にすべてそろっている。そのうちのいくつかはメタ計算、
+CbCは基本\texttt{goto}で\texttt{CodeGaar}というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と
+呼ばれる隠れた状態を持たない。このため、計算のための情報は\texttt{CodeGear}の入力にすべてそろっている。そのうちのいくつかはメタ計算、
 つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(DataGear)である。メタ計算とノーマルレベルの
 区別は入力のどこを扱うかの差に帰着される。
 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
-CbCは GCC \cite{}あるいは LLVM \cite{}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。
-またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
-% すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。
+CbCは\texttt{GCC}\cite{gcc}\cite{weko_82695_1}あるいは\texttt{LLVM}\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。
+またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{agda-ryokka}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
 
 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。
 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。
@@ -140,34 +136,28 @@
     \label{fig:cgdg}
 \end{figure}
 
-CbCで階乗を求める例題をCode \ref{src:cbc_example}に示す。
-例題ではCodeGearとして\texttt{factorial}を宣言している。
-\texttt{factorial}はCodeGearの引数として\texttt{struct F}型の変数\texttt{arg}を受け取り、\texttt{arg}のメンバー変数によって\texttt{factorial}の再帰呼び出しを行う。
-CodeGearの呼び出しは\texttt{goto}文によって行われる。
-この例題を状態遷移図にしたものを図\ref{fig:factorial_cbc}に示す。
-図中の四角がDataGear、 円がCodeGearに対応する。
-
+CbCを利用したシステムコールのディスパッチ部分をCode \ref{src:cbc_example}に示す。
+この例題では特定のシステムコールの場合、 CbCで実装された処理に\texttt{goto}文をつかって継続する。
+例題ではCodeGearへのアドレスが配列\texttt{cbccodes}に格納されている。
+引数として渡している\texttt{cbc\_ret}は、 システムコールの返り値の数値をレジスタに代入するCodeGearである。
 
-\begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={CbCで階乗を求める例題}]
-__code factorial(struct F arg) {
-    if (arg.n<0) {
-        exit(1);
+\begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={CbCを利用したシステムコールのディスパッチ}]
+void syscall(void)
+{
+    int num;
+    int ret;
+
+    if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) {
+        proc->cbc_arg.cbc_console_arg.num = num;
+        goto (cbccodes[num])(cbc_ret);
     }
-    if (arg.n==0) {
-      goto arg.next(arg);
-    } else {
-      arg.r *= arg.n;
-      arg.n--;
-      goto factorial(arg);
-    }
-}
 \end{lstlisting}
 
 \begin{figure}[tb]
     \begin{center}
-        \includegraphics[width=80mm]{fig/factorial_cbc.pdf}
+        \includegraphics[width=80mm]{fig/cbc_syscall_Trap}
     \end{center}
-    \caption{CbCで階乗を求める例題の状態遷移}
+    \caption{CbCを利用したシステムコールディスパッチの状態遷移}
     \label{fig:factorial_cbc}
 \end{figure}
 
@@ -184,7 +174,7 @@
 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。
-CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。
+CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。\cite{gears}
 現在のGearsOSは並列フレームワークとして実装されており、 実用的なOSのプロトタイプ実装として既存のOS上への実装を目指している。
 
 GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。
@@ -225,9 +215,9 @@
 
 \section{xv6 kernel}
 
-xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。
+xv6とはマサチューセッツ工科大学でv6 OS\cite{lions1996lions}を元に開発された教育用のUNIX OSである。\cite{xv6}
 xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。
-Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。
+Raspberry Pi\cite{rpi}上での動作を目的としたARMアーキテクチャのバージョンも存在する。\cite{xv6rpi}
 本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。
 
 xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。
@@ -239,16 +229,16 @@
 本論文ではxv6の継続の分析をシステムコール部分とファイルシステム、 仮想メモリなどのOSの根幹部分でそれぞれ行った。
 
 
-\section{xv6のシステムコールの継続の分析}
+\section{xv6のシステムコールの継続の分析と書き換え}
 xv6の処理を継続を中心とした記述で再実装を行う。
 この際に、 xv6のどの処理に着目するかによって継続の実装が異なっていくことが実装につれてわかった。
 
-まずxv6の\texttt{read} システムコールに着目し、 システムコール内部でどのような状態を遷移するかを分析した。
+まずxv6の\texttt{read} システムコールに着目し、 システムコール内部でどのような状態を遷移するかを分析した。 \cite{weko_195888_1}
 分析結果をCbCのCodeGearに変換し、 状態遷移図におこしたものを図\ref{fig:cbc_readsyscall}に示す。
 
 \begin{figure}[tb]
     \begin{center}
-        \includegraphics[width=80mm]{fig/readsyscall_state.pdf}
+        \includegraphics[width=80mm]{fig/readsyscall.pdf}
     \end{center}
     \caption{readシステムコールの状態遷移}
     \label{fig:cbc_readsyscall}
@@ -312,7 +302,7 @@
 
         if (dip->type == 0) {  // a free inode
             memset(dip, 0, sizeof(*dip));
-            // omission
+            ...
             return iget(dev, inum);
         }
         brelse(bp);
@@ -337,8 +327,9 @@
 \end{lstlisting}
 
 Code\ref{src:allocinode_loopcheck}ではループ条件の成立を\texttt{if}文で確認し、ループ処理に移行する場合は \texttt{allocinode\_loop}へ遷移する。
+\texttt{goto}文の中の引数の1つ\texttt{next(...)} は、 APIとして呼び出した\texttt{ialloc}の次の継続のCodeGearに対して、 \texttt{context}などの環境を渡す構文である。
 ループ条件が満たされなかった場合は、 コンテキストから\texttt{panic}に関するCodeGearの集合を取り出し、 集合中の\texttt{panic} CodeGearへと遷移する。
-オリジナルの処理では、　ループ中に\texttt{dip->type == 0}が満たされた場合は関数から\texttt{return}文により関数から復帰する。
+オリジナルの処理では、 ループ中に\texttt{dip->type == 0}が満たされた場合は関数から\texttt{return}文により関数から復帰する。
 CodeGearではCode\ref{src:alloc_loop}内で、 状態が分けられる。
 この先の継続は、　復帰用のCodeGearかループの先頭である\texttt{allocinode\_loopcheck}に再帰的に遷移するかになる。
 
@@ -390,7 +381,7 @@
 
 void userinit(void)
 {
-// omission
+...
 
     if((p->pgdir = kpt_alloc()) == NULL) {
         panic("userinit: out of memory?");
@@ -400,7 +391,7 @@
 
     p->sz = PTE_SZ;
     memset(p->tf, 0, sizeof(*p->tf));
-// omission
+...
 }
 \end{lstlisting}