edits
[cdsspec-compiler.git] / benchmark / concurrent-hashmap / hashmap.h
index 0d24925..99973e3 100644 (file)
@@ -4,18 +4,17 @@
 #include <iostream>
 #include <atomic>
 #include "stdio.h" 
-//#include <common.h>
-#ifdef STANDALONE
-#include <assert.h>
-#define MODEL_ASSERT assert 
-#else
-#include <model-assert.h>
-#endif
 #include <stdlib.h>
 #include <mutex>
 
+#include <spec_lib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h" 
+
+
 #include "common.h"
-#include "sc_annotation.h"
 
 #define relaxed memory_order_relaxed
 #define release memory_order_release
 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*> value;
+       int key;
+       atomic_int value;
        int hash;
        atomic<Entry*> 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<Entry*> *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<Entry*>[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<Entry*> *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<Entry*> *tab;
@@ -221,17 +238,25 @@ class HashMap {
 
                atomic<Entry*> *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<Entry*> *tab;
-
-               seg->lock(); // Critical region begins
-               tab = table;
-               int index = hash & (capacity - 1);
-
-               atomic<Entry*> *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