save

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index 2cfbb76a0607a9d743e8e3235fb624ad6fd975a7..b556460bd5d6fb095c6e623a786d36c0545a641b 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -35,7 +35,11 @@ int take(Deque *q) {
        int x;
        if (t <= b) {
                /* Non-empty queue. */
-               x = atomic_load_explicit(&a->buffer[b % atomic_load_explicit(&a->size,memory_order_relaxed)], memory_order_relaxed);
+               int size = atomic_load_explicit(&a->size, memory_order_relaxed);
+               if (size == 0) 
+                       model_print("take: size == 0\n");
+               // TODO: size can be zero here!!
+               x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
                /**
                        @Begin
                        @Commit_point_define_check: t != b
@@ -82,6 +86,10 @@ void resize(Deque *q) {
        atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed);
        size_t i;
        for(i=top; i < bottom; i++) {
+               if (new_size == 0)
+                       model_print("resize: new_size == 0\n");
+               if (size == 0)
+                       model_print("resize: size == 0\n");
                atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
        }
        atomic_store_explicit(&q->array, new_a, memory_order_release);
@@ -102,7 +110,10 @@ void push(Deque *q, int x) {
                //Bug in paper...should have next line...
                a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
        }
-       atomic_store_explicit(&a->buffer[b % atomic_load_explicit(&a->size, memory_order_relaxed)], x, memory_order_relaxed);
+       int size = atomic_load_explicit(&a->size, memory_order_relaxed);
+       if (size == 0) 
+               model_print("push: size == 0\n");
+       atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
        atomic_thread_fence(memory_order_release);
        /**
                @Begin
@@ -132,7 +143,10 @@ int steal(Deque *q) {
        if (t < b) {
                /* Non-empty queue. */
                Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
-               x = atomic_load_explicit(&a->buffer[t % atomic_load_explicit(&a->size, memory_order_relaxed)], memory_order_relaxed);
+               int size = atomic_load_explicit(&a->size, memory_order_relaxed);
+               if (size == 0) 
+                       model_print("steal: size == 0\n");
+               x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
                bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
                        memory_order_seq_cst, memory_order_relaxed);
                /**

diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h
index 8ddcdb6b27fb878b2a356acb086ab0a8ca3b8f81..b046cc7b7cc0d11af1d578be663ff067c39ae60a 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.h
+++ b/benchmark/chase-lev-deque-bugfix/deque.h
@@ -5,6 +5,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h"
 
 typedef struct {
        atomic_size_t size;

diff --git a/benchmark/chase-lev-deque-bugfix/main.c b/benchmark/chase-lev-deque-bugfix/main.c
index 481f3da59994833291cbf8b1e181b604ebc2e9a3..a67be6efad20e8f81fdf029c1ffe13e8e363a29c 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/main.c
+++ b/benchmark/chase-lev-deque-bugfix/main.c
@@ -13,10 +13,14 @@ int a;
 int b;
 int c;
 
-static void task(void * param) {
+static void task1(void * param) {
        a=steal(q);
 }
 
+static void task2(void * param) {
+       a=take(q);
+}
+
 int user_main(int argc, char **argv)
 {
        /**
@@ -24,15 +28,17 @@ int user_main(int argc, char **argv)
                @Entry_point
                @End
        */
-       thrd_t t;
+       thrd_t t1, t2;
        q=create();
-       thrd_create(&t, task, 0);
        push(q, 1);
        push(q, 2);
+       thrd_create(&t1, task1, 0);
+       thrd_create(&t2, task2, 0);
        push(q, 4);
        b=take(q);
        c=take(q);
-       thrd_join(t);
+       thrd_join(t1);
+       thrd_join(t2);
 
        bool correct=true;
        if (a!=1 && a!=2 && a!=4 && a!= EMPTY)
@@ -45,7 +51,7 @@ int user_main(int argc, char **argv)
                correct=false;
        if (!correct)
                printf("a=%d b=%d c=%d\n",a,b,c);
-       MODEL_ASSERT(correct);
+       //MODEL_ASSERT(correct);
 
        return 0;
 }

diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h
index c3cea0d20fef1ae5130a603201508c7acfedc279..536f1c42304ffc470c1b0547686a8f19c94f4774 100644 (file)
--- a/benchmark/cliffc-hashtable/cliffc_hashtable.h
+++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h
@@ -16,6 +16,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h" 
 
 using namespace std;
 

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index eaae816015c3cf6672a28d1990f096d922c7b2f9..6341c4c1fcf336474ea9008b5e84b3e083b0968f 100644 (file)
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -7,6 +7,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h"
 
 #include "librace.h"
 

diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h
index 27ce1807f2c3b25fb266e170139fd009d221b169..e08a0e73c1a844736daa0196e94a3dea4c3f182e 100644 (file)
--- a/benchmark/mcs-lock/mcs-lock.h
+++ b/benchmark/mcs-lock/mcs-lock.h
@@ -8,6 +8,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h" 
 
 struct mcs_node {
        std::atomic<mcs_node *> next;
@@ -34,7 +35,7 @@ public:
                m_tail.store( NULL );
        }
        ~mcs_mutex() {
-               ASSERT( m_tail.load() == NULL );
+               //ASSERT( m_tail.load() == NULL );
        }
 
        // Each thread will have their own guard.

diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h
index d78ff6cfe03d3496e3e173c2b90eb7018f3449ea..cd9d430082a4229311f277ba5a96243d1ba82b05 100644 (file)
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -7,6 +7,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h" 
 
 /**
        @Begin

diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index 0346c1ddeb97db4f2f58b56d2681b852e2a0fccd..200ae4558eab7e5251ea47eeac582f723511016e 100644 (file)
--- a/benchmark/ms-queue/main.c
+++ b/benchmark/ms-queue/main.c
@@ -19,7 +19,7 @@ int get_thread_num()
        for (i = 0; i < num_threads; i++)
                if (curr.priv == threads[i].priv)
                        return i;
-       MODEL_ASSERT(0);
+       //MODEL_ASSERT(0);
        return -1;
 }
 

diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index 9ef2d6399cc00ff6fb63fd995d2a5728df682e5f..0d833921a127dd4c99aac45a35efbf2ccab99902 100644 (file)
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -8,6 +8,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h" 
 
 #define MAX_NODES                      0xf
 

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index 3b495592a5f3a726d57793655af7fcd7466d7eea..34deba7e857aca5c85c8705a80d49e98e2d0791e 100644 (file)
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -98,6 +98,21 @@ void write(Data *new_data) {
        //model_print("Write: %d\n", new_data);
 }
 
+/*
+Data *prev = data.load(memory_order_acquire);
+bool succ = false;
+Data *tmp = malloc(sizeof(Data));
+do {
+        tmp->data1=prev->data1+new_data->data1;
+        tmp->data2=prev->data2+new_data->data2;
+        tmp->data3=prev->data3+new_data->data3;
+        succ = data.compare_exchange_strong(prev, tmp,
+                           memory_order_release, memory_order_acquire);
+           } while (!succ);
+           //model_print("Write: %d\n", new_data);
+}
+*/
+
 void threadA(void *arg) {
        Data *dataA = (Data*) malloc(sizeof(Data));
        dataA->data1 = 3;

diff --git a/benchmark/spsc-bugfix/queue.h b/benchmark/spsc-bugfix/queue.h
index 76c520036e7dc3b37aaf436e75014c987dfa6397..b47452e5b61d0cc98bf1572524ce71f1189a7444 100644 (file)
--- a/benchmark/spsc-bugfix/queue.h
+++ b/benchmark/spsc-bugfix/queue.h
@@ -9,6 +9,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h" 
 
 #include "eventcount.h"
 

diff --git a/benchmark/spsc-bugfix/spsc-queue.cc b/benchmark/spsc-bugfix/spsc-queue.cc
index f8528a862acd8f5097ebb3d781e73e8eb7955864..e3a4a6d568d0553ef65f13addd2507e21f31288b 100644 (file)
--- a/benchmark/spsc-bugfix/spsc-queue.cc
+++ b/benchmark/spsc-bugfix/spsc-queue.cc
@@ -13,7 +13,7 @@ spsc_queue<int> *q;
                else
                {
                        int d = q->dequeue();
-                       RL_ASSERT(11 == d);
+                       //RL_ASSERT(11 == d);
                }
        }