7 #include "eventcount.h"
30 node* n = new node ();
37 RL_ASSERT(head == tail);
38 delete ((node*)head($));
48 typedef struct tag_elem {
57 __queue = new_spec_list();
60 tag_elem_t* new_tag_elem(call_id_t id, T data) {
61 tag_elem_t *e = (tag_elem_t*) MODEL_MALLOC(sizeof(tag_elem_t));
67 call_id_t get_id(void *wrapper) {
68 return ((tag_elem_t*) wrapper)->id;
71 unsigned int get_data(void *wrapper) {
72 return ((tag_elem_t*) wrapper)->data;
83 @Commit_point_set: Enqueue_Point
86 tag_elem_t *elem = new_tag_elem(__ID__, data);
87 push_back(__queue, elem);
92 node* n = new node (data);
93 head($)->next.store(n, std::memory_order_release);
96 @Commit_point_define_check: true
107 @Commit_point_set: Dequeue_Point
108 @ID: get_id(front(__queue))
110 T _Old_Val = get_data(front(__queue));
118 T data = try_dequeue();
122 data = try_dequeue();
126 data = try_dequeue();
136 std::atomic<node*> next;
154 node* n = t->next.load(std::memory_order_acquire);
157 @Commit_point_define_check: n != 0
158 @Label: Dequeue_Point