--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/AtomicTImpl.cbc	Sun Jan 24 15:53:29 2021 +0900
@@ -0,0 +1,28 @@
+#include "../../../context.h"
+#impl "AtomicT_int.h" for "AtomicT_intImpl_int.h"
+#include <stdio.h>
+
+AtomicT_int* createAtomicT_intImpl_int(struct Context* context,int init) {
+    struct AtomicT_int* atomicT_int  = new AtomicT_int();
+    struct AtomicT_intImpl_int* atomic_t_impl = new AtomicT_intImpl_int();
+    atomicT_int->atomicT_int = (union Data*)atomic_t_impl;
+    atomicT_int->checkAndSet = C_checkAndSet_AtomicT_intImpl;
+    atomicT_int->set = C_set_AtomicT_intImpl;
+    atomic_t_impl->atomic = init;
+    atomic_t_impl->init = init;
+    return atomicT_int;
+
+}
+
+__code checkAndSet_AtomicT_intImpl(struct AtomicT_intImpl_int* atomicT_int, int oldData, int newData, __code next(...), __code fail(...)) {
+    if (__sync_bool_compare_and_swap(&atomicT_int->atomic, oldData, newData)) {
+        goto next(...);
+    }
+    goto fail(...);
+}
+
+__code set_AtomicT_intImpl(struct AtomicT_intImpl_int* atomicT_int, int newData, __code next(...) ) {
+	atomicT_int->atomic = newData;
+   goto next(...);
+}
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/AtomicT_int.h	Sun Jan 24 15:53:29 2021 +0900
@@ -0,0 +1,6 @@
+typedef struct AtomicT_int <>{
+    __code checkAndSet(Impl* atomicT_int, int oldData, int newData, __code next(...), __code fail(...));
+    __code set(Impl* atomicT_int ,int newData, __code next(...));
+    __code next(...);
+    __code fail(...);
+} AtomicT_int;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/AtomicT_intImpl_int.h	Sun Jan 24 15:53:29 2021 +0900
@@ -0,0 +1,5 @@
+typedef struct AtomicT_intImpl_int <T> impl AtomicT_int {
+  int atomic;
+  int init;
+  __code next(...);
+} AtomicT_intImpl_int;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/Fork.h	Sun Jan 24 15:53:29 2021 +0900
@@ -0,0 +1,6 @@
+typedef struct Fork <> {
+  union Data* fork;
+  int id;
+  struct Phils* owner;
+  __code next(...);
+} Fork;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/ForkImpl.cbc	Sun Jan 24 15:53:29 2021 +0900
@@ -0,0 +1,17 @@
+#include "../../../context.h"
+#interface "Fork.h"
+
+// ----
+// typedef struct ForkImpl <Type, Isa> impl Fork {
+//   __code next(...);
+// } ForkImpl;
+// ----
+
+Fork* createForkImpl(struct Context* context) {
+    struct Fork* fork  = new Fork();
+    struct ForkImpl* fork_impl = new ForkImpl();
+    fork->fork = (union Data*)fork_impl;
+    fork->id = 0;
+    fork->owner = NULL;
+    return fork;
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/ForkImpl.h	Sun Jan 24 15:53:29 2021 +0900
@@ -0,0 +1,3 @@
+typedef struct ForkImpl <> impl Fork {
+  __code next(...);
+} ForkImpl;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/Phils.h	Sun Jan 24 15:53:29 2021 +0900
@@ -0,0 +1,9 @@
+typedef struct Phils <> {
+  __code putdown_lfork(Impl* phils, __code next(...));
+  __code putdown_rfork(Impl* phils, __code next(...));
+  __code thinking(Impl* phils, __code next(...));
+  __code pickup_rfork(Impl* phils, __code next(...));
+  __code pickup_lfork(Impl* phils, __code next(...));
+  __code eating(Impl* phils, __code next(...));
+  __code next(...);
+} Phils;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/PhilsImpl.cbc	Sun Jan 24 15:53:29 2021 +0900
@@ -0,0 +1,67 @@
+#include "../../../context.h"
+#include <stdio.h>
+#impl "Phils.h" for "PhilsImpl.h"
+#interface "Fork.h"
+#interface "Worker.h"
+#interface "AtomicT_int.h"
+#interface "TaskManager.h"
+
+
+// ----
+// typedef struct PhilsImpl <Self, Isa> impl Phils {
+//   __code next(...);
+//   atomic Leftfork;
+//   atomic Rightfork;
+//   int self;
+// } PhilsImpl;
+// ----
+
+Phils* createPhilsImpl(struct Context* context, int id, AtomicT_int* right, AtomicT_int* left) {
+    struct Phils* phils  = new Phils();
+    struct PhilsImpl* phils_impl = new PhilsImpl();
+    phils->phils = (union Data*)phils_impl;
+    phils_impl->Leftfork = left;
+    phils_impl->Rightfork = right;
+    phils_impl->self = id;
+    phils->putdown_lfork = C_putdown_lforkPhilsImpl;
+    phils->putdown_rfork = C_putdown_rforkPhilsImpl;
+    phils->eating = C_eatingPhilsImpl;
+    phils->pickup_rfork = C_pickup_rforkPhilsImpl;
+    phils->pickup_lfork = C_pickup_lforkPhilsImpl;
+    phils->thinking = C_thinkingPhilsImpl;
+    return phils;
+}
+
+
+__code putdown_rfork(struct PhilsImpl* phils, __code next(...)) {
+    struct AtomicT_int* right_fork = phils->Rightfork;
+    goto right_fork->set(-1, putdown_lfork);
+}
+
+__code putdown_lfork(struct PhilsImpl* phils, __code next(...)) {
+    struct AtomicT_int* left_fork = phils->Leftfork;
+    goto left_fork->set(-1, thinking);
+
+}
+
+__code thinking(struct PhilsImpl* phils, struct Fork* fork, __code next(...)) {
+    printf("%d: thinking\n", phils->self);
+    goto pickup_lfork();
+}
+
+__code pickup_rfork(struct PhilsImpl* phils, __code next(...)) {
+    struct AtomicT_int* right_fork = phils->Rightfork;
+    goto right_fork->checkAndSet(-1, phils->self, pickup_lfork, pickup_rfork);
+}
+
+__code pickup_lfork(struct PhilsImpl* phils, __code next(...)) {
+    struct AtomicT_int* left_fork = phils->Leftfork;
+    goto left_fork->checkAndSet(-1, phils->self, pickup_rfork, eating);
+
+}
+
+__code eating(struct PhilsImpl* phils, __code next(...)) {
+    printf("%d: eating\n", phils->self);
+    goto putdown_rfork();
+}
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/PhilsImpl.h	Sun Jan 24 15:53:29 2021 +0900
@@ -0,0 +1,6 @@
+typedef struct PhilsImpl <> impl Phils {
+  int self;
+  struct AtomicT_int* Leftfork;
+  struct AtomicT_int* Rightfork;
+  __code next(...);
+} PhilsImpl;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/PhilsImplMC.cbc	Sun Jan 24 15:53:29 2021 +0900
@@ -0,0 +1,64 @@
+#include "../../../context.h"
+#include <stdio.h>
+#interface "Phils.h"
+#interface "Fork.h"
+#interface "Worker.h"
+#interface "Atomic.h"
+#interface "TaskManager.h"
+
+
+// ----
+// typedef struct PhilsImpl <Self, Isa> impl Phils {
+//   __code next(...);
+//   atomic Leftfork;
+//   atomic Rightfork;
+//   int self;
+// } PhilsImpl;
+// ----
+
+Phils* createPhilsImpl(struct Context* context, int id, AtomicT_int right, AtomicT_int left) {
+    struct Phils* phils  = new Phils();
+    struct PhilsImpl* phils_impl = new PhilsImpl();
+    phils->phils = (union Data*)phils_impl;
+    phils_impl->Leftfork = left;
+    phils_impl->Rightfork = right;
+    phils_impl->self = 0;
+    phils->putdown_lfork = C_putdown_lfork_PhilsImpl;
+    phils->putdown_rfork = C_putdown_rfork_PhilsImpl;
+    phils->eating = C_eating_PhilsImpl;
+    phils->pickup_rfork = C_pickup_rfork_PhilsImpl;
+    phils->pickup_lfork = C_pickup_lfork_PhilsImpl;
+    phils->thinking = C_thinking_PhilsImpl;
+    return phils;
+    }
+
+__code putdown_lfork_PhilsImpl(struct PhilsImpl* phils, __code next(...)) {
+ 	   goto phils->Leftfork->checkAndSet(id, putdown_rfork_PhilsImpl, putdown_lfork_PhilsImpl);
+
+}
+
+__code putdown_rfork_PhilsImpl(struct PhilsImpl* phils, __code next(...)) {
+    	   goto phils->Rightfork->checkAndSet(id, putdown_lfork_PhilsImpl, thinking_PhilsImpl);
+}
+
+__code eating_PhilsImpl(struct PhilsImpl* phils, __code next(...)) {
+        printf("%d: eating\n", phils_impl->self->id);
+           goto putdown_rfork();
+}
+
+__code pickup_rfork_PhilsImpl(struct PhilsImpl* phils, __code next(...)) {
+        struct Atomic* atomic = phils_impl->rightfork->atomic;
+ 	   goto atomic->checkAndSet(-1, pickup_lfork_Phils, pickup_rfork_Phils);
+}
+
+__code pickup_lfork_PhilsImpl(struct PhilsImpl* phils, __code next(...)) {
+        struct Atomic* atomic = phils_impl->leftfork->atomic;
+    	   goto atomic->checkAndSet(-1, pickup_rfork_Phils, eating_PhilsImpl);
+
+}
+
+__code thinking_PhilsImpl(struct PhilsImpl* phils, struct Fork* fork, __code next(...)) {
+        printf("%d: thinking\n", phils->phils->id);
+	  goto pickup_lfork(phils_impl->self);;
+}
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/examples/DPPMC/main.cbc	Sun Jan 24 15:53:29 2021 +0900
@@ -0,0 +1,90 @@
+#include <stdio.h>
+#include <string.h>
+#include <stdlib.h>
+#include <unistd.h>
+
+
+#include "../../../context.h"
+#interface "TaskManager.h"
+#interface "Phils.h"
+#interface "Fork.h"
+#interface "AtomicT_int.h"
+
+int cpu_num = 5;
+int length = 102400;
+int split = 8;
+int* array_ptr;
+int gpu_num = 0;
+int CPU_ANY = -1;
+int CPU_CUDA = -1;
+
+__code initDataGears(struct LoopCounter* loopCounter, struct TaskManager* taskManager) {
+    // loopCounter->tree = createRedBlackTree(context);
+    loopCounter->i = 0;
+    taskManager->taskManager = (union Data*)createTaskManagerImpl(context, cpu_num, gpu_num, 0);
+    goto code1();
+}
+
+__code code1(struct LoopCounter* loopCounter) {
+    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();
+}
+
+
+__code createTask1(struct LoopCounter* loopCounter, struct TaskManager* taskManager) {
+    AtomicT_int* fork0 = createAtomicT_intImpl_int(context,-1); // model checking : fork0
+    AtomicT_int* fork1 = createAtomicT_intImpl_int(context,-1); // model checking : fork1
+    AtomicT_int* fork2 = createAtomicT_intImpl_int(context,-1); // model checking : fork2
+    AtomicT_int* fork3 = createAtomicT_intImpl_int(context,-1); // model checking : fork3
+    AtomicT_int* fork4 = createAtomicT_intImpl_int(context,-1); // model checking : fork4
+
+    Phils* phils0 = createPhilsImpl(context,0,fork0,fork1); // model checking : phils0
+    Phils* phils1 = createPhilsImpl(context,1,fork1,fork2); // model checking : phils1
+    Phils* phils2 = createPhilsImpl(context,2,fork2,fork3); // model checking : phils2
+    Phils* phils3 = createPhilsImpl(context,3,fork3,fork4); // model checking : phils3
+    Phils* phils4 = createPhilsImpl(context,4,fork4,fork0); // model checking : phils4
+
+    par goto phils0->thinking(exit_code);
+    par goto phils1->thinking(exit_code);
+    par goto phils2->thinking(exit_code);
+    par goto phils3->thinking(exit_code);
+    par goto phils4->thinking(exit_code);
+
+    goto code2();
+}
+
+__code code2(struct TaskManager* taskManager) {
+    goto taskManager->shutdown(exit_code);
+}
+
+__code code2_stub(struct Context* contextt) {
+    goto code2(contextt, &Gearef(contextt, TaskManager)->taskManager->TaskManager);
+}
+
+void init(int argc, char** argv) {
+    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;
+        }
+    }
+}
+
+int main(int argc, char** argv) {
+    init(argc, argv);
+    goto initDataGears();
+}