X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=concurrent-hashmap%2Fhashmap.h;h=8e6f196cb0e8c73d8a02f9dee01b152dddea7cc9;hb=1438eb7c0715e53611a717e593bfa3fe1bd30588;hp=8e9a06da705dd12ba3f503cb3c976b980ca1456f;hpb=05fe3d047f4a969591fe47c55735565186415760;p=model-checker-benchmarks.git

diff --git a/concurrent-hashmap/hashmap.h b/concurrent-hashmap/hashmap.h
index 8e9a06d..8e6f196 100644
--- 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