X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=benchmark%2Fchase-lev-deque-bugfix%2Fdeque.c;fp=benchmark%2Fchase-lev-deque-bugfix%2Fdeque.c;h=ff28527a1ec2569bdfcf78884af698ff6e682937;hp=9c6625e7a88bfe904054ba0299f5bf12a188c117;hb=d061668cac2e5a74a40dace627b63ec74187f98e;hpb=fb52175d1e1ebe5f73f6b4b0513b6302d3c03031 diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c index 9c6625e..ff28527 100644 --- a/benchmark/chase-lev-deque-bugfix/deque.c +++ b/benchmark/chase-lev-deque-bugfix/deque.c @@ -26,12 +26,6 @@ Deque * create() { */ int take(Deque *q) { size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1; - /** - @Begin - @Commit_point_define_check: true - @Label: TakeReadBottom - @End - */ Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); atomic_store_explicit(&q->bottom, b, memory_order_relaxed); /**** SPEC (sequential) (testcase1.c) ****/ @@ -39,13 +33,6 @@ int take(Deque *q) { size_t t = atomic_load_explicit(&q->top, memory_order_relaxed); int x; if (t <= b) { - /** - @Begin - @Commit_point_clear: true - @Label: TakeClear1 - @End - */ - /* Non-empty queue. */ int size = atomic_load_explicit(&a->size,memory_order_relaxed); x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed); @@ -61,20 +48,6 @@ int take(Deque *q) { bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed); if (!succ) { - /** - @Begin - @Commit_point_clear: true - @Label: TakeClear2 - @End - */ - - /** - @Begin - @Commit_point_define_check: true - @Label: TakeReadTop - @End - */ - /* Failed race. */ x = EMPTY; } @@ -131,12 +104,8 @@ void push(Deque *q, int x) { int size = atomic_load_explicit(&a->size, memory_order_relaxed); atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed); - /** - @Begin - @Commit_point_define_check: true - @Label: PushUpdateBuffer - @End - */ + /** @OPDefine: true */ + /**** UL & 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);