X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=treiber-stack%2Fstack_wildcard.h;h=72a761af741b0a2c3c2d5f65b0c1478b381f06c9;hb=d634d19b6134309ed0893c6fd58d815cbafecd16;hp=75c375ad86777cff85bbe6feb9d973114b5d38ad;hpb=bab731cf43b743adfd95447f5f72200cd22611dd;p=model-checker-benchmarks.git

diff --git a/treiber-stack/stack_wildcard.h b/treiber-stack/stack_wildcard.h
index 75c375a..72a761a 100644
--- a/treiber-stack/stack_wildcard.h
+++ b/treiber-stack/stack_wildcard.h
@@ -10,7 +10,10 @@
 
 struct node {
 	unsigned int value;
-	node *next;
+	// This field does not have to be atomic, but in the inference analysis, we
+	// might have a data race for this field without the proper synchronization.
+	//node *next;
+	atomic<node*> next;
 
 	node(unsigned int v) {
 		value = v;
@@ -29,20 +32,22 @@ struct stack {
 		node *n = new node(val);
 		node *old = top.load(wildcard(1)); // acquire
 		do {
-			n->next = old;
-		} while (!top.compare_exchange_strong(old, n, wildcard(2), wildcard(3)));
-		// acq_rel & relaxed
+			// n->next = old;
+			n->next.store(old, wildcard(2));
+		} while (!top.compare_exchange_strong(old, n, wildcard(3), wildcard(4)));
+		// relaxed & relaxed
 	}
 
 	unsigned int pop() {
-		node *old = top.load(wildcard(4)); // acquire
+		node *old = top.load(wildcard(5)); // acquire
 		node *n;
 		do {
 			if (!old)
 				return 0;
-			n = old->next;
-		} while (!top.compare_exchange_strong(old, n, wildcard(5), wildcard(6)));
-		// acq_rel & acquire
+			// n = old->next;
+			n = old->next.load(relaxed);
+		} while (!top.compare_exchange_strong(old, n, wildcard(6), wildcard(7)));
+		// relaxed & relaxed 
 		return old->value;
 	}
 };