Mercurial > hg > Papers > 2023 > matac-sigos

--- a/gearsos_db.mm	Sat May 13 12:58:31 2023 +0900
+++ b/gearsos_db.mm	Sat May 13 16:03:48 2023 +0900
@@ -267,7 +267,13 @@
 <node TEXT="FSとDBの要素をRBTreeに対応させていく" ID="ID_1427881933" CREATED="1683883563484" MODIFIED="1683883616544"/>
 </node>
 <node TEXT="GearsOS" ID="ID_1141426374" CREATED="1683793922513" MODIFIED="1683883705146">
-<node TEXT="Continuation based C" ID="ID_1395196542" CREATED="1683793321859" MODIFIED="1683793874759"/>
+<node TEXT="Continuation based C" ID="ID_1395196542" CREATED="1683793321859" MODIFIED="1683793874759">
+<node TEXT="Cの下位言語" ID="ID_80856245" CREATED="1683948781065" MODIFIED="1683948809171"/>
+<node TEXT="処理の単位 CodeGear" ID="ID_404486795" CREATED="1683948812843" MODIFIED="1683948823529"/>
+<node TEXT="データの単位 DataGear" ID="ID_645800728" CREATED="1683948824112" MODIFIED="1683948831553"/>
+<node TEXT="ノーマルレベルとメタレベルの切り分け" ID="ID_1226372683" CREATED="1683948832790" MODIFIED="1683948848006"/>
+<node TEXT="gotoによる軽量継続" ID="ID_774603241" CREATED="1683948859720" MODIFIED="1683948866953"/>
+</node>
 <node TEXT="CodeGearとmetaCodeGearの関係" ID="ID_753651085" CREATED="1683794931069" MODIFIED="1683794966888"/>
 <node TEXT="Context" ID="ID_1314882832" CREATED="1683806340214" MODIFIED="1683806344795">
 <node TEXT="プロセスに相当" ID="ID_984799865" CREATED="1683883760580" MODIFIED="1683883769571"/>
@@ -357,8 +363,12 @@
 <node TEXT="ファイルシステムとDBの両方で使える" ID="ID_403512281" CREATED="1683885769067" MODIFIED="1683885779073"/>
 </node>
 </node>
-<node TEXT="時系列データ" ID="ID_332372763" CREATED="1683794801000" MODIFIED="1683794806307"/>
-<node TEXT="スタンドアロンなDB" ID="ID_797110426" CREATED="1683794806575" MODIFIED="1683794819595"/>
+<node TEXT="時系列データ" ID="ID_332372763" CREATED="1683794801000" MODIFIED="1683794806307">
+<node TEXT="データ圧縮" ID="ID_659511341" CREATED="1683951033179" MODIFIED="1683951038486"/>
+</node>
+<node TEXT="スタンドアロンなDB" ID="ID_797110426" CREATED="1683794806575" MODIFIED="1683794819595">
+<node TEXT="ポータビリティ" ID="ID_345345262" CREATED="1683951039757" MODIFIED="1683951045256"/>
+</node>
 </node>
 </node>
 </node>
--- a/marp-slide/slide.md	Sat May 13 12:58:31 2023 +0900
+++ b/marp-slide/slide.md	Sat May 13 16:03:48 2023 +0900
@@ -13,7 +13,7 @@
 琉球大学 理工学研究科 知能情報プログラム
 河野研究室

-### 又吉 雄斗, 佐野 巧曜, 河野 真治
+又吉 雄斗, 佐野 巧曜, 河野 真治

 ---

@@ -33,8 +33,12 @@
 ## Gears OSを使って実現する

 - CodeGear
+  - 処理の単位
 - DataGear
+  - データの単位
 - metaGear
+  - データの整合性
+  - 資源管理

 ---

@@ -44,16 +48,14 @@
   - GearsAgdaを使ってinvariantを証明する
 - テスト
 - モデル検査
-
-システムの構成要素全体にこれらの方法を適用したい
+- システムの構成要素全体にこれらの方法を適用したい

 ---

-## ファイルシステムとDBをRedBlackTreeで統一する
+## FSとDBの要素をRBTreeに対応させる

--
-  - RedBlackTreeはinvariantで証明する
-- ファイルシステムとDBの要素をRedBlackTreeに対応させていく
+- ファイルシステムとDBをRedBlackTreeで統一する
+- RedBlackTreeはinvariantで証明する

 ---

@@ -69,9 +71,6 @@

 ## CodeGearとmetaCodeGearの関係

-<!-- - CodeGearがDataGearを受け取り，処理後にDataGearを次のCodeGearに渡すという動作をしているように見える
-- 実際にはデータの整合性の確認や資源管理などのメタレベルの処理が存在し，それらの計算はMetaCodeGearで行われる -->
-
 - ノーマルレベルとメタレベルの存在

 ![w:1100](figs/meta_cg_dg.svg)
@@ -108,21 +107,45 @@

 ## ファイルシステムとDB

-- 両方ともRBTreeで実装する
+- 両方ともRedBlackTreeで実装する
+  - 本質的な役割は一緒
+  - 信頼性の向上
+  - 証明のしやすさ
 - 非破壊Tree
+  - データの持続性
+
+---
+
+## 非破壊的なRedBlackTree
+
+![w:1100](figs/nondestructive_tree_modification.png)

 ---

-## RBTreeはDBのテーブル
+## RedBlackTreeはDBのテーブル

-- テーブルのキーがRBTreeのkey
+- テーブルのキーがRedBlackTreeのkey
 - トランザクションはテーブルのルートの置き換え
-- 持続性
-  - オンメモリーなRBTree
-  - SSD上のコピー
-    - ログ的にコピーしていく
-- スキーマ
-  - DBの各テーブルのレコードの型定義
+- 複数の書き込みポイント
+
+![bg right:45% 65%](figs/transaction.svg)
+
+---
+
+## データの持続性
+
+- オンメモリーなRedBlackTree
+- SSD上のコピー
+  - ログ的にコピーしていく
+  - Copying GC
+
+---
+
+## スキーマ
+
+- DBの各テーブルのレコードの型定義
+- Contextに登録されているDataGearの型
+- キーを用いたDataGearの参照

 ---

@@ -132,18 +155,18 @@
   - queue
   - stack
 - DBにはリストやキューは入らない
-  - 第一正規系じゃないから
+  - 第一正規系でないから
 - データ構造を持続的にしたい
   - なのでファイルシステムが必要

 ---

-## RBTreeベースのファイルシステム
+## RedBlackTreeベースのファイルシステム

 - i-node番号をkeyにする
 - inodeにはDGのリストが入る
 - 持続性
-  - オンメモリーなRBTree
+  - オンメモリーなRedBlackTree
   - SSD上のコピー
     - ログ的にコピーしていく

@@ -155,23 +178,25 @@
   - トランザクションの失敗
   - システムクラッシュ
 - SSDのログからロールバックする
+  - Copying GCによるバックアップ
+  - ルートノードがデータのバージョン

 ---

 ## 構成要素

-- すべてRBTreeで構成されている
-  - 検証はRBTreeだけで良い
+- すべてRedBlackTreeで構成されている
+  - 検証はRedBlackTreeだけで良い
   - invariantで証明する
 - RedBlackTreeによる権限の表現
   - metaDGで行う
-  - ContextからアクセスできるRBTreeがある
+  - ContextからアクセスできるRedBlackTreeがある

 ---

 ## 信頼性の保証

-- RBTreeの変更の正しさ
+- RedBlackTreeの変更の正しさ
 - トランザクションの正しさ
 - アクセス権限の正しさ
 - SSDへのコピーの正しさ
@@ -186,13 +211,17 @@

 ## 今後の課題

-データクエリ言語
-    SQL
-    SQLより良いものが欲しい
-        ファイルシステムとDBの両方で使える
-時系列データ
-スタンドアロンなDB
+- データクエリ言語
+  - SQL
+  - SQLより良いものが欲しい
+    - ファイルシステムとDBの両方で使える
+- 時系列データ
+  - データ圧縮
+- スタンドアロンなDB
+  - ポータビリティ

+<!-- - CodeGearがDataGearを受け取り，処理後にDataGearを次のCodeGearに渡すという動作をしているように見える
+- 実際にはデータの整合性の確認や資源管理などのメタレベルの処理が存在し，それらの計算はMetaCodeGearで行われる -->

 <!-- ## RedBlackTreeを用いたFSの構築