benchmark/cliffc-hashtable/cliffc_hashtable.h

   1 #ifndef CLIFFC_HASHTABLE_H
   2 #define CLIFFC_HASHTABLE_H
   3
   4 #include <iostream>
   5 #include <atomic>
   6 //#include <common.h>
   7 #ifdef STANDALONE
   8 #include <assert.h>
   9 #define MODEL_ASSERT assert
  10 #else
  11 #include <model-assert.h>
  12 #endif
  13
  14 #include <spec_lib.h>
  15 #include <stdlib.h>
  16 #include <cdsannotate.h>
  17 #include <specannotation.h>
  18 #include <model_memory.h>
  19 #include "common.h"
  20
  21 using namespace std;
  22
  23 /**
  24         This header file declares and defines a simplified version of Cliff Click's
  25         NonblockingHashMap. It contains all the necessary structrues and main
  26         functions. In simplified_cliffc_hashtable.cc file, it has the definition for
  27         the static fields.
  28 */
  29
  30 template<typename TypeK, typename TypeV>
  31 class cliffc_hashtable;
  32
  33 /**
  34         Corresponding the the Object[] array in Cliff Click's Java implementation.
  35         It keeps the first two slots for CHM (Hashtable control unit) and the hash
  36         records (an array of hash used for fast negative key-equality check).
  37 */
  38 struct kvs_data {
  39         int _size;
  40         atomic<void*> *_data;
  41
  42         kvs_data(int sz) {
  43                 _size = sz;
  44                 int real_size = sz * 2 + 2;
  45                 _data = new atomic<void*>[real_size];
  46                 // The control block should be initialized in resize()
  47                 // Init the hash record array
  48                 int *hashes = new int[_size];
  49                 int i;
  50                 for (i = 0; i < _size; i++) {
  51                         hashes[i] = 0;
  52                 }
  53                 // Init the data to Null slot
  54                 for (i = 2; i < real_size; i++) {
  55                         _data[i].store(NULL, memory_order_relaxed);
  56                 }
  57                 _data[1].store(hashes, memory_order_release);
  58         }
  59
  60         ~kvs_data() {
  61                 int *hashes = (int*) _data[1].load(memory_order_relaxed);
  62                 delete hashes;
  63                 delete[] _data;
  64         }
  65 };
  66
  67 struct slot {
  68         bool _prime;
  69         void *_ptr;
  70
  71         slot(bool prime, void *ptr) {
  72                 _prime = prime;
  73                 _ptr = ptr;
  74         }
  75 };
  76
  77
  78 /**
  79         TypeK must have defined function "int hashCode()" which return the hash
  80         code for the its object, and "int equals(TypeK anotherKey)" which is
  81         used to judge equality.
  82         TypeK and TypeV should define their own copy constructor.
  83 */
  84 /**
  85         @Begin
  86         @Class_begin
  87         @End
  88 */
  89 template<typename TypeK, typename TypeV>
  90 class cliffc_hashtable {
  91         /**
  92                 # The synchronization we have for the hashtable gives us the property of
  93                 # serializability, so we should have a sequential hashtable when we check the
  94                 # correctness. The key thing is to identify all the commit point.
  95
  96                 @Begin
  97                 @Options:
  98                         LANG = CPP;
  99                         CLASS = cliffc_hashtable;
 100                 @Global_define:
 101                         @DeclareVar:
 102                         spec_table *map;
 103                         spec_table *id_map;
 104                         id_tag_t *tag;
 105                         @InitVar:
 106                                 map = new_spec_table_default(equals_key);
 107                                 id_map = new_spec_table_default(equals_id);
 108                                 tag = new_id_tag();
 109
 110                         @DefineFunc:
 111                         bool equals_key(void *ptr1, void *ptr2) {
 112                                 TypeK *key1 = (TypeK*) ptr1,
 113                                         *key2 = (TypeK*) ptr2;
 114                                 if (key1 == NULL || key2 == NULL)
 115                                         return false;
 116                                 return key1->equals(key2);
 117                         }
 118
 119                         @DefineFunc:
 120                         bool equals_val(void *ptr1, void *ptr2) {
 121                                 if (ptr1 == ptr2)
 122                                         return true;
 123                                 TypeV *val1 = (TypeV*) ptr1,
 124                                         *val2 = (TypeV*) ptr2;
 125                                 if (val1 == NULL || val2 == NULL)
 126                                         return false;
 127                                 return val1->equals(val2);
 128                         }
 129
 130                         @DefineFunc:
 131                         bool equals_id(void *ptr1, void *ptr2) {
 132                                 id_tag_t *id1 = (id_tag_t*) ptr1,
 133                                         *id2 = (id_tag_t*) ptr2;
 134                                 if (id1 == NULL || id2 == NULL)
 135                                         return false;
 136                                 return (*id1).tag == (*id2).tag;
 137                         }
 138
 139                         @DefineFunc:
 140                         # Update the tag for the current key slot if the corresponding tag
 141                         # is NULL, otherwise just return that tag. It will update the next
 142                         # available tag too if it requires a new tag for that key slot.
 143                         call_id_t getKeyTag(TypeK *key) {
 144                                 if (!spec_table_contains(id_map, key)) {
 145                                         call_id_t cur_id = current(tag);
 146                                         spec_table_put(id_map, key, (void*) cur_id);
 147                                         next(tag);
 148                                         return cur_id;
 149                                 } else {
 150                                         call_id_t res = (call_id_t) spec_table_get(id_map, key);
 151                                         return res;
 152                                 }
 153                         }
 154
 155                 @Interface_cluster:
 156                         Read_interface = {
 157                                 Get,
 158                                 PutIfAbsent,
 159                                 RemoveAny,
 160                                 RemoveIfMatch,
 161                                 ReplaceAny,
 162                                 ReplaceIfMatch
 163                         }
 164
 165                         Write_interface = {
 166                                 Put,
 167                                 PutIfAbsent(COND_PutIfAbsentSucc),
 168                                 RemoveAny,
 169                                 RemoveIfMatch(COND_RemoveIfMatchSucc),
 170                                 ReplaceAny,
 171                                 ReplaceIfMatch(COND_ReplaceIfMatchSucc)
 172                         }
 173                 @Happens_before:
 174                         //Write_interface -> Read_interface
 175                         Put->Get
 176                         Put->Put
 177                 @End
 178         */
 179
 180 friend class CHM;
 181         /**
 182                 The control structure for the hashtable
 183         */
 184         private:
 185         class CHM {
 186                 friend class cliffc_hashtable;
 187                 private:
 188                 atomic<kvs_data*> _newkvs;
 189
 190                 // Size of active K,V pairs
 191                 atomic_int _size;
 192
 193                 // Count of used slots
 194                 atomic_int _slots;
 195
 196                 // The next part of the table to copy
 197                 atomic_int _copy_idx;
 198
 199                 // Work-done reporting
 200                 atomic_int _copy_done;
 201
 202                 public:
 203                 CHM(int size) {
 204                         _newkvs.store(NULL, memory_order_relaxed);
 205                         _size.store(size, memory_order_relaxed);
 206                         _slots.store(0, memory_order_relaxed);
 207
 208                         _copy_idx.store(0, memory_order_relaxed);
 209                         _copy_done.store(0, memory_order_release);
 210                 }
 211
 212                 ~CHM() {}
 213
 214                 private:
 215
 216                 // Heuristic to decide if the table is too full
 217                 bool table_full(int reprobe_cnt, int len) {
 218                         return
 219                                 reprobe_cnt >= REPROBE_LIMIT &&
 220                                 _slots.load(memory_order_relaxed) >= reprobe_limit(len);
 221                 }
 222
 223                 kvs_data* resize(cliffc_hashtable *topmap, kvs_data *kvs) {
 224                         //model_print("resizing...\n");
 225                         kvs_data *newkvs = _newkvs.load(memory_order_acquire);
 226                         if (newkvs != NULL)
 227                                 return newkvs;
 228
 229                         // No copy in-progress, start one; Only double the table size
 230                         int oldlen = kvs->_size;
 231                         int sz = _size.load(memory_order_relaxed);
 232                         int newsz = sz;
 233
 234                         // Just follow Cliff Click's heuristic to decide the new size
 235                         if (sz >= (oldlen >> 2)) { // If we are 25% full
 236                                 newsz = oldlen << 1; // Double size
 237                                 if (sz >= (oldlen >> 1))
 238                                         newsz = oldlen << 2; // Double double size
 239                         }
 240
 241                         // We do not record the record timestamp
 242                         if (newsz <= oldlen) newsz = oldlen << 1;
 243                         // Do not shrink ever
 244                         if (newsz < oldlen) newsz = oldlen;
 245
 246                         // Last check cause the 'new' below is expensive
 247                         newkvs = _newkvs.load(memory_order_acquire);
 248                         if (newkvs != NULL) return newkvs;
 249
 250                         newkvs = new kvs_data(newsz);
 251                         void *chm = (void*) new CHM(sz);
 252                         newkvs->_data[0].store(chm, memory_order_release);
 253
 254                         kvs_data *cur_newkvs;
 255                         // Another check after the slow allocation
 256                         if ((cur_newkvs = _newkvs.load(memory_order_acquire)) != NULL)
 257                                 return cur_newkvs;
 258                         // CAS the _newkvs to the allocated table
 259                         kvs_data *desired = (kvs_data*) NULL;
 260                         kvs_data *expected = (kvs_data*) newkvs;
 261                         if (!_newkvs.compare_exchange_strong(desired, expected, memory_order_release,
 262                                         memory_order_relaxed)) {
 263                                 // Should clean the allocated area
 264                                 delete newkvs;
 265                                 newkvs = _newkvs.load(memory_order_acquire);
 266                         }
 267                         return newkvs;
 268                 }
 269
 270                 void help_copy_impl(cliffc_hashtable *topmap, kvs_data *oldkvs,
 271                         bool copy_all) {
 272                         MODEL_ASSERT (get_chm(oldkvs) == this);
 273                         kvs_data *newkvs = _newkvs.load(memory_order_acquire);
 274                         int oldlen = oldkvs->_size;
 275                         int min_copy_work = oldlen > 1024 ? 1024 : oldlen;
 276
 277                         // Just follow Cliff Click's code here
 278                         int panic_start = -1;
 279                         int copyidx;
 280                         while (_copy_done.load(memory_order_acquire) < oldlen) {
 281                                 copyidx = _copy_idx.load(memory_order_acquire);
 282                                 if (panic_start == -1) { // No painc
 283                                         copyidx = _copy_idx.load(memory_order_acquire);
 284                                         while (copyidx < (oldlen << 1) &&
 285                                                 !_copy_idx.compare_exchange_strong(copyidx, copyidx +
 286                                                         min_copy_work, memory_order_release, memory_order_relaxed))
 287                                                 copyidx = _copy_idx.load(memory_order_relaxed);
 288                                         if (!(copyidx < (oldlen << 1)))
 289                                                 panic_start = copyidx;
 290                                 }
 291
 292                                 // Now copy the chunk of work we claimed
 293                                 int workdone = 0;
 294                                 for (int i = 0; i < min_copy_work; i++)
 295                                         if (copy_slot(topmap, (copyidx + i) & (oldlen - 1), oldkvs,
 296                                                 newkvs))
 297                                                 workdone++;
 298                                 if (workdone > 0)
 299                                         copy_check_and_promote(topmap, oldkvs, workdone);
 300
 301                                 copyidx += min_copy_work;
 302                                 if (!copy_all && panic_start == -1)
 303                                         return; // We are done with the work we claim
 304                         }
 305                         copy_check_and_promote(topmap, oldkvs, 0); // See if we can promote
 306                 }
 307
 308                 kvs_data* copy_slot_and_check(cliffc_hashtable *topmap, kvs_data
 309                         *oldkvs, int idx, void *should_help) {
 310                         kvs_data *newkvs = _newkvs.load(memory_order_acquire);
 311                         // We're only here cause the caller saw a Prime
 312                         if (copy_slot(topmap, idx, oldkvs, newkvs))
 313                                 copy_check_and_promote(topmap, oldkvs, 1); // Record the slot copied
 314                         return (should_help == NULL) ? newkvs : topmap->help_copy(newkvs);
 315                 }
 316
 317                 void copy_check_and_promote(cliffc_hashtable *topmap, kvs_data*
 318                         oldkvs, int workdone) {
 319                         int oldlen = oldkvs->_size;
 320                         int copyDone = _copy_done.load(memory_order_relaxed);
 321                         if (workdone > 0) {
 322                                 while (true) {
 323                                         copyDone = _copy_done.load(memory_order_relaxed);
 324                                         if (_copy_done.compare_exchange_weak(copyDone, copyDone +
 325                                                 workdone, memory_order_relaxed, memory_order_relaxed))
 326                                                 break;
 327                                 }
 328                         }
 329
 330                         // Promote the new table to the current table
 331                         if (copyDone + workdone == oldlen &&
 332                                 topmap->_kvs.load(memory_order_acquire) == oldkvs) {
 333                                 kvs_data *newkvs = _newkvs.load(memory_order_acquire);
 334                                 topmap->_kvs.compare_exchange_strong(oldkvs, newkvs, memory_order_release,
 335                                         memory_order_relaxed);
 336                         }
 337                 }
 338
 339                 bool copy_slot(cliffc_hashtable *topmap, int idx, kvs_data *oldkvs,
 340                         kvs_data *newkvs) {
 341                         slot *key_slot;
 342                         while ((key_slot = key(oldkvs, idx)) == NULL)
 343                                 CAS_key(oldkvs, idx, NULL, TOMBSTONE);
 344
 345                         // First CAS old to Prime
 346                         slot *oldval = val(oldkvs, idx);
 347                         while (!is_prime(oldval)) {
 348                                 slot *box = (oldval == NULL || oldval == TOMBSTONE)
 349                                         ? TOMBPRIME : new slot(true, oldval->_ptr);
 350                                 if (CAS_val(oldkvs, idx, oldval, box)) {
 351                                         if (box == TOMBPRIME)
 352                                                 return 1; // Copy done
 353                                         // Otherwise we CAS'd the box
 354                                         oldval = box; // Record updated oldval
 355                                         break;
 356                                 }
 357                                 oldval = val(oldkvs, idx); // Else re-try
 358                         }
 359
 360                         if (oldval == TOMBPRIME) return false; // Copy already completed here
 361
 362                         slot *old_unboxed = new slot(false, oldval->_ptr);
 363                         int copied_into_new = (putIfMatch(topmap, newkvs, key_slot, old_unboxed,
 364                                 NULL) == NULL);
 365
 366                         // Old value is exposed in the new table
 367                         while (!CAS_val(oldkvs, idx, oldval, TOMBPRIME))
 368                                 oldval = val(oldkvs, idx);
 369
 370                         return copied_into_new;
 371                 }
 372         };
 373
 374
 375
 376         private:
 377         static const int Default_Init_Size = 4; // Intial table size
 378
 379         static slot* const MATCH_ANY;
 380         static slot* const NO_MATCH_OLD;
 381
 382         static slot* const TOMBPRIME;
 383         static slot* const TOMBSTONE;
 384
 385         static const int REPROBE_LIMIT = 10; // Forces a table-resize
 386
 387         atomic<kvs_data*> _kvs;
 388
 389         public:
 390         cliffc_hashtable() {
 391                 // Should initialize the CHM for the construction of the table
 392                 // For other CHM in kvs_data, they should be initialzed in resize()
 393                 // because the size is determined dynamically
 394                 /**
 395                         @Begin
 396                         @Entry_point
 397                         @End
 398                 */
 399                 kvs_data *kvs = new kvs_data(Default_Init_Size);
 400                 void *chm = (void*) new CHM(0);
 401                 kvs->_data[0].store(chm, memory_order_relaxed);
 402                 _kvs.store(kvs, memory_order_release);
 403         }
 404
 405         cliffc_hashtable(int init_size) {
 406                 // Should initialize the CHM for the construction of the table
 407                 // For other CHM in kvs_data, they should be initialzed in resize()
 408                 // because the size is determined dynamically
 409
 410                 /**
 411                         @Begin
 412                         @Entry_point
 413                         @End
 414                 */
 415                 kvs_data *kvs = new kvs_data(init_size);
 416                 void *chm = (void*) new CHM(0);
 417                 kvs->_data[0].store(chm, memory_order_relaxed);
 418                 _kvs.store(kvs, memory_order_release);
 419         }
 420
 421         /**
 422                 @Begin
 423                 @Interface: Get
 424                 @Commit_point_set: Get_Success_Point1 | Get_Success_Point2 | Get_Success_Point3
 425                 @ID: getKeyTag(key)
 426                 @Action:
 427                         void *_Old_Val = spec_table_get(map, key);
 428                 @Post_check:
 429                         __RET__ == NULL ? true : equals_val(_Old_Val, __RET__)
 430                 @End
 431         */
 432         TypeV* get(TypeK *key) {
 433                 slot *key_slot = new slot(false, key);
 434                 int fullhash = hash(key_slot);
 435                 kvs_data *kvs = _kvs.load(memory_order_acquire);
 436                 slot *V = get_impl(this, kvs, key_slot, fullhash);
 437                 if (V == NULL) return NULL;
 438                 MODEL_ASSERT (!is_prime(V));
 439                 return (TypeV*) V->_ptr;
 440         }
 441
 442         /**
 443                 @Begin
 444                 @Interface: Put
 445                 @Commit_point_set: Write_Success_Point
 446                 @ID: getKeyTag(key)
 447                 @Action:
 448                         # Remember this old value at checking point
 449                         void *_Old_Val = spec_table_get(map, key);
 450                         spec_table_put(map, key, val);
 451                 @Post_check:
 452                         equals_val(__RET__, _Old_Val)
 453                 @End
 454         */
 455         TypeV* put(TypeK *key, TypeV *val) {
 456                 return putIfMatch(key, val, NO_MATCH_OLD);
 457         }
 458
 459         /**
 460 //              @Begin
 461                 @Interface: PutIfAbsent
 462                 @Commit_point_set:
 463                         Write_Success_Point | PutIfAbsent_Fail_Point
 464                 @Condition: !spec_table_contains(map, key)
 465                 @HB_condition:
 466                         COND_PutIfAbsentSucc :: __RET__ == NULL
 467                 @ID: getKeyTag(key)
 468                 @Action:
 469                         void *_Old_Val = spec_table_get(map, key);
 470                         if (__COND_SAT__)
 471                                 spec_table_put(map, key, value);
 472                 @Post_check:
 473                         __COND_SAT__ ? __RET__ == NULL : equals_val(_Old_Val, __RET__)
 474                 @End
 475         */
 476         TypeV* putIfAbsent(TypeK *key, TypeV *value) {
 477                 return putIfMatch(key, val, TOMBSTONE);
 478         }
 479
 480         /**
 481 //              @Begin
 482                 @Interface: RemoveAny
 483                 @Commit_point_set: Write_Success_Point
 484                 @ID: getKeyTag(key)
 485                 @Action:
 486                         void *_Old_Val = spec_table_get(map, key);
 487                         spec_table_put(map, key, NULL);
 488                 @Post_check:
 489                         equals_val(__RET__, _Old_Val)
 490                 @End
 491         */
 492         TypeV* remove(TypeK *key) {
 493                 return putIfMatch(key, TOMBSTONE, NO_MATCH_OLD);
 494         }
 495
 496         /**
 497 //              @Begin
 498                 @Interface: RemoveIfMatch
 499                 @Commit_point_set:
 500                         Write_Success_Point | RemoveIfMatch_Fail_Point
 501                 @Condition:
 502                         equals_val(spec_table_get(map, key), val)
 503                 @HB_condition:
 504                         COND_RemoveIfMatchSucc :: __RET__ == true
 505                 @ID: getKeyTag(key)
 506                 @Action:
 507                         if (__COND_SAT__)
 508                                 spec_table_put(map, key, NULL);
 509                 @Post_check:
 510                         __COND_SAT__ ? __RET__ : !__RET__
 511                 @End
 512         */
 513         bool remove(TypeK *key, TypeV *val) {
 514                 slot *val_slot = val == NULL ? NULL : new slot(false, val);
 515                 return putIfMatch(key, TOMBSTONE, val) == val;
 516
 517         }
 518
 519         /**
 520 //              @Begin
 521                 @Interface: ReplaceAny
 522                 @Commit_point_set:
 523                         Write_Success_Point
 524                 @ID: getKeyTag(key)
 525                 @Action:
 526                         void *_Old_Val = spec_table_get(map, key);
 527                 @Post_check:
 528                         equals_val(__RET__, _Old_Val)
 529                 @End
 530         */
 531         TypeV* replace(TypeK *key, TypeV *val) {
 532                 return putIfMatch(key, val, MATCH_ANY);
 533         }
 534
 535         /**
 536 //              @Begin
 537                 @Interface: ReplaceIfMatch
 538                 @Commit_point_set:
 539                         Write_Success_Point | ReplaceIfMatch_Fail_Point
 540                 @Condition:
 541                         equals_val(spec_table_get(map, key), oldval)
 542                 @HB_condition:
 543                         COND_ReplaceIfMatchSucc :: __RET__ == true
 544                 @ID: getKeyTag(key)
 545                 @Action:
 546                         if (__COND_SAT__)
 547                                 spec_table_put(map, key, newval);
 548                 @Post_check:
 549                         __COND_SAT__ ? __RET__ : !__RET__
 550                 @End
 551         */
 552         bool replace(TypeK *key, TypeV *oldval, TypeV *newval) {
 553                 return putIfMatch(key, newval, oldval) == oldval;
 554         }
 555
 556         private:
 557         static CHM* get_chm(kvs_data* kvs) {
 558                 CHM *res = (CHM*) kvs->_data[0].load(memory_order_relaxed);
 559                 return res;
 560         }
 561
 562         static int* get_hashes(kvs_data *kvs) {
 563                 return (int *) kvs->_data[1].load(memory_order_relaxed);
 564         }
 565
 566         // Preserve happens-before semantics on newly inserted keys
 567         static inline slot* key(kvs_data *kvs, int idx) {
 568                 MODEL_ASSERT (idx >= 0 && idx < kvs->_size);
 569                 // Corresponding to the volatile read in get_impl() and putIfMatch in
 570                 // Cliff Click's Java implementation
 571                 slot *res = (slot*) kvs->_data[idx * 2 + 2].load(memory_order_acquire);
 572                 return res;
 573         }
 574
 575         /**
 576                 The atomic operation in val() function is a "potential" commit point,
 577                 which means in some case it is a real commit point while it is not for
 578                 some other cases. This so happens because the val() function is such a
 579                 fundamental function that many internal operation will call. Our
 580                 strategy is that we label any potential commit points and check if they
 581                 really are the commit points later.
 582         */
 583         // Preserve happens-before semantics on newly inserted values
 584         static inline slot* val(kvs_data *kvs, int idx) {
 585                 MODEL_ASSERT (idx >= 0 && idx < kvs->_size);
 586                 // Corresponding to the volatile read in get_impl() and putIfMatch in
 587                 // Cliff Click's Java implementation
 588                 slot *res = (slot*) kvs->_data[idx * 2 + 3].load(memory_order_acquire);
 589                 /**
 590                         @Begin
 591                         # This is a complicated potential commit point since many many functions are
 592                         # calling val().
 593                         @Potential_commit_point_define: true
 594                         @Label: Read_Val_Point
 595                         @End
 596                 */
 597                 return res;
 598
 599
 600         }
 601
 602         static int hash(slot *key_slot) {
 603                 MODEL_ASSERT(key_slot != NULL && key_slot->_ptr != NULL);
 604                 TypeK* key = (TypeK*) key_slot->_ptr;
 605                 int h = key->hashCode();
 606                 // Spread bits according to Cliff Click's code
 607                 h += (h << 15) ^ 0xffffcd7d;
 608                 h ^= (h >> 10);
 609                 h += (h << 3);
 610                 h ^= (h >> 6);
 611                 h += (h << 2) + (h << 14);
 612                 return h ^ (h >> 16);
 613         }
 614
 615         // Heuristic to decide if reprobed too many times.
 616         // Be careful here: Running over the limit on a 'get' acts as a 'miss'; on a
 617         // put it triggers a table resize. Several places MUST have exact agreement.
 618         static int reprobe_limit(int len) {
 619                 return REPROBE_LIMIT + (len >> 2);
 620         }
 621
 622         static inline bool is_prime(slot *val) {
 623                 return (val != NULL) && val->_prime;
 624         }
 625
 626         // Check for key equality. Try direct pointer comparison first (fast
 627         // negative teset) and then the full 'equals' call
 628         static bool keyeq(slot *K, slot *key_slot, int *hashes, int hash,
 629                 int fullhash) {
 630                 // Caller should've checked this.
 631                 MODEL_ASSERT (K != NULL);
 632                 TypeK* key_ptr = (TypeK*) key_slot->_ptr;
 633                 return
 634                         K == key_slot ||
 635                                 ((hashes[hash] == 0 || hashes[hash] == fullhash) &&
 636                                 K != TOMBSTONE &&
 637                                 key_ptr->equals(K->_ptr));
 638         }
 639
 640         static bool valeq(slot *val_slot1, slot *val_slot2) {
 641                 MODEL_ASSERT (val_slot1 != NULL);
 642                 TypeK* ptr1 = (TypeV*) val_slot1->_ptr;
 643                 if (val_slot2 == NULL || ptr1 == NULL) return false;
 644                 return ptr1->equals(val_slot2->_ptr);
 645         }
 646
 647         // Together with key() preserve the happens-before relationship on newly
 648         // inserted keys
 649         static inline bool CAS_key(kvs_data *kvs, int idx, void *expected, void *desired) {
 650                 return kvs->_data[2 * idx + 2].compare_exchange_strong(expected,
 651                         desired, memory_order_release, memory_order_relaxed);
 652         }
 653
 654         /**
 655                 Same as the val() function, we only label the CAS operation as the
 656                 potential commit point.
 657         */
 658         // Together with val() preserve the happens-before relationship on newly
 659         // inserted values
 660         static inline bool CAS_val(kvs_data *kvs, int idx, void *expected, void
 661                 *desired) {
 662                 bool res =  kvs->_data[2 * idx + 3].compare_exchange_strong(expected,
 663                         desired, memory_order_release, memory_order_relaxed);
 664                 /**
 665                         # If it is a successful put instead of a copy or any other internal
 666                         # operantions, expected != NULL
 667                         @Begin
 668                         @Potential_commit_point_define: res == true
 669                         @Label: Write_Val_Point
 670                         @End
 671                 */
 672                 return res;
 673         }
 674
 675         slot* get_impl(cliffc_hashtable *topmap, kvs_data *kvs, slot* key_slot, int
 676                 fullhash) {
 677                 int len = kvs->_size;
 678                 CHM *chm = get_chm(kvs);
 679                 int *hashes = get_hashes(kvs);
 680
 681                 int idx = fullhash & (len - 1);
 682                 int reprobe_cnt = 0;
 683                 while (true) {
 684                         slot *K = key(kvs, idx);
 685                         slot *V = val(kvs, idx);
 686                         /**
 687                                 @Begin
 688                                 @Commit_point_define: K == NULL
 689                                 @Potential_commit_point_label: Read_Val_Point
 690                                 @Label: Get_Success_Point_1
 691                                 @End
 692                         */
 693
 694                         if (K == NULL) return NULL; // A miss
 695
 696                         if (keyeq(K, key_slot, hashes, idx, fullhash)) {
 697                                 // Key hit! Check if table-resize in progress
 698                                 if (!is_prime(V)) {
 699                                         /**
 700                                                 @Begin
 701                                                 @Commit_point_define: true
 702                                                 @Potential_commit_point_label: Read_Val_Point
 703                                                 @Label: Get_Success_Point_2
 704                                                 @End
 705                                         */
 706                                         return (V == TOMBSTONE) ? NULL : V; // Return this value
 707                                 }
 708                                 // Otherwise, finish the copy & retry in the new table
 709                                 return get_impl(topmap, chm->copy_slot_and_check(topmap, kvs,
 710                                         idx, key_slot), key_slot, fullhash);
 711                         }
 712
 713                         if (++reprobe_cnt >= REPROBE_LIMIT ||
 714                                 key_slot == TOMBSTONE) {
 715                                 // Retry in new table
 716                                 // Atomic read (acquire) can be here
 717                                 kvs_data *newkvs = chm->_newkvs.load(memory_order_acquire);
 718                                 /**
 719                                         @Begin
 720                                         @Commit_point_define_check: newkvs == NULL
 721                                         @Label: Get_Success_Point_3
 722                                         @End
 723                                 */
 724                                 return newkvs == NULL ? NULL : get_impl(topmap,
 725                                         topmap->help_copy(newkvs), key_slot, fullhash);
 726                         }
 727
 728                         idx = (idx + 1) & (len - 1); // Reprobe by 1
 729                 }
 730         }
 731
 732         // A wrapper of the essential function putIfMatch()
 733         TypeV* putIfMatch(TypeK *key, TypeV *value, slot *old_val) {
 734                 // TODO: Should throw an exception rather return NULL
 735                 if (old_val == NULL) {
 736                         return NULL;
 737                 }
 738                 slot *key_slot = new slot(false, key);
 739
 740                 slot *value_slot = new slot(false, value);
 741                 kvs_data *kvs = _kvs.load(memory_order_acquire);
 742                 slot *res = putIfMatch(this, kvs, key_slot, value_slot, old_val);
 743                 // Only when copy_slot() call putIfMatch() will it return NULL
 744                 MODEL_ASSERT (res != NULL);
 745                 MODEL_ASSERT (!is_prime(res));
 746                 return res == TOMBSTONE ? NULL : (TypeV*) res->_ptr;
 747         }
 748
 749         /**
 750                 Put, Remove, PutIfAbsent, etc will call this function. Return the old
 751                 value. If the returned value is equals to the expVal (or expVal is
 752                 NO_MATCH_OLD), then this function puts the val_slot to the table 'kvs'.
 753                 Only copy_slot will pass a NULL expVal, and putIfMatch only returns a
 754                 NULL if passed a NULL expVal.
 755         */
 756         static slot* putIfMatch(cliffc_hashtable *topmap, kvs_data *kvs, slot
 757                 *key_slot, slot *val_slot, slot *expVal) {
 758                 MODEL_ASSERT (val_slot != NULL);
 759                 MODEL_ASSERT (!is_prime(val_slot));
 760                 MODEL_ASSERT (!is_prime(expVal));
 761
 762                 int fullhash = hash(key_slot);
 763                 int len = kvs->_size;
 764                 CHM *chm = get_chm(kvs);
 765                 int *hashes = get_hashes(kvs);
 766                 int idx = fullhash & (len - 1);
 767
 768                 // Claim a key slot
 769                 int reprobe_cnt = 0;
 770                 slot *K;
 771                 slot *V;
 772                 kvs_data *newkvs;
 773
 774                 while (true) { // Spin till we get a key slot
 775                         K = key(kvs, idx);
 776                         V = val(kvs, idx);
 777                         if (K == NULL) { // Get a free slot
 778                                 if (val_slot == TOMBSTONE) return val_slot;
 779                                 // Claim the null key-slot
 780                                 if (CAS_key(kvs, idx, NULL, key_slot)) {
 781                                         chm->_slots.fetch_add(1, memory_order_relaxed); // Inc key-slots-used count
 782                                         hashes[idx] = fullhash; // Memorize full hash
 783                                         break;
 784                                 }
 785                                 K = key(kvs, idx); // CAS failed, get updated value
 786                                 MODEL_ASSERT (K != NULL);
 787                         }
 788
 789                         // Key slot not null, there exists a Key here
 790                         if (keyeq(K, key_slot, hashes, idx, fullhash))
 791                                 break; // Got it
 792
 793                         // Notice that the logic here should be consistent with that of get.
 794                         // The first predicate means too many reprobes means nothing in the
 795                         // old table.
 796                         if (++reprobe_cnt >= reprobe_limit(len) ||
 797                                 K == TOMBSTONE) { // Found a Tombstone key, no more keys
 798                                 newkvs = chm->resize(topmap, kvs);
 799                                 //model_print("resize1\n");
 800                                 // Help along an existing copy
 801                                 if (expVal != NULL) topmap->help_copy(newkvs);
 802                                 return putIfMatch(topmap, newkvs, key_slot, val_slot, expVal);
 803                         }
 804
 805                         idx = (idx + 1) & (len - 1); // Reprobe
 806                 } // End of spinning till we get a Key slot
 807
 808                 if (val_slot == V) return V; // Fast cutout for no-change
 809
 810                 // Here it tries to resize cause it doesn't want other threads to stop
 811                 // its progress (eagerly try to resize soon)
 812                 newkvs = chm->_newkvs.load(memory_order_acquire);
 813                 if (newkvs == NULL &&
 814                         ((V == NULL && chm->table_full(reprobe_cnt, len)) || is_prime(V))) {
 815                         //model_print("resize2\n");
 816                         newkvs = chm->resize(topmap, kvs); // Force the copy to start
 817                 }
 818
 819                 // Finish the copy and then put it in the new table
 820                 if (newkvs != NULL)
 821                         return putIfMatch(topmap, chm->copy_slot_and_check(topmap, kvs, idx,
 822                                 expVal), key_slot, val_slot, expVal);
 823
 824                 // Decided to update the existing table
 825                 while (true) {
 826                         MODEL_ASSERT (!is_prime(V));
 827
 828                         if (expVal != NO_MATCH_OLD &&
 829                                 V != expVal &&
 830                                 (expVal != MATCH_ANY || V == TOMBSTONE || V == NULL) &&
 831                                 !(V == NULL && expVal == TOMBSTONE) &&
 832                                 (expVal == NULL || !valeq(expVal, V))) {
 833                                 /**
 834                                         @Begin
 835                                         @Commit_point_define: expVal == TOMBSTONE
 836                                         @Potential_commit_point_label: Read_Val_Point
 837                                         @Label: PutIfAbsent_Fail_Point
 838                                                 # This is a check for the PutIfAbsent() when the value
 839                                                 # is not absent
 840                                         @End
 841                                 */
 842                                 /**
 843                                         @Begin
 844                                         @Commit_point_define: expVal != NULL && val_slot == TOMBSTONE
 845                                         @Potential_commit_point_label: Read_Val_Point
 846                                         @Label: RemoveIfMatch_Fail_Point
 847                                         @End
 848                                 */
 849                                 /**
 850                                         @Begin
 851                                         @Commit_point_define: expVal != NULL && !valeq(expVal, V)
 852                                         @Potential_commit_point_label: Read_Val_Point
 853                                         @Label: ReplaceIfMatch_Fail_Point
 854                                         @End
 855                                 */
 856                                 return V; // Do not update!
 857                         }
 858
 859                         if (CAS_val(kvs, idx, V, val_slot)) {
 860                                 /**
 861                                         @Begin
 862                                         # The only point where a successful put happens
 863                                         @Commit_point_define: true
 864                                         @Potential_commit_point_label: Write_Val_Point
 865                                         @Label: Write_Success_Point
 866                                         @End
 867                                 */
 868                                 if (expVal != NULL) { // Not called by a table-copy
 869                                         // CAS succeeded, should adjust size
 870                                         // Both normal put's and table-copy calls putIfMatch, but
 871                                         // table-copy does not increase the number of live K/V pairs
 872                                         if ((V == NULL || V == TOMBSTONE) &&
 873                                                 val_slot != TOMBSTONE)
 874                                                 chm->_size.fetch_add(1, memory_order_relaxed);
 875                                         if (!(V == NULL || V == TOMBSTONE) &&
 876                                                 val_slot == TOMBSTONE)
 877                                                 chm->_size.fetch_add(-1, memory_order_relaxed);
 878                                 }
 879                                 return (V == NULL && expVal != NULL) ? TOMBSTONE : V;
 880                         }
 881                         // Else CAS failed
 882                         V = val(kvs, idx);
 883                         if (is_prime(V))
 884                                 return putIfMatch(topmap, chm->copy_slot_and_check(topmap, kvs,
 885                                         idx, expVal), key_slot, val_slot, expVal);
 886                 }
 887         }
 888
 889         // Help along an existing table-resize. This is a fast cut-out wrapper.
 890         kvs_data* help_copy(kvs_data *helper) {
 891                 kvs_data *topkvs = _kvs.load(memory_order_acquire);
 892                 CHM *topchm = get_chm(topkvs);
 893                 // No cpy in progress
 894                 if (topchm->_newkvs.load(memory_order_acquire) == NULL) return helper;
 895                 topchm->help_copy_impl(this, topkvs, false);
 896                 return helper;
 897         }
 898 };
 899 /**
 900         @Begin
 901         @Class_end
 902         @End
 903 */
 904
 905 #endif