edits

[cdsspec-compiler.git] / benchmark / ms-queue / my_queue.c

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();
                        }