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         /**** SPEC (sequential) (testcase1.c) ****/
  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         /**** SPEC (sequential) ****/
 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                 // CDSSpec can actually detect the same bug if we avoid the UL error
 120                 //Bug in paper...should have next line...
 121                 a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
 122                 /**
 123                         //@Begin
 124                         @Commit_point_define_check: true
 125                         @Label: Push_Read_Array
 126                         @End
 127                 */
 128         }
 129         int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 130
 131         atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
 132         /**
 133                 //@Begin
 134                 @Commit_point_define_check: true
 135                 @Label: Push_Update_Buffer
 136                 @End
 137         */
 138         /**** SPEC (Sync) (run with -u100 to avoid the uninitialized bug) ****/
 139         atomic_thread_fence(memory_order_release);
 140         // Watch out!!! We need to specifiy the fence as the commit point because
 141         // the synchronization in C11 actually is established at the fence.
 142         /**
 143                 @Begin
 144                 @Commit_point_define_check: true
 145                 @Label: Push_Update_Bottom
 146                 @End
 147         */
 148         atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
 149
 150 }
 151
 152 /**
 153         @Begin
 154         @Interface_define: Steal
 155         @End
 156 */
 157 int steal(Deque *q) {
 158         //Watch out: actually on need to be an acquire (don't count it)
 159         // An old bug
 160         size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
 161         /**
 162                 //@Begin
 163                 @Potential_commit_point_define: true
 164                 @Label: Steal_Potential_Read_Tail
 165                 @End
 166         */
 167         //FIXME: remove the fence causes no error and fewer executions..
 168         atomic_thread_fence(memory_order_seq_cst);
 169         /**** SPEC & UL ****/
 170         size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
 171         /**
 172                 @Begin
 173                 @Commit_point_define_check: true
 174                 @Label: Steal_Read_Bottom
 175                 @End
 176         */
 177
 178         /**
 179                 //@Begin
 180                 @Commit_point_define: t >= b
 181                 @Potential_commit_point_label: Steal_Potential_Read_Tail
 182                 @Label: Steal_Read_Tail
 183                 @End
 184         */
 185         int x = EMPTY;
 186         if (t < b) {
 187                 /* Non-empty queue. */
 188                 /**** detected UL ****/
 189                 Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
 190                 /**
 191                         //@Begin
 192                         @Commit_point_define_check: true
 193                         @Label: Steal_Read_Array
 194                         @End
 195                 */
 196                 int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 197                 x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
 198                 /**
 199                         //@Begin
 200                         @Potential_commit_point_define: true
 201                         @Label: Steal_Potential_Read_Buffer
 202                         @End
 203                 */
 204                 /**** SPEC (sequential) ****/
 205                 bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
 206                         memory_order_seq_cst, memory_order_relaxed);
 207                 /**
 208                         //@Begin
 209                         @Commit_point_define_check: succ
 210                         @Label: Steal_CAS_Top
 211                         @End
 212                 */
 213
 214                 /**
 215                         @Begin
 216                         @Additional_ordering_point_define_check: true
 217                         @Label: Steal_Additional_Point
 218                         @End
 219                 */
 220
 221                 /**
 222                         //@Begin
 223                         @Commit_point_define: succ
 224                         @Potential_commit_point_label: Steal_Potential_Read_Buffer
 225                         @Label: Steal_Read_Buffer
 226                         @End
 227                 */
 228                 if (!succ) {
 229                         /* Failed race. */
 230                         return ABORT;
 231                 }
 232         }
 233         return x;
 234 }