From: Peizhao Ou <peizhaoo@uci.edu>
Date: Fri, 16 Jan 2015 18:09:15 +0000 (-0800)
Subject: spec changes to deque
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=1e0b916ec3d9ecfa30066b07b15a871ce30f8576

spec changes to deque
---

diff --git a/benchmark/chase-lev-deque-bugfix/main.c b/benchmark/chase-lev-deque-bugfix/main.c
index fd67b60..87e5b9b 100644
--- 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
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
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 89bc6a6..7ebc101 100644
--- 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 = {