@End
*/
atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
- /**** detected correctness ****/
+ /**** SPEC (sequential) (testcase1.c) ****/
atomic_thread_fence(memory_order_seq_cst);
size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
/**
*/
void push(Deque *q, int x) {
size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
- /**** detected correctness ****/
+ /**** SPEC (sequential) ****/
size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ {
resize(q);
+ // CDSSpec can actually detect the same bug if we avoid the UL error
//Bug in paper...should have next line...
- a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+ //a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
/**
//@Begin
@Commit_point_define_check: true
@Label: Push_Update_Buffer
@End
*/
- /**** detected HB error (run with -u100 to avoid the uninitialized bug) ****/
+ /**** SPEC (Sync) (run with -u100 to avoid the uninitialized bug) ****/
atomic_thread_fence(memory_order_release);
-
- atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
+ // Watch out!!! We need to specifiy the fence as the commit point because
+ // the synchronization in C11 actually is established at the fence.
/**
@Begin
@Commit_point_define_check: true
@Label: Push_Update_Bottom
@End
*/
+ atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
+
}
/**
@End
*/
int steal(Deque *q) {
- //FIXME: weaken the following acquire causes no spec problem
+ //Watch out: actually on need to be an acquire (don't count it)
+ // An old bug
size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
/**
//@Begin
*/
//FIXME: remove the fence causes no error and fewer executions..
atomic_thread_fence(memory_order_seq_cst);
- /**** detected HB error (run with -u100 to avoid the uninitialized bug) ****/
+ /**** SPEC & UL ****/
size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
/**
@Begin
@Label: Steal_Potential_Read_Buffer
@End
*/
- /**** detected correctness failure ****/
+ /**** SPEC (sequential) ****/
bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
memory_order_seq_cst, memory_order_relaxed);
/**