title: GearsOSの分散ファイルシステムの設計
author: Takahiro Ikki, Shinji Kono
profile: 琉球大学理工学研究科情報工学専攻
lang: Japanese
code-engine: coderay


## 継続を導入したGearsOS
- OSの信頼性の保証と拡張性を目指したOS開発プロジェクトである
  - アプリケーションの土台となるOSはより高い信頼性が保証されるべきである
- OS自体の信頼性検証はプログラムが膨大な量となるため、テストコードによるデバッグは難しい
- GearsOSではメタレベルの処理からユーザープログラムの検証を行うアプローチをとる
  - ノーマルレベルとメタレベルを分けて記述できる
  - メタレベルな処理を検証用のものに切り替えることで信頼性の検証を行う
  - 信頼性の検証には定理支援証明系やモデル検査を用いる
- 関数遷移に代わり、**CodeGear**と**DataGear**と言う単位で記述を行う
  - 複数のCodeGearをgoto(jump命令)で遷移することで処理が実行される


## 研究目的
- GearsOSにより信頼性が裏付けられる、分散ファイルシステムの開発/検証を行いたい
- 開発物はGearsOSによるAPIレベルなTransactionが実装される
  - Transactionとはデータ操作の不可分化による整合性の保護
  - 従来のアプリでは、ユーザーレベルで実装される
- GearsOSが持つTransactionの実用性の検証
- 将来的にAPIやプロセスは定理支援証明系により整合性の検証が行われる

## 研究目的
- 分散フレームワークChristieの仕組みを用いた分散ファイルシステムの提案
  - 純粋なデータの送り合いだけで構成されるシンプルな通信
  - 自律分散ファイルシステムを目指したい
    - ネットワーク上で複数のプロトコルが使われることによる煩雑性を防ぐ
- GearsOSの処理単位であるDataGearでファイルを構成できる

## 分散フレームワーク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例題
- まとめと課題

## この先保留

## CodeGearとDataGear
- CodeGear
  - 実行Codeの単位
  - 入力/出力のDataGearを持つ
  - goto文(jump命令)で遷移する
  - 割り込みが行われない(atomicity)
- DataGear
  - 変数にあたり、構造体の型を持つ

## CodeGearとDataGearの関係
- InputDataGearを受け取って、CodeGearが処理し、OutputDataGearを出力する
- OutputDataGearは次のCodeGearのInputDataGearとなる
- CodeGear/DataGearはContextというオブジェクトで管理される
<div style="text-align: center;">
  　<img src="images/cg-dg.pdf" alt=cgdgの関係図 width="600">
</div>

## 研究概要
- GearsOSの分散ファイルシステムの設計・実装を行った
  - ファイル構造の設計
  - ファイルAPIの設計
  - 複数streamを用いたファイル通信とデバイス保存
- 最低限のデータを送信することにより通信が行える
- 分散フレームワークChristieの仕組みを利用している



## 本研究の目的
- 分散フレームワークChristieのファイルシステムへの応用
  - プロトコルを用いず、最低限のデータの送受信で通信を構成する
  - 複雑な分散通信の見通しの改善
  - 自律分散通信を目指した設計
- OSレベルなTransactionによるファイル通信記述の検証
  - GearsOSではAPIをTransactionとして構成できる
  - 従来のファイルシステムはアプリケーションレベルで実装される

## GearsOS
- OSの信頼性の向上と拡張性を目指している
- CodeGear/DataGearという単位で記述される
- ノーマルレベルとメタレベルを分離して記述できる
  - メタレベル処理を切り替えることで、信頼性検証やデバッグを行う
  - 将来的に本研究の成果物も信頼性の検証を行う

## CodeGearとDataGear
- CodeGear
  - 実行Codeの単位
  - 入力/出力のDataGearを持つ
  - goto文(jump命令)で遷移する
- DataGear
  - 変数にあたり、構造体の型を持つ

## CodeGearとDataGearの関係
- InputDataGearを受け取って、CodeGearが処理し、OutputDataGearを出力する
- OutputDataGearは次のCodeGearのInputDataGearとなる
- CodeGear/DataGearはContextというオブジェクトで管理される
<div style="text-align: center;">
  　<img src="images/cg-dg.pdf" alt=cgdgの関係図 width="600">
</div>


## 分散フレームワークChristie
- Javaで記述された分散フレームワーク
- GearsOSと似たGearという概念を持つ
- CodeGearManagerと言うノードがCodeGear/DataGearを管理する
  - DataGearはDataGearManagerと言うデータプールに記録される
- DataGearをノード間で送り合うことで通信を行う

## Christieの通信
- LocalDGM
  - そのノードに対応するデータプール
  - CodeGearはLocalDGMからDataGearを参照する
- RemoteDGM
  - 他のノードのLocalDGMに対応するproxy
  - RemoteDGMに書き込むと対応したLocalDGMに送信される
- DataGearManagerの仕組みをGearsOSのファイルに利用する

## RemoteDGMによる通信
- 任意の相手のRemoteDGMを作成することで接続が形成される
- RemoteDGMに書き込むと相手のLocalDGMに書き込みが行われる
<div style="text-align: center;">
　<img src="images/Remote_DataGearManager.pdf" alt="RemoteDGMの関係図" width="550">
</div>


## ポスター発表概要
- Christieの仕組みを用いたファイルシステム設計/実装の解説
  - QueueとTreeを用いたファイル構造
  - ファイルAPI
    - Put/Take/Peek
  - 複数socketを用いたファイル通信の構成
  - WordCount例題
- まとめと課題




## まとめ
- GearsOSの通信を含めたファイルシステムの設計・開発を行った
  - DataGear単位によるファイル操作
  - 複数のstreamを用いた通信の設計
    - 現時点では単一streamによる通信のみ開発済み
- 課題
    - WordCount例題の再現
    - API/プロセスの信頼性や性能の調査

## GearsOSのファイルシステム
- ファイルデータの最小単位はDataGearとなる
- ファイルデータとなるDataGearはQueueに格納される
- APIはPut/Take/Peekの三つで操作する
<div style="text-align: center;">
  　<img src="images/QueueElement.pdf" alt=Queue width="800">
</div>

## GearsOSにおけるファイル
- ファイルは複数のQueueを持つ赤黒木である
- Queueはkeyでアクセスされる
- Queueはstreamの役割を持つ

<div style="text-align: center;">
  　<img src="images/newGearsFile.pdf" alt=Queue width="400">
</div>

## ファイルによる通信の構成
- GearsOSのファイルは通信も担当する
- 通信先のファイルのproxyを生成し通信する
- proxyに対してデータを書き込むことで通信が行われる
- WordCount例題を通して設計を行った  
<div style="text-align: center;">
  <img src="images/slideGearsWC.pdf" alt=Queue width="500">
</div>

## GearsOSの分散ファイルシステム
- GearsOSのファイルは通信の役割も持つ
- 遠隔上のファイルに対応するproxyを作成して通信を行う
  - 対象ファイルとproxyはsocketで接続される
  - proxyの操作はLocalなファイルと相違なく行える
- 記録デバイスへの保存も同様な仕組みで行う

## GearsFSの展望
- ノードの配線を担当するTopologyManagerの実装
  - 参加表明したノードを任意の形のTopologyへ配線する
- 将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う
- 複数streamにより制御を行う分散ファイル通信の検証
- GearsOSによるOSレベルTransactionの信頼性/実用性調査
  - 従来ではアプリケーションレベルにより実装される