output/mpmc-queue/mpmc-queue.h

   1 #include <stdatomic.h>
   2 #include <unrelacy.h>
   3 #include <common.h>
   4
   5 #include <spec_lib.h>
   6 #include <stdlib.h>
   7 #include <cdsannotate.h>
   8 #include <specannotation.h>
   9 #include <model_memory.h>
  10
  11
  12 template <typename t_element, size_t t_size>
  13 struct mpmc_boundq_1_alt
  14 {
  15 private:
  16
  17         unsigned int MASK;
  18
  19                 t_element               m_array[t_size];
  20
  21                 atomic<unsigned int>    m_rdwr;
  22                 atomic<unsigned int>    m_read;
  23         atomic<unsigned int>    m_written;
  24
  25 public:
  26
  27         mpmc_boundq_1_alt()
  28         {
  29         __sequential_init();
  30
  31                 m_rdwr = 0;
  32                 m_read = 0;
  33                 m_written = 0;
  34                                 MASK = 0x1;     }
  35
  36
  37 /* All other user-defined structs */
  38 /* All other user-defined functions */
  39 /* Definition of interface info struct: Publish */
  40 typedef struct Publish_info {
  41 t_element * bin;
  42 } Publish_info;
  43 /* End of info struct definition: Publish */
  44
  45 /* ID function of interface: Publish */
  46 inline static call_id_t Publish_id(void *info, thread_id_t __TID__) {
  47         Publish_info* theInfo = (Publish_info*)info;
  48         t_element * bin = theInfo->bin;
  49
  50         call_id_t __ID__ = ( call_id_t ) bin;
  51         return __ID__;
  52 }
  53 /* End of ID function: Publish */
  54
  55 /* Check action function of interface: Publish */
  56 inline static bool Publish_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
  57         bool check_passed;
  58         Publish_info* theInfo = (Publish_info*)info;
  59         t_element * bin = theInfo->bin;
  60
  61         return true;
  62 }
  63 /* End of check action function: Publish */
  64
  65 /* Definition of interface info struct: Fetch */
  66 typedef struct Fetch_info {
  67 t_element * __RET__;
  68 } Fetch_info;
  69 /* End of info struct definition: Fetch */
  70
  71 /* ID function of interface: Fetch */
  72 inline static call_id_t Fetch_id(void *info, thread_id_t __TID__) {
  73         Fetch_info* theInfo = (Fetch_info*)info;
  74         t_element * __RET__ = theInfo->__RET__;
  75
  76         call_id_t __ID__ = ( call_id_t ) __RET__;
  77         return __ID__;
  78 }
  79 /* End of ID function: Fetch */
  80
  81 /* Check action function of interface: Fetch */
  82 inline static bool Fetch_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
  83         bool check_passed;
  84         Fetch_info* theInfo = (Fetch_info*)info;
  85         t_element * __RET__ = theInfo->__RET__;
  86
  87         return true;
  88 }
  89 /* End of check action function: Fetch */
  90
  91 /* Definition of interface info struct: Prepare */
  92 typedef struct Prepare_info {
  93 t_element * __RET__;
  94 } Prepare_info;
  95 /* End of info struct definition: Prepare */
  96
  97 /* ID function of interface: Prepare */
  98 inline static call_id_t Prepare_id(void *info, thread_id_t __TID__) {
  99         Prepare_info* theInfo = (Prepare_info*)info;
 100         t_element * __RET__ = theInfo->__RET__;
 101
 102         call_id_t __ID__ = ( call_id_t ) __RET__;
 103         return __ID__;
 104 }
 105 /* End of ID function: Prepare */
 106
 107 /* Check action function of interface: Prepare */
 108 inline static bool Prepare_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
 109         bool check_passed;
 110         Prepare_info* theInfo = (Prepare_info*)info;
 111         t_element * __RET__ = theInfo->__RET__;
 112
 113         return true;
 114 }
 115 /* End of check action function: Prepare */
 116
 117 /* Definition of interface info struct: Consume */
 118 typedef struct Consume_info {
 119 t_element * bin;
 120 } Consume_info;
 121 /* End of info struct definition: Consume */
 122
 123 /* ID function of interface: Consume */
 124 inline static call_id_t Consume_id(void *info, thread_id_t __TID__) {
 125         Consume_info* theInfo = (Consume_info*)info;
 126         t_element * bin = theInfo->bin;
 127
 128         call_id_t __ID__ = ( call_id_t ) bin;
 129         return __ID__;
 130 }
 131 /* End of ID function: Consume */
 132
 133 /* Check action function of interface: Consume */
 134 inline static bool Consume_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
 135         bool check_passed;
 136         Consume_info* theInfo = (Consume_info*)info;
 137         t_element * bin = theInfo->bin;
 138
 139         return true;
 140 }
 141 /* End of check action function: Consume */
 142
 143 #define INTERFACE_SIZE 4
 144 static void** func_ptr_table;
 145 static hb_rule** hb_rule_table;
 146 static commutativity_rule** commutativity_rule_table;
 147 inline static bool CommutativityCondition0(void *info1, void *info2) {
 148         Prepare_info *_info1 = (Prepare_info*) info1;
 149         Prepare_info *_info2 = (Prepare_info*) info2;
 150         return _info1-> __RET__ != _info2-> __RET__ || ! _info1-> __RET__ || ! _info2-> __RET__;
 151 }
 152 inline static bool CommutativityCondition1(void *info1, void *info2) {
 153         Prepare_info *_info1 = (Prepare_info*) info1;
 154         Publish_info *_info2 = (Publish_info*) info2;
 155         return _info1-> __RET__ != _info2-> bin || ! _info1-> __RET__;
 156 }
 157 inline static bool CommutativityCondition2(void *info1, void *info2) {
 158         Prepare_info *_info1 = (Prepare_info*) info1;
 159         Fetch_info *_info2 = (Fetch_info*) info2;
 160         return _info1-> __RET__ != _info2-> __RET__ || ! _info1-> __RET__ || ! _info2-> __RET__;
 161 }
 162 inline static bool CommutativityCondition3(void *info1, void *info2) {
 163         Prepare_info *_info1 = (Prepare_info*) info1;
 164         Consume_info *_info2 = (Consume_info*) info2;
 165         return _info1-> __RET__ != _info2-> bin || ! _info1-> __RET__;
 166 }
 167 inline static bool CommutativityCondition4(void *info1, void *info2) {
 168         Publish_info *_info1 = (Publish_info*) info1;
 169         Publish_info *_info2 = (Publish_info*) info2;
 170         return _info1-> bin != _info2-> bin;
 171 }
 172 inline static bool CommutativityCondition5(void *info1, void *info2) {
 173         Publish_info *_info1 = (Publish_info*) info1;
 174         Fetch_info *_info2 = (Fetch_info*) info2;
 175         return _info1-> bin != _info2-> __RET__ || ! _info2-> __RET__;
 176 }
 177 inline static bool CommutativityCondition6(void *info1, void *info2) {
 178         Publish_info *_info1 = (Publish_info*) info1;
 179         Consume_info *_info2 = (Consume_info*) info2;
 180         return _info1-> bin != _info2-> bin;
 181 }
 182 inline static bool CommutativityCondition7(void *info1, void *info2) {
 183         Fetch_info *_info1 = (Fetch_info*) info1;
 184         Fetch_info *_info2 = (Fetch_info*) info2;
 185         return _info1-> __RET__ != _info2-> __RET__ || ! _info1-> __RET__ || ! _info2-> __RET__;
 186 }
 187 inline static bool CommutativityCondition8(void *info1, void *info2) {
 188         Fetch_info *_info1 = (Fetch_info*) info1;
 189         Consume_info *_info2 = (Consume_info*) info2;
 190         return _info1-> __RET__ != _info2-> bin || ! _info1-> __RET__;
 191 }
 192 inline static bool CommutativityCondition9(void *info1, void *info2) {
 193         Consume_info *_info1 = (Consume_info*) info1;
 194         Consume_info *_info2 = (Consume_info*) info2;
 195         return _info1-> bin != _info2-> bin;
 196 }
 197
 198 /* Initialization of sequential varialbes */
 199 static void __SPEC_INIT__() {
 200 }
 201
 202 /* Cleanup routine of sequential variables */
 203 static bool __SPEC_CLEANUP__() {
 204         return true;
 205 }
 206
 207 /* Define function for sequential code initialization */
 208 inline static void __sequential_init() {
 209         /* Init func_ptr_table */
 210         func_ptr_table = (void**) malloc(sizeof(void*) * 4 * 2);
 211         func_ptr_table[2 * 3] = (void*) &Publish_id;
 212         func_ptr_table[2 * 3 + 1] = (void*) &Publish_check_action;
 213         func_ptr_table[2 * 0] = (void*) &Fetch_id;
 214         func_ptr_table[2 * 0 + 1] = (void*) &Fetch_check_action;
 215         func_ptr_table[2 * 2] = (void*) &Prepare_id;
 216         func_ptr_table[2 * 2 + 1] = (void*) &Prepare_check_action;
 217         func_ptr_table[2 * 1] = (void*) &Consume_id;
 218         func_ptr_table[2 * 1 + 1] = (void*) &Consume_check_action;
 219         /* Consume(true) -> Prepare(true) */
 220         struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
 221         hbConditionInit0->interface_num_before = 1; // Consume
 222         hbConditionInit0->hb_condition_num_before = 0; //
 223         hbConditionInit0->interface_num_after = 2; // Prepare
 224         hbConditionInit0->hb_condition_num_after = 0; //
 225         /* Publish(true) -> Fetch(true) */
 226         struct hb_rule *hbConditionInit1 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
 227         hbConditionInit1->interface_num_before = 3; // Publish
 228         hbConditionInit1->hb_condition_num_before = 0; //
 229         hbConditionInit1->interface_num_after = 0; // Fetch
 230         hbConditionInit1->hb_condition_num_after = 0; //
 231         /* Init hb_rule_table */
 232         hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 2);
 233         #define HB_RULE_TABLE_SIZE 2
 234         hb_rule_table[0] = hbConditionInit0;
 235         hb_rule_table[1] = hbConditionInit1;
 236         /* Init commutativity_rule_table */
 237         commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 10);
 238         commutativity_rule* rule;
 239         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 240         rule->interface_num_before = 2;
 241         rule->interface_num_after = 2;
 242         rule->rule = "_Method1 . __RET__ != _Method2 . __RET__ || ! _Method1 . __RET__ || ! _Method2 . __RET__";
 243         rule->condition = CommutativityCondition0;
 244         commutativity_rule_table[0] = rule;
 245         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 246         rule->interface_num_before = 2;
 247         rule->interface_num_after = 3;
 248         rule->rule = "_Method1 . __RET__ != _Method2 . bin || ! _Method1 . __RET__";
 249         rule->condition = CommutativityCondition1;
 250         commutativity_rule_table[1] = rule;
 251         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 252         rule->interface_num_before = 2;
 253         rule->interface_num_after = 0;
 254         rule->rule = "_Method1 . __RET__ != _Method2 . __RET__ || ! _Method1 . __RET__ || ! _Method2 . __RET__";
 255         rule->condition = CommutativityCondition2;
 256         commutativity_rule_table[2] = rule;
 257         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 258         rule->interface_num_before = 2;
 259         rule->interface_num_after = 1;
 260         rule->rule = "_Method1 . __RET__ != _Method2 . bin || ! _Method1 . __RET__";
 261         rule->condition = CommutativityCondition3;
 262         commutativity_rule_table[3] = rule;
 263         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 264         rule->interface_num_before = 3;
 265         rule->interface_num_after = 3;
 266         rule->rule = "_Method1 . bin != _Method2 . bin";
 267         rule->condition = CommutativityCondition4;
 268         commutativity_rule_table[4] = rule;
 269         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 270         rule->interface_num_before = 3;
 271         rule->interface_num_after = 0;
 272         rule->rule = "_Method1 . bin != _Method2 . __RET__ || ! _Method2 . __RET__";
 273         rule->condition = CommutativityCondition5;
 274         commutativity_rule_table[5] = rule;
 275         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 276         rule->interface_num_before = 3;
 277         rule->interface_num_after = 1;
 278         rule->rule = "_Method1 . bin != _Method2 . bin";
 279         rule->condition = CommutativityCondition6;
 280         commutativity_rule_table[6] = rule;
 281         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 282         rule->interface_num_before = 0;
 283         rule->interface_num_after = 0;
 284         rule->rule = "_Method1 . __RET__ != _Method2 . __RET__ || ! _Method1 . __RET__ || ! _Method2 . __RET__";
 285         rule->condition = CommutativityCondition7;
 286         commutativity_rule_table[7] = rule;
 287         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 288         rule->interface_num_before = 0;
 289         rule->interface_num_after = 1;
 290         rule->rule = "_Method1 . __RET__ != _Method2 . bin || ! _Method1 . __RET__";
 291         rule->condition = CommutativityCondition8;
 292         commutativity_rule_table[8] = rule;
 293         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 294         rule->interface_num_before = 1;
 295         rule->interface_num_after = 1;
 296         rule->rule = "_Method1 . bin != _Method2 . bin";
 297         rule->condition = CommutativityCondition9;
 298         commutativity_rule_table[9] = rule;
 299         /* Pass init info, including function table info & HB rules & Commutativity Rules */
 300         struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
 301         anno_init->init_func = (void_func_t) __SPEC_INIT__;
 302         anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
 303         anno_init->func_table = func_ptr_table;
 304         anno_init->func_table_size = INTERFACE_SIZE;
 305         anno_init->hb_rule_table = hb_rule_table;
 306         anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
 307         anno_init->commutativity_rule_table = commutativity_rule_table;
 308         anno_init->commutativity_rule_table_size = 10;
 309         struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 310         init->type = INIT;
 311         init->annotation = anno_init;
 312         cdsannotate(SPEC_ANALYSIS, init);
 313
 314 }
 315
 316 /* End of Global construct generation in class */
 317
 318
 319
 320
 321 t_element * read_fetch() {
 322         /* Interface begins */
 323         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 324         interface_begin->interface_num = 0; // Fetch
 325                 interface_begin->interface_name = "Fetch";
 326         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 327         annotation_interface_begin->type = INTERFACE_BEGIN;
 328         annotation_interface_begin->annotation = interface_begin;
 329         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 330         t_element * __RET__ = __wrapper__read_fetch();
 331         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 332         hb_condition->interface_num = 0; // Fetch
 333         hb_condition->hb_condition_num = 0;
 334         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 335         annotation_hb_condition->type = HB_CONDITION;
 336         annotation_hb_condition->annotation = hb_condition;
 337         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 338
 339         Fetch_info* info = (Fetch_info*) malloc(sizeof(Fetch_info));
 340         info->__RET__ = __RET__;
 341         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 342         interface_end->interface_num = 0; // Fetch
 343         interface_end->info = info;
 344         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 345         annoation_interface_end->type = INTERFACE_END;
 346         annoation_interface_end->annotation = interface_end;
 347         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 348         return __RET__;
 349 }
 350
 351 t_element * __wrapper__read_fetch() {
 352                                 unsigned int rdwr = m_rdwr.load(mo_acquire);
 353         /* Automatically generated code for potential commit point: Fetch_Potential_RW_Load */
 354
 355         if (true) {
 356                 struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
 357                 potential_cp_define->label_num = 0;
 358                 potential_cp_define->label_name = "Fetch_Potential_RW_Load";
 359                 struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 360                 annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
 361                 annotation_potential_cp_define->annotation = potential_cp_define;
 362                 cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
 363         }
 364
 365                 unsigned int rd,wr;
 366                 for(;;) {
 367                         rd = (rdwr>>16) & MASK;
 368                         wr = rdwr & MASK;
 369
 370                         if ( wr == rd ) {
 371         /* Automatically generated code for commit point define: Fetch_RW_Load_Empty */
 372
 373         if (true) {
 374                 struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
 375                 cp_define->label_num = 1;
 376                 cp_define->label_name = "Fetch_RW_Load_Empty";
 377                 cp_define->potential_cp_label_num = 0;
 378                 cp_define->potential_label_name = "Fetch_Potential_RW_Load";
 379                 cp_define->interface_num = 0;
 380                 struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 381                 annotation_cp_define->type = CP_DEFINE;
 382                 annotation_cp_define->annotation = cp_define;
 383                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
 384         }
 385
 386
 387                                 return false;
 388                         }
 389
 390
 391                         bool succ =
 392                         m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
 393         /* Automatically generated code for commit point define check: Fetch_RW_RMW */
 394
 395         if (succ) {
 396                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 397                 cp_define_check->label_num = 2;
 398                 cp_define_check->label_name = "Fetch_RW_RMW";
 399                 cp_define_check->interface_num = 0;
 400                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 401                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 402                 annotation_cp_define_check->annotation = cp_define_check;
 403                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 404         }
 405
 406                         if (succ)
 407                                 break;
 408                         else
 409                                 thrd_yield();
 410                 }
 411
 412                                 rl::backoff bo;
 413                 while (true) {
 414
 415                         int written = m_written.load(mo_acquire);
 416         /* Automatically generated code for potential commit point: Fetch_Potential_W_Load */
 417
 418         if (true) {
 419                 struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
 420                 potential_cp_define->label_num = 3;
 421                 potential_cp_define->label_name = "Fetch_Potential_W_Load";
 422                 struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 423                 annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
 424                 annotation_potential_cp_define->annotation = potential_cp_define;
 425                 cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
 426         }
 427
 428                         if ((written & MASK) != wr) {
 429                                 thrd_yield();
 430                         } else {
 431                                 printf("Fetch: m_written=%d\n", written);
 432                                 break;
 433                         }
 434                 }
 435
 436         /* Automatically generated code for commit point define: Fetch_W_Load */
 437
 438         if (true) {
 439                 struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
 440                 cp_define->label_num = 4;
 441                 cp_define->label_name = "Fetch_W_Load";
 442                 cp_define->potential_cp_label_num = 3;
 443                 cp_define->potential_label_name = "Fetch_Potential_W_Load";
 444                 cp_define->interface_num = 0;
 445                 struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 446                 annotation_cp_define->type = CP_DEFINE;
 447                 annotation_cp_define->annotation = cp_define;
 448                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
 449         }
 450
 451
 452                 t_element * p = & ( m_array[ rd % t_size ] );
 453
 454                 return p;
 455         }
 456
 457
 458 void read_consume(t_element * bin) {
 459         /* Interface begins */
 460         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 461         interface_begin->interface_num = 1; // Consume
 462                 interface_begin->interface_name = "Consume";
 463         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 464         annotation_interface_begin->type = INTERFACE_BEGIN;
 465         annotation_interface_begin->annotation = interface_begin;
 466         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 467         __wrapper__read_consume(bin);
 468         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 469         hb_condition->interface_num = 1; // Consume
 470         hb_condition->hb_condition_num = 0;
 471         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 472         annotation_hb_condition->type = HB_CONDITION;
 473         annotation_hb_condition->annotation = hb_condition;
 474         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 475
 476         Consume_info* info = (Consume_info*) malloc(sizeof(Consume_info));
 477         info->bin = bin;
 478         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 479         interface_end->interface_num = 1; // Consume
 480         interface_end->info = info;
 481         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 482         annoation_interface_end->type = INTERFACE_END;
 483         annoation_interface_end->annotation = interface_end;
 484         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 485 }
 486
 487 void __wrapper__read_consume(t_element * bin) {
 488
 489                 m_read.fetch_add(1,mo_release);
 490         /* Automatically generated code for commit point define check: Consume_R_RMW */
 491
 492         if (true) {
 493                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 494                 cp_define_check->label_num = 5;
 495                 cp_define_check->label_name = "Consume_R_RMW";
 496                 cp_define_check->interface_num = 1;
 497                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 498                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 499                 annotation_cp_define_check->annotation = cp_define_check;
 500                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 501         }
 502
 503         }
 504
 505
 506
 507 t_element * write_prepare() {
 508         /* Interface begins */
 509         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 510         interface_begin->interface_num = 2; // Prepare
 511                 interface_begin->interface_name = "Prepare";
 512         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 513         annotation_interface_begin->type = INTERFACE_BEGIN;
 514         annotation_interface_begin->annotation = interface_begin;
 515         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 516         t_element * __RET__ = __wrapper__write_prepare();
 517         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 518         hb_condition->interface_num = 2; // Prepare
 519         hb_condition->hb_condition_num = 0;
 520         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 521         annotation_hb_condition->type = HB_CONDITION;
 522         annotation_hb_condition->annotation = hb_condition;
 523         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 524
 525         Prepare_info* info = (Prepare_info*) malloc(sizeof(Prepare_info));
 526         info->__RET__ = __RET__;
 527         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 528         interface_end->interface_num = 2; // Prepare
 529         interface_end->info = info;
 530         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 531         annoation_interface_end->type = INTERFACE_END;
 532         annoation_interface_end->annotation = interface_end;
 533         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 534         return __RET__;
 535 }
 536
 537 t_element * __wrapper__write_prepare() {
 538                                                 unsigned int rdwr = m_rdwr.load(mo_acquire);
 539         /* Automatically generated code for potential commit point: Prepare_Potential_RW_Load */
 540
 541         if (true) {
 542                 struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
 543                 potential_cp_define->label_num = 6;
 544                 potential_cp_define->label_name = "Prepare_Potential_RW_Load";
 545                 struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 546                 annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
 547                 annotation_potential_cp_define->annotation = potential_cp_define;
 548                 cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
 549         }
 550
 551                 unsigned int rd,wr;
 552                 for(;;) {
 553                         rd = (rdwr>>16) & MASK;
 554                         wr = rdwr & MASK;
 555
 556                         if ( wr == ((rd + t_size)&MASK) ) {
 557         /* Automatically generated code for commit point define: Prepare_RW_Load_Full */
 558
 559         if (true) {
 560                 struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
 561                 cp_define->label_num = 7;
 562                 cp_define->label_name = "Prepare_RW_Load_Full";
 563                 cp_define->potential_cp_label_num = 6;
 564                 cp_define->potential_label_name = "Prepare_Potential_RW_Load";
 565                 cp_define->interface_num = 2;
 566                 struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 567                 annotation_cp_define->type = CP_DEFINE;
 568                 annotation_cp_define->annotation = cp_define;
 569                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
 570         }
 571
 572                                 return NULL;
 573                         }
 574
 575
 576                         bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) |
 577                                 ((wr+1)&MASK),mo_acq_rel);
 578         /* Automatically generated code for commit point define check: Prepare_RW_RMW */
 579
 580         if (succ) {
 581                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 582                 cp_define_check->label_num = 8;
 583                 cp_define_check->label_name = "Prepare_RW_RMW";
 584                 cp_define_check->interface_num = 2;
 585                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 586                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 587                 annotation_cp_define_check->annotation = cp_define_check;
 588                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 589         }
 590
 591                                                 if (succ)
 592                                 break;
 593                         else
 594                                 thrd_yield();
 595                 }
 596
 597                                 rl::backoff bo;
 598                 while (true) {
 599
 600                         int read = m_read.load(mo_acquire);
 601         /* Automatically generated code for potential commit point: Prepare_Potential_R_Load */
 602
 603         if (true) {
 604                 struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
 605                 potential_cp_define->label_num = 9;
 606                 potential_cp_define->label_name = "Prepare_Potential_R_Load";
 607                 struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 608                 annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
 609                 annotation_potential_cp_define->annotation = potential_cp_define;
 610                 cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
 611         }
 612
 613                         if ((read & MASK) != rd)
 614                                 thrd_yield();
 615                         else
 616                                 break;
 617                 }
 618
 619         /* Automatically generated code for commit point define: Prepare_R_Load */
 620
 621         if (true) {
 622                 struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
 623                 cp_define->label_num = 10;
 624                 cp_define->label_name = "Prepare_R_Load";
 625                 cp_define->potential_cp_label_num = 9;
 626                 cp_define->potential_label_name = "Prepare_Potential_R_Load";
 627                 cp_define->interface_num = 2;
 628                 struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 629                 annotation_cp_define->type = CP_DEFINE;
 630                 annotation_cp_define->annotation = cp_define;
 631                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
 632         }
 633
 634
 635                 t_element * p = & ( m_array[ wr % t_size ] );
 636
 637                 return p;
 638         }
 639
 640
 641 void write_publish(t_element * bin) {
 642         /* Interface begins */
 643         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 644         interface_begin->interface_num = 3; // Publish
 645                 interface_begin->interface_name = "Publish";
 646         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 647         annotation_interface_begin->type = INTERFACE_BEGIN;
 648         annotation_interface_begin->annotation = interface_begin;
 649         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 650         __wrapper__write_publish(bin);
 651         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 652         hb_condition->interface_num = 3; // Publish
 653         hb_condition->hb_condition_num = 0;
 654         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 655         annotation_hb_condition->type = HB_CONDITION;
 656         annotation_hb_condition->annotation = hb_condition;
 657         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 658
 659         Publish_info* info = (Publish_info*) malloc(sizeof(Publish_info));
 660         info->bin = bin;
 661         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 662         interface_end->interface_num = 3; // Publish
 663         interface_end->info = info;
 664         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 665         annoation_interface_end->type = INTERFACE_END;
 666         annoation_interface_end->annotation = interface_end;
 667         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 668 }
 669
 670 void __wrapper__write_publish(t_element * bin)
 671         {
 672
 673                 int tmp = m_written.fetch_add(1,mo_release);
 674         /* Automatically generated code for commit point define check: Publish_W_RMW */
 675
 676         if (true) {
 677                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 678                 cp_define_check->label_num = 11;
 679                 cp_define_check->label_name = "Publish_W_RMW";
 680                 cp_define_check->interface_num = 3;
 681                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 682                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 683                 annotation_cp_define_check->annotation = cp_define_check;
 684                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 685         }
 686
 687                 printf("publish: m_written=%d\n", tmp + 1);
 688         }
 689
 690
 691
 692 };
 693 template <typename t_element, size_t t_size>
 694 void** mpmc_boundq_1_alt<t_element, t_size>::func_ptr_table;
 695 template <typename t_element, size_t t_size>
 696 hb_rule** mpmc_boundq_1_alt<t_element, t_size>::hb_rule_table;
 697 template <typename t_element, size_t t_size>
 698 commutativity_rule** mpmc_boundq_1_alt<t_element, t_size>::commutativity_rule_table;
 699
 700