From fbc06391161f561c10228740688e2e0bb6b936fa Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Tue, 26 Aug 2014 16:53:46 -0700
Subject: [PATCH] changes

---
 benchmark/ms-queue/main.c     |  6 +++---
 benchmark/ms-queue/my_queue.c | 10 ++++++----
 benchmark/ms-queue/my_queue.h |  4 ++--
 3 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index a2e8e9a..4840014 100644
--- a/benchmark/ms-queue/main.c
+++ b/benchmark/ms-queue/main.c
@@ -32,13 +32,13 @@ static void main_task(void *param)
 		input[0] = 17;
 		//enqueue(queue, input[0]);
 		enqueue(queue, input[0]);
-		output[0] = dequeue(queue);
+		//output[0] = dequeue(queue);
 	} else {
 		input[1] = 37;
-		enqueue(queue, input[1]);
+		//enqueue(queue, input[1]);
 		//output[1] = dequeue(queue);
 		//output[0] = dequeue(queue);
-		output[0] = dequeue(queue);
+		bool succ = dequeue(queue, &output[0]);
 	}
 }
 
diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 1f4835e..5078785 100644
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -156,7 +156,7 @@ void enqueue(queue_t *q, unsigned int val)
 	@Interface_define: Dequeue
 	@End
 */
-unsigned int dequeue(queue_t *q)
+bool dequeue(queue_t *q, unsigned int *retVal)
 {
 	unsigned int value;
 	int success = 0;
@@ -167,6 +167,8 @@ unsigned int dequeue(queue_t *q)
 	while (!success) {
 		/**** detected correctness error ****/
 		head = atomic_load_explicit(&q->head, acquire);
+		// FIXME: This must be acquire otherwise we have a bug with 1 enqueue &
+		// 1 dequeue
 		tail = atomic_load_explicit(&q->tail, relaxed);
 		/****FIXME: miss ****/
 		next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
@@ -184,7 +186,7 @@ unsigned int dequeue(queue_t *q)
 						@Label: Dequeue_Empty_Point
 						@End
 					*/
-					return 0; // NULL
+					return false; // NULL
 				}
 				/****FIXME: miss (not reached) ****/
 				// Second release can be just relaxed
@@ -199,7 +201,7 @@ unsigned int dequeue(queue_t *q)
 				//printf("miss4_dequeue\n");
 				thrd_yield();
 			} else {
-				value = load_32(&q->nodes[get_ptr(next)].value);
+				*retVal = load_32(&q->nodes[get_ptr(next)].value);
 				//value = q->nodes[get_ptr(next)].value;
 				/****FIXME: correctness error ****/
 				// Seconde release can be just relaxed
@@ -219,5 +221,5 @@ unsigned int dequeue(queue_t *q)
 		}
 	}
 	reclaim(get_ptr(head));
-	return value;
+	return true;
 }
diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index bc4c345..d6b2a69 100644
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -113,10 +113,10 @@ void enqueue(queue_t *q, unsigned int val);
 			_Old_Val = 0;
 		}
 	@Post_check:
-		_Old_Val == __RET__
+		_Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
 	@End
 */
-unsigned int dequeue(queue_t *q);
+bool dequeue(queue_t *q, unsigned int *retVal);
 int get_thread_num();
 
 #endif
-- 
2.34.1