X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=ms-queue%2Fqueue_wildcard.c;h=73289a7af9f044581841c0b671fc05db005b1d62;hb=e4f5d19cd0d94393277381f8aab95126f201fb26;hp=df1702aa375cd38581ea499e74cb3c2583f8531a;hpb=1438eb7c0715e53611a717e593bfa3fe1bd30588;p=model-checker-benchmarks.git

diff --git a/ms-queue/queue_wildcard.c b/ms-queue/queue_wildcard.c
index df1702a..73289a7 100644
--- a/ms-queue/queue_wildcard.c
+++ b/ms-queue/queue_wildcard.c
@@ -103,12 +103,19 @@ void enqueue(queue_t *q, unsigned int val)
 
 			if (get_ptr(next) == 0) { // == NULL
 				pointer value = MAKE_POINTER(node, get_count(next) + 1);
+				
+				// ***********************************
+				// Inference analysis results have two choices here, it either
+				// makes wildcard(6) acq_rel and wildcard(8) relaxed or
+				// wildcard(6) release and wildcard(8) acquire. The
+				// synchronization here is for enqueue() to dequeue(), and
+				// actually either synchronization options will work!!!
 				success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
 						&next, value, wildcard(6), wildcard(7)); // release & relaxed
 			}
 			if (!success) {
 				unsigned int ptr =
-				get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, wildcard(8))); // acquire
+					get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, wildcard(8))); // acquire
 				pointer value = MAKE_POINTER(ptr,
 						get_count(tail) + 1);
 				atomic_compare_exchange_strong_explicit(&q->tail,
@@ -134,7 +141,7 @@ bool dequeue(queue_t *q, unsigned int *retVal)
 
 	while (!success) {
 		head = atomic_load_explicit(&q->head, wildcard(13)); // acquire
-		// FIXME: SCFence makes this acquire
+		// SCFence makes this acquire, and we actually need an acquire here!!!
 		tail = atomic_load_explicit(&q->tail, wildcard(14)); // relaxed 
 		next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, wildcard(15)); // acquire
 		if (atomic_load_explicit(&q->head, wildcard(16)) == head) { // relaxed
@@ -154,7 +161,6 @@ bool dequeue(queue_t *q, unsigned int *retVal)
 			} else {
 				//value = load_32(&q->nodes[get_ptr(next)].value);
 				value = q->nodes[get_ptr(next)].value;
-				// FIXME: SCFence makes this relaxed 
 				success = atomic_compare_exchange_strong_explicit(&q->head,
 						&head, MAKE_POINTER(get_ptr(next), get_count(head) + 1),
 						wildcard(19), wildcard(20)); // release & relaxed