X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=benchmark%2Fconcurrent-hashmap%2Fhashmap.h;h=99973e3cedc0cefcd007fdd6abcf80d4188472ff;hp=0d249251ec99dcaabbd10d301df8873a5f3a9cc1;hb=7537757f9cbddcfa61076053bea0bddad28e37ad;hpb=61f78baa3c639e3c9ea58c209d2446c7005fdd32;ds=sidebyside diff --git a/benchmark/concurrent-hashmap/hashmap.h b/benchmark/concurrent-hashmap/hashmap.h index 0d24925..99973e3 100644 --- a/benchmark/concurrent-hashmap/hashmap.h +++ b/benchmark/concurrent-hashmap/hashmap.h @@ -4,18 +4,17 @@ #include #include #include "stdio.h" -//#include -#ifdef STANDALONE -#include -#define MODEL_ASSERT assert -#else -#include -#endif #include #include +#include +#include +#include +#include +#include "common.h" + + #include "common.h" -#include "sc_annotation.h" #define relaxed memory_order_relaxed #define release memory_order_release @@ -26,63 +25,17 @@ using namespace std; /** - For the sake of simplicity, we do not use template but some toy structs to - represent the Key and Value. + For the sake of simplicity, we map Integer -> Integer. */ -struct Key { - // Probably represent the coordinate (x, y, z) - int x; - int y; - int z; - - int hashCode() { - return x + 31 * y + 31 * 31 * z; - } - - bool equals(Key *other) { - if (!other) - return false; - return x == other->x && y == other->y && z == other->z; - } - - Key(int x, int y, int z) : - x(x), - y(y), - z(z) - { - - } -}; - -struct Value { - // Probably represent the speed vector (vX, vY, vZ) - int vX; - int vY; - int vZ; - - Value(int vX, int vY, int vZ) : - vX(vX), - vY(vY), - vZ(vZ) - { - - } - - bool equals(Value *other) { - if (!other) - return false; - return vX == other->vX && vY == other->vY && vZ == other->vZ; - } -}; class Entry { public: - Key *key; - atomic value; + int key; + atomic_int value; int hash; atomic next; - Entry(int h, Key *k, Value *v, Entry *n) { + Entry(int h, int k, int v, Entry *n) { this->hash = h; this->key = k; this->value.store(v, relaxed); @@ -108,14 +61,41 @@ class Segment { } }; +/** + @Begin + @Class_begin + @End +*/ class HashMap { public: + + /** + @Begin + @Options: + LANG = CPP; + CLASS = HashMap; + @Global_define: + @DeclareVar: + IntegerMap *__map; + @InitVar: + __map = createIntegerMap(); + @Finalize: + if (__map) + destroyIntegerMap(__map); + return true; + @Happens_before: Put -> Get + @Commutativity: Put <-> Put: _Method1.key != _Method2.key + @Commutativity: Put <-> Get: _Method1.key != _Method2.key + @Commutativity: Get <-> Get: true + @End + */ + atomic *table; int capacity; int size; - static const int CONCURRENCY_LEVEL = 16; + static const int CONCURRENCY_LEVEL = 4; static const int SEGMENT_MASK = CONCURRENCY_LEVEL - 1; @@ -126,6 +106,11 @@ class HashMap { // Not gonna consider resize now... HashMap() { + /** + @Begin + @Entry_point + @End + */ this->size = 0; this->capacity = DEFAULT_INITIAL_CAPACITY; this->table = new atomic[capacity]; @@ -137,19 +122,25 @@ class HashMap { } } - int hashKey(Key *x) { - int h = x->hashCode(); - // Use logical right shift - unsigned int tmp = (unsigned int) h; - return ((h << 7) - h + (tmp >> 9) + (tmp >> 17)); - } - - bool eq(Key *x, Key *y) { - return x == y || x->equals(y); + int hashKey(int key) { + return key; } + - Value* get(Key *key) { - MODEL_ASSERT (key); + /** + @Begin + @Interface: Get + @Commit_point_set: GetReadValue1 | GetReadValue2 | GetReadNothing + @ID: __RET__ + @Action: + int res = getIntegerMap(__map, key); + //model_print("Get: key=%d, res=%d\n", key, res); + + @Post_check: __RET__ ? res == __RET__: true + @End + */ + int get(int key) { + ASSERT (key); int hash = hashKey(key); // Try first without locking... @@ -157,7 +148,7 @@ class HashMap { int index = hash & (capacity - 1); atomic *first = &tab[index]; Entry *e; - Value *res = NULL; + int res = 0; // Should be a load acquire // This load action here makes it problematic for the SC analysis, what @@ -165,15 +156,21 @@ class HashMap { // lock, we ignore this operation for the SC analysis, and otherwise we // take it into consideration - SC_BEGIN(); + /**** UL (main.cc) ****/ Entry *firstPtr = first->load(acquire); - SC_END(); e = firstPtr; while (e != NULL) { - if (e->hash == hash && eq(key, e->key)) { + if (key, e->key) { + /**** inadmissible (testcase1.cc) ****/ res = e->value.load(seq_cst); - if (res != NULL) + /** + @Begin + @Commit_point_define_check: res != 0 + @Label: GetReadValue1 + @End + */ + if (res != 0) return res; else break; @@ -193,9 +190,15 @@ class HashMap { if (e != NULL || firstPtr != newFirstPtr) { e = newFirstPtr; while (e != NULL) { - if (e->hash == hash && eq(key, e->key)) { + if (key == e->key) { // Protected by lock, no need to be SC res = e->value.load(relaxed); + /** + @Begin + @Commit_point_define_check: true + @Label: GetReadValue2 + @End + */ seg->unlock(); // Critical region ends return res; } @@ -204,13 +207,27 @@ class HashMap { } } seg->unlock(); // Critical region ends - return NULL; + /** + @Begin + @Commit_point_define_check: true + @Label: GetReadNothing + @End + */ + return 0; } - Value* put(Key *key, Value *value) { - // Don't allow NULL key or value - MODEL_ASSERT (key && value); - + /** + @Begin + @Interface: Put + @Commit_point_set: PutUpdateValue | PutInsertValue + @ID: value + @Action: + putIntegerMap(__map, key, value); + //model_print("Put: key=%d, val=%d\n", key, value); + @End + */ + int put(int key, int value) { + ASSERT (key && value); int hash = hashKey(key); Segment *seg = segments[hash & SEGMENT_MASK]; atomic *tab; @@ -221,17 +238,25 @@ class HashMap { atomic *first = &tab[index]; Entry *e; - Value *oldValue = NULL; + int oldValue = 0; // The written of the entry is synchronized by locking Entry *firstPtr = first->load(relaxed); e = firstPtr; while (e != NULL) { - if (e->hash == hash && eq(key, e->key)) { - // FIXME: This could be a relaxed (because locking synchronize - // with the previous put())?? no need to be acquire + if (key == e->key) { + // This could be a relaxed (because locking synchronize + // with the previous put()), no need to be acquire oldValue = e->value.load(relaxed); + + /**** inadmissible (testcase1.cc) ****/ e->value.store(value, seq_cst); + /** + @Begin + @Commit_point_define_check: true + @Label: PutUpdateValue + @End + */ seg->unlock(); // Don't forget to unlock before return return oldValue; } @@ -241,68 +266,31 @@ class HashMap { // Add to front of list Entry *newEntry = new Entry(hash, key, value, firstPtr); + + /**** UL (main.cc) ****/ // Publish the newEntry to others first->store(newEntry, release); + /** + @Begin + @Commit_point_clear: true + @Label: PutClear + @End + */ + + /** + @Begin + @Commit_point_define_check: true + @Label: PutInsertValue + @End + */ seg->unlock(); // Critical region ends - return NULL; - } - - Value* remove(Key *key, Value *value) { - MODEL_ASSERT (key); - int hash = hashKey(key); - Segment *seg = segments[hash & SEGMENT_MASK]; - atomic *tab; - - seg->lock(); // Critical region begins - tab = table; - int index = hash & (capacity - 1); - - atomic *first = &tab[index]; - Entry *e; - Value *oldValue = NULL; - - // The written of the entry is synchronized by locking - Entry *firstPtr = first->load(relaxed); - e = firstPtr; - - while (true) { - if (e != NULL) { - seg->unlock(); // Don't forget to unlock - return NULL; - } - if (e->hash == hash && eq(key, e->key)) - break; - // Synchronized by locking - e = e->next.load(relaxed); - } - - // FIXME: This could be a relaxed (because locking synchronize - // with the previous put())?? No need to be acquire - oldValue = e->value.load(relaxed); - // If the value parameter is NULL, we will remove the entry anyway - if (value != NULL && value->equals(oldValue)) { - seg->unlock(); - return NULL; - } - - // Force the get() to grab the lock and retry - e->value.store(NULL, relaxed); - - // The strategy to remove the entry is to keep the entries after the - // removed one and copy the ones before it - Entry *head = e->next.load(relaxed); - Entry *p; - p = first->load(relaxed); - while (p != e) { - head = new Entry(p->hash, p->key, p->value.load(relaxed), head); - p = p->next.load(relaxed); - } - - // Publish the new head to readers - first->store(head, release); - seg->unlock(); // Critical region ends - return oldValue; + return 0; } }; +/** + @Begin + @Class_end + @End +*/ #endif