Mercurial > hg > Papers > 2024 > matac-master

changeset 73:c4b013299ff6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
outline(slide & poster)
author matac42 <matac@cr.ie.u-ryukyu.ac.jp>
date Tue, 13 Feb 2024 20:25:58 +0900
parents b2a541a2c178
children 8c087f2ae631
files marp-slide/slide.md mindmaps/gears_fs_db.mm poster/matac-poster.graffle
diffstat 3 files changed, 107 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/marp-slide/slide.md	Tue Feb 13 17:12:55 2024 +0900
+++ b/marp-slide/slide.md	Tue Feb 13 20:25:58 2024 +0900
@@ -16,7 +16,7 @@
 スピーカーノート
 -->
 
-琉球大学 理工学研究科 知能情報プログラム
+琉球大学 理工学研究科 工学専攻 知能情報プログラム
 河野研究室
 
 又吉 雄斗
@@ -96,43 +96,102 @@
 
 - GearsAgda(Agda)
   - 形式手法による信頼性の向上
-- Gears OS(CbC)
+- CbC x.v6
+  - スタンドアロンOS
+- Gears OS(CbC) ← 今回の実装対象
   - ユーザーレベルタスクマネージメント
-- CbC x.v6 ← 今回の実装対象
-  - スタンドアロンOS
 
 ---
 
-## GearsOSとGearsAgda
+## GearsAgdaとGearsOSの対応
+
+- GearsOSのCodeGearと直接対応している
+- GearsAgdaでRedBlackTreeの証明が進められている
+  - find完了、insert証明中
+- GearsOSの構造はRedBlackTreeが多くを占める
+
+GearsAgdaでRedBlackTreeが証明できれば、GearsOSの大部分を証明したことになる
 
 ---
 
-<!-- ここまでがGears OSの基礎概念だと明示する -->
-
 ## CodeGear遷移の流れ
 
 ![w:1100](figs/context.svg)
 
 ---
 
-## 非破壊RedBlackTreeによる構成
+## 非破壊RedBlackTree
+
+![w:1100](figs/nondestructive_tree_modification.png)
+
+---
+
+<!-- ここまでがGears OSの基礎概念だと明示する -->
+
+## GearsFilesystem
+
+- GearsOSで書かれたファイルシステム
+  - i-nodeによるディレクトリシステム
+  - 分散ファイルシステムの通信機能
+- 非破壊RedBlackTreeで構成される
+- ディスク上とメモリ上のデータ構造を統一する
 
 ---
 
-## GearsFilesystem
+## ファイルシステムの信頼性
+
+- 電源断時にデータが残るpersistency
+- データを書き込めたかどうかを判定するatomic write
+- ノード喪失時にデータを保護する多重性
+- 複数のコピーを調停するコミット機構
+
+---
+
+## メモリ管理や多重性の機能がない
+
+メモリ管理
+
+- GC(ガベージコレクション)
+
+多重性
+
+- レプリケーション
+- バックアップ
 
 
 ---
 
-## 多重性やメモリ管理に必要な機能がない
+## メモリ管理や多重性の機能の要件
+
+- データの持続性
+  - 証明のしやすさの維持
+  - データを破壊しない
+- 非破壊RedBlackTreeの増大抑制
+  - 非破壊RedBlackTreeは履歴を全て持つ
+  - そのままにすると増大し、メモリを圧迫する
+
+---
+
+## GearsOSにおけるGC
+
+CopyingGCを採用する
+
+---
+
+## GearsOSにおけるレプリケーション
+
+単純に木をコピーする
 
 ---
 
 ## copyRedBlackTreeの実装をした
 
+- RedBlackTreeのコピーを行う
+- GCやレプリケーションの機能のために木のコピーが必要
+
 ---
 
-## copyRedBlackTreeができると何ができるようになるか
+## copyRedBlackTreeによって出来ること
 
 多重性やメモリ管理に関する機能を追加できる
 GC(defragmentation)
@@ -141,24 +200,30 @@
 
 ---
 
-## GCによる非破壊RedBlackTreeの増大問題
-
----
-
 ## Tree InterfaceのAPIとして実装
 
 ---
 
-## コピーのアルゴリズム
+## コピーのアルゴリズム詳細
+
+![w:1100](figs/)
 
 ---
 
 ## アロケーション部分
 
+![w:1100](figs/)
+
 ---
 
 ## swap
 
+![w:1100](figs/)
+
+---
+
+## 実行方法
+
 ---
 
 ## 評価
@@ -167,11 +232,17 @@
 コピーするだけなので木が持続的
 課題点
   同一Contextへコピーしている
+コピーの正しさ
+
 
 ---
 
 ## 今後の研究方針
 
+別Contextコピー
+GC，レプリケーションの実装
+多重性以外の機能
+
 ---
 
 ## まとめ
@@ -179,4 +250,4 @@
 copyRedBlackTreeを実装した
 それにより多重性を確保できるようになった
 多重性はシステムの信頼性を向上させる
-非破壊RedBlackTreeの増大抑制により実用的に
+非破壊RedBlackTreeの増大抑制により実用的なシステム構築が可能になった
--- a/mindmaps/gears_fs_db.mm	Tue Feb 13 17:12:55 2024 +0900
+++ b/mindmaps/gears_fs_db.mm	Tue Feb 13 20:25:58 2024 +0900
@@ -1,6 +1,6 @@
 <map version="freeplane 1.9.8">
 <!--To view this file, download free mind mapping software Freeplane from https://www.freeplane.org -->
-<node TEXT="GearsOS上のファイルシステムとDBの信頼性(仮)" FOLDED="false" ID="ID_452131666" CREATED="1610381621610" MODIFIED="1707801882816" STYLE="oval">
+<node TEXT="GearsOS上のファイルシステムとDBの信頼性(仮)" FOLDED="false" ID="ID_452131666" CREATED="1610381621610" MODIFIED="1707822387228" STYLE="oval">
 <font SIZE="18"/>
 <hook NAME="MapStyle" zoom="0.8">
     <properties edgeColorConfiguration="#808080ff,#ff0000ff,#0000ffff,#00ff00ff,#ff00ffff,#00ffffff,#7c0000ff,#00007cff,#007c00ff,#7c007cff,#007c7cff,#7c7c00ff" associatedTemplateLocation="template:/standard-1.6-noEdgeColor.mm" fit_to_viewport="false"/>
@@ -1266,7 +1266,7 @@
 </node>
 </node>
 </node>
-<node TEXT="スライド" POSITION="left" ID="ID_1109312213" CREATED="1707801871675" MODIFIED="1707810947177">
+<node TEXT="スライド" FOLDED="true" POSITION="left" ID="ID_1109312213" CREATED="1707801871675" MODIFIED="1707813260044">
 <node TEXT="システム全体の信頼性を向上させたい" ID="ID_1519013410" CREATED="1707809324624" MODIFIED="1707809621777" HGAP_QUANTITY="14 pt" VSHIFT_QUANTITY="-3 pt"/>
 <node TEXT="GearsOSで実現する" ID="ID_1781659444" CREATED="1707809341570" MODIFIED="1707809348782"/>
 <node TEXT="信頼性を上げる方法" ID="ID_284645498" CREATED="1707809403391" MODIFIED="1707809624565" HGAP_QUANTITY="12.5 pt" VSHIFT_QUANTITY="-33.75 pt"/>
@@ -1276,19 +1276,20 @@
 <node TEXT="3種類のGearsOS" ID="ID_1789403817" CREATED="1707809449604" MODIFIED="1707809454625"/>
 <node TEXT="GearsOSとGearsAgda" ID="ID_1922073865" CREATED="1707810849140" MODIFIED="1707810857063"/>
 <node TEXT="CodeGear遷移の流れ" ID="ID_1864344252" CREATED="1707809502144" MODIFIED="1707809508404"/>
-<node TEXT="非破壊RedBlackTreeによる構成" ID="ID_622602101" CREATED="1707805849509" MODIFIED="1707810947176" HGAP_QUANTITY="12.5 pt" VSHIFT_QUANTITY="3.75 pt"/>
+<node TEXT="非破壊RedBlackTree" ID="ID_622602101" CREATED="1707805849509" MODIFIED="1707819298376" HGAP_QUANTITY="12.5 pt" VSHIFT_QUANTITY="3.75 pt"/>
 <node TEXT="GearsFilesystem" ID="ID_9731029" CREATED="1707810937030" MODIFIED="1707810953288" HGAP_QUANTITY="15.5 pt" VSHIFT_QUANTITY="-61.5 pt"/>
-<node TEXT="多重性やメモリ管理に必要な機能がない" ID="ID_1755524219" CREATED="1707809043957" MODIFIED="1707809590104"/>
+<node TEXT="ファイルシステムの信頼性" ID="ID_1312841457" CREATED="1707819281060" MODIFIED="1707819289625"/>
+<node TEXT="メモリ管理や多重性の機能がない" ID="ID_1755524219" CREATED="1707809043957" MODIFIED="1707819996876"/>
 <node TEXT="copyRedBlackTreeの実装をした" ID="ID_3452822" CREATED="1707802848111" MODIFIED="1707802871025"/>
-<node TEXT="copyRedBlackTreeができると何ができるようになるか" FOLDED="true" ID="ID_108556449" CREATED="1707804472923" MODIFIED="1707809906416">
+<node TEXT="copyRedBlackTreeによって出来ること" FOLDED="true" ID="ID_108556449" CREATED="1707804472923" MODIFIED="1707813284750">
 <node TEXT="多重性やメモリ管理に関する機能を追加できる" ID="ID_42031813" CREATED="1707804510984" MODIFIED="1707805366037"/>
-<node TEXT="GC(defragmentation)" ID="ID_240352266" CREATED="1707802572704" MODIFIED="1707809162287">
-<node TEXT="特にこれは欲しい" ID="ID_245613381" CREATED="1707809727579" MODIFIED="1707809740497"/>
-</node>
+<node TEXT="GC(defragmentation)" ID="ID_240352266" CREATED="1707802572704" MODIFIED="1707809162287"/>
 <node TEXT="レプリケーション" ID="ID_854911737" CREATED="1707802624641" MODIFIED="1707802629911"/>
 <node TEXT="バックアップ" ID="ID_1828283529" CREATED="1707809645235" MODIFIED="1707809648227"/>
 </node>
-<node TEXT="GCによる非破壊RedBlackTreeの増大問題" ID="ID_561572897" CREATED="1707809658587" MODIFIED="1707809922510" HGAP_QUANTITY="13.25 pt" VSHIFT_QUANTITY="-71.25 pt"/>
+<node TEXT="GearsOSにおけるGCの仕組み" ID="ID_1212824888" CREATED="1707813214599" MODIFIED="1707813226175"/>
+<node TEXT="GCによる非破壊RedBlackTreeの増大抑制" ID="ID_561572897" CREATED="1707809658587" MODIFIED="1707813256692" HGAP_QUANTITY="14.75 pt" VSHIFT_QUANTITY="3.75 pt"/>
+<node TEXT="GearsOSにおけるレプリケーションの仕組み" ID="ID_685680544" CREATED="1707813227111" MODIFIED="1707813260043" HGAP_QUANTITY="13.25 pt" VSHIFT_QUANTITY="-72.75 pt"/>
 <node TEXT="Tree InterfaceのAPIとして実装" ID="ID_235794385" CREATED="1707802437228" MODIFIED="1707802472777"/>
 <node TEXT="コピーのアルゴリズム" ID="ID_1999989614" CREATED="1707802473477" MODIFIED="1707802480540"/>
 <node TEXT="アロケーション部分" ID="ID_952299777" CREATED="1707802483093" MODIFIED="1707802493772"/>
@@ -1308,5 +1309,14 @@
 <node TEXT="非破壊RedBlackTreeの増大抑制により実用的に" ID="ID_1391218931" CREATED="1707802699292" MODIFIED="1707809767003"/>
 </node>
 </node>
+<node TEXT="ポスターに入れたいもの" POSITION="left" ID="ID_1881273288" CREATED="1707822259912" MODIFIED="1707822387227" HGAP_QUANTITY="12.5 pt" VSHIFT_QUANTITY="64.5 pt">
+<node TEXT="GearsOS" ID="ID_244799882" CREATED="1707822267808" MODIFIED="1707822983639"/>
+<node TEXT="ファイルシステムの信頼性" ID="ID_136338806" CREATED="1707823012701" MODIFIED="1707823018332"/>
+<node TEXT="GCとレプリケーションの設計" ID="ID_992154700" CREATED="1707823067343" MODIFIED="1707823073222"/>
+<node TEXT="非破壊RedBlackTree" ID="ID_1835595740" CREATED="1707822970774" MODIFIED="1707822979862"/>
+<node TEXT="copyRedBlackTree" ID="ID_353953232" CREATED="1707822958701" MODIFIED="1707822989023"/>
+<node TEXT="評価" ID="ID_1506754242" CREATED="1707822992003" MODIFIED="1707822996084"/>
+<node TEXT="まとめと今後の課題" ID="ID_198670271" CREATED="1707822300449" MODIFIED="1707822329881"/>
+</node>
 </node>
 </map>
Binary file poster/matac-poster.graffle has changed