GearsOSのメタ計算

# HG changeset patch # User anatofuz # Date 1612003365 -32400 # Node ID 657784b3bae13d4306d647135368ee3acd1d938d # Parent d9c29dddf64f5d70d62475ecb61faccc7b2b8886 add slide diff -r d9c29dddf64f -r 657784b3bae1 paper/chapter/introduction.tex --- a/paper/chapter/introduction.tex Sat Jan 30 19:10:07 2021 +0900 +++ b/paper/chapter/introduction.tex Sat Jan 30 19:42:45 2021 +0900 @@ -37,9 +37,9 @@ 例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。 OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。 -しかしOSの処理は膨大であり、様々な関数呼び出しや非決定的な処理、並行処理などが発生する。 -モデル検査を行う場合でも、やみくもにOSのすべての処理を検査するのは難しい。 -モデル検査自体が巨大な状態の検証を行うため、状態を有限に制限したり抽象化を行う必要がある。 +しかしOSの処理は膨大である。 +すべての存在可能な状態を数え上げるモデル検査では状態爆発が問題となる。 +状態を有限に制限したり抽象化を行う必要がある。 OSのシステムコールは、ユーザーからAPI経由で呼び出され、いくつかの処理を行う。 @@ -54,10 +54,14 @@ これはプログラマが通常プログラミングするものである。それ以外にデータをメモリに保存するためにメモリのアロケーションをする処理や、メモリから値を持ってくる処理が入る。メモリのほかにCPUの資源管理なども必要となる。 -さらにオブジェクト型の整合性の為にキャストなどの型変換が必要となる場合もある。 +ユーザーレベルから見ると、データの読み込みなどは資源へのアクセスが必要であるため、システムコールを呼ぶ必要がある。 +システムコール自体もメタ計算である。ユーザーが本来やりたい計算以外に、資源管理などのこれら計算を行う上でやらなければならない計算が存在する。前者の計算をノーマルレベルの計算と呼び、後者をメタレベルの計算と呼ぶ。 -プログラムの整合性の検証はメタレベルの計算と考えられる。 +ノーマルレベルの計算を確実に行う為には、メタレベルの計算が重要となる。 + + +プログラムの整合性の検証はメタレベルの計算で行いたい。ユーザーが実装したノーマルレベルの計算に対応するメタレベルの計算を、自由にメタレベルの計算で証明したい。またメタレベルで検証ががすでにされたプログラムがあった場合、都度実行ユーザーの環境で検証が行われるとパフォーマンスに問題が発生する。この場合はメタレベルの計算を検証をするもの、しないものと切り替えられる柔軟なAPIが必要となる。 diff -r d9c29dddf64f -r 657784b3bae1 paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r d9c29dddf64f -r 657784b3bae1 slide/slide.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/slide.html Sat Jan 30 19:42:45 2021 +0900 @@ -0,0 +1,51 @@ +GearsOSのメタ計算

\ No newline at end of file diff -r d9c29dddf64f -r 657784b3bae1 slide/slide.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/slide.md Sat Jan 30 19:42:45 2021 +0900 @@ -0,0 +1,243 @@ +--- +marp: true +title: GearsOSのメタ計算 +paginate: true +--- + + +# GearsOSのメタ計算 + +- 清水隆博 + - 198584B + - 河野研 + + +--- + +# 研究目的 + +- アプリケーションの信頼性を向上させたい + - その為には土台となる OS 自体の信頼性が重要である +- OSそのものも巨大なプログラム +- 並列並行処理など起因するバグや、そもそもOSを構成する処理が巨大 + - テストコードで信頼性を保証しきれない +- 形式手法を用いて信頼性を保証したい + - モデル検査 + +--- + +# ノーマルレベルとメタレベルを用いた信頼性の向上 + +- プログラムの実行部分は以下の2つからなる + - 入力と出力の関係を決める計算(ノーマルレベル) + - プログラムを実行したり、信頼性を保証するために必要な計算(メタレベル) +- メタレベルの例 + - メモリやCPUの資源管理 + - システムコールの動作(副作用) + - 並行実行(他のプロセスとの干渉) + - モデル検査(可能な実行を列挙する方式の実行) + - 証明(入力時と出力時の論理的な条件)、(invariant) +- メタレベルの計算として信頼性を保証する + +--- + +# モデル検査 +- 実際に想定されるパターンを全て動かして検証する +- デッドロック発生の検知 + - JavaPathFinderなど +- 状態爆発が問題になる +- Spinを用いる方法では、 promelaという言語で実装し直す必要がある + +--- + +# 定理証明支援系 +- 論理学的なモデルに変更して証明する + - Agda + - Coq +- HoareLogicを用いる + - PreCondition -> Statement -> PostCondition +- 従来の方法ではStatementには限られたコマンドしか使えない + - ループは不変条件を使うが、条件を見つけることが一般的には困難 + - 実装言語と同じ記述で証明をすることはできない + +--- +# GearsOSでの信頼性の保証 +- メタレベルのみで信頼性の保証を行う + - ノーマルレベルでの記述は変更しない +- Continuation Based C(CbC)をつかって、ノーマルレベルとメタレベルの分離を行う +- C言語の下位言語であり、いくつかのCコンパイラ上で実装している +- C言語の構文は使用可能だが、関数呼び出しの他に軽量継続を持つ + - 関数呼び出し時のスタックの操作を行わず`jmp`命令で次の処理に移動する + - schemaなどと違い環境を持たず継続するために軽量継続と呼ぶ + +--- +# GearsOSでの信頼性の保証 + +- デフォルトのメタレベルの計算は自動生成される +- 資源管理あるいは検証用のメタ計算は必要に応じて挿入する +- これにより大きなコード変更が無くモデル検査や定理証明を行うことができる +- モデル検査や定理証明の困難さはメタレベルのプログラミングとして吸収する + - 例えばOSで使用するデータ構造に合わせたモデル検査用の状態圧縮 + - OSの検証に利用できるinvariantの提供 +- CbCを用いたOSであるGearsOSを開発している + +--- +# CbCとCodeGear(ノーマルレベル) +- 軽量継続で表現する単位をCodeGearと呼ぶ +- CodeGearはCの関数とアセンブラの中間の様に使える +- CodeGearは返り値の型の代わりに`__code`で宣言する + +``` +__code cbc_read(__code (*next)(int ret)){ + struct file *f; + int n; + char *p; + + if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) { + goto next(-1); + } + goto cbc_fileread(f, p, n, next); +} +``` +- cbcで書き直したxv6の`read`システムコールの例 + + +--- +# CbCとCodeGear(メタレベル) + +- `cbc_read_stub`内で必要な引数をcontextから取り出す + - 取得するものがなければノーマルレベルのCodeGearに継続する + +```c +__code cbc_read_stub(struct Context* cbc_context, enum Code next) { + goto cbc_read(cbc_context, next); +} +``` + +--- +# cbcで書き直したシステムコールディスパッチの例 + +- CbCは`goto`文で呼び出す + - 受け取ったシステムコール番号に対応するCodeGearに継続する + +```c +void syscall(void) +{ + int num; + int ret; + + if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) { + proc->cbc_arg.cbc_console_arg.num = num; + goto (cbccodes[num])(cbc_ret); + } +``` + + +--- + +# ノーマルレベルとメタレベルを用いた信頼性の向上 + +- プログラムの実行部分は以下の2つからなる + - 入力と出力の関係を決める計算(ノーマルレベル) + - プログラムを実行したり、信頼性を保証するために必要な計算(メタレベル) +- メタレベルの例 + - メモリやCPUの資源管理 + - システムコールの動作(副作用) + - 並行実行(他のプロセスとの干渉) + - モデル検査(可能な実行を列挙する方式の実行) + - 証明(入力時と出力時の論理的な条件)、(invariant) +- メタレベルの計算として信頼性を保証する + +--- + +# モデル検査 +- 実際に想定されるパターンを全て動かして検証する +- デッドロック発生の検知 + - JavaPathFinderなど +- 状態爆発が問題になる +- Spinを用いる方法では、 promelaという言語で実装し直す必要がある + +--- + +# 定理証明支援系 +- 論理学的なモデルに変更して証明する + - Agda + - Coq +- HoareLogicを用いる + - PreCondition -> Statement -> PostCondition +- 従来の方法ではStatementには限られたコマンドしか使えない + - ループは不変条件を使うが、条件を見つけることが一般的には困難 + - 実装言語と同じ記述で証明をすることはできない + +--- +# GearsOSでの信頼性の保証 +- メタレベルのみで信頼性の保証を行う + - ノーマルレベルでの記述は変更しない +- Continuation Based C(CbC)をつかって、ノーマルレベルとメタレベルの分離を行う +- C言語の下位言語であり、いくつかのCコンパイラ上で実装している +- C言語の構文は使用可能だが、関数呼び出しの他に軽量継続を持つ + - 関数呼び出し時のスタックの操作を行わず`jmp`命令で次の処理に移動する + - schemaなどと違い環境を持たず継続するために軽量継続と呼ぶ + +--- +# GearsOSでの信頼性の保証 + +- デフォルトのメタレベルの計算は自動生成される +- 資源管理あるいは検証用のメタ計算は必要に応じて挿入する +- これにより大きなコード変更が無くモデル検査や定理証明を行うことができる +- モデル検査や定理証明の困難さはメタレベルのプログラミングとして吸収する + - 例えばOSで使用するデータ構造に合わせたモデル検査用の状態圧縮 + - OSの検証に利用できるinvariantの提供 +- CbCを用いたOSであるGearsOSを開発している + +--- +# CbCとCodeGear(ノーマルレベル) +- 軽量継続で表現する単位をCodeGearと呼ぶ +- CodeGearはCの関数とアセンブラの中間の様に使える +- CodeGearは返り値の型の代わりに`__code`で宣言する + +``` +__code cbc_read(__code (*next)(int ret)){ + struct file *f; + int n; + char *p; + + if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) { + goto next(-1); + } + goto cbc_fileread(f, p, n, next); +} +``` +- cbcで書き直したxv6の`read`システムコールの例 + + +--- +# CbCとCodeGear(メタレベル) + +- `cbc_read_stub`内で必要な引数をcontextから取り出す + - 取得するものがなければノーマルレベルのCodeGearに継続する + +```c +__code cbc_read_stub(struct Context* cbc_context, enum Code next) { + goto cbc_read(cbc_context, next); +} +``` + +--- +# cbcで書き直したシステムコールディスパッチの例 + +- CbCは`goto`文で呼び出す + - 受け取ったシステムコール番号に対応するCodeGearに継続する + +```c +void syscall(void) +{ + int num; + int ret; + + if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) { + proc->cbc_arg.cbc_console_arg.num = num; + goto (cbccodes[num])(cbc_ret); + } +``` +---

GearsOSのメタ計算

目次