output/ms-queue/my_queue.c

   1 #include <threads.h>
   2 #include <stdlib.h>
   3 #include "librace.h"
   4 #include "model-assert.h"
   5
   6 #include "my_queue.h"
   7
   8 #define relaxed memory_order_relaxed
   9 #define release memory_order_release
  10 #define acquire memory_order_acquire
  11
  12 #define MAX_FREELIST 4
  13 #define INITIAL_FREE 3
  14
  15 #define POISON_IDX 0x666
  16
  17 static unsigned int (*free_lists)[MAX_FREELIST];
  18
  19
  20 static unsigned int new_node()
  21 {
  22         int i;
  23         int t = get_thread_num();
  24         for (i = 0; i < MAX_FREELIST; i++) {
  25                                 unsigned int node = free_lists[t][i];
  26                 if (node) {
  27                                                 free_lists[t][i] = 0;
  28                         return node;
  29                 }
  30         }
  31
  32                 return 0;
  33 }
  34
  35
  36 static void reclaim(unsigned int node)
  37 {
  38         int i;
  39         int t = get_thread_num();
  40
  41
  42
  43         for (i = 0; i < MAX_FREELIST; i++) {
  44
  45                                 unsigned int idx = free_lists[t][i];
  46
  47
  48                 if (idx == 0) {
  49                         store_32(&free_lists[t][i], node);
  50                                                 return;
  51                 }
  52         }
  53
  54         }
  55
  56 void init_queue(queue_t *q, int num_threads)
  57 {
  58         int i, j;
  59         for (i = 0; i < MAX_NODES; i++) {
  60                 atomic_init(&q->nodes[i].next, MAKE_POINTER(POISON_IDX, 0));
  61         }
  62
  63
  64
  65         free_lists = malloc(num_threads * sizeof(*free_lists));
  66         for (i = 0; i < num_threads; i++) {
  67                 for (j = 0; j < INITIAL_FREE; j++) {
  68                         free_lists[i][j] = 2 + i * MAX_FREELIST + j;
  69                         atomic_init(&q->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0));
  70                 }
  71         }
  72
  73
  74         atomic_init(&q->head, MAKE_POINTER(1, 0));
  75         atomic_init(&q->tail, MAKE_POINTER(1, 0));
  76         atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0));
  77 }
  78
  79
  80 void enqueue(queue_t * q,  unsigned int val) {
  81         /* Interface begins */
  82         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
  83         interface_begin->interface_num = 0; // Enqueue
  84                 interface_begin->interface_name = "Enqueue";
  85         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
  86         annotation_interface_begin->type = INTERFACE_BEGIN;
  87         annotation_interface_begin->annotation = interface_begin;
  88         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
  89         __wrapper__enqueue(q, val);
  90         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
  91         hb_condition->interface_num = 0; // Enqueue
  92         hb_condition->hb_condition_num = 0;
  93         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
  94         annotation_hb_condition->type = HB_CONDITION;
  95         annotation_hb_condition->annotation = hb_condition;
  96         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
  97
  98         Enqueue_info* info = (Enqueue_info*) malloc(sizeof(Enqueue_info));
  99         info->q = q;
 100         info->val = val;
 101         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 102         interface_end->interface_num = 0; // Enqueue
 103         interface_end->info = info;
 104         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 105         annoation_interface_end->type = INTERFACE_END;
 106         annoation_interface_end->annotation = interface_end;
 107         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 108 }
 109
 110 void __wrapper__enqueue(queue_t * q,  unsigned int val)
 111 {
 112         int success = 0;
 113         unsigned int node;
 114         pointer tail;
 115         pointer next;
 116         pointer tmp;
 117
 118         node = new_node();
 119                 q->nodes[node].value = val;
 120         tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
 121         set_ptr(&tmp, 0);       atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
 122
 123         while (!success) {
 124
 125         /* Automatically generated code for commit point clear: Enqueue_Clear */
 126
 127         if (true) {
 128                 struct anno_cp_clear *cp_clear = (struct anno_cp_clear*) malloc(sizeof(struct anno_cp_clear));
 129                 cp_clear->label_name = "Enqueue_Clear";
 130                 cp_clear->label_num = 0;
 131                 struct spec_annotation *annotation_cp_clear = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 132                 annotation_cp_clear->type = CP_CLEAR;
 133                 annotation_cp_clear->annotation = cp_clear;
 134                 cdsannotate(SPEC_ANALYSIS, annotation_cp_clear);
 135         }
 136
 137
 138                 tail = atomic_load_explicit(&q->tail, acquire);
 139
 140                 next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
 141                                 if (tail == atomic_load_explicit(&q->tail, relaxed)) {
 142
 143
 144
 145                         if (get_ptr(next) == 0) {                               pointer value = MAKE_POINTER(node, get_count(next) + 1);
 146
 147                                                                 success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
 148                                                 &next, value, release, relaxed);
 149         /* Automatically generated code for commit point define check: EnqueueUpdateNext */
 150
 151         if (success) {
 152                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 153                 cp_define_check->label_num = 1;
 154                 cp_define_check->label_name = "EnqueueUpdateNext";
 155                 cp_define_check->interface_num = 0;
 156                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 157                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 158                 annotation_cp_define_check->annotation = cp_define_check;
 159                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 160         }
 161
 162                         }
 163                         if (!success) {
 164
 165                                 unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
 166                                 pointer value = MAKE_POINTER(ptr,
 167                                                 get_count(tail) + 1);
 168
 169                                                                 bool succ = false;
 170                                 succ = atomic_compare_exchange_strong_explicit(&q->tail,
 171                                                 &tail, value, relaxed, relaxed);
 172                                 if (succ) {
 173                                                                         }
 174                                                                 thrd_yield();
 175                         }
 176                 }
 177         }
 178
 179                 bool succ = atomic_compare_exchange_strong_explicit(&q->tail,
 180                         &tail,
 181                         MAKE_POINTER(node, get_count(tail) + 1),
 182                         release, relaxed);
 183 }
 184
 185
 186 bool dequeue(queue_t * q, int * retVal) {
 187         /* Interface begins */
 188         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 189         interface_begin->interface_num = 1; // Dequeue
 190                 interface_begin->interface_name = "Dequeue";
 191         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 192         annotation_interface_begin->type = INTERFACE_BEGIN;
 193         annotation_interface_begin->annotation = interface_begin;
 194         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 195         bool __RET__ = __wrapper__dequeue(q, retVal);
 196         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 197         hb_condition->interface_num = 1; // Dequeue
 198         hb_condition->hb_condition_num = 0;
 199         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 200         annotation_hb_condition->type = HB_CONDITION;
 201         annotation_hb_condition->annotation = hb_condition;
 202         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 203
 204         Dequeue_info* info = (Dequeue_info*) malloc(sizeof(Dequeue_info));
 205         info->__RET__ = __RET__;
 206         info->q = q;
 207         info->retVal = retVal;
 208         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 209         interface_end->interface_num = 1; // Dequeue
 210         interface_end->info = info;
 211         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 212         annoation_interface_end->type = INTERFACE_END;
 213         annoation_interface_end->annotation = interface_end;
 214         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 215         return __RET__;
 216 }
 217
 218 bool __wrapper__dequeue(queue_t * q, int * retVal)
 219 {
 220         unsigned int value = 0;
 221         int success = 0;
 222         pointer head;
 223         pointer tail;
 224         pointer next;
 225
 226         while (!success) {
 227         /* Automatically generated code for commit point clear: Dequeue_Clear */
 228
 229         if (true) {
 230                 struct anno_cp_clear *cp_clear = (struct anno_cp_clear*) malloc(sizeof(struct anno_cp_clear));
 231                 cp_clear->label_name = "Dequeue_Clear";
 232                 cp_clear->label_num = 2;
 233                 struct spec_annotation *annotation_cp_clear = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 234                 annotation_cp_clear->type = CP_CLEAR;
 235                 annotation_cp_clear->annotation = cp_clear;
 236                 cdsannotate(SPEC_ANALYSIS, annotation_cp_clear);
 237         }
 238
 239
 240                 head = atomic_load_explicit(&q->head, acquire);
 241         /* Automatically generated code for commit point define check: DequeueReadHead */
 242
 243         if (true) {
 244                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 245                 cp_define_check->label_num = 3;
 246                 cp_define_check->label_name = "DequeueReadHead";
 247                 cp_define_check->interface_num = 1;
 248                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 249                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 250                 annotation_cp_define_check->annotation = cp_define_check;
 251                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 252         }
 253
 254
 255
 256
 257                 tail = atomic_load_explicit(&q->tail, acquire);
 258
 259
 260                 next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
 261         /* Automatically generated code for potential commit point: DequeueReadNext */
 262
 263         if (true) {
 264                 struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
 265                 potential_cp_define->label_num = 4;
 266                 potential_cp_define->label_name = "DequeueReadNext";
 267                 struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 268                 annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
 269                 annotation_potential_cp_define->annotation = potential_cp_define;
 270                 cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
 271         }
 272
 273                 if (atomic_load_explicit(&q->head, relaxed) == head) {
 274                         if (get_ptr(head) == get_ptr(tail)) {
 275
 276
 277
 278                                 if (get_ptr(next) == 0) {                                       return false;                           }
 279
 280                                                                 bool succ = false;
 281                                 succ = atomic_compare_exchange_strong_explicit(&q->tail,
 282                                                 &tail,
 283                                                 MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
 284                                                         release, relaxed);
 285                                 if (succ) {
 286                                                                         }
 287                                                                 thrd_yield();
 288                         } else {
 289                                                                 value = q->nodes[get_ptr(next)].value;
 290
 291                                 success = atomic_compare_exchange_strong_explicit(&q->head,
 292                                                 &head,
 293                                                 MAKE_POINTER(get_ptr(next), get_count(head) + 1),
 294                                                 release, relaxed);
 295         /* Automatically generated code for commit point define check: DequeueUpdateHead */
 296
 297         if (success) {
 298                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 299                 cp_define_check->label_num = 5;
 300                 cp_define_check->label_name = "DequeueUpdateHead";
 301                 cp_define_check->interface_num = 1;
 302                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 303                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 304                 annotation_cp_define_check->annotation = cp_define_check;
 305                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 306         }
 307
 308
 309         /* Automatically generated code for commit point define: DequeueReadNextVerify */
 310
 311         if (success) {
 312                 struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
 313                 cp_define->label_num = 6;
 314                 cp_define->label_name = "DequeueReadNextVerify";
 315                 cp_define->potential_cp_label_num = 4;
 316                 cp_define->potential_label_name = "DequeueReadNext";
 317                 cp_define->interface_num = 1;
 318                 struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 319                 annotation_cp_define->type = CP_DEFINE;
 320                 annotation_cp_define->annotation = cp_define;
 321                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
 322         }
 323
 324                                 if (!success)
 325                                         thrd_yield();
 326                         }
 327                 }
 328         }
 329         reclaim(get_ptr(head));
 330         *retVal = value;
 331         return true;
 332 }
 333