From: Peizhao Ou Date: Tue, 17 Nov 2015 10:36:34 +0000 (-0800) Subject: edits X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=fc0b24243f667dc9938d081305aa66dac66dc6ed edits --- diff --git a/benchmark/concurrent-hashmap/Makefile b/benchmark/concurrent-hashmap/Makefile index 8fa9693..6b615a1 100644 --- a/benchmark/concurrent-hashmap/Makefile +++ b/benchmark/concurrent-hashmap/Makefile @@ -1,7 +1,7 @@ include ../benchmarks.mk BENCH := hashmap -TESTS := main +TESTS := main testcase1 all: $(TESTS) 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 #include + +#include +#include +#include +#include +#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 *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[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 index 0000000..8a69d4a --- /dev/null +++ b/benchmark/concurrent-hashmap/testcase1.cc @@ -0,0 +1,36 @@ +#include +#include +#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; +} + + diff --git a/output/concurrent-hashmap/Makefile b/output/concurrent-hashmap/Makefile index 8fa9693..6b615a1 100644 --- a/output/concurrent-hashmap/Makefile +++ b/output/concurrent-hashmap/Makefile @@ -1,7 +1,7 @@ include ../benchmarks.mk BENCH := hashmap -TESTS := main +TESTS := main testcase1 all: $(TESTS) diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index 377d70a..95637ee 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -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"), diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java index b9ab022..4d19458 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -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);