--- a/gearsos_db.mm	Fri May 12 19:17:03 2023 +0900
+++ b/gearsos_db.mm	Sat May 13 12:58:31 2023 +0900
@@ -2,7 +2,7 @@
 <!--To view this file, download free mind mapping software Freeplane from https://www.freeplane.org -->
 <node TEXT="Gears OSの&#xa;FS &amp; DB" FOLDED="false" ID="ID_452131666" CREATED="1610381621610" MODIFIED="1680514786893" STYLE="oval">
 <font SIZE="18"/>
-<hook NAME="MapStyle" zoom="0.5">
+<hook NAME="MapStyle">
     <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"/>
 
 <map_styles>

--- a/marp-slide/slide.md	Fri May 12 19:17:03 2023 +0900
+++ b/marp-slide/slide.md	Sat May 13 12:58:31 2023 +0900
@@ -27,6 +27,7 @@
   - メモリとSSD
   - 分散ノード
   - ネットワーク
+
 ---
 
 ## Gears OSを使って実現する
@@ -42,35 +43,53 @@
 - 証明
   - GearsAgdaを使ってinvariantを証明する
 - テスト
-  - 
 - モデル検査
 
+システムの構成要素全体にこれらの方法を適用したい
+
+---
+
+## ファイルシステムとDBをRedBlackTreeで統一する
+
+- 
+  - RedBlackTreeはinvariantで証明する
+- ファイルシステムとDBの要素をRedBlackTreeに対応させていく
+
+---
+
+## Continuation based C
+
+- Cの下位言語である
+- 処理の単位 CodeGear
+- データの単位 DataGear
+- ノーマルレベルとメタレベルの切り分け
+- gotoによる軽量継続
+
 ---
 
-## Gears OS
-
-
+## CodeGearとmetaCodeGearの関係
 
-<!-- - アプリケーションの信頼性を保証するために，
-  アプリケーションが動作するOSの信頼性を高める必要がある
-- 信頼性確保の方法として定理証明やモデル検査がある
-- 当研究室では，信頼性の保証を目的としたGears OSを開発している
-- 証明や検証を容易に行えるよう，ファイルシステムのシンプルな実装を考えたい -->
+<!-- - CodeGearがDataGearを受け取り，処理後にDataGearを次のCodeGearに渡すという動作をしているように見える
+- 実際にはデータの整合性の確認や資源管理などのメタレベルの処理が存在し，それらの計算はMetaCodeGearで行われる -->
+
+- ノーマルレベルとメタレベルの存在
+
+![w:1100](figs/meta_cg_dg.svg)
 
 ---
 
-## RedBlackTreeを用いたFSの構築
+## Context
 
-- Gears OSへファイルシステムを実装するにあたり，RedBlackTreeを用いる
-- DBはファイルシステムと本質的に同じ役割を持っているため，同じRedBlackTreeでDBも表現することが可能であると考える
-
-### Gears OSにおけるDBの機能を持ち合わせたファイルシステムの設計を</br>信頼性の向上と， RedBlackTreeのみのシンプルな構造を基軸として考える
+- Gears OS上全てのCodeGear，DataGearの参照を持つ
+- OS上の処理の実行単位
+  - プロセスに相当
+- Gearの概念ではmetaDataGearに当たる
+- ノーマルレベルから直接参照されない
+  - metaCodeGearから参照される
 
 ---
 
-## 信頼性の保証を目的としたOS
-
-### 3種類のGears OS
+## 3種類のGears OS
 
 - GearsAgda(Agda)
   - 形式手法による信頼性の向上
@@ -81,40 +100,107 @@
 
 ---
 
-## Gears OS(CbC x.v6)
+## CodeGear遷移の流れ
+
+![w:1100](figs/context.svg)
+
+---
+
+## ファイルシステムとDB
+
+- 両方ともRBTreeで実装する
+- 非破壊Tree
+
+---
+
+## RBTreeはDBのテーブル
 
-- 当研究室にて，信頼性と拡張性の両立を目的として開発している
-- CbCで記述されている
-- Gearという概念があり，実行の単位をCodeGear，データの単位をDataGearと呼ぶ
-- ノーマルレベルとメタレベルの処理を切り分けることが容易にできる
+- テーブルのキーがRBTreeのkey
+- トランザクションはテーブルのルートの置き換え
+- 持続性
+  - オンメモリーなRBTree
+  - SSD上のコピー
+    - ログ的にコピーしていく
+- スキーマ
+  - DBの各テーブルのレコードの型定義
+
+---
+
+## インピーダンスミスマッチ
+
+- プログラムで使用するデータ構造
+  - queue
+  - stack
+- DBにはリストやキューは入らない
+  - 第一正規系じゃないから
+- データ構造を持続的にしたい
+  - なのでファイルシステムが必要
+
+---
+
+## RBTreeベースのファイルシステム
+
+- i-node番号をkeyにする
+- inodeにはDGのリストが入る
+- 持続性
+  - オンメモリーなRBTree
+  - SSD上のコピー
+    - ログ的にコピーしていく
 
 ---
 
-## CodeGearとmetaCodeGearの関係
+## バックアップとロールバック
 
-### ノーマルレベルとメタレベルの存在
-- CodeGearがDataGearを受け取り，処理後にDataGearを次のCodeGearに渡すという動作をしているように見える
-- 実際にはデータの整合性の確認や資源管理などのメタレベルの処理が存在し，それらの計算はMetaCodeGearで行われる
+- ロールバックの必要性
+  - トランザクションの失敗
+  - システムクラッシュ
+- SSDのログからロールバックする
 
 ---
-## CodeGearとmetaCodeGearの関係
+
+## 構成要素
 
-![w:1100](figs/meta_cg_dg.svg)
+- すべてRBTreeで構成されている
+  - 検証はRBTreeだけで良い
+  - invariantで証明する
+- RedBlackTreeによる権限の表現
+  - metaDGで行う
+  - ContextからアクセスできるRBTreeがある
 
 ---
 
-## Context
+## 信頼性の保証
 
-- Gears OS上全てのCodeGear，DataGearの参照を持つ
-- OS上の処理の実行単位
-- Gearの概念ではMetaDataGearに当たる
-- ノーマルレベルから直接参照されず，必ずMetaDataGearとしてMetaCodeGearから参照される
+- RBTreeの変更の正しさ
+- トランザクションの正しさ
+- アクセス権限の正しさ
+- SSDへのコピーの正しさ
+- ポータビリティ
+  - 異なる計算機アーキテクチャ
+  - 異なるエンコード
+  - 異なる分散ノード
+- 正しくスキーマに対応しているかどうか
+  - 違反しても良い
 
 ---
 
-## CodeGear遷移の流れ
+## 今後の課題
+
+データクエリ言語
+    SQL
+    SQLより良いものが欲しい
+        ファイルシステムとDBの両方で使える
+時系列データ
+スタンドアロンなDB
 
-![w:1100](figs/context.svg)
+
+<!-- ## RedBlackTreeを用いたFSの構築
+
+- Gears OSへファイルシステムを実装するにあたり，RedBlackTreeを用いる
+- DBはファイルシステムと本質的に同じ役割を持っているため，同じRedBlackTreeでDBも表現することが可能であると考える
+
+### Gears OSにおけるDBの機能を持ち合わせたファイルシステムの設計を</br>信頼性の向上と， RedBlackTreeのみのシンプルな構造を基軸として考える
+
 
 ---
 
@@ -239,4 +325,4 @@
 
 - データクエリ言語
 - 時系列データ
-- スタンドアロンDB
\ No newline at end of file
+- スタンドアロンDB -->
\ No newline at end of file