--- a/marp-slide/slide.md	Tue Feb 13 20:25:58 2024 +0900
+++ b/marp-slide/slide.md	Wed Feb 14 09:44:07 2024 +0900
@@ -110,7 +110,7 @@
   - find完了、insert証明中
 - GearsOSの構造はRedBlackTreeが多くを占める
 
-GearsAgdaでRedBlackTreeが証明できれば、GearsOSの大部分を証明したことになる
+GearsAgdaでRedBlackTreeが証明できれば、GearsOSのファイルシステムの大部分を証明したことになる
 
 ---
 
@@ -149,8 +149,11 @@
 
 ## メモリ管理や多重性の機能がない
 
+<!-- それぞれが何のためにあるのか説明する感じでやると良い -->
+
 メモリ管理
 
+- アロケーション
 - GC(ガベージコレクション)
 
 多重性
@@ -163,24 +166,46 @@
 
 ## メモリ管理や多重性の機能の要件
 
+<!-- 照明のしやすさの維持が唐突な感じ
+動作の正しさがわかりやすい実装で証明しやすく -->
+
+- 信頼性を上げたい
+  - 証明のしやすい実装
 - データの持続性
-  - 証明のしやすさの維持
-  - データを破壊しない
-- 非破壊RedBlackTreeの増大抑制
+  - 持続性のあるストレージにちゃんとコピーする
+  - 適切なタイミングでコピーを行う
+- 非破壊RedBlackTreeのメモリ管理
   - 非破壊RedBlackTreeは履歴を全て持つ
-  - そのままにすると増大し、メモリを圧迫する
+  - 過去の履歴分のメモリを解放する必要がある
 
 ---
 
 ## GearsOSにおけるGC
-
+<!--  -->
 CopyingGCを採用する
+- 新しいContextのメモリに新規にコピーする
+- 古いContextをそのまま全部解放する
 
 ---
 
 ## GearsOSにおけるレプリケーション
 
+<!--  -->
+
 単純に木をコピーする
+複数のストレージに同時に木を置く
+そのうちの一部は持続的なストレージにする
+システム起動時には必要な分をメモリにコピーする
+
+トランザクションも考慮する
+
+---
+
+## RedBlackTreeのトランザクション
+
+- 木のルートのすげ替えがトランザクションになる
+- read
+- write
 
 ---
 
@@ -233,13 +258,19 @@
 課題点
   同一Contextへコピーしている
 コピーの正しさ
-
+Stack使っているので余計なメモリを消費する
+Stackも非破壊であるという問題がある
+-> 証明しやすさを優先しているから
+Stackが非破壊である意味があまりない？のでここを破壊でやる。
 
 ---
 
 ## 今後の研究方針
 
 別Contextコピー
+GearsAgdaでの記述
+Stack領域の圧縮
+- Stackの再利用？
 GC，レプリケーションの実装
 多重性以外の機能
 
@@ -247,7 +278,7 @@
 
 ## まとめ
 
-copyRedBlackTreeを実装した
-それにより多重性を確保できるようになった
-多重性はシステムの信頼性を向上させる
-非破壊RedBlackTreeの増大抑制により実用的なシステム構築が可能になった
+- copyRedBlackTreeを実装した
+- それにより多重性を確保できるようになった
+- 多重性はシステムの信頼性を向上させる
+- 非破壊RedBlackTreeの増大抑制により実用的なシステム構築が可能になった