view Paper/paper.tex @ 10:a8cea37083e2

fix: ( to (
author matac42 <matac@cr.ie.u-ryukyu.ac.jp>
date Thu, 05 May 2022 21:15:02 +0900
parents 8519074552f9
children 90a3b987451a
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{GearsOSにおけるinodeを用いたファイルシステムの構築}

\etitle{Building a Filesystem using inode in GearsOS}

\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{河野 真治}{Kono Shinzi}{IE}[kono@ie.u-ryukyu.ac.jp]

\begin{abstract}
アプリケーションの信頼性を保証するために,アプリケーションが動作するOSの信頼性を高める必要がある.
当研究室では,CbC(Continuation Based C)を用い,定理証明やモデル検査による信頼性の保証を目的としたGearsOSを開発している.
CbCは当研究室で開発しているノーマルレベル,メタレベルの処理を切り分けることができるC言語の下位言語である.
GearsOSで未実装の機能であるファイルシステムをinodeの仕組みを用いて実装を行う.

\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におけるファイルシステム}

アプリケーションの信頼性を保証することは
情報システムやコンピュータを用いる業務の信頼性の保障につながる重要な課題である.
したがって,アプリケーションの信頼性を保証するために,基盤となるOSの信頼性を高める必要がある.

当研究室では,信頼性の保証を目的としたGearsOSを開発している.
GearsOSは,OSの信頼性を定理証明やモデル検査を行うことで保証することを目指している\cite{modelcheck}.
同じく,当研究室で開発しているプログラム言語であるCbC(Continuation based C)で記述されており,
ノーマルレベルとメタレベルを簡単に切り分けることを可能としている.
そのようにして,CbCでメタレベルの処理を切り出したものに対して,定理証明やモデル検査を行うことで信頼性を保証する.

GearsOSは現在OSとして重要な機能がいくつか未実装であり,その一つとしてファイルシステムが挙げられる.
ファイルシステムはファイルやディレクトリといった構造を持ち,データの保存,整理を行う.
また,OSが管理するデータの操作を人間が行いやすいようにインターフェースを提供する.
OSの機能の中でも特に重要な機能であるため,GearsOSにも実装を行う必要がある.

今回GearsOSへファイルシステムを実装するにあたり,Unixのファイルシステムを参考にした.
Unixのファイルシステムではファイルのメタデータをinodeの形式で保持している.
同様に,inodeの仕組みを用いてGearsOSのファイルシステムを実装したい.
また,インターフェースについても,cd,ls,mkdirというようにUnix likeに実装したい.
当研究室ではxv6のCbCでの書き換えを行なっているが,今回はxv6のルーチンをCbCで書き換えるのではなく
GearsOSへUnixのファイルシステムの仕組みを取り入れるアプローチをとりたい.
それはGearsOSとCbCで書き換えたxv6の比較や,互いにファイルシステムの機能の移植が行える様にするためである.

\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による継続と区別して,軽量継続と呼ぶ.
これらの仕組みにより,ノーマルレベルとメタレベルの処理を容易に切り分けることが可能となる.

\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}

\section{Unixのファイルシステム}

UnixのファイルシステムはBTreeとinodeで構成されており,xv6もその仕組みを用いている.
xv6\cite{xv6}はMITで教育用の目的で開発されたOSで,Unixの基本的な構造を持つ.
当研究室ではxv6のCbCでの書き換え,分析を行なっている\cite{xv6component,xv6kernel}.

inodeは主にUnix系のファイルシステムで用いられる,ファイルの属性情報が書かれたデータである.
inodeにおけるファイルの属性情報はFile Type,Permissions,File Sizeなどが上げられる.
また,inodeは識別番号としてinode numberを持つ.
inode numberは一つのファイルシステム内で一意の番号であり,\emph{ls -i}コマンドで確認可能である.
inodeはファイルシステム始動時にinode領域をディスク上に確保する.
そのため,inode numberには上限があり,それに伴いファイルシステム上で扱えるファイル数の上限も決まる.
inode numberの最大値は\emph{df -i}コマンドで確認可能である.

\section{GearsFileSystemにおけるディレクトリの構成}

当研究室ではxv6のCbCでの実装を行なっているが,今回はxv6のFileルーチンをCbCで書き換えるのではなく
GearsOSへUnixのファイルシステムの仕組みを取り入れるアプローチをとる.
まず,ファイルシステムを大まかにディレクトリシステムとファイルの二つに分けて考える.
ディレクトリシステムはUnixのinodeの仕組みを取り入れる.
今回作成した,GearsOSのディレクトリシステムであるGearsDirectoryについて説明する.
ファイルについては後の章で述べる.

FileSystemTreeはディレクトリ構造,inodeの仕組みを取り入れる際に用いるTreeである.
ソースコード\ref{src:ftree}はFileSystemTreeのinterfaceである.
GearsOSにおけるinterfaceはCodeGearと各CodeGearが用いるI/O DataGearの集合を記述する.
よって,FileSystemTreeのinterfaceはfTreeとnodeのDataGearとput,get,remove,nextのCodeGearを持つ.
FileSystemTreeのfTreeはGearsOSの永続データを構築する際に使用されるRedBlackTreeであり,put,get,removeはRedBlackTreeの操作を行うためのCodeGearである.
また,nextは遷移先のCodeGearを参照するために用いる.
\lstinputlisting[caption=FTreeのinterface,label=src:ftree]{src/FTree.h}

ディレクトリ構造は2つのFileSystemTreeで実装する.
1つ目はinode numberとfileのポインタのペアを持つ木である.
それは,inode numberをkey,inodeをvalueとして持つためinode numberからinodeを検索するために用いる(以下,inode treeとする).
2つ目はfilenameとinode numberのペアを持つ木である.
それは,filenameをkey, inode numberをvalueとして持つため,filenameからinode numberを検索するために用いる.
また,inodeをfilenameで検索するためのindex treeであるといえる(以下,index treeとする).

図\ref{fig:inode}はindex treeを用いたinodeの検索の流れを表す.
まずindex treeからkeyがfilenameのnodeをgetする.
keyがfilenameのnodeのvalueよりinode numberがわかる.
次に,取得したinode numberをkeyとしてinode treeを検索する.
keyがinode numberのnodeはvalueとしてinodeを持っていて,inodeを参照することができる.

\begin{figure}[ht]
  \begin{center}
      \includegraphics[width=80mm]{figs/inode.pdf}
  \end{center}
  \caption{index treeを用いたinodeの検索の流れ}
  \label{fig:inode}
\end{figure}

GearsOSにおける永続データは非破壊的な編集を行う木構造を用いて保存する.
図\ref{fig:TreeEdit}は非破壊的編集を木構造に対し行う様子である.
赤で示されたノード6をAに編集する場合,まずルートノードから編集ノードまでのパスを全てコピーする.
コピーしたパス上に存在しないノードは,コピー元の木構造と共有する.
それにより,編集後の木構造の赤のルートノードから探索を行う場合は編集されたAのノードが見え,
黒のルートノードから探索を行う場合は編集前の6のノードを見ることができる.
ディレクトリシステムを非破壊的な木構造の編集を用いて実装することにより,
ディレクトリシステム自体にバックアップの機能を搭載することが可能であると考える.

\begin{figure}[ht]
  \begin{center}
      \includegraphics[width=80mm]{figs/nonDestroyTreeEdit.pdf}
  \end{center}
  \caption{非破壊的なTree編集}
  \label{fig:TreeEdit}
\end{figure}

\section{GearsFileSystemにおけるインターフェース}

ファイルやディレクトリの操作を行うインターフェースをUnix Likeに実装を行った.
実装を行ったmkdir, ls, cdを説明する.

\subsection{mkdir}
Unixにおいてmkdirは新しくディレクトリを作成するコマンドである.
GearsDirectoryのmkdirはindex treeとinode treeにnodeをputすることでディレクトリを作成する.
ソースコード\ref{src:mkdir}はGearsDirectoryにおけるmkdirのCodeGearであり,図\ref{fig:mkdir}はその処理を図で表したものである.
まず1行目の\emph{\_\_code mkdir}ではinode treeへinodeのputが行われ,\emph{\_\_code mkdir2}へ遷移する.
inodeは4,5行目でkeyにinode number, valueにディレクトリのポインタがセットされる.
次に,11行目の\emph{\_\_code mkdir2}ではindex treeへkeyがfilename,valueがinode numberのnodeのputが行われ,nextのCodeGearへ遷移する.
このように,FileSystemTreeのputを2回行うため,mkdirは\emph{\_\_code mkdir}と\emph{\_\_code mkdir2}の2つのCodeGearで構成されている.
また,InputDataGearの\emph{name}はfilenameを表す.
\lstinputlisting[caption=mkdirのCodeGear,label=src:mkdir]{src/mkdir.cbc}
\begin{figure}[ht]
  \begin{center}
      \includegraphics[width=80mm]{figs/mkdir.pdf}
  \end{center}
  \caption{mkdirの操作の流れ}
  \label{fig:mkdir}
\end{figure}

\subsection{ls}
Unixにおいてlsはファイルやディレクトリの一覧,メタ情報を表示するコマンドである.
GearsDirectoryのlsはindex treeに対し,getをすることでディレクトリのnameを取得する.
これは,Unixのlsコマンドにおける\emph{\$ls filename}に等しい機能である.
ソースコード\ref{src:ls}はGearsDirectoryにおけるlsのCodeGearであり,図\ref{fig:ls}はその処理を図で表したものである.
まず1行目の\emph{\_\_code ls}ではindex treeに対しgetを行うため,
3行目でgetしたいfilenameをkeyにセットし,index treeのgetへgotoしている.
その後,9行目の\emph{\_\_code ls2}ではnode\verb|->|keyに格納されたgetの結果をprintfで出力する.
本来lsコマンドは引数を渡さずに実行するとカレントディレクトリ下のディレクトリやファイルを一覧で表示するが,
現時点では未実装である.
なお,一覧表示の機能はfilenameのリストをディレクトリに持たせることで実装可能であると思われる.
\lstinputlisting[caption=lsのCodeGear,label=src:ls]{src/ls.cbc}
\begin{figure}[ht]
  \begin{center}
      \includegraphics[width=80mm]{figs/ls.pdf}
  \end{center}
  \caption{lsの操作の流れ}
  \label{fig:ls}
\end{figure}

\subsection{cd}
Unixにおいてcdはディレクトリを移動するコマンドである.
GearsDirectoryのcdはindex treeとinode treeに対しgetを行い,currentDirectoryを書き換えることで実装する.
機能としてはディレクトリが持つ子ディレクトリへの移動ができる.
ソースコード\ref{src:cd}はGearsDirectoryにおけるcdのCodeGearであり,図\ref{fig:cd}はその処理を図で表したものである.
まず1行目の\emph{\_\_code cd2Child}でindex treeに対しgetを行うため,index treeのgetへgotoしている.
次に,9行目の\emph{\_\_code cd2Child2}でinode treeに対しgetを行うため,inode treeのgetへgotoしている.
この際,getは1行目のcd2Childでgetしたnodeのvalueをもとに行う.valueにはinode numberがセットされている.
その後,15行目の\emph{\_\_code cd2Child3}でcurrent ディレクトリを保存しているgearsDirectory\verb|->|currentDirectoryを
getしたnode\verb|->|valueに書き換える.
\lstinputlisting[caption=cdのCodeGear,label=src:cd]{src/cd.cbc}
\begin{figure}[ht]
  \begin{center}
      \includegraphics[width=80mm]{figs/cd.pdf}
  \end{center}
  \caption{cdの操作の流れ}
  \label{fig:cd}
\end{figure}

\section{GearsFileSystemにおけるファイルの構成}

ファイルシステムはディレクトリの構成だけでなく,ファイルの構成についても考える必要がある.
本研究と並行する形で一木貴裕による分散ファイルシステムの設計が行われており\cite{cfile},
ファイルの構成に関しても実装,検討されている.
GearsOSにおけるファイル構成を説明する.

ファイルのInput/Output Streamは競合的なアクセスに対応するため,3つのSynchronizedQueueを用いる.
それぞれをInputQueue, OutputQueue, mainQueueと呼ぶ.
データをinputしたい場合InputQueueへputを行い,取得したい場合OutputQueueからgetを行う.
mainQueueはデータそのものであり,InputQueueからmainQueue,mainQueueからOutputQueueへデータが流れるように接続される.
これらは,Gearの概念ではDataGearにあたり,DataGearManagerにkeyとI/O Queueが対応する形で保持される.
ファイルの中身のデータをレコードに分割し,レコードをQueueにputしてstreamに入れる.
データを取り出す際はQueueからgetし,順番に読むことでファイルを構築する.

分散ファイルシステムはファイルのデータ送受信をする際に用いられるAPIを作成する必要がある.
WordCount例題\cite{file}を通して,GearsFileのAPIの作成を行う.
WordCount例題は指定したファイルの文字数や行数,ファイルの内の文字列を出力する.
図\ref{fig:WCStates}はWordCount例題の処理の流れを示している.
これは大きく分けて,指定したファイルをFile構造体としてopenするFileOpenスレッド,
File構造体を受け取り文字数と行数をcountUpするWordCountスレッドの二つのCodeGearで記述することができる.
また,ファイル内の文字列を行ごとにCountUpに送信し,EOFを受け取ったらループを抜けfinishに移行する.
\begin{figure}[ht]
  \begin{center}
      \includegraphics[width=80mm]{figs/wordCountStates.pdf}
  \end{center}
  \caption{WordCount with CbC}
  \label{fig:WCStates}
\end{figure}

\section{今後の課題}

\subsection{GearsShell}
GearsOSに存在する未実装の機能の一つにshellが挙げられる.
現状のGearsOSはユーザーの入力を受け付けることが出来ず,プログラミングインターフェースの様に機能している.
GearsFileSystemなどGearsOSの各機能と接続し,今回作成したcdやlsの様なコマンドを受け付けるGearsShellを作成したい.

\subsection{GearsDirectory filename}
現状はGearsDirectoryのfilenameはIntegerの構造で管理されている.
しかしながら,filenameは一般的に文字列型であるためIntegerから文字列型に変更する必要がある.

\subsection{GearsDirectory path}
GearsDirectoryにはpathの機能が実装されていない.
よってfull path指定のlsなどが実装できない状態である.
FileSystemTreeを拡張し,ノードをたどりpathを生成する様な機能を実装する必要がある.

\subsection{ファイルのバックアップ}
ディレクトリに関しては非破壊的なTree編集を用いることで,バックアップを行うことを考えたが
ファイルに関してはレコードのDataをファイルの差分履歴として保持し,
日時情報を付け加えることでVersion Control Systemのような機能を持たせることが可能であると考えられる.

\subsection{GearsDirectory on disk}
現状はGearsDirectoryのinodeはon memoryで実装されている.
データの保存はdisk上に行うため,inodeをdisk上に構築し必要がある

\subsection{Memory Management}

\section{まとめ}

本研究では主としてGearsFileSystemの構築に必要なGearsDirectoryの実装について説明した.
いくつか課題はあるが,RedBlackTreeのシンプルなinterfaceにより比較的容易に実装を行うことができた.
また,RedBlackTreeを用いてinodeの仕組みを構築し,ls,cd,mkdirを作成するなどして,
Unix Likeに構築することが出来た.

信頼性については,定理証明やモデル検査を用いて保証を行うが,
非破壊的なTree編集によるディレクトリのバックアップやファイルのバックアップをファイルシステムに組み込むことでも
信頼性の向上が期待できる.形式手法とファイルシステムの機能の両面で信頼性の向上が図れると考える.

\nocite{*}
\bibliographystyle{ipsjunsrt}
\bibliography{matac-bib}

\end{document}