minor fix to hashtable spec
authorPeizhao Ou <peizhaoo@uci.edu>
Wed, 5 Feb 2014 00:47:23 +0000 (16:47 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Wed, 5 Feb 2014 00:47:23 +0000 (16:47 -0800)
benchmark/cliffc-hashtable/cliffc_hashtable.h
benchmark/cliffc-hashtable/main.cc

index 49dc728..756cbb9 100644 (file)
@@ -3,8 +3,13 @@
 
 #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;
 
@@ -69,6 +74,11 @@ struct slot {
        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 {
        /**
@@ -78,34 +88,59 @@ 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;
                                }
                        }
                
@@ -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(TypeKkey) {
+       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
index cadedce..cecaa0c 100644 (file)
@@ -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<IntWrapper, IntWrapper> *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<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) {
@@ -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;
 }
+