8 Deque * q = (Deque *) calloc(1, sizeof(Deque));
9 Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int));
10 atomic_store_explicit(&q->array, a, memory_order_relaxed);
11 atomic_store_explicit(&q->top, 0, memory_order_relaxed);
12 atomic_store_explicit(&q->bottom, 0, memory_order_relaxed);
13 atomic_store_explicit(&a->size, 2, memory_order_relaxed);
20 /* Interface begins */
21 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
22 interface_begin->interface_num = 0; // Take
23 interface_begin->interface_name = "Take";
24 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
25 annotation_interface_begin->type = INTERFACE_BEGIN;
26 annotation_interface_begin->annotation = interface_begin;
27 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
28 int __RET__ = __wrapper__take(q);
29 Take_info* info = (Take_info*) malloc(sizeof(Take_info));
30 info->__RET__ = __RET__;
32 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
33 interface_end->interface_num = 0; // Take
34 interface_end->info = info;
35 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
36 annoation_interface_end->type = INTERFACE_END;
37 annoation_interface_end->annotation = interface_end;
38 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
42 int __wrapper__take(Deque * q) {
43 size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
44 /* Automatically generated code for commit point define check: Take_Read_Bottom */
47 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
48 cp_define_check->label_num = 0;
49 cp_define_check->label_name = "Take_Read_Bottom";
50 cp_define_check->interface_num = 0;
51 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
52 annotation_cp_define_check->type = CP_DEFINE_CHECK;
53 annotation_cp_define_check->annotation = cp_define_check;
54 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
57 Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
59 atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
61 atomic_thread_fence(memory_order_seq_cst);
62 size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
67 int size = atomic_load_explicit(&a->size,memory_order_relaxed);
68 x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
72 bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
73 1, memory_order_seq_cst, memory_order_relaxed);
76 /* Automatically generated code for commit point define check: Take_Additional_Point */
79 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
80 cp_define_check->label_num = 1;
81 cp_define_check->label_name = "Take_Additional_Point";
82 cp_define_check->interface_num = 0;
83 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
84 annotation_cp_define_check->type = CP_DEFINE_CHECK;
85 annotation_cp_define_check->annotation = cp_define_check;
86 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
93 atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
97 atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
102 void resize(Deque *q) {
103 Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
104 size_t size=atomic_load_explicit(&a->size, memory_order_relaxed);
105 size_t new_size=size << 1;
106 Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array));
107 size_t top=atomic_load_explicit(&q->top, memory_order_relaxed);
108 size_t bottom=atomic_load_explicit(&q->bottom, memory_order_relaxed);
109 atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed);
111 for(i=top; i < bottom; i++) {
112 atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
115 atomic_store_explicit(&q->array, new_a, memory_order_release);
119 void push(Deque * q, int x) {
120 /* Interface begins */
121 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
122 interface_begin->interface_num = 1; // Push
123 interface_begin->interface_name = "Push";
124 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
125 annotation_interface_begin->type = INTERFACE_BEGIN;
126 annotation_interface_begin->annotation = interface_begin;
127 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
128 __wrapper__push(q, x);
129 struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
130 hb_condition->interface_num = 1; // Push
131 hb_condition->hb_condition_num = 0;
132 struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
133 annotation_hb_condition->type = HB_CONDITION;
134 annotation_hb_condition->annotation = hb_condition;
135 cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
137 Push_info* info = (Push_info*) malloc(sizeof(Push_info));
140 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
141 interface_end->interface_num = 1; // Push
142 interface_end->info = info;
143 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
144 annoation_interface_end->type = INTERFACE_END;
145 annoation_interface_end->annotation = interface_end;
146 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
149 void __wrapper__push(Deque * q, int x) {
150 size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
152 size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
153 Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
154 if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) {
158 int size = atomic_load_explicit(&a->size, memory_order_relaxed);
160 atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
163 atomic_thread_fence(memory_order_release);
164 /* Automatically generated code for commit point define check: Push_Update_Bottom */
167 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
168 cp_define_check->label_num = 2;
169 cp_define_check->label_name = "Push_Update_Bottom";
170 cp_define_check->interface_num = 1;
171 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
172 annotation_cp_define_check->type = CP_DEFINE_CHECK;
173 annotation_cp_define_check->annotation = cp_define_check;
174 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
177 atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
182 int steal(Deque * q) {
183 /* Interface begins */
184 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
185 interface_begin->interface_num = 2; // Steal
186 interface_begin->interface_name = "Steal";
187 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
188 annotation_interface_begin->type = INTERFACE_BEGIN;
189 annotation_interface_begin->annotation = interface_begin;
190 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
191 int __RET__ = __wrapper__steal(q);
192 struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
193 hb_condition->interface_num = 2; // Steal
194 hb_condition->hb_condition_num = 0;
195 struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
196 annotation_hb_condition->type = HB_CONDITION;
197 annotation_hb_condition->annotation = hb_condition;
198 cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
200 Steal_info* info = (Steal_info*) malloc(sizeof(Steal_info));
201 info->__RET__ = __RET__;
203 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
204 interface_end->interface_num = 2; // Steal
205 interface_end->info = info;
206 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
207 annoation_interface_end->type = INTERFACE_END;
208 annoation_interface_end->annotation = interface_end;
209 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
213 int __wrapper__steal(Deque * q) {
214 size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
216 atomic_thread_fence(memory_order_seq_cst);
218 size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
219 /* Automatically generated code for commit point define check: Steal_Read_Bottom */
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 = 3;
224 cp_define_check->label_name = "Steal_Read_Bottom";
225 cp_define_check->interface_num = 2;
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);
238 Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
240 int size = atomic_load_explicit(&a->size, memory_order_relaxed);
241 x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
244 bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
245 memory_order_seq_cst, memory_order_relaxed);
248 /* Automatically generated code for commit point define check: Steal_Additional_Point */
251 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
252 cp_define_check->label_num = 4;
253 cp_define_check->label_name = "Steal_Additional_Point";
254 cp_define_check->interface_num = 2;
255 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
256 annotation_cp_define_check->type = CP_DEFINE_CHECK;
257 annotation_cp_define_check->annotation = cp_define_check;
258 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);