--- a/src/parallel_execution/DebugTaskManagerImpl.cbc	Tue Jan 18 19:54:28 2022 +0900
+++ b/src/parallel_execution/DebugTaskManagerImpl.cbc	Mon Jan 24 17:05:11 2022 +0900
@@ -14,7 +14,7 @@
 
 // DebugTaskManagerの作成。enumや変数の初期化を行う。
 TaskManager* createDebugTaskManagerImpl(struct Context* context, int numCPU, int numGPU, int numIO) {
-    printf("[Debug log] createDebugTaskManagerImpl in DebugTaskManager\n");
+    // printf("[Debug log] createDebugTaskManagerImpl in DebugTaskManager\n");
     // TaskManager構造体の生成および、構造体で定義された関数とenumの紐付け。
     struct TaskManager* taskManager = new TaskManager();
     taskManager->spawnTasks = C_spawnTasksDebugTaskManagerImpl;
@@ -48,7 +48,7 @@
 
 // workerの作成。CPUやGPU, モデル検査など環境によって作成するWorkerを変更する。
 void createWorkers(struct Context* context, DebugTaskManagerImpl* taskManager) {
-    printf("[Debug log] createWorkers in DebugTaskManager\n");
+    // printf("[Debug log] createWorkers in DebugTaskManager\n");
     int i = 0;
     taskManager->workers = (Worker**)ALLOCATE_PTR_ARRAY(context, Worker, taskManager->maxCPU);
     for (;i<taskManager->gpu;i++) {
@@ -71,13 +71,13 @@
 
 // 一連のspawnTaskの始動関数
 __code spawnTasksDebugTaskManagerImpl(struct DebugTaskManagerImpl* taskManager, struct Element* taskList, __code next1(...)) {
-    printf("[Debug log] spawnTaskDebugTaskManagerImpl in DebugTaskManager\n");
+    // printf("[Debug log] spawnTaskDebugTaskManagerImpl in DebugTaskManager\n");
     taskManager->taskList = taskList;
     goto spawnTasksDebugTaskManagerImpl1();
 }
 
 __code spawnTasksDebugTaskManagerImpl1(struct DebugTaskManagerImpl* taskManagerImpl, struct TaskManager* taskManager) {
-    printf("[Debug log] spawnTasksDebugTaskManagerImpl1 in DebugTaskManager\n");
+    // printf("[Debug log] spawnTasksDebugTaskManagerImpl1 in DebugTaskManager\n");
     // TaskListにTaskがない場合
     if (taskManagerImpl->taskList == NULL) {
         goto spawnTasksDebugTaskManagerImpl2();
@@ -95,13 +95,13 @@
 }
 
 __code spawnTasksDebugTaskManagerImpl2(struct DebugTaskManagerImpl* taskManager, struct Element* taskList, __code next1(...)) {
-    printf("[Debug log] spawnTasksDebugTaskManagerImpl2 DebugTaskManager\n");
+    // printf("[Debug log] spawnTasksDebugTaskManagerImpl2 DebugTaskManager\n");
     taskManager->taskList = taskList;
     goto spawnTasksDebugTaskManagerImpl3();
 }
 
 __code spawnTasksDebugTaskManagerImpl3(struct DebugTaskManagerImpl* taskManagerImpl, __code next1(...), struct TaskManager* taskManager) {
-    printf("[Debug log] spawnTasksDebugTaskManagerImpl3 in DebugTaskManager\n");
+    // printf("[Debug log] spawnTasksDebugTaskManagerImpl3 in DebugTaskManager\n");
     if (taskManagerImpl->taskList == NULL) {
         // struct Queue* tasks = taskManagerImpl->workers[0]->tasks;
         // printf("put NULL\n");
@@ -122,7 +122,7 @@
 
 // TaskをQueueにputする
 __code setWaitTaskDebugTaskManagerImpl(struct DebugTaskManagerImpl* taskManager, struct Context* task, __code next(...)) {
-    printf("[Debug log] setWaitTaskDebugTaskManagerImpl in DebugTaskManager\n");
+    // printf("[Debug log] setWaitTaskDebugTaskManagerImpl in DebugTaskManager\n");
     int i = taskManager->loopCounter;
     if (task->idg+i < task->maxIdg) {
         struct Queue* queue = GET_WAIT_LIST(task->data[task->idg + i]);
@@ -134,19 +134,19 @@
 }
 
 __code incrementTaskCountDebugTaskManagerImpl(struct DebugTaskManagerImpl* taskManager, __code next(...)) {
-    printf("[Debug log] incrementTaskCountDebugTaskManagerImpl in DebugTaskManager\n");
+    // printf("[Debug log] incrementTaskCountDebugTaskManagerImpl in DebugTaskManager\n");
     __sync_fetch_and_add(&taskManager->taskCount, 1);
     goto next(...);
 }
 
 __code decrementTaskCountDebugTaskManagerImpl(struct DebugTaskManagerImpl* taskManager, __code next(...)) {
-    printf("[Debug log] decrementTaskCountDebugTaskManagerImpl in DebugTaskManager\n");
+    // printf("[Debug log] decrementTaskCountDebugTaskManagerImpl in DebugTaskManager\n");
     __sync_fetch_and_sub(&taskManager->taskCount, 1);
     goto next(...);
 }
 
 __code spawnDebugTaskManagerImpl(struct DebugTaskManagerImpl* taskManagerImpl, struct Context* task, __code next(...), struct TaskManager* taskManager) {
-    printf("[Debug log] spawnDebugTaskManagerImpl in DebugTaskManager\n");
+    // printf("[Debug log] spawnDebugTaskManagerImpl in DebugTaskManager\n");
     task->taskManager = taskManager;
     if (task->idgCount == 0) {
         // iterator task is normal task until spawned
@@ -174,7 +174,7 @@
 
 
 __code taskSend(struct DebugTaskManagerImpl* taskManager, struct Context* task, __code next(...)) {
-    printf("[Debug log] taskSend in DebugTaskManager\n");
+    // printf("[Debug log] taskSend in DebugTaskManager\n");
     // set workerId
     if (task->gpu) {
         goto taskSend1();
@@ -195,7 +195,7 @@
 }
 
 __code taskSend2(struct DebugTaskManagerImpl* taskManager, struct Context* task, __code next(...)) {
-    printf("[Debug log] taskSend2 in DebugTaskManager\n");
+    // printf("[Debug log] taskSend2 in DebugTaskManager\n");
     int workerId = taskManager->sendCPUWorkerIndex;
     if (++taskManager->sendCPUWorkerIndex >= taskManager->maxCPU) {
         taskManager->sendCPUWorkerIndex = taskManager->cpu;
@@ -207,7 +207,7 @@
 }
 
 __code shutdownDebugTaskManagerImpl(struct DebugTaskManagerImpl* taskManager, __code next(...)) {
-    printf("[Debug log] shutdownDebugTaskManagerImpl in DebugTaskManager\n");
+    // printf("[Debug log] shutdownDebugTaskManagerImpl in DebugTaskManager\n");
     if (taskManager->taskCount != 0) {
         usleep(1000);
         goto shutdownDebugTaskManagerImpl();
@@ -222,13 +222,13 @@
 }
 
 __code shutdownDebugTaskManagerImpl1(struct DebugTaskManagerImpl* taskManager, __code next(...)) {
-    printf("[Debug log] shutdownDebugTaskManagerImpl1 in DebugTaskManager\n");
+    // printf("[Debug log] shutdownDebugTaskManagerImpl1 in DebugTaskManager\n");
     taskManager->loopCounter++;
     goto shutdownDebugTaskManagerImpl();
 }
 
 __code shutdownDebugTaskManagerImpl2(struct DebugTaskManagerImpl* taskManager, __code next(...)) {
-    printf("[Debug log] shutdownDebugTaskManagerImpl2 in DebugTaskManager\n");
+    // printf("[Debug log] shutdownDebugTaskManagerImpl2 in DebugTaskManager\n");
     int i = taskManager->loopCounter;
     if (i < taskManager->numWorker) {
         pthread_join(taskManager->workers[i]->thread, NULL);

--- a/src/parallel_execution/DebugWorker/DebugWorker.cbc	Tue Jan 18 19:54:28 2022 +0900
+++ b/src/parallel_execution/DebugWorker/DebugWorker.cbc	Mon Jan 24 17:05:11 2022 +0900
@@ -8,16 +8,18 @@
 #interface "Worker.h"
 #interface "Iterator.h"
 #interface "Queue.h"
-
+#interface "SingleLinkedQueue.h"
 
 static void startWorker(Worker* worker);
 
+static int dump = 1;
+
 #define INPUT_BUFFER_SIZE 256
 #define NUM_OF_COMMAND 2
 
 // workerの作成、初期化、スレッド作成
 Worker* createDebugWorker(struct Context* context, int id, Queue* queue) {
-    printf("[Debug log] createDebugWorker in DebugWorker\n");
+    // printf("[Debug log] createDebugWorker in DebugWorker\n");
     struct Worker* worker = new Worker();
     struct DebugWorker* debugWorker = new DebugWorker();
     worker->worker = (union Data*)debugWorker;
@@ -35,25 +37,39 @@
     worker->taskReceive = C_taskReceiveDebugWorker;
     worker->shutdown = C_shutdownDebugWorker;
     pthread_create(&worker->thread, NULL, (void*)&startWorker, worker);
+
+    // context->worker = worker;
     return worker;
 }
 
 // スレッド用Contextの作成
 static void startWorker(struct Worker* worker) {
-    printf("[Debug log] startWorker in DebugWorker\n");
+    // printf("[Debug log] startWorker in DebugWorker\n");
     struct DebugWorker* debugWorker = &worker->worker->DebugWorker;
     debugWorker->context = NEW(struct Context);
     initContext(debugWorker->context);
     debugWorker->context->worker = worker;
     Gearef(debugWorker->context, Worker)->worker = (union Data*)worker;
     Gearef(debugWorker->context, Worker)->tasks = worker->tasks;
-    printf("[Debug log] finished startWorker in DebugWorker\n");
+
+    // init state DB
+    struct DebugTaskManagerImpl* debugTaskManagerImpl = (struct DebugTaskManagerImpl *)debugWorker->taskManager->taskManager;
+    StateNode st ;
+    StateDB out = &st;
+    out->memory = debugTaskManagerImpl->mem;
+    out->hash = get_memory_hash(debugTaskManagerImpl->mem,0);    
+    lookup_StateDB(out, &debugTaskManagerImpl->state_db, &out);
+    if (dump) {
+        dump_memory(debugTaskManagerImpl->mem);
+        printf(" flag %0x %p -> %p hash %0x \n", out->flag, debugWorker->parent, out, out->hash);
+    }
+
     goto meta(debugWorker->context, worker->taskReceive);
 }
 
 // task Queueからtaskの取得
 __code taskReceiveDebugWorker(struct DebugWorker* worker, struct Queue* tasks) {
-    printf("[Debug log] taskReceiveDebugWorker in debug worker\n");
+    // printf("[Debug log] taskReceiveDebugWorker in debug worker\n");
     goto tasks->take(getTaskDebugWorker);
 }
 
@@ -83,23 +99,32 @@
     goto debugMeta(context, context->next);
 }
 
+__ncode printTrace(struct Context* context, enum Code next) {
+    printf("[Debug log] print trace\n");
+
+    context->next = next; // remember next Code
+    
+    // TODO: stateDBに保存したメモリ状態をトレースとして表示させる
+    struct DebugWorker* debugWorker = (struct DebugWorker*) context->worker->worker;
+    struct DebugTaskManagerImpl* debugTaskManagerImpl = (struct DebugTaskManagerImpl *)debugWorker->taskManager->taskManager;
+
+    goto debugMeta(context, context->next);
+}
+
 __ncode debugMeta(struct Context* context, enum Code next) {
-    printf("[Debug log] debugMeta in DebugWorker\n");
+    // printf("[Debug log] debugMeta in DebugWorker\n");
     context->next = next; // remember next Code Gear
-    printf("start get debugWorker\n");
-    struct DebugWorker* debugWorker = (struct DebugWorker*) Gearef(context, Worker);
-	// struct DebugWorker* debugWorker = (struct DebugWorker*) context->worker->worker;
-    printf("finish get debugWorker\n");
+	struct DebugWorker* debugWorker = (struct DebugWorker*) context->worker->worker;
 	StateNode st;
 	StateDB out = &st;
     struct Element* list = NULL;
 	struct DebugTaskManagerImpl* debugTaskManagerImpl = (struct DebugTaskManagerImpl *)debugWorker->taskManager->taskManager;
 	out->memory = debugTaskManagerImpl->mem;
     out->hash = get_memory_hash(debugTaskManagerImpl->mem,0);
+    int found = visit_StateDB(out, &debugTaskManagerImpl->state_db, &out,debugWorker->visit);
     // debugTaskManagerImpl->statefunc(debugTaskManagerImpl, debugWorker, debugWorker->parent, out, debugWorker->checking);
 
     char command_arr[NUM_OF_COMMAND][INPUT_BUFFER_SIZE];
-
     while(1) {
         printf("\n(Gears Debugger) ");
         // ユーザーインプット処理
@@ -116,15 +141,15 @@
         }
         
         // checking for input
+        /*
         for (i = 0; i < NUM_OF_COMMAND; i++) {
             printf("command_arr[%d] : %s\n", i, command_arr[i]);
         }
+        */
         
         // next
         // nextする前にstateDBへ保存する処理を書きたい
         if (strcmp(command_arr[0], "next") == 0 || strcmp(command_arr[0], "n") == 0) {
-            dump_memory(debugTaskManagerImpl->mem);
-            // printf(" flag %0x %p -> %p hash %0x \n", out->flag, debugWorker->parent, out, out->hash);
             goto meta(context, context->next);       
         // quit
         } else if (strcmp(command_arr[0], "quit") == 0 || strcmp(command_arr[0], "q") == 0) {
@@ -140,6 +165,10 @@
         // pd(print DataGear)
         } else if (strcmp(command_arr[0], "pd") == 0){
             goto printDataGear(context, context->next, &command_arr[1]);
+        } else if (strcmp(command_arr[0], "pt") == 0){
+            goto printTrace(context, context->next);
+        } else if (strcmp(command_arr[0], "dump") == 0){
+            dump_memory(debugTaskManagerImpl->mem);
         //others    
         } else {
             printf("invalid input. Please enter correct debugger commands.\n");
@@ -148,9 +177,9 @@
 }
 
 __code getTaskDebugWorker(struct DebugWorker* debugWorker, struct Context* task, struct Worker* worker) {
-    printf("[Debug log] getTaskDebugWorker in DebugWorker\n");
+    // printf("[Debug log] getTaskDebugWorker in DebugWorker\n");
     if (!task) {
-        printf("debug worker take task finished\n");
+        // printf("debug worker take task finished\n");
         goto worker->shutdown();
     }
     printf("debug worker get task\n");
@@ -168,7 +197,7 @@
 }
 
 __code odgCommitDebugWorker(struct DebugWorker* worker, struct Context* task) {
-    printf("[Debug log] odgCommitDebugWorker in DebugWorker\n");
+    // printf("[Debug log] odgCommitDebugWorker in DebugWorker\n");
     if (task->iterate) {
         struct Iterator* iterator = task->iterator;
         goto iterator->barrier(task, odgCommitDebugWorker1, odgCommitDebugWorker6);
@@ -189,7 +218,7 @@
 }
 
 __code odgCommitDebugWorker1(struct DebugWorker* worker, struct Context* task) {
-    printf("[Debug log] odgCommitDebugWorker1 in DebugWorker\n");
+    // printf("[Debug log] odgCommitDebugWorker1 in DebugWorker\n");
     int i = worker->loopCounter;
     if (task->odg+i < task->maxOdg) {
         goto odgCommitDebugWorker2();
@@ -200,21 +229,21 @@
 }
 
 __code odgCommitDebugWorker2(struct DebugWorker* worker, struct Context* task) {
-    printf("[Debug log] odgCommitDebugWorker2 in DebugWorker\n");
+    // printf("[Debug log] odgCommitDebugWorker2 in DebugWorker\n");
     int i = worker->loopCounter;
     struct Queue* queue = GET_WAIT_LIST(task->data[task->odg+i]);
     goto queue->isEmpty(odgCommitDebugWorker3, odgCommitDebugWorker5);
 }
 
 __code odgCommitDebugWorker3(struct DebugWorker* worker, struct Context* task) {
-    printf("[Debug log] odgCommitDebugWorker3 in DebugWorker\n");
+    // printf("[Debug log] odgCommitDebugWorker3 in DebugWorker\n");
     int i = worker->loopCounter;
     struct Queue* queue = GET_WAIT_LIST(task->data[task->odg+i]);
     goto queue->take(odgCommitDebugWorker4);
 }
 
 __code odgCommitDebugWorker4(struct DebugWorker* worker, struct Context* task, struct Context* waitTask) {
-    printf("[Debug log] odgCommitDebugWorker4 in DebugWorker\n");
+    // printf("[Debug log] odgCommitDebugWorker4 in DebugWorker\n");
     if (__sync_fetch_and_sub(&waitTask->idgCount, 1) == 1) { // atomic decrement idg counter(__sync_fetch_and_sub function return initial value of waitTask->idgCount point)
         struct TaskManager* taskManager = waitTask->taskManager;
         goto taskManager->spawn(waitTask, odgCommitDebugWorker2);
@@ -233,18 +262,18 @@
 }
 
 __code odgCommitDebugWorker5(struct DebugWorker* worker, struct Context* task) {
-    printf("[Debug log] odgCommitDebugWorker5 in DebugWorker\n");
+    // printf("[Debug log] odgCommitDebugWorker5 in DebugWorker\n");
     worker->loopCounter++;
     goto odgCommitDebugWorker1();
 }
 
 __code odgCommitDebugWorker6(struct DebugWorker* worker, struct Context* task) {
-    printf("[Debug log] odgCommitDebugWorker6 in DebugWorker\n");
+    // printf("[Debug log] odgCommitDebugWorker6 in DebugWorker\n");
     struct Worker* taskWorker = task->worker;
     goto taskWorker->taskReceive(taskWorker->tasks);
 }
 
 __code shutdownDebugWorker(struct DebugWorker* worker) {
-    printf("[Debug log] shutdownDebugWorker in DebugWorker\n");
+    // printf("[Debug log] shutdownDebugWorker in DebugWorker\n");
     goto exit_code();
 }

--- a/src/parallel_execution/RedBlackTree.agda	Tue Jan 18 19:54:28 2022 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,145 +0,0 @@
-module RedBlackTree where
-
-open import stack
-open import Level
-
-record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
-  field
-    putImpl : treeImpl -> a -> (treeImpl -> t) -> t
-    getImpl  : treeImpl -> (treeImpl -> Maybe a -> t) -> t
-open TreeMethods
-
-record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
-  field
-    tree : treeImpl
-    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
-  putTree : a -> (Tree treeImpl -> t) -> t
-  putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
-  getTree : (Tree treeImpl -> Maybe a -> t) -> t
-  getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
-
-open Tree
-
-data Color {n : Level } : Set n where
-  Red   : Color
-  Black : Color
-
-data CompareResult {n : Level } : Set n where
-  LT : CompareResult
-  GT : CompareResult
-  EQ : CompareResult
-
-record Node {n : Level } (a k : Set n) : Set n where
-  inductive
-  field
-    key   : k
-    value : a
-    right : Maybe (Node a k)
-    left  : Maybe (Node a k)
-    color : Color {n}
-open Node
-
-record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where
-  field
-    root : Maybe (Node a k)
-    nodeStack : Stack {n} {m} (Node a k) {t} si
-    compare : k -> k -> CompareResult {n}
-
-open RedBlackTree
-
-open Stack
-
---
--- put new node at parent node, and rebuild tree to the top
---
-{-# TERMINATING #-}   -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html
-replaceNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-replaceNode {n} {m} {t} {a} {k} {si} tree s parent n0 next = popStack s (
-      \s grandParent -> replaceNode1 s grandParent ( compare tree (key parent) (key n0) ) )
-  where
-        replaceNode1 : Stack (Node a k) si -> Maybe ( Node a k ) -> CompareResult -> t
-        replaceNode1 s Nothing LT = next ( record tree { root = Just ( record parent { left = Just n0 ; color = Black } ) } )   
-        replaceNode1 s Nothing GT = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )   
-        replaceNode1 s Nothing EQ = next ( record tree { root = Just ( record parent { right = Just n0 ; color = Black } ) } )   
-        replaceNode1 s (Just grandParent) result with result
-        ... | LT =  replaceNode tree s grandParent ( record parent { left = Just n0 } ) next
-        ... | GT =  replaceNode tree s grandParent ( record parent { right = Just n0 } ) next
-        ... | EQ =  next tree 
-
-rotateRight : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node  a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-rotateRight {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
-
-rotateLeft : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-rotateLeft {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
-
-insertCase5 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertCase5 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
-
-insertCase4 : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> Node a k -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertCase4 {n} {m} {t} {a} {k} {si} tree s n0 parent grandParent next = {!!}
-
-{-# TERMINATING #-}
-insertNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) {t} si -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-insertNode {n} {m} {t} {a} {k} {si} tree s n0 next = get2Stack s (\ s d1 d2 -> insertCase1 s n0 d1 d2 )
-   where
-    insertCase1 : Stack (Node a k) si -> Node a k -> Maybe (Node a k) -> Maybe (Node a k) -> t    -- placed here to allow mutual recursion
-          -- http://agda.readthedocs.io/en/v2.5.2/language/mutual-recursion.html
-    insertCase3 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
-    insertCase3 s n0 parent grandParent with left grandParent | right grandParent
-    ... | Nothing | Nothing = insertCase4 tree s n0 parent grandParent next
-    ... | Nothing | Just uncle  = insertCase4 tree s n0 parent grandParent next
-    ... | Just uncle | _  with compare tree ( key uncle ) ( key parent )
-    ...                   | EQ =  insertCase4 tree s n0 parent grandParent next
-    ...                   | _ with color uncle
-    ...                           | Red = pop2Stack s ( \s p0 p1 -> insertCase1 s ( 
-           record grandParent { color = Red ; left = Just ( record parent { color = Black ; left = Just n0 } )  ; right = Just ( record uncle { color = Black } ) }) p0 p1 )
-    ...                           | Black = insertCase4 tree s n0 parent grandParent next
-    insertCase2 : Stack (Node a k) si -> Node a k -> Node a k -> Node a k -> t
-    insertCase2 s n0 parent grandParent with color parent
-    ... | Black = replaceNode tree s grandParent n0 next
-    ... | Red = insertCase3 s n0 parent grandParent
-    insertCase1 s n0 Nothing Nothing = next tree
-    insertCase1 s n0 Nothing (Just grandParent) = replaceNode tree s grandParent n0 next
-    insertCase1 s n0 (Just grandParent) Nothing = replaceNode tree s grandParent n0 next
-    insertCase1 s n0 (Just parent) (Just grandParent) = insertCase2 s n0 parent grandParent
-      where
-
-findNode : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t
-findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1)
-  where
-    findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t
-    findNode2 s Nothing = next tree s n0
-    findNode2 s (Just n) = findNode tree s n0 n next
-    findNode1 : Stack (Node a k) si -> (Node a k)  -> t
-    findNode1 s n1 with (compare tree (key n0) (key n1))
-    ...                                | EQ = next tree s n0 
-    ...                                | GT = findNode2 s (right n1)
-    ...                                | LT = findNode2 s (left n1)
-
-
-leafNode : {n : Level } {a k : Set n}  -> k -> a -> Node a k
-leafNode k1 value = record {
-    key   = k1 ;
-    value = value ;
-    right = Nothing ;
-    left  = Nothing ;
-    color = Black 
-  }
-
-putRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t
-putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree)
-...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
-...                                | Just n2  = findNode tree (nodeStack tree) (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next)
-
-getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> (RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> t) -> t
-getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree)
-  where
-    checkNode : Maybe (Node a k) -> t
-    checkNode Nothing = cs tree Nothing
-    checkNode (Just n) = search n
-      where
-        search : Node a k -> t
-        search n with compare tree k1 (key n)
-        search n | LT = checkNode (left n)
-        search n | GT = checkNode (right n)
-        search n | EQ = cs tree (Just n)

--- a/src/parallel_execution/examples/DebughelloWorld/HelloImpl.cbc	Tue Jan 18 19:54:28 2022 +0900
+++ b/src/parallel_execution/examples/DebughelloWorld/HelloImpl.cbc	Mon Jan 24 17:05:11 2022 +0900
@@ -15,7 +15,6 @@
 // ----
 
 Hello* createHelloImpl(struct Context* context) {
-    printf("[Debug log] createHelloImpl in HelloImpl\n");
     struct Hello* hello  = new Hello();
     struct HelloImpl* hello_impl = new HelloImpl();
     hello->hello = (union Data*)hello_impl;
@@ -27,14 +26,12 @@
     return hello;
 }
 __code h(struct HelloImpl* hello, __code next(...)) {
-    printf("[Debug log] h in HelloImpl\n");
     hello->hString = "Hello, "; //createImpl部分では_implなのだが動く
     printf("%s", hello->hString);
     goto w(hello, next);
 }
 
 __code w(struct HelloImpl* hello, __code next(...)) {
-    printf("[Debug log] w in HelloImpl\n");
     hello->wString = "World.\n";
     printf("%s", hello->wString);
     goto next(...);

--- a/src/parallel_execution/examples/DebughelloWorld/main.cbc	Tue Jan 18 19:54:28 2022 +0900
+++ b/src/parallel_execution/examples/DebughelloWorld/main.cbc	Mon Jan 24 17:05:11 2022 +0900
@@ -17,7 +17,7 @@
 int CPU_CUDA = -1;
 
 __code initDataGears(struct LoopCounter* loopCounter, struct TaskManager* taskManager) {
-    printf("[Debug log] initDataGears in main\n");
+    // printf("[Debug log] initDataGears in main\n");
     // loopCounter->tree = createRedBlackTree(context);
     loopCounter->i = 0;
     taskManager->taskManager = (union Data*)createDebugTaskManagerImpl(context, cpu_num, gpu_num, 0);
@@ -25,7 +25,7 @@
 }
 
 __code code1(struct LoopCounter* loopCounter) {
-    printf("[Debug log] code1 in main\n");
+    // printf("[Debug log] code1 in main\n");
     printf("cpus:\t\t%d\n", cpu_num);
     printf("gpus:\t\t%d\n", gpu_num);
     printf("length:\t\t%d\n", length);
@@ -35,14 +35,17 @@
 
 
 __code createTask1(struct LoopCounter* loopCounter, struct TaskManager* taskManager) {
-    printf("[Debug log] createTask1 in main\n");
+    // printf("[Debug log] createTask1 in main\n");
     Hello* hello = createHelloImpl(context);
-    goto hello->h(code2); 
+    struct DebugTaskManagerImpl *debugTaskManagerImpl = (struct DebugTaskManagerImpl *)context->taskManager->taskManager;
+    add_memory_range((void *)hello, sizeof(Hello), &debugTaskManagerImpl->mem);
+    par goto hello->h(code2); 
+    goto code2();
 }
 
 
 __code code2(struct TaskManager* taskManager) {
-    printf("[Debug log] code2 in main\n");
+    // printf("[Debug log] code2 in main\n");
     goto taskManager->shutdown(exit_code);
 }
 
@@ -51,7 +54,7 @@
 }
 
 void init(int argc, char** argv) {
-    printf("[Debug log] init in main\n");
+    // printf("[Debug log] init in main\n");
     for (int i = 1; argv[i]; ++i) {
         if (strcmp(argv[i], "-cpu") == 0)
             cpu_num = (int)atoi(argv[i+1]);
@@ -67,7 +70,7 @@
 }
 
 int main(int argc, char** argv) {
-    printf("[Debug log] main in main\n");
+    // printf("[Debug log] main in main\n");
     init(argc, argv);
     goto initDataGears();
 }

--- a/src/parallel_execution/stack.agda	Tue Jan 18 19:54:28 2022 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,255 +0,0 @@
-open import Level renaming (suc to succ ; zero to Zero )
-module stack  where
-
-open import Relation.Binary.PropositionalEquality
-open import Relation.Binary.Core
-open import Data.Nat
-
-ex : 1 + 2 ≡ 3
-ex = refl
-
-data Bool {n : Level } : Set n where
-  True  : Bool
-  False : Bool
-
-record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
-  field
-    pi1 : a
-    pi2 : b
-
-data Maybe {n : Level } (a : Set n) : Set n where
-  Nothing : Maybe a
-  Just    : a -> Maybe a
-
-record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
-  field
-    push : stackImpl -> a -> (stackImpl -> t) -> t
-    pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
-    pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
-    get  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
-    get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
-open StackMethods
-
-record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
-  field
-    stack : si
-    stackMethods : StackMethods {n} {m} a {t} si
-  pushStack :  a -> (Stack a si -> t) -> t
-  pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
-  popStack : (Stack a si -> Maybe a  -> t) -> t
-  popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
-  pop2Stack :  (Stack a si -> Maybe a -> Maybe a -> t) -> t
-  pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
-  getStack :  (Stack a si -> Maybe a  -> t) -> t
-  getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
-  get2Stack :  (Stack a si -> Maybe a -> Maybe a -> t) -> t
-  get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
-
-open Stack
-
-data Element {n : Level } (a : Set n) : Set n where
-  cons : a -> Maybe (Element a) -> Element a
-
-datum : {n : Level } {a : Set n} -> Element a -> a
-datum (cons a _) = a
-
-next : {n : Level } {a : Set n} -> Element a -> Maybe (Element a)
-next (cons _ n) = n
-
-
-{-
--- cannot define recrusive record definition. so use linked list with maybe.
-record Element {l : Level} (a : Set n l) : Set n (suc l) where
-  field
-    datum : a  -- `data` is reserved by Agda.
-    next : Maybe (Element a)
--}
-
-
-
-record SingleLinkedStack {n : Level } (a : Set n) : Set n where
-  field
-    top : Maybe (Element a)
-open SingleLinkedStack
-
-pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
-pushSingleLinkedStack stack datum next = next stack1
-  where
-    element = cons datum (top stack)
-    stack1  = record {top = Just element}
-
-
-popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
-popSingleLinkedStack stack cs with (top stack)
-...                                | Nothing = cs stack  Nothing
-...                                | Just d  = cs stack1 (Just data1)
-  where
-    data1  = datum d
-    stack1 = record { top = (next d) }
-
-pop2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
-pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
-...                                | Nothing = cs stack Nothing Nothing
-...                                | Just d = pop2SingleLinkedStack' {n} {m} stack cs
-  where
-    pop2SingleLinkedStack' : {n m : Level } {t : Set m }  -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
-    pop2SingleLinkedStack' stack cs with (next d)
-    ...              | Nothing = cs stack Nothing Nothing
-    ...              | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
-    
-
-getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
-getSingleLinkedStack stack cs with (top stack)
-...                                | Nothing = cs stack  Nothing
-...                                | Just d  = cs stack (Just data1)
-  where
-    data1  = datum d
-
-get2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
-get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
-...                                | Nothing = cs stack Nothing Nothing
-...                                | Just d = get2SingleLinkedStack' {n} {m} stack cs
-  where
-    get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
-    get2SingleLinkedStack' stack cs with (next d)
-    ...              | Nothing = cs stack Nothing Nothing
-    ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
-
-
-
-emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
-emptySingleLinkedStack = record {top = Nothing}
-
------
--- Basic stack implementations are specifications of a Stack
---
-singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
-singleLinkedStackSpec = record {
-                                   push = pushSingleLinkedStack
-                                 ; pop  = popSingleLinkedStack
-                                 ; pop2 = pop2SingleLinkedStack
-                                 ; get  = getSingleLinkedStack
-                                 ; get2 = get2SingleLinkedStack
-                           }
-
-createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
-createSingleLinkedStack = record {
-                             stack = emptySingleLinkedStack ;
-                             stackMethods = singleLinkedStackSpec 
-                           }
-
-----
---
--- proof of properties ( concrete cases )
---
-
-test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n}
-test01 stack _ with (top stack)
-...                  | (Just _) = True
-...                  | Nothing  = False
-
-
-test02 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Bool
-test02 stack = popSingleLinkedStack stack test01
-
-test03 : {n : Level } {a : Set n} -> a ->  Bool
-test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
-
--- after a push and a pop, the stack is empty
-lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
-lemma = refl
-
-testStack01 : {n m : Level } {a : Set n} -> a -> Bool {m}
-testStack01 v = pushStack createSingleLinkedStack v (
-   \s -> popStack s (\s1 d1 -> True))
-
--- after push 1 and 2, pop2 get 1 and 2
-
-testStack02 : {m : Level } ->  ( Stack  ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
-testStack02 cs = pushStack createSingleLinkedStack 1 (
-   \s -> pushStack s 2 cs)
-
-
-testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
-testStack031 2 1 = True
-testStack031 _ _ = False
-
-testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
-testStack032  (Just d1) (Just d2) = testStack031 d1 d2
-testStack032  _ _ = False
-
-testStack03 : {m : Level } -> Stack  ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
-testStack03 s cs = pop2Stack s (
-   \s d1 d2 -> cs d1 d2 )
-
-testStack04 : Bool
-testStack04 = testStack02 (\s -> testStack03 s testStack032)
-
-testStack05 : testStack04 ≡ True
-testStack05 = refl
-
-------
---
--- proof of properties with indefinite state of stack
---
--- this should be proved by properties of the stack inteface, not only by the implementation,
---    and the implementation have to provides the properties.
---
---    we cannot write "s ≡ s3", since level of the Set does not fit , but use stack s ≡ stack s3 is ok.
---    anyway some implementations may result s != s3
---  
-
-stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
-stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
-
-push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
-    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
-
-
-id : {n : Level} {A : Set n} -> A -> A
-id a = a
-
--- push a, n times
-
-n-push : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
-n-push zero s            = s
-n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s ) 
-
-n-pop :  {n : Level}{A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
-n-pop zero    s         = s
-n-pop  {_} {A} {a} (suc n) s = popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s )
-
-open ≡-Reasoning
-
-push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> (popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ) ≡ s
-push-pop-equiv s = refl
-
-push-and-n-pop : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {_} {A} {a} n s
-push-and-n-pop zero s            = refl
-push-and-n-pop {_} {A} {a} (suc n) s = begin
-   n-pop {_} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id)
-  ≡⟨ refl ⟩
-   popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
-  ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩ 
-   popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s)
-  ≡⟨ refl ⟩
-    n-pop {_} {A} {a} (suc n) s
-  ∎
-  
-
-n-push-pop-equiv : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> (n-pop {_} {A} {a} n (n-push {_} {A} {a} n s)) ≡ s
-n-push-pop-equiv zero s            = refl
-n-push-pop-equiv {_} {A} {a} (suc n) s = begin
-    n-pop {_} {A} {a} (suc n) (n-push (suc n) s)
-  ≡⟨ refl ⟩
-    n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
-  ≡⟨ push-and-n-pop n (n-push n s)  ⟩
-    n-pop {_} {A} {a} n (n-push n s)
-  ≡⟨ n-push-pop-equiv n s ⟩
-    s
-  ∎
-
-
-n-push-pop-equiv-empty : {n : Level} {A : Set n} {a : A} -> (n : ℕ) -> n-pop {_} {A} {a} n (n-push {_} {A} {a} n emptySingleLinkedStack)  ≡ emptySingleLinkedStack
-n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack