edits

[cdsspec-compiler.git] / benchmark / chase-lev-deque-bugfix / deque.c

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index b4f63171fde4fda413384f3f7eeae90f816fcdab..3ad32afb74700a602a70632b690148ccb86de0d3 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -158,12 +158,6 @@ int steal(Deque *q) {
        //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
-               @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);
        /**** SPEC & UL ****/
@@ -174,57 +168,22 @@ int steal(Deque *q) {
                @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);
-               /**
-                       //@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
-               */
                /**** SPEC (sequential) ****/ 
                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
-                       @Label: Steal_CAS_Top
-                       @End
-               */
-
                /**
                        @Begin
                        @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) {
                        /* Failed race. */
                        return ABORT;