output/chase-lev-deque-bugfix/deque.c

   1 #include <stdatomic.h>
   2 #include <inttypes.h>
   3 #include "deque.h"
   4 #include <stdlib.h>
   5 #include <stdio.h>
   6
   7 Deque * create() {
   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);
  14         return q;
  15 }
  16
  17
  18
  19 int take(Deque * q) {
  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__;
  31         info->q = q;
  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);
  39         return __RET__;
  40 }
  41
  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 */
  45
  46         if (true) {
  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);
  55         }
  56
  57         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
  58
  59         atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
  60
  61         atomic_thread_fence(memory_order_seq_cst);
  62         size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
  63
  64         int x;
  65         if (t <= b) {
  66
  67                 int size = atomic_load_explicit(&a->size,memory_order_relaxed);
  68                 x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
  69
  70                 if (t == b) {
  71
  72                                                 bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
  73                                 1, memory_order_seq_cst, memory_order_relaxed);
  74
  75
  76         /* Automatically generated code for commit point define check: Take_Additional_Point */
  77
  78         if (true) {
  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);
  87         }
  88
  89                         if (!succ) {
  90
  91                                 x = EMPTY;
  92                         }
  93                         atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
  94                 }
  95         } else {
  96                 x = EMPTY;
  97                 atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
  98         }
  99         return x;
 100 }
 101
 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);
 110         size_t i;
 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);
 113         }
 114
 115         atomic_store_explicit(&q->array, new_a, memory_order_release);
 116         }
 117
 118
 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);
 136
 137         Push_info* info = (Push_info*) malloc(sizeof(Push_info));
 138         info->q = q;
 139         info->x = x;
 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);
 147 }
 148
 149 void __wrapper__push(Deque * q, int x) {
 150         size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
 151
 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)  {
 155                 resize(q);
 156
 157         }
 158         int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 159
 160         atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
 161
 162
 163         atomic_thread_fence(memory_order_release);
 164         /* Automatically generated code for commit point define check: Push_Update_Bottom */
 165
 166         if (true) {
 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);
 175         }
 176
 177         atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
 178
 179 }
 180
 181
 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);
 199
 200         Steal_info* info = (Steal_info*) malloc(sizeof(Steal_info));
 201         info->__RET__ = __RET__;
 202         info->q = q;
 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);
 210         return __RET__;
 211 }
 212
 213 int __wrapper__steal(Deque * q) {
 214                         size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
 215
 216                 atomic_thread_fence(memory_order_seq_cst);
 217
 218         size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
 219         /* Automatically generated code for commit point define check: Steal_Read_Bottom */
 220
 221         if (true) {
 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);
 230         }
 231
 232
 233
 234         int x = EMPTY;
 235         if (t < b) {
 236
 237
 238                 Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
 239
 240                 int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 241                 x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
 242
 243
 244                 bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
 245                         memory_order_seq_cst, memory_order_relaxed);
 246
 247
 248         /* Automatically generated code for commit point define check: Steal_Additional_Point */
 249
 250         if (true) {
 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);
 259         }
 260
 261
 262
 263                 if (!succ) {
 264
 265                         return ABORT;
 266                 }
 267         }
 268         return x;
 269 }
 270