save

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index 7c326560746464e35eff2db47416c4ea066063f3..e94da48abe8aeb92127052fff4b5a34f1d3cd8a4 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -45,11 +45,12 @@ int take(Deque *q) {
                */
                if (t == b) {
                        /* Single last element in queue. */
+                       //FIXME: weaken the following seq_cst causes no spec problem
                        bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
                                1, memory_order_seq_cst, memory_order_relaxed);
                        /**
                                @Begin
-                               @Commit_point_define_check: succ
+                               @Commit_point_define_check: true
                                @Label: Take_Point3
                                @End
                        */
@@ -116,6 +117,7 @@ void push(Deque *q, int x) {
        @End
 */
 int steal(Deque *q) {
+       //FIXME: weaken the following acquire causes no spec problem
        size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
        atomic_thread_fence(memory_order_seq_cst);
        size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
@@ -143,7 +145,7 @@ int steal(Deque *q) {
                /**
                        @Begin
                        @Commit_point_define_check: !succ
-                       @Label: Steal_Point4
+                       @Label: Steal_Point2
                        @End
                */
 

diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h
index 5861eb036b7ce527eed596593e8a71bca6dea4e7..6bb4698fee6480f95152f51e53bd8617c2176cdd 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.h
+++ b/benchmark/chase-lev-deque-bugfix/deque.h
@@ -70,9 +70,11 @@ void resize(Deque *q);
     @ID: __RET__ == EMPTY ? DEFAULT_CALL_ID : get_id(back(__deque))
     @Action:
         int _Old_Val = EMPTY;
-               if (size(__deque) > 0) {
-                       _Old_Val = get_data(back(__deque));
-               pop_back(__deque);
+               if (__RET__ != EMPTY) {
+                       if (size(__deque) > 0) {
+                               _Old_Val = get_data(back(__deque));
+                       pop_back(__deque);
+                       }       
                }
     @Post_check:
         _Old_Val == __RET__
@@ -95,16 +97,18 @@ void push(Deque *q, int x);
 /**
     @Begin
     @Interface: Steal 
-    @Commit_point_set: Steal_Point1 | Steal_Point2
+    @Commit_point_set: Steal_Point1 | Steal_Point2 | Steal_Point3
     @ID: (__RET__ == EMPTY || __RET__ == ABORT) ? DEFAULT_CALL_ID : get_id(front(__deque))
     @Action:
         int _Old_Val = EMPTY;
-               if (size(__deque) > 0) {
-                       _Old_Val = get_data(front(__deque));
-               pop_front(__deque);
+               if (__RET__ != EMPTY && __RET__ != ABORT) {
+                       if (size(__deque) > 0) {
+                               _Old_Val = get_data(front(__deque));
+                               pop_front(__deque);
+                       }
                }
     @Post_check:
-        _Old_Val == __RET__
+        _Old_Val == __RET__ || __RET__ == EMPTY || __RET__ == ABORT
     @End
 */
 int steal(Deque *q);

diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h
index 536f1c42304ffc470c1b0547686a8f19c94f4774..738201cea156b98161bbc5b4d389b1f59553e359 100644 (file)
--- a/benchmark/cliffc-hashtable/cliffc_hashtable.h
+++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h
@@ -391,9 +391,12 @@ friend class CHM;
                // For other CHM in kvs_data, they should be initialzed in resize()
                // because the size is determined dynamically
                kvs_data *kvs = new kvs_data(Default_Init_Size);
+               
+               /*
                void *chm = (void*) new CHM(0);
                kvs->_data[0].store(chm, memory_order_relaxed);
                _kvs.store(kvs, memory_order_release);
+               */
        }
 
        cliffc_hashtable(int init_size) {

diff --git a/benchmark/cliffc-hashtable/main.cc b/benchmark/cliffc-hashtable/main.cc
index cecaa0cb81524307dc88fe34761ded6b9b2465f7..517e4a7b895bb81fa193ca4ea685ccd4fbd668f2 100644 (file)
--- a/benchmark/cliffc-hashtable/main.cc
+++ b/benchmark/cliffc-hashtable/main.cc
@@ -53,6 +53,7 @@ cliffc_hashtable<IntWrapper, IntWrapper> *table;
 IntWrapper *val1, *val2;
 
 void threadA(void *arg) {
+       /*
        IntWrapper *k1 = new IntWrapper(3), *k2 = new IntWrapper(5),
                *k3 = new IntWrapper(1024), *k4 = new IntWrapper(1025);
        IntWrapper *v1 = new IntWrapper(1024), *v2 = new IntWrapper(1025),
@@ -61,52 +62,51 @@ void threadA(void *arg) {
        table->put(k2, v2);
        val1 = table->get(k3);
        table->put(k3, v3);
+       */
 }
 
 void threadB(void *arg) {
+       /*
        IntWrapper *k1 = new IntWrapper(3), *k2 = new IntWrapper(5),
                *k3 = new IntWrapper(1024), *k4 = new IntWrapper(1025);
        IntWrapper *v1 = new IntWrapper(1024), *v2 = new IntWrapper(1025),
                *v3 = new IntWrapper(73), *v4 = new IntWrapper(81);
        table->put(k1, v3);
+       val1 = table->get(k2);
        table->put(k2, v4);
        val1 = table->get(k2);
-}
-
-void threadC(void *arg) {
-       IntWrapper *k1 = new IntWrapper(3), *k2 = new IntWrapper(5),
-               *k3 = new IntWrapper(1024), *k4 = new IntWrapper(1025);
-       IntWrapper *v1 = new IntWrapper(1024), *v2 = new IntWrapper(1025),
-               *v3 = new IntWrapper(73), *v4 = new IntWrapper(81);
-       table->put(k1, v1);
-       table->put(k2, v2);
-       val2 = table->get(k1);
+       */
 }
 
 void threadMain(void *arg) {
-       for (int i = 200; i < 300; i++) {
+       /*
+       for (int i = 0; i < 5; i++) {
                IntWrapper *k = new IntWrapper(i), *v = new IntWrapper(i * 2);
                table->put(k, v);
        }
+       */
+       IntWrapper *k1 = new IntWrapper(3), *k2 = new IntWrapper(5),
+               *k3 = new IntWrapper(1024), *k4 = new IntWrapper(1025);
+       IntWrapper *v1 = new IntWrapper(1024), *v2 = new IntWrapper(1025),
+               *v3 = new IntWrapper(73), *v4 = new IntWrapper(81);
+       table->put(k1, v3);
+       val1 = table->get(k2);
 }
 
 int user_main(int argc, char *argv[]) {
-       thrd_t t1, t2, t3, t4;
+       thrd_t t1, t2;
        table = new cliffc_hashtable<IntWrapper, IntWrapper>();
        val1 = NULL;
        val2 = NULL;
-       threadMain(NULL);
+       //threadMain(NULL);
 
        thrd_create(&t1, threadA, NULL);
        thrd_create(&t2, threadB, NULL);
-       //thrd_create(&t3, threadC, NULL);
-       //thrd_create(&t4, threadD, NULL);
+       threadMain(NULL);
 
        thrd_join(t1);
        thrd_join(t2);
-       //thrd_join(t3);
-       //thrd_join(t4);
-       
+       /*
        if (val1 == NULL) {
                cout << "val1: NULL" << endl;
        } else {
@@ -118,6 +118,7 @@ int user_main(int argc, char *argv[]) {
        } else {
                cout << val2->get() << endl;
        }
+       */
        return 0;
 }
 

diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h
index e08a0e73c1a844736daa0196e94a3dea4c3f182e..27db46981f3d165823ce3a3372cc6ecc1a7e0e96 100644 (file)
--- a/benchmark/mcs-lock/mcs-lock.h
+++ b/benchmark/mcs-lock/mcs-lock.h
@@ -83,6 +83,7 @@ public:
 
                // publish my node as the new tail :
                mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
+               // FIXME: Only weakening the mo_acq_rel cause the spec error
                /**
                        @Begin
                        @Commit_point_define_check: pred == NULL
@@ -136,6 +137,7 @@ public:
                        bool success;
                        success = m_tail.compare_exchange_strong(
                                tail_was_me,NULL,std::mo_acq_rel);
+                       // FIXME: Only weakening the mo_acq_rel cause the spec error
                        /**
                                @Begin
                                @Commit_point_define_check: success == true

diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h
index 5d20f3067f4674dde6b5dc936bdbd41e7c45eedf..823603fe4a566abd1aa1d6bdf5fe40b881770729 100644 (file)
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -101,16 +101,17 @@ public:
 
                // (*1)
                rl::backoff bo;
+               
                while ( true ) {
-                       unsigned int tmp = m_written.load(mo_acquire);
-                       /**
-                               @Begin
-                               @Commit_point_define_check: (tmp & 0xFFFF) == wr
-                               @Label: Fetch_Succ_Point
-                               @End
-                       */
-                       if ((tmp & 0xFFFF) == wr)
+                       if ((m_written.load(mo_acquire) & 0xFFFF) == wr) {
+                               /**
+                                       @Begin
+                                       @Commit_point_define_check: true 
+                                       @Label: Fetch_Succ_Point
+                                       @End
+                               */
                                break;
+                       }
                        thrd_yield();
                }
 

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index 44ce9862bd7cc713fd0fdbc60f9b57be7f26e416..cc512d6c3b000d9fb5cfa73dda01af24a9a1b2c8 100644 (file)
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -53,7 +53,7 @@ atomic<Data*> data;
 
        @Happens_before:
                Write -> Read
-               //Write -> Write
+               Write -> Write
        @End
 */
 
@@ -107,7 +107,7 @@ Data* write(int d1, int d2, int d3) {
            tmp->data2 = prev->data2 + d2;
            tmp->data3 = prev->data3 + d3;
         succ = data.compare_exchange_strong(prev, tmp,
-            memory_order_release, memory_order_acquire);
+            memory_order_acq_rel, memory_order_acquire);
                /**
                        @Begin
                        @Commit_point_define_check: succ
@@ -149,7 +149,7 @@ int user_main(int argc, char **argv) {
        dataInit->data2 = 0;
        dataInit->data3 = 0;
        atomic_init(&data, dataInit);
-       //write(0, 0, 0);
+       write(0, 0, 0);
 
        thrd_create(&t1, threadA, NULL);
        thrd_create(&t2, threadB, NULL);