edits
authorPeizhao Ou <peizhaoo@uci.edu>
Tue, 17 Nov 2015 10:36:34 +0000 (02:36 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Tue, 17 Nov 2015 10:36:34 +0000 (02:36 -0800)
benchmark/concurrent-hashmap/Makefile
benchmark/concurrent-hashmap/hashmap.h
benchmark/concurrent-hashmap/testcase1.cc [new file with mode: 0644]
output/concurrent-hashmap/Makefile
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java

index 8fa9693..6b615a1 100644 (file)
@@ -1,7 +1,7 @@
 include ../benchmarks.mk
 
 BENCH := hashmap
-TESTS := main 
+TESTS := main testcase1
 
 all: $(TESTS)
 
index e813d23..904d0b8 100644 (file)
@@ -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
diff --git a/benchmark/concurrent-hashmap/testcase1.cc b/benchmark/concurrent-hashmap/testcase1.cc
new file mode 100644 (file)
index 0000000..8a69d4a
--- /dev/null
@@ -0,0 +1,36 @@
+#include <iostream>
+#include <threads.h>
+#include "hashmap.h"
+
+HashMap *table;
+
+void threadA(void *arg) {
+       table->put(1, 11);
+       printf("Thrd A: Put %d -> %d\n", 1, 11);
+       int r1 = table->get(2);
+       printf("Thrd A: Get %d\n", r1);
+}
+
+void threadB(void *arg) {
+       table->put(2, 22);
+       printf("Thrd B: Put %d -> %d\n", 2, 22);
+       int r2 = table->get(1);
+       printf("Thrd B: Get %d\n", r2);
+}
+
+int user_main(int argc, char *argv[]) {
+       thrd_t t1, t2;
+
+       table = new HashMap;
+       table->put(1, 1);
+       table->put(2, 2);
+
+       thrd_create(&t1, threadA, NULL);
+       thrd_create(&t2, threadB, NULL);
+       thrd_join(t1);
+       thrd_join(t2);
+       
+       return 0;
+}
+
+
index 8fa9693..6b615a1 100644 (file)
@@ -1,7 +1,7 @@
 include ../benchmarks.mk
 
 BENCH := hashmap
-TESTS := main 
+TESTS := main testcase1
 
 all: $(TESTS)
 
index 377d70a..95637ee 100644 (file)
@@ -294,7 +294,8 @@ public class CodeGenerator {
                File[] srcHashtable = {
                                new File(homeDir
                                                + "/benchmark/concurrent-hashmap/hashmap.h"),
-                               new File(homeDir + "/benchmark/concurrent-hashmap/main.cc") };
+                                               new File(homeDir + "/benchmark/concurrent-hashmap/testcase1.cc"),
+                               new File(homeDir + "/benchmark/concurrent-hashmap/main.cc")};
 
                File[] srcMSQueue = {
                                new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
index b9ab022..4d19458 100644 (file)
@@ -509,10 +509,10 @@ public class CodeVariables {
                newCode.add("\t" + STRUCT_NEW_DECLARE_DEFINE(ANNO_INIT, structName));
                newCode.add("\t"
                                + ASSIGN_TO_PTR(structName, "init_func",
-                                               "(void*) __SPEC_INIT__"));
+                                               "(void_func_t) __SPEC_INIT__"));
                newCode.add("\t"
                                + ASSIGN_TO_PTR(structName, "cleanup_func",
-                                               "(void*) __SPEC_CLEANUP__"));
+                                               "(cleanup_func_t) __SPEC_CLEANUP__"));
                newCode.add("\t"
                                + ASSIGN_TO_PTR(structName, "func_table", "func_ptr_table"));
                newCode.add("\t"
@@ -561,6 +561,7 @@ public class CodeVariables {
                if (templateList == null) {
                        newCode.add(DECLARE("void**", varPrefix + "func_ptr_table"));
                        newCode.add(DECLARE("hb_rule**", varPrefix + "hb_rule_table"));
+                       newCode.add(DECLARE("commutativity_rule**", varPrefix + "commutativity_rule_table"));
                        for (int i = 0; i < construct.code.declareVar.size(); i++) {
                                VariableDeclaration varDecl = construct.code.declareVar.get(i);
                                newCode.add(DECLARE(varDecl.type, varPrefix + varDecl.name));
@@ -570,6 +571,7 @@ public class CodeVariables {
                        newCode.add(DECLARE("void**", varPrefix + "func_ptr_table"));
                        newCode.add(templateDecl);
                        newCode.add(DECLARE("hb_rule**", varPrefix + "hb_rule_table"));
+                       newCode.add(DECLARE("commutativity_rule**", varPrefix + "commutativity_rule_table"));
                        for (int i = 0; i < construct.code.declareVar.size(); i++) {
                                VariableDeclaration varDecl = construct.code.declareVar.get(i);
                                newCode.add(templateDecl);