#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
For the sake of simplicity, we map Integer -> Integer.
*/
-
-
class Entry {
public:
int key;
/**
@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;
// Not gonna consider resize now...
HashMap() {
+ /**
+ @Begin
+ @Entry_point
+ @End
+ */
this->size = 0;
this->capacity = DEFAULT_INITIAL_CAPACITY;
this->table = new atomic<Entry*>[capacity];
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);
// 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
// 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;
}
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);
// 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;
}
// 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
--- /dev/null
+#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;
+}
+
+
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"
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));
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);
projects / cdsspec-compiler.git / commitdiff