X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=benchmark%2Fchase-lev-deque-bugfix%2Fdeque.c;h=854091ff41d9845ebbace331b04eaf0d85f70a79;hb=9811b5edc5910159c1248ca2745f83ff5edc1e0d;hp=2cfbb76a0607a9d743e8e3235fb624ad6fd975a7;hpb=010b0488385988be23280784a128f5ba778e193a;p=cdsspec-compiler.git diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c index 2cfbb76..854091f 100644 --- a/benchmark/chase-lev-deque-bugfix/deque.c +++ b/benchmark/chase-lev-deque-bugfix/deque.c @@ -22,41 +22,56 @@ 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: Take_Read_Bottom + @End + */ Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); + /** + //@Begin + @Commit_point_define_check: true + @Label: Take_Read_Array + @End + */ atomic_store_explicit(&q->bottom, b, memory_order_relaxed); + /**** detected correctness ****/ atomic_thread_fence(memory_order_seq_cst); size_t t = atomic_load_explicit(&q->top, memory_order_relaxed); /** - @Begin - @Commit_point_define_check: t > b - @Label: Take_Point_1 + //@Begin + @Commit_point_define_check: t != b + @Label: Take_Read_Top @End */ int x; if (t <= b) { /* Non-empty queue. */ - x = atomic_load_explicit(&a->buffer[b % atomic_load_explicit(&a->size,memory_order_relaxed)], memory_order_relaxed); + int size = atomic_load_explicit(&a->size,memory_order_relaxed); + x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed); /** - @Begin + //@Begin @Commit_point_define_check: t != b - @Label: Take_Point2 + @Label: Take_Read_Buffer @End */ if (t == b) { /* Single last element in queue. */ + //FIXME: weaken the following seq_cst causes no spec problem bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed); /** - @Begin - @Commit_point_define_check: succ == true - @Label: Take_Point3 + //@Begin + @Commit_point_define_check: succ + @Label: Take_CAS_Top @End */ - + /** @Begin - @Commit_point_define_check: succ == false - @Label: Take_Point4 + @Additional_ordering_point_define_check: true + @Label: Take_Additional_Point @End */ if (!succ) { @@ -84,8 +99,9 @@ void resize(Deque *q) { for(i=top; i < bottom; i++) { atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed); } + /**** detected UL ****/ atomic_store_explicit(&q->array, new_a, memory_order_release); - printf("resize\n"); + //printf("resize\n"); } /** @@ -95,22 +111,39 @@ void resize(Deque *q) { */ void push(Deque *q, int x) { size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed); + /**** detected correctness ****/ 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); //Bug in paper...should have next line... a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); + /** + //@Begin + @Commit_point_define_check: true + @Label: Push_Read_Array + @End + */ } - atomic_store_explicit(&a->buffer[b % atomic_load_explicit(&a->size, memory_order_relaxed)], x, memory_order_relaxed); + 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: Push_Update_Buffer + @End + */ + /**** detected HB error (run with -u100 to avoid the uninitialized bug) ****/ atomic_thread_fence(memory_order_release); + + atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); /** @Begin @Commit_point_define_check: true - @Label: Push_Point + @Label: Push_Update_Bottom @End */ - atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); } /** @@ -119,33 +152,73 @@ void push(Deque *q, int x) { @End */ int steal(Deque *q) { + //FIXME: weaken the following acquire causes no spec problem size_t t = atomic_load_explicit(&q->top, memory_order_acquire); + /** + //@Begin + @Potential_commit_point_define: true + @Label: Steal_Potential_Read_Tail + @End + */ + //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) ****/ size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire); /** @Begin - @Commit_point_define_check: t >= b - @Label: Steal_Point1 + @Commit_point_define_check: true + @Label: Steal_Read_Bottom + @End + */ + + /** + //@Begin + @Commit_point_define: t >= b + @Potential_commit_point_label: Steal_Potential_Read_Tail + @Label: Steal_Read_Tail @End */ int x = EMPTY; if (t < b) { /* Non-empty queue. */ + /**** detected UL ****/ Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire); - x = atomic_load_explicit(&a->buffer[t % atomic_load_explicit(&a->size, memory_order_relaxed)], memory_order_relaxed); + /** + //@Begin + @Commit_point_define_check: true + @Label: Steal_Read_Array + @End + */ + int size = atomic_load_explicit(&a->size, memory_order_relaxed); + x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed); + /** + //@Begin + @Potential_commit_point_define: true + @Label: Steal_Potential_Read_Buffer + @End + */ + /**** detected correctness failure ****/ bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed); /** - @Begin - @Commit_point_define_check: succ == true - @Label: Steal_Point2 + //@Begin + @Commit_point_define_check: succ + @Label: Steal_CAS_Top @End */ - + /** @Begin - @Commit_point_define_check: succ == false - @Label: Steal_Point3 + @Additional_ordering_point_define_check: true + @Label: Steal_Additional_Point + @End + */ + + /** + //@Begin + @Commit_point_define: succ + @Potential_commit_point_label: Steal_Potential_Read_Buffer + @Label: Steal_Read_Buffer @End */ if (!succ) {