spec changes to deque

diff --git a/benchmark/chase-lev-deque-bugfix/main.c b/benchmark/chase-lev-deque-bugfix/main.c
index fd67b60ec7a02ebf39244821030f541699260737..87e5b9b8ca1e4170955e2d42254a47c301291e26 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/main.c
+++ b/benchmark/chase-lev-deque-bugfix/main.c
@@ -20,12 +20,6 @@ static void task(void * param) {
        } else {
                printf("Steal %d\n", a);
        }
-       int x=steal(q);
-       if (x == ABORT) {
-               printf("Steal NULL\n");
-       } else {
-               printf("Steal %d\n", x);
-       }
 }
 
 int user_main(int argc, char **argv)

diff --git a/benchmark/chase-lev-deque-bugfix/note.txt b/benchmark/chase-lev-deque-bugfix/note.txt
new file mode 100644 (file)
index 0000000..bfeb604
--- /dev/null
+++ b/benchmark/chase-lev-deque-bugfix/note.txt
@@ -0,0 +1,12 @@
+#1: Ordering point of the deque as the following: 
+
+First of all, the normal usage scenario of the deque is that the main thread
+calls push() or take() to add or remove elements into the deque from the bottom
+(at the same side) while other independent threads call steal() to remove
+elements from the top (at the other side). Thus intuitively, we use the store of
+the Bottom as the ordering point of push(). For take() and steal(), when there's
+no race between them, meaning that there are more than one element, we also use
+the load of Bottom as their ordering points. However, when take() has to remove
+an preemptively, it will use a CAS to update the Top to race with other stealing
+threads. Thus, in that case, we have additional ordering points at the CAS/Load
+(when failure happens) to order the steal() and the take().

diff --git a/benchmark/chase-lev-deque-bugfix/testcase.c b/benchmark/chase-lev-deque-bugfix/testcase.c
new file mode 100644 (file)
index 0000000..761ff46
--- /dev/null
+++ b/benchmark/chase-lev-deque-bugfix/testcase.c
@@ -0,0 +1,77 @@
+#include <stdlib.h>
+#include <assert.h>
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#include "model-assert.h"
+
+#include "deque.h"
+
+Deque *q;
+int a;
+int b;
+int c;
+int x;
+
+static void task(void * param) {
+       a=steal(q);
+       if (a == ABORT) {
+               printf("Steal NULL\n");
+       } else {
+               printf("Steal %d\n", a);
+       }
+       x=steal(q);
+       if (x == ABORT) {
+               printf("Steal NULL\n");
+       } else {
+               printf("Steal %d\n", x);
+       }
+}
+
+int user_main(int argc, char **argv)
+{
+       /**
+               @Begin
+               @Entry_point
+               @End
+       */
+       thrd_t t;
+       q=create();
+       thrd_create(&t, task, 0);
+       push(q, 1);
+       printf("Push 1\n");
+       push(q, 2);
+       printf("Push 2\n");
+       push(q, 4);
+       printf("Push 4\n");
+       b=take(q);
+       if (b == EMPTY) {
+               printf("Take NULL\n");
+       } else {
+               printf("Take %d\n", b);
+       }
+       c=take(q);
+       if (c == EMPTY) {
+               printf("Take NULL\n");
+       } else {
+               printf("Take %d\n", c);
+       }
+       thrd_join(t);
+/*
+       bool correct=true;
+       if (a!=1 && a!=2 && a!=4 && a!= EMPTY)
+               correct=false;
+       if (b!=1 && b!=2 && b!=4 && b!= EMPTY)
+               correct=false;
+       if (c!=1 && c!=2 && c!=4 && a!= EMPTY)
+               correct=false;
+       if (a!=EMPTY && b!=EMPTY && c!=EMPTY && (a+b+c)!=7)
+               correct=false;
+       if (!correct)
+               printf("a=%d b=%d c=%d\n",a,b,c);
+               */
+       //MODEL_ASSERT(correct);
+
+       return 0;
+}

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 89bc6a61e873550003362c87736b47628be9efb9..7ebc101385f6a7b8c2cc0ecc6123d23bea6f5fc5 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -309,6 +309,7 @@ public class CodeGenerator {
                File[] srcDeque = {
                                new File(homeDir + "/benchmark/chase-lev-deque-bugfix/deque.c"),
                                new File(homeDir + "/benchmark/chase-lev-deque-bugfix/main.c"),
+                               new File(homeDir + "/benchmark/chase-lev-deque-bugfix/testcase.c"),
                                new File(homeDir + "/benchmark/chase-lev-deque-bugfix/deque.h") };
 
                File[] srcMCSLock = {