Mercurial > hg > Papers > 2020 > anatofuz-sigos
annotate paper/anatofuz-sigos.md @ 52:778f4b2b68f0
fix
| author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 07 May 2020 20:47:22 +0900 |
| parents | 305181ddeb7d |
| children |
| rev | line source |
|---|---|
| 47 | 1 # アプリケーションの信頼性 |
| 2 アプリケーションの信頼性を向上させるためには、 土台となるOS自体の信頼性が高く保証されていなければならない。 | |
| 3 OSそのものも巨大なプログラムであるため、テストコードを用いた方法で信頼性を確保する事が可能である。 | |
| 4 しかし並列並行処理などに起因するバグや、そもそもOSを構成する処理が巨大であることから、 テストで完全にバグを発見するのは困難である。 | |
| 10 | 5 テスト以外の方法でOSの信頼性を高めたい。 |
| 6 | |
| 47 | 7 そこで数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。 |
| 49 | 8 OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、定理証明支援系Agda\cite{agda}を利用した証明ベースでの信頼性の確保などの手法が考えられる。\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402} |
| 48 | 9 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。\cite{hyperKernel} |
| 10 | 10 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。 |
| 22 | 11 しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。 |
| 10 | 12 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。 |
| 13 | |
| 47 | 14 OS上のアプリケーションには本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理がある。 |
| 15 前者をノーマルレベルの計算と呼び、後者をメタ計算と呼ぶ。 | |
| 16 OSはメタ計算を担当していると言える。 | |
| 17 実装のソースコードはノーマルレベルであり検証用のソースコードはメタ計算だと考えると、OSそのものが | |
| 18 検証を行ない、システム全体の信頼を高める機能を持つべきだと考える。 | |
| 19 ノーマルレベル上でのバグを例えばモデル検査のようなメタ計算によって発見し信頼性を向上させたい。 | |
| 21 | 20 |
| 21 ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。 | |
| 48 | 22 CbCは基本`goto`で`CodeGaar`というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と |
| 51 | 23 呼ばれる隠れた状態を持たない。このため、計算のための情報は`CodeGear`の入力にすべてそろっている。 |
| 24 そのうちのいくつかはメタ計算、つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(DataGear)である。 | |
| 25 メタ計算とノーマルレベルの区別は入力のどこを扱うかの差に帰着される。 | |
| 11 | 26 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。 |
| 27 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。 | |
| 48 | 28 CbCは`GCC`\cite{gcc}\cite{weko_82695_1}あるいは`LLVM`\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。 |
| 29 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{agda-ryokka}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。 | |
| 10 | 30 |
| 50 | 31 現在小さなunixであるxv6 kernelをCbCを用いて書き換えている。 |
| 32 書き換えの為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。 | |
| 11 | 33 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。 |
| 34 | |
| 13 | 35 |
| 36 # Continuation Based C | |
| 37 | |
| 38 Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。 | |
| 47 | 39 CbCでは通常の関数呼び出しの他に、 関数呼び出し時のスタックの操作を行わず、次のコードブロックに\texttt{jmp}命令で移動する継続が導入されている。 |
| 13 | 40 この継続はSchemeなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である為に軽量である事から軽量継続と呼べる。 |
| 47 | 41 またCbCではこの軽量継続を用いて\texttt{for}文などのループ文を実装する。これは関数型プログラミングでのTail callスタイルでプログラミングすることに相当する。 |
| 42 実際、Agda よる関数型のCbCの記述も用意されている\cite{}。 | |
| 43 実際のOSやアプリケーションを記述する場合には | |
| 44 GCC及びLLVM/clang上のCbC実装を用いる。 | |
| 14 | 45 |
| 17 | 46 CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。 |
| 47 | 47 CodeGearは通常のCの関数宣言の返り値の型の代わりに\texttt{\_\_code}で宣言を行う。 |
| 27 | 48 各CodeGearはDataGearと呼ばれるデータの単位で入力を受け取り、 その結果を別のDataGearに書き込む。 |
| 49 入力のDataGearをInputDataGearと呼び、 出力のDataGearをOutputDataGearと呼ぶ。 | |
| 50 CodeGearがアクセスできるDataGearは、 InputDataGearとOutputDataGearに限定される。 | |
| 51 これらの関係図を図\ref{fig:cgdg}に示す。 | |
| 52 | |
| 53  | |
| 17 | 54 |
| 48 | 55 CbCを利用したシステムコールのディスパッチ部分をCode \ref{src:cbc_example}に示す。 |
| 56 この例題では特定のシステムコールの場合、 CbCで実装された処理に`goto`文をつかって継続する。 | |
| 57 例題ではCodeGearへのアドレスが配列`cbccodes`に格納されている。 | |
| 58 引数として渡している`cbc_ret`は、 システムコールの返り値の数値をレジスタに代入するCodeGearである。 | |
| 51 | 59 実際に`cbc_ret`に継続が行われるのは、 `read`などのシステムコールの一連の処理の継続が終わったタイミングである。 |
| 14 | 60 |
| 48 | 61 ``` lab:src:cbc_example, cap:CbCを利用したシステムコールのディスパッチ |
| 62 void syscall(void) | |
| 63 { | |
| 64 int num; | |
| 65 int ret; | |
| 66 | |
| 67 if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) { | |
| 68 proc->cbc_arg.cbc_console_arg.num = num; | |
| 69 goto (cbccodes[num])(cbc_ret); | |
| 15 | 70 } |
| 71 ``` | |
| 14 | 72 |
| 51 | 73 Code\ref{src:cbc_example}の状態遷移図を図\ref{fig:dispatch}に示す。 |
| 74 図中の`cbc_read`などは、 `read`システムコールを実装しているCodeGearの集合である。 | |
| 75 | |
| 76  | |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
77 |
| 17 | 78 CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。 |
| 79 しかしCodeGearを呼び出す直前のスタックは保存されるため、 部分的にCbCを適用する場合はCodeGearを呼び出す`void`型などの関数を経由することで呼び出しが可能となる。 | |
| 80 | |
| 81 この他にCbCからCへ復帰する為のAPIとして、 環境付きgotoという機能がある。 | |
| 82 これはGCCでは内部コードを生成、 LLVM/clangでは`setjmp`と`longjmp`を使うことでCodeGearの次の継続対象として呼び出し元の関数を設定することが可能となる。 | |
| 83 したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。 | |
| 84 | |
| 20 | 85 # CbCを用いたOSの実装 |
| 86 | |
| 87 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。 | |
| 88 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。 | |
| 89 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。 | |
| 22 | 90 CodeGearを元にプログラミングをするにつれて、 CodeGearの入出力のDataも重要であることが解ってきた。 |
| 48 | 91 CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。\cite{gears} |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
92 現在のGearsOSは並列フレームワークとして実装されており、 実用的なOSのプロトタイプ実装として既存のOS上への実装を目指している。 |
| 22 | 93 |
| 94 GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。 | |
| 21 | 95 遷移する各CodeGearの実行に必要なデータの整合性の確認などのメタ計算は、 MetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。 |
| 22 | 96 このMetaCodeGearの中で参照されるDataGearをMetaDataGearと呼ぶ。 |
| 27 | 97 また、 対象のCodeGearの直前で実行されるMetaCodeGearをStubCodeGearと呼ぶ。 |
| 36 | 98 MetaCodeGearやMetaDataGearは、プログラマが直接実装することはなく、 現在はPerlスクリプトによってGearsOSのビルド時に生成される。 |
| 26 | 99 CodeGearから別のCodeGearに遷移する際のDataGearなどの関係性を、図\ref{meta-cg-dg}に示す。 |
| 23 | 100 |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
101  |
| 26 | 102 |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
103 通常のコード中では入力のDataGearを受け取りCodeGearを実行、 結果をDataGearに書き込んだ上で別のCodeGearに継続する様に見える。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
104 この流れを図\ref{meta-cg-dg}の上段に示す。 |
| 52 | 105 しかし実際はCodeGearの実行の前後に実行されるMetaCodeGearや入出力のDataGearをMetaDataGearから取り出すなどのメタ計算が加わる。 |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
106 これは図\ref{meta-cg-dg}の下段に対応する。 |
| 26 | 107 |
| 52 | 108 遷移先のCodeGearとMetaCodeGearの紐付けや、 計算に必要なDataGearを保存や管理を行うMetaDataGearとして`context`がある。 |
| 26 | 109 contextは処理に必要なCodeGearの番号とMetaCodeGearの対応表や、 DataGearの格納場所を持つ。 |
| 27 | 110 計算に必要なデータ構造と処理を持つデータ構造であることから、 contextは従来のOSのプロセスに相当するものと言える。 |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
111 cotnextと各データ構造の関わりを図\ref{fig:context_ref}に示す。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
112  |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
113 |
| 26 | 114 コード上では別のCodeGearに直接遷移している様に見えるが、 実際はcontext内の遷移先のCodeGearに対応するスロットから、対応するMetaCodeGearに遷移する。 |
| 36 | 115 MetaCodeGear中で、次に実行するCodeGearで必要なDataGearをcontextから取り出し、 実際の計算が行われる。 |
| 27 | 116 |
| 18 | 117 |
| 22 | 118 # xv6 kernel |
| 119 | |
| 48 | 120 xv6とはマサチューセッツ工科大学でv6 OS\cite{lions1996lions}を元に開発された教育用のUNIX OSである。\cite{xv6} |
| 22 | 121 xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。 |
| 48 | 122 Raspberry Pi\cite{rpi}上での動作を目的としたARMアーキテクチャのバージョンも存在する。\cite{xv6rpi} |
| 22 | 123 本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。 |
| 124 | |
| 125 xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。 | |
| 126 またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。 | |
| 127 | |
| 128 本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。 | |
| 129 xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。 | |
| 130 | |
| 36 | 131 本論文ではxv6の継続の分析をシステムコール部分とファイルシステム、 仮想メモリなどのOSの根幹部分でそれぞれ行った。 |
| 32 | 132 |
| 18 | 133 |
| 48 | 134 # xv6のシステムコールの継続の分析と書き換え |
| 50 | 135 xv6の処理を継続を中心とした記述で書き換えを行う。 |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
136 この際に、 xv6のどの処理に着目するかによって継続の実装が異なっていくことが実装につれてわかった。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
137 |
| 48 | 138 まずxv6の`read` システムコールに着目し、 システムコール内部でどのような状態を遷移するかを分析した。 \cite{weko_195888_1} |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
139 分析結果をCbCのCodeGearに変換し、 状態遷移図におこしたものを図\ref{fig:cbc_readsyscall}に示す。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
140 |
| 48 | 141  |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
142 |
| 50 | 143 CbCで書き換えた`read`システムコールは、 xv6の`read`システムコールのディスパッチ部分から、 `cbc_read`CodeGearに`goto`文で軽量継続される。 |
| 30 | 144 継続後はreadする対象によって`cbc_readi`や、 `cbc_consoleread`などに状態が変化していく。 |
| 32 | 145 各CodeGearの遷移時にはDataGearがやり取りされる。 |
| 146 DataGearはxv6のプロセス構造体に埋め込まれたcontextを経由してCodeGearに渡される。 | |
| 147 | |
| 30 | 148 この実装の利点として、 CodeGearの命名と状態が対応しており、 状態遷移図などに落としても自然言語で説明が可能となる点が挙げられる。 |
| 149 しかし実際には`cbc_readi`の状態はさらに複数のCodeGearに分離しており、 実際に`read`システムコールを実装するCodeGearの数は図の状態より多い。 | |
| 150 この事から、 複数のCodeGearを1つにまとめた上で見た状態と、 各CodeGearそれぞれの状態の2種類の状態があるといえる。 | |
| 151 | |
| 34 | 152 複数のCodeGearをまとめた状態は、 抽象化したAPIの操作時におけるアルゴリズム上の問題が無いかの確認として使用出来る。 |
| 30 | 153 対して各CodeGearそれぞれはモデル検査や、 特定の関数の中の処理が適しているかどうかの検査として見ることが出来ると考えられる。 |
| 154 | |
| 32 | 155 この事からGearsOSでは、 各CodeGearのモジュール化の仕組みであるInterface機能を導入している。 |
| 156 Interfaceの導入によってCodeGearを定義することで状態数を増やしても、 抽象化されたAPIを利用することで細部の状態まで意識する必要が無くなった。 | |
| 50 | 157 xv6の処理をCbCで書き換える際には、 対象の継続のAPIをまず決定しモジュール化を図る必要がある。 |
| 30 | 158 |
| 159 # xv6のシステムコール以外の継続の分析 | |
| 33 | 160 xv6はシステムコール以外に、 ファイルシステムの操作やページテーブルの管理などの処理も存在している。 |
| 161 これらはOSの立ち上げ時やシステムコールの中で、ファイルシステムの操作に対応した関数や構造体などのAPIを通して操作される。 | |
| 35 | 162 システムコールの一連の流れに着目するのではなく、 特定の対象のAPIに着目して継続の分析を検討した。 |
| 163 | |
| 38 | 164 xv6のファイルシステムに関する関数などのAPIは主に`fs.c`中に記述されている。 |
| 51 | 165 APIの内部をCodeGearに分割をすると、 APIを呼び出す時点でAPI細部の継続を考慮する必要がある。 |
| 166 細部の継続を隠蔽するために、 抽象的に複数のCodeGearをまとめる機能であるInterfaceを導入したい。 | |
| 36 | 167 Code\ref{src:fs_interface}に示す様に、 `fs.c`中に定義されているAPIを抜き出し、 CbCのInterfaceとして定義した。 |
| 168 `__code`から始まるCodeGearの名前が、 それぞれ抽象化されたCodeGearの集合の最初の継続となる。 | |
| 35 | 169 |
| 170 | |
| 171 ``` lab:src:fs_interface, cap:ファイルシステム操作のAPIの一部 | |
| 172 typedef struct fs<Type,Impl> { | |
| 173 __code readsb(Impl* fs, uint dev, struct superblock* sb, __code next(...)); | |
| 174 __code iinit(Impl* fs, __code next(...)); | |
| 175 __code ialloc(Impl* fs, uint dev, short type, __code next(...)); | |
| 176 __code iupdate(Impl* fs, struct inode* ip, __code next(...)); | |
| 177 __code idup(Impl* fs, struct inode* ip, __code next(...)); | |
| 178 __code ilock(Impl* fs, struct inode* ip, __code next(...)); | |
| 179 __code iunlock(Impl* fs, struct inode* ip, __code next(...)); | |
| 180 __code iput(Impl* fs, struct inode* ip, __code next(...)); | |
| 181 .... | |
| 182 } fs; | |
| 183 ``` | |
| 184 | |
| 36 | 185 Code\ref{src:fs_interface}内の `readsb`などは`fs.c`内で定義されているCの関数名と対応している。 |
| 37 | 186 このCの関数を更に継続ごと分割するために、 関数内のif文などの分岐を持たない基本単位であるBasic Blockに着目した。 |
| 30 | 187 |
| 15 | 188 CbCのCodeGearの粒度はCの関数とアセンブラの中間であるといえるので、 BasicBlockをCodeGearに置き換える事が可能である。 |
| 35 | 189 したがって特定の関数内の処理のBasicBlockを分析し、 BasicBlockに対応したCodeGearへ変換することが可能となる。 |
| 38 | 190 実際にBasicBlock単位で切り分ける前の処理と、切り分けたあとの処理の一部を示す。 |
| 191 例としてinodeのアロケーションを行うAPIでる`ialloc`の元のコードをCode\ref{src:ialloc_origin}に示す。 | |
| 192 | |
| 193 ``` lab:src:ialloc_origin, cap:iallocの元のソースコード | |
| 194 struct inode* ialloc (uint dev, short type) | |
| 195 { | |
| 196 readsb(dev, &sb); | |
| 197 for (inum = 1; inum < sb.ninodes; inum++) { | |
| 198 bp = bread(dev, IBLOCK(inum)); | |
| 199 dip = (struct dinode*) bp->data + inum % IPB; | |
| 37 | 200 |
| 38 | 201 if (dip->type == 0) { // a free inode |
| 202 memset(dip, 0, sizeof(*dip)); | |
| 48 | 203 ... |
| 38 | 204 return iget(dev, inum); |
| 205 } | |
| 206 brelse(bp); | |
| 207 } | |
| 208 panic("ialloc: no inodes"); | |
| 209 } | |
| 210 ``` | |
| 211 | |
| 212 `ialloc`はループ条件である `inum < sb.ninodes`が成立しなかった場合は`panic`へと状態が遷移する。 | |
| 213 この`for`文での状態遷移をCodeGearに変換したものをCode\ref{src:allocinode_loopcheck}に示す。 | |
| 214 | |
| 215 | |
| 216 ``` lab:src:allocinode_loopcheck, cap:ループ条件を確認するCodeGear | |
| 217 __code allocinode_loopcheck(struct fs_impl* fs_impl, uint inum, uint dev, struct superblock* sb, struct buf* bp, struct dinode* dip, __code next(...)){ | |
| 218 if( inum < sb->ninodes){ | |
| 219 goto allocinode_loop(fs_impl, inum, dev, type, sb, bp, dip, next(...)); | |
| 220 } | |
| 221 char* msg = "failed allocinode..."; | |
| 222 struct Err* err = createKernelError(&proc->cbc_context); | |
| 223 goto err->panic(msg); | |
| 224 } | |
| 225 ``` | |
| 15 | 226 |
| 40 | 227 Code\ref{src:allocinode_loopcheck}ではループ条件の成立を`if`文で確認し、ループ処理に移行する場合は `allocinode_loop`へ遷移する。 |
| 48 | 228 `goto`文の中の引数の1つ`next(...)` は、 APIとして呼び出した`ialloc`の次の継続のCodeGearに対して、 `context`などの環境を渡す構文である。 |
| 40 | 229 ループ条件が満たされなかった場合は、 コンテキストから`panic`に関するCodeGearの集合を取り出し、 集合中の`panic` CodeGearへと遷移する。 |
| 48 | 230 オリジナルの処理では、 ループ中に`dip->type == 0`が満たされた場合は関数から`return`文により関数から復帰する。 |
| 40 | 231 CodeGearではCode\ref{src:alloc_loop}内で、 状態が分けられる。 |
| 232 この先の継続は、 復帰用のCodeGearかループの先頭である`allocinode_loopcheck`に再帰的に遷移するかになる。 | |
| 233 | |
| 234 ``` lab:src:alloc_loop, cap:ループ中に復帰するかどうかの確認をするCodeGear | |
| 235 __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(...)){ | |
| 236 bp = bread(dev, IBLOCK(inum)); | |
| 237 dip = (struct dinode*) bp->data + inum % IPB; | |
| 238 if(dip->type = 0){ | |
| 239 goto allocinode_loopexit(fs_impl, inum, dev, sb, bp, dip, next(...)); | |
| 240 } | |
| 241 | |
| 242 brelse(bp); | |
| 243 inum++; | |
| 244 goto allocinode_loopcheck(fs_impl, inum, dev, type, sb, bp, dip, next(...)); | |
| 245 } | |
| 246 ``` | |
| 247 | |
| 248 この継続の分析方法の利点として、 既存のコードのBasic Block単位でCodeGearに変換可能であるため機械的にCodeGearへの変更が可能となる。 | |
| 249 既存の関数上のアルゴリズムや処理に殆ど変更がなく変更可能であるために、 CodeGearで細分化して表現することは容易となる。 | |
| 41 | 250 |
| 251 現在は従来のxv6の関数呼び出しを元にしたAPIの中でCodeGearに分割している。 | |
| 252 このために既存のAPI内の処理の細分化は可能とはなったが、 APIそのものをCodeGearを用いた継続に適した形には表現できていない。 | |
| 253 APIの内部のCodeGearはあくまでBasic Block単位に基づいているために、 状態遷移図で表現した際に自然言語で表現できないCodeGearも存在してしまう。 | |
| 254 | |
| 255 さらに、 `for`ループをCodeGearに分割することを考えるとループ中にループのindexを利用している場合は、 そのindexも次の継続に渡さなければならない。 | |
| 256 このためindexを使用していないCodeGearでも継続の引数としてindexを受け取り、 実際にindexを利用するCodeGearに伝搬させる必要がある。 | |
| 42 | 257 これらの問題を解決する為には、 APIを分割したCodeGearそれぞれのDataGearに型を与え、 どの継続でDataGearの意味が変わるかを追求する必要がある。 |
| 43 | 258 APIを分割して作成したCodeGearのDataGearは、 現在各APIに対応した1つの巨大な構造体に隠蔽されている。 |
| 42 | 259 巨大な構造体で管理するのではなく、 構造体で次のCodeGearの状態に影響を与える要素を適宜組み合わせたDataGearを作る必要がある。 |
| 40 | 260 |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
261 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
262 # CbCを用いた部分的なxv6の書き換え |
| 27 | 263 |
| 264 CbCではCodeGear、 DataGearからなる単位を基本とし、 それぞれにメタなGearが付随する。 | |
| 265 また実行に必要なCodeGearとDataGearをまとめたcontextというMetaDataGearが存在する。 | |
| 266 この機能を元にxv6の書き換えを検討した。 | |
| 267 | |
| 268 xv6内でCbCの軽量継続に突入する際は、 元の処理関数に通常の方法では戻ってくることができず、部分的に書き換えていくのが困難である。 | |
| 269 今回は呼び出し関数に戻れるスタックフレームを操作したい為に、 ダミーの`void`関数を用意した。 | |
| 270 この関数内でCodeGearに`goto`文を用いて遷移することで、 CbCから帯域脱出した際に`void`関数の呼び出し元から処理を継続し、部分的にCbCに書き換えることが可能となった。 | |
| 271 Code\ref{src:dumy_function_cbc}では、 `userinit`関数へ戻るために、 `cbc_init_vmm_dumy`を経由している。 | |
| 272 | |
| 273 ``` lab:src:dumy_function_cbc, cap:部分的にCbCを適応する例 | |
| 274 void cbc_init_vmm_dummy(struct Context* cbc_context, struct proc* p, pde_t* pgdir, char* init, uint sz) | |
| 275 { | |
| 276 struct vm* vm = createvm_impl(cbc_context); | |
| 277 goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret); | |
| 278 } | |
| 279 | |
| 280 void userinit(void) | |
| 281 { | |
| 48 | 282 ... |
| 27 | 283 |
| 284 if((p->pgdir = kpt_alloc()) == NULL) { | |
| 285 panic("userinit: out of memory?"); | |
| 286 } | |
| 287 | |
| 288 cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size); | |
| 289 | |
| 290 p->sz = PTE_SZ; | |
| 291 memset(p->tf, 0, sizeof(*p->tf)); | |
| 48 | 292 ... |
| 43 | 293 } |
| 31 | 294 ``` |
| 295 | |
| 43 | 296 Code\ref{src:dumy_function_cbc}中で、 CodeGearへの遷移が行われる`goto vm->init_vmm()`の`vm->void_ret`は`init_vmm`の次の継続のCodeGear名である。 |
| 297 この`vm->void_ret`は`return`するのみのCodeGearであり、 void型関数と組み合わせることで呼び出し元へと復帰する事が可能となる。 | |
| 298 | |
| 31 | 299 |
| 50 | 300 # xv6の今後の書き換え |
| 31 | 301 |
| 302 xv6ではカーネルパニックの発生時や、 inodeのキャッシュなどをグローバル変数として利用している。 | |
| 303 グローバル変数を使用してしまうと、 CodeGearで定義した状態がDataGear以外のグローバル変数によって変更されてしまう。 | |
| 304 グローバル変数を極力使わず継続を中心とした実装を行いたい。 | |
| 305 | |
| 36 | 306 contextは現在プロセス構造体に埋め込まれており、 kernelそのものの状態を制御するためには各contextを管理する機能が必要であると考えられる。 |
| 43 | 307 |
| 50 | 308 現状はxv6の全ての機能をまだCbCを用いて書き換えていない。 |
| 309 ファイルシステムや仮想メモリにまつわる処理などはAPI単位では書き換えているが、 APIを呼び出す箇所はCの関数上で部分的に呼び出している。 | |
| 44 | 310 そのためにOSそのものを状態遷移単位で完全に書き直す必要が存在し、 そのためには全ての処理に対して状態を定義していく必要がある。 |
| 311 | |
| 312 またOS上でDataGearとCodeGearの位置づけを明確に定義する必要も存在する。 | |
| 313 DataGearの依存関係やCodeGearの並列実行など、 プロセスベースで実装していた処理をCodeGearなどで意味がある形式にする必要がある。 | |
| 314 | |
| 43 | 315 # まとめ |
| 316 | |
| 50 | 317 本稿ではxv6を継続を用いた単位での書き換えを検討し、 実際にいくつかの処理を書き換えた。 |
| 51 | 318 書き換えはシステムコールに着目しCodeGearへ分割する手法と、 BasicBlockごとにCodeGearへ分割する手法で行った。 |
| 319 現状はまだxv6の実装を利用した証明や、 xv6にモデル検査機能の実装を行いたい。 | |
| 44 | 320 またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。 |
| 321 |