+++ /dev/null
-#ifndef CLIFFC_HASHTABLE_H
-#define CLIFFC_HASHTABLE_H
-
-#include <iostream>
-#include <atomic>
-#include "stdio.h"
-#ifdef STANDALONE
-#include <assert.h>
-#define MODEL_ASSERT assert
-#else
-#include <model-assert.h>
-#endif
-
-#include <spec_lib.h>
-#include <stdlib.h>
-#include <cdsannotate.h>
-#include <specannotation.h>
-#include <model_memory.h>
-#include "common.h"
-
-using namespace std;
-
-
-
-template<typename TypeK, typename TypeV>
-class cliffc_hashtable;
-
-
-struct kvs_data {
- int _size;
- atomic<void*> *_data;
-
- kvs_data(int sz) {
- _size = sz;
- int real_size = sz * 2 + 2;
- _data = new atomic<void*>[real_size];
- int *hashes = new int[_size];
- int i;
- for (i = 0; i < _size; i++) {
- hashes[i] = 0;
- }
- for (i = 2; i < real_size; i++) {
- _data[i].store(NULL, memory_order_relaxed);
- }
- _data[1].store(hashes, memory_order_relaxed);
- }
-
- ~kvs_data() {
- int *hashes = (int*) _data[1].load(memory_order_relaxed);
- delete hashes;
- delete[] _data;
- }
-};
-
-struct slot {
- bool _prime;
- void *_ptr;
-
- slot(bool prime, void *ptr) {
- _prime = prime;
- _ptr = ptr;
- }
-};
-
-
-
-
-template<typename TypeK, typename TypeV>
-class cliffc_hashtable {
-/* All other user-defined structs */
-static spec_table * map;
-static spec_table * id_map;
-static id_tag_t * tag;
-/* All other user-defined functions */
-inline static bool equals_key ( void * ptr1 , void * ptr2 ) {
-TypeK * key1 = ( TypeK * ) ptr1 , * key2 = ( TypeK * ) ptr2 ;
-if ( key1 == NULL || key2 == NULL ) return false ;
-return key1 -> equals ( key2 ) ;
-}
-
-inline static bool equals_val ( void * ptr1 , void * ptr2 ) {
-if ( ptr1 == ptr2 ) return true ;
-TypeV * val1 = ( TypeV * ) ptr1 , * val2 = ( TypeV * ) ptr2 ;
-if ( val1 == NULL || val2 == NULL ) return false ;
-return val1 -> equals ( val2 ) ;
-}
-
-inline static bool equals_id ( void * ptr1 , void * ptr2 ) {
-id_tag_t * id1 = ( id_tag_t * ) ptr1 , * id2 = ( id_tag_t * ) ptr2 ;
-if ( id1 == NULL || id2 == NULL ) return false ;
-return ( * id1 ) . tag == ( * id2 ) . tag ;
-}
-
-inline static call_id_t getKeyTag ( TypeK * key ) {
-if ( ! spec_table_contains ( id_map , key ) ) {
-call_id_t cur_id = current ( tag ) ;
-spec_table_put ( id_map , key , ( void * ) cur_id ) ;
-next ( tag ) ;
-return cur_id ;
-}
-else {
-call_id_t res = ( call_id_t ) spec_table_get ( id_map , key ) ;
-return res ;
-}
-}
-
-/* Definition of interface info struct: Put */
-typedef struct Put_info {
-TypeV * __RET__;
-TypeK * key;
-TypeV * val;
-} Put_info;
-/* End of info struct definition: Put */
-
-/* ID function of interface: Put */
-inline static call_id_t Put_id(void *info, thread_id_t __TID__) {
- Put_info* theInfo = (Put_info*)info;
- TypeV * __RET__ = theInfo->__RET__;
- TypeK * key = theInfo->key;
- TypeV * val = theInfo->val;
-
- call_id_t __ID__ = getKeyTag ( key );
- return __ID__;
-}
-/* End of ID function: Put */
-
-/* Check action function of interface: Put */
-inline static bool Put_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
- bool check_passed;
- Put_info* theInfo = (Put_info*)info;
- TypeV * __RET__ = theInfo->__RET__;
- TypeK * key = theInfo->key;
- TypeV * val = theInfo->val;
-
- TypeV * _Old_Val = ( TypeV * ) spec_table_get ( map , key ) ;
- spec_table_put ( map , key , val ) ;
- bool passed = false ;
- if ( ! passed ) {
- int old = _Old_Val == NULL ? 0 : _Old_Val -> _val ;
- int ret = __RET__ == NULL ? 0 : __RET__ -> _val ;
- }
- check_passed = equals_val ( __RET__ , _Old_Val );
- if (!check_passed)
- return false;
- return true;
-}
-/* End of check action function: Put */
-
-/* Definition of interface info struct: Get */
-typedef struct Get_info {
-TypeV * __RET__;
-TypeK * key;
-} Get_info;
-/* End of info struct definition: Get */
-
-/* ID function of interface: Get */
-inline static call_id_t Get_id(void *info, thread_id_t __TID__) {
- Get_info* theInfo = (Get_info*)info;
- TypeV * __RET__ = theInfo->__RET__;
- TypeK * key = theInfo->key;
-
- call_id_t __ID__ = getKeyTag ( key );
- return __ID__;
-}
-/* End of ID function: Get */
-
-/* Check action function of interface: Get */
-inline static bool Get_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
- bool check_passed;
- Get_info* theInfo = (Get_info*)info;
- TypeV * __RET__ = theInfo->__RET__;
- TypeK * key = theInfo->key;
-
- TypeV * _Old_Val = ( TypeV * ) spec_table_get ( map , key ) ;
- bool passed = false ;
- if ( ! passed ) {
- int old = _Old_Val == NULL ? 0 : _Old_Val -> _val ;
- int ret = __RET__ == NULL ? 0 : __RET__ -> _val ;
- }
- check_passed = equals_val ( _Old_Val , __RET__ );
- if (!check_passed)
- return false;
- return true;
-}
-/* End of check action function: Get */
-
-#define INTERFACE_SIZE 2
-static void** func_ptr_table;
-static anno_hb_init** hb_init_table;
-
-/* Initialization of sequential varialbes */
-static void __SPEC_INIT__() {
- map = new_spec_table_default ( equals_key ) ;
- id_map = new_spec_table_default ( equals_id ) ;
- tag = new_id_tag ( ) ;
-}
-
-/* Cleanup routine of sequential variables */
-static void __SPEC_CLEANUP__() {
-}
-
-/* Define function for sequential code initialization */
-inline static void __sequential_init() {
- /* Init func_ptr_table */
- func_ptr_table = (void**) malloc(sizeof(void*) * 2 * 2);
- func_ptr_table[2 * 1] = (void*) &Put_id;
- func_ptr_table[2 * 1 + 1] = (void*) &Put_check_action;
- func_ptr_table[2 * 0] = (void*) &Get_id;
- func_ptr_table[2 * 0 + 1] = (void*) &Get_check_action;
- /* Put(true) -> Put(true) */
- struct anno_hb_init *hbConditionInit0 = (struct anno_hb_init*) malloc(sizeof(struct anno_hb_init));
- hbConditionInit0->interface_num_before = 1; // Put
- hbConditionInit0->hb_condition_num_before = 0; //
- hbConditionInit0->interface_num_after = 1; // Put
- hbConditionInit0->hb_condition_num_after = 0; //
- /* Put(true) -> Get(true) */
- struct anno_hb_init *hbConditionInit1 = (struct anno_hb_init*) malloc(sizeof(struct anno_hb_init));
- hbConditionInit1->interface_num_before = 1; // Put
- hbConditionInit1->hb_condition_num_before = 0; //
- hbConditionInit1->interface_num_after = 0; // Get
- hbConditionInit1->hb_condition_num_after = 0; //
- /* Init hb_init_table */
- hb_init_table = (anno_hb_init**) malloc(sizeof(anno_hb_init*) * 2);
- #define HB_INIT_TABLE_SIZE 2
- hb_init_table[0] = hbConditionInit0;
- hb_init_table[1] = hbConditionInit1;
- /* Pass init info, including function table info & HB rules */
- struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
- anno_init->init_func = (void*) __SPEC_INIT__;
- anno_init->cleanup_func = (void*) __SPEC_CLEANUP__;
- anno_init->func_table = func_ptr_table;
- anno_init->func_table_size = INTERFACE_SIZE;
- anno_init->hb_init_table = hb_init_table;
- anno_init->hb_init_table_size = HB_INIT_TABLE_SIZE;
- struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- init->type = INIT;
- init->annotation = anno_init;
- cdsannotate(SPEC_ANALYSIS, init);
-
-}
-
-/* End of Global construct generation in class */
-
-
-friend class CHM;
-
- private:
- class CHM {
- friend class cliffc_hashtable;
- private:
- atomic<kvs_data*> _newkvs;
-
- atomic_int _size;
-
- atomic_int _slots;
-
- atomic_int _copy_idx;
-
- atomic_int _copy_done;
-
- public:
- CHM(int size) {
- _newkvs.store(NULL, memory_order_relaxed);
- _size.store(size, memory_order_relaxed);
- _slots.store(0, memory_order_relaxed);
-
- _copy_idx.store(0, memory_order_relaxed);
- _copy_done.store(0, memory_order_relaxed);
- }
-
- ~CHM() {}
-
- private:
-
- bool table_full(int reprobe_cnt, int len) {
- return
- reprobe_cnt >= REPROBE_LIMIT &&
- _slots.load(memory_order_relaxed) >= reprobe_limit(len);
- }
-
- kvs_data* resize(cliffc_hashtable *topmap, kvs_data *kvs) {
-
- kvs_data *newkvs = _newkvs.load(memory_order_acquire);
- if (newkvs != NULL)
- return newkvs;
-
- int oldlen = kvs->_size;
- int sz = _size.load(memory_order_relaxed);
- int newsz = sz;
-
- if (sz >= (oldlen >> 2)) { newsz = oldlen << 1; if (sz >= (oldlen >> 1))
- newsz = oldlen << 2; }
-
- if (newsz <= oldlen) newsz = oldlen << 1;
- if (newsz < oldlen) newsz = oldlen;
-
-
- newkvs = _newkvs.load(memory_order_acquire);
- if (newkvs != NULL) return newkvs;
-
- newkvs = new kvs_data(newsz);
- void *chm = (void*) new CHM(sz);
- newkvs->_data[0].store(chm, memory_order_relaxed);
-
- kvs_data *cur_newkvs;
-
- if ((cur_newkvs = _newkvs.load(memory_order_acquire)) != NULL)
- return cur_newkvs;
- kvs_data *desired = (kvs_data*) NULL;
- kvs_data *expected = (kvs_data*) newkvs;
-
- if (!_newkvs.compare_exchange_strong(desired, expected, memory_order_release,
- memory_order_relaxed)) {
- delete newkvs;
-
- newkvs = _newkvs.load(memory_order_acquire);
- }
- return newkvs;
- }
-
- void help_copy_impl(cliffc_hashtable *topmap, kvs_data *oldkvs,
- bool copy_all) {
- MODEL_ASSERT (get_chm(oldkvs) == this);
-
- kvs_data *newkvs = _newkvs.load(memory_order_acquire);
- int oldlen = oldkvs->_size;
- int min_copy_work = oldlen > 1024 ? 1024 : oldlen;
-
- int panic_start = -1;
- int copyidx;
- while (_copy_done.load(memory_order_relaxed) < oldlen) {
- copyidx = _copy_idx.load(memory_order_relaxed);
- if (panic_start == -1) { copyidx = _copy_idx.load(memory_order_relaxed);
- while (copyidx < (oldlen << 1) &&
- !_copy_idx.compare_exchange_strong(copyidx, copyidx +
- min_copy_work, memory_order_relaxed, memory_order_relaxed))
- copyidx = _copy_idx.load(memory_order_relaxed);
- if (!(copyidx < (oldlen << 1)))
- panic_start = copyidx;
- }
-
- int workdone = 0;
- for (int i = 0; i < min_copy_work; i++)
- if (copy_slot(topmap, (copyidx + i) & (oldlen - 1), oldkvs,
- newkvs))
- workdone++;
- if (workdone > 0)
- copy_check_and_promote(topmap, oldkvs, workdone);
-
- copyidx += min_copy_work;
- if (!copy_all && panic_start == -1)
- return; }
- copy_check_and_promote(topmap, oldkvs, 0); }
-
- kvs_data* copy_slot_and_check(cliffc_hashtable *topmap, kvs_data
- *oldkvs, int idx, void *should_help) {
-
- kvs_data *newkvs = _newkvs.load(memory_order_acquire);
- if (copy_slot(topmap, idx, oldkvs, newkvs))
- copy_check_and_promote(topmap, oldkvs, 1); return (should_help == NULL) ? newkvs : topmap->help_copy(newkvs);
- }
-
- void copy_check_and_promote(cliffc_hashtable *topmap, kvs_data*
- oldkvs, int workdone) {
- int oldlen = oldkvs->_size;
- int copyDone = _copy_done.load(memory_order_relaxed);
- if (workdone > 0) {
- while (true) {
- copyDone = _copy_done.load(memory_order_relaxed);
- if (_copy_done.compare_exchange_weak(copyDone, copyDone +
- workdone, memory_order_relaxed, memory_order_relaxed))
- break;
- }
- }
-
- if (copyDone + workdone == oldlen &&
- topmap->_kvs.load(memory_order_relaxed) == oldkvs) {
-
- kvs_data *newkvs = _newkvs.load(memory_order_acquire);
-
- topmap->_kvs.compare_exchange_strong(oldkvs, newkvs, memory_order_release,
- memory_order_relaxed);
- }
- }
-
- bool copy_slot(cliffc_hashtable *topmap, int idx, kvs_data *oldkvs,
- kvs_data *newkvs) {
- slot *key_slot;
- while ((key_slot = key(oldkvs, idx)) == NULL)
- CAS_key(oldkvs, idx, NULL, TOMBSTONE);
-
- slot *oldval = val(oldkvs, idx);
- while (!is_prime(oldval)) {
- slot *box = (oldval == NULL || oldval == TOMBSTONE)
- ? TOMBPRIME : new slot(true, oldval->_ptr);
- if (CAS_val(oldkvs, idx, oldval, box)) {
- if (box == TOMBPRIME)
- return 1; oldval = box; break;
- }
- oldval = val(oldkvs, idx); }
-
- if (oldval == TOMBPRIME) return false;
- slot *old_unboxed = new slot(false, oldval->_ptr);
- int copied_into_new = (putIfMatch(topmap, newkvs, key_slot, old_unboxed,
- NULL) == NULL);
-
- while (!CAS_val(oldkvs, idx, oldval, TOMBPRIME))
- oldval = val(oldkvs, idx);
-
- return copied_into_new;
- }
- };
-
-
-
- private:
- static const int Default_Init_Size = 4;
- static slot* const MATCH_ANY;
- static slot* const NO_MATCH_OLD;
-
- static slot* const TOMBPRIME;
- static slot* const TOMBSTONE;
-
- static const int REPROBE_LIMIT = 10;
- atomic<kvs_data*> _kvs;
-
- public:
- cliffc_hashtable() {
- __sequential_init();
-
- kvs_data *kvs = new kvs_data(Default_Init_Size);
- void *chm = (void*) new CHM(0);
- kvs->_data[0].store(chm, memory_order_relaxed);
- _kvs.store(kvs, memory_order_relaxed);
- }
-
- cliffc_hashtable(int init_size) {
-
- __sequential_init();
-
- kvs_data *kvs = new kvs_data(init_size);
- void *chm = (void*) new CHM(0);
- kvs->_data[0].store(chm, memory_order_relaxed);
- _kvs.store(kvs, memory_order_relaxed);
- }
-
-
-TypeV * get(TypeK * key) {
- /* Interface begins */
- struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
- interface_begin->interface_num = 0; // Get
- interface_begin->interface_name = "Get";
- struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_interface_begin->type = INTERFACE_BEGIN;
- annotation_interface_begin->annotation = interface_begin;
- cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
- TypeV * __RET__ = __wrapper__get(key);
- struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
- hb_condition->interface_num = 0; // Get
- hb_condition->hb_condition_num = 0;
- struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_hb_condition->type = HB_CONDITION;
- annotation_hb_condition->annotation = hb_condition;
- cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
- Get_info* info = (Get_info*) malloc(sizeof(Get_info));
- info->__RET__ = __RET__;
- info->key = key;
- struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
- interface_end->interface_num = 0; // Get
- interface_end->info = info;
- struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annoation_interface_end->type = INTERFACE_END;
- annoation_interface_end->annotation = interface_end;
- cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
- return __RET__;
-}
-
-TypeV * __wrapper__get(TypeK * key) {
- slot *key_slot = new slot(false, key);
- int fullhash = hash(key_slot);
-
- kvs_data *kvs = _kvs.load(memory_order_acquire);
-
- slot *V = get_impl(this, kvs, key_slot, fullhash);
- if (V == NULL) return NULL;
- MODEL_ASSERT (!is_prime(V));
- return (TypeV*) V->_ptr;
- }
-
-
-TypeV * put(TypeK * key, TypeV * val) {
- /* Interface begins */
- struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
- interface_begin->interface_num = 1; // Put
- interface_begin->interface_name = "Put";
- struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_interface_begin->type = INTERFACE_BEGIN;
- annotation_interface_begin->annotation = interface_begin;
- cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
- TypeV * __RET__ = __wrapper__put(key, val);
- struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
- hb_condition->interface_num = 1; // Put
- hb_condition->hb_condition_num = 0;
- struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_hb_condition->type = HB_CONDITION;
- annotation_hb_condition->annotation = hb_condition;
- cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
- Put_info* info = (Put_info*) malloc(sizeof(Put_info));
- info->__RET__ = __RET__;
- info->key = key;
- info->val = val;
- struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
- interface_end->interface_num = 1; // Put
- interface_end->info = info;
- struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annoation_interface_end->type = INTERFACE_END;
- annoation_interface_end->annotation = interface_end;
- cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
- return __RET__;
-}
-
-TypeV * __wrapper__put(TypeK * key, TypeV * val) {
- return putIfMatch(key, val, NO_MATCH_OLD);
- }
-
-
- TypeV* putIfAbsent(TypeK *key, TypeV *value) {
- return putIfMatch(key, val, TOMBSTONE);
- }
-
-
- TypeV* remove(TypeK *key) {
- return putIfMatch(key, TOMBSTONE, NO_MATCH_OLD);
- }
-
-
- bool remove(TypeK *key, TypeV *val) {
- slot *val_slot = val == NULL ? NULL : new slot(false, val);
- return putIfMatch(key, TOMBSTONE, val) == val;
-
- }
-
-
- TypeV* replace(TypeK *key, TypeV *val) {
- return putIfMatch(key, val, MATCH_ANY);
- }
-
-
- bool replace(TypeK *key, TypeV *oldval, TypeV *newval) {
- return putIfMatch(key, newval, oldval) == oldval;
- }
-
- private:
- static CHM* get_chm(kvs_data* kvs) {
- CHM *res = (CHM*) kvs->_data[0].load(memory_order_relaxed);
- return res;
- }
-
- static int* get_hashes(kvs_data *kvs) {
- return (int *) kvs->_data[1].load(memory_order_relaxed);
- }
-
- static inline slot* key(kvs_data *kvs, int idx) {
- MODEL_ASSERT (idx >= 0 && idx < kvs->_size);
- slot *res = (slot*) kvs->_data[idx * 2 + 2].load(memory_order_relaxed);
- /* Automatically generated code for potential commit point: Read_Key_Point */
-
- if (true) {
- struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
- potential_cp_define->label_num = 0;
- potential_cp_define->label_name = "Read_Key_Point";
- potential_cp_define->is_additional_point = false;
- struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
- annotation_potential_cp_define->annotation = potential_cp_define;
- cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
- }
-
- return res;
- }
-
-
- static inline slot* val(kvs_data *kvs, int idx) {
- MODEL_ASSERT (idx >= 0 && idx < kvs->_size);
-
- slot *res = (slot*) kvs->_data[idx * 2 + 3].load(memory_order_acquire);
- /* Automatically generated code for potential commit point: Read_Val_Point */
-
- if (true) {
- struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
- potential_cp_define->label_num = 1;
- potential_cp_define->label_name = "Read_Val_Point";
- potential_cp_define->is_additional_point = false;
- struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
- annotation_potential_cp_define->annotation = potential_cp_define;
- cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
- }
-
- return res;
-
-
- }
-
- static int hash(slot *key_slot) {
- MODEL_ASSERT(key_slot != NULL && key_slot->_ptr != NULL);
- TypeK* key = (TypeK*) key_slot->_ptr;
- int h = key->hashCode();
- h += (h << 15) ^ 0xffffcd7d;
- h ^= (h >> 10);
- h += (h << 3);
- h ^= (h >> 6);
- h += (h << 2) + (h << 14);
- return h ^ (h >> 16);
- }
-
- static int reprobe_limit(int len) {
- return REPROBE_LIMIT + (len >> 2);
- }
-
- static inline bool is_prime(slot *val) {
- return (val != NULL) && val->_prime;
- }
-
- static bool keyeq(slot *K, slot *key_slot, int *hashes, int hash,
- int fullhash) {
- MODEL_ASSERT (K != NULL);
- TypeK* key_ptr = (TypeK*) key_slot->_ptr;
- return
- K == key_slot ||
- ((hashes[hash] == 0 || hashes[hash] == fullhash) &&
- K != TOMBSTONE &&
- key_ptr->equals(K->_ptr));
- }
-
- static bool valeq(slot *val_slot1, slot *val_slot2) {
- MODEL_ASSERT (val_slot1 != NULL);
- TypeK* ptr1 = (TypeV*) val_slot1->_ptr;
- if (val_slot2 == NULL || ptr1 == NULL) return false;
- return ptr1->equals(val_slot2->_ptr);
- }
-
- static inline bool CAS_key(kvs_data *kvs, int idx, void *expected, void *desired) {
- bool res = kvs->_data[2 * idx + 2].compare_exchange_strong(expected,
- desired, memory_order_relaxed, memory_order_relaxed);
- /* Automatically generated code for potential commit point: Write_Key_Point */
-
- if (res) {
- struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
- potential_cp_define->label_num = 2;
- potential_cp_define->label_name = "Write_Key_Point";
- potential_cp_define->is_additional_point = false;
- struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
- annotation_potential_cp_define->annotation = potential_cp_define;
- cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
- }
-
- return res;
- }
-
-
- static inline bool CAS_val(kvs_data *kvs, int idx, void *expected, void
- *desired) {
-
- bool res = kvs->_data[2 * idx + 3].compare_exchange_strong(expected,
- desired, memory_order_acq_rel, memory_order_relaxed);
- /* Automatically generated code for potential commit point: Write_Val_Point */
-
- if (res) {
- struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
- potential_cp_define->label_num = 3;
- potential_cp_define->label_name = "Write_Val_Point";
- potential_cp_define->is_additional_point = false;
- struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
- annotation_potential_cp_define->annotation = potential_cp_define;
- cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
- }
-
- return res;
- }
-
- slot* get_impl(cliffc_hashtable *topmap, kvs_data *kvs, slot* key_slot, int
- fullhash) {
- int len = kvs->_size;
- CHM *chm = get_chm(kvs);
- int *hashes = get_hashes(kvs);
-
- int idx = fullhash & (len - 1);
- int reprobe_cnt = 0;
- while (true) {
- slot *K = key(kvs, idx);
- /* Automatically generated code for commit point define: Get_Point1 */
-
- if (K == NULL) {
- struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
- cp_define->label_num = 4;
- cp_define->label_name = "Get_Point1";
- cp_define->potential_cp_label_num = 0;
- cp_define->potential_label_name = "Read_Key_Point";
- cp_define->interface_num = 0;
- cp_define->is_additional_point = false;
- struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_cp_define->type = CP_DEFINE;
- annotation_cp_define->annotation = cp_define;
- cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
- }
-
- slot *V = val(kvs, idx);
-
- if (K == NULL) {
- return NULL; }
-
- if (keyeq(K, key_slot, hashes, idx, fullhash)) {
- if (!is_prime(V)) {
- /* Automatically generated code for commit point clear: Get_Clear */
-
- if (true) {
- struct anno_cp_clear *cp_clear = (struct anno_cp_clear*) malloc(sizeof(struct anno_cp_clear));
- struct spec_annotation *annotation_cp_clear = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_cp_clear->type = CP_CLEAR;
- annotation_cp_clear->annotation = cp_clear;
- cdsannotate(SPEC_ANALYSIS, annotation_cp_clear);
- }
-
-
- /* Automatically generated code for commit point define: Get_Point2 */
-
- if (true) {
- struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
- cp_define->label_num = 6;
- cp_define->label_name = "Get_Point2";
- cp_define->potential_cp_label_num = 1;
- cp_define->potential_label_name = "Read_Val_Point";
- cp_define->interface_num = 0;
- cp_define->is_additional_point = false;
- struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_cp_define->type = CP_DEFINE;
- annotation_cp_define->annotation = cp_define;
- cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
- }
-
- return (V == TOMBSTONE) ? NULL : V; }
- return get_impl(topmap, chm->copy_slot_and_check(topmap, kvs,
- idx, key_slot), key_slot, fullhash);
- }
-
- if (++reprobe_cnt >= REPROBE_LIMIT ||
- key_slot == TOMBSTONE) {
-
- kvs_data *newkvs = chm->_newkvs.load(memory_order_acquire);
-
- return newkvs == NULL ? NULL : get_impl(topmap,
- topmap->help_copy(newkvs), key_slot, fullhash);
- }
-
- idx = (idx + 1) & (len - 1); }
- }
-
- TypeV* putIfMatch(TypeK *key, TypeV *value, slot *old_val) {
- if (old_val == NULL) {
- return NULL;
- }
- slot *key_slot = new slot(false, key);
-
- slot *value_slot = new slot(false, value);
-
- kvs_data *kvs = _kvs.load(memory_order_acquire);
-
- slot *res = putIfMatch(this, kvs, key_slot, value_slot, old_val);
- MODEL_ASSERT (res != NULL);
- MODEL_ASSERT (!is_prime(res));
- return res == TOMBSTONE ? NULL : (TypeV*) res->_ptr;
- }
-
-
- static slot* putIfMatch(cliffc_hashtable *topmap, kvs_data *kvs, slot
- *key_slot, slot *val_slot, slot *expVal) {
- MODEL_ASSERT (val_slot != NULL);
- MODEL_ASSERT (!is_prime(val_slot));
- MODEL_ASSERT (!is_prime(expVal));
-
- int fullhash = hash(key_slot);
- int len = kvs->_size;
- CHM *chm = get_chm(kvs);
- int *hashes = get_hashes(kvs);
- int idx = fullhash & (len - 1);
-
- int reprobe_cnt = 0;
- slot *K;
- slot *V;
- kvs_data *newkvs;
-
- while (true) { K = key(kvs, idx);
- V = val(kvs, idx);
- if (K == NULL) { if (val_slot == TOMBSTONE) return val_slot;
- if (CAS_key(kvs, idx, NULL, key_slot)) {
- /* Automatically generated code for commit point define: Put_WriteKey */
-
- if (true) {
- struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
- cp_define->label_num = 7;
- cp_define->label_name = "Put_WriteKey";
- cp_define->potential_cp_label_num = 2;
- cp_define->potential_label_name = "Write_Key_Point";
- cp_define->interface_num = 1;
- cp_define->is_additional_point = false;
- struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_cp_define->type = CP_DEFINE;
- annotation_cp_define->annotation = cp_define;
- cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
- }
-
- chm->_slots.fetch_add(1, memory_order_relaxed); hashes[idx] = fullhash; break;
- }
- K = key(kvs, idx); MODEL_ASSERT (K != NULL);
- }
-
- if (keyeq(K, key_slot, hashes, idx, fullhash))
- break;
- if (++reprobe_cnt >= reprobe_limit(len) ||
- K == TOMBSTONE) { newkvs = chm->resize(topmap, kvs);
- if (expVal != NULL) topmap->help_copy(newkvs);
- return putIfMatch(topmap, newkvs, key_slot, val_slot, expVal);
- }
-
- idx = (idx + 1) & (len - 1); }
- if (val_slot == V) return V;
-
- newkvs = chm->_newkvs.load(memory_order_acquire);
-
- if (newkvs == NULL &&
- ((V == NULL && chm->table_full(reprobe_cnt, len)) || is_prime(V))) {
- newkvs = chm->resize(topmap, kvs); }
-
- if (newkvs != NULL)
- return putIfMatch(topmap, chm->copy_slot_and_check(topmap, kvs, idx,
- expVal), key_slot, val_slot, expVal);
-
- while (true) {
- MODEL_ASSERT (!is_prime(V));
-
- if (expVal != NO_MATCH_OLD &&
- V != expVal &&
- (expVal != MATCH_ANY || V == TOMBSTONE || V == NULL) &&
- !(V == NULL && expVal == TOMBSTONE) &&
- (expVal == NULL || !valeq(expVal, V))) {
-
-
-
- return V; }
-
- if (CAS_val(kvs, idx, V, val_slot)) {
- /* Automatically generated code for commit point define: Put_Point */
-
- if (true) {
- struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
- cp_define->label_num = 8;
- cp_define->label_name = "Put_Point";
- cp_define->potential_cp_label_num = 3;
- cp_define->potential_label_name = "Write_Val_Point";
- cp_define->interface_num = 1;
- cp_define->is_additional_point = false;
- struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
- annotation_cp_define->type = CP_DEFINE;
- annotation_cp_define->annotation = cp_define;
- cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
- }
-
- if (expVal != NULL) { if ((V == NULL || V == TOMBSTONE) &&
- val_slot != TOMBSTONE)
- chm->_size.fetch_add(1, memory_order_relaxed);
- if (!(V == NULL || V == TOMBSTONE) &&
- val_slot == TOMBSTONE)
- chm->_size.fetch_add(-1, memory_order_relaxed);
- }
- return (V == NULL && expVal != NULL) ? TOMBSTONE : V;
- }
- V = val(kvs, idx);
- if (is_prime(V))
- return putIfMatch(topmap, chm->copy_slot_and_check(topmap, kvs,
- idx, expVal), key_slot, val_slot, expVal);
- }
- }
-
- kvs_data* help_copy(kvs_data *helper) {
-
- kvs_data *topkvs = _kvs.load(memory_order_acquire);
- CHM *topchm = get_chm(topkvs);
- if (topchm->_newkvs.load(memory_order_relaxed) == NULL) return helper;
- topchm->help_copy_impl(this, topkvs, false);
- return helper;
- }
-};
-template<typename TypeK, typename TypeV>
-void** cliffc_hashtable<TypeK, TypeV>::func_ptr_table;
-template<typename TypeK, typename TypeV>
-anno_hb_init** cliffc_hashtable<TypeK, TypeV>::hb_init_table;
-template<typename TypeK, typename TypeV>
-spec_table * cliffc_hashtable<TypeK, TypeV>::map;
-template<typename TypeK, typename TypeV>
-spec_table * cliffc_hashtable<TypeK, TypeV>::id_map;
-template<typename TypeK, typename TypeV>
-id_tag_t * cliffc_hashtable<TypeK, TypeV>::tag;
-
-
-#endif
-
projects / cdsspec-compiler.git / blobdiff