Mercurial > hg > Gears > Gears
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); }