return res;
}
}
-
- @Interface_cluster:
- Read_interface = {
- Get,
- PutIfAbsent,
- RemoveAny,
- RemoveIfMatch,
- ReplaceAny,
- ReplaceIfMatch
- }
-
- Write_interface = {
- Put,
- PutIfAbsent(COND_PutIfAbsentSucc),
- RemoveAny,
- RemoveIfMatch(COND_RemoveIfMatchSucc),
- ReplaceAny,
- ReplaceIfMatch(COND_ReplaceIfMatchSucc)
- }
@Happens_before:
- //Write_interface -> Read_interface
Put->Get
Put->Put
@End
kvs_data* resize(cliffc_hashtable *topmap, kvs_data *kvs) {
//model_print("resizing...\n");
+ /**** FIXME: miss ****/
kvs_data *newkvs = _newkvs.load(memory_order_acquire);
if (newkvs != NULL)
return newkvs;
if (newsz < oldlen) newsz = oldlen;
// Last check cause the 'new' below is expensive
+ /**** FIXME: miss ****/
newkvs = _newkvs.load(memory_order_acquire);
//model_print("hey1\n");
if (newkvs != NULL) return newkvs;
kvs_data *cur_newkvs;
// Another check after the slow allocation
+ /**** FIXME: miss ****/
if ((cur_newkvs = _newkvs.load(memory_order_acquire)) != NULL)
return cur_newkvs;
// CAS the _newkvs to the allocated table
kvs_data *desired = (kvs_data*) NULL;
kvs_data *expected = (kvs_data*) newkvs;
+ /**** FIXME: miss ****/
+ //model_print("release in resize!\n");
if (!_newkvs.compare_exchange_strong(desired, expected, memory_order_release,
memory_order_relaxed)) {
// Should clean the allocated area
delete newkvs;
+ /**** FIXME: miss ****/
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);
+ /**** FIXME: miss ****/
kvs_data *newkvs = _newkvs.load(memory_order_acquire);
int oldlen = oldkvs->_size;
int min_copy_work = oldlen > 1024 ? 1024 : oldlen;
copyidx = _copy_idx.load(memory_order_relaxed);
while (copyidx < (oldlen << 1) &&
!_copy_idx.compare_exchange_strong(copyidx, copyidx +
- min_copy_work, memory_order_release, memory_order_relaxed))
+ min_copy_work, memory_order_relaxed, memory_order_relaxed))
copyidx = _copy_idx.load(memory_order_relaxed);
if (!(copyidx < (oldlen << 1)))
panic_start = copyidx;
kvs_data* copy_slot_and_check(cliffc_hashtable *topmap, kvs_data
*oldkvs, int idx, void *should_help) {
+ /**** FIXME: miss ****/
kvs_data *newkvs = _newkvs.load(memory_order_acquire);
// We're only here cause the caller saw a Prime
if (copy_slot(topmap, idx, oldkvs, newkvs))
// Promote the new table to the current table
if (copyDone + workdone == oldlen &&
topmap->_kvs.load(memory_order_relaxed) == oldkvs) {
+ /**** FIXME: miss ****/
kvs_data *newkvs = _newkvs.load(memory_order_acquire);
+ /**** CDSChecker error ****/
topmap->_kvs.compare_exchange_strong(oldkvs, newkvs, memory_order_release,
memory_order_relaxed);
}
/**
@Begin
@Interface: Get
- @Commit_point_set: Get_Success_Point1 | Get_Success_Point2 | Get_Success_Point3
+ //@Commit_point_set: Get_Point1 | Get_Point2 | Get_Point3 | Get_ReadKVS
+ @Commit_point_set: Get_Point1 | Get_Point2 | Get_Point3
@ID: getKeyTag(key)
@Action:
TypeV *_Old_Val = (TypeV*) spec_table_get(map, key);
TypeV* get(TypeK *key) {
slot *key_slot = new slot(false, key);
int fullhash = hash(key_slot);
+ /**** CDSChecker error ****/
kvs_data *kvs = _kvs.load(memory_order_acquire);
+ /**
+ //@Begin
+ @Commit_point_define_check: true
+ @Label: Get_ReadKVS
+ @End
+ */
slot *V = get_impl(this, kvs, key_slot, fullhash);
if (V == NULL) return NULL;
MODEL_ASSERT (!is_prime(V));
/**
@Begin
@Interface: Put
- @Commit_point_set: Write_Success_Point
+ @Commit_point_set: Put_Point
@ID: getKeyTag(key)
@Action:
# Remember this old value at checking point
MODEL_ASSERT (idx >= 0 && idx < kvs->_size);
// Corresponding to the volatile read in get_impl() and putIfMatch in
// Cliff Click's Java implementation
+ /**** CDSChecker error & hb violation ****/
slot *res = (slot*) kvs->_data[idx * 2 + 3].load(memory_order_acquire);
/**
@Begin
// Together with key() preserve the happens-before relationship on newly
// inserted keys
static inline bool CAS_key(kvs_data *kvs, int idx, void *expected, void *desired) {
- return kvs->_data[2 * idx + 2].compare_exchange_strong(expected,
+ bool res = kvs->_data[2 * idx + 2].compare_exchange_strong(expected,
desired, memory_order_relaxed, memory_order_relaxed);
+ /**
+ # If it is a successful put instead of a copy or any other internal
+ # operantions, expected != NULL
+ @Begin
+ @Potential_commit_point_define: res
+ @Label: Write_Key_Point
+ @End
+ */
+ return res;
}
/**
// inserted values
static inline bool CAS_val(kvs_data *kvs, int idx, void *expected, void
*desired) {
+ /**** CDSChecker error & HB violation ****/
bool res = kvs->_data[2 * idx + 3].compare_exchange_strong(expected,
desired, memory_order_acq_rel, memory_order_relaxed);
/**
@Begin
@Commit_point_define: K == NULL
@Potential_commit_point_label: Read_Key_Point
- @Label: Get_Success_Point_1
+ @Label: Get_Point1
@End
*/
slot *V = val(kvs, idx);
-
if (K == NULL) {
//model_print("Key is null\n");
return NULL; // A miss
@Begin
@Commit_point_define: true
@Potential_commit_point_label: Read_Val_Point
- @Label: Get_Success_Point_2
+ @Label: Get_Point2
@End
*/
return (V == TOMBSTONE) ? NULL : V; // Return this value
key_slot == TOMBSTONE) {
// Retry in new table
// Atomic read can be here
+ /**** FIXME: miss ****/
kvs_data *newkvs = chm->_newkvs.load(memory_order_acquire);
/**
@Begin
@Commit_point_define_check: newkvs == NULL
- @Label: Get_Success_Point_3
+ @Label: Get_Point3
@End
*/
return newkvs == NULL ? NULL : get_impl(topmap,
slot *key_slot = new slot(false, key);
slot *value_slot = new slot(false, value);
+ /**** FIXME: miss ****/
kvs_data *kvs = _kvs.load(memory_order_acquire);
+ /**
+ //@Begin
+ @Commit_point_define_check: true
+ @Label: Put_ReadKVS
+ @End
+ */
slot *res = putIfMatch(this, kvs, key_slot, value_slot, old_val);
// Only when copy_slot() call putIfMatch() will it return NULL
MODEL_ASSERT (res != NULL);
// Here it tries to resize cause it doesn't want other threads to stop
// its progress (eagerly try to resize soon)
+ /**** FIXME: miss ****/
newkvs = chm->_newkvs.load(memory_order_acquire);
if (newkvs == NULL &&
((V == NULL && chm->table_full(reprobe_cnt, len)) || is_prime(V))) {
!(V == NULL && expVal == TOMBSTONE) &&
(expVal == NULL || !valeq(expVal, V))) {
/**
- @Begin
+ //@Begin
@Commit_point_define: expVal == TOMBSTONE
@Potential_commit_point_label: Read_Val_Point
@Label: PutIfAbsent_Fail_Point
@End
*/
/**
- @Begin
+ //@Begin
@Commit_point_define: expVal != NULL && val_slot == TOMBSTONE
@Potential_commit_point_label: Read_Val_Point
@Label: RemoveIfMatch_Fail_Point
@End
*/
/**
- @Begin
+ //@Begin
@Commit_point_define: expVal != NULL && !valeq(expVal, V)
@Potential_commit_point_label: Read_Val_Point
@Label: ReplaceIfMatch_Fail_Point
# The only point where a successful put happens
@Commit_point_define: true
@Potential_commit_point_label: Write_Val_Point
- @Label: Write_Success_Point
+ @Label: Put_Point
@End
*/
if (expVal != NULL) { // Not called by a table-copy
// Help along an existing table-resize. This is a fast cut-out wrapper.
kvs_data* help_copy(kvs_data *helper) {
+ /**** FIXME: miss ****/
kvs_data *topkvs = _kvs.load(memory_order_acquire);
CHM *topchm = get_chm(topkvs);
// No cpy in progress
projects / cdsspec-compiler.git / blobdiff