Mercurial > hg > Document > Growi

changeset 21:4a2bfdc45e69

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
backup 2021-01-13
author autobackup
date Wed, 13 Jan 2021 00:10:04 +0900
parents 3fd21f4cadc3
children 8bc110e35f8d
files Christie/for.NET.md Christie/for.NET/優先度つきThreadPool.md user/anatofuz/note/2021/01/12.md user/ikkun/memo/2020/12/15.md user/soto/log/2021-01-12.md
diffstat 5 files changed, 549 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/Christie/for.NET.md	Sun Jan 10 00:10:03 2021 +0900
+++ b/Christie/for.NET.md	Wed Jan 13 00:10:04 2021 +0900
@@ -49,6 +49,11 @@
 PriorityThreadPoolExecutor ThreadPoolの優先度実装
 
 ---
+## 実装時検証項目
+* 優先度が動いているか
+* HelloWorldが動くか
+
+---
 ## Tips
 C# 
 object → 全ての継承元クラス
@@ -288,7 +293,7 @@
 ---
 javaではserverSocketクラスがあり、listenerはこれを使えばいいが、c# 側にはない。  
 
-ここで注意するのが、javaではacceptでlistenを開始するが、C#ではListenでlistenを開始することに注意
+ここで注意するのが、javaではacceptでlistenを開始するが、C#ではListenでlistenをした後にacceptを行うこと開始することに注意
 
 
 ---
@@ -335,7 +340,7 @@
     * CodeGearManager 
         * IncomingTcpConnection要実装
         * ChristieDeamon要実装
-        * ThreadPoolExecutorとは
+        * RemoteDataGearManager要実装
     * CodeGearExecutor
         * cgm要実装
         * cg要実装
--- a/Christie/for.NET/優先度つきThreadPool.md	Sun Jan 10 00:10:03 2021 +0900
+++ b/Christie/for.NET/優先度つきThreadPool.md	Wed Jan 13 00:10:04 2021 +0900
@@ -185,6 +185,11 @@
 0の場合優先度の差がないので、instance生成順で並び替える  
 
 ---
+## 書き換えの方針
+https://docs.microsoft.com/en-us/dotnet/api/system.threading.tasks.taskscheduler?view=net-5.0  
+C#だとTaskSchedulerを拡張して中のQueueの順番を優先度に従って更新する感じで実装するとできそう  
+
+---
 ## 参考ページ
 http://normalse.hatenablog.jp/entry/2015/04/03/075443  
 https://qiita.com/sano1202/items/64593e8e981e8d6439d3  
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/anatofuz/note/2021/01/12.md	Wed Jan 13 00:10:04 2021 +0900
@@ -0,0 +1,431 @@
+# 2021/01/12
+
+# やったこと
+- gmain実装
+- `generate_stub.pl`で内部で`.cbc`を書き換えられるようになった
+    - ファイルにしなくてもPerl内部で変換前のコードを生成出来る
+- `genrate_stub.pl`に簡易デバッグモード追加
+- genrics関連の実装
+- 主査/副査の先生が発表されました
+
+# generate_stub.pl
+
+- `*.cbc`(Gearsのsyntaxで書かれたCbC)から `*.c` (純粋なCbC)に変換するスクリプト
+- cmakeで呼び出す
+    - 各`.cbc`ファイルごと処理される
+    - cmake上で実行した場合、`c/`ディレクトリの中に`.c`ファイルが生成される
+- CbCのトランスコンパイラっぽいやつ
+
+## 処理の修正
+
+- data gear, このファイルが何なのかを調べる`getDataGear`
+- 実際にファイルを生成する`generateDataGear`の大きく2つで行われる
+
+- 以前
+    - cbcファイルを読み込んで処理(`getDataGear`)
+    - もう一度読みながら`*.c`を生成(`generateDataGear`)
+- 現在
+    - 最初にCbCファイルを配列として読み込む
+    - 配列を読んで処理(`getDataGear`)
+    - すでに配列に保存されているcbcを読みながら`*.c`を生成(`generateDataGear`)
+
+- 配列にしたので、ファイルを経由せずににPerlでCbCの操作が出来るようになった
+    - 何かを適応してstubを生成するのがわりと書きやすくなった
+
+
+# gmain
+- main関数を作るのが大変
+    - `initCode`などを書かないといけない
+    - ほとんどコピペで済ましている
+- コピペで済ましているので、`gnerate_stub.pl`を使うことで変換出来るようにした
+    - 終了する場合は`shutdown`に継続する
+
+## 変換前
+
+```c
+#interface "Stack.h"
+#interface "StackTest.h"
+#interface "TaskManager.h"
+
+__code gmain(){
+    Stack* stack = createSingleLinkedStack(context);
+    StackTest* stackTest = createStackTestImpl3(context);
+    goto stackTest->insertTest1(stack, shutdown);
+}
+```
+
+## 変換後
+
+```c
+#include <stdio.h>
+#include <string.h>
+#include <stdlib.h>
+#include <unistd.h>
+
+#include "../../../context.h"
+
+int cpu_num = 1;
+int length = 102400;
+int split = 8;
+int* array_ptr;
+int gpu_num = 0;
+int CPU_ANY = -1;
+int CPU_CUDA = -1;
+
+__code initDataGears(struct Context *context,struct LoopCounter* loopCounter, struct TaskManager* taskManager) {
+    // loopCounter->tree = createRedBlackTree(context);
+    loopCounter->i = 0;
+    taskManager->taskManager = (union Data*)createTaskManagerImpl(context, cpu_num, gpu_num, 0);
+    goto meta(context, C_prevTask);
+}
+
+__code initDataGears_stub(struct Context* context) {
+	LoopCounter* loopCounter = Gearef(context, LoopCounter);
+	TaskManager* taskManager = Gearef(context, TaskManager);
+	goto initDataGears(context, loopCounter, taskManager);
+}
+
+__code prevTask(struct Context *context,struct LoopCounter* loopCounter) {
+    printf("cpus:\t\t%d\n", cpu_num);
+    printf("gpus:\t\t%d\n", gpu_num);
+    printf("length:\t\t%d\n", length);
+    printf("length/task:\t%d\n", length/split);
+    /* puts("queue"); */
+    /* print_queue(context->data[ActiveQueue]->queue.first); */
+    /* puts("tree"); */
+    /* print_tree(context->data[Tree]->tree.root); */
+    /* puts("result"); */
+    goto meta(context, C_createTask);
+}
+
+
+__code prevTask_stub(struct Context* context) {
+	LoopCounter* loopCounter = Gearef(context, LoopCounter);
+	goto prevTask(context, loopCounter);
+}
+
+__code createTask(struct Context *context,struct LoopCounter* loopCounter, struct TaskManager* taskManager) {
+    Stack* stack = createSingleLinkedStack(context);
+    StackTest* stackTest = createStackTestImpl3(context);
+    Gearef(context, StackTest)->stackTest = (union Data*) stackTest;
+    Gearef(context, StackTest)->stack = stack;
+    Gearef(context, StackTest)->next = C_shutdown;
+    goto meta(context, stackTest->insertTest1);
+}
+
+__code createTask_stub(struct Context* context) {
+	LoopCounter* loopCounter = Gearef(context, LoopCounter);
+	TaskManager* taskManager = Gearef(context, TaskManager);
+	goto createTask(context, loopCounter, taskManager);
+}
+
+__code shutdown(struct Context *context,struct TaskManager* taskManager) {
+    Gearef(context, TaskManager)->taskManager = (union Data*) taskManager;
+    Gearef(context, TaskManager)->next = C_exit_code;
+    goto meta(context, taskManager->shutdown);
+}
+
+__code shutdown_stub(struct Context* context) {
+    goto shutdown(context, &Gearef(context, TaskManager)->taskManager->TaskManager);
+}
+
+
+
+void init(int argc, char** argv) {
+    for (int i = 1; argv[i]; ++i) {
+        if (strcmp(argv[i], "-cpu") == 0)
+            cpu_num = (int)atoi(argv[i+1]);
+        else if (strcmp(argv[i], "-l") == 0)
+            length = (int)atoi(argv[i+1]);
+        else if (strcmp(argv[i], "-s") == 0)
+            split = (int)atoi(argv[i+1]);
+        else if (strcmp(argv[i], "-cuda") == 0) {
+            gpu_num = 1;
+            CPU_CUDA = 0;
+        }
+    }
+}
+
+int main(int argc, char** argv) {
+    init(argc, argv);
+    struct Context* main_context = NEW(struct Context);
+    initContext(main_context);
+    main_context->next = C_initDataGears;
+    goto start_code(main_context);
+}
+```
+
+# コンパイル時チェック機能
+
+- Interfaceの引数があってないのがありがち
+    - `generate_stub.pl`で生成された`.c`と`.cbc`をにらめっこしないといけない
+    - 気づくまで難しい, 気づかないケースがある(今までの実装)
+- `generate_stub.pl`の中でinterface gotoをしている箇所で引数検査を行う
+
+```
+[
+    [0] {
+        argc   1,
+        args   "Impl* phils, __code next(...)",
+        name   "thinking"
+    }
+]
+[
+    [0] "fork0",
+    [1] " __exit"
+]
+1
+[EROR] invalid arg     par goto phils0->thinking(fork0, __exit);
+  you shoud impl Impl* phils, __code next(...)
+```
+
+- そもそもそんなメソッドが無いケースも判定
+
+```c
+[ERROR] not found phils0 definition at     par goto phils0->think(fork0, __exit);
+ in c/examples/DPP/main.c
+```
+
+
+
+
+
+
+## debug
+
+- 実行時に`--debug`をつけるとデバッグオプションが起動
+- Perlで正規表現マッチしまくっているが、どこでマッチしたかデバッグするのが難しい
+    - 具体的にPerlの何行目にマッチしたのかを表示してくれる
+
+```perl
+            } elsif (/^(.*)goto (\w+)\((.*)\);/) {
+                debug_print("generateDataGear",__LINE__, $_) if $opt_debug;
+```
+
+```shell
+$ perl generate_stub.pl --debug examples/pop_and_push/StackTest2Impl.cbc
+[getDataGear] match 175 : #interface "StackTest2.h"
+[getDataGear] match 137 : typedef struct StackTest2 <> {
+[getDataGear] match 327 :   __code insertTest1(Impl* stackTest2, struct Stack* stack, union Data* data1, __code next(...));
+[getDataGear] match 327 :   __code gotoOtherInterface(Impl* stackTest2, struct Stack* stack, union Data* data1, struct StackTest* stackTest, __code next(...));
+[getDataGear] match 327 :   __code next(...);
+[getDataGear] match 309 : } StackTest2;
+[getDataGear] match 336 : } StackTest2;
+[getCodeGear] match 381 : typedef struct StackTest2 <> {
+[getCodeGear] match 386 :   __code insertTest1(Impl* stackTest2, struct Stack* stack, union Data* data1, __code next(...));
+[getCodeGear] match 386 :   __code gotoOtherInterface(Impl* stackTest2, struct Stack* stack, union Data* data1, struct StackTest* stackTest, __code next(...));
+[getCodeGear] match 386 :   __code next(...);
+[getDataGear] match 153 : StackTest2* createStackTest2Impl(struct Context* context) {
+[getDataGear] match 206 : __code insertTest1_StackTest2Impl(struct StackTest2Impl* stackTest2, struct Stack* stack, union Data* data1, __code next(...)) {
+[getDataGear] match 244 :     goto stack->push(data1, next);
+[AUTOINCLUDE] Forget #interface 'Stack'  declaration in examples/pop_and_push/StackTest2Impl.cbc at generate_stub.pl line 265.
+[getDataGear] match 137 : typedef struct Stack<>{
+[getDataGear] match 327 :         __code clear(Impl* stack,__code next(...));
+[getDataGear] match 327 :         __code push(Impl* stack,union Data* data, __code next(...));
+[getDataGear] match 327 :         __code pop(Impl* stack, __code next(union Data* data, ...));
+[getDataGear] match 327 :         __code pop2(Impl* stack, __code next(union Data* data, union Data* data1, ...));
+[getDataGear] match 327 :         __code isEmpty(Impl* stack, __code next(...), __code whenEmpty(...));
+[getDataGear] match 327 :         __code get(Impl* stack, __code next(union Data* data, ...));
+[getDataGear] match 327 :         __code get2(Impl* stack, __code next(union Data* data, union Data* data1, ...));
+[getDataGear] match 327 :         __code next(...);
+[getDataGear] match 327 :         __code whenEmpty(...);
+[getDataGear] match 309 : } Stack;
+[getDataGear] match 336 : } Stack;
+[getCodeGear] match 381 : typedef struct Stack<>{
+[getCodeGear] match 386 :         __code clear(Impl* stack,__code next(...));
+[getCodeGear] match 386 :         __code push(Impl* stack,union Data* data, __code next(...));
+[getCodeGear] match 386 :         __code pop(Impl* stack, __code next(union Data* data, ...));
+[getCodeGear] match 386 :         __code pop2(Impl* stack, __code next(union Data* data, union Data* data1, ...));
+[getCodeGear] match 386 :         __code isEmpty(Impl* stack, __code next(...), __code whenEmpty(...));
+[getCodeGear] match 386 :         __code get(Impl* stack, __code next(union Data* data, ...));
+[getCodeGear] match 386 :         __code get2(Impl* stack, __code next(union Data* data, union Data* data1, ...));
+[getCodeGear] match 386 :         __code next(...);
+[getCodeGear] match 386 :         __code whenEmpty(...);
+[getDataGear] match 206 : __code gotoOtherInterface(struct StackTest2Impl* stackTest2, struct Stack* stack, union Data* data1, struct StackTest* stackTest, __code next(...)) {
+[getDataGear] match 244 :   goto stack->push(data1, stackTest->pop2Test);
+[generateDataGear] match 655 : #include "../../../context.h"
+[generateDataGear] match 650 : #interface "StackTest2.h"
+[generateDataGear] match 783 :
+[generateDataGear] match 783 : // ----
+[generateDataGear] match 783 : // typedef struct StackTest2Impl <Self, Isa> impl StackTest2 {
+[generateDataGear] match 783 : //   __code next(...);
+[generateDataGear] match 783 : // } StackTest2Impl;
+[generateDataGear] match 783 : // ----
+[generateDataGear] match 783 :
+[generateDataGear] match 783 : StackTest2* createStackTest2Impl(struct Context* context) {
+[generateDataGear] match 783 :     struct StackTest2* stackTest2  = new StackTest2();
+[generateDataGear] match 783 :     struct StackTest2Impl* stack_test2impl = new StackTest2Impl();
+[generateDataGear] match 783 :     stackTest2->stackTest2 = (union Data*)stack_test2impl;
+[generateDataGear] match 783 :     stackTest2->insertTest1 = C_insertTest1_StackTest2Impl;
+[generateDataGear] match 783 :     return stackTest2;
+[generateDataGear] match 783 : }
+[generateDataGear] match 783 :
+[generateDataGear] match 674 : __code insertTest1_StackTest2Impl(struct StackTest2Impl* stackTest2, struct Stack* stack, union Data* data1, __code next(...)) {
+[generateDataGear] match 788 :     goto stack->push(data1, next);
+[generateDataGear] match 1030 : }
+[generateDataGear] match 1054 : }
+[generateDataGear] match 783 :
+[generateDataGear] match 674 : __code gotoOtherInterface(struct StackTest2Impl* stackTest2, struct Stack* stack, union Data* data1, struct StackTest* stackTest, __code next(...)) {
+[generateDataGear] match 788 :   goto stack->push(data1, stackTest->pop2Test);
+[generateDataGear] match 1030 : }
+[generateDataGear] match 1054 : }
+[generateDataGear] match 783 :
+[generateDataGear] match 783 :
+```
+
+
+# generics関連
+- 今までのヘッダーファイルの`typedef struct SingleLinkedStack <Type, Impl> {`の`<Type, Impl>`がこれと言った意味がなかった
+    - 一種の特殊変数(型エイリアス)っぽく使っていたけれど、特に意味がなかった
+    - 型エイリアスならグローバルで定義(== Gearsの構文としてサポートしているべき)な気がする
+- いらんそうなので全部削除した
+- 今まで使っていた型はデフォルトで定義していることにしたい
+    - `Self`
+    - `Impl`
+
+```c
+typedef struct Stack<>{
+        __code clear(Impl* stack,__code next(...));
+        __code push(Impl* stack,union Data* data, __code next(...));
+        __code pop(Impl* stack, __code next(union Data* data, ...));
+        __code pop2(Impl* stack, __code next(union Data* data, union Data* data1, ...));
+        __code isEmpty(Impl* stack, __code next(...), __code whenEmpty(...));
+        __code get(Impl* stack, __code next(union Data* data, ...));
+        __code get2(Impl* stack, __code next(union Data* data, union Data* data1, ...));
+        __code next(...);
+        __code whenEmpty(...);
+} Stack;
+```
+
+
+# genericsの使用例
+
+いくつかのパターンが存在する
+
+## 型宣言時にgenericsを使用する
+
+- `<>`の中に型変数を導入する
+    - genericsになる
+- 複数存在しても可能
+- genericsが満たしていてほしいInterfaceを`:`のあとに続けてかける
+    - この場合はSayは保証される
+    - 保証はコンパイルタイム (Perl level)
+    - 実行時タイム (cbc level)
+
+```c
+typedef struct GenericsTest <T:Say> {
+  __code print(Impl* generics_test, T* pointer, __code next(...));
+  __code print2(Impl* generics_test, D* integer, __code next(...));
+  __code next(...);
+} GenericsTest;
+```
+
+
+- Tの境界が指定されていない場合
+    - 置き換えられるかの確認
+    - 置き換えられそうならコードを生成する
+        - 型(header)
+        - CodeGear
+- Tの境界が指定されている場合
+    - 型チェック
+        - data gearの同一性
+        - primitive typeはwrapeperをいれる?
+    - 置き換えられそうなら置換する
+- Genericsを使っている対象がInterfaceの場合はめんどう
+    - いずれかのImpl側で実装している必要がある
+    - どのImplがどのInterfaceの実装なのかはPerlレベルで判定済み
+        - generate_contextあたりで判定したい
+- `c/`以下に型名でファイルを生成して、それをコンパイル時に使う
+    - generate_stubからc/以下をアクセスする必要がある
+
+
+## 現状
+
+- とりあえずgenerics使っている箇所の検知まで到達
+    - `Interface_Generics`の命名規則
+    - `AtomicT_Int`みたいに変換される
+
+```c
+typedef struct PhilsImpl <> impl Phils {
+  int self;
+  AtomicT<int> Leftfork;
+  Atomic<int> Rightfork;
+  __code next(...);
+} PhilsImpl;
+```
+
+```c
+$ perl tools/check_convert_context_struct.pl examples/DPP/PhilsImpl.h
+[INFO] use generics AtomicT int at AtomicT<int> Leftfork;
+[INFO] use generics Atomic int at Atomic<int> Rightfork;
+    struct PhilsImpl {
+        int self;
+        AtomicT_Int Leftfork;
+        Atomic_Int Rightfork;
+        enum Code next;
+    } PhilsImpl;
+```
+
+## codeGearの内部で別のgenericsを使うケース
+
+```c
+typedef struct GenericsTest <T:Say, D> {
+  __code print(Impl* generics_test, T* pointer, __code next(...));
+  __code print2(Impl* generics_test, D* integer, __code next(...));
+  __code print3(Impl* generics_test, AtomicT<int>* atomic_t, __code next(...));
+  __code next(...);
+} GenericsTest;
+```
+
+```c
+$ perl tools/check_convert_context_struct.pl examples/sandbox/GenericsTest.h
+    struct GenericsTest {
+        union Data* generics_test;
+        T* pointer;
+        D* integer;
+        AtomicT_int* atomic_t;
+        enum Code print;
+        enum Code print2;
+        enum Code print3;
+        enum Code next;
+    } GenericsTest;
+```
+
+```c
+$ perl tools/check_convert_context_struct.pl examples/sandbox/GenericsTest.h
+    struct GenericsTest {
+        union Data generics_test*;
+        GENERICS pointer*;
+        GENERICS integer*;
+        AtomicT_int atomic_t*;
+        enum Code print;
+        enum Code print2;
+        enum Code print3;
+        enum Code next;
+    } GenericsTest;
+```
+
+## context.hのぬけ
+
+- さっき直した
+    - context.hの中身を回収する正規表現がちょっとバグってた
+
+
+```c
+#endif
+    ///home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/AtomicT.h
+#ifndef ATOMICT_STRUCT
+    struct AtomicT {
+        union Data* atomicTImpl;
+        union Data newData;
+        union Data init;
+        enum Code checkAndSet;
+        enum Code set;
+        enum Code next;
+        enum Code fail;
+    } AtomicT;
+#define ATOMICT_STRUCT
+#else
+    struct AtomicT;
+#endif
+```
--- a/user/ikkun/memo/2020/12/15.md	Sun Jan 10 00:10:03 2021 +0900
+++ b/user/ikkun/memo/2020/12/15.md	Wed Jan 13 00:10:04 2021 +0900
@@ -15,7 +15,7 @@
 
 * 1_序論(研究目的、背景）
 * 2_モデル検査によるアプローチ（他のモデル検査ツール、CｂCによる検証、goto）
-* 3_GearsOSによるモデル検査手法（DPP、タブロー展開、）
+* 3_GearsOSによるモデル検査手法（DPP、）
 * 4_GearsOS上での実装（pargoto、synchronizedqueue、cpuworker、statmantDB、memoryTree
  pargoto でのphilsの起動
  cpuworkerをSynchronizedqueueのCaS優先に
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/soto/log/2021-01-12.md	Wed Jan 13 00:10:04 2021 +0900
@@ -0,0 +1,105 @@
+# 研究目的
+
+- OSやアプリケーションの信頼性を高めることは重要な課題である。
+
+- 研究室でCbCという言語を開発している。その信頼性を証明したい。
+    - CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。
+
+- cbcはサブルーチンとループ制御をcから取り除いている。その為、それを実装した際のプログラムを検証をする必要がある。
+
+- プログラムの検証手法のひとつに、Hoare Logic がある。
+    - これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というものである。
+
+    - つまり、関数が任意の値が引数として実行された際に、任意の値が帰ってきた場合を「関数は正常に実行される」といえる。
+
+    - CbC では実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。それを繋げていくため、個々の関数の正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。
+
+
+- cbcの実行を継続するという性質に Hoare Logicを連続して用いると、個々の関数の正当性の証明と接続の健全性について証明する事でプログラム全体の検証を行う事ができる。
+
+- これらのことから、Hoare Logicを用いてCbCを検証する。
+
+
+- 先行研究ではCbCにおけるWhileLoopの検証を行なった。
+
+- agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である赤黒木の検証を行う
+
+## 今週の進捗
+- 検証用に順序要素を持ったListを作成
+
+- RBTのmeta部分に順序要素を持ったListを使用した。
+
+- WindowsでAgdaを動かせるようになりました。
+
+- マインドマップを若干書きました。
+
+### 順序要素を持ったList
+fresh listは難しすぎた… \
+ひとまずこれでやってみたかった。
+
+定義
+```Agda
+mutual
+  data  right-List : Set where
+    [] : right-List
+    [_] : ℕ → right-List
+    _∷>_Cond_ : (x : ℕ) → (xs : right-List ) → (p : x Data.Nat.> top-r xs) → right-List
+
+  top-r : right-List → ℕ
+  top-r [] = {!!}
+  top-r [ x ] = x
+  top-r (x ∷> l Cond x₁) = x
+```
+
+insert
+```Agda
+mutual
+  insert-r : ℕ → right-List → right-List
+  insert-r x [] = [ x ]
+  insert-r x l@([ y ]) with <-cmp x y
+  ... | tri< a ¬b ¬c = l
+  ... | tri≈ ¬a b ¬c = l
+  ... | tri> ¬a ¬b c = x ∷> l Cond c
+  insert-r x l@(y ∷> ys Cond p) with <-cmp x y
+  ... | tri< a ¬b ¬c = l
+  ... | tri≈ ¬a b ¬c = l
+  ... | tri> ¬a ¬b c = x ∷> l Cond c
+```
+
+- Listのtopと比較してそれより(大きい/小さい)場合にListに追加するというもの
+
+### RBTのmetaに追加する
+
+metaの作成はひとまず再帰的に書いて上の順序を持ったListを持つようにしました。
+
+### WindowsでAgda
+文献が全く見つからずに難航した。
+Spacemacsを使ってAgdaを書けるようになりました。
+
+以下手順
+
+- chocolateという謎のHaskellを入れるツールを使った。
+    - こいつでghcとcabalをインストール
+
+- Darcsのコードを取ってくる。そのディレクトリに入って`cabal -f-curl install`
+
+- AgdaのコードをGitHubから取ってきて、そこでまた `cabal -f-curl install` でAgdaが入った。
+
+- そこからDeja-vuフォントをinstallし設定するとコンパイル時に文字化けせずAgdaが使えるようになりました。
+
+### マインドマップ
+感覚で書きました。
+
+## 余談
+- 今後
+    - 検証を進める
+        - Hoare Logic で(Pre / Post) Condition を使って 検証する
+        - 赤のnodeの下に黒のnodeがないことを確かめる。
+        - 黒nodeの数が全て正しいか
+        - 深さがlogn以下であるか
+    - 健全性についてやる
+    - find, deleteを実装して上のやつを対応する
+
+- 院試の書類提出しました。
+    - どうやって対策するか考え中
+    - スライドを作成しようかなと思っています。
\ No newline at end of file