changes

[model-checker-benchmarks.git] / treiber-stack / stack_wildcard.h

diff --git a/treiber-stack/stack_wildcard.h b/treiber-stack/stack_wildcard.h
index 75c375ad86777cff85bbe6feb9d973114b5d38ad..72a761af741b0a2c3c2d5f65b0c1478b381f06c9 100644 (file)
--- 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;
        }
 };