X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=benchmark%2Fconcurrent-hashmap%2Fhashmap.h;h=904d0b84e9233ce79246c404eec439eb86ebe62e;hp=e813d23fff2cc651a9c0485bb084bbcc612c55f8;hb=fc0b24243f667dc9938d081305aa66dac66dc6ed;hpb=b568a7063faeb671240c8b3a169ea60cee01858e

diff --git a/benchmark/concurrent-hashmap/hashmap.h b/benchmark/concurrent-hashmap/hashmap.h
index e813d23..904d0b8 100644
--- a/benchmark/concurrent-hashmap/hashmap.h
+++ b/benchmark/concurrent-hashmap/hashmap.h
@@ -6,6 +6,14 @@
 #include "stdio.h" 
 #include <stdlib.h>
 #include <mutex>
+
+#include <spec_lib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h" 
+
+
 #include "common.h"
 
 #define relaxed memory_order_relaxed
@@ -20,8 +28,6 @@ using namespace std;
 	For the sake of simplicity, we map Integer -> Integer.
 */
 
-
-
 class Entry {
 	public:
 	int key;
@@ -58,9 +64,32 @@ class Segment {
 /**
     @Begin
 	@Class_begin
-	@End*/
+	@End
+*/
 class HashMap {
 	public:
+
+	/**
+		@Begin
+		@Options:
+			LANG = CPP;
+			CLASS = HashMap;
+		@Global_define:
+			@DeclareVar:
+				IntegerMap *__map;
+			@InitVar:
+				__map = createIntegerMap();
+			@Finalize:
+				if (__map)
+					destroyIntegerMap(__map);
+				return true;
+		@Happens_before: Put -> Get 
+		@Commutativity: Put <-> Put: _Method1.key != _Method2.key 
+		@Commutativity: Put <-> Get: _Method1.key != _Method2.key
+		@Commutativity: Get <-> Get: true 
+		@End
+	*/
+
 	atomic<Entry*> *table;
 
 	int capacity;
@@ -77,6 +106,11 @@ class HashMap {
 	// Not gonna consider resize now...
 	
 	HashMap() {
+		/**
+			@Begin
+			@Entry_point
+			@End
+		*/
 		this->size = 0;
 		this->capacity = DEFAULT_INITIAL_CAPACITY;
 		this->table = new atomic<Entry*>[capacity];
@@ -91,7 +125,20 @@ class HashMap {
 	int hashKey(int key) {
 		return key;
 	}
+	
 
+	/**
+		@Begin
+		@Interface: Get 
+		@Commit_point_set: GetReadValue1 | GetReadEntry | GetReadValue2
+		@ID: __RET__ 
+		@Action:
+			int res = getIntegerMap(__map, key);
+			//model_print("Get: key=%d, res=%d\n", key, res);
+
+		@Post_check: __RET__ ? res == __RET__: true
+		@End
+	*/
 	int get(int key) {
 		ASSERT (key);
 		int hash = hashKey(key);
@@ -109,12 +156,20 @@ class HashMap {
 		// lock, we ignore this operation for the SC analysis, and otherwise we
 		// take it into consideration
 		
+		/**** UL ****/
 		Entry *firstPtr = first->load(acquire);
 
 		e = firstPtr;
 		while (e != NULL) {
 			if (key, e->key) {
+				/**** inadmissible ****/
 				res = e->value.load(seq_cst);
+				/**
+					@Begin
+					@Commit_point_define_check: res != 0
+					@Label: GetReadValue1
+					@End
+				*/
 				if (res != 0)
 					return res;
 				else
@@ -132,12 +187,24 @@ class HashMap {
 
 		// Synchronized by locking, no need to be load acquire
 		Entry *newFirstPtr = first->load(relaxed);
+		/**
+			@Begin
+			@Commit_point_define_check: true 
+			@Label: GetReadEntry
+			@End
+		*/
 		if (e != NULL || firstPtr != newFirstPtr) {
 			e = newFirstPtr;
 			while (e != NULL) {
 				if (key == e->key) {
 					// Protected by lock, no need to be SC
 					res = e->value.load(relaxed);
+					/**
+						@Begin
+						@Commit_point_define_check: true 
+						@Label: GetReadValue2
+						@End
+					*/
 					seg->unlock(); // Critical region ends
 					return res;
 				}
@@ -149,6 +216,16 @@ class HashMap {
 		return 0;
 	}
 
+	/**
+		@Begin
+		@Interface: Put 
+		@Commit_point_set: PutUpdateValue | PutInsertValue
+		@ID: value
+		@Action:
+			putIntegerMap(__map, key, value);
+			//model_print("Put: key=%d, val=%d\n", key, value);
+		@End
+	*/
 	int put(int key, int value) {
 		ASSERT (key && value);
 		int hash = hashKey(key);
@@ -171,7 +248,15 @@ class HashMap {
 				// This could be a relaxed (because locking synchronize
 				// with the previous put()),  no need to be acquire
 				oldValue = e->value.load(relaxed);
+				
+				/**** inadmissible ****/
 				e->value.store(value, seq_cst);
+				/**
+					@Begin
+					@Commit_point_define_check: true 
+					@Label: PutUpdateValue
+					@End
+				*/
 				seg->unlock(); // Don't forget to unlock before return
 				return oldValue;
 			}
@@ -181,11 +266,24 @@ class HashMap {
 
 		// Add to front of list
 		Entry *newEntry = new Entry(hash, key, value, firstPtr);
+		
+		/**** UL ****/
 		// Publish the newEntry to others
 		first->store(newEntry, release);
+		/**
+			@Begin
+			@Commit_point_define_check: true 
+			@Label: PutInsertValue
+			@End
+		*/
 		seg->unlock(); // Critical region ends
 		return 0;
 	}
 };
+/**
+    @Begin
+	@Class_end
+	@End
+*/
 
 #endif