changes to ms-queue spec
[cdsspec-compiler.git] / benchmark / ms-queue / my_queue.c
index c70adac..1d9e924 100644 (file)
@@ -22,12 +22,10 @@ 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;
                }
@@ -48,14 +46,12 @@ 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) {
-                       //store_32(&free_lists[t][i], node);
-                       free_lists[t][i] = node;
+                       store_32(&free_lists[t][i], node);
                        //free_lists[t][i] = node;
                        return;
                }
@@ -98,18 +94,30 @@ 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) {
-               /**** detected UL (2 threads, 1 enqueue & 1 dequeue)  ****/
+               /**
+                       @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");
                if (tail == atomic_load_explicit(&q->tail, relaxed)) {
 
                        /* Check for uninitialized 'next' */
@@ -117,23 +125,25 @@ void enqueue(queue_t *q, unsigned int val)
 
                        if (get_ptr(next) == 0) { // == NULL
                                pointer value = MAKE_POINTER(node, get_count(next) + 1);
-                               /**** correctness error (1 dequeue & 1 enqueue) ****/
+                               /**** detected UL ****/
+                               // 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 == true
-                                       @Label: Enqueue_Success_Point
+                                       @Commit_point_define_check: success
+                                       @Label: Enqueue_UpdateNext
                                        @End
                                */
                        }
                        if (!success) {
                                // This routine helps the other enqueue to update the tail
-                               /**** detected UL (2 threads, 1 enqueue & 1 dequeue) ****/
+                               /**** detected UL ****/
                                unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
                                pointer value = MAKE_POINTER(ptr,
                                                get_count(tail) + 1);
                                /****FIXME: miss ****/
+                               // Second release can be just relaxed
                                bool succ = false;
                                succ = atomic_compare_exchange_strong_explicit(&q->tail,
                                                &tail, value, release, relaxed);
@@ -145,11 +155,18 @@ void enqueue(queue_t *q, unsigned int val)
                        }
                }
        }
-       /**** correctness error (1 dequeue & 1 enqueue) ****/
-       atomic_compare_exchange_strong_explicit(&q->tail,
+       /**** dectected UL ****/
+       // 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: succ 
+               @Label: Enqueue_UpdateOrLoad_Tail
+               @End
+       */
 }
 
 /**
@@ -157,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;
@@ -166,15 +183,37 @@ bool dequeue(queue_t *q, unsigned int *retVal)
        pointer next;
 
        while (!success) {
-               /**** FIXME: miss ****/
+               /**
+                       @Begin
+                       @Commit_point_clear: true
+                       @Label: Dequeue_Clear
+                       @End
+               */
+               /**** detected correctness error ****/
                head = atomic_load_explicit(&q->head, acquire);
-               // This must be acquire otherwise we have a bug with 1 enqueue &
-               // 1 dequeue
-               /**** correctness error (1 dequeue & 1 enqueue) ****/
-               tail = atomic_load_explicit(&q->tail, acquire);
-               /**** correctness error (1 dequeue & 1 enqueue) ****/
+               /**
+                       @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)) {
 
@@ -184,13 +223,15 @@ 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
                                }
                                /****FIXME: miss (not reached) ****/
+                               // Second release can be just relaxed
                                bool succ = false;
                                succ = atomic_compare_exchange_strong_explicit(&q->tail,
                                                &tail,
@@ -202,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);
-                               *retVal = 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: miss (not reached) ****/
+                               /****FIXME: 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 == true
-                                       @Label: Dequeue_Success_Point
-                                       @End
-                               */
                                if (!success)
                                        thrd_yield();
                        }
                }
        }
        reclaim(get_ptr(head));
+       *output = value;
        return true;
 }