changeset 912:1d58c2f250ab

backtrack does not work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 28 Jan 2021 00:04:05 +0900
parents 6a619da280ff
children 49f519a0d079
files src/parallel_execution/MCTaskManagerImpl.cbc src/parallel_execution/ModelChecking/MCWorker.cbc src/parallel_execution/examples/DPPMC/PhilsImpl.cbc
diffstat 3 files changed, 14 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/MCTaskManagerImpl.cbc	Wed Jan 27 23:43:25 2021 +0900
+++ b/src/parallel_execution/MCTaskManagerImpl.cbc	Thu Jan 28 00:04:05 2021 +0900
@@ -86,7 +86,7 @@
 __code spawnTasksMCTaskManagerImpl3(struct MCTaskManagerImpl* taskManagerImpl, __code next1(...), struct TaskManager* taskManager) {
     if (taskManagerImpl->taskList == NULL) {
         struct Queue* tasks = taskManagerImpl->workers[0]->tasks;
-        printf("put NULL\n");
+        // printf("put NULL\n");
         goto tasks->put(NULL, shutdownMCTaskManagerImpl1);
 
     }
@@ -174,7 +174,7 @@
     }
     pthread_mutex_unlock(&taskManager->mutex);
     struct Queue* queue = taskManager->workers[workerId]->tasks;
-    printf("tasks->put taskSend1\n");
+    // printf("tasks->put taskSend1\n");
     goto queue->put(task, next(...));
 }
 
@@ -185,7 +185,7 @@
     }
     pthread_mutex_unlock(&taskManager->mutex);
     struct Queue* queue = taskManager->workers[workerId]->tasks;
-    printf("tasks->put taskSend2\n");
+    // printf("tasks->put taskSend2\n");
     goto queue->put(task, next(...));
 }
 
@@ -196,7 +196,7 @@
     }
     int workerId = taskManager->sendCPUWorkerIndex;
     struct Queue* tasks = taskManager->workers[workerId]->tasks;
-    printf("tasks->put shutdown\n");
+    // printf("tasks->put shutdown\n");
     goto tasks->put(NULL, shutdownMCTaskManagerImpl1);
 }
 
--- a/src/parallel_execution/ModelChecking/MCWorker.cbc	Wed Jan 27 23:43:25 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.cbc	Thu Jan 28 00:04:05 2021 +0900
@@ -14,6 +14,7 @@
 extern int lengthSingleLinkedQueue(struct SingleLinkedQueue* queue);
 extern Element* getElementByIdx(struct SingleLinkedQueue* queue, int idx);
 
+static int dump = 0;
 
 Worker* createMCWorker(struct Context* context, int id, Queue* queue) {
     struct Worker* worker = new Worker();
@@ -47,7 +48,7 @@
 }
 
 __code taskReceiveMCWorker(struct MCWorker* worker, struct Queue* tasks) {
-    printf("task receive mc worker\n");
+    // printf("task receive mc worker\n");
     goto tasks->take(getTaskMCWorker);
 }
 
@@ -65,7 +66,7 @@
         struct Element* tmpElem = getElementByIdx(mcQueue, i);
         struct Context* tmpContext = (struct Context*)tmpElem->data;
 	MCTaskManagerImpl *mcti = (struct MCTaskManagerImpl *)worker->taskManager->taskManager;
-	add_memory(&tmpContext->next, sizeof(enum Code), &mcti->mem);
+	add_memory_range(&tmpContext->next, sizeof(enum Code), &mcti->mem);
     }
     goto meta(ncontext, ncontext->next);
 }
@@ -84,11 +85,12 @@
     StateNode st;
     st.memory = mcti->mem;
     st.hash = get_memory_hash(mcti->mem,0);
-    dump_memory(mcti->mem);printf("\n");
+    if (dump) {
+        dump_memory(mcti->mem);printf("\n");
+    }
     if (lookup_StateDB(&st, &mcti->state_db, &out)) {
     // found in the state database
       // printf("found %d\n",count);
-      printf("found\n");
       while(!(list = (struct Context*)takeNextIterator(mcworker->task_iter))) {
           // no more branch, go back to the previous one
           TaskIterator* prev_iter = mcworker->task_iter->prev;
@@ -121,10 +123,10 @@
 
 __code getTaskMCWorker(struct MCWorker* mcWorker, struct Context* task, struct Worker* worker) {
     if (!task) {
-        printf("mc worker take end\n");
+        // printf("mc worker take end\n");
         goto startModelChecker(); // end thread
     }
-    printf("mc worker take\n");
+    // printf("mc worker take\n");
     task->worker = worker;
     //enum Code taskCg = task->next;
     struct Queue* mcQueue = mcWorker->mcQueue;
--- a/src/parallel_execution/examples/DPPMC/PhilsImpl.cbc	Wed Jan 27 23:43:25 2021 +0900
+++ b/src/parallel_execution/examples/DPPMC/PhilsImpl.cbc	Thu Jan 28 00:04:05 2021 +0900
@@ -36,8 +36,8 @@
 void addMemoryPhilsImpl(MCTaskManagerImpl *mcti, struct PhilsImpl* phils) {
      struct AtomicT_intImpl_int* right = (struct AtomicT_intImpl_int*)phils->Rightfork->atomicT_int;
      struct AtomicT_intImpl_int* left  = (struct AtomicT_intImpl_int*)phils->Leftfork->atomicT_int;
-     add_memory(&right->atomic, sizeof(int), &mcti->mem);
-     add_memory(&left->atomic, sizeof(int), &mcti->mem);
+     add_memory_range(&right->atomic, sizeof(int), &mcti->mem);
+     add_memory_range(&left->atomic, sizeof(int), &mcti->mem);
 }