X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=read-copy-update%2Frcu.cc;h=8c6a956dd18f5d6e4e90ba8c96edce9b0ce600ca;hb=fd62fd9d7f0bb39d19155db6af758c44e3dbb43b;hp=52a82db028651ace056766b5aa4205564e6f3774;hpb=1e4cd56e5cf72f7cb6dddb2990183f050afc4cbc;p=model-checker-benchmarks.git

diff --git a/read-copy-update/rcu.cc b/read-copy-update/rcu.cc
index 52a82db..8c6a956 100644
--- a/read-copy-update/rcu.cc
+++ b/read-copy-update/rcu.cc
@@ -12,6 +12,9 @@ atomic<Data*> dataPtr;
 
 /** @JustifyingPrecondition: return STATE(data1) == *data1 && STATE(data2) == *data2; */
 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 **********/
 	Data *res = dataPtr.load(memory_order_acquire);
 	/** @OPDefine: true */
@@ -31,9 +34,16 @@ void write(int data1, int data2) {
 	bool succ = false;
 	Data *tmp = new Data;
 	do {
+        // 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 **********/
 		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 **********/
 		succ = dataPtr.compare_exchange_strong(prev, tmp,
             memory_order_release, memory_order_relaxed);