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         //FIXME: remove the fence causes no error and fewer executions..
 162         atomic_thread_fence(memory_order_seq_cst);
 163         /**** SPEC & UL ****/
 164         size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
 165         /**
 166                 @Begin
 167                 @Commit_point_define_check: true
 168                 @Label: Steal_Read_Bottom
 169                 @End
 170         */
 171         int x = EMPTY;
 172         if (t < b) {
 173                 /* Non-empty queue. */
 174                 /**** detected UL ****/
 175                 Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
 176                 int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 177                 x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
 178                 /**** SPEC (sequential) ****/
 179                 bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
 180                         memory_order_seq_cst, memory_order_relaxed);
 181                 /**
 182                         @Begin
 183                         @Additional_ordering_point_define_check: true
 184                         @Label: Steal_Additional_Point
 185                         @End
 186                 */
 187                 if (!succ) {
 188                         /* Failed race. */
 189                         return ABORT;
 190                 }
 191         }
 192         return x;
 193 }