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                                                 a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
 157
 158         }
 159         int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 160
 161         atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
 162
 163
 164         atomic_thread_fence(memory_order_release);
 165         /* Automatically generated code for commit point define check: Push_Update_Bottom */
 166
 167         if (true) {
 168                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 169                 cp_define_check->label_num = 2;
 170                 cp_define_check->label_name = "Push_Update_Bottom";
 171                 cp_define_check->interface_num = 1;
 172                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 173                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 174                 annotation_cp_define_check->annotation = cp_define_check;
 175                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 176         }
 177
 178         atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
 179
 180 }
 181
 182
 183 int steal(Deque * q) {
 184         /* Interface begins */
 185         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 186         interface_begin->interface_num = 2; // Steal
 187                 interface_begin->interface_name = "Steal";
 188         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 189         annotation_interface_begin->type = INTERFACE_BEGIN;
 190         annotation_interface_begin->annotation = interface_begin;
 191         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 192         int __RET__ = __wrapper__steal(q);
 193         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 194         hb_condition->interface_num = 2; // Steal
 195         hb_condition->hb_condition_num = 0;
 196         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 197         annotation_hb_condition->type = HB_CONDITION;
 198         annotation_hb_condition->annotation = hb_condition;
 199         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 200
 201         Steal_info* info = (Steal_info*) malloc(sizeof(Steal_info));
 202         info->__RET__ = __RET__;
 203         info->q = q;
 204         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 205         interface_end->interface_num = 2; // Steal
 206         interface_end->info = info;
 207         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 208         annoation_interface_end->type = INTERFACE_END;
 209         annoation_interface_end->annotation = interface_end;
 210         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 211         return __RET__;
 212 }
 213
 214 int __wrapper__steal(Deque * q) {
 215                         size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
 216
 217                 atomic_thread_fence(memory_order_seq_cst);
 218
 219         size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
 220         /* Automatically generated code for commit point define check: Steal_Read_Bottom */
 221
 222         if (true) {
 223                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 224                 cp_define_check->label_num = 3;
 225                 cp_define_check->label_name = "Steal_Read_Bottom";
 226                 cp_define_check->interface_num = 2;
 227                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 228                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 229                 annotation_cp_define_check->annotation = cp_define_check;
 230                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 231         }
 232
 233
 234
 235         int x = EMPTY;
 236         if (t < b) {
 237
 238
 239                 Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
 240
 241                 int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 242                 x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
 243
 244
 245                 bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
 246                         memory_order_seq_cst, memory_order_relaxed);
 247
 248
 249         /* Automatically generated code for commit point define check: Steal_Additional_Point */
 250
 251         if (true) {
 252                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 253                 cp_define_check->label_num = 4;
 254                 cp_define_check->label_name = "Steal_Additional_Point";
 255                 cp_define_check->interface_num = 2;
 256                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 257                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 258                 annotation_cp_define_check->annotation = cp_define_check;
 259                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 260         }
 261
 262
 263
 264                 if (!succ) {
 265
 266                         return ABORT;
 267                 }
 268         }
 269         return x;
 270 }
 271