Mercurial > hg > Papers > 2024 > matac-master

--- a/Paper/chapter/appendix.tex	Thu Feb 15 22:50:21 2024 +0900
+++ b/Paper/chapter/appendix.tex	Wed Feb 28 12:47:59 2024 +0900
@@ -1,8 +1,11 @@
 \appendix
-\chapter{研究会業績}
+\chapter{研究関連資料}

 \section{研究会発表資料}
 \begin{itemize}
   \item GearsOSにおけるinodeを用いたファイルシステムの構築 又吉 雄斗, 河野 真治 情報処理会 システムソフトウェアとオペレーティング・システム研究会（OS）, May, 2022
   \item Gears OSのファイルシステムとDB 又吉 雄斗, 佐野 巧曜, 河野 真治 情報処理会 システムソフトウェアとオペレーティング・システム研究会（OS）, May, 2023
 \end{itemize}
+
+\section{CopyRedBlackTreeソースコード}
+\lstinputlisting[label=src:swap.cbc]{src/CopyRedBlackTree.cbc}
\ No newline at end of file
--- a/Paper/chapter/thanks.tex	Thu Feb 15 22:50:21 2024 +0900
+++ b/Paper/chapter/thanks.tex	Wed Feb 28 12:47:59 2024 +0900
@@ -1,8 +1,10 @@
 \chapter*{謝辞}
 \addcontentsline{toc}{chapter}{謝辞}
 本研究を行うにあたりご多忙にも関わらず日頃より多くのご助言，ご指導をいただきました河野真治准教授に心より感謝いたします。
-また，学士時代に研究に対する意見，実装，実験に協力いただいた研究室OBの一木貴裕さんや，
-研究室の同期としてともに研究の遂行をしてくださった木山瑞基をはじめとする並列信頼研究室の皆さまに感謝いたします。
+また，学士時代に研究に対する意見，実装，実験にご協力いただいた研究室OBの一木貴裕さん，
+研究室の同期としてともに研究の遂行をしてくださった木山瑞基さん，
+DBについて一緒に考えてくださった佐野巧曜さんをはじめとする並列信頼研究室の皆さま，
+友人として研究を遂行するにあたり心を支えて下さった中井奎太朗さんに感謝いたします．
 最後に，長年に渡り理解を示し，支援してくださった家族に感謝いたします。

 \begin{flushright}
--- a/Paper/master_paper.lol	Thu Feb 15 22:50:21 2024 +0900
+++ b/Paper/master_paper.lol	Wed Feb 28 12:47:59 2024 +0900
@@ -14,3 +14,4 @@
 \contentsline {lstlisting}{\numberline {6.3}leftDown1 CodeGear(アロケーション部分の例)}{36}{}%
 \contentsline {lstlisting}{\numberline {6.4}ビルド時に生成されたALLOCATE部分}{37}{}%
 \contentsline {lstlisting}{\numberline {6.5}swap2 CodeGear(木の入れ替え処理部分)}{38}{}%
+\contentsline {lstlisting}{src/CopyRedBlackTree.cbc}{48}{}%
Binary file Paper/master_paper.pdf has changed
--- a/Paper/master_paper.tex	Thu Feb 15 22:50:21 2024 +0900
+++ b/Paper/master_paper.tex	Wed Feb 28 12:47:59 2024 +0900
@@ -104,7 +104,7 @@
 これらの一つ一つに対する厳密な検証が，全体としての堅牢性を高めることに繋がる．

 当研究室では，信頼性の保証を目的としたGearsOSを開発しており，
-定理証明やモデル検査などの形式手法を用いて信頼性を保証できることを目標としている．\cite{modelcheck}．
+定理証明やモデル検査などの形式手法を用いて信頼性を保証できることを目標としている\cite{modelcheck}．
 一般的にソフトウェアの動作を検証する手法としてテストコードを用いることが挙げられる．
 しかしながら，OSなどの大規模なソフトウェアにおいて人力で記述するテストコードのみでは
 カバレッジが不十分であり，検証漏れが発生する可能性がある．
@@ -792,7 +792,6 @@
 レプリケーションを実装する際の通信の仕組みについて考える必要がある．
 データの送受信はDataGearManagerのSocket通信の仕組みを使うことが考えられる．

-既存のDBにおけるレプリケーション手法は同期のタイミングやレプリカの作成単位によっていくつか種類がある．

 \section{コピー実行のタイミング}

@@ -827,12 +826,7 @@
 CodeGearは遷移先のCodeGearの参照を持つ必要があるため，
 inputDataGearとしてnextとwhenEmptyを渡している．
 条件分岐は通常のif文で行われ，条件ごとに次のCodeGearを指定している．
-
 このようにして，条件分岐をして実行するCodeGearを切り替えることができる．
-しかし，GCは本来行いたい処理ではなくメタレベルの処理である．
-そのため，GCへの切り替えにおいてソースコード\ref{src:isEmpty.cbc}のようなコードを記述すると，
-ノーマルレベルとメタレベルが混在するCodeGearとなる問題がある．
-これは，GC処理を自動的に % TODO

 \section{別Contextへのコピー}

@@ -1091,6 +1085,13 @@
 また，GearsOS全体をGCすることも考えられる．
 レプリケーションは別ノードでのコピーの実行やレプリカとの通信プロトコルを定義する必要があるだろう．

+\section{形式手法による信頼性の検証}
+
+Stack領域の圧縮と再利用の仕組み，別Contextへのコピーを実装した後は，
+モデル検査で並行実行下で正しく動くことをメモリアロケーション部分を含めて調べたい．
+また，GearsAgdaに変換，もしくは記述を行い，定理証明によって並列実行下で正しく動くか，
+メモリが正しく開放されているかどうかを検証したい．
+
 \section{その他ファイルシステムの信頼性に関する機能}

 今回は木のコピーによる多重度の確保を主に扱った．
--- a/Paper/src/CopyRedBlackTree.cbc	Thu Feb 15 22:50:21 2024 +0900
+++ b/Paper/src/CopyRedBlackTree.cbc	Wed Feb 28 12:47:59 2024 +0900
@@ -5,7 +5,7 @@
     tree->copied = 0;

     struct Stack* toStack = tree->toStack;
-    struct Node* newNode = &ALLOCATE(context, Node)->Node;
+    struct Node* newNode = new Node();
     newNode->key = tree->current->key;
     newNode->value = (union Data*)new Integer();
     ((Integer*)newNode->value)->value = ((Integer*)tree->current->value)->value;
@@ -19,7 +19,6 @@
 // current->leftがある場合、コピーしてから降りる。
 //   ない場合はrightを見に行く(rightDown)
 //
-
 __code leftDown(struct RedBlackTree* tree) {
     printf("leftDown\n");
     struct Stack* toStack = tree->toStack;
@@ -35,7 +34,7 @@
     }

     struct Stack* toStack = tree->toStack;
-    struct Node* newNode = &ALLOCATE(context, Node)->Node;
+    struct Node* newNode = new Node();
     struct Node* data = (Node*)(stack->data);
     newNode->key = tree->current->left->key;
     newNode->value = (union Data*)new Integer();
@@ -107,12 +106,16 @@
 __code rightDown1(struct RedBlackTree* tree, struct Stack* stack) {
     printf("rightDown1\n");

+    if (tree->current == NULL) {
+        goto swap();
+    }
+
     if (tree->current->right == NULL) {
         goto up();
     }

     struct Stack* toStack = tree->toStack;
-    struct Node* newNode = &ALLOCATE(context, Node)->Node;
+    struct Node* newNode = new Node();
     struct Node* data = (Node*)(stack->data);
     newNode->key = tree->current->right->key;
     newNode->value = (union Data*)new Integer();
@@ -169,6 +172,9 @@
     if (tree->current == NULL) {
         goto swap(tree);
     }
+    if (tree->current == tree->root) {
+        goto swap(tree);
+    }

     goto toStack->pop(up2);
 }
@@ -179,8 +185,6 @@
     struct Stack* toStack = tree->toStack;

     if (tree->current->right) {
-        // toStackのtopにrightがあればup(すでにコピー済みなので)
-        // それがNULLならup3(rightDown)(そこからupしてきたのでNULLであるということはまだコピーできていないということになる(leftからのupをしたということ))
         goto up4(tree);
     }
--- a/TODO.md	Thu Feb 15 22:50:21 2024 +0900
+++ b/TODO.md	Wed Feb 28 12:47:59 2024 +0900
@@ -46,5 +46,5 @@
 - [x] 信頼性とどうつながるかを言及する
 - [x] LFSへ言及する
 - [x] 今後の課題追加
-- [ ] GearsAgdaのことを書く(何を書く？)
-- [ ] Filesystem Fragmentation
+- [x] GearsAgdaのことを書く(何を書く？)
+- [x] Filesystem Fragmentation
\ No newline at end of file
Binary file marp-slide/slide.pdf has changed
--- a/mindmaps/gears_fs_db.mm	Thu Feb 15 22:50:21 2024 +0900
+++ b/mindmaps/gears_fs_db.mm	Wed Feb 28 12:47:59 2024 +0900
@@ -2,7 +2,7 @@
 <!--To view this file, download free mind mapping software Freeplane from https://www.freeplane.org -->
 <node TEXT="GearsOS上のファイルシステムとDBの信頼性(仮)" FOLDED="false" ID="ID_452131666" CREATED="1610381621610" MODIFIED="1707981795106" STYLE="oval">
 <font SIZE="18"/>
-<hook NAME="MapStyle" zoom="0.8">
+<hook NAME="MapStyle" zoom="0.25">
     <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>
@@ -68,7 +68,7 @@
 </stylenode>
 </map_styles>
 </hook>
-<node TEXT="Gears OS" FOLDED="true" POSITION="right" ID="ID_1060626979" CREATED="1699848393025" MODIFIED="1702111913149" HGAP_QUANTITY="-5.5 pt" VSHIFT_QUANTITY="-72.75 pt">
+<node TEXT="Gears OS" POSITION="right" ID="ID_1060626979" CREATED="1699848393025" MODIFIED="1702111913149" HGAP_QUANTITY="-5.5 pt" VSHIFT_QUANTITY="-72.75 pt">
 <node TEXT="特徴" ID="ID_943482341" CREATED="1702111230723" MODIFIED="1702111233987">
 <node TEXT="metaGear" ID="ID_160728835" CREATED="1702111234234" MODIFIED="1702111815711">
 <node TEXT="データの整合性" ID="ID_1532293232" CREATED="1702111816103" MODIFIED="1702111830986"/>
@@ -283,7 +283,7 @@
 </node>
 <node TEXT="向上手法をシステム全体に適用したい" ID="ID_829551002" CREATED="1699850006058" MODIFIED="1699850017727"/>
 </node>
-<node TEXT="RedBlackTree" FOLDED="true" POSITION="right" ID="ID_858040690" CREATED="1699848437129" MODIFIED="1699848446060">
+<node TEXT="RedBlackTree" POSITION="right" ID="ID_858040690" CREATED="1699848437129" MODIFIED="1699848446060">
 <node TEXT="Copy" ID="ID_76598812" CREATED="1699848476363" MODIFIED="1699848479936">
 <node TEXT="単なる2分木のコピー" ID="ID_1535596989" CREATED="1699849455588" MODIFIED="1699849469353"/>
 <node TEXT="Stack無しで書くとおそらく結構複雑" ID="ID_527329681" CREATED="1699849470075" MODIFIED="1699857892247"/>
@@ -434,7 +434,7 @@
 <node TEXT="評価方法" POSITION="right" ID="ID_1979397312" CREATED="1699850131177" MODIFIED="1699850137060"/>
 <node TEXT="erasure coding" POSITION="right" ID="ID_1412038732" CREATED="1706607173301" MODIFIED="1706607177606"/>
 <node TEXT="章立て" POSITION="left" ID="ID_378600647" CREATED="1699848424709" MODIFIED="1706520588455" HGAP_QUANTITY="8 pt" VSHIFT_QUANTITY="-117 pt">
-<node TEXT="要旨" FOLDED="true" ID="ID_1862870052" CREATED="1705571598152" MODIFIED="1705571620770">
+<node TEXT="要旨" ID="ID_1862870052" CREATED="1705571598152" MODIFIED="1705571620770">
 <node TEXT="CbCでGearsOSを開発している" ID="ID_1596447160" CREATED="1705571621398" MODIFIED="1705571639432"/>
 <node TEXT="OSの重要な機能の一つにファイルシステムがある" ID="ID_1812705807" CREATED="1705571640078" MODIFIED="1705571676397">
 <node TEXT="プロセス管理やデータの保持" ID="ID_1002371513" CREATED="1705636979706" MODIFIED="1705636992169"/>
@@ -523,11 +523,11 @@
 <node TEXT="Gears OS" ID="ID_1367848198" CREATED="1705044112079" MODIFIED="1705044114581"/>
 <node TEXT="CbC_x.v6" ID="ID_323899306" CREATED="1705044116042" MODIFIED="1705044124351"/>
 </node>
-<node TEXT="メタ処理を記述するmetaGear" FOLDED="true" ID="ID_1666892566" CREATED="1703309692742" MODIFIED="1703309713823">
+<node TEXT="メタ処理を記述するmetaGear" ID="ID_1666892566" CREATED="1703309692742" MODIFIED="1703309713823">
 <node TEXT="ノーマルレベルとメタレベルの切り分け" ID="ID_719507396" CREATED="1703308470210" MODIFIED="1703308478844"/>
 <node TEXT="CbCによって容易に切り分け可能" ID="ID_1803106515" CREATED="1704785297162" MODIFIED="1704785306308"/>
 </node>
-<node TEXT="全てのGearを参照するContext" FOLDED="true" ID="ID_91888278" CREATED="1703309731224" MODIFIED="1705052148391">
+<node TEXT="全てのGearを参照するContext" ID="ID_91888278" CREATED="1703309731224" MODIFIED="1705052148391">
 <node TEXT="全てのCodeGear, DataGearの参照を持つ" ID="ID_816175749" CREATED="1704777710835" MODIFIED="1704777722631"/>
 <node TEXT="従来OSのプロセスに相当する概念" ID="ID_485427631" CREATED="1704777731086" MODIFIED="1704777739954"/>
 <node TEXT="Contextにも種類がある" ID="ID_309360319" CREATED="1704787077056" MODIFIED="1704787082791"/>
@@ -540,7 +540,7 @@
 </node>
 <node TEXT="Contextを含めたGear遷移" ID="ID_1897519980" CREATED="1704779305504" MODIFIED="1704779324312"/>
 </node>
-<node TEXT="モジュール化の仕組みinterface" FOLDED="true" ID="ID_979914453" CREATED="1705044283721" MODIFIED="1705045105599">
+<node TEXT="モジュール化の仕組みinterface" ID="ID_979914453" CREATED="1705044283721" MODIFIED="1705045105599">
 <node TEXT="モジュール化の仕組み" ID="ID_1323690074" CREATED="1705044424301" MODIFIED="1705044435039">
 <node TEXT="Javaのクラスのような仕組み" ID="ID_515246380" CREATED="1705044987112" MODIFIED="1705045006109"/>
 <node TEXT="使用するDGとCGをまとめる" ID="ID_1867289776" CREATED="1705045011571" MODIFIED="1705045022968"/>
@@ -605,14 +605,14 @@
 </node>
 </node>
 <node TEXT="GearsFileSystemにおけるGCとレプリケーション" ID="ID_1092227909" CREATED="1701690558237" MODIFIED="1705569492385" HGAP_QUANTITY="16.25 pt" VSHIFT_QUANTITY="-1.5 pt">
-<node TEXT="ファイルシステムの信頼性" FOLDED="true" ID="ID_200982245" CREATED="1704630258973" MODIFIED="1706091519737">
+<node TEXT="ファイルシステムの信頼性" ID="ID_200982245" CREATED="1704630258973" MODIFIED="1706091519737">
 <node TEXT="信頼性に関する追加機能" ID="ID_1574949535" CREATED="1704630312069" MODIFIED="1704630320377"/>
 <node TEXT="GCやレプリケーションの機能がない" ID="ID_878946385" CREATED="1704630323433" MODIFIED="1704632961588"/>
 <node TEXT="実装するためにはデータのCopyが必要" ID="ID_822351907" CREATED="1704630337081" MODIFIED="1706091519737"/>
 <node TEXT="現状はTreeにCopyがない" ID="ID_65833123" CREATED="1704630383271" MODIFIED="1704630397371"/>
 <node TEXT="Copyを実装したい" ID="ID_1314300132" CREATED="1704632535428" MODIFIED="1704632976417"/>
 </node>
-<node TEXT="GCの種類" FOLDED="true" ID="ID_1746770811" CREATED="1704695739812" MODIFIED="1706686162814">
+<node TEXT="GCの種類" ID="ID_1746770811" CREATED="1704695739812" MODIFIED="1706686162814">
 <node TEXT="CopyingGCとは" ID="ID_344664264" CREATED="1704692777863" MODIFIED="1704692782352">
 <node TEXT="正確なGC" ID="ID_267216671" CREATED="1704696904268" MODIFIED="1704696908732"/>
 <node TEXT="ヒープ領域をFrom領域とTo領域に分割" ID="ID_1262852949" CREATED="1704711856815" MODIFIED="1704711932146"/>
@@ -633,7 +633,7 @@
 </node>
 </node>
 </node>
-<node TEXT="GCは併用される" FOLDED="true" ID="ID_1496671439" CREATED="1704696631667" MODIFIED="1704696640285">
+<node TEXT="GCは併用される" ID="ID_1496671439" CREATED="1704696631667" MODIFIED="1704696640285">
 <node TEXT="一般的にGCは組み合わせで使われる" ID="ID_1275851809" CREATED="1704776562321" MODIFIED="1704776594813"/>
 <node TEXT="例えば世代別GC" ID="ID_1572156993" CREATED="1704776595339" MODIFIED="1704776711350"/>
 <node TEXT="メジャーGCでMark &amp; Sweep GC" ID="ID_118548516" CREATED="1704776713708" MODIFIED="1704776746730"/>
@@ -641,7 +641,7 @@
 <node TEXT="それぞれのGCの利点を享受できる" ID="ID_704438541" CREATED="1704776762298" MODIFIED="1704776776709"/>
 </node>
 <node TEXT="Rustのスマートポインタ" ID="ID_881149259" CREATED="1704696608959" MODIFIED="1704696615328"/>
-<node TEXT="CopyingGCを用いる" FOLDED="true" ID="ID_1639428535" CREATED="1704692768575" MODIFIED="1705569492385">
+<node TEXT="CopyingGCを用いる" ID="ID_1639428535" CREATED="1704692768575" MODIFIED="1705569492385">
 <node TEXT="どのように利用するか" ID="ID_549509034" CREATED="1704696775586" MODIFIED="1704696779463">
 <node TEXT="通常のCopyingGCではヒープ領がコピーされる" ID="ID_830576894" CREATED="1704692782815" MODIFIED="1704692814222"/>
 <node TEXT="GearsFileSystemの場合は木をコピーする" ID="ID_1003156855" CREATED="1704692814851" MODIFIED="1704692831840"/>
@@ -723,7 +723,7 @@
 <node TEXT="メモ" ID="ID_1983774695" CREATED="1705551362475" MODIFIED="1705551366046">
 <node TEXT="i-node treeをbackup, replication, gc可能であることを書きたい" ID="ID_559931709" CREATED="1705551366386" MODIFIED="1705551399134"/>
 </node>
-<node TEXT="別Contextへのコピー" FOLDED="true" ID="ID_399369896" CREATED="1706681655595" MODIFIED="1706686153089">
+<node TEXT="別Contextへのコピー" ID="ID_399369896" CREATED="1706681655595" MODIFIED="1706686153089">
 <node TEXT="Contextとデータの関係" ID="ID_886743343" CREATED="1706682841186" MODIFIED="1706682863894">
 <node TEXT="ContextはCode tableとData tableをそれぞれ持つ" ID="ID_21894122" CREATED="1706682868410" MODIFIED="1706682889001"/>
 <node TEXT="ALLOCATIONするとData tableのヒープ領域に，そのDataGear分の領域が確保される" ID="ID_1585444915" CREATED="1706682889540" MODIFIED="1706682925919"/>
@@ -805,7 +805,7 @@
 <node TEXT="実行したCodeGearを出力する仕組みが欲しい" POSITION="right" ID="ID_566018654" CREATED="1706690111878" MODIFIED="1706690124375">
 <node TEXT="毎回printfするの面倒" ID="ID_402999765" CREATED="1706690125223" MODIFIED="1706690134582"/>
 </node>
-<node TEXT="別ContextへのCopy" FOLDED="true" POSITION="right" ID="ID_1256969896" CREATED="1706608691732" MODIFIED="1706691074851" HGAP_QUANTITY="14.75 pt" VSHIFT_QUANTITY="21 pt">
+<node TEXT="別ContextへのCopy" POSITION="right" ID="ID_1256969896" CREATED="1706608691732" MODIFIED="1706691074851" HGAP_QUANTITY="14.75 pt" VSHIFT_QUANTITY="21 pt">
 <node TEXT="新たにヒープ領域を確保することによりコンパクションされる" ID="ID_1570751579" CREATED="1706610433391" MODIFIED="1706610495922">
 <node TEXT="少なくとも論理的には" ID="ID_1203172749" CREATED="1706610530004" MODIFIED="1706610535897"/>
 </node>
@@ -875,7 +875,7 @@
 </node>
 </node>
 </node>
-<node TEXT="CopyRedBlackTreeの実装" FOLDED="true" POSITION="right" ID="ID_1875155929" CREATED="1706686273106" MODIFIED="1707213582715" HGAP_QUANTITY="17.75 pt" VSHIFT_QUANTITY="6.75 pt">
+<node TEXT="CopyRedBlackTreeの実装" POSITION="right" ID="ID_1875155929" CREATED="1706686273106" MODIFIED="1707213582715" HGAP_QUANTITY="17.75 pt" VSHIFT_QUANTITY="6.75 pt">
 <node TEXT="説明" ID="ID_1618684595" CREATED="1706689938660" MODIFIED="1706689944053">
 <node TEXT="TreeのAPIのひとつとして実装" ID="ID_1013219955" CREATED="1706934961492" MODIFIED="1706934969874"/>
 <node TEXT="アルゴリズム" ID="ID_73867053" CREATED="1706934970286" MODIFIED="1706934976931"/>
@@ -988,7 +988,7 @@
 </node>
 <node TEXT="評価" POSITION="right" ID="ID_1699170037" CREATED="1706803749390" MODIFIED="1707213585346" HGAP_QUANTITY="14.75 pt" VSHIFT_QUANTITY="121.5 pt">
 <node TEXT="説明" ID="ID_1332913546" CREATED="1707024290462" MODIFIED="1707024304655">
-<node TEXT="テストコード" FOLDED="true" ID="ID_83989606" CREATED="1707024312272" MODIFIED="1707024315913">
+<node TEXT="テストコード" ID="ID_83989606" CREATED="1707024312272" MODIFIED="1707024315913">
 <node TEXT="いくつかの考えられる木の形はテストした" ID="ID_401372478" CREATED="1707024501611" MODIFIED="1707024539431">
 <node TEXT="11パターン" ID="ID_1060583266" CREATED="1707036504432" MODIFIED="1707110133774"/>
 <node TEXT="動作した" ID="ID_854834536" CREATED="1707024607282" MODIFIED="1707024611419"/>
@@ -1002,7 +1002,7 @@
 <node TEXT="上限を拡大する仕組みがいる" ID="ID_37519178" CREATED="1707024740319" MODIFIED="1707024747188"/>
 </node>
 </node>
-<node TEXT="非破壊RedBlackTreeの増大抑制" FOLDED="true" ID="ID_529836819" CREATED="1707024322382" MODIFIED="1707024336261">
+<node TEXT="非破壊RedBlackTreeの増大抑制" ID="ID_529836819" CREATED="1707024322382" MODIFIED="1707024336261">
 <node TEXT="非破壊なので過去の履歴がそのまま残り木が増大する問題があった" ID="ID_1452229252" CREATED="1707219315165" MODIFIED="1707219344850"/>
 <node TEXT="Copyによって参照される木の増大は防がれる" ID="ID_1864064653" CREATED="1707024754607" MODIFIED="1707024920464">
 <node TEXT="履歴部分が削がれるので" ID="ID_1998328102" CREATED="1707219356967" MODIFIED="1707219363161"/>
@@ -1012,10 +1012,10 @@
 <node TEXT="ゴミをフリーリストなどに接続する必要がある" ID="ID_891844429" CREATED="1707024810210" MODIFIED="1707024822315"/>
 <node TEXT="もしくは，別Contextへのコピーができていれば，Contextごと捨てることが考えられる" ID="ID_1594506897" CREATED="1707024822639" MODIFIED="1707024844218"/>
 </node>
-<node TEXT="RedBlackTreeの持続性" FOLDED="true" ID="ID_661781686" CREATED="1707024357426" MODIFIED="1707024367737">
+<node TEXT="RedBlackTreeの持続性" ID="ID_661781686" CREATED="1707024357426" MODIFIED="1707024367737">
 <node TEXT="単純なコピーで実装したため，データの持続性が保たれている" ID="ID_1984829925" CREATED="1707025135915" MODIFIED="1707025157178"/>
 </node>
-<node TEXT="Stackの使用" FOLDED="true" ID="ID_1762844508" CREATED="1707024350775" MODIFIED="1707024356847">
+<node TEXT="Stackの使用" ID="ID_1762844508" CREATED="1707024350775" MODIFIED="1707024356847">
 <node TEXT="軽量継続の利点はcall stackなどの状態をもたいないことにある" ID="ID_1185503713" CREATED="1707025000678" MODIFIED="1707025032692"/>
 <node TEXT="しかし，Stackを使用している" ID="ID_206860039" CREATED="1707025033563" MODIFIED="1707025074768"/>
 <node TEXT="明示的に使用しており，CodeGear自体が状態を持っているわけではないので問題ない" ID="ID_1843110566" CREATED="1707025055736" MODIFIED="1707025100382"/>
@@ -1128,6 +1128,13 @@
 <node TEXT="動作確認を困難にしている" ID="ID_729064103" CREATED="1707286242799" MODIFIED="1707286251072"/>
 <node TEXT="もっと簡潔に書ける仕組みが必要である" ID="ID_1162968810" CREATED="1707286225521" MODIFIED="1707286238147"/>
 </node>
+<node TEXT="モデル検査で並行実行下で正しく動くことを調べる" ID="ID_809389781" CREATED="1708499048406" MODIFIED="1708499074712">
+<node TEXT="メモリアロケーションを含めたモデル検査" ID="ID_1867917279" CREATED="1708499074988" MODIFIED="1708499085583"/>
+</node>
+<node TEXT="GearsAgdaでの記述" ID="ID_1601563606" CREATED="1708499091272" MODIFIED="1708499098375">
+<node TEXT="並列実行下で正しく動くか" ID="ID_473953074" CREATED="1708499106015" MODIFIED="1708499122316"/>
+<node TEXT="メモリが正しく開放されているか" ID="ID_1407864639" CREATED="1708499130161" MODIFIED="1708499140285"/>
+</node>
 <node TEXT="GCとレプリケーションの実装" ID="ID_1710394671" CREATED="1707286605335" MODIFIED="1707286619440">
 <node TEXT="今回は簡易的なswapの実装まで行った．" ID="ID_1766016847" CREATED="1707291693108" MODIFIED="1707291717793"/>
 <node TEXT="GCとレプリケーションを実装したい" ID="ID_398459676" CREATED="1707291718649" MODIFIED="1707291726995"/>
@@ -1146,7 +1153,26 @@
 </node>
 </node>
 </node>
-<node TEXT="バックアップやGCのタイミング" FOLDED="true" POSITION="left" ID="ID_1968325106" CREATED="1705995867783" MODIFIED="1707801876355" HGAP_QUANTITY="20 pt" VSHIFT_QUANTITY="-73.5 pt">
+<node TEXT="GearsOSでプログラムを書く理由" POSITION="right" ID="ID_1377446278" CREATED="1708497889835" MODIFIED="1708497927999">
+<node TEXT="GearsOSプログラミングと通常プログラミングの違い" ID="ID_983576587" CREATED="1708497928550" MODIFIED="1708497941327">
+<node TEXT="実行するプログラムをCodeGear単位に分割" ID="ID_1117945974" CREATED="1708497977620" MODIFIED="1708497988987"/>
+<node TEXT="CodeGearの引数とContextにプログラムの状態が全て入っている" ID="ID_1649806643" CREATED="1708497989646" MODIFIED="1708498016790"/>
+<node TEXT="通常のプログラムではcall stackやループが隠されている" ID="ID_1938146050" CREATED="1708498017795" MODIFIED="1708498048371"/>
+<node TEXT="照明の際には状態の明示化が必要である" ID="ID_418751667" CREATED="1708498159751" MODIFIED="1708498179891">
+<node TEXT="" ID="ID_876960664" CREATED="1708498233186" MODIFIED="1708498233186"/>
+</node>
+<node TEXT="CodeGearの切り替え点でモデル検査や証明が行える" ID="ID_920082921" CREATED="1708498128041" MODIFIED="1708498149779"/>
+</node>
+<node TEXT="基本的なデータ構造の処理をGearsOSに書き換える必要性" ID="ID_758255180" CREATED="1708497941808" MODIFIED="1708498265020">
+<node TEXT="既存のプログラムをそのままCodeGearに書き換えることは可能" ID="ID_879271430" CREATED="1708498265624" MODIFIED="1708498292858"/>
+<node TEXT="しかしCodeGear, DataGearともに複雑になる" ID="ID_323046419" CREATED="1708498293627" MODIFIED="1708498309138"/>
+<node TEXT="既存のプログラムは人間向けの読みやすさ優先だから" ID="ID_1347425608" CREATED="1708498309477" MODIFIED="1708498341399"/>
+<node TEXT="ここで重要なのはモデル検査と定理証明のしやすさ" ID="ID_335907196" CREATED="1708498341949" MODIFIED="1708498364377"/>
+<node TEXT="基本的なデータ構造を証明優先に書き換える必要がある" ID="ID_291897793" CREATED="1708498364719" MODIFIED="1708498396203"/>
+<node TEXT="これらは既存のプログラムとは違うプログラミングスタイルになる" ID="ID_752128558" CREATED="1708498396485" MODIFIED="1708498414704"/>
+</node>
+</node>
+<node TEXT="バックアップやGCのタイミング" POSITION="left" ID="ID_1968325106" CREATED="1705995867783" MODIFIED="1707801876355" HGAP_QUANTITY="20 pt" VSHIFT_QUANTITY="-73.5 pt">
 <node TEXT="木の操作の度にGCしていては効率が悪い" ID="ID_1270257607" CREATED="1705995886579" MODIFIED="1705995983113">
 <node TEXT="システムの状態によって処理を切り替える" ID="ID_835268540" CREATED="1705995987307" MODIFIED="1705995998232"/>
 <node TEXT="メモリがこれくらい使われている" ID="ID_708465587" CREATED="1705996000486" MODIFIED="1705996008587"/>
@@ -1167,7 +1193,7 @@
 </node>
 </node>
 </node>
-<node TEXT="レプリケーション手法" FOLDED="true" POSITION="left" ID="ID_1667606869" CREATED="1705990967981" MODIFIED="1707801878703" HGAP_QUANTITY="23 pt" VSHIFT_QUANTITY="-65.25 pt">
+<node TEXT="レプリケーション手法" POSITION="left" ID="ID_1667606869" CREATED="1705990967981" MODIFIED="1707801878703" HGAP_QUANTITY="23 pt" VSHIFT_QUANTITY="-65.25 pt">
 <node TEXT="bin log" ID="ID_1578494368" CREATED="1705990975951" MODIFIED="1705990978180"/>
 <node TEXT="WAL" ID="ID_173341311" CREATED="1705991115261" MODIFIED="1705991117448">
 <node TEXT="Write Ahead Logging" ID="ID_885834048" CREATED="1705991256045" MODIFIED="1705991267446"/>
@@ -1184,19 +1210,19 @@
 </node>
 <node TEXT="実装" POSITION="left" ID="ID_1462455862" CREATED="1706417525408" MODIFIED="1707801880634" HGAP_QUANTITY="29.75 pt" VSHIFT_QUANTITY="-83.25 pt">
 <node TEXT="CopyRedBlackTreeの実装" ID="ID_1619882257" CREATED="1701697553803" MODIFIED="1706520562137" VSHIFT_QUANTITY="-4.5 pt">
-<node TEXT="実装方法" FOLDED="true" ID="ID_1774988166" CREATED="1705735668943" MODIFIED="1705735677711">
+<node TEXT="実装方法" ID="ID_1774988166" CREATED="1705735668943" MODIFIED="1705735677711">
 <node TEXT="Tree InterfaceのAPIにCopyを追加する" ID="ID_95904284" CREATED="1705735678228" MODIFIED="1705735715335"/>
 <node TEXT="RedBlackTreeのコピーとして実装する" ID="ID_748405331" CREATED="1706417169892" MODIFIED="1706417179625"/>
 </node>
-<node TEXT="使い方（test）" FOLDED="true" ID="ID_952766134" CREATED="1706417138868" MODIFIED="1706417138868">
+<node TEXT="使い方（test）" ID="ID_952766134" CREATED="1706417138868" MODIFIED="1706417138868">
 <node TEXT="Copy()にはtree以外何も渡さない" ID="ID_1081702361" CREATED="1706417367338" MODIFIED="1706417401749">
 <node TEXT="何か渡すことも考えられる" ID="ID_1227095307" CREATED="1706417402206" MODIFIED="1706417409509"/>
 <node TEXT="GCする場合とreplicationする場合で動作を切り替えるとか" ID="ID_431028898" CREATED="1706417409901" MODIFIED="1706417421736"/>
 </node>
 </node>
-<node TEXT="コピーのアルゴリズム" FOLDED="true" ID="ID_64994373" CREATED="1703491215841" MODIFIED="1706691006775">
+<node TEXT="コピーのアルゴリズム" ID="ID_64994373" CREATED="1703491215841" MODIFIED="1706691006775">
 <node TEXT="アルゴリズム" ID="ID_972208221" CREATED="1699849518269" MODIFIED="1706691006775">
-<node TEXT="Stackを使う" FOLDED="true" ID="ID_799370781" CREATED="1706417204202" MODIFIED="1706417282682">
+<node TEXT="Stackを使う" ID="ID_799370781" CREATED="1706417204202" MODIFIED="1706417282682">
 <node TEXT="2つのStack" ID="ID_1829045504" CREATED="1706417283299" MODIFIED="1706417289209">
 <node TEXT="nodeStack" ID="ID_651682201" CREATED="1706417210255" MODIFIED="1706417229905">
 <node TEXT="From木を辿るためのStack" ID="ID_1782478294" CREATED="1706417237281" MODIFIED="1706417257704"/>
@@ -1207,25 +1233,25 @@
 </node>
 <node TEXT="SingleLinkedStack" ID="ID_1528506233" CREATED="1706417294502" MODIFIED="1706417299177"/>
 </node>
-<node TEXT="左側を深さ優先で辿る" FOLDED="true" ID="ID_239741561" CREATED="1699849525266" MODIFIED="1706690997244">
+<node TEXT="左側を深さ優先で辿る" ID="ID_239741561" CREATED="1699849525266" MODIFIED="1706690997244">
 <node TEXT="子にcurrentを付け替えて親をnodeStackにpush" ID="ID_1852624670" CREATED="1706417608144" MODIFIED="1706417658172"/>
 <node TEXT="nodeStackはcurrentより以前のノードを持つ" ID="ID_304892775" CREATED="1706417633577" MODIFIED="1706690997243"/>
 <node TEXT="allocateした新しいnodeはinputStackにpush" ID="ID_749123856" CREATED="1706418475694" MODIFIED="1706418497889"/>
 </node>
-<node TEXT="アロケートしたノードは別のContext上に作る" FOLDED="true" ID="ID_573859973" CREATED="1699849620905" MODIFIED="1699849638042">
+<node TEXT="アロケートしたノードは別のContext上に作る" ID="ID_573859973" CREATED="1699849620905" MODIFIED="1699849638042">
 <node TEXT="GCのため" ID="ID_259949416" CREATED="1699849638520" MODIFIED="1699849668501"/>
 <node TEXT="Copy後古いContextを消す" ID="ID_1297792398" CREATED="1699849646521" MODIFIED="1699849693755"/>
 <node TEXT="メモリ管理をモナドで表していることになる" ID="ID_152951728" CREATED="1699849705089" MODIFIED="1699849715878"/>
 <node TEXT="ALLOCで別のContextに書き込むようにしたいな" ID="ID_1289215093" CREATED="1706417832741" MODIFIED="1706417849017"/>
 <node TEXT="別ノードに書き込むことになるのでそのままreplicationになる" ID="ID_1997482213" CREATED="1706508692481" MODIFIED="1706508711469"/>
 </node>
-<node TEXT="リーフまで降りたらroot方向に木を戻る" FOLDED="true" ID="ID_1233772087" CREATED="1699849731393" MODIFIED="1699849765553">
+<node TEXT="リーフまで降りたらroot方向に木を戻る" ID="ID_1233772087" CREATED="1699849731393" MODIFIED="1699849765553">
 <node TEXT="Stack pop" ID="ID_1907664340" CREATED="1699849765982" MODIFIED="1699849773214"/>
 <node TEXT="右側を呼び出す" ID="ID_1658933965" CREATED="1699849789218" MODIFIED="1699849803550"/>
 </node>
 </node>
 </node>
-<node TEXT="コード説明" FOLDED="true" ID="ID_1352482727" CREATED="1704630501155" MODIFIED="1704630507416">
+<node TEXT="コード説明" ID="ID_1352482727" CREATED="1704630501155" MODIFIED="1704630507416">
 <node TEXT="ALLOCATEの部分" ID="ID_933840077" CREATED="1706418297855" MODIFIED="1706418365645">
 <node TEXT="" ID="ID_1621850954" CREATED="1706503638877" MODIFIED="1706503638877"/>
 </node>
@@ -1244,7 +1270,7 @@
 <node TEXT="swap" ID="ID_11264463" CREATED="1706419404827" MODIFIED="1706419406275"/>
 </node>
 </node>
-<node TEXT="動作確認" FOLDED="true" ID="ID_793097790" CREATED="1706419438278" MODIFIED="1706691045584">
+<node TEXT="動作確認" ID="ID_793097790" CREATED="1706419438278" MODIFIED="1706691045584">
 <node TEXT="テストケース" ID="ID_596576048" CREATED="1706420024765" MODIFIED="1706691045584"/>
 </node>
 </node>
@@ -1256,7 +1282,7 @@
 <node TEXT="copy機能が追加されたことにより信頼性を確保する機能が実装できるようになるだろう" ID="ID_759285029" CREATED="1706424528708" MODIFIED="1706424548485"/>
 <node TEXT="今回は簡易的なGCに留まる" ID="ID_945220922" CREATED="1706424556818" MODIFIED="1706424564389"/>
 <node TEXT="ここまで動作確認はした" ID="ID_1964377761" CREATED="1706424650365" MODIFIED="1706424656184"/>
-<node TEXT="証明のしやすさについて" FOLDED="true" ID="ID_2776247" CREATED="1703492904417" MODIFIED="1703492910899">
+<node TEXT="証明のしやすさについて" ID="ID_2776247" CREATED="1703492904417" MODIFIED="1703492910899">
 <node TEXT="Stackの使用に関して" ID="ID_432827984" CREATED="1703492856041" MODIFIED="1703492863503">
 <node TEXT="使用していることを明示しているので問題ない" ID="ID_203410953" CREATED="1706418581660" MODIFIED="1706418592724"/>
 <node TEXT="それはそれで証明する必要があるんだけども" ID="ID_1283008974" CREATED="1706418601289" MODIFIED="1706418613023"/>
@@ -1266,7 +1292,7 @@
 </node>
 </node>
 </node>
-<node TEXT="スライド" FOLDED="true" POSITION="left" ID="ID_1109312213" CREATED="1707801871675" MODIFIED="1707813260044">
+<node TEXT="スライド" POSITION="left" ID="ID_1109312213" CREATED="1707801871675" MODIFIED="1707813260044">
 <node TEXT="システム全体の信頼性を向上させたい" ID="ID_1519013410" CREATED="1707809324624" MODIFIED="1707809621777" HGAP_QUANTITY="14 pt" VSHIFT_QUANTITY="-3 pt"/>
 <node TEXT="GearsOSで実現する" ID="ID_1781659444" CREATED="1707809341570" MODIFIED="1707809348782"/>
 <node TEXT="信頼性を上げる方法" ID="ID_284645498" CREATED="1707809403391" MODIFIED="1707809624565" HGAP_QUANTITY="12.5 pt" VSHIFT_QUANTITY="-33.75 pt"/>
@@ -1281,7 +1307,7 @@
 <node TEXT="ファイルシステムの信頼性" ID="ID_1312841457" CREATED="1707819281060" MODIFIED="1707819289625"/>
 <node TEXT="メモリ管理や多重性の機能がない" ID="ID_1755524219" CREATED="1707809043957" MODIFIED="1707819996876"/>
 <node TEXT="copyRedBlackTreeの実装をした" ID="ID_3452822" CREATED="1707802848111" MODIFIED="1707802871025"/>
-<node TEXT="copyRedBlackTreeによって出来ること" FOLDED="true" ID="ID_108556449" CREATED="1707804472923" MODIFIED="1707813284750">
+<node TEXT="copyRedBlackTreeによって出来ること" ID="ID_108556449" CREATED="1707804472923" MODIFIED="1707813284750">
 <node TEXT="多重性やメモリ管理に関する機能を追加できる" ID="ID_42031813" CREATED="1707804510984" MODIFIED="1707805366037"/>
 <node TEXT="GC(defragmentation)" ID="ID_240352266" CREATED="1707802572704" MODIFIED="1707809162287"/>
 <node TEXT="レプリケーション" ID="ID_854911737" CREATED="1707802624641" MODIFIED="1707802629911"/>
@@ -1309,7 +1335,7 @@
 <node TEXT="非破壊RedBlackTreeの増大抑制により実用的に" ID="ID_1391218931" CREATED="1707802699292" MODIFIED="1707809767003"/>
 </node>
 </node>
-<node TEXT="Gears記述時の問題点" FOLDED="true" POSITION="left" ID="ID_1902607339" CREATED="1707959403247" MODIFIED="1707959412801">
+<node TEXT="Gears記述時の問題点" POSITION="left" ID="ID_1902607339" CREATED="1707959403247" MODIFIED="1707959412801">
 <node TEXT="ループ文がない" ID="ID_1779927572" CREATED="1707959413129" MODIFIED="1707959424169">
 <node TEXT="gotoのループで表現する必要がある" ID="ID_693586670" CREATED="1707959482423" MODIFIED="1707959498438"/>
 <node TEXT="動作確認用のテストコードが書きづらい" ID="ID_583316910" CREATED="1707959575090" MODIFIED="1707959607654">
Binary file poster/matac-poster.graffle has changed