4 #include "eventcount.h"
12 typedef struct tag_elem {
18 spec_queue<tag_elem> __queue;
20 static bool _is_elem_equals(void *ptr1, void *ptr2) {
22 // return if the elements pointed to are equal
32 node* n = new node ();
39 RL_ASSERT(head == tail);
40 delete ((node*)head($));
46 Enqueue = Enqueue_Success_Point
49 __queue.enqueue(tag_elem_t(tag.current(), node(data));
55 node* n = new node (data);
56 head($)->next.store(n, std::memory_order_release);
59 @Commit_point_define: true
60 @Label: Enqueue_Success_Point
71 Dequeue = Try_Dequeue_Success_Point
72 @ID: __queue.peak().tag
73 @Check: __queue.size() > 0 && _is_elem_equals(&RET, &__queue.peek().data)
74 @Action: __queue.dequeue();
79 T data = try_dequeue();
97 std::atomic<node*> next;
115 node* n = t->next.load(std::memory_order_acquire);
118 @Commit_point_define: ATOMIC_RET != NULL
119 @Label: Try_Dequeue_Success_Point