title: GearsOSの分散ファイルシステムの設計 author: Takahiro Ikki, Shinji Kono profile: 琉球大学理工学研究科情報工学専攻 lang: Japanese code-engine: coderay ## 継続を導入したGearsOS - 継続を導入した、信頼性の保証を目指したOS開発プロジェクトである - 関数遷移を用いず、**CodeGear**と**DataGear**と言う単位で記述を行う - 複数のCodeGearをgoto(jump命令)で遷移することで処理が実行される - OS自体の検証はプログラムが膨大な量となるため、テストコードを用いるのは難しい - GearsOSではメタレベルの処理からユーザープログラムの検証をする構成となる - GearsOSはノーマルレベルとメタレベルを分けて記述できる - メタレベルな処理を検証用のものに切り替えることで検証を行う - 信頼性の検証には定理支援証明系やモデル検査を用いる ## GearsOSのファイルシステム開発 - GearsOSファイルシステムの開発にあたり要件定義を行った - ファイルシステムも同様にGear単位で操作を行う - 従来ではアプリケーションが持つ機能の一部を取り入れたい - Transaction - データ操作の整合性保護が施された処理 - バックアップ - 分散フレームワークChristieの仕組みを用いたい ## 分散フレームワークChristie - 当研究室が開発する、Javaで書かれた分散フレームワークである - GearsOSと似たGearと言うプログラミング概念を持つ - ノード間の通信はDataGearの送り合いで構成される - Threadは任意のDataGearが揃ったら実行される - 通信されるデータを意識しながら分散処理の記述が行える - これらの構成は自律分散を目指した設計となっている ## Christie likeな通信の分散ファイルシステムの提案 - Christieの仕組みを用いた分散ファイルシステムを設計/検証したい - ファイルデータとなるDataGearを追いながらプロセスが記述できる - データのみの送受信による通信でネットワークの見通しを確保する - 自律分散なファイルシステムを目指す - APIやプロセスの正当性は将来的に定理支援証明系agdaで検証される ## GearsOSが持つOSレベルなTransactionの実装検証 - GearsOSはAPIレベルでTransactionな記述が行える - 従来のアプリケーションでは、ユーザーレベルで実装される - API自体のTransactionが保証されていれば、アプリケーションの信頼性保証が容易になる - GearsOSのAPIレベルで実装されるTransactionの実装と検証を行う ## ポスター発表 - GearsOSのChristie likeなファイルシステムの設計と実装 - ファイル構造 - QueueとTreeを用いる - ファイルAPI - Put/Take/Peek - 複数streamを用いたファイル通信 - WordCount例題 - まとめと課題 ## この先保留 ## CodeGearとDataGear - CodeGear - 実行Codeの単位 - 入力/出力のDataGearを持つ - goto文(jump命令)で遷移する - 割り込みが行われない(atomicity) - DataGear - 変数にあたり、構造体の型を持つ ## CodeGearとDataGearの関係 - InputDataGearを受け取って、CodeGearが処理し、OutputDataGearを出力する - OutputDataGearは次のCodeGearのInputDataGearとなる - CodeGear/DataGearはContextというオブジェクトで管理される