From: Brian Norris <banorris@uci.edu>
Date: Fri, 8 Mar 2013 02:09:18 +0000 (-0800)
Subject: ms-queue: relax the second load of head/tail
X-Git-Tag: oopsla2013-final~21
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker-benchmarks.git;a=commitdiff_plain;h=606a0838f29e24305626a4229935f2ce4d96e963;hp=688f4bdb69ca33ce415fff112af8000a669466e2

ms-queue: relax the second load of head/tail
---

diff --git a/ms-queue/my_queue.c b/ms-queue/my_queue.c
index efab237..d658407 100644
--- a/ms-queue/my_queue.c
+++ b/ms-queue/my_queue.c
@@ -70,7 +70,7 @@ void enqueue(queue_t *q, unsigned int val)
 	while (!success) {
 		tail = atomic_load_explicit(&q->tail, acquire);
 		next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
-		if (tail == atomic_load_explicit(&q->tail, acquire)) {
+		if (tail == atomic_load_explicit(&q->tail, relaxed)) {
 			if (get_ptr(next) == 0) { // == NULL
 				pointer value = MAKE_POINTER(node, get_count(next) + 1);
 				success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
@@ -105,7 +105,7 @@ unsigned int dequeue(queue_t *q)
 		head = atomic_load_explicit(&q->head, acquire);
 		tail = atomic_load_explicit(&q->tail, acquire);
 		next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
-		if (atomic_load_explicit(&q->head, acquire) == head) {
+		if (atomic_load_explicit(&q->head, relaxed) == head) {
 			if (get_ptr(head) == get_ptr(tail)) {
 				if (get_ptr(next) == 0) { // NULL
 					return 0; // NULL