// "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
// 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;
// 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 */