Mercurial > hg > Gears > Gears
changeset 918:26e3d0226cc6
add McDPP.cbc
author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 29 Jan 2021 12:17:43 +0900 |
parents | 0111b0f68c4d |
children | 765871c90c74 31ea8f75e9e6 |
files | src/parallel_execution/MCTaskManagerImpl.h src/parallel_execution/ModelChecking/MCWorker.cbc src/parallel_execution/examples/DPPMC/McDPP.cbc src/parallel_execution/examples/DPPMC/meta.pm |
diffstat | 4 files changed, 23 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/src/parallel_execution/MCTaskManagerImpl.h Fri Jan 29 11:55:16 2021 +0900 +++ b/src/parallel_execution/MCTaskManagerImpl.h Fri Jan 29 12:17:43 2021 +0900 @@ -9,6 +9,7 @@ struct Element* taskList; MemoryPtr mem; // modelchecking memorylenge StateDB state_db; + StateNode st; int loopCounter; int cpu; int gpu;
--- a/src/parallel_execution/ModelChecking/MCWorker.cbc Fri Jan 29 11:55:16 2021 +0900 +++ b/src/parallel_execution/ModelChecking/MCWorker.cbc Fri Jan 29 12:17:43 2021 +0900 @@ -93,14 +93,13 @@ StateDB out = NULL; struct Element* list = NULL; struct MCTaskManagerImpl* mcti = (struct MCTaskManagerImpl *)mcworker->taskManager->taskManager; - StateNode st; - st.memory = mcti->mem; - st.hash = get_memory_hash(mcti->mem,0); + mcti->st.memory = mcti->mem; + mcti->st.hash = get_memory_hash(mcti->mem,0); if (dump) { dump_memory(mcti->mem);printf("\n"); } - if (visit_StateDB(&st, &mcti->state_db, &out,mcti->visit)) { - // found in the state database + if (visit_StateDB(&mcti->st, &mcti->state_db, &out,mcti->visit)) { + // found in the state database // printf("found %d\n",count); while(!(list = takeNextIterator(mcworker->task_iter))) { // no more branch, go back to the previous one @@ -123,6 +122,7 @@ // here we assume task list is fixed, we don't have to // recover task list itself restore_memory(mcworker->task_iter->state->memory); + mcti->st = *out; context = (Context *)list->data; // printf("restore list %x next %x\n",(int)list,(int)(list->next)); } else {
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/parallel_execution/examples/DPPMC/McDPP.cbc Fri Jan 29 12:17:43 2021 +0900 @@ -0,0 +1,14 @@ +__ncode mcDPP(struct Context* context, enum Code next) { + struct MCWorker* mcworker = (struct MCWorker*) context->worker->worker; + struct MCTaskManagerImpl* mcti = (struct MCTaskManagerImpl *)mcworker->taskManager->taskManager; + + if (mcti->prev == C_eatingPhisImpl) { + mcti->st->flag |= P_eating; + } + + if (current_st & p_F_eating) { + mcti->st->flag |= P_F_eating; + } + + goto mcMeta(context, next); +}
--- a/src/parallel_execution/examples/DPPMC/meta.pm Fri Jan 29 11:55:16 2021 +0900 +++ b/src/parallel_execution/examples/DPPMC/meta.pm Fri Jan 29 12:17:43 2021 +0900 @@ -10,14 +10,14 @@ #my ($currentCodeGearName, $context, $next) = @_; -sub generateRondomMeta { +sub generateRandomMeta { my ($context, $next) = @_; - return "goto rondom($context, $next);"; + return "goto random($context, $next);"; } sub generateMcMeta { my ($context, $next) = @_; - return "goto mcMeta($context, $next);"; + return "goto mcDPP($context, $next);"; } 1;