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

diff --git a/concurrent-hashmap/hashmap.h b/concurrent-hashmap/hashmap.h
index 3014c70..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
@@ -157,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)) {
@@ -166,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
@@ -183,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
@@ -266,8 +279,10 @@ class HashMap {
 		// 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))
+		if (value != NULL && value->equals(oldValue)) {
+			seg->unlock();
 			return NULL;
+		}
 
 		// Force the get() to grab the lock and retry
 		e->value.store(NULL, relaxed);