output/mcs-lock/mcs-lock.h

   1
   2 #include <stdatomic.h>
   3 #include <unrelacy.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 #include "common.h"
  11
  12 struct mcs_node {
  13         std::atomic<mcs_node *> next;
  14         std::atomic<int> gate;
  15
  16         mcs_node() {
  17                 next.store(0);
  18                 gate.store(0);
  19         }
  20 };
  21
  22
  23 struct mcs_mutex {
  24 public:
  25                 std::atomic<mcs_node *> m_tail;
  26
  27         mcs_mutex() {
  28         __sequential_init();
  29
  30                 m_tail.store( NULL );
  31         }
  32         ~mcs_mutex() {
  33                         }
  34
  35                 class guard {
  36         public:
  37                 mcs_mutex * m_t;
  38                 mcs_node    m_node;
  39                 guard(mcs_mutex * t) : m_t(t) { t->lock(this); }
  40                 ~guard() { m_t->unlock(this); }
  41         };
  42
  43 /* All other user-defined structs */
  44 static bool _lock_acquired;
  45 /* All other user-defined functions */
  46 /* Definition of interface info struct: Unlock */
  47 typedef struct Unlock_info {
  48 guard * I;
  49 } Unlock_info;
  50 /* End of info struct definition: Unlock */
  51
  52 /* ID function of interface: Unlock */
  53 inline static call_id_t Unlock_id(void *info, thread_id_t __TID__) {
  54         Unlock_info* theInfo = (Unlock_info*)info;
  55         guard * I = theInfo->I;
  56
  57         call_id_t __ID__ = 0;
  58         return __ID__;
  59 }
  60 /* End of ID function: Unlock */
  61
  62 /* Check action function of interface: Unlock */
  63 inline static bool Unlock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
  64         bool check_passed;
  65         Unlock_info* theInfo = (Unlock_info*)info;
  66         guard * I = theInfo->I;
  67
  68         check_passed = _lock_acquired == true;
  69         if (!check_passed)
  70                 return false;
  71         _lock_acquired = false ;
  72         return true;
  73 }
  74 /* End of check action function: Unlock */
  75
  76 /* Definition of interface info struct: Lock */
  77 typedef struct Lock_info {
  78 guard * I;
  79 } Lock_info;
  80 /* End of info struct definition: Lock */
  81
  82 /* ID function of interface: Lock */
  83 inline static call_id_t Lock_id(void *info, thread_id_t __TID__) {
  84         Lock_info* theInfo = (Lock_info*)info;
  85         guard * I = theInfo->I;
  86
  87         call_id_t __ID__ = 0;
  88         return __ID__;
  89 }
  90 /* End of ID function: Lock */
  91
  92 /* Check action function of interface: Lock */
  93 inline static bool Lock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
  94         bool check_passed;
  95         Lock_info* theInfo = (Lock_info*)info;
  96         guard * I = theInfo->I;
  97
  98         check_passed = _lock_acquired == false ;;
  99         if (!check_passed)
 100                 return false;
 101         _lock_acquired = true ;
 102         return true;
 103 }
 104 /* End of check action function: Lock */
 105
 106 #define INTERFACE_SIZE 2
 107 static void** func_ptr_table;
 108 static hb_rule** hb_rule_table;
 109 static commutativity_rule** commutativity_rule_table;
 110
 111 /* Initialization of sequential varialbes */
 112 static void __SPEC_INIT__() {
 113         _lock_acquired = false ;
 114 }
 115
 116 /* Cleanup routine of sequential variables */
 117 static bool __SPEC_CLEANUP__() {
 118         return true;
 119 }
 120
 121 /* Define function for sequential code initialization */
 122 inline static void __sequential_init() {
 123         /* Init func_ptr_table */
 124         func_ptr_table = (void**) malloc(sizeof(void*) * 2 * 2);
 125         func_ptr_table[2 * 1] = (void*) &Unlock_id;
 126         func_ptr_table[2 * 1 + 1] = (void*) &Unlock_check_action;
 127         func_ptr_table[2 * 0] = (void*) &Lock_id;
 128         func_ptr_table[2 * 0 + 1] = (void*) &Lock_check_action;
 129         /* Unlock(true) -> Lock(true) */
 130         struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
 131         hbConditionInit0->interface_num_before = 1; // Unlock
 132         hbConditionInit0->hb_condition_num_before = 0; //
 133         hbConditionInit0->interface_num_after = 0; // Lock
 134         hbConditionInit0->hb_condition_num_after = 0; //
 135         /* Init hb_rule_table */
 136         hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 1);
 137         #define HB_RULE_TABLE_SIZE 1
 138         hb_rule_table[0] = hbConditionInit0;
 139         /* Init commutativity_rule_table */
 140         /* Pass init info, including function table info & HB rules & Commutativity Rules */
 141         struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
 142         anno_init->init_func = (void_func_t) __SPEC_INIT__;
 143         anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
 144         anno_init->func_table = func_ptr_table;
 145         anno_init->func_table_size = INTERFACE_SIZE;
 146         anno_init->hb_rule_table = hb_rule_table;
 147         anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
 148         anno_init->commutativity_rule_table = commutativity_rule_table;
 149         anno_init->commutativity_rule_table_size = 0;
 150         struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 151         init->type = INIT;
 152         init->annotation = anno_init;
 153         cdsannotate(SPEC_ANALYSIS, init);
 154
 155 }
 156
 157 /* End of Global construct generation in class */
 158
 159
 160
 161 void lock(guard * I) {
 162         /* Interface begins */
 163         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 164         interface_begin->interface_num = 0; // Lock
 165                 interface_begin->interface_name = "Lock";
 166         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 167         annotation_interface_begin->type = INTERFACE_BEGIN;
 168         annotation_interface_begin->annotation = interface_begin;
 169         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 170         __wrapper__lock(I);
 171         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 172         hb_condition->interface_num = 0; // Lock
 173         hb_condition->hb_condition_num = 0;
 174         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 175         annotation_hb_condition->type = HB_CONDITION;
 176         annotation_hb_condition->annotation = hb_condition;
 177         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 178
 179         Lock_info* info = (Lock_info*) malloc(sizeof(Lock_info));
 180         info->I = I;
 181         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 182         interface_end->interface_num = 0; // Lock
 183         interface_end->info = info;
 184         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 185         annoation_interface_end->type = INTERFACE_END;
 186         annoation_interface_end->annotation = interface_end;
 187         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 188 }
 189
 190 void __wrapper__lock(guard * I) {
 191                 mcs_node * me = &(I->m_node);
 192
 193                                                 me->next.store(NULL, std::mo_relaxed );
 194                 me->gate.store(1, std::mo_relaxed );
 195
 196
 197
 198                                 mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
 199         /* Automatically generated code for commit point define check: Lock_Enqueue_Point1 */
 200
 201         if (pred == NULL) {
 202                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 203                 cp_define_check->label_num = 0;
 204                 cp_define_check->label_name = "Lock_Enqueue_Point1";
 205                 cp_define_check->interface_num = 0;
 206                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 207                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 208                 annotation_cp_define_check->annotation = cp_define_check;
 209                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 210         }
 211
 212                 if ( pred != NULL ) {
 213
 214                                                                                                                         pred->next.store(me, std::mo_release );
 215
 216
 217                                                                         rl::linear_backoff bo;
 218                         int my_gate = 1;
 219                         while (my_gate ) {
 220
 221                                 my_gate = me->gate.load(std::mo_acquire);
 222         /* Automatically generated code for commit point define check: Lock_Enqueue_Point2 */
 223
 224         if (my_gate == 0) {
 225                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 226                 cp_define_check->label_num = 1;
 227                 cp_define_check->label_name = "Lock_Enqueue_Point2";
 228                 cp_define_check->interface_num = 0;
 229                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 230                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 231                 annotation_cp_define_check->annotation = cp_define_check;
 232                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 233         }
 234
 235                                 thrd_yield();
 236                         }
 237                 }
 238         }
 239
 240
 241 void unlock(guard * I) {
 242         /* Interface begins */
 243         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 244         interface_begin->interface_num = 1; // Unlock
 245                 interface_begin->interface_name = "Unlock";
 246         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 247         annotation_interface_begin->type = INTERFACE_BEGIN;
 248         annotation_interface_begin->annotation = interface_begin;
 249         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 250         __wrapper__unlock(I);
 251         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 252         hb_condition->interface_num = 1; // Unlock
 253         hb_condition->hb_condition_num = 0;
 254         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 255         annotation_hb_condition->type = HB_CONDITION;
 256         annotation_hb_condition->annotation = hb_condition;
 257         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 258
 259         Unlock_info* info = (Unlock_info*) malloc(sizeof(Unlock_info));
 260         info->I = I;
 261         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 262         interface_end->interface_num = 1; // Unlock
 263         interface_end->info = info;
 264         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 265         annoation_interface_end->type = INTERFACE_END;
 266         annoation_interface_end->annotation = interface_end;
 267         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 268 }
 269
 270 void __wrapper__unlock(guard * I) {
 271                 mcs_node * me = &(I->m_node);
 272
 273                                 mcs_node * next = me->next.load(std::mo_acquire);
 274                                 if ( next == NULL )
 275                 {
 276                         mcs_node * tail_was_me = me;
 277                         bool success;
 278
 279
 280                         success = m_tail.compare_exchange_strong(
 281                                 tail_was_me,NULL,std::mo_acq_rel);
 282         /* Automatically generated code for commit point define check: Unlock_Point_Success_1 */
 283
 284         if (success == true) {
 285                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 286                 cp_define_check->label_num = 2;
 287                 cp_define_check->label_name = "Unlock_Point_Success_1";
 288                 cp_define_check->interface_num = 1;
 289                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 290                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 291                 annotation_cp_define_check->annotation = cp_define_check;
 292                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 293         }
 294
 295                         if (success) {
 296
 297                                                                 return;
 298                         }
 299
 300                                                 rl::linear_backoff bo;
 301                         for(;;) {
 302                                                                 next = me->next.load(std::mo_acquire);
 303                                                                 if ( next != NULL )
 304                                         break;
 305                                 thrd_yield();
 306                         }
 307                 }
 308
 309
 310
 311                                 next->gate.store( 0, std::mo_release );
 312         /* Automatically generated code for commit point define check: Unlock_Point_Success_2 */
 313
 314         if (true) {
 315                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 316                 cp_define_check->label_num = 3;
 317                 cp_define_check->label_name = "Unlock_Point_Success_2";
 318                 cp_define_check->interface_num = 1;
 319                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 320                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 321                 annotation_cp_define_check->annotation = cp_define_check;
 322                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 323         }
 324
 325         }
 326 };
 327 void** mcs_mutex::func_ptr_table;
 328 hb_rule** mcs_mutex::hb_rule_table;
 329 commutativity_rule** mcs_mutex::commutativity_rule_table;
 330 bool mcs_mutex::_lock_acquired;
 331
 332