まとめ

xv6の処理の一部を継続を用いてcbcで書き換えた diff -r 58349e71879a -r 76a8f55f23fa slide/slide.md --- a/slide/slide.md Wed May 27 16:02:23 2020 +0900 +++ b/slide/slide.md Wed May 27 22:03:59 2020 +0900 @@ -17,67 +17,71 @@ # 研究目的 -- アプリケーションの信頼性を向上させるたい - - その為には土台となる OS 自体の信頼性を高く保証したい +- アプリケーションの信頼性を向上させたい + - その為には土台となる OS 自体の信頼性が重要である - OSそのものも巨大なプログラムである - - テストコードを用いた方法で信頼性を確保する事が可能 -- しかし並列並行処理などに起因するバグや、そもそもOSを構成する処理が巨大 - - テストで完全にバグを発見するのは困難 - - テスト以外の方法でOSの信頼性を高めたい +- 並列並行処理などに起因するバグや、そもそもOSを構成する処理が巨大 + - テストコードを用いた方法で信頼性を確保することが困難 + - テストではなく定理証明とモデル検査でOSの信頼性を高めたい --- -# OSの信頼性 -- OSそのもの動作も保証されるべき -- アプリケーションが行いたい処理の他に、メモリやCPUの資源管理などが存在する - - アプリケーション側からするとOSの機能 -- 本来行いたい処理 - - ノーマルレベルと呼ぶ -- 資源管理など - - メタレベルと呼ぶ - - この別け方はOSの実装でも存在する -- ノーマル、メタレベルの計算の両方を保証しないといけない + +# ノーマルレベルとメタレベルを用いた信頼性の向上 + +- プログラムの実行部分は以下の2つからなる + - 入力と出力の関係を決める計算(ノーマルレベル) + - プログラムを実行したり、信頼性を保証するために必要な計算(メタレベル) +- メタレベルの例 + - メモリやCPUの資源管理 + - システムコールの動作(副作用) + - 並行実行(他のプロセスとの干渉) + - モデル検査(可能な実行を列挙する方式の実行) + - 証明(入力時と出力時の論理的な条件)、(invariant) +- メタレベルの計算として信頼性を保証する --- -# テスト以外で信頼性を高める方法 -- モデル検査 - - 実際に想定されるパターンを全て動かして検証する - - デッドロック発生の検知 - - JavaPathFinderなど -- 定理証明支援系 - - 論理学的なモデルに変更して証明する - - Agda - - Coq -- OSをこれらの方法で信頼性を高めたい - - +# モデル検査 +- 実際に想定されるパターンを全て動かして検証する +- デッドロック発生の検知 + - JavaPathFinderなど +- 状態爆発が問題になる +- Spinを用いる方法では、 promelaという言語で実装し直す必要がある --- -# OSの信頼性を高めるためには -- 既存のOSのソースコードをそのまま使うのは困難 -- モデル検査の場合 - - OS自体をモデル検査する機能をOSに組み込む必要がある -- 定理証明系の場合 - - Agda/CoqでOSを再実装する必要がある - - それらのコードはそのままコンパイルする事ができない -- ノーマルレベル/メタレベルを切り分けるのも困難 -- 動きつつ証明可能なOSを目指したい - - これらを同時に達成出来るプログラミング言語でOSを実装する必要がある +# 定理証明支援系 +- 論理学的なモデルに変更して証明する + - Agda + - Coq +- HoareLogicを用いる + - PreCondition -> Statement -> PostCondition +- 従来の方法ではStatementには限られたコマンドしか使えない + - ループは不変条件を使うが、条件を見つけることが一般的には困難 + - 実装言語と同じ記述で証明をすることはできない --- -# Continuation Based C -- ノーマルレベル/メタレベルの実装に適している言語 - - 通称CbC +# GearsOSでの信頼性の保証 +- メタレベルのみで信頼性の保証を行う + - ノーマルレベルでの記述は変更しない +- Continuation Based C(CbC)をつかって、ノーマルレベルとメタレベルの分離を行う - C言語の下位言語であり、いくつかのCコンパイラ上で実装している - - gcc - - llvm/clang - C言語の構文は使用可能だが、関数呼び出しの他に軽量継続を持つ - 関数呼び出し時のスタックの操作を行わず`jmp`命令で次の処理に移動する - schemaなどと違い環境を持たず継続するために軽量継続と呼ぶ --- -# CbCとCodeGear +# GearsOSでの信頼性の保証 + +- デフォルトのメタレベルの計算は自動生成される +- 資源管理あるいは検証用のメタ計算は必要に応じて挿入する +- これにより大きなコード変更無くモデル検査や定理証明を行うことができる +- モデル検査や定理証明の困難さはメタレベルのプログラミングとして吸収する + - 例えばOSで使用するデータ構造に合わせたモデル検査用の状態圧縮 + - OSの検証に利用できるinvariantの提供 + +--- +# CbCとCodeGear(ノーマルレベル) - 軽量継続で表現する単位をCodeGearと呼ぶ - CodeGearはCの関数とアセンブラの中間の様に使える - CodeGearは返り値の型の代わりに`__code`で宣言する @@ -97,11 +101,10 @@ - cbcで書き直したxv6の`read`システムコールの例 --- -# CbCの呼び出し +# cbcで書き直したシステムコールディスパッチの例 - CbCは`goto`文で呼び出す -- cbcで書き直したシステムコールディスパッチの例 - - 受け取ったシステムコール番号に対応するCodeGearに継続する + - 受け取ったシステムコール番号に対応するCodeGearに継続する ```c void syscall(void) @@ -116,9 +119,67 @@ ``` - 呼び出し元には返ってこない + - goto trapreturn() ユーザープログラムにディスパッチする + - goto panic() 致命的なエラーとしてOSを止める + - goto err() システムコールのエラー処理をしてユーザープログラムにディスパッチする + +--- + +# CbCを用いたソフトウェアの実装 + +- 計算を実行するためのメモリ領域が必要 + - MetaDataGearと呼ぶ +- メタレベルから見た実行ではcontextとして持ち歩く +- ノーマルレベルからはアクセスするDataGearのみが見えていて、ポインタなどは直接は見えない +- contextはプロセスごとに別に存在する +- kernel内で共有されているデータ構造 + - ページテーブル + - ファイル構造体 + - キャッシュやバッファ + - これらはkernel context内に置かれる --- + +# CbCのcotnext +- CbCのプログラムで利用するCodeGearとデータの組を管理する機能 + - データをDataGearという単位として扱う + - 計算で使用する各DataGearを実際に保存している +- ノーマルレベルのCodeGear間を遷移するようにプログラミングする + - ノーマルレベルからはCodeGearを直接操作できない + - メタ計算中でCodeGearの番号をcontextでディスパッチする + - この間にMetaCodeGearが実行される +- 実際のデータの入手、保存はcontextを触ることが出来るMeta Code Gearが行う + +--- + +# 通常のCbCプログラム + +- プログラマから見るとCodeGearからCodeGearへの継続のみに見える + + +--- + +# 実際のCbCプログラム + +- 実際は1度contextを参照するMetaCodeGearに継続する + - 番号から次のCodeGearに対応するMetaCodeGearを取り出す + + + +--- + +# 実際のCbCプログラム + +- MetaCodeGearでは次の計算に必要なDataGearを取り出す + - 全てのDataGearが確保できたらCodeGearにgotoする + + + + +--- + # CbCを用いたOSの再実装 + - CbCのCodeGearは状態遷移単位での記述に向いている - 状態遷移を基本としたモデルに変換し、HoareLogicなどの形式手法を用いて信頼性を高めたい - CbCは比較的文法が簡易 @@ -127,7 +188,9 @@ - 最初の段階として既存のOSをCbCで再実装する --- + # xv6 + - マサチューセッツ工科大学で開発されたv6OSをもとにしたOS - x86向けにANSI Cで実装されている - 比較的小さなUNIX @@ -139,40 +202,79 @@ --- -# xv6のCbCを用いた書き換え -- xv6をCbCで部分的に書き換えていく - - 今回はシステムコール部分の一部、メモリ管理部分、ファイルシステムなどを書き換えた -- 全てをCodeGearに書き換えてしまうとデータの管理やCodeGearの管理が困難になる - - スタックを持たないので、実際に利用するデータの管理はメタ計算などで処理をしたい -- OS内部でノーマルレベル/メタレベルの処理の切り分けをしたい - - メタな計算を行うCodeGearは直接呼び出したくない -- ノーマル/メタのCodeGearの切り分けと、データの管理をする構造を作成した + +# xv6のCbCでの書き換え +- 既存のOSを段階的にCbCで書き換えていく + - 一部スタックを持っている + - CbCでOSを実装する際のプロトタイプ実装としての段階 +- 今回はシステムコール部分の一部、メモリ管理部分、ファイルシステムなどを書き換えた +- CbCのcontextをプロセス構造体に埋め込み、 `goto`文を利用する場合はcontextからデータを参照する + +--- + +# read system callの書き換え +- xv6のシステムコールの一部を書き換えることを検討する +- 最初にread systemcallの処理をCodeGearへの書き換えを行った +- readシステムコールなのでreadする対象によって処理が分岐する + - ファイル + - inode + - コンソール +- 読む対象によってCodeGearを書き換えた + - スケジューラーに接続する箇所や、 sleepする箇所もCodeGearとして書き換える --- -# CbCのcotnext -- CbCのプログラムで利用するCodeGearとデータの組を管理する機能 - - データをDataGearという単位として扱う - - 計算で使用する各DataGearを実際に保存している -- ノーマルレベルのCodeGear間を遷移するようにプログラミングする - - ノーマルレベルからはCodeGearを直接操作できない - - メタ計算中でCodeGearの番号をcontextでディスパッチする - - この間にMetaCodeGearが実行される -- 実際のデータの入手、保存はcontextを触ることが出来るMeta Code Gearが行う + +# read system callの継続の一部 + +- 実際に処理を切り分けているCodeGear + - ファイルの`type`によって継続先を変更する + +```c +__code cbc_fileread (struct file *f, char *addr, int n, __code (*next)(int ret)) +{ + if (f->readable == 0) { + goto next(-1); + } + + if (f->type == FD_PIPE) { + goto cbc_piperead(f->pipe, addr, n, next); + } + + if (f->type == FD_INODE) { + ilock(f->ip); + proc->cbc_arg.cbc_console_arg.f = f; + goto cbc_readi(f->ip, addr, f->off, n, cbc_fileread1); + } + + goto cbc_panic("fileread"); +} +``` + --- -プログラマから見るとCodeGearからCodeGearへの継続のみ - + +# read システムコールの状態遷移図 + +- システムコール中のCodeGearを状態遷移図にした + - 自然言語で説明可能となる利点がある + --- -実際は1度contextを参照するMetaCodeGearに継続する -- 番号から次のCodeGearに対応するMetaCodeGearを取り出す + +# Basic Block単位での書き換え - +- Basic Blockとはコンパイラの用語でループやリターンを区切りとするプログラミング単位 + - 長くかかるループは間にgotoを挟むことによりメタ計算を間にいれる + - 1つのCodeGearにいる間は(論理的に)preemptされないことを保証する +- これによりCodeGearを割り込まれない検証の単位とする事ができる +- 仮想メモリ管理やファイルシステムなどの関数はxv6の場合Cのファイル単位でまとまっている + - CodeGear用のAPIをいきなり設計するのではなく、段階的に書き換える +- 今回はこれらの関数の内容をCodeGearで書き直した + - 各関数への呼び出し時にダミーの関数を呼び出すことでCとCbCの相互移動が可能 --- -# read system callの書き換え -- xv6のシステムコールの一部を書き換えることを検討する -- 素直にread systemcallの処理をCodeGearに変換していく + +# メモリ管理部分の書き換え ---

xv6の構成要素の継続の分析

研究目的

OSの信頼性

テスト以外で信頼性を高める方法

OSの信頼性を高めるためには

Continuation Based C

CbCとCodeGear

CbCの呼び出し

CbCを用いたソフトウェアの実装

CbCのcotnext

通常のCbCプログラム

実際のCbCプログラム

実際のCbCプログラム

CbCのcotnext

CbCを用いたOSの再実装

xv6

xv6のCbCを用いた書き換え

xv6のCbCでの書き換え

CbCのcotnext

read system callの書き換え

read system callの継続の一部

read システムコールの状態遷移図

Basic Block単位での書き換え

メモリ管理部分の書き換え

まとめ