\chapter{GearsOSにおけるFile system}

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

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

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

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

本論文ではGearsOSのファイルシステムに関する基礎概念と，ファイルシステムの構築について記述する．