Mercurial > hg > Papers > 2020 > tobaru-master
changeset 45:c20cd7493f5e
fix and add Spine
| author | tobaru |
|---|---|
| date | Fri, 06 Mar 2020 22:30:22 +0900 |
| parents | ee0ea632634b |
| children | 90773155134d |
| files | paper/GearsOS.tex paper/Xv6.tex paper/abstract.tex paper/fig/背表紙.graffle paper/master_paper.pdf paper/master_paper.synctex.gz paper/memory_manage.tex |
| diffstat | 7 files changed, 9 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/GearsOS.tex Thu Mar 05 15:35:10 2020 +0900 +++ b/paper/GearsOS.tex Fri Mar 06 22:30:22 2020 +0900 @@ -28,7 +28,9 @@ \section{Meta Code Gear と Meta Data Gear} - CbC ではノーマルレベルの記述と別にメタレベルで記述することができる。メタレベルの記述によって User Space 側からメモリ管理を行えるようになる。 + CbC ではノーマルレベルの記述と別にメタレベルで記述することができる。 +メタレベルとは、メモリや CPU などの資源管理を行える部分で C言語だと systemcall で呼び出し扱う処理で、Linix だとカーネル空間に相当する。 +メタレベルからノーマルレベルの記述の正しさを証明する。 メタ計算は Meta Code Gear と Meta Data Gear を用いる。
--- a/paper/Xv6.tex Thu Mar 05 15:35:10 2020 +0900 +++ b/paper/Xv6.tex Fri Mar 06 22:30:22 2020 +0900 @@ -1,5 +1,5 @@ \chapter{xv6} - xv6 とは、マサチューセッツ工科大の大学院生向け講義の教材として使うために、UNIX V6 という OS を ANSI-C(規格化されたC言語) に書き換え、x86 に移植した Xv6 OS である。 + xv6\cite{xv6} とは、マサチューセッツ工科大の大学院生向け講義の教材として使うために、UNIX V6 という OS を ANSI-C(規格化されたC言語) に書き換え、x86 に移植した Xv6 OS である。
--- a/paper/abstract.tex Thu Mar 05 15:35:10 2020 +0900 +++ b/paper/abstract.tex Fri Mar 06 22:30:22 2020 +0900 @@ -15,7 +15,7 @@ CbCの接続はメタレベルの記述になる。OSで使われる すべてのコードとデータはcontextと呼ばれるメタデータ に記述される。contextのデータを書き換えることにより -、x.v6で仮想OSやコンテナを定義できるようになると +、xv6で仮想OSやコンテナを定義できるようになると 考えられる。 本論文では
--- a/paper/memory_manage.tex Thu Mar 05 15:35:10 2020 +0900 +++ b/paper/memory_manage.tex Fri Mar 06 22:30:22 2020 +0900 @@ -28,11 +28,14 @@ % 資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する xv6\cite{xv6} という OS を参考にした Geas OS の書き換えの説明を行う。 OS の信頼性の基本であるメモリ管理部分を書き換えることで信頼性を保証したい。 -具体的にはPage のバリデーションチェックによる不正なデータの変更やサンドボックスによるエクセプションを飛ばすなどが挙げられる。 +具体的には Page のバリデーションチェックによる不正なデータの変更やサンドボックスによるエクセプションを飛ばすなどが挙げられる。 また、Gears OS のメタレベルとノーマルレベルでは書き換えなどを防ぐために見えるデータに違いが生じ、Code Gear と Meta Code Gear の記述も煩雑になる。それを解消するために、インターフェースによるモジュール化を導入\cite{mitsuki-master}した。 % インターフェースは Agda に対応するようになっている。これにより Code Gear、Data Gearんの Agda による証明が可能になるように Geas OS の構築を行った。 インターフェースを使うことで検証や機能の入れ替えによる拡張が可能となることを目的する。 + +また、CbC は状態遷移ベースで記述される上に、実行される環境やデータも Stack を使わず遷移されていく。 +そのため、OS の書き換えを行った後に実行環境を複数用意し、それぞれで実行することで OS 内でコンテナや VM を実装できると考えられる。 % 既存の Gears OS でのメモリ管理では単に Page Table Entry をコピーする Fork を実装 % しているが、 さらに資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する Xv6 を参考に GearsOS にメモリ管理を行う API を考察する。