Mercurial > hg > Gears > Gears
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"