X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=benchmark%2Fms-queue%2Fmy_queue.c;h=e30535cabbcfb93e8f1cf873a1516d9860349105;hp=145c91d30dcd8723ceb5da0c57918ee3a711d097;hb=d81ef0a8f5a876f83b327107451bff887c2cb305;hpb=8ac7b8682c102a5c2661e7798c9a0f11cfcec4e3

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 145c91d..e30535c 100644
--- 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);
+		/**
+			@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!!