# HG changeset patch # User menikon # Date 1581504893 -32400 # Node ID b67e4c9f037447af6469a06d7e2c089669a9491c # Parent c8adccdd011a9a693a922519f9b022c2d5cc695f tweak diff -r c8adccdd011a -r b67e4c9f0374 final_main/chapter1.tex --- a/final_main/chapter1.tex Wed Feb 12 11:28:11 2020 +0900 +++ b/final_main/chapter1.tex Wed Feb 12 19:54:53 2020 +0900 @@ -4,3 +4,6 @@ %序論の目安としては1枚半ぐらい． %英語発表者は，最終予稿の「はじめに」の英訳などを載せてもいいかも． + + + diff -r c8adccdd011a -r b67e4c9f0374 final_main/chapter2.tex --- a/final_main/chapter2.tex Wed Feb 12 11:28:11 2020 +0900 +++ b/final_main/chapter2.tex Wed Feb 12 19:54:53 2020 +0900 @@ -11,6 +11,9 @@ \label{fig:codegear} \end{figure} +また、プログラムを記述する際、ノーマルレベルの記述と別にメモリ管理、スレッド管理など記述しなければならない処理が存在する。これらをメタ計算と呼ぶ。 +CbC の CodeGear 、DataGear にはそれぞれ Meta CodeGear 、Meta DataGear と呼ばれるメタレベルの単位が存在する。これらを用いることによってメタ計算を実現し、 OS の信頼性を保証できる。 + 現在 CbC は C コンパイラであるGCC\cite{gcc} \cite{nobu-prosym}及びLLVM\cite{llvm} \cite{kaito-lola}をバックエンドとした clang 上で実装されている。 本研究では、このプログラミング言語を用いて xv6 の Filesystemを書き換える。 \section{CodeGear} @@ -33,7 +36,7 @@ この CbC における CodeGear 間の継続にスタックが使用されない性質は信頼性の高い OS の開発に適している。 \newpage \section{DataGear} -DataGear は CbCにおけるデータの基本的な単位である。CodeGear は Input DataGear、Output DataGear を引数に持ち、図\ref{fig:DataGear}で示したように遷移する際に任意のInput DataGearを参照し、Output DataGearを書き出す。 +DataGear は CbCにおけるデータの基本的な単位である。CodeGear は Input DataGear、Output DataGear を引数に持ち、図\ref{fig:DataGear}で示すように遷移する際に任意のInput DataGearを参照し、Output DataGearを書き出す。 \begin{figure}[ht] \begin{center} @@ -43,5 +46,19 @@ \label{fig:DataGear} \end{figure} +\section{Meta CodeGear と Meta DataGear} +Meta Code Gear は図\ref{fig:meta}で示すようにノーマルレベルの Code Gear の直後に遷移され、メタ計算を実行する。 + +\begin{figure}[ht] + \begin{center} + \includegraphics[width=150mm]{fig/meta_cg_dg.pdf} + \end{center} + \caption{メタレベルの処理を可視化した CodeGearとDataGear} + \label{fig:meta} +\end{figure} + +Meta Data Gear は CbC の 接続可能な Code Gear、 Data Gear のリストでありData Gear を確保するメモリ空間でもある。 +ノーマルレベルからの書き換えやアクセスを防ぐために存在している。GearsOS の Context がこれにあたる。 +%\section{Meta DataGear} diff -r c8adccdd011a -r b67e4c9f0374 final_main/chapter3.tex --- a/final_main/chapter3.tex Wed Feb 12 11:28:11 2020 +0900 +++ b/final_main/chapter3.tex Wed Feb 12 19:54:53 2020 +0900 @@ -5,9 +5,9 @@ Gears OS は 一連の実行が行われる際に使用される CodeGear と DataGear を全て持つ Context と呼ばれるものを持っている。Gears OS は CodeGear 間の継続などの際、常に context を持ち歩いており CodeGear と DataGear の参照が必要になる場合、この Context を通して参照される。 \section{Context} -context とは一連の実行が行われる際に使用される CodeGear と DataGear の集合である。 従来のスレッドやプロセスに対応する。Context は接続可能な CodeGear、 Data Gear のリスト、 Data Gear を確保するメモリ空間、 実行される Task への Code Gear 等を持っている。 CodeGear が 別の CodeGear に遷移する際、 必ず context を参照し enum -で定義された CodeGear の番号を指定し遷移する。 ノーマルレベルで見た際の CodeGear、DataGear および context の関係を以下の図\ref{fig:cbc} に簡潔に示す。 - +Context とは一連の実行が行われる際に使用される CodeGear と DataGear の集合である。 従来のスレッドやプロセスに対応する。Context は接続可能な CodeGear、 Data Gear のリスト、 Data Gear を確保するメモリ空間、 実行される Task への Code Gear 等を持っている。 CodeGear が 別の CodeGear に遷移する際、 必ず context を参照し enum +で定義された CodeGear の番号を指定し遷移する。ノーマルレベルで見た際の CodeGear、DataGear および context の関係を以下の図\ref{fig:cbc} に簡潔に示す。 +%Context は Meta Data Gear であるため、Meta Code Gear を介してアクセスする。 %\vspace{10mm} \begin{figure}[ht] \begin{center} diff -r c8adccdd011a -r b67e4c9f0374 final_main/chapter4.tex --- a/final_main/chapter4.tex Wed Feb 12 11:28:11 2020 +0900 +++ b/final_main/chapter4.tex Wed Feb 12 19:54:53 2020 +0900 @@ -4,13 +4,11 @@ 本研究で使われているのは ARM\cite{arm} 上で動作する Raspberry Pi 用に改良されたxv6を使用する。 -\section{FileSystem} +\section{xv6 のFileSystem} %どんなものか書く -FileSystem とは、コンピュータの資源を操作するための OS が持つ機能のことである。ファイルといえば記憶装置内に格納されている情報を指すが、デバイスやプロセス、カーネル内の処理をする際の情報などをファイルとして扱う FileSystem も存在する。 OS ごとに利用している FileSystem は異なるが、一部の OS を除きほとんどの OS には FileSystem が存在する。 +FileSystem とは、コンピュータの資源を操作するための OS が持つ機能のことである。ファイルといえば記憶装置内に格納されている情報を指すが、xv6 の FileSystem は、デバイスやプロセス、カーネル内の処理をする際の情報などをファイルとして扱う。 OS ごとに利用している FileSystem は異なるが、一部の OS を除きほとんどの OS には FileSystem が存在する。 %記憶装置内に格納されているデータ,デバイスやプロセス,カーネル内の処理をする際の情報などファイルとして管理している. %processについて(軽く) -\section{xv6 のFileSystem} -.xv6 の FileSystem は、デバイスやプロセス、カーネル内の処理をする際の情報などをファイルとして扱う FileSystem を使用している。 xv6 の FileSystem は図\ref{fig:xv6filesystem} のように7つの階層によって構成されている。 \newpage @@ -18,7 +16,7 @@ \begin{center} \includegraphics[width=50mm]{fig/FileSystemLayout.pdf} \end{center} - \caption{xv6 の FileSystem 構造} + \caption{xv6 の FileSystem Layer} \label{fig:xv6filesystem} \end{figure} @@ -31,66 +29,55 @@ \begin{itemize} \item readsb \\ブロックのファイルサイズやデータブロックの数、inodeの数、log 中のブロック数などが格納されている super block を読み込む。 - \\log.c で呼び出されて使用している。 \item iinit - \\main.c で呼び出されて使用している。 \item ialloc \\デバイスで指定されたタイプを新しい inode に割り当てる。 - \\mkfs.c で呼び出されて使用している。 \item iupdate \\変更されたメモリ内の inode をディスクにコピーする。 - \\fs.c で呼び出されて使用している。 \item idup - \\fs.c で呼び出されて使用している。 - + \\IPの参照カウントをインクリメントする。 + \item ilock \\指定した inode をロックする。またその際に必要であるならば、ディスクから inode を読み込む。 - \\fs.c と exec.c で呼び出されて使用している。 \item iunlock \\指定された inode のロックを解除する。 - \\fs.c と exec.c で呼び出されて使用している。 \item iput \\メモリ内の inode への参照を削除する。 %それが最後の参照であった場合、iノードキャッシュエントリはリサイクルできます。それが最後の参照であり、iノードにリンクがない場合、ディスク上のiノード（およびそのコンテンツ）を解放します。 - \\fs.c で呼び出されて使用している。 \item iunlockput \\指定された inode のロックを解除してから iput を実行する。 %後でまとめる - \\fs.c と exec.c で呼び出されて使用している。 \item stati \\inode から ファイルに関する統計情報を複製する。 - \\fs.c で呼び出されて使用している。 \item readi \\inode からデータを読み込む。 - \\fs.c と exec.c とvm.c で呼び出されて使用している。 - + \item writei \\inode へデータを書き込む。 - \\fs.c で呼び出されて使用している。 + + \item namecmp - \item namecmp - \\fs.c で呼び出されて使用している。 \item dirlookup - \\fs.c で呼び出されて使用している。 + \\ディレクトリ内のディレクトリエントリを探す。 +%見つかった場合は、* poffをエントリのバイトオフセットに設定します。 \item dirlink - \\fs.c で呼び出されて使用している。 + \\新しいディレクトリエントリ（名前、inum）をディレクトリdpに書き込む。 \item namei - \\fs.c と exec.c で呼び出されて使用している。 - %src/usr/usertests.cでも呼び出されてる？要質問 + \item nameiparent - \\fs.c で呼び出されて使用している。 + \end{itemize} diff -r c8adccdd011a -r b67e4c9f0374 final_main/chapter5.tex --- a/final_main/chapter5.tex Wed Feb 12 11:28:11 2020 +0900 +++ b/final_main/chapter5.tex Wed Feb 12 19:54:53 2020 +0900 @@ -1,11 +1,15 @@ \chapter{CbCによるFileSystemの書き換え} \section{書き換え方針} +FileSystem の処理は複雑である。 %xv6 を CbC で書き換え、Gears OS の機能と置き換えることで Gears OS に OS の基本構造を持たせたい。 %このためには xv6 をモジュール化することで、xv6 の機能を明らかにする必要がある。 %xv6 の Interface を定義し、Gears OS の機能をこれに合わせることによって実現したい。 %\newpage -\section{FileSystem の Interface の定義(fs.dg)} +\section{FileSystem の Interface の定義} +インターフェースはある Data Gear の定義と、それに対する操作を行う Code Gear の 集合を表現する Meta Data Gear である。Context では全ての Code Gaer と Data Gear の集合を表現していることに対し、インターフェースは一部の Code Gear と一部の Data Gear の集合を表現する。 +インターフェースを記述することによってノーマルレベルとメタレベルの分離が可能となる。 + \begin{figure}[ht] \begin{center} \includegraphics[width=100mm]{fig/fsInterface.pdf} @@ -17,8 +21,22 @@ %\newpage FileSystem の Interface を記述したコードをソースコード\ref{fs_interface}に示す。 -\lstinputlisting[label=fs_interface, caption=FileSystem の Interface]{src/fs.dg} +\lstinputlisting[label=fs_interface, caption=FileSystem の Interface (fs.dg)]{src/fs1.dg} + +1行目で Interface名を定義している。typedef struct の後に Interface名 (今回は fs) を書く。 +CodeGear は \_\_code CodeGear名 (引数) の形で記述する。第一引数である Impl* fs が CodeGear の型、第二引数以降は Interface の実装時に利用する CodeGear が必要とする引数が入る。 +CodeGaer は 2 行目から 18 行目のように ”\_\_code [CodeGear 名]([引数])”で記述する。この引数が input Data Gear になる。 + +\section{FileSystem の Interface の実装} + +\lstinputlisting[label=fs_interface_impl, caption=FileSystem の Interface の実装(fs\_impl.cbc 一部抜粋)]{src/fs_impl1.cbc} -\section{FileSystem の Interface の実装(fs\_impl.cbc)} +2 行目のようにインターフェースのヘッダーファイルは \#include ではなく \#interface で呼び出す。 +4行目の create fs\_impl は Java などのコンストラクタに相当する。7行目から66行目で Interface と実装の紐付けしている。 +CbC は1つ1つの CodeGear の信頼性を保障させるために細かくするべきであるため、 for 文や if 文がある場合はさらに実装を分ける。fs と同じように fs\_impl を定義し、遷移する関数名に対応させていく。分けた実装はさらに別で実装する (fs\_impl\_private.cbc)。 -\lstinputlisting[label=fs_interface_impl, caption=FileSystem の Interface の実装]{src/fs_impl1.cbc} \ No newline at end of file +\section{FileSystem の Interface の private な実装} +インターフェースで定義した CodeGear 以外の CodeGaer も記述することができる。この Code Gear は基本的にインターフェースで指定された Code Gear 内からのみ継続されるため、Java の private メソッドのように扱われる。 +インターフェースと同じようにヘッダーファイルをソースコード\ref{fs_impl}で定義する。 + +\lstinputlisting[label=fs_impl, caption=fs private のヘッダーファイル(fs\_impl.h)]{src/fs_impl1.h} diff -r c8adccdd011a -r b67e4c9f0374 final_main/fig/fsInterface.graffle Binary file final_main/fig/fsInterface.graffle has changed diff -r c8adccdd011a -r b67e4c9f0374 final_main/fig/fsInterface.pdf Binary file final_main/fig/fsInterface.pdf has changed diff -r c8adccdd011a -r b67e4c9f0374 final_main/fig/meta_cg_dg.graffle Binary file final_main/fig/meta_cg_dg.graffle has changed diff -r c8adccdd011a -r b67e4c9f0374 final_main/fig/meta_cg_dg.pdf Binary file final_main/fig/meta_cg_dg.pdf has changed diff -r c8adccdd011a -r b67e4c9f0374 final_main/future.tex --- a/final_main/future.tex Wed Feb 12 11:28:11 2020 +0900 +++ b/final_main/future.tex Wed Feb 12 19:54:53 2020 +0900 @@ -1,4 +1,4 @@ \chapter{まとめと今後の課題} 今回の研究では xv6 の FileSystem 部分について CbC を用いて書き換えを行った。しかし、 xv6 はGears OS を開発する前段階として開発しているので今後は書き換えた xv6 を Gears OS に適応した形に改良していく必要がある。 xv6 の FileSystem 部分書き換え後 make し build することはできたが、デバックをまだ行っていないため正常に動くかどうか確認することが求められる。また、動かなかった場合修正を行い OS として機能しているか再確認する必要がある。 -%後々は証明支援器 agda で証明できる OS として開発したい \ No newline at end of file +後々は定理証明支援機 agda で証明できる OS として開発したい。 \ No newline at end of file diff -r c8adccdd011a -r b67e4c9f0374 final_main/main.out --- a/final_main/main.out Wed Feb 12 11:28:11 2020 +0900 +++ b/final_main/main.out Wed Feb 12 19:54:53 2020 +0900 @@ -3,17 +3,18 @@ \BOOKMARK [1][-]{section.2.1}{2.1 Continuation based Cの概要}{chapter.2}% 3 \BOOKMARK [1][-]{section.2.2}{2.2 CodeGear}{chapter.2}% 4 \BOOKMARK [1][-]{section.2.3}{2.3 DataGear}{chapter.2}% 5 -\BOOKMARK [0][-]{chapter.3}{第3章 GearsOS}{}% 6 -\BOOKMARK [1][-]{section.3.1}{3.1 GearsOS の概要}{chapter.3}% 7 -\BOOKMARK [1][-]{section.3.2}{3.2 Context}{chapter.3}% 8 -\BOOKMARK [1][-]{section.3.3}{3.3 Inetrface}{chapter.3}% 9 -\BOOKMARK [0][-]{chapter.4}{第4章 xv6}{}% 10 -\BOOKMARK [1][-]{section.4.1}{4.1 xv6 の概要}{chapter.4}% 11 -\BOOKMARK [1][-]{section.4.2}{4.2 FileSystem}{chapter.4}% 12 -\BOOKMARK [1][-]{section.4.3}{4.3 xv6 のFileSystem}{chapter.4}% 13 -\BOOKMARK [1][-]{section.4.4}{4.4 FilleSystem の API}{chapter.4}% 14 +\BOOKMARK [1][-]{section.2.4}{2.4 Meta CodeGear と Meta DataGear}{chapter.2}% 6 +\BOOKMARK [0][-]{chapter.3}{第3章 GearsOS}{}% 7 +\BOOKMARK [1][-]{section.3.1}{3.1 GearsOS の概要}{chapter.3}% 8 +\BOOKMARK [1][-]{section.3.2}{3.2 Context}{chapter.3}% 9 +\BOOKMARK [1][-]{section.3.3}{3.3 Inetrface}{chapter.3}% 10 +\BOOKMARK [0][-]{chapter.4}{第4章 xv6}{}% 11 +\BOOKMARK [1][-]{section.4.1}{4.1 xv6 の概要}{chapter.4}% 12 +\BOOKMARK [1][-]{section.4.2}{4.2 xv6 のFileSystem}{chapter.4}% 13 +\BOOKMARK [1][-]{section.4.3}{4.3 FilleSystem の API}{chapter.4}% 14 \BOOKMARK [0][-]{chapter.5}{第5章 CbCによるFileSystemの書き換え}{}% 15 \BOOKMARK [1][-]{section.5.1}{5.1 書き換え方針}{chapter.5}% 16 -\BOOKMARK [1][-]{section.5.2}{5.2 FileSystem の Interface の定義\(fs.dg\)}{chapter.5}% 17 -\BOOKMARK [1][-]{section.5.3}{5.3 FileSystem の Interface の実装\(fs\137impl.cbc\)}{chapter.5}% 18 -\BOOKMARK [0][-]{chapter.6}{第6章 まとめと今後の課題}{}% 19 +\BOOKMARK [1][-]{section.5.2}{5.2 FileSystem の Interface の定義}{chapter.5}% 17 +\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 diff -r c8adccdd011a -r b67e4c9f0374 final_main/main.pdf Binary file final_main/main.pdf has changed diff -r c8adccdd011a -r b67e4c9f0374 final_main/src/fs1.dg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/fs1.dg Wed Feb 12 19:54:53 2020 +0900 @@ -0,0 +1,20 @@ +typedef struct fs { + __code readsb(Impl* fs, uint dev, struct superblock* sb, __code next(...)); + __code iinit(Impl* fs, __code next(...)); + __code ialloc(Impl* fs, uint dev, short type, __code next(...)); + __code iupdate(Impl* fs, struct inode* ip, __code next(...)); + __code idup(Impl* fs, struct inode* ip, __code next(...)); + __code ilock(Impl* fs, struct inode* ip, __code next(...)); + __code iunlock(Impl* fs, struct inode* ip, __code next(...)); + __code iput(Impl* fs, struct inode* ip, __code next(...)); + __code iunlockput(Impl* fs, struct inode* ip, __code next(...)); + __code stati(Impl* fs , struct inode* ip, struct stat* st, __code next(...)); + __code readi(Impl* fs, struct inode* ip, char* dst, uint off, uint tot, uint n, __code next(int ret, ...)); + __code writei(Impl* fs, struct inode* ip, char* src, uint off, uint tot, uint n, __code next(int ret, ...)); + __code namecmp(Impl* fs, const char* s, const char* t, __code next(int strncmp_val, ...)); + __code dirlookup(Impl* fs, struct inode* dp, char* name, uint off, uint* poff, dirent* de, __code next(int ret, ...)); + __code dirlink(struct fs_impl* fs, struct inode* ip, struct dirent* de, struct inode* dp, char* name, uint off, uint inum, __code next(...)); + __code namei(Impl* fs, char* path, __code next(int namex_val, ...)); + __code nameiparent(Impl* fs, char* path, char* name, __code next(int namex_val, ...)); + __code next(...); +} fs; diff -r c8adccdd011a -r b67e4c9f0374 final_main/src/fs_impl1.h --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/fs_impl1.h Wed Feb 12 19:54:53 2020 +0900 @@ -0,0 +1,28 @@ +typedef struct fs_impl impl fs{ + __code allocinode(Type* fs_impl, uint dev, struct superblock* sb, __code next(...)); + __code allocinode_loop(Type* fs_impl, uint inum, uint dev, short type, struct superblock* sb, struct buf* bp, struct dinode* dip, __code next(...)); + __code allocinode_loopcheck(Type* fs_impl, uint inum, uint dev, struct superblock* sb, struct buf* bp, struct dinode* dip, __code next(...)); + __code allocinode_noloop(Type* fs_impl, uint inum, uint dev, short type, struct superblock* sb, struct buf* bp, struct dinode* dip, __code next(int ret, ...)); + __code lockinode1(Type* fs_impl, struct inode *ip, struct buf *bp, struct dinode *dip, __code next(...)); + __code lockinode2(Type* fs_impl, struct inode* ip, struct buf* bp, struct dinode* dip, __code next(...)); + __code lockinode_sleepcheck(Type* fs_impl, struct inode* ip, __code next(...)); + __code iput_check(Type* fs_impl, struct inode* ip, __code next(...)); + __code iput_inode_nolink(Type* fs_impl, struct inode* ip, __code next(...)); + __code readi_check_diskinode(Type* fs_impl,struct inode* ip, char* dst, uint n, next(int ret, ...)); + __code readi_loopcheck(Type* fs_impl, uint tot, uint m, char* dst, uint off, uint n, __code next(...)); + __code readi_loop(Type* fs_impl, struct inode *ip, struct buf* bp, uint tot, uint m, char* dst, uint off, uint n, __code next(...)); + __code readi_noloop(Type* fs_impl, uint n, __code next(int ret, ...)); + __code writei_check_diskinode(Type* fs_impl,struct inode* ip, char* src, uint n, __code next(int ret, ...)); + __code writei_loopcheck(Type* fs_impl, uint tot, uint m, char* src, uint off, uint n, __code next(...)); + __code writei_loop(Type* fs_impl, struct inode* ip, struct buf* bp, uint tot, uint m, char* src, uint off, uint n, __code next(...)); + __code writei_noloop(Type* fs_impl, struct inode* ip, uint n, uint off, __code next(int ret, ...)); + __code dirlookup_loopcheck(Type* fs_impl, struct inode* dp, char* name, uint off, uint* poff, dirent* de, next(...)); + __code dirlookup_loop(Type* fs_impl, struct inode* dp, char* name, uint off, uint inum, uint* poff, dirent* de, __code next(int ret, ...)); + __code dirlookup_noloop(Type* fs_impl, __code next(int ret, ...)); + __code dirlink_namecheck(Type* fs_impl, struct inode* ip, __code next(int ret, ...)); + __code dirlink_loopcheck(Type* fs_impl, struct dirent* de, struct inode* dp, uint off, __code next(...)); + __code dirlink_loop(Type* fs_impl, struct dirent* de, struct inode* dp, uint off, uint inum, __code next(...)); + __code dirlink_noloop(Type* fs_impl, struct dirent* de, struct inode* dp, uint off, uint inum, char* name, __code next(int ret, ...)); + __code next(...); + __code next2(...); +} fs_impl; diff -r c8adccdd011a -r b67e4c9f0374 slide/thesis_slide.md --- a/slide/thesis_slide.md Wed Feb 12 11:28:11 2020 +0900 +++ b/slide/thesis_slide.md Wed Feb 12 19:54:53 2020 +0900 @@ -6,7 +6,7 @@ ## 研究目的 -## Continuatuin based C +## Continuation based C ## CbC のコード例 * CbC では Code Gear は \_\_code Code Gear 名 (引数) の形で記述される