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

## 概要
- 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となる
<div style="text-align: center;">
  　<img src="images/cg-dg.pdf" alt=cgdgの関係図 width="600">
</div>


## GearsOSにおけるファイル
- ファイルデータの最小単位はDataGearとなる
  - 任意の構造体で構成できる
- ファイルデータとなるDataGearはQueueに格納される
<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の分散ファイルシステム
- GearsOSのファイルは通信の役割も持つ
- 規格が決められたプロトコルを用いない
  - 最低限のデータ(DataGear)でのみ通信を行う
  - 分散通信の見通しの確保を目指す
- 将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う

## Transactionalなファイルシステム
- GearsFSはDataGear単位で操作を行う
- これによりAPIをTransactionとして実装できる
  - 従来ではアプリケーションレベルで実装される
- Transactionは様々な分類のアプリケーションに必要となる
- GearsOSによるOSレベルのTransactionを用いた開発物の検証を兼ねる

## ポスターセッション
- ファイル構造の詳細
- ファイルアクセスAPI
- proxyを用いたファイル通信の構成解説
- 研究のまとめと課題