X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=benchmark%2Fms-queue%2Fmy_queue.c;h=fdea1a4bab7148323c07d0edc6d5e5ba62d4b9ce;hp=b8189c930e8dc3e224ced2c2cfe266d886829f27;hb=660ed177edb1a5750969661cb4df4626edf80bc0;hpb=48fb6334c3bc1e63a33a80cce2ab50a08348d272

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index b8189c9..fdea1a4 100644
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -111,7 +111,7 @@ void enqueue(queue_t *q, unsigned int val)
 			@Label: Enqueue_Clear
 			@End
 		*/
-		/**** detected UL ****/
+		/**** UL & inadmissible ****/
 		tail = atomic_load_explicit(&q->tail, acquire);
 		/****FIXME: miss ****/
 		next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
@@ -123,7 +123,7 @@ void enqueue(queue_t *q, unsigned int val)
 
 			if (get_ptr(next) == 0) { // == NULL
 				pointer value = MAKE_POINTER(node, get_count(next) + 1);
-				/**** detected UL ****/
+				/**** SPEC Error (testcase1.c) ****/
 				// Second release can be just relaxed
 				success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
 						&next, value, release, relaxed);
@@ -136,15 +136,15 @@ void enqueue(queue_t *q, unsigned int val)
 			}
 			if (!success) {
 				// This routine helps the other enqueue to update the tail
-				/**** detected UL ****/
+				/**** UL & Inadmissible ****/
 				unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
 				pointer value = MAKE_POINTER(ptr,
 						get_count(tail) + 1);
-				/****FIXME: miss ****/
+				/**** SPEC (sequential, testcase2.c) ****/
 				// Second release can be just relaxed
 				bool succ = false;
 				succ = atomic_compare_exchange_strong_explicit(&q->tail,
-						&tail, value, release, relaxed);
+						&tail, value, relaxed, relaxed);
 				if (succ) {
 					//printf("miss2_enqueue CAS succ\n");
 				}
@@ -153,7 +153,7 @@ void enqueue(queue_t *q, unsigned int val)
 			}
 		}
 	}
-	/**** dectected UL ****/
+	/**** UL & Inadmissible ****/
 	// Second release can be just relaxed
 	bool succ = atomic_compare_exchange_strong_explicit(&q->tail,
 			&tail,
@@ -181,7 +181,7 @@ bool dequeue(queue_t *q, int *retVal)
 			@Label: Dequeue_Clear
 			@End
 		*/
-		/**** detected correctness error ****/
+		/**** Inadmissible ****/
 		head = atomic_load_explicit(&q->head, acquire);
 		/**
 			@Begin
@@ -194,9 +194,11 @@ bool dequeue(queue_t *q, int *retVal)
 		 * relaxed (it introduces a bug when there's two dequeuers and one
 		 * enqueuer) correctness bug!!
 		 */
+		/**** SPEC (sequential) (testcase1.c) ****/
+		/**** New bug ****/
 		tail = atomic_load_explicit(&q->tail, acquire);
 
-		/**** Detected UL/DR (testcase1.c) ****/
+		/**** SPEC Error (testcase1.c) ****/
 		next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
 		/**
 			@Begin
@@ -213,13 +215,13 @@ bool dequeue(queue_t *q, int *retVal)
 				if (get_ptr(next) == 0) { // NULL	
 					return false; // NULL
 				}
-				/**** Detected UL (testcase1.c) ****/
+				/**** SPEC (sequential testcase3.c) ****/
 				// Second release can be just relaxed
 				bool succ = false;
 				succ = atomic_compare_exchange_strong_explicit(&q->tail,
 						&tail,
 						MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
-						release, relaxed);
+							release, relaxed);
 				if (succ) {
 					//printf("miss4_dequeue CAS succ\n");
 				}
@@ -228,7 +230,7 @@ bool dequeue(queue_t *q, int *retVal)
 			} else {
 				//value = load_32(&q->nodes[get_ptr(next)].value);
 				value = q->nodes[get_ptr(next)].value;
-				/**** correctness error ****/
+				/**** inadmissibility ****/
 				success = atomic_compare_exchange_strong_explicit(&q->head,
 						&head,
 						MAKE_POINTER(get_ptr(next), get_count(head) + 1),