Mercurial > hg > Papers > 2023 > matac-sigos
diff Paper/paper.tex @ 14:c0cdf7130bd8
...
author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 17 Apr 2023 09:42:47 +0900 |
parents | bb32b4cbb6d6 |
children | 619ba13d0661 |
line wrap: on
line diff
--- a/Paper/paper.tex Mon Apr 17 03:24:55 2023 +0900 +++ b/Paper/paper.tex Mon Apr 17 09:42:47 2023 +0900 @@ -96,7 +96,7 @@ \maketitle %1 -\section{GearsOSにおけるファイルシステム} +\section{GearsOSにおけるファイルシステムとDB} アプリケーションの信頼性を保証することは 情報システムやコンピュータを用いる業務の信頼性の保障につながる重要な課題である. @@ -106,14 +106,19 @@ GearsOSは,OSの信頼性を定理証明やモデル検査を行うことで保証することを目指している\cite{modelcheck}. 同じく,当研究室で開発しているプログラム言語であるCbC(Continuation based C)で記述されており, ノーマルレベルとメタレベルを簡単に切り分けることを可能としている. -そのようにして,CbCでメタレベルの処理を切り出したものに対して,定理証明やモデル検査を行うことで信頼性を保証する. +そのようにして,CbCでメタレベルの処理を切り出したものに対して, +定理証明やモデル検査を行うことで信頼性を保証する. -GearsOSは現在OSとして重要な機能がいくつか未実装であり,その一つとしてファイルシステムが挙げられる. +GearsOSは現在OSとして重要な機能がいくつか未実装であり, +その一つとしてファイルシステムが挙げられる. ファイルシステムはファイルやディレクトリといった構造を持ち,データの保存,整理を行う. -また,OSが管理するデータの操作を人間が行いやすいようにインターフェースを提供する. OSの機能の中でも特に重要な機能であるため,GearsOSにも実装を行う必要がある. -今回GearsOSへファイルシステムを実装するにあたり, +GearsOSへファイルシステムとDBを実装するにあたり,RedBlackTreeを用いる. +DBはファイルシステムと本質的に同じ役割を持っているため同じRedBlackTreeで +表現することが可能であると考える. +よって,今回はGearsOSにおけるファイルシステムとDBをRedBlackTreeで実装するための +設計を行う. \section{Continuation based C} @@ -162,15 +167,6 @@ 同様にGearの概念を持つContinuation based C(CbC)で記述されており,ノーマルレベルとメタレベルの処理を切り分けることが容易である. また,GearsOSは現在開発途上であり,OSとして動作するために今後実装しなければならない機能がいくつか残っている. -GearsOSには現在3つの種類がある. -1つ目が型式手法による信頼性の向上を目的とした,GearsAgdaと呼ばれるGearsOSである. -これは,Agdaによって実装されている. -2つ目がユーザーレベルタスクマネジメントの実装を目的としたGearsOSがある. -これは,CbCによって実装されている. -3つ目はスタンドアロンOSの開発を目的とした,CbC\_xv6と呼ばれるGearsOSがある. -これは,教育用に開発されたx.v6 OSをCbCで書き換える形で実装している. -今回,ファイルシステムを実装する対象は3つ目のCbC\_xv6である. - ContextはGearsOS上全てのCodeGear,DataGearの参照を持ち,CodeGearとDataGearの接続に用いられる. OS上の処理の実行単位で,従来のOSにおけるプロセスに相当する機能であるといえる. また,CodeGearをDataGearの一種であると考えると,ContextはGearの概念ではMetaDataGearに当たる. @@ -212,12 +208,21 @@ \label{fig:meta-cgdg} \end{figure} +GearsOSには現在3つの種類がある. +1つ目が型式手法による信頼性の向上を目的とした,GearsAgdaと呼ばれるGearsOSである. +これは,Agdaによって実装されている. +2つ目がユーザーレベルタスクマネジメントの実装を目的としたGearsOSがある. +これは,CbCによって実装されている. +3つ目はスタンドアロンOSの開発を目的とした,CbC\_xv6と呼ばれるGearsOSがある. +これは,教育用に開発されたx.v6 OSをCbCで書き換える形で実装している. +今回,ファイルシステムを実装する対象は3つ目のCbC\_xv6である. + \section{RedBlackTreeよるファイルシステムの構成} ファイルシステムは全てRedBlackTreeで構成する. それにより,プログラムの証明がより簡単になるからである. また,ファイルシステムとDBはデータを保管するという本質的な役割は同じである. -よって,それらをまとめてRedBlackTreeで構成する. +よって,それらはまとめてRedBlackTreeで構成する. ファイルシステムとDBの違いとして,スキーマが挙げられる. DBは事前にスキーマを定義し,それに沿ってデータを挿入したり参照したりする. @@ -265,8 +270,6 @@ よって,ディスク上とメモリ上のデータ構造をRedBlackTreeに統一することが考えられる. そうすることによって,ディスク上とメモリ上のデータのやりとりは単純なコピーで実装できる. -% メモリからディスクに書き戻すタイミングの話をしたい - \section{データのロールバックとバックアップ} DBの重要な機能の一つにロールバックがある. @@ -350,10 +353,6 @@ DataGearはKernelのContextからプロセスのContextを経由して全て繋がっている. よって,KernelのContext上にキーを用いたDataGearの参照を書き込む. -\section{i-node numberによるインデックス} - - - \section{RedBlackTreeによる権限の表現} ファイルの権限はファイルシステムの重要な機能の一つであるため実装する必要がある. @@ -362,9 +361,22 @@ ルートに対してアクセスする権限がなければ, 読み書きができないといった実装になると考える. -\section{今後の課題} +\section{まとめと今後の課題} + +本論文ではGearsOSのファイルシステムとDBの設計について説明した. +今後,実装を行いながら設計と動作の確認,計測を行い, +設計の意図が反映されていることやプログラムの検証ができることを確認する必要がある. + +また,今後の課題や議題として次のようなものが挙げられる. -\section{まとめ} +\subsection{ログなどの時系列データの保存} + +\subsection{スタンドアロンなDB} + +\subsection{インデックスの更新・作成} + +\subsection{データクエリ言語} + \nocite{*} \bibliographystyle{ipsjunsrt}