Mercurial > hg > Papers > 2020 > tobaru-master
changeset 14:3952ffd84dfe
context, etc
| author | tobaru |
|---|---|
| date | Thu, 06 Feb 2020 17:45:09 +0900 |
| parents | 1ef114182e80 |
| children | b7ae3aa6548e |
| files | paper/GearsOS.tex paper/Xv6.tex paper/abstract.tex paper/master_paper.aux paper/master_paper.log paper/master_paper.lol paper/master_paper.pdf paper/master_paper.synctex.gz paper/master_paper.toc paper/memory_manage.tex paper/src/context.h thsis_paging.mm |
| diffstat | 12 files changed, 127 insertions(+), 63 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/GearsOS.tex Wed Feb 05 17:08:43 2020 +0900 +++ b/paper/GearsOS.tex Thu Feb 06 17:45:09 2020 +0900 @@ -59,8 +59,17 @@ Meta Code Gear はユーザーが記述することも可能である。そうすることでメタ計算を記述することができるようになったり、goto による継続先を変更することで Geas OS の機能を置き換えることができる。 -\lstinputlisting[label=contexth、 caption={\footnotesize Context}]{./src/context.h} + 第5章で扱うメモリ管理部分である vm の Context を ソースコード \ref{contexth} に示す。 + +\lstinputlisting[label=contexth, caption={\footnotesize 生成された Context}]{./src/context.h} -ソースコードの説明書く +% code は全ての Code Gear を列挙した enum と関数ポインタの組みで表現される。(ソースコード \ref{contexth} 55行目~68行目) +Code Gear の名前は enum で定義され、コンパイル後には整数で変換される。 +Code Gear に接続する際は enum で定義された番号を指定する。 +これによってメタ計算時に接続する Code Gear を切り替えることができる。 +Data Gear のメモリ空間は事前に領域を確保した後、必要に応じて領域を割り当てることで実現する。 +実際に Allocation する際は ソースコード \ref{contexth} 9行目で定義した heap を Data Gear のサイズ分増やすことで実現する。 + +
--- a/paper/Xv6.tex Wed Feb 05 17:08:43 2020 +0900 +++ b/paper/Xv6.tex Thu Feb 06 17:45:09 2020 +0900 @@ -1,6 +1,9 @@ \chapter{Xv6} Xv6 とは、マサチューセッツ工科大の大学院生向け講義の教材として使うために、UNIX V6 という OS を ANSI-C(規格化されたC言語) に書き換え、x86 に移植した Xv6 OS である。 -Xv6 は Arm のバイナリを出力するので、シングルボードコンピュータである Raspberry Pi や携帯電話など様々なハードウェアで動かすことができる。 + + + +本研究では、この Xv6 を参考に Gears OS の開発を行なっている。 \section{Kernel Space と User Space} Xv6 は Kernel を採用している。 Kernel は OS にとって中核となるプログラムである。 @@ -44,4 +47,5 @@ \end{lstlisting} \section{Xv6-rpi} - +Xv6 は Arm のバイナリを出力するので、シングルボードコンピュータである Raspberry Pi や携帯電話など様々なハードウェアで動かすことができる。 +実際に Raspberry Pi 上で動かすために xv6-rpi という OS を用意して動作しているか検証中である。
--- a/paper/abstract.tex Wed Feb 05 17:08:43 2020 +0900 +++ b/paper/abstract.tex Thu Feb 06 17:45:09 2020 +0900 @@ -1,9 +1,18 @@ \chapter*{要旨} - OS を要する機器に依存している現代では、OS のバグは日常に支障を来たすことに繋がる。 -OS 自体に信頼性が求められるが、複雑な機能が増えている OS では、全てのコードに対して検証を行うのは困難である。 -本研究室で開発したメタレベルの記述ができる CbC という言語を用いて OS を実装することで、 OS の信頼性を保証したい。 -OS の実装は、CbC で軽量なハードウェアでも動かせるように Arm のバイナリを 出力する OS である Xv6 を参考に行う。 -本研究では、OSの信頼性の基本であるメモリ管理部分を CbC で記述する。 +OS を要する機器に依存している現代では、OS のバグは日常に支障を来たすことに繋がる。 +OS 自体に信頼性が求められるが、機能が多く短期間のアップデートが必要な OS では、全てのコードに対して何度も検証を行うのは困難である。 + + +本研究室で開発したメタレベルの記述ができる CbC という言語を用いて OS の信頼性を保証するために Gears OS を開発中である。 +本研究での Gears OS の実装は、CbC で軽量なハードウェアでも動かせるように Arm のバイナリを 出力する OS である Xv6 を参考に行っている。 +CbC は継続を中心とした言語であるため、状態遷移モデルに落とし込むことができる。 +状態遷移の1つ1つの関数に対して検証を行うことで OS の機能の信頼性を保証することができる。 + + +しかし、ノーマルレベルとメタレベルで見え方が異なるデータに対して継続の記述が煩雑になる。 +そこで本研究では、インターフェースを用いたモジュール化を行う。 +インターフェースによって形式化され柔軟に再利用することもできる。 +OSの信頼性の基本であるメモリ管理部分のインターフェースと実装の記述と考察を行う。 @@ -11,3 +20,5 @@ \chapter*{Abstract} % 英語 + +
--- a/paper/master_paper.aux Wed Feb 05 17:08:43 2020 +0900 +++ b/paper/master_paper.aux Thu Feb 06 17:45:09 2020 +0900 @@ -1,5 +1,5 @@ \relax -\@writefile{toc}{\contentsline {chapter}{\numberline {第1章}メモリ管理による信頼性の保証}{2}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{\numberline {第1章}OS の信頼性の保障}{2}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} \@writefile{toc}{\contentsline {chapter}{\numberline {第2章}CbC による Geas OS の開発}{3}\protected@file@percent } @@ -12,8 +12,8 @@ \@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces ノーマルレベルとメタレベルの継続の見え方}}{4}\protected@file@percent } \newlabel{fig:meta_cg_dg}{{2.2}{4}} \@writefile{toc}{\contentsline {section}{\numberline {2.3}Context}{4}\protected@file@percent } -\newlabel{contexth、 caption}{{2.3}{5}} -\@writefile{lol}{\contentsline {lstlisting}{./src/context.h}{5}\protected@file@percent } +\newlabel{contexth}{{2.1}{5}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.1}\footnotesize 生成された Context}{5}\protected@file@percent } \@writefile{toc}{\contentsline {chapter}{\numberline {第3章}Xv6}{7}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }}
--- a/paper/master_paper.log Wed Feb 05 17:08:43 2020 +0900 +++ b/paper/master_paper.log Thu Feb 06 17:45:09 2020 +0900 @@ -1,4 +1,4 @@ -This is e-pTeX, Version 3.14159265-p3.8.2-190131-2.6 (utf8.euc) (TeX Live 2019) (preloaded format=platex 2020.1.16) 5 FEB 2020 17:05 +This is e-pTeX, Version 3.14159265-p3.8.2-190131-2.6 (utf8.euc) (TeX Live 2019) (preloaded format=platex 2020.1.16) 6 FEB 2020 17:42 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -348,9 +348,9 @@ ] (./master_paper.lol LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 9.6222pt on input line 2. +(Font) scaled to size 9.6222pt on input line 1. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 9.6222pt on input line 2. +(Font) scaled to size 9.6222pt on input line 1. ) \tf@lol=\write7 \openout7 = `master_paper.lol'. @@ -482,11 +482,11 @@ ) Here is how much of TeX's memory you used: 6421 strings out of 493985 - 91090 string characters out of 6166648 + 91080 string characters out of 6166648 375234 words of memory out of 5000000 10693 multiletter control sequences out of 15000+600000 17126 words of font info for 87 fonts, out of 8000000 for 9000 107 hyphenation exceptions out of 8191 33i,11n,36p,410b,1835s stack positions out of 5000i,500n,10000p,200000b,80000s -Output written on master_paper.dvi (55 pages, 235152 bytes). +Output written on master_paper.dvi (55 pages, 240400 bytes).
--- a/paper/master_paper.lol Wed Feb 05 17:08:43 2020 +0900 +++ b/paper/master_paper.lol Thu Feb 06 17:45:09 2020 +0900 @@ -1,4 +1,4 @@ -\contentsline {lstlisting}{./src/context.h}{5}% +\contentsline {lstlisting}{\numberline {2.1}\footnotesize 生成された Context}{5}% \contentsline {lstlisting}{\numberline {3.1}\footnotesize xv6 のシステムコールのリスト}{7}% \contentsline {lstlisting}{\numberline {5.1}\footnotesize vm のインターフェースの定義(vm.h)}{12}% \contentsline {lstlisting}{\numberline {5.2}\footnotesize vm インターフェースの実装}{14}%
--- a/paper/master_paper.toc Wed Feb 05 17:08:43 2020 +0900 +++ b/paper/master_paper.toc Thu Feb 06 17:45:09 2020 +0900 @@ -1,4 +1,4 @@ -\contentsline {chapter}{\numberline {第1章}メモリ管理による信頼性の保証}{2}% +\contentsline {chapter}{\numberline {第1章}OS の信頼性の保障}{2}% \contentsline {chapter}{\numberline {第2章}CbC による Geas OS の開発}{3}% \contentsline {section}{\numberline {2.1}Code Gear と Data Gear}{3}% \contentsline {section}{\numberline {2.2}Meta Code Gear と Meta Data Gear}{4}%
--- a/paper/memory_manage.tex Wed Feb 05 17:08:43 2020 +0900 +++ b/paper/memory_manage.tex Thu Feb 06 17:45:09 2020 +0900 @@ -1,13 +1,44 @@ -\chapter{メモリ管理による信頼性の保証} -メモリ管理は OS の信頼性の基本であるが、 現代の OS では、 User Space で Page Table Entry によるメモリ管理を行える OS は少ない。 -これは User レベルの操作で Page Table が書き換えられたり、別の Page にアクセスするのを防ぐためだと考えられる。 -しかし、User Space でメモリ管理を行えるようにすることで、 Page のバリデーションをチェックしたり、サンドボックスによる信頼性の保証を行えるようになる。また、適切な記述をすれば最適なメモリ管理にも繋がる。 +\chapter{OS の信頼性の保障} +OS を要する機器に依存している現代では、OS のバグは日常に支障を来たすことに繋がる。 +実際にパスワードなしで root にアクセスできるバグや、コンピュータの日付の設定を変更するとコンピュータ自体が壊れるバグが発生した。 + + + OS 自体に信頼性が求められるが、複雑な機能が多く、短期間のアップデートが必要な OS では、全てのコードに対して検証を行うのは困難である。 +CPU やメモリなどの資源管理は基本的には OS が行なっている。資源管理が複雑な上、アクセスされたり書き換えられることを防ぐためだと考えられる。 +これによってユーザーは資源を気にすることなくコンピュータを扱うことができる。 + + + このように OS には資源管理やシステムコールされた後の処理などユーザーが記述するプログラム以外の部分が存在する。 +その処理をメタレベルの計算、ユーザーが記述する部分をノーマルレベルの計算と呼ぶ。 + + + + 本研究室ではノーマルレベルとメタレベルの記述を行える CbC というプログラミング言語を開発してきた。 +CbC はノーマルレベルとメタレベルの記述の間を関数型プログラミング言語のように goto によって継続する。そのため、状態遷移モデルに落とし込むことができる。関数の1つ1つをモデル検査することで信頼性を保証したい。 + + +モデル検査には定理証明支援系である Agda を用いる。 +Agda は Haure Logic という検証手法を扱うことができる。 +Haure Logic は事前条件を使ってある関数を実行して事後条件を満たすことを確認する検証手法であり、継続に事前条件と事後条件を持たせることのできる CbC と相性がいい。 + + + CbC を使って 信頼性の保証と拡張性を持たせる Gears OS の開発を行なっている。 +本論文では、 +% 資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する +Xv6 という OS を参考にした Geas OS の書き換えの説明を行う。 +OS の信頼性の基本であるメモリ管理部分を書き換えることで Page のバリデーションチェックによる不正なデータの変更やサンドボックスによるエクセプションをが可能となる。 +また、Gears OS のメタレベルとノーマルレベルの記述が煩雑になるため、インターフェースによるモジュール化を導入した。 +% インターフェースは Agda に対応するようになっている。これにより Code Gear、Data Gearんの Agda による証明が可能になるように Geas OS の構築を行った。 +インターフェースを使うことで機能の入れ替えによる拡張性や Agda による証明が可能となることを目的する。 + +% 既存の Gears OS でのメモリ管理では単に Page Table Entry をコピーする Fork を実装 +% しているが、 さらに資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する Xv6 を参考に GearsOS にメモリ管理を行う API を考察する。 + + + +% しかし、ユーザー空間で資源管理を行えるようにすることで、 +% Page のバリデーションをチェックしたり、サンドボックスによる信頼性の保証を行えるようになる。また、適切な記述をすれば最適な資源管理にも繋がる。 + - 本研究室で開発したメタレベルの記述ができる CbC という言語を用いて、 OS の信頼性の基本であるメモリ管理を行える OS を実装することで、 OS の信頼性を保証したい。 -既存の Gears OS でのメモリ管理では単に Page Table Entry をコピーする Fork を実装 -しているが、 さらに資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する Xv6 を参考に GearsOS にメモリ管理を行う API を考察する。 - - CbC は継続を中心とした言語であるため、状態遷移モデルに落とし込むことができる。 -CbC で書き換えることによって OS の機能の信頼性を保証することができる。
--- a/paper/src/context.h Wed Feb 05 17:08:43 2020 +0900 +++ b/paper/src/context.h Thu Feb 06 17:45:09 2020 +0900 @@ -1,6 +1,7 @@ -/* Context definition */ struct Context { enum Code next; + struct Worker* worker; + struct TaskManager* taskManager; int codeNum; __code (**code) (struct Context*); union Data **data; @@ -16,8 +17,6 @@ int odg; int maxOdg; int gpu; // GPU task - struct Worker* worker; - struct TaskManager* taskManager; struct Context* task; struct Element* taskList; #ifdef USE_CUDAWorker @@ -28,35 +27,48 @@ /* multi dimension parameter */ int iterate; struct Iterator* iterator; + enum Code before; }; union Data { - struct Meta { - enum DataType type; - long size; - long len; - struct Queue* wait; // tasks waiting this dataGear - } Meta; + .... + ///mnt/dalmore-home/one/src/cbcxv6/src/gearsTools/../interface/vm.h + struct vm { + union Data* vm; + uint low; + uint hi; + struct proc* p; + pde_t* pgdir; + char* init; + uint sz; + char* addr; + struct inode* ip; + uint offset; + uint oldsz; + uint newsz; + char* uva; + uint va; + void* pp; + uint len; + uint phy_low; + uint phy_hi; + enum Code init_vmm; + enum Code kpt_freerange; + enum Code kpt_alloc; + enum Code switchuvm; + enum Code init_inituvm; + enum Code loaduvm; + enum Code allocuvm; + enum Code clearpteu; + enum Code copyuvm; + enum Code uva2ka; + enum Code copyout; + enum Code paging_int; + enum Code void_ret; + enum Code next; + } vm; + .... +#ifndef CbC_XV6_CONTEXT struct Context Context; - // Stack Interface - struct Stack { - union Data* stack; - union Data* data; - union Data* data1; - enum Code whenEmpty; - enum Code clear; - enum Code push; - enum Code pop; - enum Code pop2; - enum Code isEmpty; - enum Code get; - enum Code get2; - enum Code next; - } Stack; - // Stack implementations - struct SingleLinkedStack { - struct Element* top; - } SingleLinkedStack; - .... }; // union Data end this is necessary for context generator
--- a/thsis_paging.mm Wed Feb 05 17:08:43 2020 +0900 +++ b/thsis_paging.mm Thu Feb 06 17:45:09 2020 +0900 @@ -15,11 +15,8 @@ <node CREATED="1580462026946" ID="ID_1472155882" MODIFIED="1580462030002" TEXT="英語も"/> </node> <node CREATED="1578979732696" ID="ID_457372106" MODIFIED="1580108656805" POSITION="right" TEXT="OS のメモリ管理"> -<node CREATED="1580460373935" ID="ID_1062193517" MODIFIED="1580461472303" TEXT="タイトル的にメモリ管理よりインターフェースの説明するべき？"> -<icon BUILTIN="help"/> -<icon BUILTIN="full-1"/> -</node> -<node CREATED="1580462138553" ID="ID_1846491838" MODIFIED="1580462198989" TEXT="OSの信頼性(メモリ管理以外)"> +<node CREATED="1580460373935" ID="ID_1062193517" MODIFIED="1580971072228" TEXT="タイトル的にメモリ管理よりインターフェースの説明するべき？"/> +<node CREATED="1580462138553" ID="ID_1846491838" MODIFIED="1580971088254" TEXT="OSの信頼性(メモリ管理以外)"> <icon BUILTIN="help"/> <node CREATED="1580462157478" ID="ID_1631189480" MODIFIED="1580462174061" TEXT="file system"/> <node CREATED="1580462182158" ID="ID_1466724178" MODIFIED="1580462185475" TEXT="プロセス"/>