Mercurial > hg > Papers > 2020 > anatofuz-sigos
annotate paper/anatofuz-sigos.md @ 30:1a9af340ad4a
update
| author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 05 May 2020 11:50:58 +0900 |
| parents | 5dbe39f52406 |
| children | 29369644f3a9 |
| rev | line source |
|---|---|
| 10 | 1 # OSの信頼性 |
| 2 様々なアプリケーションはOSの上で動作するのが当たり前になってきた。 | |
| 3 アプリケーションの信頼性を向上させるのはもとより、 土台となるOS自体の信頼性は高く保証されていなければならない。 | |
| 4 OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。 | |
| 5 しかし並列並行処理などに起因する動かしてみないと発見できないバグなどが存在するため、 テストで完全にバグを発見するのは困難である。 | |
| 6 また、OSを構成する処理も巨大であるため、 これら全てをテスト仕切るのも困難である。 | |
| 7 テスト以外の方法でOSの信頼性を高めたい。 | |
| 8 | |
| 9 数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。 | |
| 10 OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。 | |
| 11 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。 | |
| 12 これに適した形として、 状態遷移モデルが挙げられる。 | |
| 13 OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。 | |
| 22 | 14 既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析し、仕様記述言語などによる再実装が必要となる。 |
| 15 しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。 | |
| 10 | 16 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。 |
| 17 | |
| 21 | 18 さらに本来行いたい処理の他に、メモリ管理やスレッド、 CPUなどの資源管理も行う必要がある。 |
| 19 本来計算機で実行したい計算に必要な計算をメタ計算と呼び、 意図して行いたい処理をノーマルレベルの計算と呼ぶ。 | |
| 20 ノーマルレベル上での問題点をメタ計算上で発見し信頼性を向上させたい。 | |
| 21 プログラマからはノーマルレベルの計算のみ実装するが、整合性の確認や拡張を行う際にノーマルレベルと同様の記述力でメタ計算も実装できる必要がある。 | |
| 22 | |
| 23 ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。 | |
| 11 | 24 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。 |
| 25 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。 | |
| 15 | 26 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。 |
| 12 | 27 すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。 |
| 10 | 28 |
| 11 | 29 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。 |
| 30 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。 | |
| 31 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。 | |
| 32 | |
| 13 | 33 |
| 34 | |
| 35 # Continuation Based C | |
| 36 | |
| 37 Continuation Based C(CbC)とはC言語の下位言語であり、 関数呼び出しではなく継続を導入したプログラミング言語である。 | |
| 17 | 38 CbCでは通常の関数呼び出しの他に、 関数呼び出し時のスタックの操作を行わず、次のコードブロックに`jmp`命令で移動する継続が導入されている。 |
| 13 | 39 この継続はSchemeなどの環境を持つ継続とは異なり、 スタックを持たず環境を保存しない継続である為に軽量である事から軽量継続と呼べる。 |
| 17 | 40 またCbCではこの軽量継続を用いた再帰呼び出しを利用することで`for`文などのループ文を廃し、 関数型プログラミングに近いスタイルでプログラミングが可能となる。 |
| 13 | 41 現在CbCはGCC及びLLVM/clang上にそれぞれ実装されている。 |
| 14 | 42 |
| 43 | |
| 17 | 44 CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。 |
| 45 CodeGearは通常のCの関数宣言の返り値の型の代わりに`__code`で宣言を行う。 | |
| 27 | 46 各CodeGearはDataGearと呼ばれるデータの単位で入力を受け取り、 その結果を別のDataGearに書き込む。 |
| 47 入力のDataGearをInputDataGearと呼び、 出力のDataGearをOutputDataGearと呼ぶ。 | |
| 48 CodeGearがアクセスできるDataGearは、 InputDataGearとOutputDataGearに限定される。 | |
| 49 これらの関係図を図\ref{fig:cgdg}に示す。 | |
| 50 | |
| 51  | |
| 17 | 52 |
| 15 | 53 CbCで階乗を求める例題をCode \ref{src:cbc_example}に示す。 |
| 17 | 54 例題ではCodeGearとして`factorial`を宣言している。 |
| 55 `factorial`はCodeGearの引数として`struct F`型の変数`arg`を受け取り、`arg`のメンバー変数によって`factorial`の再帰呼び出しを行う。 | |
| 56 CodeGearの呼び出しは`goto`文によって行われる。 | |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
57 この例題を状態遷移図にしたものを図\ref{fig:factorial_cbc}に示す。 |
|
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
58 図中の四角がDataGear、 円がCodeGearに対応する。 |
| 14 | 59 |
| 60 | |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
61 ``` lab:src:cbc_example, cap:CbCで階乗を求める例題 |
| 15 | 62 __code factorial(struct F arg) { |
| 63 if (arg.n<0) { | |
| 64 exit(1); | |
| 65 } | |
| 66 if (arg.n==0) { | |
| 67 goto arg.next(arg); | |
| 68 } else { | |
| 69 arg.r *= arg.n; | |
| 70 arg.n--; | |
| 71 goto factorial(arg); | |
| 14 | 72 } |
| 73 } | |
| 15 | 74 ``` |
| 14 | 75 |
|
25
87813fb8542c
add factorial_cbc.pdf
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
76  |
|
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も重要であることが解ってきた。 |
| 91 CodeGearとその入出力であるDataGearを基本としたOSとして、 GearsOSの設計を行っている。 | |
|
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と呼ぶ。 |
| 26 | 98 MetaCodeGearやMetaDataGearは、プログラマが直接実装することはなく、 現在はPerlスクリプトによってGearsOSのビルド時に生成される。 |
| 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}の上段に示す。 |
| 26 | 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 |
| 108 遷移先のCodeGearとMetaCodeGearの紐付けや、 計算に必要なDataGearを保存や管理を行うMetaDataGearとしてcontextがある。 | |
| 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に遷移する。 |
| 115 MetaCodeGear中で、次に実行するCodeGearで必要なDataGearをcontextから取り出し、 実際の計算が行われる。 | |
| 27 | 116 |
| 18 | 117 |
| 22 | 118 # xv6 kernel |
| 119 | |
| 120 xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。 | |
| 121 xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。 | |
| 122 Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。 | |
| 123 本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。 | |
| 124 | |
| 125 xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。 | |
| 126 またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。 | |
| 127 | |
| 128 本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。 | |
| 129 xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイル記述子がある。 | |
| 130 | |
| 18 | 131 |
| 30 | 132 # xv6のシステムコールの継続の分析 |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
133 xv6の処理を継続を中心とした記述で再実装を行う。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
134 この際に、 xv6のどの処理に着目するかによって継続の実装が異なっていくことが実装につれてわかった。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
135 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
136 まずxv6の`read` システムコールに着目し、 システムコール内部でどのような状態を遷移するかを分析した。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
137 分析結果をCbCのCodeGearに変換し、 状態遷移図におこしたものを図\ref{fig:cbc_readsyscall}に示す。 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
138 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
139  |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
140 |
| 30 | 141 CbCで再実装した`read`システムコールは、 xv6の`read`システムコールのディスパッチ部分から、 `cbc_read`CodeGearに`goto`文で軽量継続される。 |
| 142 継続後はreadする対象によって`cbc_readi`や、 `cbc_consoleread`などに状態が変化していく。 | |
| 143 この実装の利点として、 CodeGearの命名と状態が対応しており、 状態遷移図などに落としても自然言語で説明が可能となる点が挙げられる。 | |
| 144 しかし実際には`cbc_readi`の状態はさらに複数のCodeGearに分離しており、 実際に`read`システムコールを実装するCodeGearの数は図の状態より多い。 | |
| 145 この事から、 複数のCodeGearを1つにまとめた上で見た状態と、 各CodeGearそれぞれの状態の2種類の状態があるといえる。 | |
| 146 | |
| 147 信頼性を向上させる観点から見ると、 複数のCodeGearをまとめた状態は実装した関数を組み合せてアルゴリズムに問題が無いかの確認として使用出来る。 | |
| 148 対して各CodeGearそれぞれはモデル検査や、 特定の関数の中の処理が適しているかどうかの検査として見ることが出来ると考えられる。 | |
| 149 この事からGearsOSでは、 各CodeGearのモジュール化の仕組みであるInterface機能を導入した。 | |
| 150 | |
| 151 | |
| 152 # xv6のシステムコール以外の継続の分析 | |
| 153 | |
| 154 | |
| 155 | |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
156 # Basic Blockに基づく分析 |
| 15 | 157 |
| 158 xv6のファイルシステムに関する定義ファイルはfs.c中に記述されている。 | |
| 159 この中に出てくる関数に着目し、 この関数をさらにCodeGearに変換していくことで状態遷移単位での記述を試みた。 | |
| 160 | |
| 161 まず関数内でif文などの分岐を持たない基本単位であるBasic Blockに着目した。 | |
| 162 CbCのCodeGearの粒度はCの関数とアセンブラの中間であるといえるので、 BasicBlockをCodeGearに置き換える事が可能である。 | |
| 17 | 163 したがって特定の関数内の処理のBasicBlockを分析し、 BasicBlockに対応したCodeGearへ変換することで状態遷移系への変換を行った。 |
| 15 | 164 |
| 165 | |
|
29
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
166 |
|
5dbe39f52406
add readsyscall_state
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
167 # CbCを用いた部分的なxv6の書き換え |
| 27 | 168 |
| 169 CbCではCodeGear、 DataGearからなる単位を基本とし、 それぞれにメタなGearが付随する。 | |
| 170 また実行に必要なCodeGearとDataGearをまとめたcontextというMetaDataGearが存在する。 | |
| 171 この機能を元にxv6の書き換えを検討した。 | |
| 172 | |
| 173 xv6内でCbCの軽量継続に突入する際は、 元の処理関数に通常の方法では戻ってくることができず、部分的に書き換えていくのが困難である。 | |
| 174 今回は呼び出し関数に戻れるスタックフレームを操作したい為に、 ダミーの`void`関数を用意した。 | |
| 175 この関数内でCodeGearに`goto`文を用いて遷移することで、 CbCから帯域脱出した際に`void`関数の呼び出し元から処理を継続し、部分的にCbCに書き換えることが可能となった。 | |
| 176 Code\ref{src:dumy_function_cbc}では、 `userinit`関数へ戻るために、 `cbc_init_vmm_dumy`を経由している。 | |
| 177 | |
| 178 ``` lab:src:dumy_function_cbc, cap:部分的にCbCを適応する例 | |
| 179 void cbc_init_vmm_dummy(struct Context* cbc_context, struct proc* p, pde_t* pgdir, char* init, uint sz) | |
| 180 { | |
| 181 struct vm* vm = createvm_impl(cbc_context); | |
| 182 goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret); | |
| 183 } | |
| 184 | |
| 185 void userinit(void) | |
| 186 { | |
| 187 // omission | |
| 188 | |
| 189 if((p->pgdir = kpt_alloc()) == NULL) { | |
| 190 panic("userinit: out of memory?"); | |
| 191 } | |
| 192 | |
| 193 cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size); | |
| 194 | |
| 195 p->sz = PTE_SZ; | |
| 196 memset(p->tf, 0, sizeof(*p->tf)); | |
| 197 ``` |