changes

diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index a2e8e9adc38536aca478427e952ba0fc9a82ce22..48400145d2c4af186bfcfeb5b8769d5449773bdd 100644 (file)
--- a/benchmark/ms-queue/main.c
+++ b/benchmark/ms-queue/main.c
@@ -32,13 +32,13 @@ static void main_task(void *param)
                input[0] = 17;
                //enqueue(queue, input[0]);
                enqueue(queue, input[0]);
-               output[0] = dequeue(queue);
+               //output[0] = dequeue(queue);
        } else {
                input[1] = 37;
-               enqueue(queue, input[1]);
+               //enqueue(queue, input[1]);
                //output[1] = dequeue(queue);
                //output[0] = dequeue(queue);
-               output[0] = dequeue(queue);
+               bool succ = dequeue(queue, &output[0]);
        }
 }
 

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 1f4835ed70c8eaf9e65773664a83808b8da42cd9..50787854561c46a787dfcd0a516b4596693d5591 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -156,7 +156,7 @@ void enqueue(queue_t *q, unsigned int val)
        @Interface_define: Dequeue
        @End
 */
-unsigned int dequeue(queue_t *q)
+bool dequeue(queue_t *q, unsigned int *retVal)
 {
        unsigned int value;
        int success = 0;
@@ -167,6 +167,8 @@ unsigned int dequeue(queue_t *q)
        while (!success) {
                /**** 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
                tail = atomic_load_explicit(&q->tail, relaxed);
                /****FIXME: miss ****/
                next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
@@ -184,7 +186,7 @@ unsigned int dequeue(queue_t *q)
                                                @Label: Dequeue_Empty_Point
                                                @End
                                        */
-                                       return 0; // NULL
+                                       return false; // NULL
                                }
                                /****FIXME: miss (not reached) ****/
                                // Second release can be just relaxed
@@ -199,7 +201,7 @@ unsigned int dequeue(queue_t *q)
                                //printf("miss4_dequeue\n");
                                thrd_yield();
                        } else {
-                               value = load_32(&q->nodes[get_ptr(next)].value);
+                               *retVal = load_32(&q->nodes[get_ptr(next)].value);
                                //value = q->nodes[get_ptr(next)].value;
                                /****FIXME: correctness error ****/
                                // Seconde release can be just relaxed
@@ -219,5 +221,5 @@ unsigned int dequeue(queue_t *q)
                }
        }
        reclaim(get_ptr(head));
-       return value;
+       return true;
 }

diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index bc4c3453b9396227ed4760d78a224e14396b6412..d6b2a695d6789a9b732bfd75eac564842bf3ecd6 100644 (file)
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -113,10 +113,10 @@ void enqueue(queue_t *q, unsigned int val);
                        _Old_Val = 0;
                }
        @Post_check:
-               _Old_Val == __RET__
+               _Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
        @End
 */
-unsigned int dequeue(queue_t *q);
+bool dequeue(queue_t *q, unsigned int *retVal);
 int get_thread_num();
 
 #endif