changeset 906:7dd8df7ceb69

fix
author ikkun <ikkun@cr.ie.u-ryukyu.ac.jp>
date Wed, 27 Jan 2021 21:17:37 +0900
parents 840458851072
children 013edcfe6f43
files src/parallel_execution/MCTaskManagerImpl.h src/parallel_execution/MCWorker.h src/parallel_execution/ModelChecking/MCWorker.cbc src/parallel_execution/examples/DPPMC/PhilsImpl.cbc src/parallel_execution/examples/DPPMC/main.cbc src/parallel_execution/lib/Gears/Template/Context.pm
diffstat 6 files changed, 29 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/MCTaskManagerImpl.h	Wed Jan 27 19:03:34 2021 +0900
+++ b/src/parallel_execution/MCTaskManagerImpl.h	Wed Jan 27 21:17:37 2021 +0900
@@ -7,6 +7,8 @@
   struct Queue* activeQueue;
   struct Worker** workers;
   struct Element* taskList;
+  MemoryPtr mem; // modelchecking memorylenge
+  StateDB state_db;
   int loopCounter;
   int cpu;
   int gpu;
--- a/src/parallel_execution/MCWorker.h	Wed Jan 27 19:03:34 2021 +0900
+++ b/src/parallel_execution/MCWorker.h	Wed Jan 27 21:17:37 2021 +0900
@@ -8,11 +8,11 @@
   struct Context* context; //simulated task
   struct Context* mcContext; // context for mcWorker
   struct Context* masterContext; // context for McTaskManager (singleton)
+  struct TaskManager* taskManager;
   int id;
   int loopCounter;
   struct Queue* mcQueue; // simulated task queue par thread
   enum Code nextStep;
-  StateNode st;
   TaskIterator* task_iter;
   int depth;
   int count;
--- a/src/parallel_execution/ModelChecking/MCWorker.cbc	Wed Jan 27 19:03:34 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.cbc	Wed Jan 27 21:17:37 2021 +0900
@@ -28,6 +28,7 @@
     mcWorker->masterContext = context; //singleton
     mcWorker->loopCounter = 0;
     mcWorker->nextStep = C_startModelChecker;
+    mcWorker->taskManager = context->taskManager;
     worker->taskReceive = C_taskReceiveMCWorker;
     worker->shutdown = C_shutdownMCWorker;
     srandom(time(NULL));
@@ -39,6 +40,7 @@
     struct MCWorker* mcWorker = &worker->worker->MCWorker;
     mcWorker->context = NEW(struct Context);
     initContext(mcWorker->context);
+    mcWorker->context->worker = worker;
     Gearef(mcWorker->context, Worker)->worker = (union Data*)worker;
     Gearef(mcWorker->context, Worker)->tasks = worker->tasks;
     goto meta(mcWorker->context, worker->taskReceive);
@@ -62,7 +64,8 @@
     for (int i = 0; i <= length; i++) {
         struct Element* tmpElem = getElementByIdx(mcQueue, i);
         struct Context* tmpContext = (struct Context*)tmpElem->data;
-        worker->st.memory = add_memory(&tmpContext->next, sizeof(enum Code), &context->mem);
+	MCTaskManagerImpl *mcti = (struct MCTaskManagerImpl *)worker->taskManager->taskManager;
+	add_memory(&tmpContext->next, sizeof(enum Code), &mcti->mem);
     }
     goto meta(ncontext, ncontext->next);
 }
@@ -77,14 +80,16 @@
     struct MCWorker* mcworker =  (struct MCWorker*) context->worker->worker;
     StateDB out = NULL;
     struct Context* list = NULL;
-
-    mcworker->st.hash = get_memory_hash(context->mem,0);
-    if (lookup_StateDB(&mcworker->st, &mcworker->masterContext->state_db, &out)) {
+    struct MCTaskManagerImpl* mcti = (struct MCTaskManagerImpl *)mcworker->taskManager->taskManager;
+    StateNode st;
+    st.memory = mcti->mem;
+    st.hash = get_memory_hash(mcti->mem,0);
+    if (lookup_StateDB(&st, &mcti->state_db, &out)) {
     // found in the state database
     //printf("found %d\n",count);
-      while(!(list = (struct Context*)takeNextIterator(task_iter))) {
+      while(!(list = (struct Context*)takeNextIterator(mcworker->task_iter))) {
           // no more branch, go back to the previous one
-          TaskIterator* prev_iter = task_iter->prev;
+          TaskIterator* prev_iter = mcworker->task_iter->prev;
           if (!prev_iter) {
             printf("All done count %d\n",mcworker->count);
             memory_usage();
@@ -92,19 +97,19 @@
           }
           //printf("no more branch %d\n",count);
           mcworker->depth--;
-          freeIterator(task_iter);
+          freeIterator(mcworker->task_iter);
           mcworker->task_iter = prev_iter;
       }
       // return to previous state
       //    here we assume task list is fixed, we don't have to
       //    recover task list itself
-      restore_memory(task_iter->state->memory);
+      restore_memory(mcworker->task_iter->state->memory);
       //printf("restore list %x next %x\n",(int)list,(int)(list->next));
     } else {
       // one step further
       mcworker->depth++;
       struct SingleLinkedQueue* mcSingleQueue = (struct SingleLinkedQueue*)mcworker->mcQueue->queue;
-      mcworker->task_iter = createQueueIterator(mcSingleQueue->top->next,out,task_iter);
+      mcworker->task_iter = createQueueIterator(mcSingleQueue->top->next,out,mcworker->task_iter);
     }
     //printf("depth %d count %d\n", depth, count++);
     mcworker->count++;
--- a/src/parallel_execution/examples/DPPMC/PhilsImpl.cbc	Wed Jan 27 19:03:34 2021 +0900
+++ b/src/parallel_execution/examples/DPPMC/PhilsImpl.cbc	Wed Jan 27 21:17:37 2021 +0900
@@ -33,11 +33,11 @@
     return phils;
 }
 
-MemoryPtr addMemoryPhilsImpl(struct Context* context, struct PhilsImpl* phils) {
+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), &context->mem);
-     return add_memory(&left->atomic, sizeof(int), &context->mem);
+     add_memory(&right->atomic, sizeof(int), &mcti->mem);
+     add_memory(&left->atomic, sizeof(int), &mcti->mem);
 }
 
 
--- a/src/parallel_execution/examples/DPPMC/main.cbc	Wed Jan 27 19:03:34 2021 +0900
+++ b/src/parallel_execution/examples/DPPMC/main.cbc	Wed Jan 27 21:17:37 2021 +0900
@@ -10,6 +10,8 @@
 #interface "Fork.h"
 #interface "AtomicT_int.h"
 
+extern void addMemoryPhilsImpl(MCTaskManagerImpl *mcti, struct PhilsImpl* phils);
+
 int cpu_num = 1;
 int length = 102400;
 int split = 8;
@@ -45,12 +47,18 @@
     AtomicT_int* fork2 = createAtomicT_intImpl_int(context,-1); // model checking : fork2
     AtomicT_int* fork3 = createAtomicT_intImpl_int(context,-1); // model checking : fork3
     AtomicT_int* fork4 = createAtomicT_intImpl_int(context,-1); // model checking : fork4
-
+    struct MCTaskManagerImpl *mcti = (struct MCTaskManagerImpl *)taskManager->taskManager;
+					     
     Phils* phils0 = createPhilsImpl(context,0,fork0,fork1); // model checking : phils0
+    addMemoryPhilsImpl(mcti,(struct PhilsImpl*)phils0->phils);
     Phils* phils1 = createPhilsImpl(context,1,fork1,fork2); // model checking : phils1
+    addMemoryPhilsImpl(mcti,(struct PhilsImpl*)phils1->phils);
     Phils* phils2 = createPhilsImpl(context,2,fork2,fork3); // model checking : phils2
+    addMemoryPhilsImpl(mcti,(struct PhilsImpl*)phils2->phils);
     Phils* phils3 = createPhilsImpl(context,3,fork3,fork4); // model checking : phils3
+    addMemoryPhilsImpl(mcti,(struct PhilsImpl*)phils3->phils);
     Phils* phils4 = createPhilsImpl(context,4,fork4,fork0); // model checking : phils4
+    addMemoryPhilsImpl(mcti,(struct PhilsImpl*)phils4->phils);
 
     par goto phils0->thinking(exit_code);
     par goto phils1->thinking(exit_code);
--- a/src/parallel_execution/lib/Gears/Template/Context.pm	Wed Jan 27 19:03:34 2021 +0900
+++ b/src/parallel_execution/lib/Gears/Template/Context.pm	Wed Jan 27 21:17:37 2021 +0900
@@ -156,8 +156,6 @@
     /* multi dimension parameter */
     int iterate;
     struct Iterator* iterator;
-    MemoryPtr mem;
-    StateDB state_db;
 };
 
 typedef int Int;