atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0));
}
-/**
- @Begin
- @Global_define:
- typedef struct tag_elem {
- Tag id;
- unsigned int data;
-
- tag_elem(Tag _id, unsigned int _data) {
- id = _id;
- data = _data;
- }
- } tag_elem_t;
-
- spec_queue<tag_elem_t> __queue;
- Tag __tag;
- @Happens_before:
- # Only check the happens-before relationship according to the id of the
- # commit_point_set. For commit_point_set that has same ID, A -> B means
- # B happens after the previous A.
- Enqueue -> Dequeue
- @End
-*/
-
/**
@Begin
@Interface_define: Enqueue