Mercurial > hg > Papers > 2024 > matac-master

changeset 11:67b68982e36e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author matac42 <matac@cr.ie.u-ryukyu.ac.jp>
date Thu, 04 Jan 2024 23:54:05 +0900
parents b7abe0e40c22
children e0bcf9dbc62c
files Paper/.vscode/settings.json Paper/chapter/abstract.tex Paper/master_paper.pdf Paper/master_paper.tex Paper/reference.bib mindmaps/gears_fs_db.mm
diffstat 6 files changed, 245 insertions(+), 104 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/.vscode/settings.json	Thu Jan 04 23:54:05 2024 +0900
@@ -0,0 +1,85 @@
+{
+    // ---------- Language ----------
+
+    "[tex]": {
+        // スニペット補完中にも補完を使えるようにする
+        "editor.suggest.snippetsPreventQuickSuggestions": false,
+        // インデント幅を2にする
+        "editor.tabSize": 2
+    },
+
+    "[latex]": {
+        // スニペット補完中にも補完を使えるようにする
+        "editor.suggest.snippetsPreventQuickSuggestions": false,
+        // インデント幅を2にする
+        "editor.tabSize": 2
+    },
+
+    "[bibtex]": {
+        // インデント幅を2にする
+        "editor.tabSize": 2
+    },
+
+
+    // ---------- LaTeX Workshop ----------
+
+    // 使用パッケージのコマンドや環境の補完を有効にする
+    "latex-workshop.intellisense.package.enabled": true,
+
+    // 生成ファイルを削除するときに対象とするファイル
+    // デフォルト値に "*.synctex.gz" を追加
+    "latex-workshop.latex.autoClean.run": "onBuilt",
+    "latex-workshop.latex.clean.fileTypes": [
+        "*.aux",
+        "*.bbl",
+        "*.blg",
+        "*.idx",
+        "*.ind",
+        "*.lof",
+        "*.lot",
+        "*.out",
+        "*.toc",
+        "*.acn",
+        "*.acr",
+        "*.alg",
+        "*.glg",
+        "*.glo",
+        "*.gls",
+        "*.ist",
+        "*.fls",
+        "*.log",
+        "*.fdb_latexmk",
+        "*.snm",
+        "*.nav",
+        "*.dvi",
+        "*.ilg",
+        "*.synctex.gz"
+    ],
+
+    // 生成ファイルを現在のディレクトリに吐き出す
+    "latex-workshop.latex.outDir": "",
+
+    // ビルドのレシピ
+    "latex-workshop.latex.recipes": [
+        {
+            "name": "latexmk",
+            "tools": [
+                "latexmk"
+            ]
+        },
+    ],
+
+    // ビルドのレシピに使われるパーツ
+    "latex-workshop.latex.tools": [
+        {
+            "name": "latexmk",
+            "command": "latexmk",
+            "args": [
+                "-silent",
+                "-outdir=%OUTDIR%",
+                "%DOC%"
+            ],
+        },
+    ],
+    "latex-workshop.view.pdf.viewer": "tab",
+}
\ No newline at end of file
--- a/Paper/chapter/abstract.tex	Sat Dec 23 16:08:07 2023 +0900
+++ b/Paper/chapter/abstract.tex	Thu Jan 04 23:54:05 2024 +0900
@@ -3,8 +3,6 @@
 当研究室では，Continuation based C（CbC）を用い，定理証明やモデル検査などで信頼性を保証することを目的としたGearsOSを開発している．
 OSにおいてファイルシステムは重要な機能の一つであるため実装する必要がある．
 現在，一般的なアプリケーションはファイルシステムとデータベースを併用する形で構成される．
-DBはSQLによってデータの挿入や変更が可能だがスキーマを事前に定義し，insert時にそれらのschemaを指定する必要がある．
-GearsOSのファイルシステムではSQLの機能に相当するgrepやfindなどのインターフェースを実装し，
 アプリケーションのデータベースとしてファイルシステムを使用する構成が取れるようにしたい．
 ファイルシステムとデータベースの違いについて考え，データベースとしても利用可能なファイルシステムを構築したい．
 本研究では，ファイルシステムとデータベースの違いについて考察し，Gears OSのファイルシステムの設計について述べる．
Binary file Paper/master_paper.pdf has changed
--- a/Paper/master_paper.tex	Sat Dec 23 16:08:07 2023 +0900
+++ b/Paper/master_paper.tex	Thu Jan 04 23:54:05 2024 +0900
@@ -99,9 +99,8 @@
 
 \chapter{GearsOSにおけるファイルシステムとDB}
 
-アプリケーションの信頼性を保証することは
-情報システムやコンピュータを用いる業務の信頼性の保障につながる重要な課題である．
-したがって，アプリケーションの信頼性を保証するために，基盤となるOSの信頼性を高める必要がある．
+情報システムにおけるファイルシステムとDBは重要な要素である．
+ファイルシステムではOSが動作するための
 
 当研究室では，信頼性の保証を目的としたGearsOSを開発している．
 GearsOSは，OSの信頼性を定理証明やモデル検査を行うことで保証することを目指している\cite{modelcheck}．
@@ -233,85 +232,11 @@
 これは，教育用に開発されたx.v6\cite{xv6}をCbCで書き換える形で実装する．
 今回，ファイルシステムを実装する対象は3つ目のCbC\_xv6である．
 
-\chapter{RedBlackTreeによるファイルシステムの構成}
-
-ファイルシステムは全てRedBlackTreeで構成する．
-それにより，プログラムの証明がより簡単になるからである．
-また，ファイルシステムとDBはデータを保管するという本質的な役割は同じである．
-よって，それらはまとめてRedBlackTreeで構成する．
-
-ファイルシステムとDBの違いとして，スキーマが挙げられる．
-DBは事前にスキーマを定義し，それに沿ってデータを挿入，参照する．
-対して，ファイルシステムにはスキーマに当たるものがなく，
-データはファイルパスによって管理される．
-スキーマを定義することによってデータは構造化され，
-構造化されたデータは非構造化データと比較して，
-インデックスを作成することが容易であり，データの検索性が向上する利点がある．
-しかしながら，スキーマはDBの運用中に変更されることがあり，
-スキーマを変更した以前へロールバックができない問題がある．
-
-ロールバックがスキーマの変更によって出来なくなることは信頼性に問題があると考えると，
-スキーマを定義する必要のないスキーマレスなDBが必要になる．
-ファイルシステムはスキーマレスなDBといえるので，ファイルシステムを構築しつつ
-DBがスキーマによって実現していた機能を付け加えることを試みる．
-
-RedBlackTreeは実装によって，操作が破壊的なものとそうでないものがある．
-今回用いるのは，非破壊的な実装のRedBlackTreeである．
-図\ref{fig:TreeEdit}は非破壊的編集を行うRedBlackTreeを表している．
-編集前の木構造の6のノードをAにアップデートすることを考える．
-まず，ルートノードからアップデートしたいノード6までをコピーする．
-その後，コピーしたもののノード6をAにアップデートする．
-これにより，アップデート前のノード6を破壊することなくAにアップデートが可能である．
-参照する時は，黒のルートノードから辿れば古い6が，赤のルートノードから辿れば新しいAが見える．
-この仕組みは，データのバックアップやDBのロールバックに用いることが可能だと考える．
-
-\begin{figure}[ht]
-  \begin{center}
-      \includegraphics[width=80mm]{fig/nonDestroyTreeEdit.pdf}
-  \end{center}
-  \caption{非破壊的なTree編集}
-  \label{fig:TreeEdit}
-\end{figure}
-
-
-\chapter{ディスク上とメモリ上のデータ構造}
-
-ディスク上とメモリ上でデータの構造は，RedBlackTreeに統一する．
-一般的に，ディスク上のデータ構造としてB-Treeが用いられることが多い．
-なぜならば，HDDを用いる場合はブロックへのアクセス回数を減らしデータアクセスの時間を短くするために，
-B-Treeのようなノードを複数持つことができる構造が効果的だからである．
-その点ではRedBlackTreeはB-Treeに劣る．
-しかしながら，SSDはランダムアクセスによってデータにアクセスするため，
-RedBlackTreeでなくB-Treeを用いる利点は少ないと考える．
-よって，ディスク上とメモリ上のデータ構造をRedBlackTreeに統一することが考えられる．
-そうすることによって，ディスク上とメモリ上のデータのやりとりは単純なコピーで実装できる．
-
-\chapter{データのロールバックとバックアップ}
-
-DBの重要な機能の一つにロールバックがある．
-RDBのロールバックは，
-コミットするまではトランザクションの開始時点に戻ることができる機能を持つ．
-コミットが完了するとそれ以前の状態に戻すことはできないが，
-データのバックアップをとっておくことで復元を行う．
-このような，ロールバックとバックアップの仕組みをファイルシステムに実装したい．
-
-今回は，RedBlackTreeのルートノードがデータのバージョンの役割を果たしていることを利用し，
-データの復元が行える仕組みを構築することを考える．
-非破壊的なTree編集はアップデートのたびに，ルートノードを増やす．
-つまり，ルートノードはアップデートのログと言えその時点のデータのバージョンを表していると考えることができる．
-よって，ロールバックを行いたい場合は参照を過去のルートノードに切り替える．
-
-ルートノードはデータのアップデート時に増えるため，
-データが際限なく増加していく問題がある．
-この問題はCopyingGCを行うことによって解決する．
-まず，RedBlackTreeを丸ごとコピーして最新のルートを残して他のルートは削除する．
-その後，コピーしたものはバックアップないしログとしてディスクに書き込む．
-そうすることで，データの増加によるリソースの枯渇を防ぎ，
-かつデータのログ付きバックアップを作成することで信頼性の向上が期待できる．
-
-% TODO: バックアップのフローを図にしたい
-
-\chapter{RedBlackTreeのトランザクション}
+\chapter{GearsFileSystem}
+\section{DataGearManagerによる分散ファイルシステム}
+\section{i-nodeを用いたファイルシステム}
+\section{非破壊RedBlackTreeによる構成}
+\section{RedBlackTreeのトランザクション}
 
 トランザクションはDBの重要な機能の一つである．
 データの競合を防ぎ信頼性を向上させ，DBとしても扱えるよう
@@ -359,8 +284,101 @@
 しかし，常に最新の情報を読み込めるとは限らない．
 最新の情報が欲しい場合は書き込みを一旦止めるような処理が必要になる．
 
+\section{ディスク上とメモリ上のデータ構造}
 
-\chapter{ファイルシステムにおけるスキーマ}
+
+ファイルシステムは全てRedBlackTreeで構成する．
+それにより，プログラムの証明がより簡単になるからである．
+また，ファイルシステムとDBはデータを保管するという本質的な役割は同じである．
+よって，それらはまとめてRedBlackTreeで構成する．
+
+ファイルシステムとDBの違いとして，スキーマが挙げられる．
+DBは事前にスキーマを定義し，それに沿ってデータを挿入，参照する．
+対して，ファイルシステムにはスキーマに当たるものがなく，
+データはファイルパスによって管理される．
+スキーマを定義することによってデータは構造化され，
+構造化されたデータは非構造化データと比較して，
+インデックスを作成することが容易であり，データの検索性が向上する利点がある．
+しかしながら，スキーマはDBの運用中に変更されることがあり，
+スキーマを変更した以前へロールバックができない問題がある．
+
+ロールバックがスキーマの変更によって出来なくなることは信頼性に問題があると考えると，
+スキーマを定義する必要のないスキーマレスなDBが必要になる．
+ファイルシステムはスキーマレスなDBといえるので，ファイルシステムを構築しつつ
+DBがスキーマによって実現していた機能を付け加えることを試みる．
+
+RedBlackTreeは実装によって，操作が破壊的なものとそうでないものがある．
+今回用いるのは，非破壊的な実装のRedBlackTreeである．
+図\ref{fig:TreeEdit}は非破壊的編集を行うRedBlackTreeを表している．
+編集前の木構造の6のノードをAにアップデートすることを考える．
+まず，ルートノードからアップデートしたいノード6までをコピーする．
+その後，コピーしたもののノード6をAにアップデートする．
+これにより，アップデート前のノード6を破壊することなくAにアップデートが可能である．
+参照する時は，黒のルートノードから辿れば古い6が，赤のルートノードから辿れば新しいAが見える．
+この仕組みは，データのバックアップやDBのロールバックに用いることが可能だと考える．
+
+\begin{figure}[ht]
+  \begin{center}
+      \includegraphics[width=80mm]{fig/nonDestroyTreeEdit.pdf}
+  \end{center}
+  \caption{非破壊的なTree編集}
+  \label{fig:TreeEdit}
+\end{figure}
+
+
+\chapter{GearsFileSystemにおけるGCとレプリケーションの仕組み}
+\section{CopyRedBlackTreeによるGCの仕組み}
+\section{CopyRedBlackTreeによるレプリケーションの仕組み}
+
+ディスク上とメモリ上でデータの構造は，RedBlackTreeに統一する．
+一般的に，ディスク上のデータ構造としてB-Treeが用いられることが多い．
+なぜならば，HDDを用いる場合はブロックへのアクセス回数を減らしデータアクセスの時間を短くするために，
+B-Treeのようなノードを複数持つことができる構造が効果的だからである．
+その点ではRedBlackTreeはB-Treeに劣る．
+しかしながら，SSDはランダムアクセスによってデータにアクセスするため，
+RedBlackTreeでなくB-Treeを用いる利点は少ないと考える．
+よって，ディスク上とメモリ上のデータ構造をRedBlackTreeに統一することが考えられる．
+そうすることによって，ディスク上とメモリ上のデータのやりとりは単純なコピーで実装できる．
+
+\chapter{CopyRedBlackTreeの実装}
+\section{コピーのアルゴリズム}
+\section{Stackの使用に関して}
+\section{証明のしやすさについて}
+
+
+DBの重要な機能の一つにロールバックがある．
+RDBのロールバックは，
+コミットするまではトランザクションの開始時点に戻ることができる機能を持つ．
+コミットが完了するとそれ以前の状態に戻すことはできないが，
+データのバックアップをとっておくことで復元を行う．
+このような，ロールバックとバックアップの仕組みをファイルシステムに実装したい．
+
+今回は，RedBlackTreeのルートノードがデータのバージョンの役割を果たしていることを利用し，
+データの復元が行える仕組みを構築することを考える．
+非破壊的なTree編集はアップデートのたびに，ルートノードを増やす．
+つまり，ルートノードはアップデートのログと言えその時点のデータのバージョンを表していると考えることができる．
+よって，ロールバックを行いたい場合は参照を過去のルートノードに切り替える．
+
+ルートノードはデータのアップデート時に増えるため，
+データが際限なく増加していく問題がある．
+この問題はCopyingGCを行うことによって解決する．
+まず，RedBlackTreeを丸ごとコピーして最新のルートを残して他のルートは削除する．
+その後，コピーしたものはバックアップないしログとしてディスクに書き込む．
+そうすることで，データの増加によるリソースの枯渇を防ぎ，
+かつデータのログ付きバックアップを作成することで信頼性の向上が期待できる．
+
+% TODO: バックアップのフローを図にしたい
+
+
+\chapter{まとめと今後の課題}
+
+本論文ではGearsOSのファイルシステムとDBの設計について説明した．
+今後，実装を行いながら設計と動作の確認，計測を行い，
+設計の意図が反映されていることやプログラムの検証ができることを確認する必要がある．
+
+また，今後の課題や議題として次のようなものが挙げられる．
+
+\section{ファイルシステムにおけるスキーマ}
 
 従来のRDBのようなスキーマが存在すると，
 個別にバックアップなどを取らない限り
@@ -390,22 +408,13 @@
 DataGearはKernelのContextからプロセスのContextを経由して全て繋がっている．
 よって，KernelのContext上にキーを用いたDataGearの参照を書き込む．
 
-\chapter{RedBlackTreeによる権限の表現}
+\section{RedBlackTreeによる権限の表現}
 
 ファイルの権限はファイルシステムの重要な機能の一つであるため実装する必要がある．
 今回のRedBlackTreeによる構成の場合，木のルートの所持者を設定することが
 ファイルに対して権限を設定することにあたる．
 ルートに対してアクセスする権限がなければ，
 読み書きができないといった実装になると考える．
-
-\chapter{まとめと今後の課題}
-
-本論文ではGearsOSのファイルシステムとDBの設計について説明した．
-今後，実装を行いながら設計と動作の確認，計測を行い，
-設計の意図が反映されていることやプログラムの検証ができることを確認する必要がある．
-
-また，今後の課題や議題として次のようなものが挙げられる．
-
 \section{データクエリ言語}
 
 ユーザーやアプリケーションがDBのデータにアクセスするための言語設計を
--- a/Paper/reference.bib	Sat Dec 23 16:08:07 2023 +0900
+++ b/Paper/reference.bib	Thu Jan 04 23:54:05 2024 +0900
@@ -105,4 +105,22 @@
   journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
   month   = {May},
   year    = 2022
+}
+
+@misc{zengin,
+  title        = {全国銀行データ通信システムの障害について},
+  author       = {一般社団法人 全国銀行資金決済ネットワーク},
+  howpublished = {https://www.zengin-net.jp/announcement/pdf/announcement\_20231201.pdf}
+}
+
+@misc{ana,
+  title        = {4月3日に発生した国内線システム不具合の原因及び再発防止策について},
+  author       = {全日本空輸株式会社},
+  howpublished = {https://www.anahd.co.jp/group/pr/202304/notification-2.html}
+}
+
+@misc{glory,
+  title        = {2月14日から2月19日にかけて発生した電子マネー決済システム（iD決済）の障害に関するお詫びとお知らせ},
+  author       = {グローリー株式会社},
+  howpublished = {https://www.glory.co.jp/news/detail/id=2017}
 }
\ No newline at end of file
--- a/mindmaps/gears_fs_db.mm	Sat Dec 23 16:08:07 2023 +0900
+++ b/mindmaps/gears_fs_db.mm	Thu Jan 04 23:54:05 2024 +0900
@@ -348,8 +348,37 @@
 <node TEXT="評価方法" POSITION="right" ID="ID_1979397312" CREATED="1699850131177" MODIFIED="1699850137060"/>
 <node TEXT="章立て" POSITION="left" ID="ID_378600647" CREATED="1699848424709" MODIFIED="1702112473403">
 <node TEXT="Gears OSのファイルシステムとDB" ID="ID_446325287" CREATED="1701690660393" MODIFIED="1701690902283">
-<node TEXT="システム全体の信頼性を上げたい" ID="ID_1572843196" CREATED="1703313460915" MODIFIED="1703313713692"/>
-<node TEXT="ファイルシステムとDBの信頼性を考える" ID="ID_1355454563" CREATED="1703313715002" MODIFIED="1703313723643"/>
+<node TEXT="重要なシステムの障害" ID="ID_780032066" CREATED="1704365424619" MODIFIED="1704365554685">
+<node TEXT="例" ID="ID_561763413" CREATED="1704365743851" MODIFIED="1704365747240">
+<node TEXT="全銀システム" ID="ID_380458549" CREATED="1704365488518" MODIFIED="1704365500548">
+<node TEXT="https://www.zengin-net.jp/announcement/pdf/announcement_20231201.pdf" ID="ID_622498163" CREATED="1704365947486" MODIFIED="1704365947486" LINK="https://www.zengin-net.jp/announcement/pdf/announcement_20231201.pdf"/>
+</node>
+<node TEXT="ANAの国内線システム" ID="ID_227546985" CREATED="1704365556083" MODIFIED="1704366884696">
+<node TEXT="https://www.anahd.co.jp/group/pr/202304/notification-2.html?_gl=1*1h2jfg0*_ga*MTkwMjE0OTIwNC4xNjgwOTIwMTUx*_ga_32F297W9WL*MTY4MDkyMDI2My4xLjEuMTY4MDkyMDMwNy4wLjAuMA.." ID="ID_918028332" CREATED="1704366735088" MODIFIED="1704366735088" LINK="https://www.anahd.co.jp/group/pr/202304/notification-2.html?_gl=1*1h2jfg0*_ga*MTkwMjE0OTIwNC4xNjgwOTIwMTUx*_ga_32F297W9WL*MTY4MDkyMDI2My4xLjEuMTY4MDkyMDMwNy4wLjAuMA.."/>
+</node>
+<node TEXT="電子決済システム" ID="ID_271892958" CREATED="1704365579825" MODIFIED="1704366979311">
+<node TEXT="https://www.glory.co.jp/news/detail/id=2017" ID="ID_650733639" CREATED="1704367245326" MODIFIED="1704367245326" LINK="https://www.glory.co.jp/news/detail/id=2017"/>
+</node>
+</node>
+<node TEXT="これらは社会に多大な影響を与える" ID="ID_1496226551" CREATED="1704365759256" MODIFIED="1704365779957"/>
+<node TEXT="よってシステムの高い信頼性が求められる" ID="ID_1365357344" CREATED="1704365780499" MODIFIED="1704365831219"/>
+</node>
+<node TEXT="システム全体の信頼性を上げたい" ID="ID_1572843196" CREATED="1703313460915" MODIFIED="1703313713692">
+<node TEXT="システムにあるさまざまな要素" ID="ID_1198542652" CREATED="1704365155193" MODIFIED="1704365166358">
+<node TEXT="アプリケーション" ID="ID_727581223" CREATED="1704365166793" MODIFIED="1704365223650"/>
+<node TEXT="OS" ID="ID_1417760159" CREATED="1704365224002" MODIFIED="1704365225602"/>
+<node TEXT="ファイルシステム" ID="ID_153728143" CREATED="1704365226160" MODIFIED="1704365231311"/>
+<node TEXT="DB" ID="ID_323366858" CREATED="1704365231782" MODIFIED="1704365232994"/>
+<node TEXT="メモリ" ID="ID_402756754" CREATED="1704365233331" MODIFIED="1704365236964"/>
+<node TEXT="SSD" ID="ID_404429414" CREATED="1704365237202" MODIFIED="1704365243718"/>
+<node TEXT="分散ノード" ID="ID_1628174426" CREATED="1704365244457" MODIFIED="1704365249457"/>
+<node TEXT="ネットワーク" ID="ID_1337491308" CREATED="1704365250196" MODIFIED="1704365253472"/>
+</node>
+<node TEXT="全体の信頼性を上げる必要がある" ID="ID_355799274" CREATED="1704365894036" MODIFIED="1704365915131"/>
+</node>
+<node TEXT="ファイルシステムとDBの信頼性を考える" ID="ID_1355454563" CREATED="1703313715002" MODIFIED="1703313723643">
+<node TEXT="システムにおいて重要なFSとDBの信頼性を保証したい" ID="ID_1811829647" CREATED="1704365294814" MODIFIED="1704365332688"/>
+</node>
 <node TEXT="ファイルシステムとは" ID="ID_1898416034" CREATED="1703313727821" MODIFIED="1703313734372"/>
 <node TEXT="DBとは" ID="ID_101598045" CREATED="1703313734729" MODIFIED="1703313737449"/>
 <node TEXT="ファイルシステムとDBの違い" ID="ID_1786247161" CREATED="1703313740484" MODIFIED="1703313748867"/>
@@ -379,18 +408,20 @@
 </node>
 <node TEXT="GearsFileSystem" ID="ID_667012992" CREATED="1701694178540" MODIFIED="1701694184160">
 <node TEXT="DataGearManagerによる分散ファイルシステム" ID="ID_540180010" CREATED="1703315001066" MODIFIED="1703315085575"/>
+<node TEXT="i-nodeを用いたファイルシステム" ID="ID_1851664363" CREATED="1703314946289" MODIFIED="1703492949059"/>
 <node TEXT="非破壊RedBlackTreeによる構成" ID="ID_262332331" CREATED="1701696133124" MODIFIED="1701696237170"/>
-<node TEXT="RedBlackTreeによるファイルシステム" ID="ID_1851664363" CREATED="1703314946289" MODIFIED="1703314992580"/>
-<node TEXT="ディスク上とメモリ上のデータ構造" ID="ID_880200197" CREATED="1703314889974" MODIFIED="1703314930213"/>
 <node TEXT="RedBlackTreeのトランザクション" ID="ID_1088328123" CREATED="1701696247760" MODIFIED="1702112463420" HGAP_QUANTITY="14.75 pt" VSHIFT_QUANTITY="3.75 pt"/>
+<node TEXT="ディスク上とメモリ上のデータ構造" ID="ID_683338430" CREATED="1701696165502" MODIFIED="1701696179372"/>
 </node>
 <node TEXT="GearsFileSystemにおけるGCとレプリケーションの仕組み" ID="ID_1092227909" CREATED="1701690558237" MODIFIED="1702112470212" HGAP_QUANTITY="16.25 pt" VSHIFT_QUANTITY="-1.5 pt">
-<node TEXT="ディスク上とメモリ上のデータ構造" ID="ID_683338430" CREATED="1701696165502" MODIFIED="1701696179372"/>
-<node TEXT="データのバックアップ" ID="ID_441653952" CREATED="1701696184549" MODIFIED="1701696189276"/>
-<node TEXT="レプリケーション" ID="ID_243135333" CREATED="1701696193660" MODIFIED="1702112458875" VSHIFT_QUANTITY="-0.75 pt"/>
-<node TEXT="ガベージコレクション" ID="ID_694714867" CREATED="1701696212033" MODIFIED="1701696219728"/>
+<node TEXT="CopyRedBlackTreeによるGCの仕組み" ID="ID_694714867" CREATED="1701696212033" MODIFIED="1703491006779"/>
+<node TEXT="CopyRedBlackTreeによるレプリケーションの仕組み" ID="ID_1106336919" CREATED="1703490971550" MODIFIED="1703491035629"/>
 </node>
-<node TEXT="実装?" ID="ID_1619882257" CREATED="1701697553803" MODIFIED="1702112473403" VSHIFT_QUANTITY="-4.5 pt"/>
+<node TEXT="CopyRedBlackTreeの実装" ID="ID_1619882257" CREATED="1701697553803" MODIFIED="1703491075408" VSHIFT_QUANTITY="-4.5 pt">
+<node TEXT="コピーのアルゴリズム" ID="ID_64994373" CREATED="1703491215841" MODIFIED="1703491223454"/>
+<node TEXT="Stackの使用に関して" ID="ID_432827984" CREATED="1703492856041" MODIFIED="1703492863503"/>
+<node TEXT="証明のしやすさについて" ID="ID_2776247" CREATED="1703492904417" MODIFIED="1703492910899"/>
+</node>
 <node TEXT="信頼性" ID="ID_1221084016" CREATED="1702289777950" MODIFIED="1702289781581">
 <node TEXT="モデル検査とAgdaによる実装" ID="ID_1438858883" CREATED="1702289781790" MODIFIED="1702289794818"/>
 </node>