Mercurial > hg > Papers > 2022 > ikki-master
changeset 35:668692d92e6e
rewrite slide
author | ichikitakahiro <e165713@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 13 Feb 2022 23:04:26 +0900 |
parents | 181eec546ad2 |
children | f636dbf689e1 |
files | finalSlide/finalSlide.html finalSlide/finalSlide.md finalSlide/finalSlide.pdf.html |
diffstat | 3 files changed, 800 insertions(+), 193 deletions(-) [+] |
line wrap: on
line diff
--- a/finalSlide/finalSlide.html Sat Feb 12 23:16:05 2022 +0900 +++ b/finalSlide/finalSlide.html Sun Feb 13 23:04:26 2022 +0900 @@ -91,17 +91,50 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="概要">概要</h2> +<h2 id="継続を導入したgearsos">継続を導入したGearsOS</h2> <ul> - <li>GearsOSの分散ファイルシステムの設計と実装を行った + <li>GearsOSは関数遷移でなく、継続を導入したOS開発プロジェクトである</li> + <li>関数遷移でなく、<strong>CodeGear</strong>と言う単位で記述する <ul> - <li>ファイル構造の設計</li> - <li>APIの定義</li> - <li>遠隔のファイルのアクセスと保存</li> + <li>各CodeGearをjump命令で推移することで処理が実行される</li> + </ul> + </li> + <li>OSの信頼性の向上を目指して開発されている + <ul> + <li>OSのプログラムは膨大なため検証が困難である</li> + </ul> + </li> + <li>GearsOSはノーマルレベルとメタレベルの処理を分けて記述できる + <ul> + <li>メタレベルな処理を実行用や検証用なものに切り替えるができる</li> + <li>これによりユーザープログラムの検証を行う</li> + <li>検証は定理支援証明系やモデル検査を用いる</li> </ul> </li> - <li>GearsOS同様の記述単位による構成</li> - <li>ファイルは複数のstreamを持ち、通信も行う</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="gearsosのファイルシステム開発">GearsOSのファイルシステム開発</h2> +<ul> + <li>GearsOSは現段階で言語フレームワークとして実装されている</li> + <li>GearsOSの分散ファイルシステムを開発したい + <ul> + <li>ファイルシステムも同様にGear単位で操作したい</li> + <li>煩雑な分散処理を簡潔に構成したい</li> + <li>従来ではアプリケーションが持つ機能の一部を取り入れたい + <ul> + <li>Transaction</li> + <li>バックアップ</li> + </ul> + </li> + </ul> + </li> + <li>分散フレームワークChrisiteの仕組みを用いることで</li> </ul> @@ -110,16 +143,35 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="gearsos">GearsOS</h2> +<h2 id="分散フレームワークchristie">分散フレームワークChristie</h2> <ul> - <li>CodeGear/DataGearという単位で記述されるOS</li> - <li>OSの信頼性の保証と拡張性を目指している</li> - <li>ノーマルレベルとメタレベルを分離して記述できる + <li>Javaで書かれた分散フレームワークである <ul> - <li>ユーザーが実装したプログラムをメタレベルから検証する</li> - <li>定理支援証明系やモデル検査が用いられる</li> + <li>GearsOSと近い, Gearと言うプログラミング概念を持つ</li> + <li>自立分散を目指した設計となっている</li> + <li>規格が決められたプロトコルを持たず、データのみの送信で通信する</li> + </ul> + </li> + <li>通信されるデータを意識しながら分散処理の記述が行える</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="christieを用いたファイルシステム開発">Christieを用いたファイルシステム開発</h2> +<ul> + <li>Christieの通信構成をファイルシステムへの適用を行う</li> + <li>ファイルは複数のstreamで構成され、データの通信も行う + <ul> + <li>これによりファイルのデータ操作をDataGearの単位で行える</li> </ul> </li> + <li>CodeGear単位の記述によりAPIはTransactionで提供される</li> + <li>将来的に定理支援証明系agdaで信頼性検証を行う</li> + <li>Christie baseなファイル通信の評価を行いたい</li> </ul> @@ -128,23 +180,56 @@ <div class='slide'> <!-- _S9SLIDE_ --> +<h2 id="ポスター発表">ポスター発表</h2> +<ul> + <li>GearsOSのファイルシステムの設計と実装 + <ul> + <li>ファイル構造 + <ul> + <li>QueueとTreeを用いる</li> + </ul> + </li> + <li>ファイルAPI + <ul> + <li>Put/Take/Peek</li> + </ul> + </li> + <li>複数streamを用いたファイル通信</li> + <li>WordCount例題</li> + </ul> + </li> + <li>まとめと課題</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="この先保留">この先保留</h2> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> <h2 id="codegearとdatagear">CodeGearとDataGear</h2> <ul> <li>CodeGear <ul> <li>実行Codeの単位</li> - <li>入力DataGearと出力DataGearを持つ</li> - <li>goto文(jump命令)を使って遷移する</li> - <li>実行単位は途中で割り込みされない(Atmocity)</li> + <li>入力/出力のDataGearを持つ</li> + <li>goto文(jump命令)で遷移する</li> + <li>割り込みが行われない(atomicity)</li> </ul> </li> <li>DataGear <ul> <li>変数にあたり、構造体の型を持つ</li> - <li>ノーマルレベルでは変更されない(関数型プログラミング)</li> </ul> </li> - <li>C言語を拡張する形でCbC言語により実装される</li> </ul> @@ -153,10 +238,11 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="codegearとdatagear-1">CodeGearとDataGear</h2> +<h2 id="codegearとdatagearの関係">CodeGearとDataGearの関係</h2> <ul> <li>InputDataGearを受け取って、CodeGearが処理し、OutputDataGearを出力する</li> <li>OutputDataGearは次のCodeGearのInputDataGearとなる</li> + <li>CodeGear/DataGearはContextというオブジェクトで管理される</li> </ul> <div style="text-align: center;"> <img src="images/cg-dg.pdf" alt="cgdgの関係図" width="600" /> @@ -168,14 +254,214 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="gearsosにおけるファイル">GearsOSにおけるファイル</h2> +<h2 id="研究概要">研究概要</h2> +<ul> + <li>GearsOSの分散ファイルシステムの設計・実装を行った + <ul> + <li>ファイル構造の設計</li> + <li>ファイルAPIの設計</li> + <li>複数streamを用いたファイル通信とデバイス保存</li> + </ul> + </li> + <li>最低限のデータを送信することにより通信が行える</li> + <li>分散フレームワークChristieの仕組みを利用している</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="本研究の目的">本研究の目的</h2> <ul> - <li>ファイルデータの最小単位はDataGearとなる + <li>分散フレームワークChristieのファイルシステムへの応用 + <ul> + <li>プロトコルを用いず、最低限のデータの送受信で通信を構成する</li> + <li>複雑な分散通信の見通しの改善</li> + <li>自律分散通信を目指した設計</li> + </ul> + </li> + <li>OSレベルなTransactionによるファイル通信記述の検証 <ul> - <li>任意の構造体で構成できる</li> + <li>GearsOSではAPIをTransactionとして構成できる</li> + <li>従来のファイルシステムはアプリケーションレベルで実装される</li> + </ul> + </li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="gearsos">GearsOS</h2> +<ul> + <li>OSの信頼性の向上と拡張性を目指している</li> + <li>CodeGear/DataGearという単位で記述される</li> + <li>ノーマルレベルとメタレベルを分離して記述できる + <ul> + <li>メタレベル処理を切り替えることで、信頼性検証やデバッグを行う</li> + <li>将来的に本研究の成果物も信頼性の検証を行う</li> + </ul> + </li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="codegearとdatagear-1">CodeGearとDataGear</h2> +<ul> + <li>CodeGear + <ul> + <li>実行Codeの単位</li> + <li>入力/出力のDataGearを持つ</li> + <li>goto文(jump命令)で遷移する</li> + </ul> + </li> + <li>DataGear + <ul> + <li>変数にあたり、構造体の型を持つ</li> </ul> </li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="codegearとdatagearの関係-1">CodeGearとDataGearの関係</h2> +<ul> + <li>InputDataGearを受け取って、CodeGearが処理し、OutputDataGearを出力する</li> + <li>OutputDataGearは次のCodeGearのInputDataGearとなる</li> + <li>CodeGear/DataGearはContextというオブジェクトで管理される</li> +</ul> +<div style="text-align: center;"> + <img src="images/cg-dg.pdf" alt="cgdgの関係図" width="600" /> +</div> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="分散フレームワークchristie-1">分散フレームワークChristie</h2> +<ul> + <li>Javaで記述された分散フレームワーク</li> + <li>GearsOSと似たGearという概念を持つ</li> + <li>CodeGearManagerと言うノードがCodeGear/DataGearを管理する + <ul> + <li>DataGearはDataGearManagerと言うデータプールに記録される</li> + </ul> + </li> + <li>DataGearをノード間で送り合うことで通信を行う</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="christieの通信">Christieの通信</h2> +<ul> + <li>LocalDGM + <ul> + <li>そのノードに対応するデータプール</li> + <li>CodeGearはLocalDGMからDataGearを参照する</li> + </ul> + </li> + <li>RemoteDGM + <ul> + <li>他のノードのLocalDGMに対応するproxy</li> + <li>RemoteDGMに書き込むと対応したLocalDGMに送信される</li> + </ul> + </li> + <li>DataGearManagerの仕組みをGearsOSのファイルに利用する</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="remotedgmによる通信">RemoteDGMによる通信</h2> +<ul> + <li>任意の相手のRemoteDGMを作成することで接続が形成される</li> + <li>RemoteDGMに書き込むと相手のLocalDGMに書き込みが行われる</li> +</ul> +<div style="text-align: center;"> + <img src="images/Remote_DataGearManager.pdf" alt="RemoteDGMの関係図" width="550" /> +</div> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="ポスター発表概要">ポスター発表概要</h2> +<ul> + <li>Christieの仕組みを用いたファイルシステム設計/実装の解説 + <ul> + <li>QueueとTreeを用いたファイル構造</li> + <li>ファイルAPI + <ul> + <li>Put/Take/Peek</li> + </ul> + </li> + <li>複数socketを用いたファイル通信の構成</li> + <li>WordCount例題</li> + </ul> + </li> + <li>まとめと課題</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="まとめ">まとめ</h2> +<ul> + <li>GearsOSの通信を含めたファイルシステムの設計・開発を行った + <ul> + <li>DataGear単位によるファイル操作</li> + <li>複数のstreamを用いた通信の設計 + <ul> + <li>現時点では単一streamによる通信のみ開発済み</li> + </ul> + </li> + </ul> + </li> + <li>課題 + <ul> + <li>WordCount例題の再現</li> + <li>API/プロセスの信頼性や性能の調査</li> + </ul> + </li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="gearsosのファイルシステム">GearsOSのファイルシステム</h2> +<ul> + <li>ファイルデータの最小単位はDataGearとなる</li> <li>ファイルデータとなるDataGearはQueueに格納される</li> + <li>APIはPut/Take/Peekの三つで操作する</li> </ul> <div style="text-align: center;"> <img src="images/QueueElement.pdf" alt="Queue" width="800" /> @@ -187,14 +473,11 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="gearsosにおけるファイル-1">GearsOSにおけるファイル</h2> +<h2 id="gearsosにおけるファイル">GearsOSにおけるファイル</h2> <ul> - <li>ファイルは複数のQueueを持つ赤黒木である - <ul> - <li>Queueはkeyでアクセスされる</li> - <li>Queueはstreamの役割を持つ</li> - </ul> - </li> + <li>ファイルは複数のQueueを持つ赤黒木である</li> + <li>Queueはkeyでアクセスされる</li> + <li>Queueはstreamの役割を持つ</li> </ul> <div style="text-align: center;"> @@ -207,27 +490,16 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="fileapi">FileAPI</h2> +<h2 id="ファイルによる通信の構成">ファイルによる通信の構成</h2> <ul> - <li>ファイルのAPIは三種類となる</li> - <li>Put - <ul> - <li>Queueに対してデータを挿入する</li> - </ul> - </li> - <li>Take - <ul> - <li>Queueからデータを取り出す</li> - </ul> - </li> - <li>Peek - <ul> - <li>Queueからデータを”読み”だす</li> - <li>Takeの先読みに相当する</li> - </ul> - </li> - <li>APIは対象のstreamをkeyで指定する</li> + <li>GearsOSのファイルは通信も担当する</li> + <li>通信先のファイルのproxyを生成し通信する</li> + <li>proxyに対してデータを書き込むことで通信が行われる</li> + <li>WordCount例題を通して設計を行った</li> </ul> +<div style="text-align: center;"> + <img src="images/slideGearsWC.pdf" alt="Queue" width="500" /> +</div> @@ -245,7 +517,6 @@ </ul> </li> <li>記録デバイスへの保存も同様な仕組みで行う</li> - <li>将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う</li> </ul> @@ -261,35 +532,15 @@ <li>参加表明したノードを任意の形のTopologyへ配線する</li> </ul> </li> - <li>複数streamにより制御を行う分散ファイル通信手法としての検証 + <li>将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う</li> + <li>複数streamにより制御を行う分散ファイル通信の検証</li> + <li>GearsOSによるOSレベルTransactionの信頼性/実用性調査 <ul> - <li>Dataのみで通信を行う通信(規格があるプロトコルを用いない)</li> - <li>自律分散通信の見通し確保</li> - </ul> - </li> - <li>OSレベルなTransactionを搭載するアプリケーションとしての評価 - <ul> - <li>GearsOSのCodeGearはTransactionとなる</li> <li>従来ではアプリケーションレベルにより実装される</li> - <li>GearsOSによるOSレベルTransactionの信頼性/実用性調査</li> </ul> </li> </ul> - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="ポスターセッション">ポスターセッション</h2> -<ul> - <li>より詳細なGearsOSのファイル構造</li> - <li>ファイルの読み出し</li> - <li>proxyを用いたファイル通信の構成解説</li> - <li>研究のまとめと課題</li> -</ul> - </div>
--- a/finalSlide/finalSlide.md Sat Feb 12 23:16:05 2022 +0900 +++ b/finalSlide/finalSlide.md Sun Feb 13 23:04:26 2022 +0900 @@ -4,72 +4,188 @@ lang: Japanese code-engine: coderay -## 概要 -- GearsOSの分散ファイルシステムの設計と実装を行った - - ファイル構造の設計 - - APIの定義 - - 遠隔のファイルのアクセスと保存 -- GearsOS同様の記述単位による構成 -- ファイルは複数のstreamを持ち、通信も行う -## GearsOS -- CodeGear/DataGearという単位で記述されるOS -- OSの信頼性の保証と拡張性を目指している -- ノーマルレベルとメタレベルを分離して記述できる - - ユーザーが実装したプログラムをメタレベルから検証する - - 定理支援証明系やモデル検査が用いられる +## 継続を導入したGearsOS +- GearsOSは関数遷移でなく、継続を導入したOS開発プロジェクトである +- 関数遷移でなく、**CodeGear**と言う単位で記述する + - 各CodeGearをjump命令で推移することで処理が実行される +- OSの信頼性の向上を目指して開発されている + - OSのプログラムは膨大なため検証が困難である +- GearsOSはノーマルレベルとメタレベルの処理を分けて記述できる + - メタレベルな処理を実行用や検証用なものに切り替えるができる + - これによりユーザープログラムの検証を行う + - 検証は定理支援証明系やモデル検査を用いる + +## GearsOSのファイルシステム開発 +- GearsOSは現段階で言語フレームワークとして実装されている +- GearsOSの分散ファイルシステムを開発したい + - ファイルシステムも同様にGear単位で操作したい + - 煩雑な分散処理を簡潔に構成したい + - 従来ではアプリケーションが持つ機能の一部を取り入れたい + - Transaction + - バックアップ +- 分散フレームワークChrisiteの仕組みを用いることで +## 分散フレームワークChristie +- Javaで書かれた分散フレームワークである + - GearsOSと近い, Gearと言うプログラミング概念を持つ + - 自立分散を目指した設計となっている + - 規格が決められたプロトコルを持たず、データのみの送信で通信する +- 通信されるデータを意識しながら分散処理の記述が行える + + +## Christieを用いたファイルシステム開発 +- Christieの通信構成をファイルシステムへの適用を行う +- ファイルは複数のstreamで構成され、データの通信も行う + - これによりファイルのデータ操作をDataGearの単位で行える +- CodeGear単位の記述によりAPIはTransactionで提供される +- 将来的に定理支援証明系agdaで信頼性検証を行う +- Christie baseなファイル通信の評価を行いたい + + +## ポスター発表 +- GearsOSのファイルシステムの設計と実装 + - ファイル構造 + - QueueとTreeを用いる + - ファイルAPI + - Put/Take/Peek + - 複数streamを用いたファイル通信 + - WordCount例題 +- まとめと課題 + +## この先保留 ## CodeGearとDataGear - CodeGear - 実行Codeの単位 - - 入力DataGearと出力DataGearを持つ - - goto文(jump命令)を使って遷移する - - 実行単位は途中で割り込みされない(Atmocity) + - 入力/出力のDataGearを持つ + - goto文(jump命令)で遷移する + - 割り込みが行われない(atomicity) - DataGear - 変数にあたり、構造体の型を持つ - - ノーマルレベルでは変更されない(関数型プログラミング) -- C言語を拡張する形でCbC言語により実装される + +## 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> -## GearsOSにおけるファイル +## 分散フレームワーク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の役割を持つ +- 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のファイルは通信も担当する +- 通信先のファイルのproxyを生成し通信する +- proxyに対してデータを書き込むことで通信が行われる +- WordCount例題を通して設計を行った +<div style="text-align: center;"> + <img src="images/slideGearsWC.pdf" alt=Queue width="500"> +</div> ## GearsOSの分散ファイルシステム - GearsOSのファイルは通信の役割も持つ @@ -77,22 +193,11 @@ - 対象ファイルとproxyはsocketで接続される - proxyの操作はLocalなファイルと相違なく行える - 記録デバイスへの保存も同様な仕組みで行う -- 将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う ## GearsFSの展望 - ノードの配線を担当するTopologyManagerの実装 - 参加表明したノードを任意の形のTopologyへ配線する -- 複数streamにより制御を行う分散ファイル通信手法としての検証 - - Dataのみで通信を行う通信(規格があるプロトコルを用いない) - - 自律分散通信の見通し確保 -- OSレベルなTransactionを搭載するアプリケーションとしての評価 - - GearsOSのCodeGearはTransactionとなる +- 将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う +- 複数streamにより制御を行う分散ファイル通信の検証 +- GearsOSによるOSレベルTransactionの信頼性/実用性調査 - 従来ではアプリケーションレベルにより実装される - - GearsOSによるOSレベルTransactionの信頼性/実用性調査 - - -## ポスターセッション -- より詳細なGearsOSのファイル構造 -- ファイルの読み出し -- proxyを用いたファイル通信の構成解説 -- 研究のまとめと課題
--- a/finalSlide/finalSlide.pdf.html Sat Feb 12 23:16:05 2022 +0900 +++ b/finalSlide/finalSlide.pdf.html Sun Feb 13 23:04:26 2022 +0900 @@ -75,17 +75,50 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="概要">概要</h2> +<h2 id="継続を導入したgearsos">継続を導入したGearsOS</h2> <ul> - <li>GearsOSの分散ファイルシステムの設計と実装を行った + <li>GearsOSは関数遷移でなく、継続を導入したOS開発プロジェクトである</li> + <li>関数遷移でなく、<strong>CodeGear</strong>と言う単位で記述する <ul> - <li>ファイル構造の設計</li> - <li>APIの定義</li> - <li>遠隔のファイルのアクセスと保存</li> + <li>各CodeGearをjump命令で推移することで処理が実行される</li> + </ul> + </li> + <li>OSの信頼性の向上を目指して開発されている + <ul> + <li>OSのプログラムは膨大なため検証が困難である</li> + </ul> + </li> + <li>GearsOSはノーマルレベルとメタレベルの処理を分けて記述できる + <ul> + <li>メタレベルな処理を実行用や検証用なものに切り替えるができる</li> + <li>これによりユーザープログラムの検証を行う</li> + <li>検証は定理支援証明系やモデル検査を用いる</li> </ul> </li> - <li>GearsOS同様の記述単位による構成</li> - <li>ファイルは複数のstreamを持ち、通信も行う</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="gearsosのファイルシステム開発">GearsOSのファイルシステム開発</h2> +<ul> + <li>GearsOSは現段階で言語フレームワークとして実装されている</li> + <li>GearsOSの分散ファイルシステムを開発したい + <ul> + <li>ファイルシステムも同様にGear単位で操作したい</li> + <li>煩雑な分散処理を簡潔に構成したい</li> + <li>従来ではアプリケーションが持つ機能の一部を取り入れたい + <ul> + <li>Transaction</li> + <li>バックアップ</li> + </ul> + </li> + </ul> + </li> + <li>分散フレームワークChrisiteの仕組みを用いることで</li> </ul> @@ -94,16 +127,35 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="gearsos">GearsOS</h2> +<h2 id="分散フレームワークchristie">分散フレームワークChristie</h2> <ul> - <li>CodeGear/DataGearという単位で記述されるOS</li> - <li>OSの信頼性の保証と拡張性を目指している</li> - <li>ノーマルレベルとメタレベルを分離して記述できる + <li>Javaで書かれた分散フレームワークである <ul> - <li>ユーザーが実装したプログラムをメタレベルから検証する</li> - <li>定理支援証明系やモデル検査が用いられる</li> + <li>GearsOSと近い, Gearと言うプログラミング概念を持つ</li> + <li>自立分散を目指した設計となっている</li> + <li>規格が決められたプロトコルを持たず、データのみの送信で通信する</li> + </ul> + </li> + <li>通信されるデータを意識しながら分散処理の記述が行える</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="christieを用いたファイルシステム開発">Christieを用いたファイルシステム開発</h2> +<ul> + <li>Christieの通信構成をファイルシステムへの適用を行う</li> + <li>ファイルは複数のstreamで構成され、データの通信も行う + <ul> + <li>これによりファイルのデータ操作をDataGearの単位で行える</li> </ul> </li> + <li>CodeGear単位の記述によりAPIはTransactionで提供される</li> + <li>将来的に定理支援証明系agdaで信頼性検証を行う</li> + <li>Christie baseなファイル通信の評価を行いたい</li> </ul> @@ -112,23 +164,56 @@ <div class='slide'> <!-- _S9SLIDE_ --> +<h2 id="ポスター発表">ポスター発表</h2> +<ul> + <li>GearsOSのファイルシステムの設計と実装 + <ul> + <li>ファイル構造 + <ul> + <li>QueueとTreeを用いる</li> + </ul> + </li> + <li>ファイルAPI + <ul> + <li>Put/Take/Peek</li> + </ul> + </li> + <li>複数streamを用いたファイル通信</li> + <li>WordCount例題</li> + </ul> + </li> + <li>まとめと課題</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="この先保留">この先保留</h2> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> <h2 id="codegearとdatagear">CodeGearとDataGear</h2> <ul> <li>CodeGear <ul> <li>実行Codeの単位</li> - <li>入力DataGearと出力DataGearを持つ</li> - <li>goto文(jump命令)を使って遷移する</li> - <li>実行単位は途中で割り込みされない(Atmocity)</li> + <li>入力/出力のDataGearを持つ</li> + <li>goto文(jump命令)で遷移する</li> + <li>割り込みが行われない(atomicity)</li> </ul> </li> <li>DataGear <ul> <li>変数にあたり、構造体の型を持つ</li> - <li>ノーマルレベルでは変更されない(関数型プログラミング)</li> </ul> </li> - <li>C言語を拡張する形でCbC言語により実装される</li> </ul> @@ -137,10 +222,11 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="codegearとdatagear-1">CodeGearとDataGear</h2> +<h2 id="codegearとdatagearの関係">CodeGearとDataGearの関係</h2> <ul> <li>InputDataGearを受け取って、CodeGearが処理し、OutputDataGearを出力する</li> <li>OutputDataGearは次のCodeGearのInputDataGearとなる</li> + <li>CodeGear/DataGearはContextというオブジェクトで管理される</li> </ul> <div style="text-align: center;"> <img src="images/cg-dg.pdf" alt="cgdgの関係図" width="600" /> @@ -152,14 +238,214 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="gearsosにおけるファイル">GearsOSにおけるファイル</h2> +<h2 id="研究概要">研究概要</h2> +<ul> + <li>GearsOSの分散ファイルシステムの設計・実装を行った + <ul> + <li>ファイル構造の設計</li> + <li>ファイルAPIの設計</li> + <li>複数streamを用いたファイル通信とデバイス保存</li> + </ul> + </li> + <li>最低限のデータを送信することにより通信が行える</li> + <li>分散フレームワークChristieの仕組みを利用している</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="本研究の目的">本研究の目的</h2> <ul> - <li>ファイルデータの最小単位はDataGearとなる + <li>分散フレームワークChristieのファイルシステムへの応用 + <ul> + <li>プロトコルを用いず、最低限のデータの送受信で通信を構成する</li> + <li>複雑な分散通信の見通しの改善</li> + <li>自律分散通信を目指した設計</li> + </ul> + </li> + <li>OSレベルなTransactionによるファイル通信記述の検証 <ul> - <li>任意の構造体で構成できる</li> + <li>GearsOSではAPIをTransactionとして構成できる</li> + <li>従来のファイルシステムはアプリケーションレベルで実装される</li> + </ul> + </li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="gearsos">GearsOS</h2> +<ul> + <li>OSの信頼性の向上と拡張性を目指している</li> + <li>CodeGear/DataGearという単位で記述される</li> + <li>ノーマルレベルとメタレベルを分離して記述できる + <ul> + <li>メタレベル処理を切り替えることで、信頼性検証やデバッグを行う</li> + <li>将来的に本研究の成果物も信頼性の検証を行う</li> + </ul> + </li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="codegearとdatagear-1">CodeGearとDataGear</h2> +<ul> + <li>CodeGear + <ul> + <li>実行Codeの単位</li> + <li>入力/出力のDataGearを持つ</li> + <li>goto文(jump命令)で遷移する</li> + </ul> + </li> + <li>DataGear + <ul> + <li>変数にあたり、構造体の型を持つ</li> </ul> </li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="codegearとdatagearの関係-1">CodeGearとDataGearの関係</h2> +<ul> + <li>InputDataGearを受け取って、CodeGearが処理し、OutputDataGearを出力する</li> + <li>OutputDataGearは次のCodeGearのInputDataGearとなる</li> + <li>CodeGear/DataGearはContextというオブジェクトで管理される</li> +</ul> +<div style="text-align: center;"> + <img src="images/cg-dg.pdf" alt="cgdgの関係図" width="600" /> +</div> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="分散フレームワークchristie-1">分散フレームワークChristie</h2> +<ul> + <li>Javaで記述された分散フレームワーク</li> + <li>GearsOSと似たGearという概念を持つ</li> + <li>CodeGearManagerと言うノードがCodeGear/DataGearを管理する + <ul> + <li>DataGearはDataGearManagerと言うデータプールに記録される</li> + </ul> + </li> + <li>DataGearをノード間で送り合うことで通信を行う</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="christieの通信">Christieの通信</h2> +<ul> + <li>LocalDGM + <ul> + <li>そのノードに対応するデータプール</li> + <li>CodeGearはLocalDGMからDataGearを参照する</li> + </ul> + </li> + <li>RemoteDGM + <ul> + <li>他のノードのLocalDGMに対応するproxy</li> + <li>RemoteDGMに書き込むと対応したLocalDGMに送信される</li> + </ul> + </li> + <li>DataGearManagerの仕組みをGearsOSのファイルに利用する</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="remotedgmによる通信">RemoteDGMによる通信</h2> +<ul> + <li>任意の相手のRemoteDGMを作成することで接続が形成される</li> + <li>RemoteDGMに書き込むと相手のLocalDGMに書き込みが行われる</li> +</ul> +<div style="text-align: center;"> + <img src="images/Remote_DataGearManager.pdf" alt="RemoteDGMの関係図" width="550" /> +</div> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="ポスター発表概要">ポスター発表概要</h2> +<ul> + <li>Christieの仕組みを用いたファイルシステム設計/実装の解説 + <ul> + <li>QueueとTreeを用いたファイル構造</li> + <li>ファイルAPI + <ul> + <li>Put/Take/Peek</li> + </ul> + </li> + <li>複数socketを用いたファイル通信の構成</li> + <li>WordCount例題</li> + </ul> + </li> + <li>まとめと課題</li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="まとめ">まとめ</h2> +<ul> + <li>GearsOSの通信を含めたファイルシステムの設計・開発を行った + <ul> + <li>DataGear単位によるファイル操作</li> + <li>複数のstreamを用いた通信の設計 + <ul> + <li>現時点では単一streamによる通信のみ開発済み</li> + </ul> + </li> + </ul> + </li> + <li>課題 + <ul> + <li>WordCount例題の再現</li> + <li>API/プロセスの信頼性や性能の調査</li> + </ul> + </li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="gearsosのファイルシステム">GearsOSのファイルシステム</h2> +<ul> + <li>ファイルデータの最小単位はDataGearとなる</li> <li>ファイルデータとなるDataGearはQueueに格納される</li> + <li>APIはPut/Take/Peekの三つで操作する</li> </ul> <div style="text-align: center;"> <img src="images/QueueElement.pdf" alt="Queue" width="800" /> @@ -171,14 +457,11 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="gearsosにおけるファイル-1">GearsOSにおけるファイル</h2> +<h2 id="gearsosにおけるファイル">GearsOSにおけるファイル</h2> <ul> - <li>ファイルは複数のQueueを持つ赤黒木である - <ul> - <li>Queueはkeyでアクセスされる</li> - <li>Queueはstreamの役割を持つ</li> - </ul> - </li> + <li>ファイルは複数のQueueを持つ赤黒木である</li> + <li>Queueはkeyでアクセスされる</li> + <li>Queueはstreamの役割を持つ</li> </ul> <div style="text-align: center;"> @@ -191,27 +474,16 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="fileapi">FileAPI</h2> +<h2 id="ファイルによる通信の構成">ファイルによる通信の構成</h2> <ul> - <li>ファイルのAPIは三種類となる</li> - <li>Put - <ul> - <li>Queueに対してデータを挿入する</li> - </ul> - </li> - <li>Take - <ul> - <li>Queueからデータを取り出す</li> - </ul> - </li> - <li>Peek - <ul> - <li>Queueからデータを”読み”だす</li> - <li>Takeの先読みに相当する</li> - </ul> - </li> - <li>APIは対象のstreamをkeyで指定する</li> + <li>GearsOSのファイルは通信も担当する</li> + <li>通信先のファイルのproxyを生成し通信する</li> + <li>proxyに対してデータを書き込むことで通信が行われる</li> + <li>WordCount例題を通して設計を行った</li> </ul> +<div style="text-align: center;"> + <img src="images/slideGearsWC.pdf" alt="Queue" width="500" /> +</div> @@ -229,7 +501,6 @@ </ul> </li> <li>記録デバイスへの保存も同様な仕組みで行う</li> - <li>将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う</li> </ul> @@ -245,35 +516,15 @@ <li>参加表明したノードを任意の形のTopologyへ配線する</li> </ul> </li> - <li>複数streamにより制御を行う分散ファイル通信手法としての検証 + <li>将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う</li> + <li>複数streamにより制御を行う分散ファイル通信の検証</li> + <li>GearsOSによるOSレベルTransactionの信頼性/実用性調査 <ul> - <li>Dataのみで通信を行う通信(規格があるプロトコルを用いない)</li> - <li>自律分散通信の見通し確保</li> - </ul> - </li> - <li>OSレベルなTransactionを搭載するアプリケーションとしての評価 - <ul> - <li>GearsOSのCodeGearはTransactionとなる</li> <li>従来ではアプリケーションレベルにより実装される</li> - <li>GearsOSによるOSレベルTransactionの信頼性/実用性調査</li> </ul> </li> </ul> - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="ポスターセッション">ポスターセッション</h2> -<ul> - <li>より詳細なGearsOSのファイル構造</li> - <li>ファイルの読み出し</li> - <li>proxyを用いたファイル通信の構成解説</li> - <li>研究のまとめと課題</li> -</ul> - </div>