#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