Mercurial > hg > Papers > 2022 > ikki-master
diff finalSlide/finalSlide.md @ 41:3959e0817369
tweak slide
author | ichikitakahiro <e165713@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 17 Feb 2022 23:24:09 +0900 |
parents | cb0c76ff9de1 |
children | 01b88c0dd337 |
line wrap: on
line diff
--- a/finalSlide/finalSlide.md Thu Feb 17 00:51:16 2022 +0900 +++ b/finalSlide/finalSlide.md Thu Feb 17 23:24:09 2022 +0900 @@ -5,47 +5,53 @@ code-engine: coderay +## 継続を導入したGearsOS +- OSの信頼性の保証と拡張性を目指したOS開発プロジェクトである + - アプリケーションの土台となるOSはより高い信頼性が保証されるべきである +- OS自体の信頼性検証はプログラムが膨大な量となるため、テストコードによるデバッグは難しい +- GearsOSではメタレベルの処理からユーザープログラムの検証を行うアプローチをとる + - ノーマルレベルとメタレベルを分けて記述できる + - メタレベルな処理を検証用のものに切り替えることで信頼性の検証を行う + - 信頼性の検証には定理支援証明系やモデル検査を用いる +- 関数遷移に代わり、**CodeGear**と**DataGear**と言う単位で記述を行う + - 複数のCodeGearをgoto(jump命令)で遷移することで処理が実行される -## 継続を導入したGearsOS -- 継続を導入した、信頼性の保証を目指したOS開発プロジェクトである -- 関数遷移を用いず、**CodeGear**と**DataGear**と言う単位で記述を行う - - 複数のCodeGearをgoto(jump命令)で遷移することで処理が実行される -- OS自体の検証はプログラムが膨大な量となるため、テストコードを用いるのは難しい -- GearsOSではメタレベルの処理からユーザープログラムの検証をする構成となる - - GearsOSはノーマルレベルとメタレベルを分けて記述できる - - メタレベルな処理を検証用のものに切り替えることで検証を行う - - 信頼性の検証には定理支援証明系やモデル検査を用いる -## GearsOSのファイルシステム開発 -- GearsOSファイルシステムの開発にあたり要件定義を行った -- ファイルシステムも同様にGear単位で操作を行う -- 従来ではアプリケーションが持つ機能の一部を取り入れたい - - Transaction - - バックアップ -- 分散フレームワークChristieの仕組みを用いたい +## 研究目的 +- GearsOSにより信頼性が裏付けられる、分散ファイルシステムの開発/検証を行いたい +- 開発物はGearsOSによるAPIレベルなTransactionが実装される + - Transactionとはデータ操作の不可分化による整合性の保護 + - 従来のアプリでは、ユーザーレベルで実装される +- GearsOSが持つTransactionの実用性の検証 +- 将来的にAPIやプロセスは定理支援証明系により整合性の検証が行われる + +## 研究目的 +- 分散フレームワークChristieの仕組みを用いた分散ファイルシステムの提案 + - 純粋なデータの送り合いだけで構成されるシンプルな通信 + - 自律分散ファイルシステムを目指したい + - ネットワーク上で複数のプロトコルが使われることによる煩雑性を防ぐ +- GearsOSの処理単位であるDataGearでファイルを構成できる ## 分散フレームワークChristie - 当研究室が開発する、Javaで書かれた分散フレームワークである - GearsOSと似たGearと言うプログラミング概念を持つ -- ノード間の通信はDataGearの送り合いで構成される - - Threadは任意のDataGearが揃ったら実行される -- 通信されるデータを意識しながら分散処理の記述が行える -- これらの構成は自律分散を目指した設計となっている +- ノード間の通信は、Threadの実行に必要になる変数データ(DataGear)の送り合いで構成される + - DataGearが揃ったThreadはノードにより実行される +- ノードはDataGearを保存するkey value storeである,DataGearManagerを持つ + - DataGearManagerにはLocalなものとRemoteのものが存在する +- GearsFSはDataGearManagerの仕組みを導入することで通信する -## Christie likeな通信の分散ファイルシステムの提案 -- Christieの仕組みを用いた分散ファイルシステムを設計/検証したい - - データのみの送受信により通信が構成される - - 分散ネットワーク全体の見通しの確保がのぞめる - - 自律分散なファイルシステムを目指したい -- APIやプロセスの正当性は将来的に定理支援証明系agdaで検証される +## スライド発表 +- GearsOSとChristieの解説 + - DataGearManagerの仕組み +- Chlistie likeなファイルシステムの設計の解説 + - ファイルとファイルデータの構造の設計 + - API + - ファイルによる通信の設計と実装 + - GearsFSの例題による通信モデル +- まとめと課題 -## GearsOSが持つOSレベルなTransactionを用いた実装 -- GearsOSはAPIレベルでTransactionな記述が行える - - Transactionとはデータ操作の不可分化による整合性の保護 - - 従来のアプリケーションでは、ユーザーレベルで実装される - - アプリケーションの土台となるOSが信頼性を保証したい -- APIにTransactionが実装されたアプリケーションの開発/検証 ## ポスター発表