From: Peizhao Ou <peizhaoo@uci.edu>
Date: Fri, 16 Jan 2015 17:42:46 +0000 (-0800)
Subject: changes to the spec of deque
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=52802de070a3314dfdd75c039c8e41d79d493996;hp=6d0e5824cfcdd3569f05e8d2a11992e7ac9a344f

changes to the spec of deque
---

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index d174122..fbd723b 100644
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -62,7 +62,7 @@ int take(Deque *q) {
 			bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
 				1, memory_order_seq_cst, memory_order_relaxed);
 			/**
-				@Begin
+				//@Begin
 				@Commit_point_define_check: succ 
 				@Label: Take_CAS_Top
 				@End
@@ -70,7 +70,7 @@ int take(Deque *q) {
 
 			/**
 				@Begin
-				@Additional_ordering_point_define_check: !succ
+				@Additional_ordering_point_define_check: true
 				@Label: Take_Additional_Point
 				@End
 			*/
@@ -201,7 +201,7 @@ int steal(Deque *q) {
 		bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
 			memory_order_seq_cst, memory_order_relaxed);
 		/**
-			@Begin
+			//@Begin
 			@Commit_point_define_check: succ
 			@Label: Steal_CAS_Top
 			@End
@@ -209,7 +209,7 @@ int steal(Deque *q) {
 
 		/**
 			@Begin
-			@Additional_ordering_point_define_check: !succ
+			@Additional_ordering_point_define_check: true 
 			@Label: Steal_Additional_Point
 			@End
 		*/
diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h
index 0a87de7..7d2df9f 100644
--- a/benchmark/chase-lev-deque-bugfix/deque.h
+++ b/benchmark/chase-lev-deque-bugfix/deque.h
@@ -72,7 +72,8 @@ void resize(Deque *q);
 /**
     @Begin
     @Interface: Take 
-    @Commit_point_set: Take_Read_Bottom | Take_CAS_Top |Take_Additional_Point
+    //@Commit_point_set: Take_Read_Bottom | Take_CAS_Top | Take_Additional_Point
+    @Commit_point_set: Take_Read_Bottom | Take_Additional_Point
     @ID: __RET__ == EMPTY ? DEFAULT_CALL_ID : get_id(back(__deque))
     @Action:
         int _Old_Val = EMPTY;
@@ -103,7 +104,8 @@ void push(Deque *q, int x);
 /**
     @Begin
     @Interface: Steal 
-    @Commit_point_set: Steal_Read_Bottom | Steal_CAS_Top | Steal_Additional_Point
+    //@Commit_point_set: Steal_Read_Bottom | Steal_CAS_Top | Steal_Additional_Point
+    @Commit_point_set: Steal_Read_Bottom | Steal_Additional_Point
     @ID: (__RET__ == EMPTY || __RET__ == ABORT) ? DEFAULT_CALL_ID : get_id(front(__deque))
     @Action:
         int _Old_Val = EMPTY;
diff --git a/benchmark/chase-lev-deque-bugfix/main.c b/benchmark/chase-lev-deque-bugfix/main.c
index 6be90a5..fd67b60 100644
--- a/benchmark/chase-lev-deque-bugfix/main.c
+++ b/benchmark/chase-lev-deque-bugfix/main.c
@@ -14,13 +14,18 @@ int b;
 int c;
 
 static void task(void * param) {
-	//a=steal(q);
 	a=steal(q);
 	if (a == ABORT) {
 		printf("Steal NULL\n");
 	} 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)