Mercurial > hg > Papers > 2022 > ikki-master
comparison finalSlide/finalSlide.md @ 39:f78096cb1f69
tweak poster
author | ichikitakahiro <e165713@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 16 Feb 2022 01:12:38 +0900 (2022-02-15) |
parents | 8efb5398e604 |
children | cb0c76ff9de1 |
comparison
equal
deleted
inserted
replaced
38:e5570db4fcb4 | 39:f78096cb1f69 |
---|---|
6 | 6 |
7 | 7 |
8 | 8 |
9 ## 継続を導入したGearsOS | 9 ## 継続を導入したGearsOS |
10 - 継続を導入した、信頼性の保証を目指したOS開発プロジェクトである | 10 - 継続を導入した、信頼性の保証を目指したOS開発プロジェクトである |
11 - 関数遷移を用いず、**CodeGear**と言う単位で記述を行う | 11 - 関数遷移を用いず、**CodeGear**と**DataGear**と言う単位で記述を行う |
12 - 複数のCodeGearをgoto(jump命令)で遷移することで処理が実行される | 12 - 複数のCodeGearをgoto(jump命令)で遷移することで処理が実行される |
13 - OS自体の検証はプログラムが膨大な量となるため、テストコードを用いるのは難しい | 13 - OS自体の検証はプログラムが膨大な量となるため、テストコードを用いるのは難しい |
14 - GearsOSではメタレベルの処理からユーザープログラムの検証をする構成となる | 14 - GearsOSではメタレベルの処理からユーザープログラムの検証をする構成となる |
15 - GearsOSはノーマルレベルとメタレベルを分けて記述できる | 15 - GearsOSはノーマルレベルとメタレベルを分けて記述できる |
16 - メタレベルな処理を検証用のものに切り替えることで検証を行う | 16 - メタレベルな処理を検証用のものに切り替えることで検証を行う |
17 - 信頼性の検証には定理支援証明系やモデル検査を用いる | 17 - 信頼性の検証には定理支援証明系やモデル検査を用いる |
18 | 18 |
19 ## GearsOSのファイルシステム開発 | 19 ## GearsOSのファイルシステム開発 |
20 - GearsOSは現段階でファイルシステムを持っていない | 20 - GearsOSファイルシステムの開発にあたり要件定義を行った |
21 - 開発にあたりGearsOSファイルシステムの要件定義を行った | 21 - ファイルシステムも同様にGear単位で操作を行う |
22 - ファイルシステムも同様にGear単位で操作する | 22 - 従来ではアプリケーションが持つ機能の一部を取り入れたい |
23 - 煩雑な分散処理記述やノードの接続を簡潔に行いたい | 23 - Transaction |
24 - 従来ではアプリケーションが持つ機能の一部を取り入れたい | 24 - データ操作の整合性保護が施された処理 |
25 - Transaction | 25 - バックアップ |
26 - バックアップなど | 26 - 分散フレームワークChristieの仕組みを用いたい |
27 - 分散フレームワークChrisiteの仕組みでGearsFSの要件を満たしたい | |
28 | |
29 | 27 |
30 ## 分散フレームワークChristie | 28 ## 分散フレームワークChristie |
31 - 当研究室が開発する、Javaで書かれた分散フレームワークである | 29 - 当研究室が開発する、Javaで書かれた分散フレームワークである |
32 - GearsOSと似たGearと言うプログラミング概念を持つ | 30 - GearsOSと似たGearと言うプログラミング概念を持つ |
33 - 規格が決められたプロトコルを持たず、ノード間の通信はデータの書き込みで送受信で行う | 31 - ノード間の通信はDataGearの送り合いで構成される |
34 - 通信されるデータを意識しながら分散処理の記述が行える | 32 - Threadは任意のDataGearが揃ったら実行される |
35 - これらの構成は自立分散を目指した設計となっている | 33 - 通信されるデータを意識しながら分散処理の記述が行える |
34 - これらの構成は自律分散を目指した設計となっている | |
36 | 35 |
37 ## Christie likeな通信の分散ファイルシステムの提案 | 36 ## Christie likeな通信の分散ファイルシステムの提案 |
38 - Christieの仕組みを分散ファイルシステムに応用/検証を行いたい | 37 - Christieの仕組みを用いた分散ファイルシステムを設計/検証したい |
39 - GearsOSのファイルは複数のstreamを持ち、通信自体も行う | 38 - ファイルデータとなるDataGearを追いながらプロセスが記述できる |
40 - APIは通信部分を含め3種類で構成される | 39 - データのみの送受信による通信でネットワークの見通しを確保する |
41 - 簡潔な記述による分散処理の構成を目指す | 40 - 自律分散なファイルシステムを目指す |
42 - Christieの通信の仕組みにより、分散ネットワーク内の通信の見通しを確保する | |
43 - APIやプロセスの正当性は将来的に定理支援証明系agdaで検証される | 41 - APIやプロセスの正当性は将来的に定理支援証明系agdaで検証される |
42 | |
44 | 43 |
45 ## GearsOSが持つOSレベルなTransactionの実装検証 | 44 ## GearsOSが持つOSレベルなTransactionの実装検証 |
46 - GearsOSはAPIレベルでTransactionな記述が行える | 45 - GearsOSはAPIレベルでTransactionな記述が行える |
47 - 従来のアプリケーションでは、ユーザーレベルで実装される | 46 - 従来のアプリケーションでは、ユーザーレベルで実装される |
48 - GearsOSのAPIレベルで実装されるTransactionの実装検証を兼ねる | 47 - API自体のTransactionが保証されていれば、アプリケーションの信頼性保証が容易になる |
49 - OS自体のTransactionが保証されていれば、アプリケーションの信頼性が高まる | 48 - GearsOSのAPIレベルで実装されるTransactionの実装と検証を行う |
50 | 49 |
51 ## ポスター発表 | 50 ## ポスター発表 |
52 - GearsOSのChristie likeなファイルシステムの設計と実装 | 51 - GearsOSのChristie likeなファイルシステムの設計と実装 |
53 - ファイル構造 | 52 - ファイル構造 |
54 - QueueとTreeを用いる | 53 - QueueとTreeを用いる |