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 b8189c930e8dc3e224ced2c2cfe266d886829f27..ae33b7d3c7db50486158c19bfc7441b6d0018b93 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -111,7 +111,7 @@ void enqueue(queue_t *q, unsigned int val)
                        @Label: Enqueue_Clear
                        @End
                */
-               /**** detected UL ****/
+               /**** UL & inadmissible ****/
                tail = atomic_load_explicit(&q->tail, acquire);
                /****FIXME: miss ****/
                next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
@@ -123,7 +123,7 @@ void enqueue(queue_t *q, unsigned int val)
 
                        if (get_ptr(next) == 0) { // == NULL
                                pointer value = MAKE_POINTER(node, get_count(next) + 1);
-                               /**** detected UL ****/
+                               /**** SPEC Error (testcase1.c) ****/
                                // Second release can be just relaxed
                                success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
                                                &next, value, release, relaxed);
@@ -136,7 +136,7 @@ void enqueue(queue_t *q, unsigned int val)
                        }
                        if (!success) {
                                // This routine helps the other enqueue to update the tail
-                               /**** detected UL ****/
+                               /**** UL & Inadmissible ****/
                                unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
                                pointer value = MAKE_POINTER(ptr,
                                                get_count(tail) + 1);
@@ -153,7 +153,7 @@ void enqueue(queue_t *q, unsigned int val)
                        }
                }
        }
-       /**** dectected UL ****/
+       /**** UL & Inadmissible ****/
        // Second release can be just relaxed
        bool succ = atomic_compare_exchange_strong_explicit(&q->tail,
                        &tail,
@@ -181,7 +181,7 @@ bool dequeue(queue_t *q, int *retVal)
                        @Label: Dequeue_Clear
                        @End
                */
-               /**** detected correctness error ****/
+               /**** Inadmissible ****/
                head = atomic_load_explicit(&q->head, acquire);
                /**
                        @Begin
@@ -194,10 +194,11 @@ bool dequeue(queue_t *q, int *retVal)
                 * relaxed (it introduces a bug when there's two dequeuers and one
                 * enqueuer) correctness bug!!
                 */
+               /**** New bug ****/
                tail = atomic_load_explicit(&q->tail, acquire);
 
-               /**** Detected UL/DR (testcase1.c) ****/
-               next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
+               /**** SPEC Error (testcase1.c) ****/
+               next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, relaxed);
                /**
                        @Begin
                        @Potential_commit_point_define: true
@@ -213,7 +214,7 @@ bool dequeue(queue_t *q, int *retVal)
                                if (get_ptr(next) == 0) { // NULL       
                                        return false; // NULL
                                }
-                               /**** Detected UL (testcase1.c) ****/
+                               /**** FIXME: miss ****/
                                // Second release can be just relaxed
                                bool succ = false;
                                succ = atomic_compare_exchange_strong_explicit(&q->tail,
@@ -228,7 +229,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;
-                               /**** correctness error ****/
+                               /**** inadmissibility ****/
                                success = atomic_compare_exchange_strong_explicit(&q->head,
                                                &head,
                                                MAKE_POINTER(get_ptr(next), get_count(head) + 1),