\chapter{GearsOSにおけるファイルシステム}
コンピュータにおけるファイルシステムは必要不可欠な存在であると言える。
コンピュータで行われる計算やそれに使われるデータは全て記憶装置上にファイルとして保持され、
ファイルという概念なしにはユーザーがコンピュータ上で用いられる資源の管理はほぼ不可能であると言える。
コンピュータの技術発展と普及に伴いファイルは物理的な存在場所に囚われない、
つまりネットワークへの接続を通して別マシン上のどこからでもアクセスが行える存在である必要が生じてきた。
物理的な位置を問わずネットワークを通してファイルを共有する機能を有するファイルシステムを特に分散ファイルシステムと呼ぶ。
分散ファイルシステムはネットワークに配置されたファイルに対して、ローカルに保存されたファイルとほとんど相違なく取り扱いが行える透過性が求められる。

・・・既存のファイルシステムとか語る？今のファイルシステムの問題点とか？

・・・アプリケーションであるFSとOSに実装されたFS？

また、当研究室では信頼性の保証と拡張性の高さを目指したOSプロジェクトである、GearsOSの開発を行なっている。
GearsOSはテストコードでなく、AgdaやCoqなどの型式手法に含まれる定理証明支援系やモデル検査を用い、
実施にOSとして動作するコードそのものを検証することで信頼性の補償を目指している。
また、GeasOSはノーマルレベルとメタレベルを分離して記述するContinuation based C(CbC)にて記述される。
ノーマルレベルとはユーザが行いたい計算をさし、メタレベルとはノーマルレベルの計算を行うための計算をさす。
ノーマルレベルのプログラムのメタレベルに対して自由に差し替えを行うことにより、
コードの整合性の検証やプログラムのデバッグを行えるような作りとなっている。

現状においてGearsOSは言語フレームワークとして実装されており、
実際にOSとして起動するためにはこれから実装が必要となる機能が複数存在している。
その中の一つとして分散ファイルシステムが挙げられる。
GearsOSのファイルシステムは既存のOSが持つファイルシステムの問題点の解決や
従来ではアプリケーションが担っているバックアップを始めとした機能を搭載したファイルシステムの構成を目指して開発を行いたいと考えた。
問題点の解決の一部として、既存のファイルシステムとは異なりファイルシステムをデータベースとして構成したい。
レコードでファイルデータを取り扱うことによりファイルの更新や操作を簡潔に行い、またFileSystemのAPIを総括してトランザクションとしたい。
加えて、データのバックアップについてもOSに搭載したい。
従来のようにバックアップデータをユーザが管理するのではなく、OSが管理をすることによりバックアップデータ自体の紛失を防ぎたい。

また、分散ファイルシステムは当研究室が開発している分散フレームワークであるChristieの仕組みを用いて構成する。
Christieを基盤としたファイルシステムを構築する理由として、
Christieの独自なシンタックスによる簡潔なプログラムにより複雑な分散処理の記述が行えるようにする目的が挙げられる。
加えてChristieが持つ、処理を行うノードごとの接続(Topology形成)の自動化を行うTopologyManagerが用いることができるようになり、
ファイルシステム上の通信接続は全てTopologyManagerに一任することができるようになる。