--- a/gearsos_db.mm	Fri May 12 17:54:45 2023 +0900
+++ b/gearsos_db.mm	Fri May 12 19:17:03 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">
+<hook NAME="MapStyle" zoom="0.5">
     <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>
@@ -247,35 +247,116 @@
 <node TEXT="メモリ不足の懸念について" ID="ID_1617906662" CREATED="1681690970726" MODIFIED="1681691008346"/>
 </node>
 <node TEXT="スライド" POSITION="left" ID="ID_431898265" CREATED="1683792995152" MODIFIED="1683793001137">
-<node TEXT="研究目的" ID="ID_1890538039" CREATED="1683793004172" MODIFIED="1683793009443"/>
-<node TEXT="RBTreeのみを用いたファイルシステム" ID="ID_1128973381" CREATED="1683793009880" MODIFIED="1683794365312"/>
-<node TEXT="基礎概念" ID="ID_1358583686" CREATED="1683794678940" MODIFIED="1683794687314">
+<node TEXT="システム全体の信頼性を上げたい" ID="ID_1890538039" CREATED="1683793004172" MODIFIED="1683883672742">
+<node TEXT="システムの構成要素" ID="ID_1014766369" CREATED="1683883297464" MODIFIED="1683883327085">
+<node TEXT="アプリケーション" ID="ID_747921644" CREATED="1683883328917" MODIFIED="1683883336669"/>
+<node TEXT="OS" ID="ID_79609665" CREATED="1683883337608" MODIFIED="1683883344561"/>
+<node TEXT="ファイルシステム" ID="ID_1153637340" CREATED="1683883345433" MODIFIED="1683883354146"/>
+<node TEXT="DB" ID="ID_831118147" CREATED="1683883435775" MODIFIED="1683883438272"/>
+</node>
+<node TEXT="全部の信頼性を上げる必要がある" ID="ID_1503745478" CREATED="1683883315579" MODIFIED="1683883380590"/>
+<node TEXT="信頼性を上げる方法" ID="ID_362676709" CREATED="1683883391223" MODIFIED="1683883398860">
+<node TEXT="証明" ID="ID_384370369" CREATED="1683883400049" MODIFIED="1683883405860"/>
+<node TEXT="テスト" ID="ID_447313982" CREATED="1683883406881" MODIFIED="1683883412697"/>
+<node TEXT="モデル検査" ID="ID_1419644121" CREATED="1683883413301" MODIFIED="1683883418846"/>
+</node>
+<node TEXT="システムの構成要素全体にこれらの方法を適用したい" ID="ID_1283219027" CREATED="1683883443218" MODIFIED="1683883457173"/>
+<node TEXT="なのでファイルシステムとDBをRBTreeで統一する" ID="ID_1025933271" CREATED="1683883468276" MODIFIED="1683883489128">
+<node TEXT="RBTreeはinvariantで証明する" ID="ID_445938459" CREATED="1683883500370" MODIFIED="1683883513878"/>
+</node>
+<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="信頼性の保証を目的としたGearsOS" ID="ID_1141426374" CREATED="1683793922513" MODIFIED="1683793933208">
-<node TEXT="3種類のGears OS" ID="ID_1638511555" CREATED="1683794932101" MODIFIED="1683794941745"/>
-<node TEXT="CbC_xv6" ID="ID_526651554" CREATED="1683795422645" MODIFIED="1683795432266">
 <node TEXT="CodeGearとmetaCodeGearの関係" ID="ID_753651085" CREATED="1683794931069" MODIFIED="1683794966888"/>
-<node TEXT="Context" ID="ID_1314882832" CREATED="1683806340214" MODIFIED="1683806344795"/>
+<node TEXT="Context" ID="ID_1314882832" CREATED="1683806340214" MODIFIED="1683806344795">
+<node TEXT="プロセスに相当" ID="ID_984799865" CREATED="1683883760580" MODIFIED="1683883769571"/>
+<node TEXT="実行するCG全部" ID="ID_661261070" CREATED="1683883776358" MODIFIED="1683883786426"/>
+<node TEXT="使用するDG全部" ID="ID_1319063458" CREATED="1683883788171" MODIFIED="1683883802746"/>
+</node>
+<node TEXT="3種類のGears OS" ID="ID_1638511555" CREATED="1683794932101" MODIFIED="1683794941745">
+<node TEXT="Gears OS" ID="ID_1681177863" CREATED="1683883064324" MODIFIED="1683883068917"/>
+<node TEXT="GearsAgda" ID="ID_375982353" CREATED="1683883069627" MODIFIED="1683883073909"/>
+<node TEXT="x.v6 Gears OS" ID="ID_190998500" CREATED="1683883075051" MODIFIED="1683883103215"/>
+</node>
 <node TEXT="CodeGear遷移の流れ" ID="ID_323902571" CREATED="1683806345281" MODIFIED="1683806357556"/>
 </node>
-</node>
-<node TEXT="RedBlackTree" ID="ID_859692491" CREATED="1683794703621" MODIFIED="1683794707722"/>
+<node TEXT="ファイルシステムとDB" ID="ID_1128973381" CREATED="1683793009880" MODIFIED="1683883898400">
+<node TEXT="両方ともRBTreeで実装する" ID="ID_338147682" CREATED="1683883903595" MODIFIED="1683883919004"/>
 <node TEXT="非破壊Tree" ID="ID_991571864" CREATED="1683806464582" MODIFIED="1683806470052"/>
 </node>
-<node TEXT="RedBlackTreeによるファイルシステムの構成" ID="ID_1294893477" CREATED="1683793023134" MODIFIED="1683794732881"/>
+<node TEXT="RBTreeはDBのテーブル" ID="ID_1210007329" CREATED="1683884139615" MODIFIED="1683884767732">
+<node TEXT="テーブルのキーがRBTreeのkey" ID="ID_1868861117" CREATED="1683884158878" MODIFIED="1683884170852"/>
+<node TEXT="トランザクションはテーブルのルートの置き換え" ID="ID_541885376" CREATED="1683884184294" MODIFIED="1683884194654"/>
+<node TEXT="持続性" ID="ID_15924648" CREATED="1683884200660" MODIFIED="1683884206382">
+<node TEXT="オンメモリーなRBTree" ID="ID_1253922918" CREATED="1683884211820" MODIFIED="1683884221207"/>
+<node TEXT="SSD上のコピー" ID="ID_1148185240" CREATED="1683884223594" MODIFIED="1683884243957">
+<node TEXT="ログ的にコピーしていく" ID="ID_1601869481" CREATED="1683884277811" MODIFIED="1683884287139"/>
+</node>
+</node>
+<node TEXT="スキーマ" ID="ID_894019841" CREATED="1683884297816" MODIFIED="1683884301716">
+<node TEXT="DBの各テーブルのレコードの型定義" ID="ID_148789198" CREATED="1683884326057" MODIFIED="1683884352477"/>
+</node>
+</node>
+<node TEXT="インピーダンスミスマッチ" ID="ID_1186788713" CREATED="1683879688032" MODIFIED="1683879695817">
+<node TEXT="プログラムで使用するデータ構造" ID="ID_1917732087" CREATED="1683884593868" MODIFIED="1683884611694">
+<node TEXT="queue" ID="ID_1295277731" CREATED="1683884613901" MODIFIED="1683884615801"/>
+<node TEXT="stack" ID="ID_1335632480" CREATED="1683884616552" MODIFIED="1683884618124"/>
+</node>
+<node TEXT="DBにはリストやキューは入らない" ID="ID_1480845790" CREATED="1683884626471" MODIFIED="1683884643941">
+<node TEXT="第一正規系じゃないから" ID="ID_335463616" CREATED="1683884649155" MODIFIED="1683884659865"/>
+</node>
+<node TEXT="データ構造を持続的にしたい" ID="ID_900229592" CREATED="1683884683285" MODIFIED="1683884695737"/>
+<node TEXT="なのでファイルシステムが必要" ID="ID_285640515" CREATED="1683884715014" MODIFIED="1683884724086"/>
+</node>
+<node TEXT="RBTreeベースのファイルシステム" ID="ID_1651173215" CREATED="1683884803188" MODIFIED="1683884813352">
+<node TEXT="i-node番号をkeyにする" ID="ID_1204818335" CREATED="1683884816711" MODIFIED="1683884839827"/>
+<node TEXT="inodeにはDGのリストが入る" ID="ID_158456106" CREATED="1683884847087" MODIFIED="1683884856157"/>
+<node TEXT="持続性" ID="ID_828038948" CREATED="1683884200660" MODIFIED="1683884206382">
+<node TEXT="オンメモリーなRBTree" ID="ID_1576608166" CREATED="1683884211820" MODIFIED="1683884221207"/>
+<node TEXT="SSD上のコピー" ID="ID_1244723646" CREATED="1683884223594" MODIFIED="1683884243957">
+<node TEXT="ログ的にコピーしていく" ID="ID_472869525" CREATED="1683884277811" MODIFIED="1683884287139"/>
+</node>
+</node>
+</node>
+<node TEXT="バックアップとロールバック" ID="ID_854574982" CREATED="1683885054716" MODIFIED="1683885061163">
+<node TEXT="ロールバックの必要性" ID="ID_477502303" CREATED="1683885063629" MODIFIED="1683885092573">
+<node TEXT="トランザクションの失敗" ID="ID_1422510197" CREATED="1683885097219" MODIFIED="1683885105977"/>
+<node TEXT="システムクラッシュ" ID="ID_1971166091" CREATED="1683885108581" MODIFIED="1683885113653"/>
+</node>
+<node TEXT="SSDのログからロールバックする" ID="ID_1211991984" CREATED="1683885094116" MODIFIED="1683885137953"/>
+</node>
 <node TEXT="構成要素" ID="ID_276464145" CREATED="1683794743578" MODIFIED="1683794755540">
-<node TEXT="ディスク上とメモリ上のデータ構造" ID="ID_1896955874" CREATED="1683793037629" MODIFIED="1683793103973"/>
-<node TEXT="データのロールバックとバックアップ" ID="ID_477481724" CREATED="1683793094263" MODIFIED="1683793271944"/>
-<node TEXT="RedBlackTreeのトランザクション" ID="ID_1405876359" CREATED="1683793274014" MODIFIED="1683793288188"/>
-<node TEXT="ファイルシステムにおけるスキーマ" ID="ID_1655208991" CREATED="1683879632410" MODIFIED="1683879640748">
-<node TEXT="ロールバック" ID="ID_1514831247" CREATED="1683879644066" MODIFIED="1683879687168"/>
-<node TEXT="インピーダンスミスマッチ" ID="ID_1186788713" CREATED="1683879688032" MODIFIED="1683879695817"/>
-<node TEXT="Gears OSにおけるスキーマ" ID="ID_408740723" CREATED="1683879711657" MODIFIED="1683879719894"/>
+<node TEXT="すべてRBTreeで構成されている" ID="ID_332682241" CREATED="1683885311240" MODIFIED="1683885327061">
+<node TEXT="検証はRBTreeだけで良い" ID="ID_582555526" CREATED="1683885328836" MODIFIED="1683885341818"/>
+<node TEXT="invariantで証明する" ID="ID_139128895" CREATED="1683885345869" MODIFIED="1683885354111"/>
+</node>
+<node TEXT="RedBlackTreeによる権限の表現" ID="ID_1216462813" CREATED="1683794500652" MODIFIED="1683794512373">
+<node TEXT="metaDGで行う" ID="ID_1630653969" CREATED="1683885292879" MODIFIED="1683885376757"/>
+<node TEXT="ContextからアクセスできるRBTreeがある" ID="ID_246875372" CREATED="1683885399127" MODIFIED="1683885417137"/>
+</node>
 </node>
-<node TEXT="RedBlackTreeによる権限の表現" ID="ID_1216462813" CREATED="1683794500652" MODIFIED="1683794512373"/>
+<node TEXT="信頼性の保証" ID="ID_1707333614" CREATED="1683885455061" MODIFIED="1683885460354">
+<node TEXT="RBTreeの変更の正しさ" ID="ID_1947487467" CREATED="1683885464005" MODIFIED="1683885481235"/>
+<node TEXT="トランザクションの正しさ" ID="ID_249206113" CREATED="1683885483792" MODIFIED="1683885490884"/>
+<node TEXT="アクセス権限の正しさ" ID="ID_228944734" CREATED="1683885493942" MODIFIED="1683885502106"/>
+<node TEXT="SSDへのコピーの正しさ" ID="ID_1162042910" CREATED="1683885517769" MODIFIED="1683885527425"/>
+<node TEXT="ポータビリティ" ID="ID_1913557735" CREATED="1683885566839" MODIFIED="1683885574074">
+<node TEXT="異なる計算機アーキテクチャ" ID="ID_1484140660" CREATED="1683885577528" MODIFIED="1683885596471"/>
+<node TEXT="異なるエンコード" ID="ID_108264570" CREATED="1683885598095" MODIFIED="1683885606608"/>
+<node TEXT="異なる分散ノード" ID="ID_215774197" CREATED="1683885608829" MODIFIED="1683885620441"/>
+</node>
+<node TEXT="正しくスキーマに対応しているかどうか" ID="ID_1511508705" CREATED="1683885679093" MODIFIED="1683885689717">
+<node TEXT="違反しても良い" ID="ID_55096761" CREATED="1683885701723" MODIFIED="1683885708755"/>
+</node>
 </node>
 <node TEXT="今後の課題" ID="ID_685047053" CREATED="1683793290797" MODIFIED="1683794487940">
-<node TEXT="データクエリ言語" ID="ID_1616582759" CREATED="1683794794770" MODIFIED="1683794800026"/>
+<node TEXT="データクエリ言語" ID="ID_1616582759" CREATED="1683794794770" MODIFIED="1683794800026">
+<node TEXT="SQL" ID="ID_76668619" CREATED="1683885753253" MODIFIED="1683885757190"/>
+<node TEXT="SQLより良いものが欲しい" ID="ID_21165219" CREATED="1683885758848" MODIFIED="1683885767794">
+<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>

--- a/marp-slide/slide.md	Fri May 12 17:54:45 2023 +0900
+++ b/marp-slide/slide.md	Fri May 12 19:17:03 2023 +0900
@@ -17,13 +17,45 @@
 
 ---
 
-## 研究目的
+## システム全体の信頼性を上げたい
+
+- システムの構成要素全体の信頼性を上げる必要がある
+  - アプリケーション
+  - OS
+  - ファイルシステム
+  - DB
+  - メモリとSSD
+  - 分散ノード
+  - ネットワーク
+---
+
+## Gears OSを使って実現する
+
+- CodeGear
+- DataGear
+- metaGear
 
-- アプリケーションの信頼性を保証するために，
+---
+
+## 信頼性を上げる方法
+
+- 証明
+  - GearsAgdaを使ってinvariantを証明する
+- テスト
+  - 
+- モデル検査
+
+---
+
+## Gears OS
+
+
+
+<!-- - アプリケーションの信頼性を保証するために，
   アプリケーションが動作するOSの信頼性を高める必要がある
 - 信頼性確保の方法として定理証明やモデル検査がある
 - 当研究室では，信頼性の保証を目的としたGears OSを開発している
-- 証明や検証を容易に行えるよう，ファイルシステムのシンプルな実装を考えたい
+- 証明や検証を容易に行えるよう，ファイルシステムのシンプルな実装を考えたい -->
 
 ---
 
@@ -185,40 +217,6 @@
 - 最新の情報が欲しい場合は書き込みを一旦止めるような処理が必要になる
 
 ---
-<!-- 
-## ファイルシステムにおけるスキーマ
-
-- 従来のRDBのようなスキーマが存在すると，個別にバックアップなどを取らない限りスキーマの変更以前にロールバックすることができない．
-- しかしながら，実際運用する上でスキーマを変更することは多々ある．
-- これは，データの信頼性を低下させると考える．
-
----
-
-## ファイルシステムにおけるスキーマ
-
-- DB上のデータ構造とプログラム上で扱うデータ構造に差が生まれるインピーダンスミスマッチが発生し，DBのデータをプログラムが扱う際に
-その差を埋めるような変換を必要とする場合が生まれる
-
----
-
-## ファイルシステムにおけるスキーマ
-
-一方で，スキーマがあることによってデータに対して高度な操作を行うことができ，
-また，インデックスを容易に作成することができるといったメリットがある．
-よって，スキーマフルなDBとスキーマレスなDBはそれぞれメリットデメリットがあり，
-状況によって使い分けるのが良いと考える．
-
----
-
-## ファイルシステムにおけるスキーマ
-
-今回は，非構造化データ内であれば構造化データを扱うことが可能であることと，
-信頼性を保証したいという点から，
-スキーマレスなDBとしてのファイルシステムを考える．
-しかしながら，トランザクションの仕組みを作る上でRedBlackTreeに対し，
-キーを設定することから完全なスキーマレスとは言えない構成となる．
-
---- -->
 
 ## ファイルシステムにおけるスキーマ