*/
/**** 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!!