X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=benchmark%2Fchase-lev-deque-bugfix%2Fdeque.c;h=854091ff41d9845ebbace331b04eaf0d85f70a79;hb=9811b5edc5910159c1248ca2745f83ff5edc1e0d;hp=e94da48abe8aeb92127052fff4b5a34f1d3cd8a4;hpb=d8379bc0ab37f46daad7fd5fa7538435591ef836;p=cdsspec-compiler.git

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index e94da48..854091f 100644
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -22,14 +22,27 @@ Deque * create() {
 */
 int take(Deque *q) {
 	size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
+	/**
+		@Begin
+		@Commit_point_define_check: true
+		@Label: Take_Read_Bottom
+		@End
+	*/
 	Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+	/**
+		//@Begin
+		@Commit_point_define_check: true
+		@Label: Take_Read_Array
+		@End
+	*/
 	atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
+	/**** detected correctness ****/
 	atomic_thread_fence(memory_order_seq_cst);
 	size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
 	/**
-		@Begin
-		@Commit_point_define_check: t > b
-		@Label: Take_Point_1
+		//@Begin
+		@Commit_point_define_check: t != b
+		@Label: Take_Read_Top
 		@End
 	*/
 	int x;
@@ -38,9 +51,9 @@ int take(Deque *q) {
 		int size = atomic_load_explicit(&a->size,memory_order_relaxed);
 		x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
 		/**
-			@Begin
+			//@Begin
 			@Commit_point_define_check: t != b
-			@Label: Take_Point2
+			@Label: Take_Read_Buffer
 			@End
 		*/
 		if (t == b) {
@@ -48,10 +61,17 @@ int take(Deque *q) {
 			//FIXME: weaken the following seq_cst causes no spec problem
 			bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
 				1, memory_order_seq_cst, memory_order_relaxed);
+			/**
+				//@Begin
+				@Commit_point_define_check: succ 
+				@Label: Take_CAS_Top
+				@End
+			*/
+
 			/**
 				@Begin
-				@Commit_point_define_check: true
-				@Label: Take_Point3
+				@Additional_ordering_point_define_check: true
+				@Label: Take_Additional_Point
 				@End
 			*/
 			if (!succ) {
@@ -79,8 +99,9 @@ void resize(Deque *q) {
 	for(i=top; i < bottom; i++) {
 		atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
 	}
+	/**** detected UL ****/
 	atomic_store_explicit(&q->array, new_a, memory_order_release);
-	printf("resize\n");
+	//printf("resize\n");
 }
 
 /**
@@ -90,25 +111,39 @@ void resize(Deque *q) {
 */
 void push(Deque *q, int x) {
 	size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
+	/**** detected correctness ****/
 	size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
 	Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
 	if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ {
 		resize(q);
 		//Bug in paper...should have next line...
 		a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+		/**
+			//@Begin
+			@Commit_point_define_check: true
+			@Label: Push_Read_Array
+			@End
+		*/
 	}
 	int size = atomic_load_explicit(&a->size, memory_order_relaxed);
+
 	atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
 	/**
-		@Begin
+		//@Begin
 		@Commit_point_define_check: true
-		@Label: Push_Point
+		@Label: Push_Update_Buffer
 		@End
 	*/
+	/**** detected HB error (run with -u100 to avoid the uninitialized bug) ****/
 	atomic_thread_fence(memory_order_release);
 	
 	atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
-	
+	/**
+		@Begin
+		@Commit_point_define_check: true
+		@Label: Push_Update_Bottom
+		@End
+	*/
 }
 
 /**
@@ -119,41 +154,71 @@ void push(Deque *q, int x) {
 int steal(Deque *q) {
 	//FIXME: weaken the following acquire causes no spec problem
 	size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
+	/**
+		//@Begin
+		@Potential_commit_point_define: true
+		@Label: Steal_Potential_Read_Tail
+		@End
+	*/
+	//FIXME: remove the fence causes no error and fewer executions..
 	atomic_thread_fence(memory_order_seq_cst);
+	/**** detected HB error (run with -u100 to avoid the uninitialized bug) ****/
 	size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
 	/**
 		@Begin
-		@Commit_point_define_check: t >= b
-		@Label: Steal_Point1
+		@Commit_point_define_check: true 
+		@Label: Steal_Read_Bottom
+		@End
+	*/
+
+	/**
+		//@Begin
+		@Commit_point_define: t >= b
+		@Potential_commit_point_label: Steal_Potential_Read_Tail
+		@Label: Steal_Read_Tail
 		@End
 	*/
 	int x = EMPTY;
 	if (t < b) {
 		/* Non-empty queue. */
+		/**** detected UL ****/
 		Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
+		/**
+			//@Begin
+			@Commit_point_define_check: true
+			@Label: Steal_Read_Array
+			@End
+		*/
 		int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 		x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
 		/**
-			@Begin
+			//@Begin
 			@Potential_commit_point_define: true
-			@Label: Potential_Steal
+			@Label: Steal_Potential_Read_Buffer
 			@End
 		*/
-		
+		/**** detected correctness failure ****/ 
 		bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
 			memory_order_seq_cst, memory_order_relaxed);
 		/**
-			@Begin
-			@Commit_point_define_check: !succ
-			@Label: Steal_Point2
+			//@Begin
+			@Commit_point_define_check: succ
+			@Label: Steal_CAS_Top
 			@End
 		*/
 
 		/**
 			@Begin
+			@Additional_ordering_point_define_check: true 
+			@Label: Steal_Additional_Point
+			@End
+		*/
+
+		/**
+			//@Begin
 			@Commit_point_define: succ
-			@Potential_commit_point_label: Potential_Steal
-			@Label: Steal_Point3
+			@Potential_commit_point_label: Steal_Potential_Read_Buffer
+			@Label: Steal_Read_Buffer
 			@End
 		*/
 		if (!succ) {