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 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         @Begin
  20         @Interface_define: Take
  21         @End
  22 */
  23 int take(Deque *q) {
  24         size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
  25         /**
  26                 @Begin
  27                 @Commit_point_define_check: true
  28                 @Label: Take_Read_Bottom
  29                 @End
  30         */
  31         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
  32         /**
  33                 //@Begin
  34                 @Commit_point_define_check: true
  35                 @Label: Take_Read_Array
  36                 @End
  37         */
  38         atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
  39         /**** detected correctness ****/
  40         atomic_thread_fence(memory_order_seq_cst);
  41         size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
  42         /**
  43                 //@Begin
  44                 @Commit_point_define_check: t != b
  45                 @Label: Take_Read_Top
  46                 @End
  47         */
  48         int x;
  49         if (t <= b) {
  50                 /* Non-empty queue. */
  51                 int size = atomic_load_explicit(&a->size,memory_order_relaxed);
  52                 x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
  53                 /**
  54                         //@Begin
  55                         @Commit_point_define_check: t != b
  56                         @Label: Take_Read_Buffer
  57                         @End
  58                 */
  59                 if (t == b) {
  60                         /* Single last element in queue. */
  61                         //FIXME: weaken the following seq_cst causes no spec problem
  62                         bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
  63                                 1, memory_order_seq_cst, memory_order_relaxed);
  64                         /**
  65                                 //@Begin
  66                                 @Commit_point_define_check: succ
  67                                 @Label: Take_CAS_Top
  68                                 @End
  69                         */
  70
  71                         /**
  72                                 @Begin
  73                                 @Additional_ordering_point_define_check: true
  74                                 @Label: Take_Additional_Point
  75                                 @End
  76                         */
  77                         if (!succ) {
  78                                 /* Failed race. */
  79                                 x = EMPTY;
  80                         }
  81                         atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
  82                 }
  83         } else { /* Empty queue. */
  84                 x = EMPTY;
  85                 atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
  86         }
  87         return x;
  88 }
  89
  90 void resize(Deque *q) {
  91         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
  92         size_t size=atomic_load_explicit(&a->size, memory_order_relaxed);
  93         size_t new_size=size << 1;
  94         Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array));
  95         size_t top=atomic_load_explicit(&q->top, memory_order_relaxed);
  96         size_t bottom=atomic_load_explicit(&q->bottom, memory_order_relaxed);
  97         atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed);
  98         size_t i;
  99         for(i=top; i < bottom; i++) {
 100                 atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
 101         }
 102         /**** detected UL ****/
 103         atomic_store_explicit(&q->array, new_a, memory_order_release);
 104         //printf("resize\n");
 105 }
 106
 107 /**
 108         @Begin
 109         @Interface_define: Push
 110         @End
 111 */
 112 void push(Deque *q, int x) {
 113         size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
 114         /**** detected correctness ****/
 115         size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
 116         Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
 117         if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ {
 118                 resize(q);
 119                 //Bug in paper...should have next line...
 120                 a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
 121                 /**
 122                         //@Begin
 123                         @Commit_point_define_check: true
 124                         @Label: Push_Read_Array
 125                         @End
 126                 */
 127         }
 128         int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 129
 130         atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
 131         /**
 132                 //@Begin
 133                 @Commit_point_define_check: true
 134                 @Label: Push_Update_Buffer
 135                 @End
 136         */
 137         /**** detected HB error (run with -u100 to avoid the uninitialized bug) ****/
 138         atomic_thread_fence(memory_order_release);
 139
 140         atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
 141         /**
 142                 @Begin
 143                 @Commit_point_define_check: true
 144                 @Label: Push_Update_Bottom
 145                 @End
 146         */
 147 }
 148
 149 /**
 150         @Begin
 151         @Interface_define: Steal
 152         @End
 153 */
 154 int steal(Deque *q) {
 155         //FIXME: weaken the following acquire causes no spec problem
 156         size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
 157         /**
 158                 //@Begin
 159                 @Potential_commit_point_define: true
 160                 @Label: Steal_Potential_Read_Tail
 161                 @End
 162         */
 163         //FIXME: remove the fence causes no error and fewer executions..
 164         atomic_thread_fence(memory_order_seq_cst);
 165         /**** detected HB error (run with -u100 to avoid the uninitialized bug) ****/
 166         size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
 167         /**
 168                 @Begin
 169                 @Commit_point_define_check: true
 170                 @Label: Steal_Read_Bottom
 171                 @End
 172         */
 173
 174         /**
 175                 //@Begin
 176                 @Commit_point_define: t >= b
 177                 @Potential_commit_point_label: Steal_Potential_Read_Tail
 178                 @Label: Steal_Read_Tail
 179                 @End
 180         */
 181         int x = EMPTY;
 182         if (t < b) {
 183                 /* Non-empty queue. */
 184                 /**** detected UL ****/
 185                 Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
 186                 /**
 187                         //@Begin
 188                         @Commit_point_define_check: true
 189                         @Label: Steal_Read_Array
 190                         @End
 191                 */
 192                 int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 193                 x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
 194                 /**
 195                         //@Begin
 196                         @Potential_commit_point_define: true
 197                         @Label: Steal_Potential_Read_Buffer
 198                         @End
 199                 */
 200                 /**** detected correctness failure ****/
 201                 bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
 202                         memory_order_seq_cst, memory_order_relaxed);
 203                 /**
 204                         //@Begin
 205                         @Commit_point_define_check: succ
 206                         @Label: Steal_CAS_Top
 207                         @End
 208                 */
 209
 210                 /**
 211                         @Begin
 212                         @Additional_ordering_point_define_check: true
 213                         @Label: Steal_Additional_Point
 214                         @End
 215                 */
 216
 217                 /**
 218                         //@Begin
 219                         @Commit_point_define: succ
 220                         @Potential_commit_point_label: Steal_Potential_Read_Buffer
 221                         @Label: Steal_Read_Buffer
 222                         @End
 223                 */
 224                 if (!succ) {
 225                         /* Failed race. */
 226                         return ABORT;
 227                 }
 228         }
 229         return x;
 230 }