minor fix

[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 6a2737f91825a9bdcee355027f6baad9135ea826..232e5d839347794a2056a5c0de5c7e17c6d50811 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -78,41 +78,7 @@ void init_queue(queue_t *q, int num_threads)
 
 /**
        @Begin
-       @Global_define:
-               @DeclareVar:
-               typedef struct tag_elem {
-                       Tag id;
-                       unsigned int data;
-                       
-                       tag_elem(Tag _id, unsigned int _data) {
-                               id = _id;
-                               data = _data;
-                       }
-               } tag_elem_t;
-
-               spec_queue<tag_elem_t> queue;
-               Tag tag;
-               @InitVar:
-                       queue = spec_queue<tag_elem_t>();
-                       tag = Tag();
-       @Happens_before:
-               # Only check the happens-before relationship according to the id of the
-               # commit_point_set. For commit_point_set that has same ID, A -> B means
-               # B happens after the previous A.
-               Enqueue -> Dequeue
-       @End
-*/
-
-/**
-       @Begin
-       @Interface: Enqueue
-       @Commit_point_set: Enqueue_Success_Point
-       @ID: __sequential.tag.getCurAndInc()
-       @Action:
-               # __ID__ is an internal macro that refers to the id of the current
-               # interface call
-               @Code:
-               __sequential.queue.enqueue(tag_elem_t(__ID__, val));
+       @Interface_define: Enqueue
        @End
 */
 void enqueue(queue_t *q, unsigned int val)
@@ -141,20 +107,19 @@ void enqueue(queue_t *q, unsigned int val)
                                pointer value = MAKE_POINTER(node, get_count(next) + 1);
                                success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
                                                &next, value, release, release);
+                               /**
+                                       @Begin
+                                       @Commit_point_define_check: success == true
+                                       @Label: Enqueue_Success_Point
+                                       @End
+                               */
                        }
                        if (!success) {
                                unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
                                pointer value = MAKE_POINTER(ptr,
                                                get_count(tail) + 1);
-                               int commit_success = 0;
-                               commit_success = atomic_compare_exchange_strong_explicit(&q->tail,
+                               atomic_compare_exchange_strong_explicit(&q->tail,
                                                &tail, value, release, release);
-                               /**
-                                       @Begin
-                                       @Commit_point_define_check: __ATOMIC_RET__ == true
-                                       @Label: Enqueue_Success_Point
-                                       @End
-                               */
                                thrd_yield();
                        }
                }
@@ -167,14 +132,7 @@ void enqueue(queue_t *q, unsigned int val)
 
 /**
        @Begin
-       @Interface: Dequeue
-       @Commit_point_set: Dequeue_Success_Point
-       @ID: __sequential.queue.peak().tag
-       @Action:
-               @Code:
-               unsigned int _Old_Val = __sequential.queue.dequeue().data;
-       @Post_check:
-               _Old_Val == __RET__
+       @Interface_define: Dequeue
        @End
 */
 unsigned int dequeue(queue_t *q)
@@ -196,6 +154,12 @@ unsigned int dequeue(queue_t *q)
                                MODEL_ASSERT(get_ptr(next) != POISON_IDX);
 
                                if (get_ptr(next) == 0) { // NULL
+                                       /**
+                                               @Begin
+                                               @Commit_point_define_check: true
+                                               @Label: Dequeue_Empty_Point
+                                               @End
+                                       */
                                        return 0; // NULL
                                }
                                atomic_compare_exchange_strong_explicit(&q->tail,
@@ -211,7 +175,7 @@ unsigned int dequeue(queue_t *q)
                                                release, release);
                                /**
                                        @Begin
-                                       @Commit_point_define_check: __ATOMIC_RET__ == true
+                                       @Commit_point_define_check: success == true
                                        @Label: Dequeue_Success_Point
                                        @End
                                */