output/concurrent-hashmap/hashmap.h

   1 #ifndef _HASHMAP_H
   2 #define _HASHMAP_H
   3
   4 #include <iostream>
   5 #include <atomic>
   6 #include "stdio.h"
   7 #include <stdlib.h>
   8 #include <mutex>
   9
  10 #include <spec_lib.h>
  11 #include <cdsannotate.h>
  12 #include <specannotation.h>
  13 #include <model_memory.h>
  14 #include "common.h"
  15
  16
  17 #include "common.h"
  18
  19 #define relaxed memory_order_relaxed
  20 #define release memory_order_release
  21 #define acquire memory_order_acquire
  22 #define acq_rel memory_order_acq_rel
  23 #define seq_cst memory_order_seq_cst
  24
  25 using namespace std;
  26
  27
  28
  29 class Entry {
  30         public:
  31         int key;
  32         atomic_int value;
  33         int hash;
  34         atomic<Entry*> next;
  35
  36         Entry(int h, int k, int v, Entry *n) {
  37                 this->hash = h;
  38                 this->key = k;
  39                 this->value.store(v, relaxed);
  40                 this->next.store(n, relaxed);
  41         }
  42 };
  43
  44 class Segment {
  45         public:
  46         int count;
  47         mutex segMutex;
  48
  49         void lock() {
  50                 segMutex.lock();
  51         }
  52
  53         void unlock() {
  54                 segMutex.unlock();
  55         }
  56
  57         Segment() {
  58                 this->count = 0;
  59         }
  60 };
  61
  62
  63 class HashMap {
  64         public:
  65
  66 /* All other user-defined structs */
  67 static IntegerMap * __map;
  68 /* All other user-defined functions */
  69 /* Definition of interface info struct: Put */
  70 typedef struct Put_info {
  71 int __RET__;
  72 int key;
  73 int value;
  74 } Put_info;
  75 /* End of info struct definition: Put */
  76
  77 /* ID function of interface: Put */
  78 inline static call_id_t Put_id(void *info, thread_id_t __TID__) {
  79         Put_info* theInfo = (Put_info*)info;
  80         int __RET__ = theInfo->__RET__;
  81         int key = theInfo->key;
  82         int value = theInfo->value;
  83
  84         call_id_t __ID__ = value;
  85         return __ID__;
  86 }
  87 /* End of ID function: Put */
  88
  89 /* Check action function of interface: Put */
  90 inline static bool Put_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
  91         bool check_passed;
  92         Put_info* theInfo = (Put_info*)info;
  93         int __RET__ = theInfo->__RET__;
  94         int key = theInfo->key;
  95         int value = theInfo->value;
  96
  97         putIntegerMap ( __map , key , value ) ;
  98         return true;
  99 }
 100 /* End of check action function: Put */
 101
 102 /* Definition of interface info struct: Get */
 103 typedef struct Get_info {
 104 int __RET__;
 105 int key;
 106 } Get_info;
 107 /* End of info struct definition: Get */
 108
 109 /* ID function of interface: Get */
 110 inline static call_id_t Get_id(void *info, thread_id_t __TID__) {
 111         Get_info* theInfo = (Get_info*)info;
 112         int __RET__ = theInfo->__RET__;
 113         int key = theInfo->key;
 114
 115         call_id_t __ID__ = __RET__;
 116         return __ID__;
 117 }
 118 /* End of ID function: Get */
 119
 120 /* Check action function of interface: Get */
 121 inline static bool Get_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
 122         bool check_passed;
 123         Get_info* theInfo = (Get_info*)info;
 124         int __RET__ = theInfo->__RET__;
 125         int key = theInfo->key;
 126
 127         int res = getIntegerMap ( __map , key ) ;
 128         check_passed = __RET__ ? res == __RET__ : true;
 129         if (!check_passed)
 130                 return false;
 131         return true;
 132 }
 133 /* End of check action function: Get */
 134
 135 #define INTERFACE_SIZE 2
 136 static void** func_ptr_table;
 137 static hb_rule** hb_rule_table;
 138 static commutativity_rule** commutativity_rule_table;
 139 inline static bool CommutativityCondition0(void *info1, void *info2) {
 140         Put_info *_info1 = (Put_info*) info1;
 141         Put_info *_info2 = (Put_info*) info2;
 142         return _info1-> key != _info2-> key;
 143 }
 144 inline static bool CommutativityCondition1(void *info1, void *info2) {
 145         Put_info *_info1 = (Put_info*) info1;
 146         Get_info *_info2 = (Get_info*) info2;
 147         return _info1-> key != _info2-> key;
 148 }
 149 inline static bool CommutativityCondition2(void *info1, void *info2) {
 150         Get_info *_info1 = (Get_info*) info1;
 151         Get_info *_info2 = (Get_info*) info2;
 152         return true;
 153 }
 154
 155 /* Initialization of sequential varialbes */
 156 static void __SPEC_INIT__() {
 157         __map = createIntegerMap ( ) ;
 158 }
 159
 160 /* Cleanup routine of sequential variables */
 161 static bool __SPEC_CLEANUP__() {
 162         if ( __map ) destroyIntegerMap ( __map ) ;
 163         return true ;
 164 }
 165
 166 /* Define function for sequential code initialization */
 167 inline static void __sequential_init() {
 168         /* Init func_ptr_table */
 169         func_ptr_table = (void**) malloc(sizeof(void*) * 2 * 2);
 170         func_ptr_table[2 * 1] = (void*) &Put_id;
 171         func_ptr_table[2 * 1 + 1] = (void*) &Put_check_action;
 172         func_ptr_table[2 * 0] = (void*) &Get_id;
 173         func_ptr_table[2 * 0 + 1] = (void*) &Get_check_action;
 174         /* Put(true) -> Get(true) */
 175         struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
 176         hbConditionInit0->interface_num_before = 1; // Put
 177         hbConditionInit0->hb_condition_num_before = 0; //
 178         hbConditionInit0->interface_num_after = 0; // Get
 179         hbConditionInit0->hb_condition_num_after = 0; //
 180         /* Init hb_rule_table */
 181         hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 1);
 182         #define HB_RULE_TABLE_SIZE 1
 183         hb_rule_table[0] = hbConditionInit0;
 184         /* Init commutativity_rule_table */
 185         commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 3);
 186         commutativity_rule* rule;
 187         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 188         rule->interface_num_before = 1;
 189         rule->interface_num_after = 1;
 190         rule->rule = "_Method1 . key != _Method2 . key";
 191         rule->condition = CommutativityCondition0;
 192         commutativity_rule_table[0] = rule;
 193         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 194         rule->interface_num_before = 1;
 195         rule->interface_num_after = 0;
 196         rule->rule = "_Method1 . key != _Method2 . key";
 197         rule->condition = CommutativityCondition1;
 198         commutativity_rule_table[1] = rule;
 199         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 200         rule->interface_num_before = 0;
 201         rule->interface_num_after = 0;
 202         rule->rule = "true";
 203         rule->condition = CommutativityCondition2;
 204         commutativity_rule_table[2] = rule;
 205         /* Pass init info, including function table info & HB rules & Commutativity Rules */
 206         struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
 207         anno_init->init_func = (void_func_t) __SPEC_INIT__;
 208         anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
 209         anno_init->func_table = func_ptr_table;
 210         anno_init->func_table_size = INTERFACE_SIZE;
 211         anno_init->hb_rule_table = hb_rule_table;
 212         anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
 213         anno_init->commutativity_rule_table = commutativity_rule_table;
 214         anno_init->commutativity_rule_table_size = 3;
 215         struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 216         init->type = INIT;
 217         init->annotation = anno_init;
 218         cdsannotate(SPEC_ANALYSIS, init);
 219
 220 }
 221
 222 /* End of Global construct generation in class */
 223
 224
 225         atomic<Entry*> *table;
 226
 227         int capacity;
 228         int size;
 229
 230         static const int CONCURRENCY_LEVEL = 4;
 231
 232         static const int SEGMENT_MASK = CONCURRENCY_LEVEL - 1;
 233
 234         Segment *segments[CONCURRENCY_LEVEL];
 235
 236         static const int DEFAULT_INITIAL_CAPACITY = 16;
 237
 238
 239         HashMap() {
 240         __sequential_init();
 241
 242                 this->size = 0;
 243                 this->capacity = DEFAULT_INITIAL_CAPACITY;
 244                 this->table = new atomic<Entry*>[capacity];
 245                 for (int i = 0; i < capacity; i++) {
 246                         atomic_init(&table[i], NULL);
 247                 }
 248                 for (int i = 0; i < CONCURRENCY_LEVEL; i++) {
 249                         segments[i] = new Segment;
 250                 }
 251         }
 252
 253         int hashKey(int key) {
 254                 return key;
 255         }
 256
 257
 258
 259 int get(int key) {
 260         /* Interface begins */
 261         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 262         interface_begin->interface_num = 0; // Get
 263                 interface_begin->interface_name = "Get";
 264         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 265         annotation_interface_begin->type = INTERFACE_BEGIN;
 266         annotation_interface_begin->annotation = interface_begin;
 267         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 268         int __RET__ = __wrapper__get(key);
 269         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 270         hb_condition->interface_num = 0; // Get
 271         hb_condition->hb_condition_num = 0;
 272         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 273         annotation_hb_condition->type = HB_CONDITION;
 274         annotation_hb_condition->annotation = hb_condition;
 275         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 276
 277         Get_info* info = (Get_info*) malloc(sizeof(Get_info));
 278         info->__RET__ = __RET__;
 279         info->key = key;
 280         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 281         interface_end->interface_num = 0; // Get
 282         interface_end->info = info;
 283         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 284         annoation_interface_end->type = INTERFACE_END;
 285         annoation_interface_end->annotation = interface_end;
 286         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 287         return __RET__;
 288 }
 289
 290 int __wrapper__get(int key) {
 291                 ASSERT (key);
 292                 int hash = hashKey(key);
 293
 294                                 atomic<Entry*> *tab = table;
 295                 int index = hash & (capacity - 1);
 296                 atomic<Entry*> *first = &tab[index];
 297                 Entry *e;
 298                 int res = 0;
 299
 300
 301
 302                 Entry *firstPtr = first->load(acquire);
 303
 304                 e = firstPtr;
 305                 while (e != NULL) {
 306                         if (key, e->key) {
 307
 308                                 res = e->value.load(seq_cst);
 309         /* Automatically generated code for commit point define check: GetReadValue1 */
 310
 311         if (res != 0) {
 312                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 313                 cp_define_check->label_num = 0;
 314                 cp_define_check->label_name = "GetReadValue1";
 315                 cp_define_check->interface_num = 0;
 316                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 317                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 318                 annotation_cp_define_check->annotation = cp_define_check;
 319                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 320         }
 321
 322                                 if (res != 0)
 323                                         return res;
 324                                 else
 325                                         break;
 326                         }
 327                                                                         e = e->next.load(relaxed);
 328                 }
 329
 330                                 Segment *seg = segments[hash & SEGMENT_MASK];
 331                 seg->lock();
 332                                 Entry *newFirstPtr = first->load(relaxed);
 333         /* Automatically generated code for commit point define check: GetReadEntry */
 334
 335         if (true) {
 336                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 337                 cp_define_check->label_num = 1;
 338                 cp_define_check->label_name = "GetReadEntry";
 339                 cp_define_check->interface_num = 0;
 340                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 341                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 342                 annotation_cp_define_check->annotation = cp_define_check;
 343                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 344         }
 345
 346                 if (e != NULL || firstPtr != newFirstPtr) {
 347                         e = newFirstPtr;
 348                         while (e != NULL) {
 349                                 if (key == e->key) {
 350                                                                                 res = e->value.load(relaxed);
 351         /* Automatically generated code for commit point define check: GetReadValue2 */
 352
 353         if (true) {
 354                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 355                 cp_define_check->label_num = 2;
 356                 cp_define_check->label_name = "GetReadValue2";
 357                 cp_define_check->interface_num = 0;
 358                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 359                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 360                 annotation_cp_define_check->annotation = cp_define_check;
 361                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 362         }
 363
 364                                         seg->unlock();                                  return res;
 365                                 }
 366                                                                 e = e->next.load(relaxed);
 367                         }
 368                 }
 369                 seg->unlock();          return 0;
 370         }
 371
 372
 373 int put(int key, int value) {
 374         /* Interface begins */
 375         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 376         interface_begin->interface_num = 1; // Put
 377                 interface_begin->interface_name = "Put";
 378         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 379         annotation_interface_begin->type = INTERFACE_BEGIN;
 380         annotation_interface_begin->annotation = interface_begin;
 381         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 382         int __RET__ = __wrapper__put(key, value);
 383         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 384         hb_condition->interface_num = 1; // Put
 385         hb_condition->hb_condition_num = 0;
 386         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 387         annotation_hb_condition->type = HB_CONDITION;
 388         annotation_hb_condition->annotation = hb_condition;
 389         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 390
 391         Put_info* info = (Put_info*) malloc(sizeof(Put_info));
 392         info->__RET__ = __RET__;
 393         info->key = key;
 394         info->value = value;
 395         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 396         interface_end->interface_num = 1; // Put
 397         interface_end->info = info;
 398         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 399         annoation_interface_end->type = INTERFACE_END;
 400         annoation_interface_end->annotation = interface_end;
 401         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 402         return __RET__;
 403 }
 404
 405 int __wrapper__put(int key, int value) {
 406                 ASSERT (key && value);
 407                 int hash = hashKey(key);
 408                 Segment *seg = segments[hash & SEGMENT_MASK];
 409                 atomic<Entry*> *tab;
 410
 411                 seg->lock();            tab = table;
 412                 int index = hash & (capacity - 1);
 413
 414                 atomic<Entry*> *first = &tab[index];
 415                 Entry *e;
 416                 int oldValue = 0;
 417
 418                                 Entry *firstPtr = first->load(relaxed);
 419                 e = firstPtr;
 420                 while (e != NULL) {
 421                         if (key == e->key) {
 422                                                                                                 oldValue = e->value.load(relaxed);
 423
 424
 425                                 e->value.store(value, seq_cst);
 426         /* Automatically generated code for commit point define check: PutUpdateValue */
 427
 428         if (true) {
 429                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 430                 cp_define_check->label_num = 3;
 431                 cp_define_check->label_name = "PutUpdateValue";
 432                 cp_define_check->interface_num = 1;
 433                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 434                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 435                 annotation_cp_define_check->annotation = cp_define_check;
 436                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 437         }
 438
 439                                 seg->unlock();                          return oldValue;
 440                         }
 441                                                 e = e->next.load(relaxed);
 442                 }
 443
 444                                 Entry *newEntry = new Entry(hash, key, value, firstPtr);
 445
 446
 447                                 first->store(newEntry, release);
 448         /* Automatically generated code for commit point define check: PutInsertValue */
 449
 450         if (true) {
 451                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 452                 cp_define_check->label_num = 4;
 453                 cp_define_check->label_name = "PutInsertValue";
 454                 cp_define_check->interface_num = 1;
 455                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 456                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 457                 annotation_cp_define_check->annotation = cp_define_check;
 458                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 459         }
 460
 461                 seg->unlock();          return 0;
 462         }
 463 };
 464 void** HashMap::func_ptr_table;
 465 hb_rule** HashMap::hb_rule_table;
 466 commutativity_rule** HashMap::commutativity_rule_table;
 467 IntegerMap * HashMap::__map;
 468
 469
 470 #endif
 471