From: Peizhao Ou <peizhaoo@uci.edu>
Date: Wed, 14 Jan 2015 02:12:00 +0000 (-0800)
Subject: changes
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=9e08fb16f226a6c13a3526150a41814746805631;hp=4256e5b631accf081eaa9a8a316715123f5f3cdb

changes
---

diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index 4a9f689..f6973a7 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 = 2;
+static int procs = 3;
 static queue_t *queue;
 static thrd_t *threads;
 static unsigned int *input;
@@ -40,24 +40,36 @@ static void main_task(void *param)
 	}
 */
 
-	if (!pid) {
+	if (pid % 3 == 0) {
 		input[0] = 17;
 		enqueue(queue, input[0]);
 		printf("Enqueue %d.\n", 17);
+		
 		succ1 = dequeue(queue, &input[0]);
 		if (succ1)
-			printf("Dequeue %d.\n", input[0]);
+			printf("Thrd 2: Dequeue %d.\n", input[0]);
 		else
-			printf("Dequeue NULL.\n");
-	} else {
+			printf("Thrd 2: Dequeue NULL.\n");
+		
+	} else if (pid % 3 == 1) {
+		
 		input[1] = 37;
 		enqueue(queue, input[1]);
 		printf("Enqueue %d.\n", 37);
+		
+		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]);
 		else
 			printf("Dequeue NULL.\n");
+			*/
 	}
 
 }
diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 1d9e924..bb237bf 100644
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -162,8 +162,8 @@ void enqueue(queue_t *q, unsigned int val)
 			MAKE_POINTER(node, get_count(tail) + 1),
 			release, relaxed);
 	/**
-		@Begin
-		@Commit_point_define_check: succ 
+		//@Begin
+		@Commit_point_define_check: succ
 		@Label: Enqueue_UpdateOrLoad_Tail
 		@End
 	*/
@@ -174,7 +174,7 @@ void enqueue(queue_t *q, unsigned int val)
 	@Interface_define: Dequeue
 	@End
 */
-bool dequeue(queue_t *q, int *output)
+bool dequeue(queue_t *q, int *retVal)
 {
 	unsigned int value;
 	int success = 0;
@@ -197,7 +197,7 @@ bool dequeue(queue_t *q, int *output)
 			@Label: Dequeue_Read_Head
 			@End
 		*/
-		tail = atomic_load_explicit(&q->tail, relaxed);
+		tail = atomic_load_explicit(&q->tail, acquire);
 		/**
 			@Begin
 			@Potential_commit_point_define: true
@@ -251,6 +251,7 @@ bool dequeue(queue_t *q, int *output)
 					@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,
@@ -263,6 +264,5 @@ bool dequeue(queue_t *q, int *output)
 		}
 	}
 	reclaim(get_ptr(head));
-	*output = value;
 	return true;
 }
diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index 714be4f..576ce9e 100644
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -88,13 +88,14 @@ void init_queue(queue_t *q, int num_threads);
 /**
 	@Begin
 	@Interface: Enqueue
-	@Commit_point_set: Enqueue_Read_Tail | Enqueue_UpdateNext | Enqueue_UpdateOrLoad_Tail
+	@Commit_point_set: Enqueue_Read_Tail | Enqueue_UpdateNext
 	@ID: get_and_inc(tag)
 	@Action:
 		# __ID__ is an internal macro that refers to the id of the current
 		# interface call
 		tag_elem_t *elem = new_tag_elem(__ID__, val);
 		push_back(__queue, elem);
+		model_print("Enqueue: input=%d\n", val);
 	@End
 */
 void enqueue(queue_t *q, unsigned int val);
@@ -109,14 +110,13 @@ void enqueue(queue_t *q, unsigned int val);
 		if (size(__queue) > 0) {
 			_Old_Val = get_data(front(__queue));
 			pop_front(__queue);
-		} else {
-			_Old_Val = 0;
 		}
+		model_print("Dequeue: __RET=%d, retVal=%d\n", __RET__, *retVal);
 	@Post_check:
-		__RET__ ? *output == _Old_Val : _Old_Val == 0
+		_Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
 	@End
 */
-bool dequeue(queue_t *q, int *output);
+bool dequeue(queue_t *q, int *retVal);
 int get_thread_num();
 
 #endif