X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=benchmark%2Fms-queue%2Fmy_queue.c;h=fe4da51fe7275a87dd062a6fef9af7152c46855f;hp=bb237bf6c0df386167749820c007ad7fe7e9908c;hb=eeea572e974cb93f35d6788250d011a031ffba2f;hpb=9e08fb16f226a6c13a3526150a41814746805631

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index bb237bf..fe4da51 100644
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -161,12 +161,6 @@ void enqueue(queue_t *q, unsigned int val)
 			&tail,
 			MAKE_POINTER(node, get_count(tail) + 1),
 			release, relaxed);
-	/**
-		//@Begin
-		@Commit_point_define_check: succ
-		@Label: Enqueue_UpdateOrLoad_Tail
-		@End
-	*/
 }
 
 /**
@@ -176,7 +170,7 @@ void enqueue(queue_t *q, unsigned int val)
 */
 bool dequeue(queue_t *q, int *retVal)
 {
-	unsigned int value;
+	unsigned int value = 0;
 	int success = 0;
 	pointer head;
 	pointer tail;
@@ -197,6 +191,10 @@ bool dequeue(queue_t *q, int *retVal)
 			@Label: Dequeue_Read_Head
 			@End
 		*/
+		/** A new bug has been found here!!! It should be acquire instead of
+		 * relaxed (it introduces a bug when there's two dequeuers and one
+		 * enqueuer)
+		 */
 		tail = atomic_load_explicit(&q->tail, acquire);
 		/**
 			@Begin
@@ -243,26 +241,26 @@ bool dequeue(queue_t *q, int *retVal)
 				//printf("miss4_dequeue\n");
 				thrd_yield();
 			} else {
-				/**
-					@Begin
-					@Commit_point_define: true
-					@Potential_commit_point_label: Dequeue_Potential_LoadNext
-					@Label: Dequeue_LoadNext
-					@End
-				*/
 				value = load_32(&q->nodes[get_ptr(next)].value);
-				*retVal = value;
 				//value = q->nodes[get_ptr(next)].value;
 				/****FIXME: correctness error ****/
 				success = atomic_compare_exchange_strong_explicit(&q->head,
 						&head,
 						MAKE_POINTER(get_ptr(next), get_count(head) + 1),
 						release, relaxed);
+				/**
+					@Begin
+					@Commit_point_define: success
+					@Potential_commit_point_label: Dequeue_Potential_LoadNext
+					@Label: Dequeue_LoadNext
+					@End
+				*/
 				if (!success)
 					thrd_yield();
 			}
 		}
 	}
 	reclaim(get_ptr(head));
+	*retVal = value;
 	return true;
 }