unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
pointer value = MAKE_POINTER(ptr,
get_count(tail) + 1);
- /****FIXME: miss ****/
+ /**** SPEC (sequential, testcase2.c) ****/
// Second release can be just relaxed
bool succ = false;
succ = atomic_compare_exchange_strong_explicit(&q->tail,
- &tail, value, release, relaxed);
+ &tail, value, relaxed, relaxed);
if (succ) {
//printf("miss2_enqueue CAS succ\n");
}
* relaxed (it introduces a bug when there's two dequeuers and one
* enqueuer) correctness bug!!
*/
+ /**** SPEC (sequential) (testcase1.c) ****/
/**** New bug ****/
tail = atomic_load_explicit(&q->tail, acquire);
if (get_ptr(next) == 0) { // NULL
return false; // NULL
}
- /**** FIXME: miss ****/
+ /**** SPEC (sequential testcase3.c) ****/
// Second release can be just relaxed
bool succ = false;
succ = atomic_compare_exchange_strong_explicit(&q->tail,
&tail,
MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
- release, relaxed);
+ release, relaxed);
if (succ) {
//printf("miss4_dequeue CAS succ\n");
}