#include <iostream>
#include <atomic>
-#include <common.h>
+//#include <common.h>
+#ifdef STANDALONE
+#include <assert.h>
+#define MODEL_ASSERT assert
+#else
#include <model-assert.h>
+#endif
using namespace std;
used to judge equality.
TypeK and TypeV should define their own copy constructor.
*/
+/**
+ @Begin
+ @Class_begin
+ @End
+*/
template<typename TypeK, typename TypeV>
class cliffc_hashtable {
/**
@Begin
@Options:
- LANG = C;
+ LANG = CPP;
CLASS = cliffc_hashtable;
@Global_define:
@DeclareVar:
- spec_hashtable<TypeK, TypeV*> map;
- spec_hashtable<TypeK, Tag> id_map;
- Tag tag;
+ spec_table *map;
+ spec_table *id_map;
+ id_tag_t *tag;
@InitVar:
- map = spec_hashtable<TypeK, TypeV*>();
- id_map = spec_hashtable<TypeK, TypeV*>();
- tag = Tag();
+ map = new_spec_table_default(equals_key);
+ id_map = new_spec_table_default(equals_id);
+ tag = new_id_tag();
+
@DefineFunc:
- bool equals_val(TypeV *ptr1, TypeV *ptr2) {
- // ...
+ 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);
}
+ @DefineFunc:
+ bool equals_val(void *ptr1, void *ptr2) {
+ TypeV *val1 = (TypeV*) ptr1,
+ *val2 = (TypeV*) ptr2;
+ if (val1 == NULL || val2 == NULL)
+ return false;
+ return val1->equals(val2);
+ }
+
+ @DefineFunc:
+ 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 == *id2;
+ }
+
@DefineFunc:
# Update the tag for the current key slot if the corresponding tag
# is NULL, otherwise just return that tag. It will update the next
# available tag too if it requires a new tag for that key slot.
- Tag getKeyTag(TypeK &key) {
- if (id_map.get(key) == NULL) {
- Tag cur_tag = tag.current();
- id_map.put(key, cur_tag);
- tag.next();
+ id_tag_t getKeyTag(TypeK *key) {
+ if (spec_table_contains(id_map, key)) {
+ id_tag_t *cur_tag = MODEL_MALLOC(sizeof(id_tag_t));
+ *cur_tag = current(tag);
+ spec_table_put(id_map, key, cur_tag);
+ next(tag);
return cur_tag;
} else {
- return id_map.get(key);
+ id_tag_t *res = (id_tag_t*) spec_table_get(id_map, key);
+ return *res;
}
}
/**
@Begin
@Interface: Get
- @Commit_point_set: Read_Val_Point1 | Read_Val_Point2 | Read_Val_Point3
- @ID: __sequential.getKeyTag(key)
+ @Commit_point_set: Get_Success_Point1 | Get_Success_Point2 | Get_Success_Point3
+ @ID: getKeyTag(key)
@Action:
- TypeV *_Old_Val = __sequential.map.get(key)
+ void *_Old_Val = spec_table_get(map, key);
@Post_check:
- __sequential.equals_val(_Old_Val, __RET__)
+ equals_val(_Old_Val, __RET__)
@End
*/
- TypeV* get(TypeK& key) {
- void *key_ptr = (void*) new TypeK(key);
- slot *key_slot = new slot(false, key_ptr);
+ TypeV* 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);
/**
@Begin
@Interface: Put
- @Commit_point_set: Write_Val_Point
- @ID: __sequential.getKeyTag(key)
+ @Commit_point_set: Write_Success_Point
+ @ID: getKeyTag(key)
@Action:
# Remember this old value at checking point
- TypeV *_Old_Val = __sequential.map.get(key)
- __sequential.map.put(key, &val);
+ void *_Old_Val = spec_table_get(map, key);
+ spec_table_put(map, key, val);
@Post_check:
- __sequential.equals_val(__RET__, _Old_Val)
+ equals_val(__RET__, _Old_Val)
@End
*/
- TypeV* put(TypeK& key, TypeV& val) {
+ TypeV* put(TypeK *key, TypeV *val) {
return putIfMatch(key, val, NO_MATCH_OLD);
}
@Begin
@Interface: PutIfAbsent
@Commit_point_set:
- Write_Val_Point | PutIfAbsent_Fail_Point
- @Condition: __sequential.map.get(key) == NULL
+ Write_Success_Point | PutIfAbsent_Fail_Point
+ @Condition: !spec_table_contains(map, key)
@HB_condition:
COND_PutIfAbsentSucc :: __RET__ == NULL
- @ID: __sequential.getKeyTag(key)
+ @ID: getKeyTag(key)
@Action:
- TypeV *_Old_Val = __sequential.map.get(key)
+ void *_Old_Val = spec_table_get(map, key);
if (__COND_SAT__)
- __sequential.map.put(key, &value);
+ spec_table_put(map, key, value);
@Post_check:
- __COND_SAT__ ? __RET__ == NULL : __sequential.equals_val(_Old_Val, __RET__)
+ __COND_SAT__ ? __RET__ == NULL : equals_val(_Old_Val, __RET__)
@End
*/
- TypeV* putIfAbsent(TypeK& key, TypeV& value) {
+ TypeV* putIfAbsent(TypeK *key, TypeV *value) {
return putIfMatch(key, val, TOMBSTONE);
}
/**
@Begin
@Interface: RemoveAny
- @Commit_point_set: Write_Val_Point
- @ID: __sequential.getKeyTag(key)
+ @Commit_point_set: Write_Success_Point
+ @ID: getKeyTag(key)
@Action:
- TypeV *_Old_Val = __sequential.map.get(key)
- __sequential.map.put(key, NULL);
+ void *_Old_Val = spec_table_get(map, key);
+ spec_table_put(map, key, NULL);
@Post_check:
- __sequential.equals_val(__RET__, _Old_Val)
+ equals_val(__RET__, _Old_Val)
@End
*/
- TypeV* remove(TypeK& key) {
+ TypeV* remove(TypeK *key) {
return putIfMatch(key, TOMBSTONE, NO_MATCH_OLD);
}
@Begin
@Interface: RemoveIfMatch
@Commit_point_set:
- Write_Val_Point | RemoveIfMatch_Fail_Point
+ Write_Success_Point | RemoveIfMatch_Fail_Point
@Condition:
- __sequential.equals_val(__sequential.map.get(key), &val)
+ equals_val(spec_table_get(map, key), val)
@HB_condition:
COND_RemoveIfMatchSucc :: __RET__ == true
- @ID: __sequential.getKeyTag(key)
+ @ID: getKeyTag(key)
@Action:
if (__COND_SAT__)
- __sequential.map.put(key, NULL);
+ spec_table_put(map, key, NULL);
@Post_check:
__COND_SAT__ ? __RET__ : !__RET__
@End
*/
- bool remove(TypeK& key, TypeV& val) {
+ bool remove(TypeK *key, TypeV *val) {
slot *val_slot = val == NULL ? NULL : new slot(false, val);
return putIfMatch(key, TOMBSTONE, val) == val;
@Begin
@Interface: ReplaceAny
@Commit_point_set:
- Write_Val_Point
- @ID: __sequential.getKeyTag(key)
+ Write_Success_Point
+ @ID: getKeyTag(key)
@Action:
- TypeV *_Old_Val = __sequential.map.get(key)
+ void *_Old_Val = spec_table_get(map, key);
@Post_check:
- __sequential.equals_val(__RET__, _Old_Val)
+ equals_val(__RET__, _Old_Val)
@End
*/
- TypeV* replace(TypeK& key, TypeV& val) {
+ TypeV* replace(TypeK *key, TypeV *val) {
return putIfMatch(key, val, MATCH_ANY);
}
@Begin
@Interface: ReplaceIfMatch
@Commit_point_set:
- Write_Val_Point | ReplaceIfMatch_Fail_Point
+ Write_Success_Point | ReplaceIfMatch_Fail_Point
@Condition:
- __sequential.equals_val(__sequential.map.get(key), &oldval)
+ equals_val(spec_table_get(map, key), oldval)
@HB_condition:
COND_ReplaceIfMatchSucc :: __RET__ == true
- @ID: __sequential.getKeyTag(key)
+ @ID: getKeyTag(key)
@Action:
if (__COND_SAT__)
- __sequential.map.put(key, &newval);
+ spec_table_put(map, key, newval);
@Post_check:
__COND_SAT__ ? __RET__ : !__RET__
@End
*/
- bool replace(TypeK& key, TypeV& oldval, TypeV& newval) {
+ bool replace(TypeK *key, TypeV *oldval, TypeV *newval) {
return putIfMatch(key, newval, oldval) == oldval;
}
# If it is a successful put instead of a copy or any other internal
# operantions, expected != NULL
@Begin
- @Potential_commit_point_define: __ATOMIC_RET__ == true
+ @Potential_commit_point_define: res == true
@Label: Write_Val_Point
@End
*/
}
// A wrapper of the essential function putIfMatch()
- TypeV* putIfMatch(TypeK& key, TypeV& value, slot *old_val) {
+ TypeV* putIfMatch(TypeK *key, TypeV *value, slot *old_val) {
// TODO: Should throw an exception rather return NULL
if (old_val == NULL) {
return NULL;
}
- void *key_ptr = (void*) new TypeK(key);
- slot *key_slot = new slot(false, key_ptr);
+ slot *key_slot = new slot(false, key);
- void *val_ptr = (void*) new TypeV(value);
- slot *value_slot = new slot(false, val_ptr);
+ 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);
// Only when copy_slot() call putIfMatch() will it return NULL
return helper;
}
};
+/**
+ @Begin
+ @Class_end
+ @End
+*/
#endif
int hashCode() {
return _val;
}
+
+ bool operator==(const IntWrapper& rhs) {
+ return false;
+ }
bool equals(const void *another) {
if (another == NULL)
IntWrapper *val1, *val2;
void threadA(void *arg) {
- /*
- IntWrapper k1(3), k2(5), k3(1024), k4(1025);
- IntWrapper v1(1), v2(2), v3(73), v4(81);
+ IntWrapper *k1 = new IntWrapper(3), *k2 = new IntWrapper(5),
+ *k3 = new IntWrapper(1024), *k4 = new IntWrapper(1025);
+ IntWrapper *v1 = new IntWrapper(1024), *v2 = new IntWrapper(1025),
+ *v3 = new IntWrapper(73), *v4 = new IntWrapper(81);
table->put(k1, v1);
table->put(k2, v2);
val1 = table->get(k3);
table->put(k3, v3);
- */
- for (int i = 200; i < 205; i++) {
- IntWrapper k(i), v(i * 2);
- table->put(k, v);
- }
}
void threadB(void *arg) {
- IntWrapper k1(3), k2(5), k3(1024), k4(1025);
- IntWrapper v1(1), v2(2), v3(73), v4(81);
+ IntWrapper *k1 = new IntWrapper(3), *k2 = new IntWrapper(5),
+ *k3 = new IntWrapper(1024), *k4 = new IntWrapper(1025);
+ IntWrapper *v1 = new IntWrapper(1024), *v2 = new IntWrapper(1025),
+ *v3 = new IntWrapper(73), *v4 = new IntWrapper(81);
table->put(k1, v3);
table->put(k2, v4);
val1 = table->get(k2);
}
void threadC(void *arg) {
- IntWrapper k1(3), k2(5), k3(1024), k4(1025);
- IntWrapper v1(1), v2(2), v3(73), v4(81);
+ IntWrapper *k1 = new IntWrapper(3), *k2 = new IntWrapper(5),
+ *k3 = new IntWrapper(1024), *k4 = new IntWrapper(1025);
+ IntWrapper *v1 = new IntWrapper(1024), *v2 = new IntWrapper(1025),
+ *v3 = new IntWrapper(73), *v4 = new IntWrapper(81);
table->put(k1, v1);
table->put(k2, v2);
val2 = table->get(k1);
}
-void threadD(void *arg) {
- IntWrapper k1(3), k2(5), k3(1024), k4(1025);
- IntWrapper v1(1), v2(2), v3(73), v4(81);
- table->put(k1, v2);
- table->put(k2, v1);
- val2 = table->get(k2);
+void threadMain(void *arg) {
+ for (int i = 200; i < 300; i++) {
+ IntWrapper *k = new IntWrapper(i), *v = new IntWrapper(i * 2);
+ table->put(k, v);
+ }
}
int user_main(int argc, char *argv[]) {
table = new cliffc_hashtable<IntWrapper, IntWrapper>();
val1 = NULL;
val2 = NULL;
+ threadMain(NULL);
+
thrd_create(&t1, threadA, NULL);
thrd_create(&t2, threadB, NULL);
- thrd_create(&t3, threadC, NULL);
+ //thrd_create(&t3, threadC, NULL);
//thrd_create(&t4, threadD, NULL);
thrd_join(t1);
thrd_join(t2);
- thrd_join(t3);
+ //thrd_join(t3);
//thrd_join(t4);
if (val1 == NULL) {
} else {
cout << val1->get() << endl;
}
- MODEL_ASSERT(val1 == NULL || val1->get() == 2 || val1->get() == 81);
+ //MODEL_ASSERT(val1 == NULL || val1->get() == 2 || val1->get() == 81);
if (val2 == NULL) {
cout << "val2: NULL" << endl;
} else {
}
return 0;
}
+
projects / cdsspec-compiler.git / commitdiff