GearsOSの分散ファイルシステムの設計
Takahiro Ikki, Shinji Kono 琉球大学理工学研究科情報工学専攻
継続を導入したGearsOS
OSの信頼性の保証と拡張性を目指したOS開発プロジェクトである
アプリケーションの土台となるOSはより高い信頼性が保証されるべきである
OS自体の信頼性検証はプログラムが膨大な量となるため、テストコードによるデバッグは難しい
GearsOSではメタレベルの処理からユーザープログラムの検証を行うアプローチをとる
ノーマルレベルとメタレベルを分けて記述できる
メタレベルな処理を検証用のものに切り替えることで信頼性の検証を行う
信頼性の検証には定理支援証明系やモデル検査を用いる
関数遷移に代わり、
CodeGear
と
DataGear
と言う単位で記述を行う
複数のCodeGearをgoto(jump命令)で遷移することで処理が実行される
研究目的
GearsOSにより信頼性が裏付けられる、分散ファイルシステムの開発/検証を行う
GearsOSの処理単位であるDataGearでファイルを構成したい
将来的にAPIやプロセスは定理支援証明系により整合性の検証が行われる
OSレベルでTransactionを持つ
Transactionとはデータ操作の不可分化による整合性の保護
従来のアプリでは、ユーザーレベルで実装される
GearsOSが持つTransactionの実用性の検証
研究目的
分散フレームワークChristieの仕組みを用いた分散ファイルシステムの設計/開発
純粋なデータの送り合いだけで構成されるシンプルな通信
自律分散ファイルシステムを目指したい
ネットワーク通信上で複数のプロトコルが送られることによる煩雑性を防ぐ
通信のデータの整合性の保護はGearsOSが行う
分散フレームワークChristie
当研究室が開発する、Javaで書かれた分散フレームワークである
GearsOSと似たGearと言うプログラミング概念を持つ
ノード間の通信は、Threadの実行に必要になる変数データ(DataGear)の送り合いで構成される
DataGearが揃ったThreadはノードにより実行される
ノードはDataGearを保存するkey value storeである,DataGearManagerを持つ
DataGearManagerにはLocalなものとRemoteのものが存在する
GearsFSはDataGearManagerの仕組みを導入することで通信する
ポスター発表
GearsOSとChristieの解説
DataGearManagerの仕組み
Chlistie likeなファイルシステムの設計の解説
ファイルとファイルデータの構造の設計
API
ファイルによる通信の設計と実装
GearsFSの例題による通信モデル
まとめと課題
ポスター発表
GearsOSのChristie likeなファイルシステムの設計と実装
ファイル構造
QueueとTreeを用いる
ファイルAPI
Put/Take/Peek
複数streamを用いたファイル通信
WordCount例題
まとめと課題
