Mercurial > hg > Papers > 2022 > ikki-master

comparison finalSlide/finalSlide.md @ 41:3959e0817369

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tweak slide
author ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
date Thu, 17 Feb 2022 23:24:09 +0900
parents cb0c76ff9de1
children 01b88c0dd337
comparison
equal deleted inserted replaced
40:cb0c76ff9de1 41:3959e0817369
3 profile: 琉球大学理工学研究科情報工学専攻 3 profile: 琉球大学理工学研究科情報工学専攻
4 lang: Japanese 4 lang: Japanese
5 code-engine: coderay 5 code-engine: coderay
6 6
7 7
8
9 ## 継続を導入したGearsOS 8 ## 継続を導入したGearsOS
10 - 継続を導入した、信頼性の保証を目指したOS開発プロジェクトである 9 - OSの信頼性の保証と拡張性を目指したOS開発プロジェクトである
11 - 関数遷移を用いず、**CodeGear**と**DataGear**と言う単位で記述を行う 10 - アプリケーションの土台となるOSはより高い信頼性が保証されるべきである
12 - 複数のCodeGearをgoto(jump命令)で遷移することで処理が実行される 11 - OS自体の信頼性検証はプログラムが膨大な量となるため、テストコードによるデバッグは難しい
13 - OS自体の検証はプログラムが膨大な量となるため、テストコードを用いるのは難しい 12 - GearsOSではメタレベルの処理からユーザープログラムの検証を行うアプローチをとる
14 - GearsOSではメタレベルの処理からユーザープログラムの検証をする構成となる 13 - ノーマルレベルとメタレベルを分けて記述できる
15 - GearsOSはノーマルレベルとメタレベルを分けて記述できる 14 - メタレベルな処理を検証用のものに切り替えることで信頼性の検証を行う
16 - メタレベルな処理を検証用のものに切り替えることで検証を行う
17 - 信頼性の検証には定理支援証明系やモデル検査を用いる 15 - 信頼性の検証には定理支援証明系やモデル検査を用いる
18 16 - 関数遷移に代わり、**CodeGear**と**DataGear**と言う単位で記述を行う
19 ## GearsOSのファイルシステム開発 17 - 複数のCodeGearをgoto(jump命令)で遷移することで処理が実行される
20 - GearsOSファイルシステムの開発にあたり要件定義を行った 18
21 - ファイルシステムも同様にGear単位で操作を行う 19
22 - 従来ではアプリケーションが持つ機能の一部を取り入れたい 20 ## 研究目的
23 - Transaction 21 - GearsOSにより信頼性が裏付けられる、分散ファイルシステムの開発/検証を行いたい
24 - バックアップ 22 - 開発物はGearsOSによるAPIレベルなTransactionが実装される
25 - 分散フレームワークChristieの仕組みを用いたい 23 - Transactionとはデータ操作の不可分化による整合性の保護
24 - 従来のアプリでは、ユーザーレベルで実装される
25 - GearsOSが持つTransactionの実用性の検証
26 - 将来的にAPIやプロセスは定理支援証明系により整合性の検証が行われる
27
28 ## 研究目的
29 - 分散フレームワークChristieの仕組みを用いた分散ファイルシステムの提案
30 - 純粋なデータの送り合いだけで構成されるシンプルな通信
31 - 自律分散ファイルシステムを目指したい
32 - ネットワーク上で複数のプロトコルが使われることによる煩雑性を防ぐ
33 - GearsOSの処理単位であるDataGearでファイルを構成できる
26 34
27 ## 分散フレームワークChristie 35 ## 分散フレームワークChristie
28 - 当研究室が開発する、Javaで書かれた分散フレームワークである 36 - 当研究室が開発する、Javaで書かれた分散フレームワークである
29 - GearsOSと似たGearと言うプログラミング概念を持つ 37 - GearsOSと似たGearと言うプログラミング概念を持つ
30 - ノード間の通信はDataGearの送り合いで構成される 38 - ノード間の通信は、Threadの実行に必要になる変数データ(DataGear)の送り合いで構成される
31 - Threadは任意のDataGearが揃ったら実行される 39 - DataGearが揃ったThreadはノードにより実行される
32 - 通信されるデータを意識しながら分散処理の記述が行える 40 - ノードはDataGearを保存するkey value storeである,DataGearManagerを持つ
33 - これらの構成は自律分散を目指した設計となっている 41 - DataGearManagerにはLocalなものとRemoteのものが存在する
34 42 - GearsFSはDataGearManagerの仕組みを導入することで通信する
35 ## Christie likeな通信の分散ファイルシステムの提案 43
36 - Christieの仕組みを用いた分散ファイルシステムを設計/検証したい 44 ## スライド発表
37 - データのみの送受信により通信が構成される 45 - GearsOSとChristieの解説
38 - 分散ネットワーク全体の見通しの確保がのぞめる 46 - DataGearManagerの仕組み
39 - 自律分散なファイルシステムを目指したい 47 - Chlistie likeなファイルシステムの設計の解説
40 - APIやプロセスの正当性は将来的に定理支援証明系agdaで検証される 48 - ファイルとファイルデータの構造の設計
41 49 - API
42 50 - ファイルによる通信の設計と実装
43 ## GearsOSが持つOSレベルなTransactionを用いた実装 51 - GearsFSの例題による通信モデル
44 - GearsOSはAPIレベルでTransactionな記述が行える 52 - まとめと課題
45 - Transactionとはデータ操作の不可分化による整合性の保護 53
46 - 従来のアプリケーションでは、ユーザーレベルで実装される 54
47 - アプリケーションの土台となるOSが信頼性を保証したい
48 - APIにTransactionが実装されたアプリケーションの開発/検証
49 55
50 56
51 ## ポスター発表 57 ## ポスター発表
52 - GearsOSのChristie likeなファイルシステムの設計と実装 58 - GearsOSのChristie likeなファイルシステムの設計と実装
53 - ファイル構造 59 - ファイル構造