edits

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;

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index fdea1a4bab7148323c07d0edc6d5e5ba62d4b9ce..b2334c8511113ff5026d8df8ed387fe88305e36a 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -104,13 +104,6 @@ void enqueue(queue_t *q, unsigned int val)
        atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
 
        while (!success) {
-               
-               /**
-                       @Begin
-                       @Commit_point_clear: true
-                       @Label: Enqueue_Clear
-                       @End
-               */
                /**** UL & inadmissible ****/
                tail = atomic_load_explicit(&q->tail, acquire);
                /****FIXME: miss ****/
@@ -144,7 +137,7 @@ void enqueue(queue_t *q, unsigned int val)
                                // Second release can be just relaxed
                                bool succ = false;
                                succ = atomic_compare_exchange_strong_explicit(&q->tail,
-                                               &tail, value, relaxed, relaxed);
+                                               &tail, value, release, relaxed);
                                if (succ) {
                                        //printf("miss2_enqueue CAS succ\n");
                                }
@@ -153,7 +146,7 @@ void enqueue(queue_t *q, unsigned int val)
                        }
                }
        }
-       /**** UL & Inadmissible ****/
+       /**** UL & Inadmissible (main.c) ****/
        // Second release can be just relaxed
        bool succ = atomic_compare_exchange_strong_explicit(&q->tail,
                        &tail,
@@ -181,7 +174,8 @@ bool dequeue(queue_t *q, int *retVal)
                        @Label: Dequeue_Clear
                        @End
                */
-               /**** Inadmissible ****/
+
+               /**** Inadmissible (main.c) ****/
                head = atomic_load_explicit(&q->head, acquire);
                /**
                        @Begin
@@ -200,12 +194,6 @@ bool dequeue(queue_t *q, int *retVal)
 
                /**** SPEC Error (testcase1.c) ****/
                next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
-               /**
-                       @Begin
-                       @Potential_commit_point_define: true
-                       @Label: DequeueReadNext
-                       @End
-               */
                if (atomic_load_explicit(&q->head, relaxed) == head) {
                        if (get_ptr(head) == get_ptr(tail)) {
 
@@ -230,7 +218,7 @@ bool dequeue(queue_t *q, int *retVal)
                        } else {
                                //value = load_32(&q->nodes[get_ptr(next)].value);
                                value = q->nodes[get_ptr(next)].value;
-                               /**** inadmissibility ****/
+                               /**** inadmissibility (main.c) ****/
                                success = atomic_compare_exchange_strong_explicit(&q->head,
                                                &head,
                                                MAKE_POINTER(get_ptr(next), get_count(head) + 1),
@@ -241,14 +229,6 @@ bool dequeue(queue_t *q, int *retVal)
                                        @Label: DequeueUpdateHead
                                        @End
                                */
-
-                               /**
-                                       @Begin
-                                       @Commit_point_define: success
-                                       @Potential_commit_point_label: DequeueReadNext
-                                       @Label: DequeueReadNextVerify
-                                       @End
-                               */
                                if (!success)
                                        thrd_yield();
                        }