CbCインターフェースによる CbCXv6 の書き換え

並列信頼研
桃原優

OS の信頼性の重要性

OS のバグは日常生活に支障をきたす +

概要

OS の信頼性を上げたい
CbCを使って xv6 という OS を書き換える
Paging の書き換えを行った
まだ実装中
将来はコンテナやVMをメタ計算として実装できるはず

OS の信頼性を上げたい

仕様を満たすことを証明する
証明しやすい形の記述を作る
CbCの goto で書く
- パスワードなしで root にアクセスできるバグ
- 日付設定でコンピュータが壊れる
- -> OS自体に信頼性が求められる
- 状態遷移系に近い形で記述できる(証明しやすい)
- 関数型の記述

OS の信頼性の重要性

-
全てのOSのコードに対して検証を行うのは困難
-
- 複雑な機能が多い
- 短期間のアップデート
-
-
ユーザーが検証を行うこともできない
-
- 資源管理はOSが行なってる
- そもそも資源管理が複雑
- アクセスされたり書き換えられるリスク
-

メタレベルとノーマルレベル

CbCのinterface で書く
記述のモジュール化

メタレベルとノーマルレベル

ノーマルレベル
- ユーザーがプログラミング言語によって記述する部分の処理
- CbCで記述される普通のアルゴリズム
メタレベル
- ユーザーが記述しないOS 側の処理 -
  - CPU
  - メモリ
  - Paging などのメモリやCPU自体の操作
  - プログラムの正しさの証明
- Context +
  - メタレベルで使用される Meta Data を置く場所
Continuation based C
Continuation based C
- ノーマルレベルとメタレベルの処理を同じ言語で行えるようにした言語(以下CbC)
- Code Gear
  - 基本的な処理の単位
  - goto 文で遷移する
- Data Gear @@ -97,212 +84,125 @@
- データの単位
Meta Code Gear +
- goto meta
- Code Gear の間に挟める計算
+
Meta Data Gear +
- Context
- Code Gearの間の接続など
+

goto による継続

Code Gear の処理の間を goto によって遷移していく

Data Gear の継続

Code 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 による証明
-

CbC による Gears OS の開発

Context

Xv6

Meta Data Gear

CbC では接続可能な Code Gear, Data Gear のリスト
Data Gear を確保するメモリ空間
ノーマルレベルでの書き換えやアクセスを防ぐために存在

Xv6

MIT の講義用教材として作られたOS
- 企画課される前のCで書かれたUNIX V6 を書き換えた
- 規格化される前のCで書かれたUNIX V6 を書き換えた
- 1万行程の軽量なOS
- Linuxだと数千万行
Xv6 を参考に CbC で書き直すことで Gears OS を実装する
Xv6 をCbCで書き換える

Xv6の構成

systemcall
Scheduler
Virtual Memory
file system
tty

カーネル空間

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 とは別
-

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 をバリデーションチェックすることで他のプロセスから書き換えられることを防ぐ
サンドボックス +

Xv6の書き換え方針

+
メタレベルとノーマルレベルを記述できるOSを実装したい
+
+
段階的に書き換えていきたい
+
+
Paging を書き換える理由
- 他のプロセスから書き換えられた時にエクセプションを飛ばす
- OS の信頼性を保証する上で重要なメモリ管理部分
+
+
__code で書き直していく
+

CbCインターフェース

+
ノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入
+
+
インターフェースによる他のメリット
+
- 煩雑な記述の解消
- 実装の入れ替え

Paging の書き換え

Xv6 では実メモリから仮想メモリの変換をvm.cで行なっている。
次の章で書き換えについて説明する

CbC インターフェースの導入

継続の記述が煩雑になる +
+
実装は別で定義し、呼び出す
+
+
インターフェースによって実装を置き換えることができる
+

CbCインターフェース

+
Data Gear と Data Gear に対して操作を行う Code Gear の集合を表現する Meta Data Gear
+
+
インターフェース実装と定義の図入れる
+

インターフェースの定義

Xv6 の Virtual Memory の API 部分のインターフェース

typedef struct vm<Type,Impl> {
+    __code init_vmm(Impl* vm, __code next(...));
+    __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...));
+    __code kpt_alloc(Impl* vm ,__code next(...));
+    __code switchuvm(Impl* vm ,struct proc* p, __code next(...));
+    __code init_inituvm(Impl* vm, pde_t* pgdir, char* init, uint sz, __code next(...));
+    __code loaduvm(Impl* vm,pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz,  __code next(...));
+    __code allocuvm(Impl* vm, pde_t* pgdir, uint oldsz, uint newsz, __code next(...));
+
+

インターフェースの命名

typedef struct の直後にインターフェース名(vm)を書く
Data Gear にマッピングされる

typedef struct vm<Type,Impl> {
+

インターフェースの Code Gear

Code Gear は __code CodeGear名(引数); で記述する
- Code Gear がどの Data Gear の番号に対応するか指定する必要がある
- ノーマルレベルとメタレベルで Data Gear の見え方が異なるため調整する必要がある
- 引数が Data Gear に相当する
->インターフェースの導入

CbC インターフェース

インターフェースは Data Gear に対しての操作を行う Code Gear
実装は別で定義し、呼び出す
インターフェースによって機能を置き換えることができる

インターフェースの定義

Data Gear と Data Gear に対して操作を行う Code Gear の集合を表現する Meta Data Gear

インターフェースのソースコード

vm.c をインターフェースで書き換えた vm.h のコードの説明をしていく

実装名の定義

typedef struct の直後に実装名(vm)を書く
第1引数の Impl* vm がインターフェースの実装の型になる

typedef struct vm<Type,Impl> {
-

Data Gear の定義

2行目から19行目で引数の Data Gear を定義している

typedef struct vm<Type,Impl> {
-    union Data* vm;
-    uint low;
-    uint hi;
-    struct proc* p;
-....
-

Code Gear の定義

Code Gear は __Code CodeGear名(引数); で記述する
第1引数の Impl* vm が Code Gear の型になる
初期化された Data Gear がそれぞれの Code Gear の引数として扱われる
例)定義された uinit が kpt_freerange の Code Gear の第1引数と対応している

    __code init_vmm(Impl* vm, __code next(...));
+    __code init_vmm(Impl* vm, __code next(...));
     __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...));
     __code kpt_alloc(Impl* vm ,__code next(...));
     __code switchuvm(Impl* vm ,struct proc* p, __code next(...));
@@ -310,43 +210,101 @@
     __code loaduvm(Impl* vm,pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz,  __code next(...));
     __code allocuvm(Impl* vm, pde_t* pgdir, uint oldsz, uint newsz, __code next(...));
 
-....
-

next(…)

__code next(…) は条件分岐によって複数の継続先が設定される
__code next(…) は次の Code Gear の継続先
それぞれの Code Gear の引数の1つに設定する

    __code kpt_freerange(Impl* vm, uint low, uint hi, __code next(...));
-....
+//....
     __code next(...);
 } vm;
-

インターフェースの実装

インターフェースの実装は別ファイルで定義する(vm_impl.cbc)
ヘッダーファイルの呼び出しは #include ではなく #interface で呼び出す

#include "../../context.h"
-#interface "vm.h"
+

__code exit(){
+//....
+}
 
-

create_impl

create_imple の関数内で vm の型を定義し、vm->CodeGear名で対応させていく
実装を Code Gear で記述していく。


-vm* createvm_impl(struct Context* cbc_context) {
+goto vm->kpt_freerange(vm, low, hi, exit);
+

Interface の実装の型

実装側のヘッダーファイルも vm_impl と同じように用意する

typedef struct vm_impl<Impl, Isa> impl vm{
+...
+    __code loaduvm_ptesize_check(Type* vm_impl, uint i, pte_t* pte, uint sz,
+__code next(...));
+

インターフェースの実装

実装は型と実装をそれぞれ別ファイルで定義する(vm_impl.h と vm_impl.cbc)
実装するインターフェースは #interface で宣言する

#interface "vm.h"
+

vm_impl のコンストラクタ

+
create_imple の関数内で vm の型を定義し、vm->CodeGear名で対応させていく
+
+
実装を Code Gear で記述していく。
+
+
struct vm* vm = new vm();
+
- インターフェースのメモリ空間を確保
+
+
vm->void_ret = C_vm_void_ret;
+
- Code Gear の enum の設定
- インターフェースのAPIと enum の番号を紐付けている
+

vm* createvm_impl(struct Context* cbc_context) {
     struct vm* vm  = new vm();
 ....
     vm->void_ret  = C_vm_void_ret;
     vm->init_vmm = C_init_vmmvm_impl;
     vm->kpt_freerange = C_kpt_freerangevm_impl;
     vm->kpt_alloc = C_kpt_allocvm_impl;
-...
-__code init_vmmvm_impl(struct vm_impl* vm,__code next(...)) {
+

APIの実装の例(init_vmm) +
- C_init_vmmvm_impl がメタレベルでinit_vmmvm_impl と対応する
+

__code init_vmmvm_impl(struct vm_impl* vm,__code next(...)) {
     initlock(&kpt_mem.lock, "vm");
     kpt_mem.freelist = NULL;
 
     goto next(...);
 }
-

private

CbC は信頼性を保証するためにそれぞれの Code Gear を細かくする必要があるので、for文やif文がある場合はさらに実装を分ける
Code Gear は基本的にインターフェースで指定された Code Gear 内からのみ継続されるため、Java の private メソッドのように扱われる。

インターフェース実装内の CbC

for文やif文がある場合はさらに実装を分ける +
- 状態遷移ベースで記述したい
+
インターフェースは外から呼び出されるAPI
それに対してインターフェースの実装の Code Gearから明示的に呼び出される Code Gearは、Java の private メソッドのように扱われる。
実際に vm.c の loaduvm の実装を分けた記述を説明する

実装内の明示的な遷移の処理

vm と同じ create_impl 内で vm_impl を定義し、private で実装する Code Gear を定義する
loaduvmvm_impl で goto によって private に遷移する

__code loaduvmvm_impl(struct vm_impl* vm, pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz,  __code next(...)) {
+    Gearef(cbc_context, vm_impl)->pgdir = pgdir;
+    Gearef(cbc_context, vm_impl)->addr = addr;
+    Gearef(cbc_context, vm_impl)->ip = ip;
+    Gearef(cbc_context, vm_impl)->offset = offset;
+    Gearef(cbc_context, vm_impl)->sz = sz;
+    Gearef(cbc_context, vm_impl)->next = next;
+
+    goto loaduvm_ptesize_checkvm_impl(vm, next(...));
+}
+

vm* createvm_impl(struct Context* cbc_context) {
+...
+    struct vm_impl* vm_impl = new vm_impl();
+...
+    vm_impl->loaduvm_ptesize_check = C_loaduvm_ptesize_checkvm_impl;
+....
+    vm->loaduvm = C_loaduvmvm_impl;
+....
+}
+

loaduvmの CbCによる書き換え

loaduvmは何でなぜ書き換えてるのか
vm.cのloaduvmの処理をCbC で書き換える

int loaduvm (pde_t *pgdir, char *addr, struct inode *ip, uint offset, uint sz)
 {
     uint i, pa, n;
@@ -376,20 +334,9 @@
 
     return 0;
 }
-

goto private

vm と同じ create_impl 内で vm_impl を定義し、private で実装する Code Gear を定義する
loaduvmvm_impl で goto によって private に遷移する

vm* createvm_impl(struct Context* cbc_context) {
-...
-    struct vm_impl* vm_impl = new vm_impl();
-...
-    vm_impl->loaduvm_ptesize_check = C_loaduvm_ptesize_checkvm_impl;
-....
-    vm->loaduvm = C_loaduvmvm_impl;
-....
-}
-
-__code loaduvmvm_impl(struct vm_impl* vm, pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz,  __code next(...)) {
+

loaduvm_impl がインターフェースから呼ばれる実装

__code loaduvmvm_impl(struct vm_impl* vm, pde_t* pgdir, char* addr, struct inode* ip, uint offset, uint sz,  __code next(...)) {
     Gearef(cbc_context, vm_impl)->pgdir = pgdir;
     Gearef(cbc_context, vm_impl)->addr = addr;
     Gearef(cbc_context, vm_impl)->ip = ip;
@@ -399,26 +346,22 @@
 
     goto loaduvm_ptesize_checkvm_impl(vm, next(...));
 }
-

private のヘッダー

private 側のヘッダーファイルも vm_impl と同じように用意する

typedef struct vm_impl<Impl, Isa> impl vm{
-...
-    __code loaduvm_ptesize_check(Type* vm_impl, uint i, pte_t* pte, uint sz,
-__code next(int ret, ...));
-

private の記述

#interface "vm_impl.h"
+

loaduvm_impl から private な Code Gear が呼ばれる

#interface "vm_impl.h"
 
-__code loaduvm_ptesize_checkvm_impl(struct vm_impl* vm_impl, __code next(int ret, ...)) {
+__code loaduvm_ptesize_checkvm_impl(struct vm_impl* vm_impl, __code next(...)) {
     char* addr = vm_impl->addr;
 
     if ((uint) addr %PTE_SZ != 0) {
        // goto panic
     }
 
-    goto loaduvm_loopvm_impl(vm_impl, next(ret, ...));
+    goto loaduvm_loopvm_impl(vm_impl, next(...));
 }

vm.cではここから for だが CbC は if文の中と外にgoto を用意して実装する

__code loaduvm_loopvm_impl(struct vm_impl* vm_impl, __code next(int ret, ...)) {
+

__code loaduvm_loopvm_impl(struct vm_impl* vm_impl, __code next(...)) {
     uint i = vm_impl->i;
     uint sz = vm_impl->sz;
 
@@ -426,11 +369,11 @@
         goto loaduvm_check_pgdir(vm_impl, next(ret, ...));
     }
 
-    goto loaduvm_exit(vm_impl, next(ret, ...));
+    goto loaduvm_exit(vm_impl, next(...));
 }
 
 
-__code loaduvm_check_pgdir(struct vm_impl* vm_impl, __code next(int ret, ...)) {
+__code loaduvm_check_pgdir(struct vm_impl* vm_impl, __code next(...)) {
     pte_t* pte = vm_impl->pte;
     pde_t* pgdir = vm_impl->pgdir;
     uint i = vm_impl->i;
@@ -447,17 +390,10 @@
     vm_impl->addr = addr;
     vm_impl->pa = pa;
 
-    goto loaduvm_check_PTE_SZ(vm_impl, next(ret, ...));
+    goto loaduvm_check_PTE_SZ(vm_impl, next(...));
 }
 
 __code loaduvm_check_PTE_SZ(struct vm_impl* vm_impl, __code next(int ret, ...)) {
-    uint sz = vm_impl->sz;
-    uint i = vm_impl->i;
-    uint n = vm_impl->n;
-    struct inode* ip = vm_impl->ip;
-    uint pa = vm_impl->pa;
-    uint offset = vm_impl->offset;
-
     if (sz - i < PTE_SZ) {
         n = sz - i;
     } else {
@@ -478,7 +414,7 @@
     ret = 0;
     goto next(ret, ...);
 }
-


 int loaduvm (pde_t *pgdir, char *addr, struct inode *ip, uint offset, uint sz)
 {
     uint i, pa, n;
@@ -508,42 +444,17 @@
 
     return 0;
 }
-

`インターフェースの呼び出し`


-定義したインターフェースの呼び出しについて説明する
+

stub

goto meta はstub を呼び込んでいる
説明

C を CbC に部分的に書き直す手法

CbC の場合 goto による遷移を行うので、関数呼び出しのように goto 以降のコードを実行できない
例) goto すると戻ってこれないためそれ以降が実行されなくなる。

void userinit(void)
-{ 
-    struct proc* p;
-    extern char _binary_initcode_start[], _binary_initcode_size[];
-
-    p = allocproc();
-    initContext(&p->cbc_context);
-
-    initproc = p;
-
-    if((p->pgdir = kpt_alloc()) == NULL) {
-        panic("userinit: out of memory?");
-    }
-
-    goto cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
-    p->sz = PTE_SZ;
-
-    // craft the trapframe as if
-    memset(p->tf, 0, sizeof(*p->tf));
-~                                          
-

呼び出しの解決

CbC から C への遷移

最初の命令は next で戻ってこれるので、dummy の関数を用意してそこで実行する

void dummy(struct proc *p, char _binary_initcode_start[], char _binary_initcode_size[])
-{ 
+

void cbc_init_vmm_dummy(struct Context* cbc_context, struct proc* p, pde_t* pgdir, char* init, uint sz)
+{
     // inituvm(p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
-    goto cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
-
-}
-
-
-
-__ncode cbc_init_vmm_dummy(struct Context* cbc_context, struct proc* p, pde_t* pgdir, char* init, uint sz){//:skip
 
     struct vm* vm = createvm_impl(cbc_context);
     // goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret);
@@ -555,7 +466,6 @@
     goto meta(cbc_context, vm->init_inituvm);
 }
 
-
 void userinit(void)
 {
     struct proc* p;
@@ -570,10 +480,9 @@
         panic("userinit: out of memory?");
     }
 
-    dummy(p, _binary_initcode_start, _binary_initcode_size);
-~                                                            
+    cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
 
-

CbCインターフェースによる CbCXv6 の書き換え

CbCインターフェースによる CbCXv6 の書き換え

目次

OS の信頼性の重要性

概要

OS の信頼性を上げたい

OS の信頼性の重要性

メタレベルとノーマルレベル

メタレベルとノーマルレベル

Continuation based C

Continuation based C

goto による継続

Data Gear の継続

Meta Code Gear

状態遷移モデル

Agda による検証

Haure Logic

Geas OS

メモリ管理

インターフェース

目次

CbC による Gears OS の開発

Context

目次

Xv6

Meta Data Gear

Xv6

Xv6の構成

カーネル空間

カーネルが提供するもの

カーネルの保護機構

system call

system call

Xv6-rpi

目次

CbCXv6 での Paging

実メモリの直接操作

Paging

Pagingの図

メタレベルでの Paging の操作

Paging の信頼性

Xv6の書き換え方針

CbCインターフェース

Paging の書き換え

目次

CbC インターフェースの導入

CbCインターフェース

インターフェースの定義

インターフェースの命名

インターフェースの Code Gear

CbC インターフェース

インターフェースの定義

インターフェースのソースコード

実装名の定義

Data Gear の定義

Code Gear の定義

next(…)

インターフェースの実装

create_impl

Interface の実装の型

インターフェースの実装

vm_impl のコンストラクタ

private

インターフェース実装内の CbC

実装内の明示的な遷移の処理

loaduvmの CbCによる書き換え

goto private

private のヘッダー

private の記述

インターフェースの呼び出し

stub

C を CbC に部分的に書き直す手法

呼び出しの解決

CbC から C への遷移

まとめ

`インターフェースの呼び出し`