From: Peizhao Ou <peizhaoo@uci.edu>
Date: Tue, 13 Jan 2015 21:06:33 +0000 (-0800)
Subject: changes to ms-queue spec
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d37341bf7e15cffc4367435b89dc94736dbe72d1;p=cdsspec-compiler.git

changes to ms-queue spec
---

diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index d3bc9c2..4a9f689 100644
--- a/benchmark/ms-queue/main.c
+++ b/benchmark/ms-queue/main.c
@@ -43,11 +43,21 @@ static void main_task(void *param)
 	if (!pid) {
 		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]);
+		else
+			printf("Dequeue NULL.\n");
 	} else {
 		input[1] = 37;
 		enqueue(queue, input[1]);
+		printf("Enqueue %d.\n", 37);
 		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 c70adac..1d9e924 100644
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -22,12 +22,10 @@ static unsigned int new_node()
 	int i;
 	int t = get_thread_num();
 	for (i = 0; i < MAX_FREELIST; i++) {
-		//unsigned int node = load_32(&free_lists[t][i]);
-		unsigned int node = free_lists[t][i];
+		unsigned int node = load_32(&free_lists[t][i]);
 		//unsigned int node = free_lists[t][i];
 		if (node) {
-			//store_32(&free_lists[t][i], 0);
-			free_lists[t][i] = 0;
+			store_32(&free_lists[t][i], 0);
 			//free_lists[t][i] = 0;
 			return node;
 		}
@@ -48,14 +46,12 @@ static void reclaim(unsigned int node)
 
 	for (i = 0; i < MAX_FREELIST; i++) {
 		/* Should never race with our own thread here */
-		//unsigned int idx = load_32(&free_lists[t][i]);
-		unsigned int idx = free_lists[t][i];
+		unsigned int idx = load_32(&free_lists[t][i]);
 		//unsigned int idx = free_lists[t][i];
 
 		/* Found empty spot in free list */
 		if (idx == 0) {
-			//store_32(&free_lists[t][i], node);
-			free_lists[t][i] = node;
+			store_32(&free_lists[t][i], node);
 			//free_lists[t][i] = node;
 			return;
 		}
@@ -98,18 +94,30 @@ void enqueue(queue_t *q, unsigned int val)
 	pointer tmp;
 
 	node = new_node();
-	//store_32(&q->nodes[node].value, val);
-	q->nodes[node].value = val;
+	store_32(&q->nodes[node].value, val);
 	//q->nodes[node].value = val;
 	tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
 	set_ptr(&tmp, 0); // NULL
 	atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
 
 	while (!success) {
-		/**** detected UL (2 threads, 1 enqueue & 1 dequeue)  ****/
+		/**
+			@Begin
+			@Commit_point_clear: true
+			@Label: Enqueue_Clear
+			@End
+		*/
+		/**** detected UL ****/
 		tail = atomic_load_explicit(&q->tail, acquire);
+		/**
+			@Begin
+			@Commit_point_define_check: true
+			@Label: Enqueue_Read_Tail
+			@End
+		*/
 		/****FIXME: miss ****/
 		next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
+		//printf("miss1_enqueue\n");
 		if (tail == atomic_load_explicit(&q->tail, relaxed)) {
 
 			/* Check for uninitialized 'next' */
@@ -117,23 +125,25 @@ void enqueue(queue_t *q, unsigned int val)
 
 			if (get_ptr(next) == 0) { // == NULL
 				pointer value = MAKE_POINTER(node, get_count(next) + 1);
-				/**** correctness error (1 dequeue & 1 enqueue) ****/
+				/**** detected UL ****/
+				// Second release can be just relaxed
 				success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
 						&next, value, release, relaxed);
 				/**
 					@Begin
-					@Commit_point_define_check: success == true
-					@Label: Enqueue_Success_Point
+					@Commit_point_define_check: success
+					@Label: Enqueue_UpdateNext
 					@End
 				*/
 			}
 			if (!success) {
 				// This routine helps the other enqueue to update the tail
-				/**** detected UL (2 threads, 1 enqueue & 1 dequeue) ****/
+				/**** detected UL ****/
 				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 ****/
+				// Second release can be just relaxed
 				bool succ = false;
 				succ = atomic_compare_exchange_strong_explicit(&q->tail,
 						&tail, value, release, relaxed);
@@ -145,11 +155,18 @@ void enqueue(queue_t *q, unsigned int val)
 			}
 		}
 	}
-	/**** correctness error (1 dequeue & 1 enqueue) ****/
-	atomic_compare_exchange_strong_explicit(&q->tail,
+	/**** dectected UL ****/
+	// Second release can be just relaxed
+	bool succ = atomic_compare_exchange_strong_explicit(&q->tail,
 			&tail,
 			MAKE_POINTER(node, get_count(tail) + 1),
 			release, relaxed);
+	/**
+		@Begin
+		@Commit_point_define_check: succ 
+		@Label: Enqueue_UpdateOrLoad_Tail
+		@End
+	*/
 }
 
 /**
@@ -157,7 +174,7 @@ void enqueue(queue_t *q, unsigned int val)
 	@Interface_define: Dequeue
 	@End
 */
-bool dequeue(queue_t *q, unsigned int *retVal)
+bool dequeue(queue_t *q, int *output)
 {
 	unsigned int value;
 	int success = 0;
@@ -166,15 +183,37 @@ bool dequeue(queue_t *q, unsigned int *retVal)
 	pointer next;
 
 	while (!success) {
-		/**** FIXME: miss ****/
+		/**
+			@Begin
+			@Commit_point_clear: true
+			@Label: Dequeue_Clear
+			@End
+		*/
+		/**** detected correctness error ****/
 		head = atomic_load_explicit(&q->head, acquire);
-		// This must be acquire otherwise we have a bug with 1 enqueue &
-		// 1 dequeue
-		/**** correctness error (1 dequeue & 1 enqueue) ****/
-		tail = atomic_load_explicit(&q->tail, acquire);
-		/**** correctness error (1 dequeue & 1 enqueue) ****/
+		/**
+			@Begin
+			@Commit_point_define_check: true
+			@Label: Dequeue_Read_Head
+			@End
+		*/
+		tail = atomic_load_explicit(&q->tail, relaxed);
+		/**
+			@Begin
+			@Potential_commit_point_define: true
+			@Label: Dequeue_Potential_Read_Tail
+			@End
+		*/
+
+		/****FIXME: miss ****/
 		next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
-		//printf("miss3_dequeue\n");
+		/**
+			@Begin
+			@Potential_commit_point_define: true 
+			@Label: Dequeue_Potential_LoadNext
+			@End
+		*/
+		
 		if (atomic_load_explicit(&q->head, relaxed) == head) {
 			if (get_ptr(head) == get_ptr(tail)) {
 
@@ -184,13 +223,15 @@ bool dequeue(queue_t *q, unsigned int *retVal)
 				if (get_ptr(next) == 0) { // NULL
 					/**
 						@Begin
-						@Commit_point_define_check: true
-						@Label: Dequeue_Empty_Point
+						@Commit_point_define: true
+						@Potential_commit_point_label: Dequeue_Potential_Read_Tail
+						@Label: Dequeue_Read_Tail
 						@End
 					*/
 					return false; // NULL
 				}
 				/****FIXME: miss (not reached) ****/
+				// Second release can be just relaxed
 				bool succ = false;
 				succ = atomic_compare_exchange_strong_explicit(&q->tail,
 						&tail,
@@ -202,25 +243,26 @@ bool dequeue(queue_t *q, unsigned int *retVal)
 				//printf("miss4_dequeue\n");
 				thrd_yield();
 			} else {
-				//*retVal = load_32(&q->nodes[get_ptr(next)].value);
-				*retVal = q->nodes[get_ptr(next)].value;
+				/**
+					@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);
 				//value = q->nodes[get_ptr(next)].value;
-				/**** FIXME: miss (not reached) ****/
+				/****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_check: success == true
-					@Label: Dequeue_Success_Point
-					@End
-				*/
 				if (!success)
 					thrd_yield();
 			}
 		}
 	}
 	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 d6b2a69..714be4f 100644
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -88,7 +88,7 @@ void init_queue(queue_t *q, int num_threads);
 /**
 	@Begin
 	@Interface: Enqueue
-	@Commit_point_set: Enqueue_Success_Point
+	@Commit_point_set: Enqueue_Read_Tail | Enqueue_UpdateNext | Enqueue_UpdateOrLoad_Tail
 	@ID: get_and_inc(tag)
 	@Action:
 		# __ID__ is an internal macro that refers to the id of the current
@@ -102,7 +102,7 @@ void enqueue(queue_t *q, unsigned int val);
 /**
 	@Begin
 	@Interface: Dequeue
-	@Commit_point_set: Dequeue_Success_Point | Dequeue_Empty_Point
+	@Commit_point_set: Dequeue_Read_Head | Dequeue_Read_Tail | Dequeue_LoadNext
 	@ID: get_id(front(__queue))
 	@Action:
 		unsigned int _Old_Val = 0;
@@ -113,10 +113,10 @@ void enqueue(queue_t *q, unsigned int val);
 			_Old_Val = 0;
 		}
 	@Post_check:
-		_Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
+		__RET__ ? *output == _Old_Val : _Old_Val == 0
 	@End
 */
-bool dequeue(queue_t *q, unsigned int *retVal);
+bool dequeue(queue_t *q, int *output);
 int get_thread_num();
 
 #endif
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index 43e4e76..0ee2ee0 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -597,6 +597,7 @@ public class CodeVariables {
 		newCode.add("\t"
 				+ ASSIGN_TO_PTR(structName, "interface_num", interfaceNum)
 				+ SHORT_COMMENT(construct.name));
+		newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_name", "\"" + construct.name + "\""));
 
 		String anno = "annotation_interface_begin";
 		newCode.add("\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
@@ -765,6 +766,7 @@ public class CodeVariables {
 		String labelNum = Integer.toString(semantics.commitPointLabel2Num
 				.get(construct.label));
 		newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_num", labelNum));
+		newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_name", "\"" + construct.label + "\""));
 		newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
 		newCode.add("\t\t"
 				+ ASSIGN_TO_PTR(anno, "type",
@@ -816,6 +818,7 @@ public class CodeVariables {
 				.get(construct.label));
 		String interfaceNum = getCPInterfaceNum(semantics, construct.label);
 		newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_num", labelNum));
+		newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_name", "\"" + construct.label + "\""));
 		newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
 		newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
 		newCode.add("\t\t"
@@ -898,9 +901,11 @@ public class CodeVariables {
 				.toString(semantics.commitPointLabel2Num
 						.get(construct.potentialCPLabel));
 		newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_num", labelNum));
+		newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_name", "\"" + construct.label + "\""));
 		newCode.add("\t\t"
 				+ ASSIGN_TO_PTR(structName, "potential_cp_label_num",
 						potentialLabelNum));
+		newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "potential_label_name", "\"" + construct.potentialCPLabel + "\""));
 		newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
 		newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
 		newCode.add("\t\t"