Mercurial > hg > Papers > 2020 > anatofuz-sigos
annotate paper/anatofuz-sigos.tex @ 26:dfcef5f101da
...
| author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 04 May 2020 16:19:35 +0900 |
| parents | 87813fb8542c |
| children | 4fccee90e43a |
| rev | line source |
|---|---|
| 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}文によって行われる。 |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
128 この例題を状態遷移図にしたものを図\ref{fig:factorial_cbc}に示す。 |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
129 図中の四角がDataGear、 円がCodeGearに対応する。 |
| 14 | 130 |
| 131 | |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
132 \begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={CbCで階乗を求める例題}] |
| 15 | 133 __code factorial(struct F arg) { |
| 134 if (arg.n<0) { | |
| 135 exit(1); | |
| 136 } | |
| 137 if (arg.n==0) { | |
| 138 goto arg.next(arg); | |
| 139 } else { | |
| 140 arg.r *= arg.n; | |
| 141 arg.n--; | |
| 142 goto factorial(arg); | |
| 14 | 143 } |
| 144 } | |
| 15 | 145 \end{lstlisting} |
| 14 | 146 |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
147 \begin{figure}[tb] |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
148 \begin{center} |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
149 \includegraphics[width=70mm]{fig/factorial_cbc.pdf} |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
150 \end{center} |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
151 \caption{CbCで階乗を求める例題の状態遷移} |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
152 \label{fig:factorial_cbc} |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
153 \end{figure} |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
154 |
| 17 | 155 CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。 |
| 156 しかしCodeGearを呼び出す直前のスタックは保存されるため、 部分的にCbCを適用する場合はCodeGearを呼び出す\texttt{void}型などの関数を経由することで呼び出しが可能となる。 | |
| 157 | |
| 158 この他にCbCからCへ復帰する為のAPIとして、 環境付きgotoという機能がある。 | |
| 18 | 159 これはGCCでは内部コードを生成、 LLVM/clangでは\texttt{setjmp}と\texttt{longjmp}を使うことでCodeGearの次の継続対象として呼び出し元の関数を設定することが可能となる。 |
| 17 | 160 したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。 |
| 161 | |
| 20 | 162 \section{CbCを用いたOSの実装} |
| 163 | |
| 164 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。 | |
| 165 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。 | |
| 166 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。 | |
| 22 | 167 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。 |
| 168 CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。 | |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
169 現在のGearsOSは並列フレームワークとして実装されており、 実用的なOSのプロトタイプ実装として既存のOS上への実装を目指している。 |
| 22 | 170 |
| 171 GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。 | |
| 21 | 172 遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。 |
| 22 | 173 このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。 |
| 26 | 174 MetaCodeGearやMetaDataGearは、プログラマが直接実装することはなく、 現在はPerlスクリプトによってGearsOSのビルド時に生成される。 |
| 175 CodeGearから別のCodeGearに遷移する際のDataGearなどの関係性を、図\ref{meta-cg-dg}に示す。 | |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
176 |
| 24 | 177 \begin{figure}[tb] |
| 178 \begin{center} | |
| 179 \includegraphics[width=70mm]{./fig/meta-cg-dg.pdf} | |
| 180 \end{center} | |
| 181 \caption{CodeGearとMetaCodeGear} | |
| 182 \label{meta-cg-dg} | |
| 183 \end{figure} | |
| 26 | 184 |
| 185 ノーマルレベルのプログラミングでは、 図\ref{meta-cg-dg}の上段に示す様に入力のDataGearを受け取りCodeGearを実行、 結果をDataGearに書き込んだ上で別のCodeGearに継続する様に見える。 | |
| 186 しかし実際はCodeGearの実行の前後に実行されるMetaCodeGearや入出力のDataGearを保存場所から取り出すMetaDataGearなどのメタ計算が加わる。 | |
| 187 | |
| 188 遷移先のCodeGearとMetaCodeGearの紐付けや、 計算に必要なDataGearを保存や管理を行うMetaDataGearとしてcontextがある。 | |
| 189 contextは処理に必要なCodeGearの番号とMetaCodeGearの対応表や、 DataGearの格納場所を持つ。 | |
| 190 コード上では別のCodeGearに直接遷移している様に見えるが、 実際はcontext内の遷移先のCodeGearに対応するスロットから、対応するMetaCodeGearに遷移する。 | |
| 191 MetaCodeGear中で、次に実行するCodeGearで必要なDataGearをcontextから取り出し、 実際の計算が行われる。 | |
| 192 contextは計算に必要なデータ構造と処理を持つデータ構造であることから、 従来のOSのプロセスに相当するものと言える。 | |
| 18 | 193 |
| 22 | 194 \section{xv6 kernel} |
| 195 | |
| 196 xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。 | |
| 197 xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。 | |
| 198 Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。 | |
| 199 本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。 | |
| 200 | |
| 201 xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。 | |
| 202 またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。 | |
| 203 | |
| 204 本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。 | |
| 205 xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。 | |
| 206 | |
| 18 | 207 |
| 15 | 208 \section{xv6のファイルシステムの一部の分析} |
| 209 | |
| 210 xv6のファイルシステムに関する定義ファイルはfs.c中に記述されている。 | |
| 211 この中に出てくる関数に着目し、 この関数をさらにCodeGearに変換していくことで状態遷移単位での記述を試みた。 | |
| 212 | |
| 213 まず関数内でif文などの分岐を持たない基本単位であるBasic Blockに着目した。 | |
| 214 CbCのCodeGearの粒度はCの関数とアセンブラの中間であるといえるので、 BasicBlockをCodeGearに置き換える事が可能である。 | |
| 17 | 215 したがって特定の関数内の処理のBasicBlockを分析し、 BasicBlockに対応したCodeGearへ変換することで状態遷移系への変換を行った。 |
| 15 | 216 |
| 217 | |
| 14 | 218 |
| 10 | 219 \nocite{*} |
| 220 \bibliographystyle{ipsjunsrt} | |
| 221 \bibliography{anatofuz-bib} | |
| 222 | |
| 223 | |
| 224 \end{document} |