9 #include <cdsannotate.h>
10 #include <specannotation.h>
11 #include <model_memory.h>
13 #include "eventcount.h"
36 node* n = new node ();
43 RL_ASSERT(head == tail);
44 delete ((node*)head($));
54 typedef struct tag_elem {
63 __queue = new_spec_list();
66 tag_elem_t* new_tag_elem(call_id_t id, T data) {
67 tag_elem_t *e = (tag_elem_t*) MODEL_MALLOC(sizeof(tag_elem_t));
73 call_id_t get_id(void *wrapper) {
74 return ((tag_elem_t*) wrapper)->id;
77 unsigned int get_data(void *wrapper) {
78 return ((tag_elem_t*) wrapper)->data;
89 @Commit_point_set: Enqueue_Point
92 tag_elem_t *elem = new_tag_elem(__ID__, data);
93 push_back(__queue, elem);
98 node* n = new node (data);
99 head($)->next.store(n, std::memory_order_release);
102 @Commit_point_define_check: true
103 @Label: Enqueue_Point
113 @Commit_point_set: Dequeue_Point
114 @ID: get_id(front(__queue))
116 T _Old_Val = get_data(front(__queue));
124 T data = try_dequeue();
128 data = try_dequeue();
132 data = try_dequeue();
142 std::atomic<node*> next;
160 node* n = t->next.load(std::memory_order_acquire);
163 @Commit_point_define_check: n != 0
164 @Label: Dequeue_Point