update the benchmarks (RCU)

diff --git a/mcs-lock/mcs-lock.cc b/mcs-lock/mcs-lock.cc
index 525ef9b07a947c9fe7ccf39b4586576bff204cd9..e36ca0efdb6741ec5d57e41e5b89db55f5db5312 100644 (file)
--- a/mcs-lock/mcs-lock.cc
+++ b/mcs-lock/mcs-lock.cc
@@ -77,6 +77,7 @@ void mcs_mutex::unlock(guard * I) {
         // "memory_order_relaxed", run "make" to recompile, and then run:
         // "./run.sh ./mcs-lock/testcase -m2 -Y -u3 -tSPEC"
         /**********  Detected Correctness **********/
+        // This was mo_acq_rel, which is stronger than necessary
                if ( m_tail.compare_exchange_strong(
                        tail_was_me,NULL,std::mo_release) ) {
                        // got null in tail, mutex is unlocked

diff --git a/read-copy-update/rcu.cc b/read-copy-update/rcu.cc
index 8c6a956dd18f5d6e4e90ba8c96edce9b0ce600ca..c4ddb3ed7c7c6fd85b200e71d822c97205b4ab66 100644 (file)
--- a/read-copy-update/rcu.cc
+++ b/read-copy-update/rcu.cc
@@ -15,17 +15,17 @@ void read(int *data1, int *data2) {
     // XXX-injection-#1: Weaken the parameter "memory_order_acquire" to
     // "memory_order_relaxed", run "make" to recompile, and then run:
     // "./run.sh ./read-copy-update/testcase -m2 -y -u3 -tSPEC"
-       /**********    Detected Correctness **********/
+       /**********    Detected UL **********/
        Data *res = dataPtr.load(memory_order_acquire);
        /** @OPDefine: true */
-       *data1 = res->data1;
-       *data2 = res->data2;
+       *data1 = res->data1.load(memory_order_relaxed);
+       *data2 = res->data2.load(memory_order_relaxed);
        //load_32(&res->data1);
 }
 
 static void inc(Data *newPtr, Data *prev, int d1, int d2) {
-       newPtr->data1 = prev->data1 + d1;
-       newPtr->data2 = prev->data2 + d2;
+       newPtr->data1.store(prev->data1.load(memory_order_relaxed) + d1, memory_order_relaxed);
+       newPtr->data2.store(prev->data2.load(memory_order_relaxed) + d2, memory_order_relaxed);
 }
 
 /** @Transition: STATE(data1) += data1;
@@ -37,14 +37,14 @@ void write(int data1, int data2) {
         // XXX-injection-#2: Weaken the parameter "memory_order_acquire" to
         // "memory_order_relaxed", run "make" to recompile, and then run:
         // "./run.sh ./read-copy-update/testcase -m2 -y -u3 -tSPEC"
-               /**********    Detected Correctness **********/
+               /**********    Detected UL **********/
                Data *prev = dataPtr.load(memory_order_acquire);
                inc(tmp, prev, data1, data2);
 
         // XXX-injection-#3: Weaken the parameter "memory_order_release" to
         // "memory_order_relaxed", run "make" to recompile, and then run:
         // "./run.sh ./read-copy-update/testcase -m2 -y -u3 -tSPEC"
-               /**********    Detected Correctness **********/
+               /**********    Detected UL **********/
                succ = dataPtr.compare_exchange_strong(prev, tmp,
             memory_order_release, memory_order_relaxed);
                /** @OPClearDefine: succ */

diff --git a/read-copy-update/rcu.h b/read-copy-update/rcu.h
index f40edf4f9fa44db2c321196d177cfb772ee56ca3..5455828eec29dab0cfa3ff1d6f7996d8170f35a4 100644 (file)
--- a/read-copy-update/rcu.h
+++ b/read-copy-update/rcu.h
@@ -11,8 +11,8 @@
 
 struct Data {
        /** Declare atomic just to expose them to CDSChecker */
-       int data1;
-       int data2;
+       atomic_int data1;
+       atomic_int data2;
 };