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 145c91d30dcd8723ceb5da0c57918ee3a711d097..e30535cabbcfb93e8f1cf873a1516d9860349105 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -183,6 +183,13 @@ bool dequeue(queue_t *q, int *retVal)
                */
                /**** detected correctness error ****/
                head = atomic_load_explicit(&q->head, acquire);
                */
                /**** detected correctness error ****/
                head = atomic_load_explicit(&q->head, acquire);

+               /**
+                       @Begin
+                       @Commit_point_define_check: true
+                       @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!!
                /** 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!!