Mercurial > hg > Papers > 2020 > anatofuz-sigos
annotate paper/anatofuz-sigos.tex @ 46:667ae17b169e
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 07 May 2020 16:25:28 +0900 |
| parents | 4cecdfd6b237 |
| children | 567288b8a89e |
| 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} | |
| 46 | 66 アプリケーションやサービスの信頼性は、OSと結びついている。OS自身が高い信頼性を持つ必要があり、 |
| 67 その上で動作するソフトウェアの信頼性をOSが保証するような仕組みがあると良い。 | |
| 68 テストは本質的に有限なケースしか調べないので、テストだけで信頼性を保証するのには限界がある。 | |
| 69 アプリケーションとOSの状態を状態遷移を基本としたモデルに変換しモデル検査やHoare Logic などの形式手法を用いて信頼性を高めたい。 | |
| 70 そのために状態遷移単位での記述に適した継続を基本とした言語であるCbC(Continuation based C)をOSとアプリケーションの記述に用いる。 | |
| 71 最初の段階として小さなunixであるxv6 kernelのCbCによる書き換えを行っている。 | |
| 72 xv6 kernelの処理がどのような状態遷移を行うのかを分析し、CbCの継続ベースでのプログラミングに変換していく必要がある。 | |
| 73 本稿ではxv6kernelの構成要素の一部に着目し、状態遷移系の分析とxv6の書き換えを行う。 | |
| 10 | 74 \end{abstract} |
| 75 | |
| 76 | |
| 77 \maketitle | |
| 78 | |
| 46 | 79 \section{アプリケーションの信頼性} |
| 80 アプリケーションの信頼性を向上させるためには、 土台となるOS自体の信頼性が高く保証されていなければならない。 | |
| 81 OSそのものも巨大なプログラムであるため、テストコードを用いた方法で信頼性を確保する事が可能である。 | |
| 82 しかし並列並行処理などに起因するバグや、そもそもOSを構成する処理が巨大であることから、 テストで完全にバグを発見するのは困難である。 | |
| 10 | 83 テスト以外の方法でOSの信頼性を高めたい。 |
| 84 | |
| 46 | 85 そこで数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。 |
| 86 OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、Agda定理証明支援系\cite{}を利用した証明ベースでの信頼性の確保などの手法が考えられる。 | |
| 10 | 87 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。 |
| 46 | 88 % これに適した形として、 状態遷移モデルが挙げられる。 |
| 10 | 89 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。 |
| 46 | 90 % 既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析し、仕様記述言語などによる再実装が必要となる。 |
| 22 | 91 しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。 |
| 10 | 92 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。 |
| 93 | |
| 46 | 94 OS上のアプリケーションには本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理がある。 |
| 95 前者をノーマルレベルの計算と呼び、後者をメタ計算と呼ぶ。 | |
| 96 OSはメタ計算を担当していると言える。 | |
| 97 実装のソースコードはノーマルレベルであり検証用のソースコードはメタ計算だと考えると、OSそのものが | |
| 98 検証を行ない、システム全体の信頼を高める機能を持つべきだと考える。 | |
| 99 ノーマルレベル上でのバグを例えばモデル検査のようなメタ計算によって発見し信頼性を向上させたい。 | |
| 100 % プログラマからはノーマルレベルの計算のみ実装するが、整合性の確認や拡張を行う際にノーマルレベルと同様の記述力でメタ計算も実装できる必要がある。 | |
| 21 | 101 |
| 102 ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。 | |
| 46 | 103 CbCは基本 goto で CodeGaar というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と |
| 104 呼ばれる隠れた状態を持たない。このため、計算のための情報は CodeGearの入力にすべてそろっている。そのうちのいくつかはメタ計算、 | |
| 105 つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(DataGear)である。メタ計算とノーマルレベルの | |
| 106 区別は入力のどこを扱うかの差に帰着される。 | |
| 12 | 107 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。 |
| 108 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。 | |
| 46 | 109 CbCは GCC \cite{}あるいは LLVM \cite{}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。 |
| 110 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。 | |
| 111 % すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。 | |
| 12 | 112 |
| 113 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。 | |
| 114 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。 | |
| 115 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。 | |
| 116 | |
| 10 | 117 |
| 13 | 118 \section{Continuation Based C} |
| 119 | |
| 120 Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。 | |
| 17 | 121 CbCでは通常の関数呼び出しの他に、 関数呼び出し時のスタックの操作を行わず、次のコードブロックに\texttt{jmp}命令で移動する継続が導入されている。 |
| 13 | 122 この継続はSchemeなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である為に軽量である事から軽量継続と呼べる。 |
| 46 | 123 またCbCではこの軽量継続を用いて\texttt{for}文などのループ文を実装する。これは関数型プログラミングでのTail callスタイルでプログラミングすることに相当する。 |
| 124 実際、Agda よる関数型のCbCの記述も用意されている\cite{}。 | |
| 125 実際のOSやアプリケーションを記述する場合には | |
| 126 GCC及びLLVM/clang上のCbC実装を用いる。 | |
| 14 | 127 |
| 17 | 128 CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。 |
| 129 CodeGearは通常のCの関数宣言の返り値の型の代わりに\texttt{\_\_code}で宣言を行う。 | |
| 28 | 130 各CodeGearはDataGearと呼ばれるデータの単位で入力を受け取り、 その結果を別のDataGearに書き込む。 |
| 131 入力のDataGearをInputDataGearと呼び、 出力のDataGearをOutputDataGearと呼ぶ。 | |
| 132 CodeGearがアクセスできるDataGearは、 InputDataGearとOutputDataGearに限定される。 | |
| 133 これらの関係図を図\ref{fig:cgdg}に示す。 | |
| 134 | |
| 135 \begin{figure}[tb] | |
| 136 \begin{center} | |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
137 \includegraphics[width=80mm]{fig/cgdg.pdf} |
| 28 | 138 \end{center} |
| 139 \caption{CodeGearと入出力の関係図} | |
| 140 \label{fig:cgdg} | |
| 141 \end{figure} | |
| 17 | 142 |
| 15 | 143 CbCで階乗を求める例題をCode \ref{src:cbc_example}に示す。 |
| 17 | 144 例題ではCodeGearとして\texttt{factorial}を宣言している。 |
| 18 | 145 \texttt{factorial}はCodeGearの引数として\texttt{struct F}型の変数\texttt{arg}を受け取り、\texttt{arg}のメンバー変数によって\texttt{factorial}の再帰呼び出しを行う。 |
| 17 | 146 CodeGearの呼び出しは\texttt{goto}文によって行われる。 |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
147 この例題を状態遷移図にしたものを図\ref{fig:factorial_cbc}に示す。 |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
148 図中の四角がDataGear、 円がCodeGearに対応する。 |
| 14 | 149 |
| 150 | |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
151 \begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={CbCで階乗を求める例題}] |
| 15 | 152 __code factorial(struct F arg) { |
| 153 if (arg.n<0) { | |
| 154 exit(1); | |
| 155 } | |
| 156 if (arg.n==0) { | |
| 157 goto arg.next(arg); | |
| 158 } else { | |
| 159 arg.r *= arg.n; | |
| 160 arg.n--; | |
| 161 goto factorial(arg); | |
| 14 | 162 } |
| 163 } | |
| 15 | 164 \end{lstlisting} |
| 14 | 165 |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
166 \begin{figure}[tb] |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
167 \begin{center} |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
168 \includegraphics[width=80mm]{fig/factorial_cbc.pdf} |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
169 \end{center} |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
170 \caption{CbCで階乗を求める例題の状態遷移} |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
171 \label{fig:factorial_cbc} |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
172 \end{figure} |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
173 |
| 17 | 174 CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。 |
| 175 しかしCodeGearを呼び出す直前のスタックは保存されるため、 部分的にCbCを適用する場合はCodeGearを呼び出す\texttt{void}型などの関数を経由することで呼び出しが可能となる。 | |
| 176 | |
| 177 この他にCbCからCへ復帰する為のAPIとして、 環境付きgotoという機能がある。 | |
| 18 | 178 これはGCCでは内部コードを生成、 LLVM/clangでは\texttt{setjmp}と\texttt{longjmp}を使うことでCodeGearの次の継続対象として呼び出し元の関数を設定することが可能となる。 |
| 17 | 179 したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。 |
| 180 | |
| 20 | 181 \section{CbCを用いたOSの実装} |
| 182 | |
| 183 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。 | |
| 184 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。 | |
| 185 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。 | |
| 22 | 186 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。 |
| 187 CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。 | |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
188 現在のGearsOSは並列フレームワークとして実装されており、 実用的なOSのプロトタイプ実装として既存のOS上への実装を目指している。 |
| 22 | 189 |
| 190 GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。 | |
| 21 | 191 遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。 |
| 22 | 192 このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。 |
| 28 | 193 また、 対象のCodeGearの直前で実行されるMetaCodeGearをStubCodeGearと呼ぶ。 |
| 36 | 194 MetaCodeGearやMetaDataGearは、プログラマが直接実装することはなく、 現在はPerlスクリプトによってGearsOSのビルド時に生成される。 |
| 26 | 195 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
|
196 |
| 24 | 197 \begin{figure}[tb] |
| 198 \begin{center} | |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
199 \includegraphics[width=80mm]{./fig/meta-cg-dg.pdf} |
| 24 | 200 \end{center} |
| 201 \caption{CodeGearとMetaCodeGear} | |
| 202 \label{meta-cg-dg} | |
| 203 \end{figure} | |
| 26 | 204 |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
205 通常のコード中では入力のDataGearを受け取りCodeGearを実行、 結果をDataGearに書き込んだ上で別のCodeGearに継続する様に見える。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
206 この流れを図\ref{meta-cg-dg}の上段に示す。 |
| 26 | 207 しかし実際はCodeGearの実行の前後に実行されるMetaCodeGearや入出力のDataGearを保存場所から取り出すMetaDataGearなどのメタ計算が加わる。 |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
208 これは図\ref{meta-cg-dg}の下段に対応する。 |
| 26 | 209 |
| 210 遷移先のCodeGearとMetaCodeGearの紐付けや、 計算に必要なDataGearを保存や管理を行うMetaDataGearとしてcontextがある。 | |
| 211 contextは処理に必要なCodeGearの番号とMetaCodeGearの対応表や、 DataGearの格納場所を持つ。 | |
| 28 | 212 計算に必要なデータ構造と処理を持つデータ構造であることから、 contextは従来のOSのプロセスに相当するものと言える。 |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
213 cotnextと各データ構造の関わりを図\ref{fig:context_ref}に示す。 |
| 28 | 214 \begin{figure}[tb] |
| 215 \begin{center} | |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
216 \includegraphics[width=80mm]{fig/Context_ref.pdf} |
| 28 | 217 \end{center} |
| 218 \caption{Contextと各データの関係図} | |
| 219 \label{fig:context_ref} | |
| 220 \end{figure} | |
| 18 | 221 |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
222 コード上では別のCodeGearに直接遷移している様に見えるが、 実際はcontext内の遷移先のCodeGearに対応するスロットから、対応するMetaCodeGearに遷移する。 |
| 36 | 223 MetaCodeGear中で、次に実行するCodeGearで必要なDataGearをcontextから取り出し、 実際の計算が行われる。 |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
224 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
225 |
| 22 | 226 \section{xv6 kernel} |
| 227 | |
| 228 xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。 | |
| 229 xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。 | |
| 230 Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。 | |
| 231 本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。 | |
| 232 | |
| 233 xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。 | |
| 234 またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。 | |
| 235 | |
| 236 本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。 | |
| 237 xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。 | |
| 238 | |
| 36 | 239 本論文ではxv6の継続の分析をシステムコール部分とファイルシステム、 仮想メモリなどのOSの根幹部分でそれぞれ行った。 |
| 32 | 240 |
| 18 | 241 |
| 30 | 242 \section{xv6のシステムコールの継続の分析} |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
243 xv6の処理を継続を中心とした記述で再実装を行う。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
244 この際に、 xv6のどの処理に着目するかによって継続の実装が異なっていくことが実装につれてわかった。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
245 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
246 まずxv6の\texttt{read} システムコールに着目し、 システムコール内部でどのような状態を遷移するかを分析した。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
247 分析結果をCbCのCodeGearに変換し、 状態遷移図におこしたものを図\ref{fig:cbc_readsyscall}に示す。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
248 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
249 \begin{figure}[tb] |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
250 \begin{center} |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
251 \includegraphics[width=80mm]{fig/readsyscall_state.pdf} |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
252 \end{center} |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
253 \caption{readシステムコールの状態遷移} |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
254 \label{fig:cbc_readsyscall} |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
255 \end{figure} |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
256 |
| 30 | 257 CbCで再実装した\texttt{read}システムコールは、 xv6の\texttt{read}システムコールのディスパッチ部分から、 \texttt{cbc\_read}CodeGearに\texttt{goto}文で軽量継続される。 |
| 258 継続後はreadする対象によって\texttt{cbc\_readi}や、 \texttt{cbc\_consoleread}などに状態が変化していく。 | |
| 32 | 259 各CodeGearの遷移時にはDataGearがやり取りされる。 |
| 260 DataGearはxv6のプロセス構造体に埋め込まれたcontextを経由してCodeGearに渡される。 | |
| 261 | |
| 30 | 262 この実装の利点として、 CodeGearの命名と状態が対応しており、 状態遷移図などに落としても自然言語で説明が可能となる点が挙げられる。 |
| 263 しかし実際には\texttt{cbc\_readi}の状態はさらに複数のCodeGearに分離しており、 実際に\texttt{read}システムコールを実装するCodeGearの数は図の状態より多い。 | |
| 264 この事から、 複数のCodeGearを1つにまとめた上で見た状態と、 各CodeGearそれぞれの状態の2種類の状態があるといえる。 | |
| 265 | |
| 34 | 266 複数のCodeGearをまとめた状態は、 抽象化したAPIの操作時におけるアルゴリズム上の問題が無いかの確認として使用出来る。 |
| 30 | 267 対して各CodeGearそれぞれはモデル検査や、 特定の関数の中の処理が適しているかどうかの検査として見ることが出来ると考えられる。 |
| 268 | |
| 32 | 269 この事からGearsOSでは、 各CodeGearのモジュール化の仕組みであるInterface機能を導入している。 |
| 270 Interfaceの導入によってCodeGearを定義することで状態数を増やしても、 抽象化されたAPIを利用することで細部の状態まで意識する必要が無くなった。 | |
| 33 | 271 xv6の処理をCbCで再実装する際には、 対象の継続のAPIをまず決定しモジュール化を図る必要がある。 |
| 30 | 272 |
| 273 \section{xv6のシステムコール以外の継続の分析} | |
| 33 | 274 xv6はシステムコール以外に、 ファイルシステムの操作やページテーブルの管理などの処理も存在している。 |
| 275 これらはOSの立ち上げ時やシステムコールの中で、ファイルシステムの操作に対応した関数や構造体などのAPIを通して操作される。 | |
| 35 | 276 システムコールの一連の流れに着目するのではなく、 特定の対象のAPIに着目して継続の分析を検討した。 |
| 277 | |
| 39 | 278 xv6のファイルシステムに関する関数などのAPIは主に\texttt{fs.c}中に記述されている。 |
| 37 | 279 Code\ref{src:fs_interface}に示す様に、 \texttt{fs.c}中に定義されているAPIを抜き出し、 CbCのInterfaceとして定義した。 |
| 36 | 280 \texttt{\_\_code}から始まるCodeGearの名前が、 それぞれ抽象化されたCodeGearの集合の最初の継続となる。 |
| 35 | 281 |
| 282 | |
| 283 \begin{lstlisting}[frame=lrbt,label=src:fs_interface,caption={ファイルシステム操作のAPIの一部}] | |
| 284 typedef struct fs<Type,Impl> { | |
| 285 __code readsb(Impl* fs, uint dev, struct superblock* sb, __code next(...)); | |
| 286 __code iinit(Impl* fs, __code next(...)); | |
| 287 __code ialloc(Impl* fs, uint dev, short type, __code next(...)); | |
| 288 __code iupdate(Impl* fs, struct inode* ip, __code next(...)); | |
| 289 __code idup(Impl* fs, struct inode* ip, __code next(...)); | |
| 290 __code ilock(Impl* fs, struct inode* ip, __code next(...)); | |
| 291 __code iunlock(Impl* fs, struct inode* ip, __code next(...)); | |
| 292 __code iput(Impl* fs, struct inode* ip, __code next(...)); | |
| 293 .... | |
| 294 } fs; | |
| 295 \end{lstlisting} | |
| 296 | |
| 37 | 297 Code\ref{src:fs_interface}内の \texttt{readsb}などは\texttt{fs.c}内で定義されているCの関数名と対応している。 |
| 298 このCの関数を更に継続ごと分割するために、 関数内のif文などの分岐を持たない基本単位であるBasic Blockに着目した。 | |
| 30 | 299 |
| 15 | 300 CbCのCodeGearの粒度はCの関数とアセンブラの中間であるといえるので、 BasicBlockをCodeGearに置き換える事が可能である。 |
| 35 | 301 したがって特定の関数内の処理のBasicBlockを分析し、 BasicBlockに対応したCodeGearへ変換することが可能となる。 |
| 39 | 302 実際にBasicBlock単位で切り分ける前の処理と、切り分けたあとの処理の一部を示す。 |
| 303 例としてinodeのアロケーションを行うAPIでる\texttt{ialloc}の元のコードをCode\ref{src:ialloc_origin}に示す。 | |
| 304 | |
| 305 \begin{lstlisting}[frame=lrbt,label=src:ialloc_origin,caption={iallocの元のソースコード}] | |
| 306 struct inode* ialloc (uint dev, short type) | |
| 307 { | |
| 308 readsb(dev, &sb); | |
| 309 for (inum = 1; inum < sb.ninodes; inum++) { | |
| 310 bp = bread(dev, IBLOCK(inum)); | |
| 311 dip = (struct dinode*) bp->data + inum % IPB; | |
| 37 | 312 |
| 39 | 313 if (dip->type == 0) { // a free inode |
| 314 memset(dip, 0, sizeof(*dip)); | |
| 315 // omission | |
| 316 return iget(dev, inum); | |
| 317 } | |
| 318 brelse(bp); | |
| 319 } | |
| 320 panic("ialloc: no inodes"); | |
| 321 } | |
| 322 \end{lstlisting} | |
| 323 | |
| 324 \texttt{ialloc}はループ条件である \texttt{inum < sb.ninodes}が成立しなかった場合は\texttt{panic}へと状態が遷移する。 | |
| 325 この\texttt{for}文での状態遷移をCodeGearに変換したものをCode\ref{src:allocinode_loopcheck}に示す。 | |
| 326 | |
| 327 | |
| 328 \begin{lstlisting}[frame=lrbt,label=src:allocinode_loopcheck,caption={ループ条件を確認するCodeGear}] | |
| 329 __code allocinode_loopcheck(struct fs_impl* fs_impl, uint inum, uint dev, struct superblock* sb, struct buf* bp, struct dinode* dip, __code next(...)){ | |
| 330 if( inum < sb->ninodes){ | |
| 331 goto allocinode_loop(fs_impl, inum, dev, type, sb, bp, dip, next(...)); | |
| 332 } | |
| 333 char* msg = "failed allocinode..."; | |
| 334 struct Err* err = createKernelError(&proc->cbc_context); | |
| 335 goto err->panic(msg); | |
| 336 } | |
| 337 \end{lstlisting} | |
| 15 | 338 |
| 40 | 339 Code\ref{src:allocinode_loopcheck}ではループ条件の成立を\texttt{if}文で確認し、ループ処理に移行する場合は \texttt{allocinode\_loop}へ遷移する。 |
| 340 ループ条件が満たされなかった場合は、 コンテキストから\texttt{panic}に関するCodeGearの集合を取り出し、 集合中の\texttt{panic} CodeGearへと遷移する。 | |
| 341 オリジナルの処理では、 ループ中に\texttt{dip->type == 0}が満たされた場合は関数から\texttt{return}文により関数から復帰する。 | |
| 342 CodeGearではCode\ref{src:alloc_loop}内で、 状態が分けられる。 | |
| 343 この先の継続は、 復帰用のCodeGearかループの先頭である\texttt{allocinode\_loopcheck}に再帰的に遷移するかになる。 | |
| 344 | |
| 345 \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(...)){ | |
| 347 bp = bread(dev, IBLOCK(inum)); | |
| 348 dip = (struct dinode*) bp->data + inum % IPB; | |
| 349 if(dip->type = 0){ | |
| 350 goto allocinode_loopexit(fs_impl, inum, dev, sb, bp, dip, next(...)); | |
| 351 } | |
| 352 | |
| 353 brelse(bp); | |
| 354 inum++; | |
| 355 goto allocinode_loopcheck(fs_impl, inum, dev, type, sb, bp, dip, next(...)); | |
| 356 } | |
| 357 \end{lstlisting} | |
| 358 | |
| 359 この継続の分析方法の利点として、 既存のコードのBasic Block単位でCodeGearに変換可能であるため機械的にCodeGearへの変更が可能となる。 | |
| 360 既存の関数上のアルゴリズムや処理に殆ど変更がなく変更可能であるために、 CodeGearで細分化して表現することは容易となる。 | |
| 41 | 361 |
| 362 現在は従来のxv6の関数呼び出しを元にしたAPIの中でCodeGearに分割している。 | |
| 363 このために既存のAPI内の処理の細分化は可能とはなったが、 APIそのものをCodeGearを用いた継続に適した形には表現できていない。 | |
| 364 APIの内部のCodeGearはあくまでBasic Block単位に基づいているために、 状態遷移図で表現した際に自然言語で表現できないCodeGearも存在してしまう。 | |
| 365 | |
| 366 さらに、 \texttt{for}ループをCodeGearに分割することを考えるとループ中にループのindexを利用している場合は、 そのindexも次の継続に渡さなければならない。 | |
| 367 このためindexを使用していないCodeGearでも継続の引数としてindexを受け取り、 実際にindexを利用するCodeGearに伝搬させる必要がある。 | |
| 42 | 368 これらの問題を解決する為には、 APIを分割したCodeGearそれぞれのDataGearに型を与え、 どの継続でDataGearの意味が変わるかを追求する必要がある。 |
| 43 | 369 APIを分割して作成したCodeGearのDataGearは、 現在各APIに対応した1つの巨大な構造体に隠蔽されている。 |
| 42 | 370 巨大な構造体で管理するのではなく、 構造体で次のCodeGearの状態に影響を与える要素を適宜組み合わせたDataGearを作る必要がある。 |
| 40 | 371 |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
372 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
373 \section{CbCを用いた部分的なxv6の書き換え} |
| 28 | 374 |
| 375 CbCではCodeGear、 DataGearからなる単位を基本とし、 それぞれにメタなGearが付随する。 | |
| 376 また実行に必要なCodeGearとDataGearをまとめたcontextというMetaDataGearが存在する。 | |
| 377 この機能を元にxv6の書き換えを検討した。 | |
| 378 | |
| 379 xv6内でCbCの軽量継続に突入する際は、 元の処理関数に通常の方法では戻ってくることができず、部分的に書き換えていくのが困難である。 | |
| 380 今回は呼び出し関数に戻れるスタックフレームを操作したい為に、 ダミーの\texttt{void}関数を用意した。 | |
| 381 この関数内でCodeGearに\texttt{goto}文を用いて遷移することで、 CbCから帯域脱出した際に\texttt{void}関数の呼び出し元から処理を継続し、部分的にCbCに書き換えることが可能となった。 | |
| 382 Code\ref{src:dumy_function_cbc}では、 \texttt{userinit}関数へ戻るために、 \texttt{cbc\_init\_vmm\_dumy}を経由している。 | |
| 383 | |
| 384 \begin{lstlisting}[frame=lrbt,label=src:dumy_function_cbc,caption={部分的にCbCを適応する例}] | |
| 385 void cbc_init_vmm_dummy(struct Context* cbc_context, struct proc* p, pde_t* pgdir, char* init, uint sz) | |
| 386 { | |
| 387 struct vm* vm = createvm_impl(cbc_context); | |
| 388 goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret); | |
| 389 } | |
| 390 | |
| 391 void userinit(void) | |
| 392 { | |
| 393 // omission | |
| 394 | |
| 395 if((p->pgdir = kpt_alloc()) == NULL) { | |
| 396 panic("userinit: out of memory?"); | |
| 397 } | |
| 398 | |
| 399 cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size); | |
| 400 | |
| 401 p->sz = PTE_SZ; | |
| 402 memset(p->tf, 0, sizeof(*p->tf)); | |
| 43 | 403 // omission |
| 404 } | |
| 28 | 405 \end{lstlisting} |
| 14 | 406 |
| 43 | 407 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型関数と組み合わせることで呼び出し元へと復帰する事が可能となる。 | |
| 409 | |
| 31 | 410 |
| 411 \section{xv6の今後の再実装} | |
| 412 | |
| 413 xv6ではカーネルパニックの発生時や、 inodeのキャッシュなどをグローバル変数として利用している。 | |
| 414 グローバル変数を使用してしまうと、 CodeGearで定義した状態がDataGear以外のグローバル変数によって変更されてしまう。 | |
| 415 グローバル変数を極力使わず継続を中心とした実装を行いたい。 | |
| 416 | |
| 36 | 417 contextは現在プロセス構造体に埋め込まれており、 kernelそのものの状態を制御するためには各contextを管理する機能が必要であると考えられる。 |
| 43 | 418 contextを管理する方法として、 各context間でメッセージなどをやりとりする方法や、 cotnextを主軸にして割り込みなどの処理を再検討するものがある。 |
| 419 他にはkernelそのもののcontextを定義し、 kernel全体の状態とプロセスの状態をそれぞれ別のcotnextで処理をするというのも検討している。 | |
| 31 | 420 |
| 44 | 421 現状はxv6の全ての機能をまだCbCを用いて再実装をしていない。 |
| 422 ファイルシステムや仮想メモリにまつわる処理などはAPI単位では再実装しているが、 APIを呼び出す箇所はCの関数上で部分的に呼び出している。 | |
| 423 そのためにOSそのものを状態遷移単位で完全に書き直す必要が存在し、 そのためには全ての処理に対して状態を定義していく必要がある。 | |
| 424 xv6にはアセンブラで記述されている処理も複数存在するため、 CodeGrarの表現においてこのような処理の扱いも決定する必要がある。 | |
| 425 | |
| 426 またOS上でDataGearとCodeGearの位置づけを明確に定義する必要も存在する。 | |
| 427 現在は関数を分割した状態としてCodeGearを定義している。 | |
| 428 DataGearの依存関係やCodeGearの並列実行など、 プロセスベースで実装していた処理をCodeGearなどで意味がある形式にする必要がある。 | |
| 429 | |
| 430 またxv6にはユーザーコマンドも存在しているために、 ユーザーコマンド向けのCbCのAPIなども考慮したい。 | |
| 431 | |
| 43 | 432 \section{まとめ} |
| 433 | |
| 434 本稿ではxv6を継続を用いた単位での再実装を検討し、 実際にいくつかの処理を再実装した。 | |
| 44 | 435 現状はまだxv6の実装を利用した証明は行っていない。 |
| 436 今後はモデル検査などを行い、 OSの信頼性を向上させていきたい。 | |
| 43 | 437 それに伴って、 xv6自体にモデル検査機能の組み込みなども行っていく。 |
| 438 またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。 | |
| 44 | 439 |
| 440 | |
| 10 | 441 \nocite{*} |
| 442 \bibliographystyle{ipsjunsrt} | |
| 443 \bibliography{anatofuz-bib} | |
| 444 | |
| 445 | |
| 446 \end{document} |