cliffc-hashtable/cliffc_hashtable.h

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