changeset 933:03b02b9b7d1e

repeating
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Feb 2021 14:55:12 +0900
parents 8afa42bb9db7
children 296be5d6d524
files src/parallel_execution/MCTaskManagerImpl.cbc src/parallel_execution/MCTaskManagerImpl.h src/parallel_execution/ModelChecking/MCWorker.cbc src/parallel_execution/ModelChecking/MCWorker.h src/parallel_execution/examples/DPPMC/McDPP.cbc src/parallel_execution/examples/DPPMC/main.cbc
diffstat 6 files changed, 44 insertions(+), 36 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/MCTaskManagerImpl.cbc	Mon Feb 01 10:52:00 2021 +0900
+++ b/src/parallel_execution/MCTaskManagerImpl.cbc	Mon Feb 01 14:55:12 2021 +0900
@@ -1,8 +1,8 @@
 #include "../context.h"
 #interface "TaskManager.h"
 #interface "Iterator.h"
-#interface "Queue.h"
-#interface "Worker.h"
+#interface "Queue.h" 
+#interface "Worker.h" 
 
 #include <stdio.h>
 #include <unistd.h>
--- a/src/parallel_execution/MCTaskManagerImpl.h	Mon Feb 01 10:52:00 2021 +0900
+++ b/src/parallel_execution/MCTaskManagerImpl.h	Mon Feb 01 14:55:12 2021 +0900
@@ -13,7 +13,6 @@
   int cpu;
   int gpu;
   int io;
-  int visit;
   int maxCPU;
   void (*statefunc)(struct MCTaskManagerImpl* mcti, struct MCWorker* mcworker, StateDB now,StateDB next);
   __code next(...);
--- a/src/parallel_execution/ModelChecking/MCWorker.cbc	Mon Feb 01 10:52:00 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.cbc	Mon Feb 01 14:55:12 2021 +0900
@@ -1,8 +1,8 @@
 #include "../../context.h"
-#include <stdio.h>
-#include <stdlib.h>
-#include <time.h>
-#include "state_db.h"
+#include <stdio.h> 
+#include <stdlib.h> 
+#include <time.h> 
+#include "ModelChecking/state_db.h" 
 
 #interface "TaskManager.h"
 #interface "Worker.h"
@@ -25,10 +25,10 @@
     mcWorker->id = id;
     mcWorker->depth = 0;
     mcWorker->count = 0;
+    mcWorker->change = 0;
     mcWorker->mcContext = NULL;
     mcWorker->masterContext = context; //singleton
     mcWorker->loopCounter = 0;
-    mcWorker->nextStep = C_startModelChecker;
     mcWorker->taskManager = context->taskManager;
     worker->taskReceive = C_taskReceiveMCWorker;
     worker->shutdown = C_shutdownMCWorker;
@@ -75,6 +75,7 @@
     worker->task_iter = createQueueIterator(mcQueue->top->next,out,NULL);
     worker->parent = out;
     worker->root   = out;
+    worker->visit   = 0;
     goto meta(ncontext, ncontext->next);
 }
 
@@ -98,58 +99,60 @@
 
 __ncode mcMeta(struct Context* context, enum Code next) {
     context->next = next; // remember next Code Gear
-    struct MCWorker* mcworker =  (struct MCWorker*) context->worker->worker;
+    struct MCWorker* mcWorker =  (struct MCWorker*) context->worker->worker;
     StateNode st ;
     StateDB out = &st;
     struct Element* list = NULL;
-    struct MCTaskManagerImpl* mcti = (struct MCTaskManagerImpl *)mcworker->taskManager->taskManager;
+    struct MCTaskManagerImpl* mcti = (struct MCTaskManagerImpl *)mcWorker->taskManager->taskManager;
     out->memory = mcti->mem;
     out->hash = get_memory_hash(mcti->mem,0);
     if (dump) {
         dump_memory(mcti->mem);printf("\n");
     }
-    int found = visit_StateDB(out, &mcti->state_db, &out,mcti->visit);
-    mcti->statefunc(mcti, mcworker, mcworker->parent, out);
+    int found = visit_StateDB(out, &mcti->state_db, &out,mcWorker->visit);
+    mcti->statefunc(mcti, mcWorker, mcWorker->parent, out);
     if (found) {
       // found in the state database
       // printf("found %d\n",count);
-      while(!(list = takeNextIterator(mcworker->task_iter))) {
+      while(!(list = takeNextIterator(mcWorker->task_iter))) {
           // no more branch, go back to the previous one
-          TaskIterator* prev_iter = mcworker->task_iter->prev;
+          TaskIterator* prev_iter = mcWorker->task_iter->prev;
           if (!prev_iter) {
-            printf("All done count %d\n",mcworker->count);
+            printf("All done count %d repeat %d\n",mcWorker->count,mcWorker->visit);
             memory_usage();
-            if (mcti->visit == 1) {
+            if (! mcWorker->change) {
               exit(0);
             } else {
-		mcti->visit++;
+                mcWorker->change = 0;
+		mcWorker->visit++;
                 // start from root state and iterator
-                mcworker->depth = 0;
-                struct SingleLinkedQueue* mcSingleQueue = (struct SingleLinkedQueue*)mcworker->mcQueue->queue;
-                mcworker->task_iter = createQueueIterator(mcSingleQueue->top->next,mcworker->root,NULL);
+                mcWorker->depth = 0;
+                struct SingleLinkedQueue* mcSingleQueue = (struct SingleLinkedQueue*)mcWorker->mcQueue->queue;
+                mcWorker->task_iter = createQueueIterator(mcSingleQueue->top->next,mcWorker->root,NULL);
             }
           } else {
             //printf("no more branch %d\n",count);
-            mcworker->depth--;
-            freeIterator(mcworker->task_iter);
-            mcworker->task_iter = prev_iter;
+            mcWorker->depth--;
+            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(mcworker->task_iter->state->memory);
+      restore_memory(mcWorker->task_iter->state->memory);
       context = (Context *)list->data;
       // 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,mcworker->task_iter);
+      mcWorker->depth++;
+      struct SingleLinkedQueue* mcSingleQueue = (struct SingleLinkedQueue*)mcWorker->mcQueue->queue;
+      mcWorker->task_iter = createQueueIterator(mcSingleQueue->top->next,out,mcWorker->task_iter);
     }
     // printf("depth %d count %d\n", depth, count++);
-    mcworker->parent = out;
-    mcworker->count++;
+    mcWorker->parent = out;
+    mcWorker->count++;
+    mcWorker->mcContext = context;
     //goto list->phils->next(list->phils,list);
     goto meta(context, context->next);
 }
--- a/src/parallel_execution/ModelChecking/MCWorker.h	Mon Feb 01 10:52:00 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.h	Mon Feb 01 14:55:12 2021 +0900
@@ -12,10 +12,11 @@
   int id;
   int loopCounter;
   struct Queue* mcQueue; // simulated task queue par thread
-  enum Code nextStep;
   TaskIterator* task_iter;
   StateDB parent;
   StateDB root;
   int depth;
+  int visit;
   int count;
+  int change;  // state db flag is changed
 } MCWorker;
--- a/src/parallel_execution/examples/DPPMC/McDPP.cbc	Mon Feb 01 10:52:00 2021 +0900
+++ b/src/parallel_execution/examples/DPPMC/McDPP.cbc	Mon Feb 01 14:55:12 2021 +0900
@@ -1,10 +1,13 @@
 #include "McDPP.h"
 
-void mcDPP(struct MCTaskManagerImpl* mcti, struct MCWorker* mcworker, StateDB now,StateDB next) {
-  if (mcworker->nextStep == C_eatingPhilsImpl ) {
-    next->flag |= t_eating;
+void mcDPP(struct MCTaskManagerImpl* mcti, struct MCWorker* mcWorker, StateDB now,StateDB next) {
+  PhilsImpl* phils = (PhilsImpl*)GearImpl(mcWorker->mcContext, Phils, phils);
+  if (phils->self != 1) return;
+  enum Code nextc = mcWorker->mcContext->next;
+  if (nextc == C_eatingPhilsImpl ) {
+    next->flag |= t_eating; mcWorker->change = 1;
   }
   if ((next->flag & t_eating )||(next->flag & t_F_eating) ) {
-    now->flag |= t_F_eating;
+    now->flag |= t_F_eating; mcWorker->change = 1;
   }
 }
--- a/src/parallel_execution/examples/DPPMC/main.cbc	Mon Feb 01 10:52:00 2021 +0900
+++ b/src/parallel_execution/examples/DPPMC/main.cbc	Mon Feb 01 14:55:12 2021 +0900
@@ -1,5 +1,7 @@
-#include <stdio.h2
-#include <string.h> #include <stdlib.h> #include <unistd.h>
+#include <stdio.h>
+#include <string.h>
+#include <stdlib.h>
+#include <unistd.h>
 
 #include "../../../context.h"
 #interface "TaskManager.h"