changes to ms-queue spec

[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 50787854561c46a787dfcd0a516b4596693d5591..1d9e924538d16bd9dc192846b1785b38d7811907 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -101,8 +101,20 @@ 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
+               */
                /**** 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");
@@ -119,8 +131,8 @@ void enqueue(queue_t *q, unsigned int val)
                                                &next, value, release, relaxed);
                                /**
                                        @Begin
-                                       @Commit_point_define_check: success == true
-                                       @Label: Enqueue_Success_Point
+                                       @Commit_point_define_check: success
+                                       @Label: Enqueue_UpdateNext
                                        @End
                                */
                        }
@@ -145,10 +157,16 @@ void enqueue(queue_t *q, unsigned int val)
        }
        /**** dectected UL ****/
        // Second release can be just relaxed
-       atomic_compare_exchange_strong_explicit(&q->tail,
+       bool succ = atomic_compare_exchange_strong_explicit(&q->tail,
                        &tail,
                        MAKE_POINTER(node, get_count(tail) + 1),
                        release, relaxed);
+       /**
+               @Begin
+               @Commit_point_define_check: succ 
+               @Label: Enqueue_UpdateOrLoad_Tail
+               @End
+       */
 }
 
 /**
@@ -156,7 +174,7 @@ void enqueue(queue_t *q, unsigned int val)
        @Interface_define: Dequeue
        @End
 */
-bool dequeue(queue_t *q, unsigned int *retVal)
+bool dequeue(queue_t *q, int *output)
 {
        unsigned int value;
        int success = 0;
@@ -165,14 +183,37 @@ bool dequeue(queue_t *q, unsigned int *retVal)
        pointer next;
 
        while (!success) {
+               /**
+                       @Begin
+                       @Commit_point_clear: true
+                       @Label: Dequeue_Clear
+                       @End
+               */
                /**** detected correctness error ****/
                head = atomic_load_explicit(&q->head, acquire);
-               // FIXME: This must be acquire otherwise we have a bug with 1 enqueue &
-               // 1 dequeue
+               /**
+                       @Begin
+                       @Commit_point_define_check: true
+                       @Label: Dequeue_Read_Head
+                       @End
+               */
                tail = atomic_load_explicit(&q->tail, relaxed);
+               /**
+                       @Begin
+                       @Potential_commit_point_define: true
+                       @Label: Dequeue_Potential_Read_Tail
+                       @End
+               */
+
                /****FIXME: miss ****/
                next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
-               //printf("miss3_dequeue\n");
+               /**
+                       @Begin
+                       @Potential_commit_point_define: true 
+                       @Label: Dequeue_Potential_LoadNext
+                       @End
+               */
+               
                if (atomic_load_explicit(&q->head, relaxed) == head) {
                        if (get_ptr(head) == get_ptr(tail)) {
 
@@ -182,8 +223,9 @@ bool dequeue(queue_t *q, unsigned int *retVal)
                                if (get_ptr(next) == 0) { // NULL
                                        /**
                                                @Begin
-                                               @Commit_point_define_check: true
-                                               @Label: Dequeue_Empty_Point
+                                               @Commit_point_define: true
+                                               @Potential_commit_point_label: Dequeue_Potential_Read_Tail
+                                               @Label: Dequeue_Read_Tail
                                                @End
                                        */
                                        return false; // NULL
@@ -201,25 +243,26 @@ bool dequeue(queue_t *q, unsigned int *retVal)
                                //printf("miss4_dequeue\n");
                                thrd_yield();
                        } else {
-                               *retVal = load_32(&q->nodes[get_ptr(next)].value);
+                               /**
+                                       @Begin
+                                       @Commit_point_define: true
+                                       @Potential_commit_point_label: Dequeue_Potential_LoadNext
+                                       @Label: Dequeue_LoadNext
+                                       @End
+                               */
+                               value = load_32(&q->nodes[get_ptr(next)].value);
                                //value = q->nodes[get_ptr(next)].value;
                                /****FIXME: correctness error ****/
-                               // Seconde release can be just relaxed
                                success = atomic_compare_exchange_strong_explicit(&q->head,
                                                &head,
                                                MAKE_POINTER(get_ptr(next), get_count(head) + 1),
                                                release, relaxed);
-                               /**
-                                       @Begin
-                                       @Commit_point_define_check: success == true
-                                       @Label: Dequeue_Success_Point
-                                       @End
-                               */
                                if (!success)
                                        thrd_yield();
                        }
                }
        }
        reclaim(get_ptr(head));
+       *output = value;
        return true;
 }