From 9401817822c7752de3f0e64be1bd82fa63242875 Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Thu, 19 Nov 2015 12:18:18 -0800
Subject: [PATCH] edits

---
 benchmark/chase-lev-deque-bugfix/deque.c | 41 ------------------------
 benchmark/ms-queue/my_queue.c            | 30 +++--------------
 2 files changed, 5 insertions(+), 66 deletions(-)

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index b4f6317..3ad32af 100644
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -158,12 +158,6 @@ int steal(Deque *q) {
 	//Watch out: actually on need to be an acquire (don't count it)
 	// An old bug
 	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);
 	/**** SPEC & UL ****/
@@ -174,57 +168,22 @@ int steal(Deque *q) {
 		@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
-			@Potential_commit_point_define: true
-			@Label: Steal_Potential_Read_Buffer
-			@End
-		*/
 		/**** SPEC (sequential) ****/ 
 		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_CAS_Top
-			@End
-		*/
-
 		/**
 			@Begin
 			@Additional_ordering_point_define_check: true 
 			@Label: Steal_Additional_Point
 			@End
 		*/
-
-		/**
-			//@Begin
-			@Commit_point_define: succ
-			@Potential_commit_point_label: Steal_Potential_Read_Buffer
-			@Label: Steal_Read_Buffer
-			@End
-		*/
 		if (!succ) {
 			/* Failed race. */
 			return ABORT;
diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index fdea1a4..b2334c8 100644
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -104,13 +104,6 @@ void enqueue(queue_t *q, unsigned int val)
 	atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
 
 	while (!success) {
-		
-		/**
-			@Begin
-			@Commit_point_clear: true
-			@Label: Enqueue_Clear
-			@End
-		*/
 		/**** UL & inadmissible ****/
 		tail = atomic_load_explicit(&q->tail, acquire);
 		/****FIXME: miss ****/
@@ -144,7 +137,7 @@ void enqueue(queue_t *q, unsigned int val)
 				// Second release can be just relaxed
 				bool succ = false;
 				succ = atomic_compare_exchange_strong_explicit(&q->tail,
-						&tail, value, relaxed, relaxed);
+						&tail, value, release, relaxed);
 				if (succ) {
 					//printf("miss2_enqueue CAS succ\n");
 				}
@@ -153,7 +146,7 @@ void enqueue(queue_t *q, unsigned int val)
 			}
 		}
 	}
-	/**** UL & Inadmissible ****/
+	/**** UL & Inadmissible (main.c) ****/
 	// Second release can be just relaxed
 	bool succ = atomic_compare_exchange_strong_explicit(&q->tail,
 			&tail,
@@ -181,7 +174,8 @@ bool dequeue(queue_t *q, int *retVal)
 			@Label: Dequeue_Clear
 			@End
 		*/
-		/**** Inadmissible ****/
+
+		/**** Inadmissible (main.c) ****/
 		head = atomic_load_explicit(&q->head, acquire);
 		/**
 			@Begin
@@ -200,12 +194,6 @@ bool dequeue(queue_t *q, int *retVal)
 
 		/**** SPEC Error (testcase1.c) ****/
 		next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
-		/**
-			@Begin
-			@Potential_commit_point_define: true
-			@Label: DequeueReadNext
-			@End
-		*/
 		if (atomic_load_explicit(&q->head, relaxed) == head) {
 			if (get_ptr(head) == get_ptr(tail)) {
 
@@ -230,7 +218,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;
-				/**** inadmissibility ****/
+				/**** inadmissibility (main.c) ****/
 				success = atomic_compare_exchange_strong_explicit(&q->head,
 						&head,
 						MAKE_POINTER(get_ptr(next), get_count(head) + 1),
@@ -241,14 +229,6 @@ bool dequeue(queue_t *q, int *retVal)
 					@Label: DequeueUpdateHead
 					@End
 				*/
-
-				/**
-					@Begin
-					@Commit_point_define: success
-					@Potential_commit_point_label: DequeueReadNext
-					@Label: DequeueReadNextVerify
-					@End
-				*/
 				if (!success)
 					thrd_yield();
 			}
-- 
2.34.1