Mercurial > hg > Papers > 2020 > tobaru-master
view slide/CbCXv6.md @ 18:afc36230cf4f
slide chapter3,4
| author | tobaru |
|---|---|
| date | Fri, 07 Feb 2020 20:06:13 +0900 |
| parents | |
| children | 98cee2f6c919 |
line wrap: on
line source
# CbCインターフェースによる CbCXv6 の書き換え - 並列信頼研 - 桃原 優 --- # 目次 1. **OS の信頼性の保証** 2. CbC による Gears OS の開発 3. Xv6 4. CbCXv6 での Paging 5. CbC インターフェース 6. 評価 7. まとめ --- # OS の信頼性の重要性 - OS のバグは日常生活に支障をきたす - パスワードなしで root にアクセスできるバグ - 日付設定でコンピュータが壊れる - -> OS自体に信頼性が求められる --- # OS の信頼性の重要性 - 全てのOSのコードに対して検証を行うのは困難 - 複雑な機能が多い - 短期間のアップデート - ユーザーが検証を行うこともできない - 資源管理はOSが行なってる - そもそも資源管理が複雑 - アクセスされたり書き換えられるリスク --- # メタレベルとノーマルレベル - ノーマルレベル - ユーザーがプログラミング言語によって記述する部分の処理 - メタレベル - ユーザーが記述しないOS 側の処理 - CPU - メモリ --- # Continuation based C - ノーマルレベルとメタレベルの処理を同じ言語で行えるようにした言語(以下CbC) - Code Gear - 基本的な処理の単位 - Data Gear - データの単位 --- # goto による継続 - Code Gear の処理の間を goto によって遷移していく  --- # Data Gear の継続 - goto の際に Data Gear も継続される  --- # Meta Code Gear - 実際にはノーマルレベルの間にメタレベルの処理がある - Meta Level では Data Gear の見え方は変わる(Meta Data Gear)  --- # 状態遷移モデル - goto の遷移によって状態遷移モデルに落とし込める - Code Gear に対しての入力に対して期待される出力がされているかで検査して**信頼性を保証する** ---- # Agda による検証 - モデル検査 - 定理証明支援系である Agda を用いる。 - Agda - Haure Logic という検証手法を扱える。 --- # Haure Logic - 検証手法 - 事前条件を使ってある関数を実行して事後条件を満たすことを確認する - CbCと相性がいい - 継続に事前条件(Input Data Gear)と事後条件(Output Data Gear)を持たせることができる --- # Geas OS - CbC を使って信頼性の保証と拡張性を持たせる Gears OS の開発を行なっている - Xv6 という OS を参考に書き換えをしている --- # メモリ管理 - OS の信頼性の1つであるメモリ管理部分を CbC で書き換える - Page のバリデーションチェック - サンドボックスによるエクセプション --- # インターフェース - 書き換えを防ぐために見える Data Gear に違いが生じる - -> Gears OS のノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入 - 機能の入れ替えによる他のメリット - 煩雑な記述の解消 - 機能の入れ替え - Agda による証明 --- # 目次 1. OS の信頼性の保証 2. **CbC による Gears OS の開発** 3. Xv6 4. CbCXv6 での Paging 5. CbC インターフェース 6. 評価 7. まとめ --- # CbC による Gears OS の開発 - a --- # Context - a --- # 目次 1. OS の信頼性の保証 2. CbC による Gears OS の開発 3. **Xv6** 4. CbCXv6 での Paging 5. CbC インターフェース 6. 評価 7. まとめ --- # Xv6 - MIT の講義用教材として作られたOS - 企画課される前のCで書かれたUNIX V6 を書き換えた - 1万行程の軽量なOS - Linuxだと数千万行 - Xv6 を参考に CbC で書き直すことで Gears OS を実装する --- # カーネル空間 - OS の中核となるプログラムで Meta Level に相当する - Xv6 ではカーネルとユーザープログラムは分離されている - ユーザープログラムはカーネルに直接アクセスできない。 - 書き換えやアクセスを防ぐため - 呼び出す場合は system call --- # カーネルが提供するもの - プロセス管理 - メモリ管理 - ファイル管理 - I/O, read, write --- # カーネルの保護機構 - CPUのハードウェア保護機構を持っている - ユーザー空間で実行されているプロセスが自身のメモリのみアクセスできるように保護 - system call - ハードウェアが一時的に特権レベルをあげ、カーネルのプログラムが実行される --- # system call - system call 呼び出し - トラップ の発生 - ユーザープログラムの中断 - 処理がカーネルに切り替わる --- # system call - ソースコード載せる --- # Xv6-rpi - Xv6 は Arm のバイナリを出力するので様々なハードウェアで動かすことができる - Raspberry Pi - 携帯電話 - 実際にRaspberry Pi で動かすために xv6-rpi を用意して動作しているかコンソールで確認中 - CbCxv6 とは別 --- # 目次 1. OS の信頼性の保証 2. CbC による Gears OS の開発 3. Xv6 4. **CbCXv6 での Paging** 5. CbC インターフェース 6. 評価 7. まとめ --- # CbCXv6 での Paging - OS の信頼性の1つであるメモリ管理部分の書き換えについて説明 --- # 実メモリの直接操作 - 実メモリを直接扱うと様々な問題が生じる - ユーザープログラムで空いているメモリ番地を探す必要 - フラグメンテーションが起こる - メモリ間に扱うには小さな隙間ができる --- # Paging - メモリ管理の手法 - Page と呼ばれる固定長のブロックに分割して、メモリとスワップ領域で Page を入れ替えて管理 - 仮想メモリとして扱うことでフラグメンテーションの解消と空き番地を探す必要がなくなる --- # Pagingの図 - 必要？ --- # メタレベルでの Paging の操作 - Page Table に相当するデータを Input Data Gear で受け取って変更した後、Context にある Meta Data Gear に goto で遷移してアクセス - メタレベルで処理することで本来カーネル側の処理である Page Table を操作できる --- # Paging の信頼性 - Input Data Gear に対しての Output Data Gear をバリデーションチェックすることで他のプロセスから書き換えられることを防ぐ - サンドボックス - 他のプロセスから書き換えられた時にエクセプションを飛ばす --- # Paging の書き換え - Xv6 では実メモリから仮想メモリの変換をvm.cで行なっている。 - 次の章で書き換えについて説明する --- # 目次 1. OS の信頼性の保証 2. CbC による Gears OS の開発 3. Xv6 4. CbCXv6 での Paging** 5. **CbC インターフェース** 6. 評価 7. まとめ ---