view finalSlide/finalSlide.md @ 34:181eec546ad2

tweak slide
author ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
date Sat, 12 Feb 2022 23:16:05 +0900 (2022-02-12)
parents ab77a291294d
children 668692d92e6e
line wrap: on
line source
title: GearsOSの分散ファイルシステムの設計
author: Takahiro Ikki, Shinji Kono
profile: 琉球大学理工学研究科情報工学専攻
lang: Japanese
code-engine: coderay

## 概要
- 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となる
<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>


## 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を用いたファイル通信の構成解説
- 研究のまとめと課題