Mercurial > hg > Papers > 2020 > menikon-thesis
changeset 21:a03d74165189
tweak
line wrap: on
line diff
--- a/final_main/appendix.tex Fri Feb 14 14:50:28 2020 +0900 +++ b/final_main/appendix.tex Sat Feb 15 00:01:24 2020 +0900 @@ -1,6 +1,19 @@ -\chapter*{付録} +\chapter{ソースコード} +本文中に紹介したソースコードの内、量が膨大なため一部しか掲載できなかったソース +コードを示す。 + +\section{FileSystem の Interface} +FileSystem の Interface を定義したソースコードの全記述をソースコード\ref{1fs.ds}に示す。 +\lstinputlisting[label=1fs.ds, caption=FileSystem の Interface]{src/fs.dg} -\lstinputlisting[label=fs.ds, caption=FileSystem の Interface]{src/fs.dg} -\lstinputlisting[label=fs_impl.h, caption=fs private のヘッダーファイル]{src/fs_impl.h} -\lstinputlisting[label=fs_impl.cbc, caption=fs Interface の実装]{src/fs_impl.cbc} -\lstinputlisting[label=fs_impl_private.cbc, caption=fs Interface の private 実装]{src/fs_impl_private.cbc} \ No newline at end of file +\section{fFileSystem Interface private 実装のヘッダーファイル} +FileSystem Interface の private 実装 に利用する全ての定義がされているヘッダーファイルの全ソースコードをソースコード\ref{1fs_impl.h}に示す。 +\lstinputlisting[label=1fs_impl.h, caption=fs private のヘッダーファイル]{src/fs_impl.h} + +\section{FileSystem Interface の 実装} +FileSystem Interface を 実装したソースコードの全記述をソースコード\ref{1fs_impl.cbc}に示す。 +\lstinputlisting[label=1fs_impl.cbc, caption=fs Interface の実装]{src/fs_impl.cbc} + +\section{FileSystem Interface の private 実装} +FileSystem Interface の private 実装を記述した全ソースコードをソースコード\ref{1fs_impl_private.cbc}に示す。 +\lstinputlisting[label=1fs_impl_private.cbc, caption=fs Interface の private 実装]{src/fs_impl_private.cbc} \ No newline at end of file
--- a/final_main/chapter1.tex Fri Feb 14 14:50:28 2020 +0900 +++ b/final_main/chapter1.tex Sat Feb 15 00:01:24 2020 +0900 @@ -1,13 +1,13 @@ -\chapter{xv6 の OS の信頼性保証} +\chapter{OS に対する信頼性の保証} %\label{chap:introduction} \pagenumbering{arabic} + OS には信頼性の保証と拡張性の実現が求められている。信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Continuation based C (CbC) を用いて Gears OS を開発中である。 -%序論の目安としては1枚半ぐらい． -%英語発表者は，最終予稿の「はじめに」の英訳などを載せてもいいかも． +CbC は Code Gear という基本的な処理の単位と Data Gear というデータの単位を用いる。細かい処理に対してノーマルレベルとメタレベルの Code Gear を記述し、stack に値を積む事なく CodeGear 間を遷移することができる。% stack が無い事に よって OS 内部の明確化が実現できる。 +Code Gear に対して入力の Data Gear と 出力の Data Gear が存在し、入力に対して期待される出力がされてるか検査することで信頼性を保証する。 -OS には信頼性の保証と拡張性の実現が求められている。信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Continuation based C (CbC) を用いて Gears OS を開発中である。前段階としてシンプルであるがプロセス、仮想メモリ、カーネルとユーザーの分離、割り込み、ファイルシステムなど Unix の基本的な構造を持っている OS である xv6 を CbC で書き換えている。 -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 を使うことで検証や機能の入れ替えによる拡張が可能となる。 +CbC の Interface は Gears OS のモジュール化の仕組みである。この Interface は、Java の Interface や Haskell の型クラスに対応し、導入することで仕様と実装に分けて記述することが出来る。Interface を使うことで検証や機能の入れ替えによる拡張が可能となる。 + +前段階としてシンプルであるがプロセス、仮想メモリ、カーネルとユーザーの分離、割り込み、ファイルシステムなど Unix の基本的な構造を持っている OS である xv6 を CbC で書き換えている。 + 本論文では、xv6 の FileSystem をCbCによって書き換えることにより 複雑な処理である FileSystem を明確化させ信頼性を保証、 Interface を使用可能とすることで拡張性を実現することを目標とする。
--- a/final_main/chapter4.tex Fri Feb 14 14:50:28 2020 +0900 +++ b/final_main/chapter4.tex Sat Feb 15 00:01:24 2020 +0900 @@ -39,7 +39,7 @@ \label{fig:filesystem} \end{figure} -boot sector はシステムを起動するためのものであるが、FileSystem がこのブロックを使用することはない。super block はブロックのファイルサイズやデータブロックの数,、inode の数,、log 中のブロック数などが格納されている。 inodes は inode に関するリストが格納されている。block bitmap は使用しているブロックが記憶されている。data blocks は block bitmap において使用可能であることが記録されており、ファイルやディレクトリが保持されている。Logging 階層の log が格納されている。 +boot sector はシステムを起動するためのものであるが、FileSystem がこのブロックを使用することはない。super block はブロックのファイルサイズやデータブロックの数,、inode の数,、log 中のブロック数などが格納されている。 inodes は inode に関するリストが格納されている。block bitmap は使用しているブロックが記憶されている。data blocks は block bitmap において使用可能であることが記録されており、ファイルやディレクトリが保持されている。log は Logging 階層に関する情報が格納されている。 \section{FilleSystem の API} FileSystem について記述している fs.c ではファイルを操作、管理する際に様々な関数がプロセスやデバイスなどから呼び出され使用されている。
--- a/final_main/future.tex Fri Feb 14 14:50:28 2020 +0900 +++ b/final_main/future.tex Sat Feb 15 00:01:24 2020 +0900 @@ -1,4 +1,15 @@ \chapter{まとめと今後の課題} -今回の研究では xv6 の FileSystem 部分について CbC を用いて書き換えを行った。しかし、 xv6 はGears OS を開発する前段階として開発しているので今後は書き換えた xv6 を Gears OS に適応した形に改良していく必要がある。 -xv6 の FileSystem 部分書き換え後 make し build することはできたが、デバックをまだ行っていないため正常に動くかどうか確認することが求められる。また、動かなかった場合修正を行い OS として機能しているか再確認する必要がある。 -後々は定理証明支援機 agda で証明できる OS として開発したい。 \ No newline at end of file + 本研究では xv6 の FileSystem 部分について CbC を用いて書き換えを行った。 +実際に FileSystem をCbC で書き換えることによって、複雑であった処理の流れを明確にすることができた。 +さらに、FileSystem を Interface とその実装に書き換えることによって仕様と実装に分けることができた。 +仕様と実装に分けることによって拡張性を高めることができた。 +しかし、xv6 はGears OS を開発する前段階として開発しているので今後は書き換えた xv6 を Gears OS に適応した形に改良していく必要がある。 +xv6 の FileSystem 部分書き換え後 、デバックをまだ行っていないため正常に動くかどうか確認することが求められる。 +また、正常に動作しなかった場合は修正を行い、OS として機能しているか再確認する必要がある。 + + +今後の課題として、現段階では FileSystem とPaging などの kernelの一部のみ書き換えられているため kernel 全体の書き換えを完了させる必要がある。 +また、書き換えにより実装した xv6 が実機上で動作するか確認する必要がある。 + + +%後々は定理証明支援機 agda で証明できる OS として開発したい。 \ No newline at end of file
--- a/final_main/main.out Fri Feb 14 14:50:28 2020 +0900 +++ b/final_main/main.out Sat Feb 15 00:01:24 2020 +0900 @@ -1,4 +1,4 @@ -\BOOKMARK [0][-]{chapter.1}{第1章 xv6 の OS の信頼性保証}{}% 1 +\BOOKMARK [0][-]{chapter.1}{第1章 OS に対する信頼性の保証}{}% 1 \BOOKMARK [0][-]{chapter.2}{第2章 Continuation based C}{}% 2 \BOOKMARK [1][-]{section.2.1}{2.1 Continuation based Cの概要}{chapter.2}% 3 \BOOKMARK [1][-]{section.2.2}{2.2 CodeGear}{chapter.2}% 4 @@ -18,3 +18,11 @@ \BOOKMARK [1][-]{section.5.3}{5.3 FileSystem の Interface の実装}{chapter.5}% 18 \BOOKMARK [1][-]{section.5.4}{5.4 FileSystem の Interface の private な実装}{chapter.5}% 19 \BOOKMARK [0][-]{chapter.6}{第6章 まとめと今後の課題}{}% 20 +\BOOKMARK [0][-]{chapter*.14}{参考文献}{}% 21 +\BOOKMARK [0][-]{chapter*.15}{謝辞}{}% 22 +\BOOKMARK [0][-]{chapter*.16}{発表履歴}{}% 23 +\BOOKMARK [0][-]{appendix.A}{付 録A \040ソースコード}{}% 24 +\BOOKMARK [1][-]{section.A.1}{A.1 FileSystem の Interface}{appendix.A}% 25 +\BOOKMARK [1][-]{section.A.2}{A.2 fFileSystem Interface private 実装のヘッダーファイル}{appendix.A}% 26 +\BOOKMARK [1][-]{section.A.3}{A.3 FileSystem Interface の 実装}{appendix.A}% 27 +\BOOKMARK [1][-]{section.A.4}{A.4 FileSystem Interface の private 実装}{appendix.A}% 28
--- a/final_main/main.tex Fri Feb 14 14:50:28 2020 +0900 +++ b/final_main/main.tex Sat Feb 15 00:01:24 2020 +0900 @@ -101,11 +101,15 @@ \nocite{*} \bibliographystyle{junsrt} \bibliography{reference} - +\addcontentsline{toc}{chapter}{参考文献} % 謝辞 \input{thanks.tex} - +\addcontentsline{toc}{chapter}{謝辞} +%発表履歴 +\input{sigos.tex} +\addcontentsline{toc}{chapter}{発表履歴} % 付録 +\appendix \input{appendix.tex} \end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/sigos.tex Sat Feb 15 00:01:24 2020 +0900 @@ -0,0 +1,4 @@ +\chapter*{発表履歴} +\begin{itemize} + \item 坂本昂弘, 桃原優, 河野真治. 継続を用いた x. v6 kernel の書き換え. 研究報告システムソフトウェアとオペレーティング・システム (OS), April,2019 +\end{itemize} \ No newline at end of file
--- a/final_main/src/fs_impl_private.cbc Fri Feb 14 14:50:28 2020 +0900 +++ b/final_main/src/fs_impl_private.cbc Sat Feb 15 00:01:24 2020 +0900 @@ -70,7 +70,7 @@ return ip; } - if (empty == 0 && ip->ref == 0) { // Remember empty slot. + if (empty == 0 && ip->ref == 0) { empty = ip; } } @@ -279,7 +279,7 @@ for (bi = 0; bi < BPB && b + bi < sb.size; bi++) { m = 1 << (bi % 8); - if ((bp->data[bi / 8] & m) == 0) { // Is block free? + if ((bp->data[bi / 8] & m) == 0) { bp->data[bi / 8] |= m; // Mark block in use. log_write(bp); brelse(bp);
--- a/final_main/thanks.tex Fri Feb 14 14:50:28 2020 +0900 +++ b/final_main/thanks.tex Sat Feb 15 00:01:24 2020 +0900 @@ -1,5 +1,5 @@ \chapter*{謝辞} -\thispagestyle{empty} +%\thispagestyle{empty} %基本的な内容は以下の通り．参考にしてみて下さい． %厳密な決まりは無いので，個々人の文体でも構わない． @@ -8,11 +8,9 @@ \hspace{1zw}本研究の遂行，また本論文の作成にあたり、御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治准教授に深く感謝したします。 -%また、本研究の遂行及び本論文の作成にあたり、日頃より終始懇切なる御教授と御指導を賜わりましたhoge教授に心より深く感謝致します。 +数々の貴重な御助言と細かな御配慮を戴いた並列信頼研究室の外間政尊さん、桃原優さん、清水隆博さん、東恩納琢偉さんに深く感謝致します。 -数々の貴重な御助言と細かな御配慮を戴いた並列信頼研究室のhoge氏に深く感謝致します。 - -また一年間共に研究を行い、暖かな気遣いと励ましをもって支えてくれた並列信頼研究室のhoge君、hoge君、hogeさんに感謝致します。 +また一年間共に研究を行い、暖かな気遣いと励ましをもって支えてくれた並列信頼研究室の一木貴裕君、安田亮君、福田光希君に感謝致します。 最後に、有意義な時間を共に過ごした情報工学科の学友、並びに物心両面で支えてくれた両親に深く感謝致します。
--- a/final_sub/utf8.tex Fri Feb 14 14:50:28 2020 +0900 +++ b/final_sub/utf8.tex Sat Feb 15 00:01:24 2020 +0900 @@ -59,40 +59,42 @@ \maketitle \thispagestyle{fancy} -\section{section1} +\section{xv6 の OS の信頼性保証} \section{xv6} -xv6\cite{xv6}とはMITのオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである. -xv6 はオリジナルである v6 が非常に古いC言語で書かれている為, ANSI-Cに書き換えられ x86 に再実装された. xv6 はreadやwriteなどのsystemcall,プロセス,仮想メモリ,カーネルとユーザーの分離,割り込み,ファイルシステムなどUnixの基本的な構造を持っている. +xv6\cite{xv6}とはMITのオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである。 +xv6 はオリジナルである v6 が非常に古いC言語で書かれている為、ANSI-C に書き換えられ x86 に再実装された。 xv6 は read や write などの systemcall、プロセス、仮想メモリ、カーネルとユーザーの分離、割り込み、ファイルシステムなど Unix の基本的な構造を持っている。 -section{Continuation based C} -xv6 kernel上でinterfaceを実装する際,当研究室で開発されたプログラミング言語 Continuation based C (CbC)を用いる. -CbC は基本的な処理単位を CodeGearとして定義し，CodeGea間で遷移するようにプログラムを記述するC言語と互換性のあるプログラミング言語である. -CodeGearは返り値を持たない為,関数内で処理が終了すると呼び出し元の関数に戻ることがなく別のCodeGearへ遷移する. -以下のCode1にCodeGear遷移時のコード例を示す. +\section{Continuation based C} +xv6 kernel 上で interface を実装する際、当研究室で開発されたプログラミング言語 Continuation based C \cite{cbc}(以下 CbC)を用いる。 +CbC は基本的な処理単位を CodeGearとして定義し、CodeGea間で遷移するようにプログラムを記述する C 言語と互換性のあるプログラミング言語である。 +CodeGearは返り値を持たない為、関数内で処理が終了すると呼び出し元の関数に戻ることがなく別の CodeGear へ遷移する。 +以下の Code1 に CodeGear 遷移時のコード例を示す。 \lstinputlisting[label=cbcexample, caption=CodeGearの継続の例]{src/cbc_example.cbc} -またCbCにおけるCodeGear間の継続にはスタックが使用できず,呼び出し元の環境などを持たない為軽量継続と呼ぶ. -現在CbCはCコンパイラであるGCC及びLLVMをバックエンドとしたclang上で実装されている． +また CbC における CodeGear 間の継続にはスタックが使用されず、呼び出し元の環境などを持たない為軽量継続と呼ぶ。 +現在 CbC は C コンパイラである GCC 及び LLVM をバックエンドとした clang 上で実装されている。 \section{context} -contextとは一連の実行が行われる際に使用されるCodeGearとDataGearの集合である. -従来のスレッドやプロセスに対応する.Context は接続可能な CodeGear, Data Gear のリスト. Data Gear を確保するメモリ空間,実行される Task への Code Gear 等を持っている. -CodeGearが別のCodeGearに遷移する際,必ずcontextを参照しenumで定義されたCodeGearの番号を指定し遷移する.ノーマルレベルで見た際のCodeGar,DataGerおよびcontextの関係を以下の図1に簡潔に示す. +context とは一連の実行が行われる際に使用される CodeGear と DataGear の集合である。 +従来のスレッドやプロセスに対応する。Context は接続可能な CodeGear、Data Gear のリスト、Data Gear を確保するメモリ空間、実行される Task への Code Gear 等を持っている。 +CodeGear が別の CodeGear に遷移する際、必ず context を参照し enum で定義された CodeGear の番号を指定し遷移する。ノーマルレベルで見た際の CodeGear、DataGear および context の関係を以下の図1に簡潔に示す。 \begin{figure}[ht] \begin{center} \includegraphics[width=65mm]{pic/context.pdf} \end{center} - \caption{CodeGear,DataGear,contxtの関係図} + \caption{CodeGear、DataGear、contxtの関係図} \label{fig:perl6buil} \end{figure} \section{CbCのInterface} -先述した通り, CbCのInterface は Gears OS のモジュール化の仕組みである. Interface は呼び出しの引数になる Data Gear の集合であり，そこで呼び出される Code Gear のエントリである.呼び出される Code Gear の引数となる Data Gear はここで 全て定義される. Interface を定義することで複数の実装を持つことができる.このInterfaceは,JavaのInterfaceやHaskellの型クラスに対応し,導入することで仕様と実装に分けて記述することが出来る. +先述した通り、CbC の Interface は Gears OS のモジュール化の仕組みである。 Interface は呼び出しの引数になる Data Gear の集合であり、そこで呼び出される Code Gear のエントリである。呼び出される Code Gear の引数となる Data Gear はここで 全て定義される。 Interface を定義することで複数の実装を持つことができる。このInterfaceは、Java の Interface や Haskell の型クラスに対応し、導入することで仕様と実装に分けて記述することが出来る。 \section{xv6 の FileSystem} +FileSystem とは、コンピュータの資源を操作するための OS が持つ機能のことである。 ファイルといえば記憶装置内に格納されている情報を指すが、xv6 の FileSystem は、デバ イスやプロセス、カーネル内の処理をする際の情報などをファイルとして扱う。OS ごとに 利用している FileSystem は異なるが、一部の OS を除きほとんどの OS には FileSystem が存在する。 + \section{CbC による xv6 FileSystem の書き換え}