edits

[cdsspec-compiler.git] / benchmark / concurrent-hashmap / hashmap.h

diff --git a/benchmark/concurrent-hashmap/hashmap.h b/benchmark/concurrent-hashmap/hashmap.h
index e813d23fff2cc651a9c0485bb084bbcc612c55f8..904d0b84e9233ce79246c404eec439eb86ebe62e 100644 (file)
--- 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