# HG changeset patch # User tobaru # Date 1581158710 -32400 # Node ID 49d691a92b413797b8ec05cacd9d099bfd187094 # Parent a60721938bf1f174a74f04953c1b254c54fda788 fix slide diff -r a60721938bf1 -r 49d691a92b41 slide/CbCXv6.md --- a/slide/CbCXv6.md Sat Feb 08 19:03:35 2020 +0900 +++ b/slide/CbCXv6.md Sat Feb 08 19:45:10 2020 +0900 @@ -5,42 +5,33 @@ --- # 概要 -- OS の信頼性を保証したい -- メタレベルを記述できる CbC で OS の開発 -- インターフェースの導入 - - 煩雑な記述の解消 - - Agdaによる証明のため +- OS の信頼性を上げたい +- CbCを使って xv6 を書き換える +- Paging の書き換えを行った +- まだ実装中 +- 将来はコンテナやVMをメタ計算として実装できるはず --- -# OS の信頼性の重要性 -- OS のバグは日常生活に支障をきたす - - パスワードなしで root にアクセスできるバグ - - 日付設定でコンピュータが壊れる - - -> OS自体に信頼性が求められる - ---- - -# OS の検証 - -- 全てのOSのコードに対して検証を行うのは困難 - - 複雑な機能が多い - - 短期間のアップデート - -- ユーザーが検証を行うこともできない - - 資源管理はOSが行なってる - - そもそも資源管理が複雑 - - アクセスされたり書き換えられるリスク +# OS の信頼性を上げたい +- 仕様を満たすことを証明する +- 証明しやすい形の記述を作る +- CbCの goto で書く + - 状態遷移系に近い形で記述できる + - 関数型の記述 +- CbCのinterface で書く +- 記述のモジュール化 --- # メタレベルとノーマルレベル - ノーマルレベル - - ユーザーがプログラミング言語によって記述する部分の処理 + - CbCで記述される普通のアルゴリズム - メタレベル - - ユーザーが記述しないOS 側の処理 - - CPU - - メモリ + - Paging などのメモリやCPU自体の操作 + - プログラムの正しさの証明 +- Context + - メタレベルで使用される Meta Data を置く場所 --- @@ -48,8 +39,15 @@ - ノーマルレベルとメタレベルの処理を同じ言語で行えるようにした言語(以下CbC) - Code Gear - 基本的な処理の単位 + - goto 文で遷移する - Data Gear - データの単位 +- Meta Code Gear + - goto meta + - Code Gear の間に挟める計算 +- Meta Data Gear + - Context + - Code Gearの間の接続など --- @@ -69,50 +67,6 @@ --- -# Meta Code Gear -- 実際にはノーマルレベルの間にメタレベルの処理がある -- Meta Level では Data Gear の見え方は変わる(Meta Data Gear) - - 書き換えやアクセスを防ぐため - -![](https://i.imgur.com/vy0NxrG.png) - ---- - -# 状態遷移モデル -- goto の遷移によって状態遷移モデルに落とし込める -- Code Gear に対しての入力に対して期待される出力がされているかで検査して**信頼性を保証する** - ----- - -# Agda による検証 -- モデル検査 - - 定理証明支援系である Agda を用いる。 -- Agda - - Hoare Logic という検証手法を扱える。 - ---- - -# Hoare Logic -- 検証手法 - - 事前条件を使ってある関数を実行して事後条件を満たすことを確認する -- CbCと相性がいい - - 継続に事前条件(Input Data Gear)と事後条件(Output Data Gear)を持たせることができる - ---- - -# Geas OS -- CbC を使って信頼性の保証と拡張性を持たせる Gears OS の開発を行なっている -- Xv6 という OS を参考に書き換えをしている - ---- - -# メモリ管理 -- OS の信頼性の1つであるメモリ管理部分を CbC で書き換える - - Page のバリデーションチェック - - サンドボックスによるエクセプション - ---- - # インターフェース - 書き換えを防ぐために見える Data Gear に違いが生じる - -> Gears OS のノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入 @@ -123,23 +77,18 @@ --- -# CbC による Gears OS の開発 + +# Meta Code Gear +- 実際にはノーマルレベルの間にメタレベルの処理がある +- Meta Level では Data Gear の見え方は変わる(Meta Data Gear) + - 書き換えやアクセスを防ぐため + +![](https://i.imgur.com/vy0NxrG.png) --- -# Context -- Meta Data Gear - - Code Gear - - Data Gear のリスト - - Data Gear を確保するメモリ空間 -- スレッドやプロセスに対応 -- ノーマルレベルに必要な処理のみ Code Gear に渡す -- Meta Code Gear は Perlスクリプトで自動生成 -- 継続先を変えることで機能を置き換えることも可能 - ---- - -# Xv6 +# Geas OS +- Xv6 をCbCで書き換える - MIT の講義用教材として作られたOS - 企画課される前のCで書かれたUNIX V6 を書き換えた - 1万行程の軽量なOS @@ -148,6 +97,24 @@ --- + +# Xv6の構成 +- systemcall +- Scheduler +- VM +- file system +- tty + + +--- + +# Context +- Meta Data Gear +- ユーザープロセスに対応して1つのcontextがある +- Contextには実行されるすべてのCode Gear が登録される +- Data GearもContext上にある + +--- # カーネル空間 - OS の中核となるプログラムで Meta Level に相当する - Xv6 ではカーネルとユーザープログラムは分離されている @@ -157,55 +124,15 @@ --- -# カーネルが提供するもの -- プロセス管理 -- メモリ管理 -- ファイル管理 - - I/O, read, write - - ---- - -# カーネルの保護機構 -- CPUのハードウェア保護機構を持っている -- ユーザー空間で実行されているプロセスが自身のメモリのみアクセスできるように保護 -- system call - - ハードウェアが一時的に特権レベルをあげ、カーネルのプログラムが実行される - ---- - # system call - system call 呼び出し - トラップ の発生 - ユーザープログラムの中断 - 処理がカーネルに切り替わる ---- - -# Xv6-rpi -- Xv6 は　Arm のバイナリを出力するので様々なハードウェアで動かすことができる - - Raspberry Pi - - 携帯電話 -- 実際にRaspberry Pi で動かすために xv6-rpi を用意して動作しているか確認中 - - CbCxv6 とは別のプロジェクト - ---- - # CbCXv6 での Paging -- OS の信頼性の1つであるメモリ管理部分の書き換えについて説明 - ---- - -# 実メモリの直接操作 -- 実メモリを直接扱うと様々な問題が生じる - - ユーザープログラムで空いているメモリ番地を探す必要 - - フラグメンテーションが起こる - - メモリ間に扱うには小さな隙間ができる - ---- - -# Paging -- メモリ管理の手法 +- OS の信頼性の1つであるメモリ管理部分 +- メモリ管理するpage table - Page と呼ばれる固定長のブロックに分割して、メモリとスワップ領域で Page を入れ替えて管理 - 仮想メモリとして扱うことでフラグメンテーションの解消と空き番地を探す必要がなくなる @@ -217,37 +144,6 @@ --- - -# メタレベルでの Paging の操作 -- Page Table に相当するデータを Input Data Gear で受け取って変更した後、Context にある Meta Data Gear に goto で遷移してアクセス -- メタレベルで処理することで本来カーネル側の処理である Page Table を操作できる - ---- - -# Paging の信頼性 -- Input Data Gear に対しての Output Data Gear をバリデーションチェックすることで他のプロセスから書き換えられることを防ぐ -- サンドボックス - - 他のプロセスから書き換えられた時にエクセプションを飛ばす - ---- - -# Paging の書き換え -- Xv6 では実メモリから仮想メモリの変換をvm.cで行なっている。 -- 次の章で書き換えについて説明する - - - ---- - -# CbC インターフェースの導入 -- 継続の記述が煩雑になる - - Code Gear がどの Data Gear の番号に対応するか指定する必要がある - - ノーマルレベルとメタレベルで Data Gear の見え方が異なるため調整する必要がある -- ->インターフェースの導入 - - ---- - # CbC インターフェース - インターフェースは Data Gear に対しての操作を行う Code Gear - 実装は別で定義し、呼び出す @@ -277,6 +173,9 @@ --- +# init_vmm + + # Code Gear の定義 - Code Gear は __Code CodeGear名(引数); で記述する - 第1引数の Impl* vm が Code Gear の型になる