# GearsOSの分散ファイルシステムの設計 author: 一木 貴裕, 河野 真治 profile: 琉球大学理工学研究科情報工学専攻 河野研究室 lang: Japanese code-engine: coderay ## OSと密に結合したファイルシステムの設計 - 信頼性と拡張性の保証を目的としたGearsOSを開発中 - GearsOSの分散ファイルシステムを開発したい - 分散フレームワークChristieの構成をもとにする - Christieが持つTopologyManagerという機能を使う - プログラムの通信とストレージの接続を管理する ## 従来のファイルシステムの問題点 - データベースになっていない - 重複度やリカバリをアプリケーションが担当している - 暗号化などのセキュリティもアプリケーションが担当している - OS自体がこれらの機能を持つのが望ましい ### 従来のファイルシステムのトランザクション - レコードのTransactionとして提供していない - 提供しているのは - ファイルのロック - ディレクトリの名前の置き換え - FileSystemのAPIを総括してトランザクションとして設計したい ### ファイルの型 - OSレベルから見たファイルの型が存在しない - 実行形式のみをOSが認識している - 型の区別はアプリケーションに委ねられている - lsとreadmeなどの型の区別がつかない - OS自体がファイルの型を見分けるように設計したい ### ファイルの名前自体がデータベースのkeyとなっていない - 従来ではファイル固有のIDとファイル名を紐付けしたりする - 様々なファイル単位が混同になっている - 複数のレコード - 複数の表 - sqlite3 - OS自体がユニークなファイルIDのリストを保持する設計にしたい ### 重複度とファイルリカバリ - ファイルの複製が行われた際の安全性が確保できない - バックアップデータを勝手な場所に置かれてしまう - バックアップデータをOSが管理する ### 署名と暗号化 - ファイルの署名もしくは暗号化の機能をOSファイルシステムに持たせたい - 公開鍵と秘密鍵 - 秘密鍵を持つファイルを作成したユーザと公開鍵を持つ任意のユーザが相互にエンコードとデコードが行える仕組み - 署名はファイルにメタデータとして保持できるようにする - 鍵の管理もOSが担うようにしたい ## OSの信頼性について - アプリケーションを動かすOSには高い信頼性が保証されるべきである - OSの処理やコードの量は膨大になる - テストコードを用いた信頼性の保証は困難であると言える - 数学的な背景に基づいた形式手法を用いて検証したい - 定理支援証明 - モデル検査 - OSを形式手法にて証明するには状態遷移単位での記述が求められる - GearsOSはメタレベルとノーマルレベルの計算を分離して記述が行える構成である - メタレベルの計算でプログラムの整合性を検証する ## Continuation based C(CbC) - CbCとはC言語の下位言語である - CbCは関数呼び出しでなくjmp命令で移動する継続を導入している - jmp命令でコード間を移動することにより軽量な継続を実現している - CbCでは継続を用いてfor 文などのループ文を実装する - Gearというプログラム概念を持つ - CbCでは関数の代わりにCodeGearという単位でプログラムを行う - CodeGearによる記述は形式手法に必要な状態遷移そのものとして見ることができる。 ## Gearsの概念 - CodeGear:従来のプログラムやスレッド - DataGear:変数データ - CodeGearはDataGearと呼ばれる変数データを入力として受け取る - CodeGearの処理結果を別のDataGear に書き込む - 入力のDataGearをInputDataGear - 出力されるDataGearをOutputDataGear - CodeGearが参照できるDataGearはInput/output DataGearに限定される。 - CodeGearは関数呼び出しのスタックを持たない - 一度コードブロックを遷移すると元の処理に戻ってこられない