Mercurial > hg > Papers > 2023 > matac-sigos
view 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 source
%% %% 研究報告用スイッチ %% [techrep] %% %% 欧文表記無しのスイッチ(etitle,eabstractは任意) %% [noauthor] %% %\documentclass[submit,techrep]{ipsj} \documentclass[submit,techrep,noauthor]{ipsj} \usepackage[dvips, dvipdfmx]{graphicx} \usepackage{latexsym} \usepackage{listings} \lstset{ language=C, tabsize=2, frame=single, basicstyle={\tt\footnotesize}, % identifierstyle={\footnotesize}, % commentstyle={\footnotesize\itshape}, % keywordstyle={\footnotesize\ttfamily}, % ndkeywordstyle={\footnotesize\ttfamily}, % stringstyle={\footnotesize\ttfamily}, breaklines=true, captionpos=t, columns=[l]{fullflexible}, % xrightmargin=0zw, % xleftmargin=1zw, % aboveskip=1zw, numberstyle={\scriptsize}, % stepnumber=1, numbersep=0.5zw, % lineskip=-0.5ex } \usepackage{caption} \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline} \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\} \def\|{\verb|} % %\setcounter{巻数}{59}%vol59=2018 %\setcounter{号数}{10} %\setcounter{page}{1} \renewcommand{\lstlistingname}{Code} \begin{document} \title{Gears OSのファイルシステムとDB} \affiliate{IPSJ}{情報処理学会\\ IPSJ, Chiyoda, Tokyo 101--0062, Japan} \paffiliate{JU}{琉球大学大学院理工学研究科工学専攻知能情報プログラム\\ University of the Ryukyus, Graduate School of Engineering and Science} \author{又吉 雄斗}{Matayoshi Yuto}{KIE}[matac@cr.ie.u-ryukyu.ac.jp] \author{佐野 巧曜}{Sano Yoshiaki}{KIE}[yoshisaur@cr.ie.u-ryukyu.ac.jp] \author{河野 真治}{Kono Shinzi}{IE}[kono@ie.u-ryukyu.ac.jp] \begin{abstract} 当研究室では,Continuation based C(CbC)を用い,定理証明やモデル検査などで信頼性を保証することを目的としたGearsOSを開発している. OSにおいてファイルシステムは重要な機能の一つであるため実装する必要がある. 現在,一般的なアプリケーションはファイルシステムとデータベースを併用する形で構成される. DBはSQLによってデータの挿入や変更が可能だがスキーマを事前に定義したり,insert時にそれらのschemaを指定したりする必要がある. GearsOSのファイルシステムではSQLの機能に相当するgrepやfindなどのインターフェースを実装し, アプリケーションのデータベースとしてファイルシステムを使用する構成が取れるようにしたい. ファイルシステムとデータベースの違いについて考え,データベースとしても利用可能なファイルシステムを構築したい. 本研究では,ファイルシステムとデータベースの違いについて考察し,Gears OSのファイルシステムの設計について述べる. \end{abstract} % %\begin{jkeyword} %情報処理学会論文誌ジャーナル,\LaTeX,スタイルファイル,べからず集 %\end{jkeyword} % %\begin{eabstract} %This document is a guide to prepare a draft for submitting to IPSJ %Journal, and the final camera-ready manuscript of a paper to appear in %IPSJ Journal, using {\LaTeX} and special style files. Since this %document itself is produced with the style files, it will help you to %refer its source file which is distributed with the style files. %\end{eabstract} % %\begin{ekeyword} %IPSJ Journal, \LaTeX, style files, ``Dos and Dont's'' list %\end{ekeyword} \maketitle %1 \section{GearsOSにおけるファイルシステムとDB} アプリケーションの信頼性を保証することは 情報システムやコンピュータを用いる業務の信頼性の保障につながる重要な課題である. したがって,アプリケーションの信頼性を保証するために,基盤となるOSの信頼性を高める必要がある. 当研究室では,信頼性の保証を目的としたGearsOSを開発している. GearsOSは,OSの信頼性を定理証明やモデル検査を行うことで保証することを目指している\cite{modelcheck}. 同じく,当研究室で開発しているプログラム言語であるCbC(Continuation based C)で記述されており, ノーマルレベルとメタレベルを簡単に切り分けることを可能としている. そのようにして,CbCでメタレベルの処理を切り出したものに対して, 定理証明やモデル検査を行うことで信頼性を保証する. GearsOSは現在OSとして重要な機能がいくつか未実装であり, その一つとしてファイルシステムが挙げられる. ファイルシステムはファイルやディレクトリといった構造を持ち,データの保存,整理を行う. OSの機能の中でも特に重要な機能であるため,GearsOSにも実装を行う必要がある. GearsOSへファイルシステムとDBを実装するにあたり,RedBlackTreeを用いる. DBはファイルシステムと本質的に同じ役割を持っているため同じRedBlackTreeで 表現することが可能であると考える. よって,今回はGearsOSにおけるファイルシステムとDBをRedBlackTreeで実装するための 設計を行う. \section{Continuation based C} Continuation based C(CbC)\cite{cbcllvm,cbc}は,当研究室で開発しているCの下位言語である. CbCでは関数の代わりにCodeGearという単位でプログラミングを行う. CodeGearは\emph{\_\_code}という記述で宣言することができる. また,データの単位にはDataGearと呼ばれる変数データを用いる. 図\ref{fig:dgcg}はCodeGearと入出力の関係を表している. CodeGearはDataGearを入力として受け取り,別のDataGearに書き込み出力することができる. 特に,入力のDataGearをInput DataGear,出力のDataGearをOutput DataGearと呼ぶ. gotoで次のCodeGearに遷移することができ,その際,Output DataGearを次のCodeGearのInput DataGearとして渡すことができる. \begin{figure}[ht] \begin{center} \includegraphics[width=80mm]{figs/cgdg.pdf} \end{center} \caption{CodeGearと入出力の関係図} \label{fig:dgcg} \end{figure} CodeGearから次のCodeGearに遷移していく一連の動作を継続と呼ぶ. 通常の関数の場合,関数から次の関数へ遷移する時にfunction callが行われる. function callは前の関数へ戻る場合があり,そのためにcall stackを保存する. 他方,CbCの継続はfunction callをせずにgotoによるjmpで行われる. jmpはfunction callと異なり,call stackのような環境を保存しない. よって,CbCのgotoによる継続はfunction callによる継続と比較して軽量であるといえる. そのことから,CbCにおける継続をfunction callによる継続と区別して,軽量継続と呼ぶ. これらの仕組みにより,ノーマルレベルとメタレベルの処理を容易に切り分けることが可能となる. CbCのプログラム例をソースコード\ref{src:cbc}に示す. まずmain関数においてadd1 CodeGearへgotoを行う. その際add1へInput DataGearとしてnを渡す. Cのgotoが\emph{goto label;}という記法で,ラベリングした箇所へjmpを行うのに対し, CbCのgotoは\emph{goto add1(n);}という記法で,add1 CodeGearへn DataGearを渡してjmpを行う. add1は処理の最後にadd2 CodeGearへgotoを行う. その際Output DataGear out\_nをadd2のInput DataGearとして渡す. このようにCbCではCodeGearのOutput DataGearを次のCodeGearのInput DataGearとして渡すことを繰り返すことで処理を進める. \lstinputlisting[caption=CbCのプログラム例,label=src:cbc]{src/hello.cbc} \section{信頼性の保証を目的としたGearsOS} GearsOS\cite{gears,gearsos,cr}は当研究室で開発している,信頼性と拡張性の両立を目的としたOSである. GearsOSにはGearという概念があり,実行の単位をCodeGear,データの単位をDataGearと呼ぶ. 軽量継続を基本とし,stackを持たない代わりに全てをContext経由で実行する. 同様にGearの概念を持つContinuation based C(CbC)で記述されており,ノーマルレベルとメタレベルの処理を切り分けることが容易である. また,GearsOSは現在開発途上であり,OSとして動作するために今後実装しなければならない機能がいくつか残っている. ContextはGearsOS上全てのCodeGear,DataGearの参照を持ち,CodeGearとDataGearの接続に用いられる. OS上の処理の実行単位で,従来のOSにおけるプロセスに相当する機能であるといえる. また,CodeGearをDataGearの一種であると考えると,ContextはGearの概念ではMetaDataGearに当たる. Contextはノーマルレベルから直接参照されず,必ずMetaDataGearとしてMetaCodeGearから参照される. それは,ノーマルレベルのCodeGearがContextを直接参照してしまうと, メタレベルを切り分けた意味がなくなってしまうためである. 図\ref{fig:context}はContextを参照する流れを表したものである. まずCodeGearがOutputDataGearへデータをoutputする. stubCodeGearはInputDataGear(前のCodeGearのOutputDataGear)とOutputDataGearをContextから参照し,次のCodeGearへgotoを行う. CodeGearでの処理後,OutputDataGearへデータをoutputする. Contextはいくつかの種類に分けることができる. OS全体のContextを管理するKernel Contextやユーザープログラムごとに存在するUser Context, CPUやGPUごとに存在するCPU Contextがある. \begin{figure}[ht] \begin{center} \includegraphics[width=80mm]{figs/context.pdf} \end{center} \caption{Contextを参照する流れ} \label{fig:context} \end{figure} 図\ref{fig:meta-cgdg}はCodeGearの遷移とMetaCodeGearの関係を表している. OSのプログラムはユーザーが実際に行いたい処理を表現するノーマルレベルと, カーネルが行う処理を表現するメタレベルが存在する. ノーマルレベルで見るとCodeGearがDataGearを受け取り, 処理後にDataGearを次のCodeGearに渡すという動作をしているように見える. しかしながら,実際にはデータの整合性の確認や資源管理などのメタレベルの処理が存在し, それらの計算はMetaCodeGearで行われる. その際,MetaCodeGearに渡されるDataGearのことは特にMetaDataGearと呼ばれる. また,CodeGearの前に実行されるMetaCodeGearは特にstubCodeGearと呼ばれ, メタレベルを含めるとstubCodeGearとCodeGearを交互に実行する形で遷移していく. \begin{figure}[ht] \begin{center} \includegraphics[width=80mm]{figs/meta-cg-dg.pdf} \end{center} \caption{CodeGearとMetaCodeGearの関係} \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で構成する. ファイルシステムとDBの違いとして,スキーマが挙げられる. DBは事前にスキーマを定義し,それに沿ってデータを挿入したり参照したりする. 対して,ファイルシステムにはスキーマに当たるものがなく, データはファイルパスによって管理される. スキーマを定義することによってデータは構造化され, 構造化されたデータは非構造化データと比較して, インデックスを作成することが容易であり,データの検索性が向上する利点がある. しかしながら,スキーマはDBの運用中に変更されることがあり, スキーマを変更した以前へロールバックができない問題がある. ロールバックがスキーマの変更によって出来なくなることは信頼性に問題があると考えると, スキーマを定義する必要のないスキーマレスなDBが必要になる. ファイルシステムはスキーマレスなDBといえるので,ファイルシステムを構築しつつ DBがスキーマによって実現していた機能を付け加えることを試みる. RedBlackTreeは実装によって,操作が破壊的なものとそうでないものがある. 今回用いるのは,非破壊的な実装のRedBlackTreeである. 図\ref{fig:TreeEdit}は非破壊的編集を行うRedBlackTreeを表している. 編集前の木構造の6のノードをAにアップデートすることを考える. まず,ルートノードからアップデートしたいノード6までをコピーする. その後,コピーしたもののノード6をAにアップデートする. これにより,アップデート前のノード6を破壊することなくAにアップデートが可能である. 参照する時は,黒のルートノードから辿れば古い6が,赤のルートノードから辿れば新しいAが見える. この仕組みは,データのバックアップやDBのロールバックに用いることが可能だと考える. \begin{figure}[ht] \begin{center} \includegraphics[width=80mm]{figs/nonDestroyTreeEdit.pdf} \end{center} \caption{非破壊的なTree編集} \label{fig:TreeEdit} \end{figure} \section{ディスク上とメモリ上のデータ構造} ディスク上とメモリ上でデータの構造は,RedBlackTreeに統一する. 一般的に,ディスク上のデータ構造としてB-Treeが用いられることが多い. なぜならば,HDDを用いる場合はブロックへのアクセス回数を減らしデータアクセスの時間を短くするために, B-Treeのようなノードを複数持つことができる構造が効果的だからである. その点ではRedBlackTreeはB-Treeに劣る. しかしながら,SSDはランダムアクセスによってデータにアクセスするため, RedBlackTreeでなくB-Treeを用いる利点は少ないと考える. よって,ディスク上とメモリ上のデータ構造をRedBlackTreeに統一することが考えられる. そうすることによって,ディスク上とメモリ上のデータのやりとりは単純なコピーで実装できる. \section{データのロールバックとバックアップ} DBの重要な機能の一つにロールバックがある. RDBのロールバックは, コミットするまではトランザクションの開始時点に戻ることができる機能である. コミットが完了するとそれ以前の状態に戻すことはできないが, データのバックアップをとっておくことで復元を行う. このような,ロールバックとバックアップの仕組みをファイルシステムに実装したい. 今回は,RedBlackTreeのルートノードがデータのバージョンの役割を果たしていることを利用し, データの復元が行える仕組みを構築することを考える. 非破壊的なTree編集はアップデートのたびに,ルートノードを増やす. つまり,ルートノードはアップデートのログと言えその時点のデータのバージョンを表していると考えることができる. よって,ロールバックを行いたい場合は参照を過去のルートノードに切り替える. ルートノードはデータのアップデート時に増えるため, データが際限なく増加していく問題がある. この問題はCopyingGCを行うことによって解決する. まず,RedBlackTreeを丸ごとコピーして最新のルートを残して他のルートは削除する. その後,コピーしたものはバックアップとしてディスクに書き込む. そうすることで,データの増加によるリソースの枯渇を防ぎ, かつデータのバックアップを作成することで信頼性の向上が期待できる. \section{RedBlackTreeのトランザクション} トランザクションはDBの重要な機能の一つである. データの競合を防ぎ信頼性を向上させ,DBとしても扱えるよう トランザクションの仕組みを考える必要がある. 今回,ファイルシステムは全てRedBlackTreeで実装するため, RedBlackTreeのノードに対するトランザクションを考える. トランザクションをwriteとreadに分けて考える. writeする場合,トランザクションはRedBlackTreeのルートの置き換えと対応する. writeするために,まずルートを生やし書き込みが終わった後ルートを置き換える. そのため,書き込みの並列度はルートの数と一致する. しかしながら,ルートの置き換えは競合的なので, 複数書き込みを行っても1つしか成功しない. よって,単一のRedBlackTreeに複数の書き込みポイントを作り, 並行実行可能にする必要がある. RedBlackTreeに複数の書き込みポイントを作るために, キーごとのルートを作成する. ノードはそれぞれがキーとRedBlackTreeを持つ状態になる. writeする際は,そのキーのルートを置き換える. それによって,RedBlackTreeは複数の書き込みポイントを持つことができ, writeを並行実行することが可能となる. readはデータに変更を加えないため,複数同時に同じノードを読み込むことが可能である. しかし,常に最新の情報を読み込めるとは限らない. 最新の情報が欲しい場合は書き込みを一旦止めるような処理が必要になる. \section{ファイルシステムにおけるスキーマ} 従来のSQLのようなスキーマが存在すると, 個別にバックアップなどを取らない限り スキーマの変更以前にロールバックすることができない. しかしながら,実際運用する上でスキーマを変更することは多々ある. これは,データの信頼性を低下させると考える. また,DB上のデータ構造とプログラム上で扱うデータ構造に差が生まれる インピーダンスミスマッチが発生し,DBのデータをプログラムが扱う際に その差を埋めるような変換を必要とする場合が生まれる. 一方で,スキーマがあることによってデータに対して高度な操作を行なったり, インデックスを容易に作成することができたりするといったメリットがある. よって,スキーマフルなDBとスキーマレスなDBはそれぞれメリットデメリットがあり, 状況によって使い分けるのが良いと考える. 今回は,非構造化データ内であれば構造化データを扱うことが可能であることと, 信頼性を保証したいという点から, スキーマレスなDBとしてのファイルシステムを考える. しかしながら,トランザクションの仕組みを作る上でRedBlackTreeに対し, キーを設定することから完全なスキーマレスとは言えない構成となる. GearsOSのデータは全てDataGearで表される. よって,GearsOSにおけるファイルシステムはDataGearの集合となる. スキーマレスとはキーがない状態のことといえるが, DataGearはキーが設定されていないため,その集合自体にスキーマは無い. そのことから,GearsOSにおけるスキーマとはDataGear上のキーの構成であることがわかる. なお,今回のRedBlackTreeによる構成の場合,キーはRedBlackTreeを指す. DataGearはKernelのContextからプロセスのContextを経由して全て繋がっている. よって,KernelのContext上にキーを用いたDataGearの参照を書き込む. \section{RedBlackTreeによる権限の表現} ファイルの権限はファイルシステムの重要な機能の一つであるため実装する必要がある. 今回のRedBlackTreeによる構成の場合,木のルートの所持者を設定することが ファイルに対して権限を設定することにあたる. ルートに対してアクセスする権限がなければ, 読み書きができないといった実装になると考える. \section{まとめと今後の課題} 本論文ではGearsOSのファイルシステムとDBの設計について説明した. 今後,実装を行いながら設計と動作の確認,計測を行い, 設計の意図が反映されていることやプログラムの検証ができることを確認する必要がある. また,今後の課題や議題として次のようなものが挙げられる. \subsection{ログなどの時系列データの保存} \subsection{スタンドアロンなDB} \subsection{インデックスの更新・作成} \subsection{データクエリ言語} \nocite{*} \bibliographystyle{ipsjunsrt} \bibliography{matac-bib} \end{document}