benchmark/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 inline bool fail(int ret) {
   8         return ret == ABORT || ret == EMPTY;
   9 }
  10
  11 Deque * create() {
  12         Deque * q = (Deque *) calloc(1, sizeof(Deque));
  13         Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int));
  14         atomic_store_explicit(&q->array, a, memory_order_relaxed);
  15         atomic_store_explicit(&q->top, 0, memory_order_relaxed);
  16         atomic_store_explicit(&q->bottom, 0, memory_order_relaxed);
  17         atomic_store_explicit(&a->size, 2, memory_order_relaxed);
  18         return q;
  19 }
  20
  21
  22 /**
  23         @Begin
  24         @Interface_define: Take
  25         @End
  26 */
  27 int take(Deque *q) {
  28         size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
  29         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
  30         atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
  31         /**** SPEC (sequential) (testcase1.c) ****/
  32         atomic_thread_fence(memory_order_seq_cst);
  33         size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
  34         int x;
  35         if (t <= b) {
  36                 /* Non-empty queue. */
  37                 int size = atomic_load_explicit(&a->size,memory_order_relaxed);
  38                 x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
  39                 /**
  40                         @Begin
  41                         @Commit_point_define_check: true
  42                         @Label: TakeReadBuffer
  43                         @End
  44                 */
  45                 if (t == b) {
  46                         /* Single last element in queue. */
  47                         //FIXME: weaken the following seq_cst causes no spec problem
  48                         bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
  49                                 1, memory_order_seq_cst, memory_order_relaxed);
  50                         if (!succ) {
  51                                 /* Failed race. */
  52                                 x = EMPTY;
  53                         }
  54                         atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
  55                 }
  56         } else { /* Empty queue. */
  57                 x = EMPTY;
  58                 atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
  59         }
  60         return x;
  61 }
  62
  63 void resize(Deque *q) {
  64         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
  65         size_t size=atomic_load_explicit(&a->size, memory_order_relaxed);
  66         size_t new_size=size << 1;
  67         Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array));
  68         size_t top=atomic_load_explicit(&q->top, memory_order_relaxed);
  69         size_t bottom=atomic_load_explicit(&q->bottom, memory_order_relaxed);
  70         atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed);
  71         size_t i;
  72
  73         // Initialize the whole new array to turn off the CDSChecker UL error
  74         // Check if CDSSpec checker can catch this bug
  75         /*
  76         for(i=0; i < new_size; i++) {
  77                 atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
  78         }
  79         */
  80         for(i=top; i < bottom; i++) {
  81                 atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
  82         }
  83         /**** detected UL ****/
  84         atomic_store_explicit(&q->array, new_a, memory_order_release);
  85         //printf("resize\n");
  86 }
  87
  88 /**
  89         @Begin
  90         @Interface_define: Push
  91         @End
  92 */
  93 void push(Deque *q, int x) {
  94         size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
  95         /**** SPEC (sequential) ****/
  96         size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
  97         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
  98         if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ {
  99                 resize(q);
 100                 // CDSSpec can actually detect the same bug if we avoid the UL error
 101                 //Bug in paper...should have next line...
 102                 a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
 103         }
 104         int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 105
 106         atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
 107         /** @OPDefine: true */
 108
 109         /**** UL & SPEC (Sync) (run with -u100 to avoid the uninitialized bug) ****/
 110         atomic_thread_fence(memory_order_release);
 111         atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
 112
 113 }
 114
 115 /**
 116         @Begin
 117         @Interface_define: Steal
 118         @End
 119 */
 120 int steal(Deque *q) {
 121         //Watch out: actually on need to be an acquire (don't count it)
 122         // An old bug
 123         size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
 124         /**
 125                 @Begin
 126                 @Commit_point_define_check: true
 127                 @Label: StealReadTop1
 128                 @End
 129         */
 130         /********** SPEC error (testcase3.c) **********/
 131         atomic_thread_fence(memory_order_seq_cst);
 132         /**** SPEC & UL ****/
 133         size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
 134
 135         int x = EMPTY;
 136         if (t < b) {
 137                 /**
 138                         @Begin
 139                         @Commit_point_clear: true
 140                         @Label: StealClear1
 141                         @End
 142                 */
 143
 144                 /* Non-empty queue. */
 145                 /**** detected UL ****/
 146                 Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
 147                 int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 148                 x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
 149                 /**
 150                         @Begin
 151                         @Commit_point_define_check: true
 152                         @Label: StealReadBuffer
 153                         @End
 154                 */
 155                 /**** SPEC (sequential) ****/
 156                 bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
 157                         memory_order_seq_cst, memory_order_relaxed);
 158                 if (!succ) {
 159                         /**
 160                                 @Begin
 161                                 @Commit_point_clear: true
 162                                 @Label: StealClear2
 163                                 @End
 164                         */
 165
 166                         /**
 167                                 @Begin
 168                                 @Commit_point_define_check: true
 169                                 @Label: StealReadTop2
 170                                 @End
 171                         */
 172
 173                         /* Failed race. */
 174                         return ABORT;
 175                 }
 176         }
 177         return x;
 178 }