output/spsc-bugfix/queue.h

   1 #ifndef _QUEUE_H
   2 #define _QUEUE_H
   3
   4 #include <unrelacy.h>
   5 #include <atomic>
   6
   7 #include <spec_lib.h>
   8 #include <stdlib.h>
   9 #include <cdsannotate.h>
  10 #include <specannotation.h>
  11 #include <model_memory.h>
  12 #include "common.h"
  13
  14 #include "eventcount.h"
  15
  16
  17 template<typename T>
  18 class spsc_queue
  19 {
  20
  21 public:
  22
  23
  24         spsc_queue()
  25         {
  26
  27         __sequential_init();
  28
  29
  30                 node* n = new node ();
  31                 head = n;
  32                 tail = n;
  33         }
  34
  35         ~spsc_queue()
  36         {
  37                                                 delete ((node*)head);
  38         }
  39
  40 /* All other user-defined structs */
  41 static IntegerList * __queue;
  42 /* All other user-defined functions */
  43 /* Definition of interface info struct: Dequeue */
  44 typedef struct Dequeue_info {
  45 T __RET__;
  46 } Dequeue_info;
  47 /* End of info struct definition: Dequeue */
  48
  49 /* ID function of interface: Dequeue */
  50 inline static call_id_t Dequeue_id(void *info, thread_id_t __TID__) {
  51         Dequeue_info* theInfo = (Dequeue_info*)info;
  52         T __RET__ = theInfo->__RET__;
  53
  54         call_id_t __ID__ = __RET__ ? __RET__ : 0;
  55         return __ID__;
  56 }
  57 /* End of ID function: Dequeue */
  58
  59 /* Check action function of interface: Dequeue */
  60 inline static bool Dequeue_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
  61         bool check_passed;
  62         Dequeue_info* theInfo = (Dequeue_info*)info;
  63         T __RET__ = theInfo->__RET__;
  64
  65         int elem = 0 ;
  66         if ( __RET__ ) {
  67         elem = front ( __queue ) ;
  68         pop_front ( __queue ) ;
  69         }
  70         check_passed = __RET__ ? __RET__ == elem : true;
  71         if (!check_passed)
  72                 return false;
  73         return true;
  74 }
  75 /* End of check action function: Dequeue */
  76
  77 /* Definition of interface info struct: Enqueue */
  78 typedef struct Enqueue_info {
  79 T data;
  80 } Enqueue_info;
  81 /* End of info struct definition: Enqueue */
  82
  83 /* ID function of interface: Enqueue */
  84 inline static call_id_t Enqueue_id(void *info, thread_id_t __TID__) {
  85         Enqueue_info* theInfo = (Enqueue_info*)info;
  86         T data = theInfo->data;
  87
  88         call_id_t __ID__ = data;
  89         return __ID__;
  90 }
  91 /* End of ID function: Enqueue */
  92
  93 /* Check action function of interface: Enqueue */
  94 inline static bool Enqueue_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
  95         bool check_passed;
  96         Enqueue_info* theInfo = (Enqueue_info*)info;
  97         T data = theInfo->data;
  98
  99         push_back ( __queue , data ) ;
 100         return true;
 101 }
 102 /* End of check action function: Enqueue */
 103
 104 #define INTERFACE_SIZE 2
 105 static void** func_ptr_table;
 106 static hb_rule** hb_rule_table;
 107 static commutativity_rule** commutativity_rule_table;
 108 inline static bool CommutativityCondition0(void *info1, void *info2) {
 109         Enqueue_info *_info1 = (Enqueue_info*) info1;
 110         Dequeue_info *_info2 = (Dequeue_info*) info2;
 111         return true;
 112 }
 113 inline static bool CommutativityCondition1(void *info1, void *info2) {
 114         Dequeue_info *_info1 = (Dequeue_info*) info1;
 115         Dequeue_info *_info2 = (Dequeue_info*) info2;
 116         return ! _info1-> __RET__ || ! _info2-> __RET__;
 117 }
 118
 119 /* Initialization of sequential varialbes */
 120 static void __SPEC_INIT__() {
 121         __queue = createIntegerList ( ) ;
 122 }
 123
 124 /* Cleanup routine of sequential variables */
 125 static bool __SPEC_CLEANUP__() {
 126         if ( __queue ) destroyIntegerList ( __queue ) ;
 127         return true ;
 128 }
 129
 130 /* Define function for sequential code initialization */
 131 inline static void __sequential_init() {
 132         /* Init func_ptr_table */
 133         func_ptr_table = (void**) malloc(sizeof(void*) * 2 * 2);
 134         func_ptr_table[2 * 1] = (void*) &Dequeue_id;
 135         func_ptr_table[2 * 1 + 1] = (void*) &Dequeue_check_action;
 136         func_ptr_table[2 * 0] = (void*) &Enqueue_id;
 137         func_ptr_table[2 * 0 + 1] = (void*) &Enqueue_check_action;
 138         /* Enqueue(true) -> Dequeue(true) */
 139         struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
 140         hbConditionInit0->interface_num_before = 0; // Enqueue
 141         hbConditionInit0->hb_condition_num_before = 0; //
 142         hbConditionInit0->interface_num_after = 1; // Dequeue
 143         hbConditionInit0->hb_condition_num_after = 0; //
 144         /* Init hb_rule_table */
 145         hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 1);
 146         #define HB_RULE_TABLE_SIZE 1
 147         hb_rule_table[0] = hbConditionInit0;
 148         /* Init commutativity_rule_table */
 149         commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 2);
 150         commutativity_rule* rule;
 151         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 152         rule->interface_num_before = 0;
 153         rule->interface_num_after = 1;
 154         rule->rule = "true";
 155         rule->condition = CommutativityCondition0;
 156         commutativity_rule_table[0] = rule;
 157         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 158         rule->interface_num_before = 1;
 159         rule->interface_num_after = 1;
 160         rule->rule = "! _Method1 . __RET__ || ! _Method2 . __RET__";
 161         rule->condition = CommutativityCondition1;
 162         commutativity_rule_table[1] = rule;
 163         /* Pass init info, including function table info & HB rules & Commutativity Rules */
 164         struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
 165         anno_init->init_func = (void_func_t) __SPEC_INIT__;
 166         anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
 167         anno_init->func_table = func_ptr_table;
 168         anno_init->func_table_size = INTERFACE_SIZE;
 169         anno_init->hb_rule_table = hb_rule_table;
 170         anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
 171         anno_init->commutativity_rule_table = commutativity_rule_table;
 172         anno_init->commutativity_rule_table_size = 2;
 173         struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 174         init->type = INIT;
 175         init->annotation = anno_init;
 176         cdsannotate(SPEC_ANALYSIS, init);
 177
 178 }
 179
 180 /* End of Global construct generation in class */
 181
 182
 183
 184
 185 void enqueue(T data) {
 186         /* Interface begins */
 187         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 188         interface_begin->interface_num = 0; // Enqueue
 189                 interface_begin->interface_name = "Enqueue";
 190         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 191         annotation_interface_begin->type = INTERFACE_BEGIN;
 192         annotation_interface_begin->annotation = interface_begin;
 193         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 194         __wrapper__enqueue(data);
 195         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 196         hb_condition->interface_num = 0; // Enqueue
 197         hb_condition->hb_condition_num = 0;
 198         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 199         annotation_hb_condition->type = HB_CONDITION;
 200         annotation_hb_condition->annotation = hb_condition;
 201         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 202
 203         Enqueue_info* info = (Enqueue_info*) malloc(sizeof(Enqueue_info));
 204         info->data = data;
 205         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 206         interface_end->interface_num = 0; // Enqueue
 207         interface_end->info = info;
 208         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 209         annoation_interface_end->type = INTERFACE_END;
 210         annoation_interface_end->annotation = interface_end;
 211         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 212 }
 213
 214 void __wrapper__enqueue(T data)
 215         {
 216                 node* n = new node (data);
 217
 218                                 head->next.store(n, std::memory_order_release);
 219         /* Automatically generated code for commit point define check: Enqueue_Point */
 220
 221         if (true) {
 222                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 223                 cp_define_check->label_num = 0;
 224                 cp_define_check->label_name = "Enqueue_Point";
 225                 cp_define_check->interface_num = 0;
 226                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 227                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 228                 annotation_cp_define_check->annotation = cp_define_check;
 229                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 230         }
 231
 232                 head = n;
 233                                 ec.signal();
 234         }
 235
 236 T dequeue() {
 237         /* Interface begins */
 238         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 239         interface_begin->interface_num = 1; // Dequeue
 240                 interface_begin->interface_name = "Dequeue";
 241         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 242         annotation_interface_begin->type = INTERFACE_BEGIN;
 243         annotation_interface_begin->annotation = interface_begin;
 244         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 245         T __RET__ = __wrapper__dequeue();
 246         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 247         hb_condition->interface_num = 1; // Dequeue
 248         hb_condition->hb_condition_num = 0;
 249         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 250         annotation_hb_condition->type = HB_CONDITION;
 251         annotation_hb_condition->annotation = hb_condition;
 252         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 253
 254         Dequeue_info* info = (Dequeue_info*) malloc(sizeof(Dequeue_info));
 255         info->__RET__ = __RET__;
 256         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 257         interface_end->interface_num = 1; // Dequeue
 258         interface_end->info = info;
 259         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 260         annoation_interface_end->type = INTERFACE_END;
 261         annoation_interface_end->annotation = interface_end;
 262         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 263         return __RET__;
 264 }
 265
 266 T __wrapper__dequeue()
 267         {
 268                 T data = try_dequeue();
 269                 while (0 == data)
 270                 {
 271                         int cmp = ec.get();
 272                         data = try_dequeue();
 273                         if (data)
 274                                 break;
 275                         ec.wait(cmp);
 276                         data = try_dequeue();
 277                         if (data)
 278                                 break;
 279                 }
 280                 return data;
 281         }
 282
 283 private:
 284         struct node
 285         {
 286                 std::atomic<node*> next;
 287                                 T data;
 288
 289                 node(T data = T())
 290                         : data(data)
 291                 {
 292                         next = 0;
 293                 }
 294         };
 295
 296                         node *head;
 297         node *tail;
 298
 299
 300
 301         eventcount ec;
 302
 303         T try_dequeue()
 304         {
 305                                 node *t = tail;
 306
 307                 node* n = t->next.load(std::memory_order_acquire);
 308         /* Automatically generated code for commit point define check: Dequeue_Point */
 309
 310         if (n != 0) {
 311                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 312                 cp_define_check->label_num = 1;
 313                 cp_define_check->label_name = "Dequeue_Point";
 314                 cp_define_check->interface_num = 1;
 315                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 316                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 317                 annotation_cp_define_check->annotation = cp_define_check;
 318                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 319         }
 320
 321                 if (0 == n)
 322                         return 0;
 323                                 T data = n->data;
 324                 delete (t);
 325                 tail = n;
 326                 return data;
 327         }
 328 };
 329 template<typename T>
 330 void** spsc_queue<T>::func_ptr_table;
 331 template<typename T>
 332 hb_rule** spsc_queue<T>::hb_rule_table;
 333 template<typename T>
 334 commutativity_rule** spsc_queue<T>::commutativity_rule_table;
 335 template<typename T>
 336 IntegerList * spsc_queue<T>::__queue;
 337
 338
 339 #endif
 340