benchmark/cliffc-hashtable/cliffc_hashtable.h

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