|
10
|
1 %%
|
|
|
2 %% 研究報告用スイッチ
|
|
|
3 %% [techrep]
|
|
|
4 %%
|
|
|
5 %% 欧文表記無しのスイッチ(etitle,eabstractは任意)
|
|
|
6 %% [noauthor]
|
|
|
7 %%
|
|
|
8
|
|
|
9 %\documentclass[submit,techrep]{ipsj}
|
|
|
10 \documentclass[submit,techrep,noauthor]{ipsj}
|
|
|
11
|
|
|
12
|
|
|
13
|
|
23
|
14 \usepackage[dvips,dvipdfmx]{graphicx}
|
|
10
|
15 \usepackage{latexsym}
|
|
14
|
16 \usepackage{listings}
|
|
|
17 \lstset{
|
|
|
18 language=C,
|
|
|
19 tabsize=2,
|
|
|
20 frame=single,
|
|
|
21 basicstyle={\tt\footnotesize}, %
|
|
|
22 identifierstyle={\footnotesize}, %
|
|
|
23 commentstyle={\footnotesize\itshape}, %
|
|
|
24 keywordstyle={\footnotesize\ttfamily}, %
|
|
|
25 ndkeywordstyle={\footnotesize\ttfamily}, %
|
|
|
26 stringstyle={\footnotesize\ttfamily},
|
|
|
27 breaklines=true,
|
|
|
28 captionpos=b,
|
|
|
29 columns=[l]{fullflexible}, %
|
|
|
30 xrightmargin=0zw, %
|
|
|
31 xleftmargin=1zw, %
|
|
|
32 aboveskip=1zw,
|
|
|
33 numberstyle={\scriptsize}, %
|
|
|
34 stepnumber=1,
|
|
|
35 numbersep=0.5zw, %
|
|
|
36 lineskip=-0.5ex,
|
|
|
37 }
|
|
|
38 \usepackage{caption}
|
|
|
39
|
|
10
|
40
|
|
|
41 \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
|
|
|
42 \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
|
|
|
43 \def\|{\verb|}
|
|
|
44 %
|
|
|
45
|
|
|
46 %\setcounter{巻数}{59}%vol59=2018
|
|
|
47 %\setcounter{号数}{10}
|
|
|
48 %\setcounter{page}{1}
|
|
14
|
49 \renewcommand{\lstlistingname}{Code}
|
|
10
|
50
|
|
|
51 \begin{document}
|
|
|
52
|
|
|
53
|
|
|
54 \title{xv6の構成要素の継続の分析}
|
|
|
55
|
|
|
56 %\etitle{How to Prepare Your Paper for IPSJ SIG Technical Report \\ (version 2018/10/29)}
|
|
|
57
|
|
|
58 \affiliate{KIE}{琉球大学大学院理工学研究科情報工学専攻}
|
|
|
59 \affiliate{IE}{琉球大学工学部工学科知能情報コース}
|
|
|
60
|
|
|
61
|
|
|
62 \author{清水 隆博}{Shimizu Takahiro}{KIE}[anatofuz@cr.ie.u-ryukyu.ac.jp]
|
|
|
63 \author{河野 真治}{Shinji Kono}{IE}[kono@ie.u-ryukyu.ac.jp]
|
|
|
64
|
|
|
65 \begin{abstract}
|
|
|
66 OS自体そのものは高い信頼性が求められるが、 OSを構成するすべての処理をテストするのは困難である。
|
|
|
67 テストを利用して信頼性を高めるのではなく、 OSの状態を状態遷移を基本としたモデルに変換し形式手法を用いて信頼性を高めたい。
|
|
|
68
|
|
|
69 状態遷移単位での記述に適した言語であるCbCを用いて、小さなunixであるxv6 kernelの書き換えを行っている。
|
|
|
70 このためには現状のxv6 kernelの処理がどのような状態遷移を行うのかを分析し、継続ベースでのプログラミングに変換していく必要がある。
|
|
|
71 本稿ではxv6kernelの構成要素の一部に着目し、状態遷移系の分析と状態遷移系を元に継続ベースでxv6の再実装を行う。
|
|
|
72 \end{abstract}
|
|
|
73
|
|
|
74
|
|
|
75 \maketitle
|
|
|
76
|
|
|
77 \section{OSの信頼性}
|
|
|
78 様々なアプリケーションはOSの上で動作するのが当たり前になってきた。
|
|
|
79 アプリケーションの信頼性を向上させるのはもとより、 土台となるOS自体の信頼性は高く保証されていなければならない。
|
|
|
80 OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。
|
|
|
81 しかし並列並行処理などに起因する動かしてみないと発見できないバグなどが存在するため、 テストで完全にバグを発見するのは困難である。
|
|
|
82 また、OSを構成する処理も巨大であるため、 これら全てをテスト仕切るのも困難である。
|
|
|
83 テスト以外の方法でOSの信頼性を高めたい。
|
|
|
84
|
|
|
85 数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
|
|
|
86 OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。
|
|
|
87 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。
|
|
|
88 これに適した形として、 状態遷移モデルが挙げられる。
|
|
|
89 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。
|
|
22
|
90 既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析し、仕様記述言語などによる再実装が必要となる。
|
|
|
91 しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。
|
|
10
|
92 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。
|
|
|
93
|
|
21
|
94 さらに本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理も行う必要がある。
|
|
|
95 本来計算機で実行したい計算に必要な計算をメタ計算と呼び、 意図して行いたい処理をノーマルレベルの計算と呼ぶ。
|
|
|
96 ノーマルレベル上での問題点をメタ計算上で発見し信頼性を向上させたい。
|
|
|
97 プログラマからはノーマルレベルの計算のみ実装するが、整合性の確認や拡張を行う際にノーマルレベルと同様の記述力でメタ計算も実装できる必要がある。
|
|
|
98
|
|
|
99 ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。
|
|
12
|
100 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
|
|
|
101 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
|
|
15
|
102 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
|
|
12
|
103 すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。
|
|
|
104
|
|
|
105 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。
|
|
|
106 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。
|
|
|
107 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。
|
|
|
108
|
|
10
|
109
|
|
13
|
110
|
|
|
111 \section{Continuation Based C}
|
|
|
112
|
|
|
113 Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。
|
|
17
|
114 CbCでは通常の関数呼び出しの他に、 関数呼び出し時のスタックの操作を行わず、次のコードブロックに\texttt{jmp}命令で移動する継続が導入されている。
|
|
13
|
115 この継続はSchemeなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である為に軽量である事から軽量継続と呼べる。
|
|
17
|
116 またCbCではこの軽量継続を用いた再帰呼び出しを利用することで\texttt{for}文などのループ文を廃し、 関数型プログラミングに近いスタイルでプログラミングが可能となる。
|
|
13
|
117 現在CbCはGCC及びLLVM/clang上にそれぞれ実装されている。
|
|
|
118
|
|
14
|
119
|
|
17
|
120 CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。
|
|
|
121 CodeGearは通常のCの関数宣言の返り値の型の代わりに\texttt{\_\_code}で宣言を行う。
|
|
|
122
|
|
15
|
123 CbCで階乗を求める例題をCode \ref{src:cbc_example}に示す。
|
|
17
|
124 例題ではCodeGearとして\texttt{factorial}を宣言している。
|
|
18
|
125 \texttt{factorial}はCodeGearの引数として\texttt{struct F}型の変数\texttt{arg}を受け取り、\texttt{arg}のメンバー変数によって\texttt{factorial}の再帰呼び出しを行う。
|
|
|
126 \texttt{arg}の様なCodeGearの引数のことを\texttt{DataGear}と呼ぶ。
|
|
17
|
127 CodeGearの呼び出しは\texttt{goto}文によって行われる。
|
|
14
|
128
|
|
|
129
|
|
18
|
130 \begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={CbCで階乗を求める処理}]
|
|
15
|
131 __code factorial(struct F arg) {
|
|
|
132 if (arg.n<0) {
|
|
|
133 exit(1);
|
|
|
134 }
|
|
|
135 if (arg.n==0) {
|
|
|
136 goto arg.next(arg);
|
|
|
137 } else {
|
|
|
138 arg.r *= arg.n;
|
|
|
139 arg.n--;
|
|
|
140 goto factorial(arg);
|
|
14
|
141 }
|
|
|
142 }
|
|
15
|
143 \end{lstlisting}
|
|
14
|
144
|
|
17
|
145 CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。
|
|
|
146 しかしCodeGearを呼び出す直前のスタックは保存されるため、 部分的にCbCを適用する場合はCodeGearを呼び出す\texttt{void}型などの関数を経由することで呼び出しが可能となる。
|
|
|
147
|
|
|
148 この他にCbCからCへ復帰する為のAPIとして、 環境付きgotoという機能がある。
|
|
18
|
149 これはGCCでは内部コードを生成、 LLVM/clangでは\texttt{setjmp}と\texttt{longjmp}を使うことでCodeGearの次の継続対象として呼び出し元の関数を設定することが可能となる。
|
|
17
|
150 したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。
|
|
|
151
|
|
20
|
152 \section{CbCを用いたOSの実装}
|
|
|
153
|
|
|
154 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。
|
|
|
155 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
|
|
|
156 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
|
|
22
|
157 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。
|
|
|
158 CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。
|
|
|
159
|
|
|
160 GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。
|
|
21
|
161 遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。
|
|
22
|
162 このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。
|
|
23
|
163
|
|
|
164 各CodeGearの入出力や、各CodeGearそのものの関数ポインタなどは、関数型プログラミングの側面から見るとプログラマが直接操作するのを禁じる必要がある。
|
|
|
165 このためにGearsOSには実行する処理に必要なCodeGear及びDataGearを管理する、 contextというMetaDataGearが存在する。
|
|
|
166 コード上では別のCodeGearに直接遷移している様に見えるが、 実際はContext内の遷移先のCodeGearに対応するスロットから、対応するMetaCodeGearに遷移する。
|
|
|
167 これらの変換はPerlスクリプトによって、 GearsOSのビルド時に静的に行われる。
|
|
18
|
168
|
|
22
|
169 \section{xv6 kernel}
|
|
|
170
|
|
|
171 xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。
|
|
|
172 xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。
|
|
|
173 Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。
|
|
|
174 本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。
|
|
|
175
|
|
|
176 xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。
|
|
|
177 またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。
|
|
|
178
|
|
|
179 本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。
|
|
|
180 xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。
|
|
|
181
|
|
18
|
182
|
|
15
|
183 \section{xv6のファイルシステムの一部の分析}
|
|
|
184
|
|
|
185 xv6のファイルシステムに関する定義ファイルはfs.c中に記述されている。
|
|
|
186 この中に出てくる関数に着目し、 この関数をさらにCodeGearに変換していくことで状態遷移単位での記述を試みた。
|
|
|
187
|
|
|
188 まず関数内でif文などの分岐を持たない基本単位であるBasic Blockに着目した。
|
|
|
189 CbCのCodeGearの粒度はCの関数とアセンブラの中間であるといえるので、 BasicBlockをCodeGearに置き換える事が可能である。
|
|
17
|
190 したがって特定の関数内の処理のBasicBlockを分析し、 BasicBlockに対応したCodeGearへ変換することで状態遷移系への変換を行った。
|
|
15
|
191
|
|
|
192
|
|
23
|
193 \begin{figure}[tb]
|
|
|
194 \begin{center}
|
|
|
195 \includegraphics[width=70mm]{./fig/meta-cg-dg.pdf}
|
|
|
196 \end{center}
|
|
|
197 \caption{perl}
|
|
|
198 \label{perf}
|
|
|
199 \end{figure}
|
|
14
|
200
|
|
10
|
201 \nocite{*}
|
|
|
202 \bibliographystyle{ipsjunsrt}
|
|
|
203 \bibliography{anatofuz-bib}
|
|
|
204
|
|
|
205
|
|
|
206 \end{document}
|
