Mercurial > hg > Gears > Gears

changeset 928:917fb0cc6d6b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mcDPP CTL state flag trying
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 31 Jan 2021 08:45:12 +0900
parents 850b6a6d2199
children 2c1f2acadf40
files src/parallel_execution/CMakeLists.txt src/parallel_execution/MCTaskManagerImpl.h src/parallel_execution/MCWorker.h src/parallel_execution/ModelChecking/MCWorker.cbc src/parallel_execution/ModelChecking/MCWorker.h src/parallel_execution/ModelChecking/TaskIterator.c src/parallel_execution/SingleLinkedQueue.cbc src/parallel_execution/examples/DPPMC/McDPP.cbc src/parallel_execution/examples/DPPMC/McDPP.h src/parallel_execution/examples/DPPMC/main.cbc
diffstat 10 files changed, 72 insertions(+), 79 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/CMakeLists.txt	Sat Jan 30 19:38:22 2021 +0900
+++ b/src/parallel_execution/CMakeLists.txt	Sun Jan 31 08:45:12 2021 +0900
@@ -153,7 +153,10 @@
   TARGET
   DPPMC
   SOURCES
-  CPUWorker.cbc SynchronizedQueue.cbc examples/DPPMC/AtomicTImpl.cbc SingleLinkedStack.cbc examples/DPPMC/PhilsImpl.cbc examples/DPPMC/main.cbc examples/DPPMC/ForkImpl.cbc ModelChecking/crc32.c ModelChecking/memory.c ModelChecking/state_db.c AtomicReference.cbc ModelChecking/MCWorker.cbc MCTaskManagerImpl.cbc SingleLinkedQueue.cbc
+  CPUWorker.cbc SynchronizedQueue.cbc examples/DPPMC/AtomicTImpl.cbc SingleLinkedStack.cbc examples/DPPMC/PhilsImpl.cbc 
+     examples/DPPMC/main.cbc examples/DPPMC/ForkImpl.cbc ModelChecking/crc32.c ModelChecking/memory.c 
+     ModelChecking/state_db.c AtomicReference.cbc ModelChecking/MCWorker.cbc MCTaskManagerImpl.cbc SingleLinkedQueue.cbc
+     ModelChecking/TaskIterator.c
 )
 
 GearsCommand(
--- a/src/parallel_execution/MCTaskManagerImpl.h	Sat Jan 30 19:38:22 2021 +0900
+++ b/src/parallel_execution/MCTaskManagerImpl.h	Sun Jan 31 08:45:12 2021 +0900
@@ -9,13 +9,12 @@
   struct Element* taskList;
   MemoryPtr mem; // modelchecking memorylenge
   StateDB state_db;
-  StateNode st;
   int loopCounter;
   int cpu;
   int gpu;
   int io;
   int visit;
   int maxCPU;
-  void (*statefunc)(struct MCTaskManagerImpl* mcti, StateDB now,StateDB next);
+  void (*statefunc)(struct MCTaskManagerImpl* mcti, struct MCWorker* mcworker, StateDB now,StateDB next);
   __code next(...);
 } MCTaskManagerImpl;
--- a/src/parallel_execution/MCWorker.h	Sat Jan 30 19:38:22 2021 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-#include "ModelChecking/state_db.h"
-#include "ModelChecking/memory.h"
-#include "ModelChecking/TaskIterator.h"
-
-typedef struct MCWorker <> {
-  pthread_mutex_t mutex;
-  pthread_cond_t cond;
-  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;
-  TaskIterator* task_iter;
-  StateDB parent;
-  StateDB root;
-  int depth;
-  int count;
-} MCWorker;
--- a/src/parallel_execution/ModelChecking/MCWorker.cbc	Sat Jan 30 19:38:22 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.cbc	Sun Jan 31 08:45:12 2021 +0900
@@ -105,7 +105,7 @@
         dump_memory(mcti->mem);printf("\n");
     }
     int found = visit_StateDB(&mcti->st, &mcti->state_db, &out,mcti->visit);
-    mcti->statefunc(mcti, mcworker->parent, out);
+    mcti->statefunc(mcti, mcworker, mcworker->parent, out);
     if (found) {
       // found in the state database
       // printf("found %d\n",count);
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/ModelChecking/MCWorker.h	Sun Jan 31 08:45:12 2021 +0900
@@ -0,0 +1,21 @@
+#include "state_db.h"
+#include "memory.h"
+#include "TaskIterator.h"
+
+typedef struct MCWorker <> {
+  pthread_mutex_t mutex;
+  pthread_cond_t cond;
+  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;
+  TaskIterator* task_iter;
+  StateDB parent;
+  StateDB root;
+  int depth;
+  int count;
+} MCWorker;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/ModelChecking/TaskIterator.c	Sun Jan 31 08:45:12 2021 +0900
@@ -0,0 +1,31 @@
+#include <stdio.h>
+#include "Elemeny.h"
+#include "TaskIterator.h"
+#include "state_db.h"
+
+TaskIterator* createQueueIterator(Element* elements, StateDB s, TaskIterator* prev) {
+    TaskIterator* new = (TaskIterator*)calloc(1, sizeof(TaskIterator));
+    if (!new) exit(1);
+    new->prev  = prev;
+    new->state = s; //
+    new->list  = elements;
+    return new;
+}
+
+Element* takeNextIterator(TaskIterator* iterator) {
+  struct Element* elem = iterator->list;
+  if (!elem) {
+    return NULL;
+  }
+  struct Element* next = elem->next;
+  if (next == NULL) {
+    return NULL;
+  }
+  iterator->list = next;
+  return next;
+}
+
+void freeIterator(TaskIterator* iterator) {
+  free(iterator);
+}
+
--- a/src/parallel_execution/SingleLinkedQueue.cbc	Sat Jan 30 19:38:22 2021 +0900
+++ b/src/parallel_execution/SingleLinkedQueue.cbc	Sun Jan 31 08:45:12 2021 +0900
@@ -1,6 +1,5 @@
 #include "../context.h"
 #include <stdio.h>
-#include "state_db.h"
 #impl "Queue.h" for "SingleLinkedQueue.h"
 #data "Node.h"
 #data "Element.h"
@@ -81,8 +80,6 @@
     return length - 1; // top is dummy
 }
 
-#include "../ModelChecking/TaskIterator.h"
-
 Element* getElementByIdx(struct SingleLinkedQueue* queue, int idx) {
     struct Element* current = queue->top;
 
@@ -95,33 +92,3 @@
     return queue->top;
 }
 
-
-
-TaskIterator* createQueueIterator(Element* elements, StateDB s, TaskIterator* prev) {
-    TaskIterator* new = (TaskIterator*)calloc(1, sizeof(TaskIterator));
-    if (!new) exit(1);
-    new->prev  = prev;
-    new->state = s; //
-    new->list  = elements;
-    return new;
-}
-
-Element* takeNextIterator(TaskIterator* iterator) {
-  struct Element* elem = iterator->list;
-  if (!elem) {
-    return NULL;
-  }
-
-  struct Element* next = elem->next;
-  if (next == NULL) {
-    return NULL;
-  }
-
-
-  iterator->list = next;
-  return next;
-}
-
-void freeIterator(TaskIterator* iterator) {
-  free(iterator);
-}
--- a/src/parallel_execution/examples/DPPMC/McDPP.cbc	Sat Jan 30 19:38:22 2021 +0900
+++ b/src/parallel_execution/examples/DPPMC/McDPP.cbc	Sun Jan 31 08:45:12 2021 +0900
@@ -1,14 +1,10 @@
-__ncode mcDPP(struct Context* context, enum Code next) {
-  struct MCWorker* mcworker =  (struct MCWorker*) context->worker->worker;
-  struct MCTaskManagerImpl* mcti = (struct MCTaskManagerImpl *)mcworker->taskManager->taskManager;
+#include "McDPP.h"
 
-  if (mcti->prev == C_eatingPhisImpl) {
-    mcti->st->flag |= P_eating;
+void mcDPP(struct MCTaskManagerImpl* mcti, struct MCWorker* mcworker, StateDB now,StateDB next) {
+  if (mcworker->nextStep == C_eatingPhisImpl) {
+    next->flag |= P_eating;
   }
-
-  if (current_st & p_F_eating) {
-    mcti->st->flag |= P_F_eating;
+  if ((next->flag & p_F_eating )||(next->flag & P_eating) ) {
+    now->flag |= P_F_eating;
   }
-
-  goto mcMeta(context, next);
 }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/McDPP.h	Sun Jan 31 08:45:12 2021 +0900
@@ -0,0 +1,6 @@
+#include "MCTaskManagerImpl.h"
+#include "MCWorker.h"
+#include "state_db.h"
+
+extern void mcDPP(struct MCTaskManagerImpl* mcti, struct MCWorker* mcworker, StateDB now,StateDB next) ;
+
--- a/src/parallel_execution/examples/DPPMC/main.cbc	Sat Jan 30 19:38:22 2021 +0900
+++ b/src/parallel_execution/examples/DPPMC/main.cbc	Sun Jan 31 08:45:12 2021 +0900
@@ -9,6 +9,7 @@
 #interface "Phils.h"
 #interface "Fork.h"
 #interface "AtomicT_int.h"
+#interface "McDPP.h"
 
 extern void addMemoryPhilsImpl(MCTaskManagerImpl *mcti, struct PhilsImpl* phils);
 
@@ -27,13 +28,6 @@
 __code code1() {
     printf("cpus:\t\t%d\n", cpu_num);
     printf("gpus:\t\t%d\n", gpu_num);
-    // printf("length:\t\t%d\n", length);
-    // printf("length/task:\t%d\n", length/split);
-    /* puts("queue"); */
-    /* print_queue(context->data[ActiveQueue]->queue.first); */
-    /* puts("tree"); */
-    /* print_tree(context->data[Tree]->tree.root); */
-    /* puts("result"); */
     goto createTask1();
 }
 
@@ -45,6 +39,7 @@
     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 *)context->taskManager->taskManager;
+    mcti->statefunc = mcDPP;
 					     
     Phils* phils0 = createPhilsImpl(context,0,fork0,fork1); // model checking : phils0
     addMemoryPhilsImpl(mcti,(struct PhilsImpl*)phils0->phils);
@@ -78,10 +73,6 @@
     for (int i = 1; argv[i]; ++i) {
         if (strcmp(argv[i], "-cpu") == 0)
             cpu_num = (int)atoi(argv[i+1]);
-        //else if (strcmp(argv[i], "-l") == 0)
-        //    length = (int)atoi(argv[i+1]);
-        //else if (strcmp(argv[i], "-s") == 0)
-        //    split = (int)atoi(argv[i+1]);
         else if (strcmp(argv[i], "-cuda") == 0) {
             gpu_num = 1;
             CPU_CUDA = 0;