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 9cd2f8e9fea9bd87117cc6d9c00e4691caa662a8..d5e889db0113c288d23d9703b813f8a708f9ee1f 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -22,11 +22,11 @@ static unsigned int new_node()
        int i;
        int t = get_thread_num();
        for (i = 0; i < MAX_FREELIST; i++) {
-               unsigned int node = load_32(&free_lists[t][i]);
-               //unsigned int node = free_lists[t][i];
+               //unsigned int node = load_32(&free_lists[t][i]);
+               unsigned int node = free_lists[t][i];
                if (node) {
-                       store_32(&free_lists[t][i], 0);
-                       //free_lists[t][i] = 0;
+                       //store_32(&free_lists[t][i], 0);
+                       free_lists[t][i] = 0;
                        return node;
                }
        }
@@ -46,8 +46,8 @@ static void reclaim(unsigned int node)
 
        for (i = 0; i < MAX_FREELIST; i++) {
                /* Should never race with our own thread here */
-               unsigned int idx = load_32(&free_lists[t][i]);
-               //unsigned int idx = free_lists[t][i];
+               //unsigned int idx = load_32(&free_lists[t][i]);
+               unsigned int idx = free_lists[t][i];
 
                /* Found empty spot in free list */
                if (idx == 0) {
@@ -97,20 +97,21 @@ void enqueue(queue_t *q, unsigned int val)
        pointer tmp;
 
        node = new_node();
-       store_32(&q->nodes[node].value, val);
-       //q->nodes[node].value = val;
+       //store_32(&q->nodes[node].value, val);
+       q->nodes[node].value = val;
        tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
        set_ptr(&tmp, 0); // NULL
        atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
 
        while (!success) {
+               
                /**
                        @Begin
                        @Commit_point_clear: true
                        @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);
@@ -122,20 +123,20 @@ 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);
                                /**
                                        @Begin
                                        @Commit_point_define_check: success
-                                       @Label: Enqueue_Update_Next
+                                       @Label: EnqueueUpdateNext
                                        @End
                                */
                        }
                        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);
@@ -152,19 +153,12 @@ 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,
                        MAKE_POINTER(node, get_count(tail) + 1),
                        release, relaxed);
-       /**
-               @Begin
-               @Commit_point_define_check: true
-               @Label: Enqueue_Update_Tail
-               @End
-       */
-
 }
 
 /**
@@ -187,32 +181,28 @@ bool dequeue(queue_t *q, int *retVal)
                        @Label: Dequeue_Clear
                        @End
                */
-               /**** detected correctness error ****/
+               /**** Inadmissible ****/
                head = atomic_load_explicit(&q->head, acquire);
                /**
                        @Begin
                        @Commit_point_define_check: true
-                       @Label: Dequeue_Read_Head
+                       @Label: DequeueReadHead
                        @End
                */
+
                /** 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) correctness bug!!
                 */
+               /**** New bug ****/
                tail = atomic_load_explicit(&q->tail, acquire);
-               /**
-                       @Begin
-                       @Potential_commit_point_define: true
-                       @Label: Dequeue_Potential_Read_Tail
-                       @End
-               */
 
-               /**** Detected UL/DR (testcase1.c) ****/
+               /**** SPEC Error (testcase1.c) ****/
                next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
                /**
                        @Begin
                        @Potential_commit_point_define: true
-                       @Label: Dequeue_Potential_Read_Next
+                       @Label: DequeueReadNext
                        @End
                */
                if (atomic_load_explicit(&q->head, relaxed) == head) {
@@ -224,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,
@@ -237,18 +227,25 @@ bool dequeue(queue_t *q, int *retVal)
                                //printf("miss4_dequeue\n");
                                thrd_yield();
                        } else {
-                               value = load_32(&q->nodes[get_ptr(next)].value);
-                               //value = q->nodes[get_ptr(next)].value;
-                               /**** correctness error ****/
+                               //value = load_32(&q->nodes[get_ptr(next)].value);
+                               value = q->nodes[get_ptr(next)].value;
+                               /**** inadmissibility ****/
                                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_Read_Next
-                                       @Label: Dequeue_Read_Next
+                                       @Potential_commit_point_label: DequeueReadNext
+                                       @Label: DequeueReadNextVerify
                                        @End
                                */
                                if (!success)