changes to the example

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

diff --git a/concurrent-hashmap/hashmap.h b/concurrent-hashmap/hashmap.h
index 3014c70e84ca16851a9345c8d05a4405a161e640..0d249251ec99dcaabbd10d301df8873a5f3a9cc1 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
@@ -157,7 +160,15 @@ 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_END();
+
                e = firstPtr;
                while (e != NULL) {
                        if (e->hash == hash && eq(key, e->key)) {
@@ -166,9 +177,10 @@ class HashMap {
                                        return res;
                                else
                                        break;
-                               // Loading the next entry
-                               e = e->next.load(acquire);
                        }
+                       // Loading the next entry, this can be relaxed because the
+                       // synchronization has been established by the load of head
+                       e = e->next.load(relaxed);
                }
        
                // Recheck under synch if key apparently not there or interference
@@ -182,7 +194,9 @@ class HashMap {
                        e = newFirstPtr;
                        while (e != NULL) {
                                if (e->hash == hash && eq(key, e->key)) {
-                                       res = e->value.load(seq_cst);
+                                       // Protected by lock, no need to be SC
+                                       res = e->value.load(relaxed);
+                                       seg->unlock(); // Critical region ends
                                        return res;
                                }
                                // Synchronized by locking
@@ -215,8 +229,8 @@ class HashMap {
                while (e != NULL) {
                        if (e->hash == hash && eq(key, e->key)) {
                                // FIXME: This could be a relaxed (because locking synchronize
-                               // with the previous put())?? 
-                               oldValue = e->value.load(acquire);
+                               // with the previous put())??  no need to be acquire
+                               oldValue = e->value.load(relaxed);
                                e->value.store(value, seq_cst);
                                seg->unlock(); // Don't forget to unlock before return
                                return oldValue;
@@ -263,11 +277,13 @@ class HashMap {
                }
 
                // FIXME: This could be a relaxed (because locking synchronize
-               // with the previous put())?? 
-               oldValue = e->value.load(acquire);
+               // 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))
+               if (value != NULL && value->equals(oldValue)) {
+                       seg->unlock();
                        return NULL;
+               }
 
                // Force the get() to grab the lock and retry
                e->value.store(NULL, relaxed);