From 0ca26c20aad3b1174624f2300d501fabd1cb7c39 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Tue, 4 Feb 2014 16:47:23 -0800 Subject: [PATCH] minor fix to hashtable spec --- benchmark/cliffc-hashtable/cliffc_hashtable.h | 163 +++++++++++------- benchmark/cliffc-hashtable/main.cc | 48 +++--- 2 files changed, 127 insertions(+), 84 deletions(-) diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h index 49dc728..756cbb9 100644 --- a/benchmark/cliffc-hashtable/cliffc_hashtable.h +++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h @@ -3,8 +3,13 @@ #include #include -#include +//#include +#ifdef STANDALONE +#include +#define MODEL_ASSERT assert +#else #include +#endif using namespace std; @@ -69,6 +74,11 @@ struct slot { used to judge equality. TypeK and TypeV should define their own copy constructor. */ +/** + @Begin + @Class_begin + @End +*/ template class cliffc_hashtable { /** @@ -78,34 +88,59 @@ class cliffc_hashtable { @Begin @Options: - LANG = C; + LANG = CPP; CLASS = cliffc_hashtable; @Global_define: @DeclareVar: - spec_hashtable map; - spec_hashtable id_map; - Tag tag; + spec_table *map; + spec_table *id_map; + id_tag_t *tag; @InitVar: - map = spec_hashtable(); - id_map = spec_hashtable(); - 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; } } @@ -365,17 +400,16 @@ friend class CHM; /** @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); @@ -387,17 +421,17 @@ friend class CHM; /** @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); } @@ -405,36 +439,36 @@ friend class CHM; @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); } @@ -442,20 +476,20 @@ friend class CHM; @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; @@ -465,15 +499,15 @@ friend class CHM; @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); } @@ -481,20 +515,20 @@ friend class CHM; @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; } @@ -610,7 +644,7 @@ friend class CHM; # 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 */ @@ -675,16 +709,14 @@ friend class CHM; } // 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 @@ -840,5 +872,10 @@ friend class CHM; return helper; } }; +/** + @Begin + @Class_end + @End +*/ #endif diff --git a/benchmark/cliffc-hashtable/main.cc b/benchmark/cliffc-hashtable/main.cc index cadedce..cecaa0c 100644 --- a/benchmark/cliffc-hashtable/main.cc +++ b/benchmark/cliffc-hashtable/main.cc @@ -35,6 +35,10 @@ class IntWrapper { int hashCode() { return _val; } + + bool operator==(const IntWrapper& rhs) { + return false; + } bool equals(const void *another) { if (another == NULL) @@ -49,42 +53,41 @@ cliffc_hashtable *table; 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[]) { @@ -92,14 +95,16 @@ int user_main(int argc, char *argv[]) { table = new cliffc_hashtable(); 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) { @@ -107,7 +112,7 @@ int user_main(int argc, char *argv[]) { } 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 { @@ -115,3 +120,4 @@ int user_main(int argc, char *argv[]) { } return 0; } + -- 2.34.1