\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 の構造を持つにも関わらず、
シンプルで学習しやすい。

\section{Raspberry Pi}
Raspberry Pi は ARM プロセッサを搭載したシングルボードコンピュータである。
教育用のコンピューターとして開発されたもので、低価格であり、小型であるため使い勝手が良い。
ストレージにハードディスクや SSD を使用するのではなく、SD カードを用いる。
HDMI 出力や USB ポートも備えており、開発に最適である。

Raspberry Pi には Raspberry Pi 3、Raspberry Pi 2、Raspberry Pi 1、Raspberry Pi Zero といったバージョンが存在する。

\section{xv6 の構成要素}
xv6 はカーネルと呼ばれる形式をとっている。
カーネルは OS にとって中核となるプログラムである。
xv6 ではカーネルとユーザープログラムは分離されており、カーネルはプログラムにプロセス管理、メモリ管理、I/O やファイルの管理などのサービスを提供する。
ユーザープログラムがカーネルのサービスを呼び出す場合、システムコールを用いてユーザー空間からカーネル空間へ入りサービスを実行する。
カーネルは CPU のハードウェア保護機構を使用して、ユーザー空間で実行されているプロセスが自身のメモリのみアクセスできるように保護している。
ユーザープログラムがシステムコールを呼び出すと、ハードウェアが特権レベルを上げ、カーネルのプログラムが実行される。
この特権レベルを持つプロセッサの状態をカーネルモード、特権のない状態をユーザーモードという。

\subsection{システムコール}

ユーザープログラムがカーネルの提供するサービスを呼び出す際にはシステムコールを用いる。
ユーザープログラムがシステムコールを呼び出すと、トラップが発生する。
トラップが発生すると、ユーザープログラムは中断され、カーネルに切り替わり処理を行う。
ソースコード \ref{syscall_list} は xv6 のシステムコールのリストである。

\begin{lstlisting}[frame=lrbt,label=syscall_list,caption={\footnotesize xv6 のシステムコールのリスト}]
static int (*syscalls[])(void) = {
        [SYS_fork]    =sys_fork,
        [SYS_exit]    =sys_exit,
        [SYS_wait]    =sys_wait,
        [SYS_pipe]    =sys_pipe,
        [SYS_read]    =sys_read,
        [SYS_kill]    =sys_kill,
        [SYS_exec]    =sys_exec,
        [SYS_fstat]   =sys_fstat,
        [SYS_chdir]   =sys_chdir,
        [SYS_dup]     =sys_dup,
        [SYS_getpid]  =sys_getpid,
        [SYS_sbrk]    =sys_sbrk,
        [SYS_sleep]   =sys_sleep,
        [SYS_uptime]  =sys_uptime,
        [SYS_open]    =sys_open,
        [SYS_write]   =sys_write,
        [SYS_mknod]   =sys_mknod,
        [SYS_unlink]  =sys_unlink,
        [SYS_link]    =sys_link,
        [SYS_mkdir]   =sys_mkdir,
        [SYS_close]   =sys_close,
};
\end{lstlisting}

\subsection{プロセス}
プロセスとは、カーネルが実行するプログラムの単位である。
xv6 のプロセスは、ユーザー空間メモリとカーネル用のプロセスの状態を持つ空間で構成されている。
プロセスは独立しており、他のプロセスからメモリを破壊されたりすることはない。
また、独立していることでカーネルそのものを破壊することもない。
各プロセスの状態は struct proc によって管理されている。
プロセスは fork システムコールによって新たに生成される。
fork は新しく、親プロセスと呼ばれる呼び出し側と同じメモリ内容の、子プロセスと呼ばれるプロセスを生成する。
fork システムコールは、親プロセスであれば子プロセスのID、子プロセスであれば 0 を返す。
親プロセスと子プロセスは最初は同じ内容を持っているが、それぞれ異なるメモリ、レジスタで実行されているため、片方のメモリ内容を変更してももう片方に影響はない。
exit システムコールはプロセスの停止を行い、メモリを解放する。
wait システムコールは終了した子プロセスのIDを返す。子プロセスが終了するまで待つ。
exec システムコールは呼び出し元のプロセスのメモリをファイルシステムのファイルのメモリイメージと置き換え実行する。
ファイルには命令、データなどの配置が指定されたフォーマット通りになっていなければならない。
xv6 は ELF と呼ばれるフォーマットを扱う。

\subsection{ファイルディスクリプタ}
ファイルディスクリプタは、カーネルが管理するプロセスが読み書きを行うオブジェクトを表す整数値である。
プロセスは、ファイル、ディレクトリ、デバイスを開く、または既存のディスクリプタを複製することによって、
ファイルディスクリプタを取得する。
xv6 はプロセス毎にファイルディスクリプタのテーブルを持っている。
ファイルディスクリプタは普通、0 が標準入力、1 が標準出力、2 がエラー出力として使われる。
ファイルディスクリプタのテーブルのエントリを変更することで入出力先を変更することができる。
1 の標準出力を close し、ファイルを open することでプログラムはファイルに出力することになる。
ファイルディスクリプタはファイルがどのように接続するか隠すことでファイルへの入出力を容易にしている。

\subsection{ファイルシステム}
xv6 のファイルシステムはバイト配列であるデータファイルとデータファイルおよび他のディレクトリの参照を含むディレクトリを提供する。
ディレクトリは root と呼ばれる特別なディレクトリから始まるツリーを形成している。
絶対パスである "/dir1/dir2/file1" というパスは root ディレクトリ内の dir1 という名前のディレクトリ内の dir2 という名前のディレクトリ内の file というデータファイルを指す。
相対パスである "dir2/file2" のようなパスは、現在のディレクトリ内の dir2 という名前のディレクトリ内の file というデータファイルを指す。

\section{xv6-rpi の CbC 対応}

オリジナルの xv6 は x86 アーキテクチャで実装されたものだが、xv6-rpi は Raspberry Pi 用に実装されたものである。

xv6-rpi を CbC で書き換えるために、
GCC 上で実装した CbC コンパイラを ARM 向けに build し xv6-rpi をコンパイルした。
これにより、 xv6-rpi を CbC で書き換えることができるようになった。

\section{システムコールの書き換え}
ソースコード \ref{syscall} は syscall() におけるシステムコールの呼び出しを行うコードである。
システムコールはソースコード \ref{syscall_list} の関数のリストから呼び出される。
CbC でも同様に num で指定された番号の cbccodes のリストの Code Gear へ goto する。
引数に持つ cbc\_ret は 継続した先でトラップに戻ってくるための Code Gear である。

\begin{lstlisting}[frame=lrbt,label=syscall,caption={\footnotesize syscall()}]
    if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) {
        proc->cbc_arg.cbc_console_arg.num = num;
        goto (cbccodes[num])(cbc_ret);
    }


    if((num > 0) && (num <= NELEM(syscalls)) && syscalls[num]) {
        ret = syscalls[num]();

        // in ARM, parameters to main (argc, argv) are passed in r0 and r1
        // do not set the return value if it is SYS_exec (the user program
        // anyway does not expect us to return anything).
        if (num != SYS_exec) {
            proc->tf->r0 = ret;
        }
    }
\end{lstlisting}

ソースコード \ref{sys_read} は CbC で書き換えた read システムコールである。
Code Gear であるため関数呼び出しではなく goto による継続となる。

\begin{lstlisting}[frame=lrbt,label=sys_read,caption={\footnotesize read システムコール}]
__code cbc_read(__code (*next)(int ret)){
    struct file *f;
    int n;
    char *p;

    if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) {
        goto next(-1);
    }
    goto cbc_fileread(f, p, n, next);
}

int sys_read(void)
{   
    struct file *f;
    int n;
    char *p;
    
    if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) {
        return -1;
    }
    
    return fileread(f, p, n);
}
\end{lstlisting}

継続で Code Gear 間を遷移するため関数呼び出しとは違い元の関数には戻ってこない。
このため、書き換えの際には ソースコード \ref{fileread} のように分割する必要がある。
プロセスの状態を持つ struct proc は大域変数であるため Code Gear を用いるために必要なパラメーターを cbc\_arg として持たせることにした。
継続を行う際には必要なパラメーターをここに格納する。

\lstinputlisting[label=fileread, caption=fileread の CbC 書き換えの例]{./src/fileread.c}

CbC では cbc\_devsw を定義しておりソースコード \ref{readi} 11行目で次の Code Gear へと継続する。

\lstinputlisting[label=readi, caption=readi の CbC 書き換えの例]{./src/readi.c}



\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 による継続で行われるため、
状態遷移ベースでのプログラムに適している。
xv6 を CbC で書き換えることにより、OS のプログラムを状態遷移モデルに落とし込むことができる。
これにより状態遷移系のモデル検査が可能となる。

また、CbC は Agda に変換できるように設計されているため CbC で記述された実行可能なプログラムが、
そのまま Agda による定理証明ができる。

これらのため、CbC で記述された実行可能な OS そのものがモデル検査と定理証明が可能となり、
OS の信頼性が保証できる。