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 a4fcbdb3b002fed7d2662294adb01911a9c25667..9cd2f8e9fea9bd87117cc6d9c00e4691caa662a8 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -112,12 +112,6 @@ void enqueue(queue_t *q, unsigned int val)
                */
                /**** detected UL ****/
                tail = atomic_load_explicit(&q->tail, acquire);
-               /**
-                       @Begin
-                       @Commit_point_define_check: true
-                       @Label: Enqueue_Read_Tail
-                       @End
-               */
                /****FIXME: miss ****/
                next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
                //printf("miss1_enqueue\n");
@@ -135,7 +129,7 @@ void enqueue(queue_t *q, unsigned int val)
                                /**
                                        @Begin
                                        @Commit_point_define_check: success
-                                       @Label: Enqueue_UpdateNext
+                                       @Label: Enqueue_Update_Next
                                        @End
                                */
                        }
@@ -166,8 +160,8 @@ void enqueue(queue_t *q, unsigned int val)
                        release, relaxed);
        /**
                @Begin
-               @Additional_ordering_point_define_check: true
-               @Label: Enqueue_Additional_Tail_LoadOrCAS
+               @Commit_point_define_check: true
+               @Label: Enqueue_Update_Tail
                @End
        */
 
@@ -217,25 +211,17 @@ bool dequeue(queue_t *q, int *retVal)
                next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
                /**
                        @Begin
-                       @Potential_commit_point_define: true 
-                       @Label: Dequeue_Potential_LoadNext
+                       @Potential_commit_point_define: true
+                       @Label: Dequeue_Potential_Read_Next
                        @End
                */
-               
                if (atomic_load_explicit(&q->head, relaxed) == head) {
                        if (get_ptr(head) == get_ptr(tail)) {
 
                                /* Check for uninitialized 'next' */
                                //MODEL_ASSERT(get_ptr(next) != POISON_IDX);
 
-                               if (get_ptr(next) == 0) { // NULL
-                                       /**
-                                               @Begin
-                                               @Commit_point_define: true
-                                               @Potential_commit_point_label: Dequeue_Potential_Read_Tail
-                                               @Label: Dequeue_Read_Tail
-                                               @End
-                                       */
+                               if (get_ptr(next) == 0) { // NULL       
                                        return false; // NULL
                                }
                                /**** Detected UL (testcase1.c) ****/
@@ -261,8 +247,8 @@ bool dequeue(queue_t *q, int *retVal)
                                /**
                                        @Begin
                                        @Commit_point_define: success
-                                       @Potential_commit_point_label: Dequeue_Potential_LoadNext
-                                       @Label: Dequeue_LoadNext
+                                       @Potential_commit_point_label: Dequeue_Potential_Read_Next
+                                       @Label: Dequeue_Read_Next
                                        @End
                                */
                                if (!success)