Mercurial > hg > Papers > 2020 > anatofuz-sigos

comparison paper/anatofuz-sigos.tex @ 48:567288b8a89e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Thu, 07 May 2020 19:04:11 +0900
parents 667ae17b169e
children 72805ecaa331
comparison
equal deleted inserted replaced
47:49940c327b4e 48:567288b8a89e
81 OSそのものも巨大なプログラムであるため、テストコードを用いた方法で信頼性を確保する事が可能である。 81 OSそのものも巨大なプログラムであるため、テストコードを用いた方法で信頼性を確保する事が可能である。
82 しかし並列並行処理などに起因するバグや、そもそもOSを構成する処理が巨大であることから、 テストで完全にバグを発見するのは困難である。 82 しかし並列並行処理などに起因するバグや、そもそもOSを構成する処理が巨大であることから、 テストで完全にバグを発見するのは困難である。
83 テスト以外の方法でOSの信頼性を高めたい。 83 テスト以外の方法でOSの信頼性を高めたい。
84 84
85 そこで数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。 85 そこで数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
86 OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、Agda定理証明支援系\cite{}を利用した証明ベースでの信頼性の確保などの手法が考えられる。 86 OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、定理証明支援系Agda\cite{agda}を利用した証明ベースでの信頼性の確保などの手法が考えられる。\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}
87 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。 87 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。\cite{hyperKernel}
88 % これに適した形として、 状態遷移モデルが挙げられる。
89 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。 88 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。
90 % 既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析し、仕様記述言語などによる再実装が必要となる。
91 しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。 89 しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。
92 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。 90 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。
93 91
94 OS上のアプリケーションには本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理がある。 92 OS上のアプリケーションには本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理がある。
95 前者をノーマルレベルの計算と呼び、後者をメタ計算と呼ぶ。 93 前者をノーマルレベルの計算と呼び、後者をメタ計算と呼ぶ。
96 OSはメタ計算を担当していると言える。 94 OSはメタ計算を担当していると言える。
97 実装のソースコードはノーマルレベルであり検証用のソースコードはメタ計算だと考えると、OSそのものが 95 実装のソースコードはノーマルレベルであり検証用のソースコードはメタ計算だと考えると、OSそのものが
98 検証を行ない、システム全体の信頼を高める機能を持つべきだと考える。 96 検証を行ない、システム全体の信頼を高める機能を持つべきだと考える。
99 ノーマルレベル上でのバグを例えばモデル検査のようなメタ計算によって発見し信頼性を向上させたい。 97 ノーマルレベル上でのバグを例えばモデル検査のようなメタ計算によって発見し信頼性を向上させたい。
100 % プログラマからはノーマルレベルの計算のみ実装するが、整合性の確認や拡張を行う際にノーマルレベルと同様の記述力でメタ計算も実装できる必要がある。
101 98
102 ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。 99 ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。
103 CbCは基本 goto で CodeGaar というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と 100 CbCは基本\texttt{goto}で\texttt{CodeGaar}というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と
104 呼ばれる隠れた状態を持たない。このため、計算のための情報は CodeGearの入力にすべてそろっている。そのうちのいくつかはメタ計算、 101 呼ばれる隠れた状態を持たない。このため、計算のための情報は\texttt{CodeGear}の入力にすべてそろっている。そのうちのいくつかはメタ計算、
105 つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(DataGear)である。メタ計算とノーマルレベルの 102 つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(DataGear)である。メタ計算とノーマルレベルの
106 区別は入力のどこを扱うかの差に帰着される。 103 区別は入力のどこを扱うかの差に帰着される。
107 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。 104 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
108 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。 105 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
109 CbCは GCC \cite{}あるいは LLVM \cite{}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。 106 CbCは\texttt{GCC}\cite{gcc}\cite{weko_82695_1}あるいは\texttt{LLVM}\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。
110 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。 107 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{agda-ryokka}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
111 % すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。
112 108
113 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。 109 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。
114 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。 110 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。
115 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。 111 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。
116 112
138 \end{center} 134 \end{center}
139 \caption{CodeGearと入出力の関係図} 135 \caption{CodeGearと入出力の関係図}
140 \label{fig:cgdg} 136 \label{fig:cgdg}
141 \end{figure} 137 \end{figure}
142 138
143 CbCで階乗を求める例題をCode \ref{src:cbc_example}に示す。 139 CbCを利用したシステムコールのディスパッチ部分をCode \ref{src:cbc_example}に示す。
144 例題ではCodeGearとして\texttt{factorial}を宣言している。 140 この例題では特定のシステムコールの場合、 CbCで実装された処理に\texttt{goto}文をつかって継続する。
145 \texttt{factorial}はCodeGearの引数として\texttt{struct F}型の変数\texttt{arg}を受け取り、\texttt{arg}のメンバー変数によって\texttt{factorial}の再帰呼び出しを行う。 141 例題ではCodeGearへのアドレスが配列\texttt{cbccodes}に格納されている。
146 CodeGearの呼び出しは\texttt{goto}文によって行われる。 142 引数として渡している\texttt{cbc\_ret}は、 システムコールの返り値の数値をレジスタに代入するCodeGearである。
147 この例題を状態遷移図にしたものを図\ref{fig:factorial_cbc}に示す。 143
148 図中の四角がDataGear、 円がCodeGearに対応する。 144 \begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={CbCを利用したシステムコールのディスパッチ}]
149 145 void syscall(void)
150 146 {
151 \begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={CbCで階乗を求める例題}] 147 int num;
152 __code factorial(struct F arg) { 148 int ret;
153 if (arg.n<0) { 149
154 exit(1); 150 if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) {
151 proc->cbc_arg.cbc_console_arg.num = num;
152 goto (cbccodes[num])(cbc_ret);
155 } 153 }
156 if (arg.n==0) {
157 goto arg.next(arg);
158 } else {
159 arg.r *= arg.n;
160 arg.n--;
161 goto factorial(arg);
162 }
163 }
164 \end{lstlisting} 154 \end{lstlisting}
165 155
166 \begin{figure}[tb] 156 \begin{figure}[tb]
167 \begin{center} 157 \begin{center}
168 \includegraphics[width=80mm]{fig/factorial_cbc.pdf} 158 \includegraphics[width=80mm]{fig/cbc_syscall_Trap}
169 \end{center} 159 \end{center}
170 \caption{CbCで階乗を求める例題の状態遷移} 160 \caption{CbCを利用したシステムコールディスパッチの状態遷移}
171 \label{fig:factorial_cbc} 161 \label{fig:factorial_cbc}
172 \end{figure} 162 \end{figure}
173 163
174 CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。 164 CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。
175 しかしCodeGearを呼び出す直前のスタックは保存されるため、 部分的にCbCを適用する場合はCodeGearを呼び出す\texttt{void}型などの関数を経由することで呼び出しが可能となる。 165 しかしCodeGearを呼び出す直前のスタックは保存されるため、 部分的にCbCを適用する場合はCodeGearを呼び出す\texttt{void}型などの関数を経由することで呼び出しが可能となる。
182 172
183 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。 173 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。
184 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。 174 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
185 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。 175 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
186 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。 176 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。
187 CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。 177 CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。\cite{gears}
188 現在のGearsOSは並列フレームワークとして実装されており、 実用的なOSのプロトタイプ実装として既存のOS上への実装を目指している。 178 現在のGearsOSは並列フレームワークとして実装されており、 実用的なOSのプロトタイプ実装として既存のOS上への実装を目指している。
189 179
190 GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。 180 GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。
191 遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。 181 遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。
192 このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。 182 このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。
223 MetaCodeGear中で、次に実行するCodeGearで必要なDataGearをcontextから取り出し、 実際の計算が行われる。 213 MetaCodeGear中で、次に実行するCodeGearで必要なDataGearをcontextから取り出し、 実際の計算が行われる。
224 214
225 215
226 \section{xv6 kernel} 216 \section{xv6 kernel}
227 217
228 xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。 218 xv6とはマサチューセッツ工科大学でv6 OS\cite{lions1996lions}を元に開発された教育用のUNIX OSである。\cite{xv6}
229 xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。 219 xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。
230 Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。 220 Raspberry Pi\cite{rpi}上での動作を目的としたARMアーキテクチャのバージョンも存在する。\cite{xv6rpi}
231 本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。 221 本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。
232 222
233 xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。 223 xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。
234 またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。 224 またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。
235 225
237 xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。 227 xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。
238 228
239 本論文ではxv6の継続の分析をシステムコール部分とファイルシステム、 仮想メモリなどのOSの根幹部分でそれぞれ行った。 229 本論文ではxv6の継続の分析をシステムコール部分とファイルシステム、 仮想メモリなどのOSの根幹部分でそれぞれ行った。
240 230
241 231
242 \section{xv6のシステムコールの継続の分析} 232 \section{xv6のシステムコールの継続の分析と書き換え}
243 xv6の処理を継続を中心とした記述で再実装を行う。 233 xv6の処理を継続を中心とした記述で再実装を行う。
244 この際に、 xv6のどの処理に着目するかによって継続の実装が異なっていくことが実装につれてわかった。 234 この際に、 xv6のどの処理に着目するかによって継続の実装が異なっていくことが実装につれてわかった。
245 235
246 まずxv6の\texttt{read} システムコールに着目し、 システムコール内部でどのような状態を遷移するかを分析した。 236 まずxv6の\texttt{read} システムコールに着目し、 システムコール内部でどのような状態を遷移するかを分析した。 \cite{weko_195888_1}
247 分析結果をCbCのCodeGearに変換し、 状態遷移図におこしたものを図\ref{fig:cbc_readsyscall}に示す。 237 分析結果をCbCのCodeGearに変換し、 状態遷移図におこしたものを図\ref{fig:cbc_readsyscall}に示す。
248 238
249 \begin{figure}[tb] 239 \begin{figure}[tb]
250 \begin{center} 240 \begin{center}
251 \includegraphics[width=80mm]{fig/readsyscall_state.pdf} 241 \includegraphics[width=80mm]{fig/readsyscall.pdf}
252 \end{center} 242 \end{center}
253 \caption{readシステムコールの状態遷移} 243 \caption{readシステムコールの状態遷移}
254 \label{fig:cbc_readsyscall} 244 \label{fig:cbc_readsyscall}
255 \end{figure} 245 \end{figure}
256 246
310 bp = bread(dev, IBLOCK(inum)); 300 bp = bread(dev, IBLOCK(inum));
311 dip = (struct dinode*) bp->data + inum % IPB; 301 dip = (struct dinode*) bp->data + inum % IPB;
312 302
313 if (dip->type == 0) { // a free inode 303 if (dip->type == 0) { // a free inode
314 memset(dip, 0, sizeof(*dip)); 304 memset(dip, 0, sizeof(*dip));
315 // omission 305 ...
316 return iget(dev, inum); 306 return iget(dev, inum);
317 } 307 }
318 brelse(bp); 308 brelse(bp);
319 } 309 }
320 panic("ialloc: no inodes"); 310 panic("ialloc: no inodes");
335 goto err->panic(msg); 325 goto err->panic(msg);
336 } 326 }
337 \end{lstlisting} 327 \end{lstlisting}
338 328
339 Code\ref{src:allocinode_loopcheck}ではループ条件の成立を\texttt{if}文で確認し、ループ処理に移行する場合は \texttt{allocinode\_loop}へ遷移する。 329 Code\ref{src:allocinode_loopcheck}ではループ条件の成立を\texttt{if}文で確認し、ループ処理に移行する場合は \texttt{allocinode\_loop}へ遷移する。
330 \texttt{goto}文の中の引数の1つ\texttt{next(...)} は、 APIとして呼び出した\texttt{ialloc}の次の継続のCodeGearに対して、 \texttt{context}などの環境を渡す構文である。
340 ループ条件が満たされなかった場合は、 コンテキストから\texttt{panic}に関するCodeGearの集合を取り出し、 集合中の\texttt{panic} CodeGearへと遷移する。 331 ループ条件が満たされなかった場合は、 コンテキストから\texttt{panic}に関するCodeGearの集合を取り出し、 集合中の\texttt{panic} CodeGearへと遷移する。
341 オリジナルの処理では、　ループ中に\texttt{dip->type == 0}が満たされた場合は関数から\texttt{return}文により関数から復帰する。 332 オリジナルの処理では、 ループ中に\texttt{dip->type == 0}が満たされた場合は関数から\texttt{return}文により関数から復帰する。
342 CodeGearではCode\ref{src:alloc_loop}内で、 状態が分けられる。 333 CodeGearではCode\ref{src:alloc_loop}内で、 状態が分けられる。
343 この先の継続は、　復帰用のCodeGearかループの先頭である\texttt{allocinode\_loopcheck}に再帰的に遷移するかになる。 334 この先の継続は、　復帰用のCodeGearかループの先頭である\texttt{allocinode\_loopcheck}に再帰的に遷移するかになる。
344 335
345 \begin{lstlisting}[frame=lrbt,label=src:alloc_loop,caption={ループ中に復帰するかどうかの確認をするCodeGear}] 336 \begin{lstlisting}[frame=lrbt,label=src:alloc_loop,caption={ループ中に復帰するかどうかの確認をするCodeGear}]
346 __code allocinode_loop(struct fs_impl* fs_impl, uint inum, uint dev, short type, struct superblock* sb, struct buf* bp, struct dinode* dip, __code next(...)){ 337 __code allocinode_loop(struct fs_impl* fs_impl, uint inum, uint dev, short type, struct superblock* sb, struct buf* bp, struct dinode* dip, __code next(...)){
388 goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret); 379 goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret);
389 } 380 }
390 381
391 void userinit(void) 382 void userinit(void)
392 { 383 {
393 // omission 384 ...
394 385
395 if((p->pgdir = kpt_alloc()) == NULL) { 386 if((p->pgdir = kpt_alloc()) == NULL) {
396 panic("userinit: out of memory?"); 387 panic("userinit: out of memory?");
397 } 388 }
398 389
399 cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size); 390 cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
400 391
401 p->sz = PTE_SZ; 392 p->sz = PTE_SZ;
402 memset(p->tf, 0, sizeof(*p->tf)); 393 memset(p->tf, 0, sizeof(*p->tf));
403 // omission 394 ...
404 } 395 }
405 \end{lstlisting} 396 \end{lstlisting}
406 397
407 Code\ref{src:dumy_function_cbc}中で、 CodeGearへの遷移が行われる\texttt{goto vm->init\_vmm()}の\texttt{vm->void\_ret}は\texttt{init\_vmm}の次の継続のCodeGear名である。 398 Code\ref{src:dumy_function_cbc}中で、 CodeGearへの遷移が行われる\texttt{goto vm->init\_vmm()}の\texttt{vm->void\_ret}は\texttt{init\_vmm}の次の継続のCodeGear名である。
408 この\texttt{vm->void\_ret}は\texttt{return}するのみのCodeGearであり、 void型関数と組み合わせることで呼び出し元へと復帰する事が可能となる。 399 この\texttt{vm->void\_ret}は\texttt{return}するのみのCodeGearであり、 void型関数と組み合わせることで呼び出し元へと復帰する事が可能となる。