# HG changeset patch # User tobaru # Date 1580290269 -32400 # Node ID 73697739a74de530dba04d5d0588517ff726fce3 # Parent a4a1a68d88117c10c5e9b1b1a45bcb052b2465f0 context xv6 paging diff -r a4a1a68d8811 -r 73697739a74d paper/GearsOS.tex --- a/paper/GearsOS.tex Tue Jan 28 16:00:07 2020 +0900 +++ b/paper/GearsOS.tex Wed Jan 29 18:31:09 2020 +0900 @@ -1,17 +1,17 @@ \chapter{Geas OS} - 信頼性の保証と並列実行のサポートを目的として, Gears OS を開発している. -従来の OS が行うメモリ管理並列実行は Meta レベル(kernel space)で処理される． -ノーマルレベルからメタレベルの記述ができる GearsOS を開発している． + 信頼性の保証と並列実行のサポートを目的として、 Gears OS を開発している。 +従来の OS が行うメモリ管理並列実行は Meta レベル(kernel space)で処理される。 +ノーマルレベルからメタレベルの記述ができる GearsOS を開発している。 \section{Code Gear と Data Gear} - Gears OS は Code Gear と Data Gear という単位でプログラムを記述する CbC を用いて実装する． -Code Gear は CbC における最も基本的な処理の単位である． -Code Gear 間で入力(Input Data Gear)と出力(Output Data Gear)を持ち，goto によって Code Gear から次の Code Gear へ遷移し，継続的に処理を行う. -関数呼び出しとは異なり，呼び出し元には戻らない．j -Code Gear 間の処理の流れを図 \ref{fig:codegear} に示す． + Gears OS は Code Gear と Data Gear という単位でプログラムを記述する CbC を用いて実装する。 +Code Gear は CbC における最も基本的な処理の単位である。 +Code Gear 間で入力(Input Data Gear)と出力(Output Data Gear)を持ち、goto によって Code Gear から次の Code Gear へ遷移し、継続的に処理を行う。 +関数呼び出しとは異なり、呼び出し元には戻らない。j +Code Gear 間の処理の流れを図 \ref{fig:codegear} に示す。 -% 状態遷移ベースのプログラミング言語である． +% 状態遷移ベースのプログラミング言語である。 % (継続的に処理を行う)ことで検証を容易に余す所なく行うことができる. \begin{figure}[ht] \begin{center} @@ -22,15 +22,16 @@ \end{figure} -Data Gear は CbC におけるデータの基本的な単位である．Input Data Gear と Output Data Gear があり，Code Gear の遷移の際に Input Data Gear を受け取り，Output Data Gear を書き出す． +Data Gear は CbC におけるデータの基本的な単位である。Input Data Gear と Output Data Gear があり、Code Gear の遷移の際に Input Data Gear を受け取り、Output Data Gear を書き出す。 \par \section{Meta Code Gear と Meta Data Gear} - CbC ではノーマルレベルの記述と別にメタレベルで記述することができる．メタレベルの記述によって User Space 側からメモリ管理を行えるようになる． + CbC ではノーマルレベルの記述と別にメタレベルで記述することができる。メタレベルの記述によって User Space 側からメモリ管理を行えるようになる。 \par -メタ計算は Meta Code Gear と Meta Data Gear を用いる．この2つはノーマルレベルからメタレベルの変換する時に使われる．メタレベルの変換は Perl スクリプトで実装している．Gears OS での Meta Code Gear は Code Gear の直前, 直後に挿入され，メタ計算を実行する． -Code Gear 間の継続はノーマルレベルでは 図 \ref{fig:codegear} のように見えるが，メタレベルでの Code Gear は図 \ref{fig:meta_cg_dg} の下のように継続を行っている． +メタ計算は Meta Code Gear と Meta Data Gear を用いる。この2つはノーマルレベルからメタレベルの変換する時に使われる。メタレベルの変換は Perl スクリプトで実装している。Gears OS での Meta Code Gear は Code Gear の直前、 直後に挿入され、メタ計算を実行する。 +Code Gear 間の継続はノーマルレベルでは 図 \ref{fig:codegear} のように見えるが、メタレベルでの Code Gear は図 \ref{fig:meta_cg_dg} の下のように継続を行っている。 + \begin{figure}[ht] \begin{center} @@ -42,11 +43,25 @@ \section{Context} - Gears OS の Context は Meta Data Gear であり，接続可能な Code Gear と Data Gear のリスト， Data Gear を確保するメモリ空間などを持っている． -従来のスレッドやプロセスに対応する．Gears OS では Code Gear と Data Gear への接続を Context を通して行う．Context が持つ Data Gear のメモリ空間は事前に確保され，Data Gear のメモリ確保の際に heap の値をずらしてメモリを割り当てる． + Gears OS の Context は Meta Data Gear であり、接続可能な Code Gear と Data Gear のリスト、 Data Gear を確保するメモリ空間などを持っている。 +従来のスレッドやプロセスに対応する。Gears OS では Code Gear と Data Gear への接続を Context を通して行う。Context が持つ Data Gear のメモリ空間は事前に確保され、Data Gear のメモリ確保の際に heap の値をずらしてメモリを割り当てる。 % パルスさん3.1 +\par +ノーマルレベルの Code Gaer から Meta Data Gear である Context を直接参照してしまうと、ユーザーがメタ計算をノーマルレベルで自由に記述できてしまい、メタ計算を分離した意味がなくなってしまう。 +この問題を防ぐため、Context から必要な Data Gear のみをノーマルレベルの Code Gear に渡す処理を行なっている。 +\par + Meta Code Gear は使用される全ての Code Gear ごとに記述する必要がある。しかし、全ての Code Gear に対して記述すると膨大な記述量になる。そのため、Interface を実装した code Gear の Meta Code Gear は Perl スクリプトで自動生成する。 +\par +Meta Code Gear はユーザーが記述することも可能である。そうすることでメタ計算を記述することができるようになったり、goto による継続先を変更することで Geas OS の機能を置き換えることができる。 -\lstinputlisting[label=contexth, caption=Context]{./src/context.h} +\lstinputlisting[label=contexth、 caption=Context]{./src/context.h} ソースコードの説明書く + + +\section{Interface} + Gears OS では Meta Code Gear で Context から値を取り出し、ノーマルレベルの Code Gear に値を渡す。しかし、メタレベルからノーマルレベルの継続の記述が煩雑になるため、Interface 化をしている。 +Interface は Data Gear に対しての操作を行う Code Gear であり、実装は別で定義する。 +Interface で定義した Code Gear に + diff -r a4a1a68d8811 -r 73697739a74d paper/Paging.tex --- a/paper/Paging.tex Tue Jan 28 16:00:07 2020 +0900 +++ b/paper/Paging.tex Wed Jan 29 18:31:09 2020 +0900 @@ -1,12 +1,12 @@ \chapter{Gears OS での Paging} \section{Paging} - メモリ管理の手法に, Paging がある．Paging ではメモリを Page と呼ばれる固定長の単位に分割し，メモリとスワップ領域で Page を入れ替えて管理を行う． + メモリ管理の手法に、Paging がある。Paging ではメモリを Page と呼ばれる固定長の単位に分割し、メモリとスワップ領域で Page を入れ替えて管理を行う。 \section{Gears OS での Paging} - Context に必要な Page Tbale を提供する Interface と User Space からアクセスする API が必要である． -Page Table に相当するデータを Input Data Gear で受け取って変更した後，Context にあるメモリコントロールを担当する Meta Data Gear に goto で遷移してアクセスする． Meta Computation レベルで処理することで Use Spaceでも Page Table を操作することができる． -Meta Computation に戻る際に，Page Table Entry のバリデーションをチェックして反映することで，他のプロセスから Page Table を書き換えられることを防ぐ．また，サンドボックスにしておいて，他のプロセスが書き換えられた時にエクセプションを飛ばすようにすることで信頼性の保証を行う． + Context に必要な Page Tbale を提供する Interface と User Space からアクセスする API が必要である。 +Page Table に相当するデータを Input Data Gear で受け取って変更した後、Context にあるメモリコントロールを担当する Meta Data Gear に goto で遷移してアクセスする。 Meta Computation レベルで処理することで Use Spaceでも Page Table を操作することができる。 +Meta Computation に戻る際に、Page Table Entry のバリデーションをチェックして反映することで、他のプロセスから Page Table を書き換えられることを防ぐ。また、サンドボックスにしておいて、他のプロセスが書き換えられた時にエクセプションを飛ばすようにすることで信頼性の保証を行う。 \section{Paging の書き換え} diff -r a4a1a68d8811 -r 73697739a74d paper/Xv6.tex --- a/paper/Xv6.tex Tue Jan 28 16:00:07 2020 +0900 +++ b/paper/Xv6.tex Wed Jan 29 18:31:09 2020 +0900 @@ -1,2 +1,56 @@ \chapter{Xv6 から Gears OS への書き換え} +\section{Xv6 について} + Xv6 とは、マサチューセッツ工科大の大学院生向け講義の教材として使うために、UNIX V6 という OS を ANSI-C(規格化されたC言語) に書き換え、x86 に移植した Xv6 OS である。 +Xv6 は Arm のバイナリを出力するので、シングルボードコンピュータである Raspberry Pi や携帯電話など様々なハードウェアで動かすことができる。 + +\section{Xv6 を元にした Gears OS の実装} +Gears OS ではハードウェア上でメタレベルの計算や並列実行を行いたいので、Raspberry Pi でもバイナリを出力できる Xv6 を CbC で書き換える。 +ANSI-C で書かれている Xv6 を CbC に書き直し、それを元に Gears OS を実装していく。 + +\section{Xv6 のインターフェース化} +構造図書く(今のcbcxv6と同じか確認してから) +\par + Xv6 の書き換えは Interface を用いてモジュール化する。そうすることで Gears OS の機能を置き換えることできるようになる。 + + +\par + +Xv6 は Kernel を採用している。 Kernel は OS にとって中核となるプログラムである。 +Xv6 では Kernel と User プログラムは分離されており、kernel はプログラムにプロセス管理、メモリ管理、I/O　やファイルの管理などのサービスを提供する。 +User プログラムは kernel に直接アクセスできない。これは重要なファイルを書き換えられたり、アクセスされるのを防ぐためだと考えられる。 +User プログラムが Kernel のサービスを呼び出す場合、system call を用いて User Space から Kernel Space Space へ入り実行される。Kernel は CPU のハードウェア保護機構を使用して、 User Space で実行されているプロセスが自身のメモリのみアクセスできるように保護している。 +User プログラムが system call をすると、ハードウェアが一時的に特権レベルを上げ、kernel のプログラムが実行される。この特権レベルを持つプロセッサの状態を kernel モード、特権のない状態を User モードと言う。 + +\section{system call} + User プログラムが Kernel の処理を行う場合、system call を用いる。 +User プログラムが system call を呼び出すと、トラップが発生する。 +トラップが発生すると、User プログラムは中断され、Kernel に切り替わり処理を行う。Xv6 のsystem call のリストを +\ref{syscall_list} + に示す + +\begin{lstlisting}[frame=lrbt,label=syscall_list,caption={\footnotesize xv6 のシステムコールのリスト}] +static int (*syscalls[])(void) = { + [SYS_fork] =sys_fork, + [SYS_exit] =sys_exit, + [SYS_wait] =sys_wait, + [SYS_pipe] =sys_pipe, + [SYS_read] =sys_read, + [SYS_kill] =sys_kill, + [SYS_exec] =sys_exec, + [SYS_fstat] =sys_fstat, + [SYS_chdir] =sys_chdir, + [SYS_dup] =sys_dup, + [SYS_getpid] =sys_getpid, + [SYS_sbrk] =sys_sbrk, + [SYS_sleep] =sys_sleep, + [SYS_uptime] =sys_uptime, + [SYS_open] =sys_open, + [SYS_write] =sys_write, + [SYS_mknod] =sys_mknod, + [SYS_unlink] =sys_unlink, + [SYS_link] =sys_link, + [SYS_mkdir] =sys_mkdir, + [SYS_close] =sys_close, +}; +\end{lstlisting} diff -r a4a1a68d8811 -r 73697739a74d paper/abstract.tex --- a/paper/abstract.tex Tue Jan 28 16:00:07 2020 +0900 +++ b/paper/abstract.tex Wed Jan 29 18:31:09 2020 +0900 @@ -1,6 +1,6 @@ \chapter*{要旨} - 時代とともに進歩するハードウェアやソフトウェアに対して, OS 自体に信頼性が求められる. メモリ管理は OS の信頼性の基本であるが, 現代の OS では, User Space で Page Table Entry によるメモリ管理を行える OS は少ない, 本研究室で開発したメタレベルの記述ができる CbC という言語を用いて, OS の信頼性の基本であるメモリ管理を行える OS を実装することで, OS の信頼性を保証したい. -既存の Gears OS でのメモリ管理では単に Page Table Entry をコピーする Fork を実装しているが, さらに資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを 出力する Xv6 を参考に GearsOS にメモリ管理を行う API を考察する。 + 時代とともに進歩するハードウェアやソフトウェアに対して、 OS 自体に信頼性が求められる. メモリ管理は OS の信頼性の基本であるが、 現代の OS では、 User Space で Page Table Entry によるメモリ管理を行える OS は少ない、 本研究室で開発したメタレベルの記述ができる CbC という言語を用いて、 OS の信頼性の基本であるメモリ管理を行える OS を実装することで、 OS の信頼性を保証したい. +既存の Gears OS でのメモリ管理では単に Page Table Entry をコピーする Fork を実装しているが、 さらに資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを 出力する Xv6 を参考に GearsOS にメモリ管理を行う API を考察する。 \chapter*{Abstract} % 英語 diff -r a4a1a68d8811 -r 73697739a74d paper/master_paper.aux --- a/paper/master_paper.aux Tue Jan 28 16:00:07 2020 +0900 +++ b/paper/master_paper.aux Wed Jan 29 18:31:09 2020 +0900 @@ -10,17 +10,24 @@ \newlabel{fig:codegear}{{2.1}{3}} \@writefile{toc}{\contentsline {section}{\numberline {2.2}Meta Code Gear と Meta Data Gear}{4}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {2.3}Context}{4}\protected@file@percent } -\newlabel{contexth}{{2.1}{4}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.1}Context}{4}\protected@file@percent } -\@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces ノーマルレベルとメタレベルの継続の見え方}}{6}\protected@file@percent } -\newlabel{fig:meta_cg_dg}{{2.2}{6}} -\@writefile{toc}{\contentsline {chapter}{\numberline {第3章}Xv6 から Gears OS への書き換え}{7}\protected@file@percent } +\newlabel{contexth、 caption}{{2.3}{4}} +\@writefile{lol}{\contentsline {lstlisting}{./src/context.h}{4}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {2.4}Interface}{6}\protected@file@percent } +\@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces ノーマルレベルとメタレベルの継続の見え方}}{7}\protected@file@percent } +\newlabel{fig:meta_cg_dg}{{2.2}{7}} +\@writefile{toc}{\contentsline {chapter}{\numberline {第3章}Xv6 から Gears OS への書き換え}{8}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\@writefile{toc}{\contentsline {chapter}{\numberline {第4章}Gears OS での Paging}{8}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {3.1}Xv6 について}{8}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {3.2}Xv6 を元にした Gears OS の実装}{8}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {3.3}Xv6 のインターフェース化}{8}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {3.4}system call}{9}\protected@file@percent } +\newlabel{syscall_list}{{3.1}{9}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {3.1}\footnotesize xv6 のシステムコールのリスト}{9}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{\numberline {第4章}Gears OS での Paging}{10}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\@writefile{toc}{\contentsline {section}{\numberline {4.1}Paging}{8}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {4.2}Gears OS での Paging}{8}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {4.3}Paging の書き換え}{8}\protected@file@percent } -\@writefile{toc}{\contentsline {chapter}{付録}{8}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {4.1}Paging}{10}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {4.2}Gears OS での Paging}{10}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {4.3}Paging の書き換え}{10}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{付録}{10}\protected@file@percent } diff -r a4a1a68d8811 -r 73697739a74d paper/master_paper.lof --- a/paper/master_paper.lof Tue Jan 28 16:00:07 2020 +0900 +++ b/paper/master_paper.lof Wed Jan 29 18:31:09 2020 +0900 @@ -1,6 +1,6 @@ \addvspace {10\p@ } \addvspace {10\p@ } \contentsline {figure}{\numberline {2.1}{\ignorespaces Code Gear 間の継続}}{3}% -\contentsline {figure}{\numberline {2.2}{\ignorespaces ノーマルレベルとメタレベルの継続の見え方}}{6}% +\contentsline {figure}{\numberline {2.2}{\ignorespaces ノーマルレベルとメタレベルの継続の見え方}}{7}% \addvspace {10\p@ } \addvspace {10\p@ } diff -r a4a1a68d8811 -r 73697739a74d paper/master_paper.log --- a/paper/master_paper.log Tue Jan 28 16:00:07 2020 +0900 +++ b/paper/master_paper.log Wed Jan 29 18:31: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) 28 JAN 2020 15:57 +This is e-pTeX, Version 3.14159265-p3.8.2-190131-2.6 (utf8.euc) (TeX Live 2019) (preloaded format=platex 2020.1.16) 29 JAN 2020 18:21 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -338,7 +338,12 @@ [3 -] (./master_paper.lol) +] (./master_paper.lol +LaTeX Font Info: Font shape `JT1/hmc/m/n' will be +(Font) scaled to size 9.6222pt on input line 2. +LaTeX Font Info: Font shape `JY1/hmc/m/n' will be +(Font) scaled to size 9.6222pt on input line 2. +) \tf@lol=\write7 \openout7 = `master_paper.lol'. @@ -367,26 +372,26 @@ <./fig/meta_cg_dg.pdf> -LaTeX Warning: Float too large for page by 43.27322pt on input line 41. +LaTeX Warning: Float too large for page by 43.27322pt on input line 42. (./src/context.h LaTeX Font Info: Font shape `JT1/hmc/m/n' will be (Font) scaled to size 7.69775pt on input line 1. LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 10.53629pt on input line 24. +(Font) scaled to size 10.53629pt on input line 12. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 10.53629pt on input line 24. +(Font) scaled to size 10.53629pt on input line 12. LaTeX Font Info: Font shape `JT1/hmc/bx/n' will be -(Font) scaled to size 10.53629pt on input line 24. +(Font) scaled to size 10.53629pt on input line 12. LaTeX Font Info: Font shape `JY1/hmc/bx/n' will be -(Font) scaled to size 10.53629pt on input line 24. - [4])) (./Xv6.tex [5] [6] -第 3 章(7ページ) -) (./Paging.tex [7 +(Font) scaled to size 10.53629pt on input line 12. + [4]) [5]) (./Xv6.tex [6] [7] +第 3 章(8ページ) +[8 -] -第 4 章(8ページ) -) [8 +]) (./Paging.tex [9] +第 4 章(10ページ) +) [10 ] (./master_paper.aux) @@ -395,12 +400,12 @@ ) Here is how much of TeX's memory you used: - 6300 strings out of 493985 - 89276 string characters out of 6166648 - 281110 words of memory out of 5000000 - 10622 multiletter control sequences out of 15000+600000 - 16375 words of font info for 82 fonts, out of 8000000 for 9000 + 6304 strings out of 493985 + 89327 string characters out of 6166648 + 323120 words of memory out of 5000000 + 10626 multiletter control sequences out of 15000+600000 + 16577 words of font info for 84 fonts, out of 8000000 for 9000 107 hyphenation exceptions out of 8191 - 38i,11n,36p,481b,1841s stack positions out of 5000i,500n,10000p,200000b,80000s + 39i,11n,36p,411b,1817s stack positions out of 5000i,500n,10000p,200000b,80000s -Output written on master_paper.dvi (15 pages, 22852 bytes). +Output written on master_paper.dvi (17 pages, 34624 bytes). diff -r a4a1a68d8811 -r 73697739a74d paper/master_paper.lol --- a/paper/master_paper.lol Tue Jan 28 16:00:07 2020 +0900 +++ b/paper/master_paper.lol Wed Jan 29 18:31:09 2020 +0900 @@ -1,1 +1,2 @@ -\contentsline {lstlisting}{\numberline {2.1}Context}{4}% +\contentsline {lstlisting}{./src/context.h}{4}% +\contentsline {lstlisting}{\numberline {3.1}\footnotesize xv6 のシステムコールのリスト}{9}% diff -r a4a1a68d8811 -r 73697739a74d paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r a4a1a68d8811 -r 73697739a74d paper/master_paper.synctex.gz Binary file paper/master_paper.synctex.gz has changed diff -r a4a1a68d8811 -r 73697739a74d paper/master_paper.toc --- a/paper/master_paper.toc Tue Jan 28 16:00:07 2020 +0900 +++ b/paper/master_paper.toc Wed Jan 29 18:31:09 2020 +0900 @@ -3,9 +3,14 @@ \contentsline {section}{\numberline {2.1}Code Gear と Data Gear}{3}% \contentsline {section}{\numberline {2.2}Meta Code Gear と Meta Data Gear}{4}% \contentsline {section}{\numberline {2.3}Context}{4}% -\contentsline {chapter}{\numberline {第3章}Xv6 から Gears OS への書き換え}{7}% -\contentsline {chapter}{\numberline {第4章}Gears OS での Paging}{8}% -\contentsline {section}{\numberline {4.1}Paging}{8}% -\contentsline {section}{\numberline {4.2}Gears OS での Paging}{8}% -\contentsline {section}{\numberline {4.3}Paging の書き換え}{8}% -\contentsline {chapter}{付録}{8}% +\contentsline {section}{\numberline {2.4}Interface}{6}% +\contentsline {chapter}{\numberline {第3章}Xv6 から Gears OS への書き換え}{8}% +\contentsline {section}{\numberline {3.1}Xv6 について}{8}% +\contentsline {section}{\numberline {3.2}Xv6 を元にした Gears OS の実装}{8}% +\contentsline {section}{\numberline {3.3}Xv6 のインターフェース化}{8}% +\contentsline {section}{\numberline {3.4}system call}{9}% +\contentsline {chapter}{\numberline {第4章}Gears OS での Paging}{10}% +\contentsline {section}{\numberline {4.1}Paging}{10}% +\contentsline {section}{\numberline {4.2}Gears OS での Paging}{10}% +\contentsline {section}{\numberline {4.3}Paging の書き換え}{10}% +\contentsline {chapter}{付録}{10}% diff -r a4a1a68d8811 -r 73697739a74d paper/memory_manage.tex --- a/paper/memory_manage.tex Tue Jan 28 16:00:07 2020 +0900 +++ b/paper/memory_manage.tex Wed Jan 29 18:31:09 2020 +0900 @@ -1,6 +1,11 @@ \chapter{メモリ管理による信頼性の保証} -メモリ管理は OS の信頼性の基本であるが, 現代の OS では, User Space で Page Table Entry によるメモリ管理を行える OS は少ない. これは User レベルの操作で Page Table が書き換えられたり，別の Page にアクセスするのを防ぐためだと考えられる．しかし，User Space でメモリ管理を行えるようにすることで, Page のバリデーションをチェックしたり，サンドボックスによる信頼性の保証を行えるようになる．また，適切な記述をすれば最適なメモリ管理にも繋がる． +メモリ管理は OS の信頼性の基本であるが、 現代の OS では、 User Space で Page Table Entry によるメモリ管理を行える OS は少ない。 +これは User レベルの操作で Page Table が書き換えられたり、別の Page にアクセスするのを防ぐためだと考えられる。 +しかし、User Space でメモリ管理を行えるようにすることで、 Page のバリデーションをチェックしたり、サンドボックスによる信頼性の保証を行えるようになる。また、適切な記述をすれば最適なメモリ管理にも繋がる。 \par - 本研究室で開発したメタレベルの記述ができる CbC という言語を用いて, OS の信頼性の基本であるメモリ管理を行える OS を実装することで, OS の信頼性を保証したい. + 本研究室で開発したメタレベルの記述ができる CbC という言語を用いて、 OS の信頼性の基本であるメモリ管理を行える OS を実装することで、 OS の信頼性を保証したい。 既存の Gears OS でのメモリ管理では単に Page Table Entry をコピーする Fork を実装 -しているが, さらに資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを 出力する Xv6 を参考に GearsOS にメモリ管理を行う API を考察する. +しているが、 さらに資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する Xv6 を参考に GearsOS にメモリ管理を行う API を考察する。 +\par +CbC は継続を中心とした言語であるため、状態遷移モデルに落とし込むことができる。 +CbC で書き換えることによって OS の機能の信頼性を保証することができる。 diff -r a4a1a68d8811 -r 73697739a74d thsis_paging.mm --- a/thsis_paging.mm Tue Jan 28 16:00:07 2020 +0900 +++ b/thsis_paging.mm Wed Jan 29 18:31:09 2020 +0900 @@ -1,6 +1,9 @@ - + + + + @@ -10,11 +13,20 @@ - + + + + - + + + + + + + @@ -22,9 +34,12 @@ - + - + + + + diff -r a4a1a68d8811 -r 73697739a74d thsis_paging.pdf Binary file thsis_paging.pdf has changed