# HG changeset patch # User menikon # Date 1581754219 -32400 # Node ID 5e0c566bba5458a91bb0e25bdf0804d052b97389 # Parent 935e11c0f150d108c4dbc8761051afda2b9b5689 fix diff -r 935e11c0f150 -r 5e0c566bba54 final_main/chapter1.tex --- a/final_main/chapter1.tex Sat Feb 15 03:36:01 2020 +0900 +++ b/final_main/chapter1.tex Sat Feb 15 17:10:19 2020 +0900 @@ -1,13 +1,13 @@ \chapter{OS に対する信頼性の保証} %\label{chap:introduction} \pagenumbering{arabic} - OS には信頼性の保証と拡張性の実現が求められている。信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Continuation based C (CbC) を用いて Gears OS を開発中である。 + OS には信頼性の保証と拡張性の実現が求められている。信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Continuation based C \cite{cbc}(CbC) を用いて Gears OS\cite{gears} を開発中である。 CbC は Code Gear という基本的な処理の単位と Data Gear というデータの単位を用いる。細かい処理に対してノーマルレベルとメタレベルの Code Gear を記述し、stack に値を積む事なく CodeGear 間を遷移することができる。% stack が無い事に よって OS 内部の明確化が実現できる。 Code Gear に対して入力の Data Gear と 出力の Data Gear が存在し、入力に対して期待される出力がされてるか検査することで信頼性を保証する。 CbC の Interface は Gears OS のモジュール化の仕組みである。この Interface は、Java の Interface や Haskell の型クラスに対応し、導入することで仕様と実装に分けて記述することが出来る。Interface を使うことで検証や機能の入れ替えによる拡張が可能となる。 -前段階としてシンプルであるがプロセス、仮想メモリ、カーネルとユーザーの分離、割り込み、ファイルシステムなど Unix の基本的な構造を持っている OS である xv6 を CbC で書き換えている。 +前段階としてシンプルであるがプロセス、仮想メモリ、カーネルとユーザーの分離、割り込み、ファイルシステムなど Unix の基本的な構造を持っている OS である xv6 \cite{xv6} を CbC で書き換えている。 本論文では、xv6 の FileSystem をCbCによって書き換えることにより 複雑な処理である FileSystem を明確化させ信頼性を保証、 Interface を使用可能とすることで拡張性を実現することを目標とする。 diff -r 935e11c0f150 -r 5e0c566bba54 final_main/chapter2.tex --- a/final_main/chapter2.tex Sat Feb 15 03:36:01 2020 +0900 +++ b/final_main/chapter2.tex Sat Feb 15 17:10:19 2020 +0900 @@ -1,7 +1,7 @@ \chapter{Continuation based C} %\label{chap:concept} \section{Continuation based Cの概要} -Continuation based C \cite{cbc} (以下CbC) は基本的な処理単位を CodeGear として定義し、CodeGea 間で遷移するようにプログラムを記述する C 言語と互換性のある当研究室で開発されたプログラミング言語である。図\ref{fig:codegear}はCodeGear間の継続する際の処理の流れを示している。 +Continuation based C (以下CbC) は基本的な処理単位を CodeGear として定義し、CodeGea 間で遷移するようにプログラムを記述する C 言語と互換性のある当研究室で開発されたプログラミング言語である。図\ref{fig:codegear}はCodeGear間の継続する際の処理の流れを示している。 \begin{figure}[ht] \begin{center} diff -r 935e11c0f150 -r 5e0c566bba54 final_main/chapter3.tex --- a/final_main/chapter3.tex Sat Feb 15 03:36:01 2020 +0900 +++ b/final_main/chapter3.tex Sat Feb 15 17:10:19 2020 +0900 @@ -1,7 +1,7 @@ \chapter{GearsOS} %\label{chap:poordirection} \section{GearsOS の概要} -Gears OS \cite{gears} は CbC によって記述されており、CodeGear と DataGear の単位を用いて開発されている OS である。 +Gears OS は CbC によって記述されており、CodeGear と DataGear の単位を用いて開発されている OS である。 Gears OS は 一連の実行が行われる際に使用される CodeGear と DataGear を全て持つ Context と呼ばれるものを持っている。Gears OS は CodeGear 間の継続などの際、常に context を持ち歩いており CodeGear と DataGear の参照が必要になる場合、この Context を通して参照される。 \section{Context} diff -r 935e11c0f150 -r 5e0c566bba54 final_main/chapter4.tex --- a/final_main/chapter4.tex Sat Feb 15 03:36:01 2020 +0900 +++ b/final_main/chapter4.tex Sat Feb 15 17:10:19 2020 +0900 @@ -1,6 +1,6 @@ \chapter{xv6} \section{xv6 の概要} -xv6 \cite{xv6} とは MIT のオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである。xv6 はオリジナルである v6 が非常に古い C 言語で書かれてい る為、ANSI-C に書き換えられ x86 に再実装された。 xv6 は read や write などの systemcall、プロセス、仮想メモリ、カーネルとユーザーの分離、割り込み、ファイルシステムなど Unix の基本的な構造を持っている。 +xv6 とは MIT のオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである。xv6 はオリジナルである v6 が非常に古い C 言語で書かれてい る為、ANSI-C に書き換えられ x86 に再実装された。 xv6 は read や write などの systemcall、プロセス、仮想メモリ、カーネルとユーザーの分離、割り込み、ファイルシステムなど Unix の基本的な構造を持っている。 本研究で使われているのは ARM\cite{arm} 上で動作する Raspberry Pi 用に改良されたxv6を使用する。 @@ -86,5 +86,5 @@ \\/usr/rtm/xv6/fs.cのような階層的なパスを構成する際の操作、管理時に呼び出される。 \end{itemize} %namecmp、dirlookup、dirlookup、dirlink、namei、nameiparent は/usr/rtm/xv6/fs.cのような階層的なパスを管理、操作するための API である。 -ilock で inode をロックした場合必ず処理の終わりには iunlock が呼び出され inode のロックを解除する必要があるように、readi でinode からデータを読み込んだり iwrite で inode へデータを書き込む場合も iput で inode を参照必要がある。このように、FileSystem の API は実行される際様々な API 同士が影響を及ぼしあっているため複雑な挙動をしている。 -これらの API の CbC による書き換えを次章で説明する。 +ilock で inode をロックした場合必ず処理の終わりには iunlock が呼び出され inode のロックを解除する必要があるように、readi でinode からデータを読み込んだり iwrite で inode へデータを書き込む場合も iput で inode を参照必要がある。このように、FileSystem の API を利用する際様々な API 同士が影響を及ぼしあっている。 + diff -r 935e11c0f150 -r 5e0c566bba54 final_main/chapter5.tex --- a/final_main/chapter5.tex Sat Feb 15 03:36:01 2020 +0900 +++ b/final_main/chapter5.tex Sat Feb 15 17:10:19 2020 +0900 @@ -1,7 +1,7 @@ \chapter{CbCによるFileSystemの書き換え} \section{書き換え方針} FileSystem の処理は複雑である。FileSystem が記述されている fs.c で定義されている関数を CbC によって書き換えることにより処理の明確化と信頼性の保証をしたい。 -そのために if 文の中に if文がある場合や for 文がある場合には処理を細かく分離してやり分かりやすくする。また、CbC の Interface を用いることにより仕様と実装を分離し拡張性を実現する。 +そのために今回は、Basic Block 単位に書き換えを行った。また、CbC の Interface を用いることにより仕様と実装を分離し拡張性を実現する。 %xv6 を CbC で書き換え、Gears OS の機能と置き換えることで Gears OS に OS の基本構造を持たせたい。 %このためには xv6 をモジュール化することで、xv6 の機能を明らかにする必要がある。 %xv6 の Interface を定義し、Gears OS の機能をこれに合わせることによって実現したい。 @@ -48,7 +48,7 @@ fs\_impl.cbc の中でCodeGear である iallocfs\_impl が処理されると goto で private な実装である fs\_impl\_private.cbc 側の allocinode という CodeGear へと遷移する。 \lstinputlisting[label=alloc, caption=iallocfs\_impl の private 実装]{src/ialloc.cbc} -private 側では iallocfs\_impl からの受け皿としての allocinode、for 文のループ条件を確認する allocinode\_loopcheck、ループした際の処理をする allocinode\_loop、ループから抜けた際の処理をする allocinode\_noloop の4つの CodeGearから成り立っている。 ループの条件に当てはまらない際は panicへと処理が移り処理が停止する。static なものはまだ書き直していないが後々実装する。これらの CodeGearの一連の挙動を図\ref{fig:iallocloop}に示す。 +今回の実装は最初の遷移先である allocinode、for 文のループ条件を確認する allocinode\_loopcheck、ループした際の処理をする allocinode\_loop、ループから抜けた際の処理をする allocinode\_noloop の4つの CodeGearから成り立っている。 ループの条件に当てはまらない際は panicへと処理が継続し停止する。static なものはまだ書き直していないが後々実装する。これらの CodeGearの一連の挙動を図\ref{fig:iallocloop}に示す。 \begin{figure}[ht] \begin{center} @@ -58,4 +58,4 @@ \label{fig:iallocloop} \end{figure} -本稿では ialloc\_impl という関数を取り上げて説明したが、FileSystem が記述されている fs.c で定義されている関数に関しては全て CbCを用いることにより状態遷移ベースに書き変え挙動を明確化した。 \ No newline at end of file +本稿では ialloc\_impl という関数を取り上げて説明したが、FileSystem が記述されている fs.c で定義されている関数に関しては全て CbC の Interface を用いることにより再実装した。 \ No newline at end of file diff -r 935e11c0f150 -r 5e0c566bba54 final_main/future.tex --- a/final_main/future.tex Sat Feb 15 03:36:01 2020 +0900 +++ b/final_main/future.tex Sat Feb 15 17:10:19 2020 +0900 @@ -1,14 +1,13 @@ \chapter{まとめと今後の課題}  本研究では xv6 の FileSystem 部分について CbC を用いて書き換えを行った。 -実際に FileSystem をCbC で書き換えることによって、複雑であった処理の流れを明確にすることができた。 +実際に FileSystem をCbC で書き換えることによって、if 文と for 文を切り出してやるができた。 さらに、FileSystem を Interface とその実装に書き換えることによって仕様と実装に分けることができた。 仕様と実装に分けることによって拡張性を高めることができた。 -しかし、xv6 はGears OS を開発する前段階として開発しているので今後は書き換えた xv6 を Gears OS に適応した形に改良していく必要がある。 +しかし、xv6 はGears OS を開発する前段階として開発しているので今後は書き換えた xv6 を Gears OS に移植しやすい形に改良していく必要がある。 xv6 の FileSystem 部分書き換え後 、デバックをまだ行っていないため正常に動くかどうか確認することが求められる。 また、正常に動作しなかった場合は修正を行い、OS として機能しているか再確認する必要がある。 今後の課題として、現段階では FileSystem とPaging などの kernelの一部のみ書き換えられているため kernel 全体の書き換えを完了させる必要がある。 -また、書き換えにより実装した xv6 が実機上で動作するか確認する必要がある。 diff -r 935e11c0f150 -r 5e0c566bba54 final_main/main.pdf Binary file final_main/main.pdf has changed