changes

[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 bb237bf6c0df386167749820c007ad7fe7e9908c..fe4da51fe7275a87dd062a6fef9af7152c46855f 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -161,12 +161,6 @@ void enqueue(queue_t *q, unsigned int val)
                        &tail,
                        MAKE_POINTER(node, get_count(tail) + 1),
                        release, relaxed);
                        &tail,
                        MAKE_POINTER(node, get_count(tail) + 1),
                        release, relaxed);

-       /**
-               //@Begin
-               @Commit_point_define_check: succ
-               @Label: Enqueue_UpdateOrLoad_Tail
-               @End
-       */

 }
 
 /**
 }
 
 /**


@@ -176,7 +170,7 @@ void enqueue(queue_t *q, unsigned int val)
 */
 bool dequeue(queue_t *q, int *retVal)
 {
 */
 bool dequeue(queue_t *q, int *retVal)
 {

-       unsigned int value;
+       unsigned int value = 0;

        int success = 0;
        pointer head;
        pointer tail;
        int success = 0;
        pointer head;
        pointer tail;


@@ -197,6 +191,10 @@ bool dequeue(queue_t *q, int *retVal)
                        @Label: Dequeue_Read_Head
                        @End
                */
                        @Label: Dequeue_Read_Head
                        @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)
+                */

                tail = atomic_load_explicit(&q->tail, acquire);
                /**
                        @Begin
                tail = atomic_load_explicit(&q->tail, acquire);
                /**
                        @Begin


@@ -243,26 +241,26 @@ bool dequeue(queue_t *q, int *retVal)
                                //printf("miss4_dequeue\n");
                                thrd_yield();
                        } else {
                                //printf("miss4_dequeue\n");
                                thrd_yield();
                        } else {

-                               /**
-                                       @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 = load_32(&q->nodes[get_ptr(next)].value);

-                               *retVal = value;

                                //value = q->nodes[get_ptr(next)].value;
                                /****FIXME: correctness error ****/
                                success = atomic_compare_exchange_strong_explicit(&q->head,
                                                &head,
                                                MAKE_POINTER(get_ptr(next), get_count(head) + 1),
                                                release, relaxed);
                                //value = q->nodes[get_ptr(next)].value;
                                /****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: success
+                                       @Potential_commit_point_label: Dequeue_Potential_LoadNext
+                                       @Label: Dequeue_LoadNext
+                                       @End
+                               */

                                if (!success)
                                        thrd_yield();
                        }
                }
        }
        reclaim(get_ptr(head));
                                if (!success)
                                        thrd_yield();
                        }
                }
        }
        reclaim(get_ptr(head));

+       *retVal = value;

        return true;
 }
        return true;
 }