GearsOSの分散ファイルシステムの設計
Takahiro Ikki, Shinji Kono 琉球大学理工学研究科情報工学専攻
概要
GearsOSの分散ファイルシステムの設計と実装を行った
ファイル構造の設計
APIの定義
遠隔のファイルのアクセスと保存
GearsOS同様の記述単位な構成
自律分散を目指した分散ファイルシステムの設計
OSレベルのTransactionによるアプリ実装
GearsOS
CodeGear/DataGearという単位で記述されるOS
OSの信頼性の保証と拡張性を目指している
ノーマルレベルとメタレベルを分離して記述できる
ユーザーが実装したプログラムをメタレベルから検証する
定理支援証明系やモデル検査が用いられる
CodeGearとDataGear
CodeGear
実行Codeの単位
入力DataGearと出力DataGearを持つ
goto文(jump命令)を使って遷移する
実行単位は途中で割り込みされない(Atmocity)
DataGear
変数にあたり、構造体の型を持つ
ノーマルレベルでは変更されない(関数型プログラミング)
C言語を拡張する形でCbC言語により実装される
CodeGearとDataGear
InputDataGearを受け取って、CodeGearが処理し、OutputDataGearを出力する
OutputDataGearは次のCodeGearのInputDataGearとなる
GearsOSにおけるファイル
ファイルデータの最小単位はDataGearとなる
任意の構造体で構成できる
ファイルデータとなるDataGearはQueueに格納される
GearsOSにおけるファイル
ファイルは複数のQueueを持つ赤黒木である
Queueはkeyでアクセスされる
Queueはstreamの役割を持つ
GearsOSの分散ファイルシステム
GearsOSのファイルは通信の役割も持つ
規格が決められたプロトコルを用いない
最低限のデータ(DataGear)でのみ通信を行う
分散通信の見通しの確保を目指す
将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う
Transactionalなファイルシステム
GearsFSはDataGear単位で操作を行う
これによりAPIをTransactionとして実装できる
従来ではアプリケーションレベルで実装される
Transactionは様々な分類のアプリケーションに必要となる
GearsOSによるOSレベルのTransactionを用いた開発物の検証を兼ねる
ポスターセッション
ファイル構造の詳細
ファイルアクセスAPI
proxyを用いたファイル通信の構成解説
研究のまとめと課題
