9 #include <cdsannotate.h>
10 #include <specannotation.h>
11 #include <model_memory.h>
14 #include "eventcount.h"
37 node* n = new node ();
44 //RL_ASSERT(head == tail);
45 delete ((node*)head($));
55 typedef struct tag_elem {
64 __queue = new_spec_list();
67 tag_elem_t* new_tag_elem(call_id_t id, T data) {
68 tag_elem_t *e = (tag_elem_t*) MODEL_MALLOC(sizeof(tag_elem_t));
74 call_id_t get_id(void *wrapper) {
75 return ((tag_elem_t*) wrapper)->id;
78 unsigned int get_data(void *wrapper) {
79 return ((tag_elem_t*) wrapper)->data;
90 @Commit_point_set: Enqueue_Point
93 tag_elem_t *elem = new_tag_elem(__ID__, data);
94 push_back(__queue, elem);
99 node* n = new node (data);
100 head($)->next.store(n, std::memory_order_release);
103 @Commit_point_define_check: true
104 @Label: Enqueue_Point
114 @Commit_point_set: Dequeue_Point
115 @ID: get_id(front(__queue))
117 T _Old_Val = get_data(front(__queue));
125 T data = try_dequeue();
129 data = try_dequeue();
133 data = try_dequeue();
143 std::atomic<node*> next;
161 node* n = t->next.load(std::memory_order_acquire);
164 @Commit_point_define_check: n != 0
165 @Label: Dequeue_Point