From: Peizhao Ou <peizhaoo@uci.edu>
Date: Sat, 7 Feb 2015 20:21:59 +0000 (-0800)
Subject: changed
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=4e0f2d853f0fba6224b1fe29a36ba8139dd50958;p=model-checker-benchmarks.git

changed
---

diff --git a/concurrent-hashmap/hashmap.h b/concurrent-hashmap/hashmap.h
index 3014c70..a66005c 100644
--- a/concurrent-hashmap/hashmap.h
+++ b/concurrent-hashmap/hashmap.h
@@ -14,6 +14,8 @@
 #include <stdlib.h>
 #include <mutex>
 
+#include "cdsannotate.h"
+
 #define relaxed memory_order_relaxed
 #define release memory_order_release
 #define acquire memory_order_acquire
@@ -157,6 +159,11 @@ 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
+		
 		Entry *firstPtr = first->load(acquire);
 		e = firstPtr;
 		while (e != NULL) {
@@ -183,6 +190,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 +274,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);
diff --git a/mpmc-queue/mpmc-queue.h b/mpmc-queue/mpmc-queue.h
index 47af8ea..fa5f37a 100644
--- a/mpmc-queue/mpmc-queue.h
+++ b/mpmc-queue/mpmc-queue.h
@@ -27,6 +27,8 @@ public:
 	//-----------------------------------------------------
 
 	t_element * read_fetch() {
+		// FIXME: We can have a relaxed for sure here since the next CAS
+		// will fix the problem
 		unsigned int rdwr = m_rdwr.load(mo_acquire);
 		unsigned int rd,wr;
 		for(;;) {
@@ -35,7 +37,7 @@ public:
 
 			if ( wr == rd ) // empty
 				return NULL;
-
+	
 			if ( m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel) )
 				break;
 			else
@@ -60,6 +62,8 @@ public:
 	//-----------------------------------------------------
 
 	t_element * write_prepare() {
+		// FIXME: We can have a relaxed for sure here since the next CAS
+		// will fix the problem
 		unsigned int rdwr = m_rdwr.load(mo_acquire);
 		unsigned int rd,wr;
 		for(;;) {