changes

[model-checker-benchmarks.git] / concurrent-hashmap / hashmap.h

diff --git a/concurrent-hashmap/hashmap.h b/concurrent-hashmap/hashmap.h
index 8e9a06da705dd12ba3f503cb3c976b980ca1456f..8e6f196cb0e8c73d8a02f9dee01b152dddea7cc9 100644 (file)
--- a/concurrent-hashmap/hashmap.h
+++ b/concurrent-hashmap/hashmap.h
@@ -14,6 +14,9 @@
 #include <stdlib.h>
 #include <mutex>
 
+#include "common.h"
+#include "sc_annotation.h"
+
 #define relaxed memory_order_relaxed
 #define release memory_order_release
 #define acquire memory_order_acquire
@@ -64,6 +67,12 @@ struct Value {
        {
 
        }
+
+       bool equals(Value *other) {
+               if (!other)
+                       return false;
+               return vX == other->vX && vY == other->vY && vZ == other->vZ;
+       }
 };
 
 class Entry {
@@ -140,7 +149,8 @@ class HashMap {
        }
 
        Value* get(Key *key) {
-               int hash = hashKey(key);        // throws null pointer exception if key null
+               MODEL_ASSERT (key);
+               int hash = hashKey(key);
 
                // Try first without locking...
                atomic<Entry*> *tab = table;
@@ -150,7 +160,16 @@ class HashMap {
                Value *res = NULL;
 
                // Should be a load acquire
+               // This load action here makes it problematic for the SC analysis, what
+               // we need to do is as follows: if the get() method ever acquires the
+               // lock, we ignore this operation for the SC analysis, and otherwise we
+               // take it into consideration
+               
+               //SC_BEGIN();
                Entry *firstPtr = first->load(acquire);
+               //SC_KEEP();
+               //SC_END();
+
                e = firstPtr;
                while (e != NULL) {
                        if (e->hash == hash && eq(key, e->key)) {
@@ -159,9 +178,9 @@ class HashMap {
                                        return res;
                                else
                                        break;
-                               // Loading the next entry
-                               e = e->next.load(acquire);
                        }
+                       // Loading the next entry
+                       e = e->next.load(acquire);
                }
        
                // Recheck under synch if key apparently not there or interference
@@ -176,6 +195,7 @@ class HashMap {
                        while (e != NULL) {
                                if (e->hash == hash && eq(key, e->key)) {
                                        res = e->value.load(seq_cst);
+                                       seg->unlock(); // Critical region ends
                                        return res;
                                }
                                // Synchronized by locking
@@ -187,8 +207,8 @@ class HashMap {
        }
 
        Value* put(Key *key, Value *value) {
-               // Don't allow NULL value
-               //ASSERT (value != NULL);
+               // Don't allow NULL key or value
+               MODEL_ASSERT (key && value);
 
                int hash = hashKey(key);
                Segment *seg = segments[hash & SEGMENT_MASK];
@@ -200,19 +220,22 @@ class HashMap {
 
                atomic<Entry*> *first = &tab[index];
                Entry *e;
-               Value *res = NULL;
+               Value *oldValue = 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 an acquire?? 
-                               res = e->value.load(acquire);
+                               // FIXME: This could be a relaxed (because locking synchronize
+                               // with the previous put())?? 
+                               oldValue = e->value.load(acquire);
                                e->value.store(value, seq_cst);
                                seg->unlock(); // Don't forget to unlock before return
-                               return res;
+                               return oldValue;
                        }
+                       // Synchronized by locking
+                       e = e->next.load(relaxed);
                }
 
                // Add to front of list
@@ -222,6 +245,63 @@ class HashMap {
                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())?? 
+               oldValue = e->value.load(acquire);
+               // 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;
+       }
 };
 
 #endif