--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/matac42/notes/2023/11/06.md	Tue Nov 07 00:10:03 2023 +0900
@@ -0,0 +1,380 @@
+# 研究目的
+
+## システム全体の信頼性を上げたい
+
+- システムの構成要素全体の信頼性を上げる必要がある
+  - アプリケーション
+  - OS
+  - ファイルシステム
+  - DB
+  - メモリとSSD
+  - 分散ノード
+  - ネットワーク
+
+## ファイルシステムとDBの信頼性を考える
+
+ファイルシステムとは何か
+
+DBとは何か
+
+これらは何が違うのか
+
+検証・モデル検査をできる形に記述したい
+
+## ファイルシステム
+
+可変長の文字列を格納するファイル
+
+そのファイルにアクセスするための名前管理
+
+同時アクセスした時に名前管理の一貫性を保証する
+
+ファイルに同時に書き込まれた時の一貫性の保証はしない
+
+(ファイルの書き込みを制御するロック機構がある
+
+## DB
+
+入力の属性名と型の組みを複数持つレコード
+
+特定の属性をキーとしたテーブル
+
+レコードのinsert, delete, updateの直列化可能性を保証する機能がある
+
+## ファイルシステムとDBの違い
+
+格納するものの形式
+
+それにアクセスする方法
+
+直列化可能性を保証する手法
+
+これらが違うだけで本質的な違いはない
+
+## ファイルシステムとDBのもつ追加機能
+
+電源切った時にデータが残る(持続性persistency)
+
+書き込めたかどうかをtrue, falseで判定するatomic write
+
+ひとつのノードが失われた時にデータを保護する多重性
+
+適当なチェックポイントからDB、ファイルシステムを回復する機能
+
+複数のコピーを調停するコミット機構
+
+## Gears OSを使って実現する
+
+
+- CodeGear
+  - 処理の単位
+- DataGear
+  - データの単位
+- metaGear
+  - データの整合性
+  - 資源管理
+
+非破壊的なRedBlackTreeでほとんどのものが記述できるのではないか
+
+## 信頼性を上げる方法
+
+- 証明
+  - GearsAgdaを使ってinvariantを証明する
+- テスト
+- モデル検査
+- システムの構成要素全体にこれらの方法を適用したい
+- 既存システムの信頼性における問題点の解決
+
+## GearsOS上のファイルシステムやDB
+
+RedBlackTreeでどちらも一応実現できてはいる
+
+が、できていないことも多い
+
+複数のreplicationを持てていない
+
+GCがない
+
+とりあえず、RedBlackTreeのコピーをやると良いのではないか
+
+## RedBlackTreeのコピー
+
+簡単なのでは？
+
+実際は複雑
+
+Treeをコピーしている間に変更されたら？
+
+頭から最後までコピーすることはできない
+
+コピー前と後で同一であることを確認する必要がある
+
+## コピーのアルゴリズム
+
+insertはRedBlackTreeを辿って必要なノードまでTreeをコピーしながら下っていく
+
+見つかったら変更したTreeを返す
+
+そのためには
+
+Stackを使ってTreeを辿っていく
+
+まず左側を深さ優先で辿る
+
+アロケートしたノードは別のContext上に作る必要がある
+
+なぜならばGCしたいから
+
+全部のTreeをコピーしたら古いContextを消すことでGCになる
+
+これはメモリ管理をモナドで表していることになる
+
+リーフまできたらStackを巻き戻すCGを呼ぶ
+
+この時左側はできているので右側を呼び出す
+
+Stackのノードの情報だけでできるのか
+
+Stackが二つ必要
+
+全体と途中まで作りかけのTreeのStack
+
+## 既存のRedBlackTreeのtestを動かしてみた
+
+ちょっとだけ修正したら動いた。
+
+```bash
+./cleanup.sh
+
+cmake .
+CMake Warning (dev) in CMakeLists.txt:
+  No project() command is present.  The top-level CMakeLists.txt file must
+  contain a literal, direct call to the project() command.  Add a line of
+  code such as
+
+    project(ProjectName)
+
+  near the top of the file, but after cmake_minimum_required().
+
+  CMake is pretending there is a "project(Project)" command on the first
+  line.
+This warning is for project developers.  Use -Wno-dev to suppress it.
+
+CMake Warning (dev) in CMakeLists.txt:
+  cmake_minimum_required() should be called prior to this top-level project()
+  call.  Please see the cmake-commands(7) manual for usage documentation of
+  both commands.
+This warning is for project developers.  Use -Wno-dev to suppress it.
+
+-- The C compiler identification is AppleClang 15.0.0.15000040
+-- The CXX compiler identification is AppleClang 15.0.0.15000040
+-- Detecting C compiler ABI info
+-- Detecting C compiler ABI info - done
+-- Check for working C compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc - skipped
+-- Detecting C compile features
+-- Detecting C compile features - done
+-- Detecting CXX compiler ABI info
+-- Detecting CXX compiler ABI info - done
+-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ - skipped
+-- Detecting CXX compile features
+-- Detecting CXX compile features - done
+-- Configuring done (0.7s)
+-- Generating done (0.1s)
+-- Build files have been written to: /Users/matac/ws/src/firefly/hg/Gears/Gears/src/parallel_execution
+make rbtree
+[  0%] Generating c-rbtree/test/rbTree_test.c
+[ 33%] Generating c-rbtree/RedBlackTree.c
+[ 33%] Generating c-rbtree/SingleLinkedQueue.c
+[ 33%] Generating c-rbtree/SingleLinkedStack.c
+[WARN] Not found SingleLinkedStack.h at generate_stub.pl line 679.
+[ 33%] Generating c-rbtree/rbtree-context.c
+[ 33%] Building C object CMakeFiles/rbtree.dir/c-rbtree/SingleLinkedQueue.c.o
+[ 66%] Building C object CMakeFiles/rbtree.dir/c-rbtree/test/rbTree_test.c.o
+[ 66%] Building C object CMakeFiles/rbtree.dir/c-rbtree/RedBlackTree.c.o
+[ 66%] Building C object CMakeFiles/rbtree.dir/c-rbtree/SingleLinkedStack.c.o
+[ 66%] Building C object CMakeFiles/rbtree.dir/compare.c.o
+[ 66%] Building C object CMakeFiles/rbtree.dir/c-rbtree/rbtree-context.c.o
+[100%] Linking C executable rbtree
+[100%] Built target rbtree
+make rbtree_test1
+[  0%] Generating c-rbtree_test1/test/rb_tree_test1.c
+[  0%] Generating c-rbtree_test1/AtomicReference.c
+[ 25%] Generating c-rbtree_test1/CPUWorker.c
+[ 25%] Generating c-rbtree_test1/RedBlackTree.c
+[ 25%] Generating c-rbtree_test1/SingleLinkedQueue.c
+[ 50%] Generating c-rbtree_test1/SingleLinkedStack.c
+[WARN] Not found SingleLinkedStack.h at generate_stub.pl line 679.
+[ 50%] Generating c-rbtree_test1/SynchronizedQueue.c
+[ 50%] Generating c-rbtree_test1/TaskManagerImpl.c
+[ 50%] Generating c-rbtree_test1/rbtree_test1-context.c
+[ 50%] Building C object CMakeFiles/rbtree_test1.dir/c-rbtree_test1/test/rb_tree_test1.c.o
+/Users/matac/ws/src/firefly/hg/Gears/Gears/src/parallel_execution/c-rbtree_test1/test/rb_tree_test1.c:7:33: warning: incompatible pointer types assigning to 'union Data *' from 'struct Tree *' [-Wincompatible-pointer-types]
+    7 |     Gearef(context, Tree)->tree = tree;
+      |                                 ^ ~~~~
+/Users/matac/ws/src/firefly/hg/Gears/Gears/src/parallel_execution/c-rbtree_test1/test/rb_tree_test1.c:23:17: warning: incompatible pointer types assigning to 'union Data *' from 'Queue *' (aka 'struct Queue *') [-Wincompatible-pointer-types]
+   23 |     node->value = queue;
+      |                 ^ ~~~~~
+/Users/matac/ws/src/firefly/hg/Gears/Gears/src/parallel_execution/c-rbtree_test1/test/rb_tree_test1.c:43:17: warning: incompatible pointer types assigning to 'union Data *' from 'Queue *' (aka 'struct Queue *') [-Wincompatible-pointer-types]
+   43 |     node->value = queue;
+      |                 ^ ~~~~~
+/Users/matac/ws/src/firefly/hg/Gears/Gears/src/parallel_execution/c-rbtree_test1/test/rb_tree_test1.c:62:17: warning: incompatible pointer types assigning to 'union Data *' from 'Queue *' (aka 'struct Queue *') [-Wincompatible-pointer-types]
+   62 |     node->value = queue;
+      |                 ^ ~~~~~
+4 warnings generated.
+[ 50%] Building C object CMakeFiles/rbtree_test1.dir/c-rbtree_test1/TaskManagerImpl.c.o
+[ 50%] Building C object CMakeFiles/rbtree_test1.dir/c-rbtree_test1/CPUWorker.c.o
+[ 75%] Building C object CMakeFiles/rbtree_test1.dir/c-rbtree_test1/SynchronizedQueue.c.o
+[ 75%] Building C object CMakeFiles/rbtree_test1.dir/c-rbtree_test1/AtomicReference.c.o
+[ 75%] Building C object CMakeFiles/rbtree_test1.dir/c-rbtree_test1/SingleLinkedQueue.c.o
+[ 75%] Building C object CMakeFiles/rbtree_test1.dir/c-rbtree_test1/RedBlackTree.c.o
+[ 75%] Building C object CMakeFiles/rbtree_test1.dir/c-rbtree_test1/SingleLinkedStack.c.o
+[100%] Building C object CMakeFiles/rbtree_test1.dir/compare.c.o
+[100%] Building C object CMakeFiles/rbtree_test1.dir/c-rbtree_test1/rbtree_test1-context.c.o
+[100%] Linking C executable rbtree_test1
+[100%] Built target rbtree_test1
+./rbtree
+test_main
+test1_stub
+Test1
+value->3,key->3
+test2_stub
+Test2
+test3
+value=3 key=3
+test4
+test5
+./rbtree_test1
+---create stub
+---create
+---put1 stub
+---put1
+---put2 stub
+---put2
+---remove stub
+---remove
+key = 0 (key = 1 (NULL), (NULL)), (NULL)
+```
+
+`rbTreeCopy_test.cbc`を追加した
+
+- いくつかputした後copyする
+
+```c
+#include <stdio.h>
+#interface "Tree.h"
+
+/* #include <assert.h> */
+
+__code rbTreeTest1(struct Tree* tree) {
+  printf("Test1\n");
+  Node* node = new Node();
+  node->value = (union Data*)new Integer();
+  ((Integer*)node->value)->value = 1;
+  node->key = 1;
+  printf("value->%d,key->%d\n",((Integer*)node->value)->value,node->key);
+  goto tree->put(node, rbTreeTest2);
+}
+
+__code rbTreeTest1_stub(struct Context* context) {
+  printf("test1_stub\n");
+  Tree* tree = createRedBlackTree(context);
+  goto rbTreeTest1(context,tree);
+}
+
+
+__code rbTreeTest2(struct Tree* tree) {
+  printf("Test2\n");
+  Node* node = new Node();
+  node->value = (union Data*)new Integer();
+  ((Integer*)(node->value))->value= 2;
+  node->key = 2;
+  goto tree->get(node, rbTreeTest3);
+}
+
+__code rbTreeTest2_stub(struct Context* context) {
+  printf("test2_stub\n");
+  Tree* tree = (struct Tree*)Gearef(context, Tree)->tree;
+  goto rbTreeTest2(context,tree);
+}
+
+
+__code rbTreeTest3(struct Tree* tree, struct Node* node0) {
+  printf("test3\n");
+  printf("value=%d key=%d\n", ((Integer*)node0->value)->value, node0->key);
+  Node* node = new Node();
+  node->value = (union Data*)new Integer();
+  ((Integer*)(node->value))->value = 3;
+  node->key = 3;
+  goto tree->put(node, rbTreeTest4);
+}
+
+__code rbTreeTest3_stub(struct Context* context) {
+  Tree* tree = (struct Tree*)Gearef(context, Tree)->tree;
+  Node* node0 = Gearef(context, Tree)->node;
+  goto rbTreeTest3(context,tree,node0);
+}
+
+__code rbTreeTest4(struct Tree* tree) {
+  printf("test4\n");
+  Node* node = new Node();
+  node->value = (union Data*)new Integer();
+  ((Integer*)(node->value))->value = 4;
+  node->key = 4;
+  goto tree->put(node, rbTreeTest5);
+}
+
+__code rbTreeTest4_stub(struct Context* context) {
+  Tree* tree = (struct Tree*)Gearef(context, Tree)->tree;
+  goto rbTreeTest4(context,tree);
+}
+
+__code rbTreeTest5(struct Tree* tree) {
+  printf("test5\n");
+  Node* node = new Node();
+  node->value = (union Data*)new Integer();
+  goto tree->copy(exit_code);
+}
+
+__code rbTreeTest5_stub(struct Context* context) {
+  Tree* tree = (struct Tree*)Gearef(context, Tree)->tree;
+  goto rbTreeTest5(context,tree);
+}
+
+int main(int argc, char const* argv[]) {
+  printf("test_main\n");
+  goto rbTreeTest1();
+}
+```
+
+## RedBlackTreeを読んでいた
+
+読みながらcopyRedBlackTreeがどんなコードになるか考えていた。
+が、`newNode`がなんなのかよくわかっていないということがわかった。
+
+↓newNodeが考慮されていない
+
+### copyRedBlackTree
+
+- leftを入れる
+- left==Nullならばrightを入れて見る
+  - そうでなければleftを次のNodeとしてgoto copyTree
+- right==Nullならばgoto copyTreePopする
+  - そうでなければrightを次のNodeとしてgoto copyTree
+
+### copyRedBlackTreePop
+
+- rootならば
+  - left != Null && right != Nullならば終了
+  - right == Nullならばrightを入れる
+  - right == Nullならば終了
+    - そうでなければrightを次のnodeとしてgoto copyTree
+- right!=Nullならばpopしてgoto copyTreePop
+- rightを入れる
+- right!=Nullならばrightを次のNodeとしてgoto copyTree
+- right==Nullならばpopしgoto copyTreePop
+  - そうでなければrightを次のNodeとしてgoto copyTree
+  
+この辺はinsertNodeのようにcaseで分ける感じか？
+
+## 明日11時からGearsをやります
+