|
11
|
1 \chapter{xv6 の CbC への書き換え}
|
|
48
|
2 xv6 は 2006 年に MIT のオペレーティングシステムコースで教育用の目的として開発されたオペレーティングシステムである。
|
|
|
3 xv6 はプロセス、仮想メモリ、カーネルとユーザの分離、割り込み、
|
|
|
4 ファイルシステムなどの基本的な Unix の構造を持つにも関わらず、
|
|
31
|
5 シンプルで学習しやすい。
|
|
|
6
|
|
48
|
7 CbC は 継続を中心とした言語であるため状態遷移モデルに落とし込むことができる。
|
|
|
8 xv6 を CbC で書き換えることにより、OS の機能の保証が可能となる。
|
|
|
9
|
|
|
10 また、ハードウェア上でのメタレベルの計算や並列実行を行いたい。
|
|
49
|
11 このため、xv6 を ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである Raspberry pi 用に移植した xv6-rpi を用いて実装する。
|
|
48
|
12
|
|
|
13 \section{xv6 のモジュール化}
|
|
41
|
14
|
|
48
|
15 xv6 全体を CbC で書き換えるためには Interface を用いてモジュール化する必要がある。
|
|
|
16 xv6 をモジュール化し、CbC で書き換えることができれば、Gears OS の機能を置き換えることもできる。
|
|
|
17 図 \ref{fig:xv6Interface} は xv6 の構成図となる。
|
|
|
18
|
|
|
19 \begin{figure}[ht]
|
|
|
20 \begin{center}
|
|
|
21 \includegraphics[width=150mm]{fig/xv6.pdf}
|
|
|
22 \end{center}
|
|
|
23 \caption{モジュール化した xv6 の構成}
|
|
|
24 \label{fig:xv6Interface}
|
|
|
25 \end{figure}
|
|
|
26
|
|
40
|
27
|
|
33
|
28 \section{xv6 の構成要素}
|
|
31
|
29 xv6 はカーネルと呼ばれる形式をとっている。
|
|
|
30 カーネルは OS にとって中核となるプログラムである。
|
|
|
31 xv6 ではカーネルとユーザープログラムは分離されており、カーネルはプログラムにプロセス管理、メモリ管理、I/O やファイルの管理などのサービスを提供する。
|
|
|
32 ユーザープログラムがカーネルのサービスを呼び出す場合、システムコールを用いてユーザー空間からカーネル空間へ入りサービスを実行する。
|
|
|
33 カーネルは CPU のハードウェア保護機構を使用して、ユーザー空間で実行されているプロセスが自身のメモリのみアクセスできるように保護している。
|
|
|
34 ユーザープログラムがシステムコールを呼び出すと、ハードウェアが特権レベルを上げ、カーネルのプログラムが実行される。
|
|
|
35 この特権レベルを持つプロセッサの状態をカーネルモード、特権のない状態をユーザーモードという。
|
|
|
36
|
|
34
|
37 \subsection{システムコール}
|
|
|
38
|
|
|
39 ユーザープログラムがカーネルの提供するサービスを呼び出す際にはシステムコールを用いる。
|
|
|
40 ユーザープログラムがシステムコールを呼び出すと、トラップが発生する。
|
|
|
41 トラップが発生すると、ユーザープログラムは中断され、カーネルに切り替わり処理を行う。
|
|
35
|
42 ソースコード \ref{syscall_list} は xv6 のシステムコールのリストである。
|
|
34
|
43
|
|
35
|
44 \begin{lstlisting}[frame=lrbt,label=syscall_list,caption={\footnotesize xv6 のシステムコールのリスト}]
|
|
34
|
45 static int (*syscalls[])(void) = {
|
|
|
46 [SYS_fork] =sys_fork,
|
|
|
47 [SYS_exit] =sys_exit,
|
|
|
48 [SYS_wait] =sys_wait,
|
|
|
49 [SYS_pipe] =sys_pipe,
|
|
|
50 [SYS_read] =sys_read,
|
|
|
51 [SYS_kill] =sys_kill,
|
|
|
52 [SYS_exec] =sys_exec,
|
|
|
53 [SYS_fstat] =sys_fstat,
|
|
|
54 [SYS_chdir] =sys_chdir,
|
|
|
55 [SYS_dup] =sys_dup,
|
|
|
56 [SYS_getpid] =sys_getpid,
|
|
|
57 [SYS_sbrk] =sys_sbrk,
|
|
|
58 [SYS_sleep] =sys_sleep,
|
|
|
59 [SYS_uptime] =sys_uptime,
|
|
|
60 [SYS_open] =sys_open,
|
|
|
61 [SYS_write] =sys_write,
|
|
|
62 [SYS_mknod] =sys_mknod,
|
|
|
63 [SYS_unlink] =sys_unlink,
|
|
|
64 [SYS_link] =sys_link,
|
|
|
65 [SYS_mkdir] =sys_mkdir,
|
|
|
66 [SYS_close] =sys_close,
|
|
|
67 };
|
|
|
68 \end{lstlisting}
|
|
|
69
|
|
33
|
70 \subsection{プロセス}
|
|
31
|
71 プロセスとは、カーネルが実行するプログラムの単位である。
|
|
|
72 xv6 のプロセスは、ユーザー空間メモリとカーネル用のプロセスの状態を持つ空間で構成されている。
|
|
|
73 プロセスは独立しており、他のプロセスからメモリを破壊されたりすることはない。
|
|
|
74 また、独立していることでカーネルそのものを破壊することもない。
|
|
|
75 各プロセスの状態は struct proc によって管理されている。
|
|
|
76 プロセスは fork システムコールによって新たに生成される。
|
|
|
77 fork は新しく、親プロセスと呼ばれる呼び出し側と同じメモリ内容の、子プロセスと呼ばれるプロセスを生成する。
|
|
|
78 fork システムコールは、親プロセスであれば子プロセスのID、子プロセスであれば 0 を返す。
|
|
|
79 親プロセスと子プロセスは最初は同じ内容を持っているが、それぞれ異なるメモリ、レジスタで実行されているため、片方のメモリ内容を変更してももう片方に影響はない。
|
|
|
80 exit システムコールはプロセスの停止を行い、メモリを解放する。
|
|
|
81 wait システムコールは終了した子プロセスのIDを返す。子プロセスが終了するまで待つ。
|
|
|
82 exec システムコールは呼び出し元のプロセスのメモリをファイルシステムのファイルのメモリイメージと置き換え実行する。
|
|
|
83 ファイルには命令、データなどの配置が指定されたフォーマット通りになっていなければならない。
|
|
|
84 xv6 は ELF と呼ばれるフォーマットを扱う。
|
|
|
85
|
|
33
|
86 \subsection{ファイルディスクリプタ}
|
|
31
|
87 ファイルディスクリプタは、カーネルが管理するプロセスが読み書きを行うオブジェクトを表す整数値である。
|
|
|
88 プロセスは、ファイル、ディレクトリ、デバイスを開く、または既存のディスクリプタを複製することによって、
|
|
|
89 ファイルディスクリプタを取得する。
|
|
33
|
90 xv6 はプロセス毎にファイルディスクリプタのテーブルを持っている。
|
|
|
91 ファイルディスクリプタは普通、0 が標準入力、1 が標準出力、2 がエラー出力として使われる。
|
|
|
92 ファイルディスクリプタのテーブルのエントリを変更することで入出力先を変更することができる。
|
|
|
93 1 の標準出力を close し、ファイルを open することでプログラムはファイルに出力することになる。
|
|
|
94 ファイルディスクリプタはファイルがどのように接続するか隠すことでファイルへの入出力を容易にしている。
|
|
|
95
|
|
|
96 \subsection{ファイルシステム}
|
|
|
97 xv6 のファイルシステムはバイト配列であるデータファイルとデータファイルおよび他のディレクトリの参照を含むディレクトリを提供する。
|
|
|
98 ディレクトリは root と呼ばれる特別なディレクトリから始まるツリーを形成している。
|
|
|
99 絶対パスである "/dir1/dir2/file1" というパスは root ディレクトリ内の dir1 という名前のディレクトリ内の dir2 という名前のディレクトリ内の file というデータファイルを指す。
|
|
|
100 相対パスである "dir2/file2" のようなパスは、現在のディレクトリ内の dir2 という名前のディレクトリ内の file というデータファイルを指す。
|
|
|
101
|
|
14
|
102 \section{xv6-rpi の CbC 対応}
|
|
11
|
103
|
|
35
|
104 オリジナルの xv6 は x86 アーキテクチャで実装されたものだが、xv6-rpi は Raspberry Pi 用に実装されたものである。
|
|
11
|
105
|
|
|
106 xv6-rpi を CbC で書き換えるために、
|
|
35
|
107 GCC 上で実装した CbC コンパイラを ARM 向けに build し xv6-rpi をコンパイルした。
|
|
|
108 これにより、 xv6-rpi を CbC で書き換えることができるようになった。
|
|
|
109
|
|
36
|
110 \section{システムコールの書き換え}
|
|
35
|
111 ソースコード \ref{syscall} は syscall() におけるシステムコールの呼び出しを行うコードである。
|
|
49
|
112 システムコールはソースコード \ref{syscall_list} の関数のリストの番号から呼び出される。
|
|
35
|
113 CbC でも同様に num で指定された番号の cbccodes のリストの Code Gear へ goto する。
|
|
49
|
114 ソースコード \ref{syscall} 6行目でトラップフレームからシステムコールの番号を取得する。
|
|
|
115 通常のシステムコールであればソースコード \ref{syscall} 13行目からの分岐へ入るが、
|
|
|
116 cbc システムコールであれば ソースコード \ref{syscall} 8行目へ入り、goto によって遷移する。
|
|
35
|
117 引数に持つ cbc\_ret は 継続した先でトラップに戻ってくるための Code Gear である。
|
|
|
118
|
|
49
|
119
|
|
35
|
120 \begin{lstlisting}[frame=lrbt,label=syscall,caption={\footnotesize syscall()}]
|
|
49
|
121 void syscall(void)
|
|
|
122 {
|
|
|
123 int num;
|
|
|
124 int ret;
|
|
|
125
|
|
|
126 num = proc->tf->r0;
|
|
|
127
|
|
35
|
128 if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) {
|
|
|
129 proc->cbc_arg.cbc_console_arg.num = num;
|
|
|
130 goto (cbccodes[num])(cbc_ret);
|
|
|
131 }
|
|
|
132
|
|
|
133 if((num > 0) && (num <= NELEM(syscalls)) && syscalls[num]) {
|
|
|
134 ret = syscalls[num]();
|
|
|
135
|
|
|
136 // in ARM, parameters to main (argc, argv) are passed in r0 and r1
|
|
|
137 // do not set the return value if it is SYS_exec (the user program
|
|
|
138 // anyway does not expect us to return anything).
|
|
|
139 if (num != SYS_exec) {
|
|
|
140 proc->tf->r0 = ret;
|
|
|
141 }
|
|
49
|
142 } else {
|
|
|
143 cprintf("%d %s: unknown sys call %d\n", proc->pid, proc->name, num);
|
|
|
144 proc->tf->r0 = -1;
|
|
35
|
145 }
|
|
49
|
146 }
|
|
35
|
147 \end{lstlisting}
|
|
|
148
|
|
49
|
149 ソースコード \ref{cbc_read} は、
|
|
|
150 read システムコールであるソースコード \ref{sys_read} を CbC で書き換えたコードである。
|
|
|
151 CbC は C の関数を呼び出すことも出来るため、書き換えたい部分だけを書き換えることができる。
|
|
|
152 Code Gear であるため、ソースコード \ref{cbc_read} 7、9行目のように関数呼び出しではなく goto による継続となる。
|
|
37
|
153
|
|
49
|
154 \begin{lstlisting}[frame=lrbt,label=sys_read,caption={\footnotesize cbc\_read システムコール}]
|
|
37
|
155 __code cbc_read(__code (*next)(int ret)){
|
|
|
156 struct file *f;
|
|
|
157 int n;
|
|
|
158 char *p;
|
|
|
159
|
|
|
160 if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) {
|
|
|
161 goto next(-1);
|
|
|
162 }
|
|
|
163 goto cbc_fileread(f, p, n, next);
|
|
|
164 }
|
|
49
|
165 \end{lstlisting}
|
|
37
|
166
|
|
49
|
167 \begin{lstlisting}[frame=lrbt,label=sys_read,caption={\footnotesize read システムコール}]
|
|
37
|
168 int sys_read(void)
|
|
|
169 {
|
|
|
170 struct file *f;
|
|
|
171 int n;
|
|
|
172 char *p;
|
|
|
173
|
|
|
174 if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) {
|
|
|
175 return -1;
|
|
|
176 }
|
|
|
177
|
|
|
178 return fileread(f, p, n);
|
|
|
179 }
|
|
|
180 \end{lstlisting}
|
|
|
181
|
|
|
182 継続で Code Gear 間を遷移するため関数呼び出しとは違い元の関数には戻ってこない。
|
|
49
|
183 このため、書き換えの際には ソースコード \ref{cbcfileread} のように分割する必要がある。
|
|
38
|
184 プロセスの状態を持つ struct proc は大域変数であるため Code Gear を用いるために必要なパラメーターを cbc\_arg として持たせることにした。
|
|
|
185 継続を行う際には必要なパラメーターをここに格納する。
|
|
37
|
186
|
|
49
|
187 \lstinputlisting[label=cbcfileread, caption=fileread の CbC 書き換えの例]{./src/fileread.cbc}
|
|
|
188 \lstinputlisting[label=fileread, caption=書き換え前の fileread]{./src/fileread.c}
|
|
38
|
189
|
|
49
|
190 CbC では cbc\_devsw を定義しておりソースコード \ref{cbcreadi} 11行目で次の Code Gear へと継続する。
|
|
41
|
191
|
|
49
|
192 \lstinputlisting[label=cbcreadi, caption=readi の CbC 書き換えの例]{./src/readi.cbc}
|
|
45
|
193 \lstinputlisting[label=readi, caption=readi の CbC 書き換えの例]{./src/readi.c}
|
|
46
|
194
|
|
48
|
195 ソースコード \ref{consoleread} 11、50、行目 では sleep へ継続する際、戻るべき継続先を一緒に送ることで、
|
|
|
196 sleep から consoleread に戻ってくることができる。
|
|
46
|
197
|
|
45
|
198 \lstinputlisting[label=consoleread, caption=consoleread の CbC 書き換えの例]{./src/console.c}
|
|
41
|
199
|
|
|
200
|
|
38
|
201 xv6 のシステムコールの関数を CbC で書き換え、QEMU 上で動作させることができた。
|
|
|
202
|
|
46
|
203 \section{xv6 の CbC 書き換えによる考察}
|
|
38
|
204
|
|
41
|
205 CbC は Code Gear 間の遷移は goto による継続で行われるため、
|
|
|
206 状態遷移ベースでのプログラムに適している。
|
|
|
207 xv6 を CbC で書き換えることにより、OS のプログラムを状態遷移モデルに落とし込むことができる。
|
|
|
208 これにより状態遷移系のモデル検査が可能となる。
|
|
38
|
209
|
|
41
|
210 また、CbC は Agda に変換できるように設計されているため CbC で記述された実行可能なプログラムが、
|
|
|
211 そのまま Agda による定理証明ができる。
|
|
|
212
|
|
|
213 これらのため、CbC で記述された実行可能な OS そのものがモデル検査と定理証明が可能となり、
|
|
|
214 OS の信頼性が保証できる。
|
|
|
215
|
|
48
|
216 \section{Raspberry Pi}
|
|
|
217 Raspberry Pi は ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである。
|
|
|
218 教育用のコンピューターとして開発されたもので、低価格であり、小型であるため使い勝手が良い。
|
|
|
219 ストレージにハードディスクや SSD を使用するのではなく、SD カードを用いる。
|
|
|
220 HDMI 出力や USB ポートも備えており、開発に最適である。
|
|
|
221
|
|
|
222 Raspberry Pi には Raspberry Pi 3、Raspberry Pi 2、Raspberry Pi 1、Raspberry Pi Zero といったバージョンが存在する。
|
|
|
223
|
