GearsOSの分散ファイルシステムの設計
Takahiro Ikki, Shinji Kono 琉球大学理工学研究科情報工学専攻
概要
GearsOSの分散ファイルシステムの設計と実装を行った
ファイル構造の設計
APIの定義
遠隔のファイルのアクセスと保存
GearsOS同様の記述単位による構成
ファイルは複数のstreamを持ち、通信も行う
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の役割を持つ
FileAPI
ファイルのAPIは三種類となる
Put
Queueに対してデータを挿入する
Take
Queueからデータを取り出す
Peek
Queueからデータを”読み”だす
Takeの先読みに相当する
APIは対象のstreamをkeyで指定する
GearsOSの分散ファイルシステム
GearsOSのファイルは通信の役割も持つ
遠隔上のファイルに対応するproxyを作成して通信を行う
対象ファイルとproxyはsocketで接続される
proxyの操作はLocalなファイルと相違なく行える
記録デバイスへの保存も同様な仕組みで行う
将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う
GearsFSの展望
ノードの配線を担当するTopologyManagerの実装
参加表明したノードを任意の形のTopologyへ配線する
複数streamにより制御を行う分散ファイル通信手法としての検証
Dataのみで通信を行う通信(規格があるプロトコルを用いない)
自律分散通信の見通し確保
OSレベルなTransactionを搭載するアプリケーションとしての評価
GearsOSのCodeGearはTransactionとなる
従来ではアプリケーションレベルにより実装される
GearsOSによるOSレベルTransactionの信頼性/実用性調査
ポスターセッション
より詳細なGearsOSのファイル構造
ファイルの読み出し
proxyを用いたファイル通信の構成解説
研究のまとめと課題
