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