From eeea572e974cb93f35d6788250d011a031ffba2f Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Wed, 14 Jan 2015 17:53:26 -0800
Subject: [PATCH] changes

---
 benchmark/ms-queue/main.c                     | 31 ++++++-------------
 benchmark/ms-queue/my_queue.c                 | 28 ++++++++---------
 benchmark/ms-queue/my_queue.h                 |  2 +-
 .../codeGenerator/CodeGenerator.java          |  3 +-
 4 files changed, 26 insertions(+), 38 deletions(-)

diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index f6973a7..6384667 100644
--- a/benchmark/ms-queue/main.c
+++ b/benchmark/ms-queue/main.c
@@ -5,7 +5,7 @@
 #include "my_queue.h"
 #include "model-assert.h"
 
-static int procs = 3;
+static int procs = 2;
 static queue_t *queue;
 static thrd_t *threads;
 static unsigned int *input;
@@ -39,39 +39,28 @@ static void main_task(void *param)
 		enqueue(queue, input[1]);
 	}
 */
-
-	if (pid % 3 == 0) {
+	if (pid % 2 == 0) {
 		input[0] = 17;
 		enqueue(queue, input[0]);
-		printf("Enqueue %d.\n", 17);
+		printf("Thrd %d Enqueue %d.\n", get_thread_num(), input[0]);
 		
-		succ1 = dequeue(queue, &input[0]);
+		succ1 = dequeue(queue, &output[0]);
 		if (succ1)
-			printf("Thrd 2: Dequeue %d.\n", input[0]);
+			printf("Thrd %d: Dequeue %d.\n", get_thread_num(), output[0]);
 		else
-			printf("Thrd 2: Dequeue NULL.\n");
-		
-	} else if (pid % 3 == 1) {
+			printf("Thrd %d: Dequeue NULL.\n", get_thread_num());
 		
+	} else if (pid % 2 == 1) {
 		input[1] = 37;
 		enqueue(queue, input[1]);
-		printf("Enqueue %d.\n", 37);
+		printf("Thrd %d Enqueue %d.\n", get_thread_num(), input[1]);
 		
-		succ1 = dequeue(queue, &input[0]);
-		if (succ1)
-			printf("Thrd 3: Dequeue %d.\n", input[0]);
-		else
-			printf("Thrd 3: Dequeue NULL.\n");
-	} else if (pid %3 == 2) {
-		/*
 		succ2 = dequeue(queue, &output[1]);
 		if (succ2)
-			printf("Dequeue %d.\n", input[1]);
+			printf("Thrd %d: Dequeue %d.\n", get_thread_num(), output[1]);
 		else
-			printf("Dequeue NULL.\n");
-			*/
+			printf("Thrd %d: Dequeue NULL.\n", get_thread_num());
 	}
-
 }
 
 int user_main(int argc, char **argv)
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;
 }
diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index 576ce9e..90f5775 100644
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -111,7 +111,7 @@ void enqueue(queue_t *q, unsigned int val);
 			_Old_Val = get_data(front(__queue));
 			pop_front(__queue);
 		}
-		model_print("Dequeue: __RET=%d, retVal=%d\n", __RET__, *retVal);
+		model_print("Dequeue: __RET__=%d, retVal=%d, Old_Val=%d\n", __RET__, *retVal, _Old_Val);
 	@Post_check:
 		_Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
 	@End
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 7386052..e95ff5f 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -298,6 +298,7 @@ public class CodeGenerator {
 
 		File[] srcMSQueue = {
 				new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
+				new File(homeDir + "/benchmark/ms-queue/testcase.c"),
 				new File(homeDir + "/benchmark/ms-queue/main.c"),
 				new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
 
@@ -325,7 +326,7 @@ public class CodeGenerator {
 //		File[][] sources = { srcLinuxRWLocks,  srcMSQueue, srcRCU,
 //				srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable };
 
-		 File[][] sources = {srcMSQueue };
+		 File[][] sources = {srcMSQueue, srcHashtable };
 		// Compile all the benchmarks
 		for (int i = 0; i < sources.length; i++) {
 			CodeGenerator gen = new CodeGenerator(sources[i]);
-- 
2.34.1