changes

diff --git a/treiber-stack/Makefile b/treiber-stack/Makefile
index 40b3cb5a535169900aeda616ad8b4517f2cc7a29..6e8bbfed36ceeb1f042742e0efcdda0a0ea2142b 100644 (file)
--- a/treiber-stack/Makefile
+++ b/treiber-stack/Makefile
@@ -10,6 +10,7 @@ TESTS := $(NORMAL_TESTS) $(WILDCARD_TESTS)
 
 all: $(TESTS)
 
+$(WILDCARD_TESTS): CXXFLAGS += -DWILDCARD
 $(WILDCARD_TESTS): %_wildcard : %.cc $(BENCH)_wildcard.h 
        $(CXX) -o $@ $^ $(CXXFLAGS) $(LDFLAGS)
 

diff --git a/treiber-stack/stack.h b/treiber-stack/stack.h
index de551cb802bd79a64012be7001cc21dcacca9881..4428876a37caa4fea6ff653906c9f2a63fce5481 100644 (file)
--- a/treiber-stack/stack.h
+++ b/treiber-stack/stack.h
@@ -8,7 +8,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;
@@ -25,10 +28,11 @@ struct stack {
 
        void push(unsigned int val) {
                node *n = new node(val);
-               node *old = top.load(acquire);
+               node *old = top.load(relaxed);
                do {
-                       n->next = old;
-               } while (!top.compare_exchange_strong(old, n, acq_rel, relaxed));
+                       // n->next = old;
+                       n->next.store(old, relaxed);
+               } while (!top.compare_exchange_strong(old, n, release, relaxed));
        }
 
        unsigned int pop() {
@@ -37,8 +41,9 @@ struct stack {
                do {
                        if (!old)
                                return 0;
-                       n = old->next;
-               } while (!top.compare_exchange_strong(old, n, acq_rel, acquire));
+                       //n = old->next;
+                       n = old->next.load(relaxed);
+               } while (!top.compare_exchange_strong(old, n, relaxed, relaxed));
                return old->value;
        }
 };

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;
        }
 };

diff --git a/treiber-stack/testcase1.cc b/treiber-stack/testcase1.cc
index 7ca474d5fa54b9b1075b5d3cf5b44619b77fadb5..dc76ebf88b859fb4426fd46abb02b5858872ff30 100644 (file)
--- a/treiber-stack/testcase1.cc
+++ b/treiber-stack/testcase1.cc
@@ -3,7 +3,11 @@
 #include <threads.h>
 #include "model-assert.h"
 
+#ifdef WILDCARD
+#include "stack_wildcard.h"
+#else
 #include "stack.h"
+#endif
 
 static int procs = 4;
 static stack *s;