cliffc-hashtable/cliffc_hashtable.h

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