Papers/2020/tobaru-master: slide/CbCXv6.md comparison

comparison slide/CbCXv6.md @ 23:49d691a92b41

fix slide

author	tobaru
date	Sat, 08 Feb 2020 19:45:10 +0900
parents	6d84ce92ff35
children	69ac4230c3f2

comparison

equal deleted inserted replaced

-:a60721938bf1
+:49d691a92b41
 - 桃原 優
 ---
 # 概要
-- OS の信頼性を保証したい
+- OS の信頼性を上げたい
-- メタレベルを記述できる CbC で OS の開発
+- CbCを使って xv6 を書き換える
-- インターフェースの導入
+- Paging の書き換えを行った
-- 煩雑な記述の解消
+- まだ実装中
-- Agdaによる証明のため
+- 将来はコンテナやVMをメタ計算として実装できるはず
 ---
-# OS の信頼性の重要性
+# OS の信頼性を上げたい
-- OS のバグは日常生活に支障をきたす
+- 仕様を満たすことを証明する
-- パスワードなしで root にアクセスできるバグ
+- 証明しやすい形の記述を作る
-- 日付設定でコンピュータが壊れる
+- CbCの goto で書く
-- -> OS自体に信頼性が求められる
+- 状態遷移系に近い形で記述できる
+- 関数型の記述
----
+- CbCのinterface で書く
+- 記述のモジュール化
-# OS の検証
-- 全てのOSのコードに対して検証を行うのは困難
-- 複雑な機能が多い
-- 短期間のアップデート
-- ユーザーが検証を行うこともできない
-- 資源管理はOSが行なってる
-- そもそも資源管理が複雑
-- アクセスされたり書き換えられるリスク
 ---
 # メタレベルとノーマルレベル
 - ノーマルレベル
-- ユーザーがプログラミング言語によって記述する部分の処理
+- CbCで記述される普通のアルゴリズム
 - メタレベル
-- ユーザーが記述しないOS 側の処理
+- Paging などのメモリやCPU自体の操作
-- CPU
+- プログラムの正しさの証明
-- メモリ
+- Context
+- メタレベルで使用される Meta Data を置く場所
 ---
 # Continuation based C
 - ノーマルレベルとメタレベルの処理を同じ言語で行えるようにした言語(以下CbC)
 - Code Gear
 - 基本的な処理の単位
+- goto 文で遷移する
 - Data Gear
 - データの単位
+- Meta Code Gear
+- goto meta
+- Code Gear の間に挟める計算
+- Meta Data Gear
+- Context
+- Code Gearの間の接続など
 ---
 # goto による継続
 # Data Gear の継続
 - goto の際に Data Gear も継続される
 ![](https://i.imgur.com/3E0DGWA.png)
----
-# 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 に違いが生じる
 - 機能の入れ替え
 - Agda による証明
 ---
-# CbC による Gears OS の開発
+# Meta Code Gear
----
+- 実際にはノーマルレベルの間にメタレベルの処理がある
+- Meta Level では Data Gear の見え方は変わる(Meta Data Gear)
-# Context
+- 書き換えやアクセスを防ぐため
-- Meta Data Gear
-- Code Gear
+![](https://i.imgur.com/vy0NxrG.png)
-- Data Gear のリスト
-- Data Gear を確保するメモリ空間
+---
-- スレッドやプロセスに対応
-- ノーマルレベルに必要な処理のみ Code Gear に渡す
+# Geas OS
-- Meta Code Gear は Perlスクリプトで自動生成
+- Xv6 をCbCで書き換える
-- 継続先を変えることで機能を置き換えることも可能
----
-# Xv6
 - MIT の講義用教材として作られたOS
 - 企画課される前のCで書かれたUNIX V6 を書き換えた
 - 1万行程の軽量なOS
 - Linuxだと数千万行
 - Xv6 を参考に CbC で書き直すことで Gears OS を実装する
 ---
+# Xv6の構成
+- systemcall
+- Scheduler
+- VM
+- file system
+- tty
+---
+# Context
+- Meta Data Gear
+- ユーザープロセスに対応して1つのcontextがある
+- Contextには実行されるすべてのCode Gear が登録される
+- Data GearもContext上にある
+---
 # カーネル空間
 - OS の中核となるプログラムで Meta Level に相当する
 - Xv6 ではカーネルとユーザープログラムは分離されている
 - ユーザープログラムはカーネルに直接アクセスできない。
 - 書き換えやアクセスを防ぐため
 - 呼び出す場合は system call
 ---
-# カーネルが提供するもの
-- プロセス管理
-- メモリ管理
-- ファイル管理
-- 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つであるメモリ管理部分の書き換えについて説明
+- OS の信頼性の1つであるメモリ管理部分
+- メモリ管理するpage table
----
-# 実メモリの直接操作
-- 実メモリを直接扱うと様々な問題が生じる
-- ユーザープログラムで空いているメモリ番地を探す必要
-- フラグメンテーションが起こる
-- メモリ間に扱うには小さな隙間ができる
----
-# Paging
-- メモリ管理の手法
 - Page と呼ばれる固定長のブロックに分割して、メモリとスワップ領域で Page を入れ替えて管理
 - 仮想メモリとして扱うことでフラグメンテーションの解消と空き番地を探す必要がなくなる
 ---
 - 必要？
 ![](https://i.imgur.com/ZNxOsNf.png)
 ---
-# メタレベルでの 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
 - 実装は別で定義し、呼び出す
 - インターフェースによって機能を置き換えることができる
 ``` c
 typedef struct vm<Type,Impl> {
 ```
 ---
+# init_vmm
 # Code Gear の定義
 - Code Gear は __Code CodeGear名(引数); で記述する
 - 第1引数の Impl* vm が Code Gear の型になる
 - 初期化された Data Gear が それぞれの Code Gear の引数として扱われる

Mercurial > hg > Papers > 2020 > tobaru-master

comparison slide/CbCXv6.md @ 23:49d691a92b41