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($));
58 __queue = createIntegerList();
61 destroyIntegerList(__queue);
63 @Happens_before: Enqueue -> Dequeue
64 @Commutativity: Enqueue <-> Dequeue: true
65 @Commutativity: Dequeue <-> Dequeue: !_Method1.__RET__ || !_Method2.__RET__
74 @Commit_point_set: Enqueue_Point
77 push_back(__queue, data);
78 //model_print("Enqueue: val=%d\n", val);
83 node* n = new node (data);
84 /********** DR & SPEC (sequential) **********/
85 //head($)->next.store(n, std::memory_order_release);
86 head->next.store(n, std::memory_order_release);
89 @Commit_point_define_check: true
100 @Commit_point_set: Dequeue_Point
101 @ID: __RET__ ? __RET__ : 0
105 elem = front(__queue);
108 //model_print("Dequeue: __RET__=%d, retVal=%d, elem=%d, \n", __RET__, *retVal, elem);
109 //model_print("Result: %d\n", __RET__ ? *retVal == elem : true);
110 @Post_check: __RET__ ? __RET__ == elem : true
115 T data = try_dequeue();
119 data = try_dequeue();
123 data = try_dequeue();
133 std::atomic<node*> next;
144 //rl::var<node*> head;
145 //rl::var<node*> tail;
157 /********** DR & SPEC (sequential) **********/
158 node* n = t->next.load(std::memory_order_acquire);
161 @Commit_point_define_check: n != 0
162 @Label: Dequeue_Point
167 //T data = n->data($);