9 #include <cdsannotate.h>
10 #include <specannotation.h>
11 #include <model_memory.h>
14 #include "eventcount.h"
30 node* n = new node ();
40 /* All other user-defined structs */
41 static IntegerList * __queue;
42 /* All other user-defined functions */
43 /* Definition of interface info struct: Dequeue */
44 typedef struct Dequeue_info {
47 /* End of info struct definition: Dequeue */
49 /* ID function of interface: Dequeue */
50 inline static call_id_t Dequeue_id(void *info, thread_id_t __TID__) {
51 Dequeue_info* theInfo = (Dequeue_info*)info;
52 T __RET__ = theInfo->__RET__;
54 call_id_t __ID__ = __RET__ ? __RET__ : 0;
57 /* End of ID function: Dequeue */
59 /* Check action function of interface: Dequeue */
60 inline static bool Dequeue_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
62 Dequeue_info* theInfo = (Dequeue_info*)info;
63 T __RET__ = theInfo->__RET__;
67 elem = front ( __queue ) ;
68 pop_front ( __queue ) ;
70 check_passed = __RET__ ? __RET__ == elem : true;
75 /* End of check action function: Dequeue */
77 /* Definition of interface info struct: Enqueue */
78 typedef struct Enqueue_info {
81 /* End of info struct definition: Enqueue */
83 /* ID function of interface: Enqueue */
84 inline static call_id_t Enqueue_id(void *info, thread_id_t __TID__) {
85 Enqueue_info* theInfo = (Enqueue_info*)info;
86 T data = theInfo->data;
88 call_id_t __ID__ = data;
91 /* End of ID function: Enqueue */
93 /* Check action function of interface: Enqueue */
94 inline static bool Enqueue_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
96 Enqueue_info* theInfo = (Enqueue_info*)info;
97 T data = theInfo->data;
99 push_back ( __queue , data ) ;
102 /* End of check action function: Enqueue */
104 #define INTERFACE_SIZE 2
105 static void** func_ptr_table;
106 static hb_rule** hb_rule_table;
107 static commutativity_rule** commutativity_rule_table;
108 inline static bool CommutativityCondition0(void *info1, void *info2) {
109 Enqueue_info *_info1 = (Enqueue_info*) info1;
110 Dequeue_info *_info2 = (Dequeue_info*) info2;
113 inline static bool CommutativityCondition1(void *info1, void *info2) {
114 Dequeue_info *_info1 = (Dequeue_info*) info1;
115 Dequeue_info *_info2 = (Dequeue_info*) info2;
116 return ! _info1-> __RET__ || ! _info2-> __RET__;
119 /* Initialization of sequential varialbes */
120 static void __SPEC_INIT__() {
121 __queue = createIntegerList ( ) ;
124 /* Cleanup routine of sequential variables */
125 static bool __SPEC_CLEANUP__() {
126 if ( __queue ) destroyIntegerList ( __queue ) ;
130 /* Define function for sequential code initialization */
131 inline static void __sequential_init() {
132 /* Init func_ptr_table */
133 func_ptr_table = (void**) malloc(sizeof(void*) * 2 * 2);
134 func_ptr_table[2 * 1] = (void*) &Dequeue_id;
135 func_ptr_table[2 * 1 + 1] = (void*) &Dequeue_check_action;
136 func_ptr_table[2 * 0] = (void*) &Enqueue_id;
137 func_ptr_table[2 * 0 + 1] = (void*) &Enqueue_check_action;
138 /* Enqueue(true) -> Dequeue(true) */
139 struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
140 hbConditionInit0->interface_num_before = 0; // Enqueue
141 hbConditionInit0->hb_condition_num_before = 0; //
142 hbConditionInit0->interface_num_after = 1; // Dequeue
143 hbConditionInit0->hb_condition_num_after = 0; //
144 /* Init hb_rule_table */
145 hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 1);
146 #define HB_RULE_TABLE_SIZE 1
147 hb_rule_table[0] = hbConditionInit0;
148 /* Init commutativity_rule_table */
149 commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 2);
150 commutativity_rule* rule;
151 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
152 rule->interface_num_before = 0;
153 rule->interface_num_after = 1;
155 rule->condition = CommutativityCondition0;
156 commutativity_rule_table[0] = rule;
157 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
158 rule->interface_num_before = 1;
159 rule->interface_num_after = 1;
160 rule->rule = "! _Method1 . __RET__ || ! _Method2 . __RET__";
161 rule->condition = CommutativityCondition1;
162 commutativity_rule_table[1] = rule;
163 /* Pass init info, including function table info & HB rules & Commutativity Rules */
164 struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
165 anno_init->init_func = (void_func_t) __SPEC_INIT__;
166 anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
167 anno_init->func_table = func_ptr_table;
168 anno_init->func_table_size = INTERFACE_SIZE;
169 anno_init->hb_rule_table = hb_rule_table;
170 anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
171 anno_init->commutativity_rule_table = commutativity_rule_table;
172 anno_init->commutativity_rule_table_size = 2;
173 struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
175 init->annotation = anno_init;
176 cdsannotate(SPEC_ANALYSIS, init);
180 /* End of Global construct generation in class */
185 void enqueue(T data) {
186 /* Interface begins */
187 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
188 interface_begin->interface_num = 0; // Enqueue
189 interface_begin->interface_name = "Enqueue";
190 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
191 annotation_interface_begin->type = INTERFACE_BEGIN;
192 annotation_interface_begin->annotation = interface_begin;
193 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
194 __wrapper__enqueue(data);
195 struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
196 hb_condition->interface_num = 0; // Enqueue
197 hb_condition->hb_condition_num = 0;
198 struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
199 annotation_hb_condition->type = HB_CONDITION;
200 annotation_hb_condition->annotation = hb_condition;
201 cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
203 Enqueue_info* info = (Enqueue_info*) malloc(sizeof(Enqueue_info));
205 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
206 interface_end->interface_num = 0; // Enqueue
207 interface_end->info = info;
208 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
209 annoation_interface_end->type = INTERFACE_END;
210 annoation_interface_end->annotation = interface_end;
211 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
214 void __wrapper__enqueue(T data)
216 node* n = new node (data);
218 head->next.store(n, std::memory_order_release);
219 /* Automatically generated code for commit point define check: Enqueue_Point */
222 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
223 cp_define_check->label_num = 0;
224 cp_define_check->label_name = "Enqueue_Point";
225 cp_define_check->interface_num = 0;
226 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
227 annotation_cp_define_check->type = CP_DEFINE_CHECK;
228 annotation_cp_define_check->annotation = cp_define_check;
229 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
237 /* Interface begins */
238 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
239 interface_begin->interface_num = 1; // Dequeue
240 interface_begin->interface_name = "Dequeue";
241 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
242 annotation_interface_begin->type = INTERFACE_BEGIN;
243 annotation_interface_begin->annotation = interface_begin;
244 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
245 T __RET__ = __wrapper__dequeue();
246 struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
247 hb_condition->interface_num = 1; // Dequeue
248 hb_condition->hb_condition_num = 0;
249 struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
250 annotation_hb_condition->type = HB_CONDITION;
251 annotation_hb_condition->annotation = hb_condition;
252 cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
254 Dequeue_info* info = (Dequeue_info*) malloc(sizeof(Dequeue_info));
255 info->__RET__ = __RET__;
256 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
257 interface_end->interface_num = 1; // Dequeue
258 interface_end->info = info;
259 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
260 annoation_interface_end->type = INTERFACE_END;
261 annoation_interface_end->annotation = interface_end;
262 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
266 T __wrapper__dequeue()
268 T data = try_dequeue();
272 data = try_dequeue();
276 data = try_dequeue();
286 std::atomic<node*> next;
307 node* n = t->next.load(std::memory_order_acquire);
308 /* Automatically generated code for commit point define check: Dequeue_Point */
311 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
312 cp_define_check->label_num = 1;
313 cp_define_check->label_name = "Dequeue_Point";
314 cp_define_check->interface_num = 1;
315 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
316 annotation_cp_define_check->type = CP_DEFINE_CHECK;
317 annotation_cp_define_check->annotation = cp_define_check;
318 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
330 void** spsc_queue<T>::func_ptr_table;
332 hb_rule** spsc_queue<T>::hb_rule_table;
334 commutativity_rule** spsc_queue<T>::commutativity_rule_table;
336 IntegerList * spsc_queue<T>::__queue;