From: Peizhao Ou <peizhaoo@uci.edu>
Date: Wed, 7 Dec 2016 23:58:50 +0000 (-0800)
Subject: update the benchmarks (RCU)
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=0cc6fde1f77ecd54e5faae3a301dad02091f6b97;p=model-checker-benchmarks.git

update the benchmarks (RCU)
---

diff --git a/mcs-lock/mcs-lock.cc b/mcs-lock/mcs-lock.cc
index 525ef9b..e36ca0e 100644
--- 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 8c6a956..c4ddb3e 100644
--- 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 f40edf4..5455828 100644
--- 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;
 };