edits

[cdsspec-compiler.git] / benchmark / concurrent-hashmap / hashmap.h

diff --git a/benchmark/concurrent-hashmap/hashmap.h b/benchmark/concurrent-hashmap/hashmap.h
index 0d249251ec99dcaabbd10d301df8873a5f3a9cc1..99973e3cedc0cefcd007fdd6abcf80d4188472ff 100644 (file)
--- a/benchmark/concurrent-hashmap/hashmap.h
+++ b/benchmark/concurrent-hashmap/hashmap.h
@@ -4,18 +4,17 @@
 #include <iostream>
 #include <atomic>
 #include "stdio.h" 
 #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 <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 "common.h"

-#include "sc_annotation.h"

 
 #define relaxed memory_order_relaxed
 #define release memory_order_release
 
 #define relaxed memory_order_relaxed
 #define release memory_order_release


@@ -26,63 +25,17 @@
 using namespace std;
 
 /**
 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:
 
 class Entry {
        public:

-       Key *key;
-       atomic<Value*> value;
+       int key;
+       atomic_int value;

        int hash;
        atomic<Entry*> next;
 
        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);
                this->hash = h;
                this->key = k;
                this->value.store(v, relaxed);


@@ -108,14 +61,41 @@ class Segment {
        }
 };
 
        }
 };
 

+/**
+    @Begin
+       @Class_begin
+       @End
+*/

 class HashMap {
        public:
 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;
 
        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;
 
 
        static const int SEGMENT_MASK = CONCURRENCY_LEVEL - 1;
 


@@ -126,6 +106,11 @@ class HashMap {
        // Not gonna consider resize now...
        
        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];
                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...
                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;
                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
 
                // 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
                
                // 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);
                Entry *firstPtr = first->load(acquire);

-               SC_END();

 
                e = firstPtr;
                while (e != NULL) {
 
                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);
                                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;
                                        return res;
                                else
                                        break;


@@ -193,9 +190,15 @@ class HashMap {
                if (e != NULL || firstPtr != newFirstPtr) {
                        e = newFirstPtr;
                        while (e != NULL) {
                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);
                                        // 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;
                                }
                                        seg->unlock(); // Critical region ends
                                        return res;
                                }


@@ -204,13 +207,27 @@ class HashMap {
                        }
                }
                seg->unlock(); // Critical region ends
                        }
                }
                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;
                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;
 
                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) {
        
                // 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);
                                oldValue = e->value.load(relaxed);

+                               
+                               /**** inadmissible (testcase1.cc) ****/

                                e->value.store(value, seq_cst);
                                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;
                        }
                                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);
 
                // 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);
                // 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
                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
 
 #endif