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 f59d77736a13ec6b4d343772a6a0117c921123bf..145c91d30dcd8723ceb5da0c57918ee3a711d097 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -104,6 +104,7 @@ void enqueue(queue_t *q, unsigned int val)
        atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
 
        while (!success) {
+               
                /**
                        @Begin
                        @Commit_point_clear: true
@@ -112,12 +113,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 +130,7 @@ void enqueue(queue_t *q, unsigned int val)
                                /**
                                        @Begin
                                        @Commit_point_define_check: success
-                                       @Label: Enqueue_UpdateNext
+                                       @Label: EnqueueUpdateNext
                                        @End
                                */
                        }
@@ -188,50 +183,30 @@ bool dequeue(queue_t *q, int *retVal)
                */
                /**** detected correctness error ****/
                head = atomic_load_explicit(&q->head, acquire);
-               /**
-                       @Begin
-                       @Commit_point_define_check: true
-                       @Label: Dequeue_Read_Head
-                       @End
-               */
-               /** FIXME: A new bug has been found here!!! It should be acquire instead of
+               /** A new bug has been found here!!! It should be acquire instead of
                 * relaxed (it introduces a bug when there's two dequeuers and one
-                * enqueuer)
+                * enqueuer) correctness bug!!
                 */
-               tail = atomic_load_explicit(&q->tail, relaxed);
-               /**
-                       @Begin
-                       @Potential_commit_point_define: true
-                       @Label: Dequeue_Potential_Read_Tail
-                       @End
-               */
+               tail = atomic_load_explicit(&q->tail, acquire);
 
-               /****FIXME: miss ****/
+               /**** Detected UL/DR (testcase1.c) ****/
                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: DequeueReadNext
                        @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
                                }
-                               /****FIXME: miss (not reached) ****/
+                               /**** Detected UL (testcase1.c) ****/
                                // Second release can be just relaxed
                                bool succ = false;
                                succ = atomic_compare_exchange_strong_explicit(&q->tail,
@@ -246,16 +221,23 @@ bool dequeue(queue_t *q, int *retVal)
                        } else {
                                value = load_32(&q->nodes[get_ptr(next)].value);
                                //value = q->nodes[get_ptr(next)].value;
-                               /****FIXME: correctness error ****/
+                               /**** correctness error ****/
                                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
+                                       @Label: DequeueUpdateHead
+                                       @End
+                               */
+
                                /**
                                        @Begin
                                        @Commit_point_define: success
-                                       @Potential_commit_point_label: Dequeue_Potential_LoadNext
-                                       @Label: Dequeue_LoadNext
+                                       @Potential_commit_point_label: DequeueReadNext
+                                       @Label: DequeueReadNextVerify
                                        @End
                                */
                                if (!success)