--- /dev/null
+#ifndef _HASHMAP_H
+#define _HASHMAP_H
+
+#include <iostream>
+#include <atomic>
+#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
+#define release memory_order_release
+#define acquire memory_order_acquire
+#define acq_rel memory_order_acq_rel
+#define seq_cst memory_order_seq_cst
+
+using namespace std;
+
+
+
+class Entry {
+ public:
+ int key;
+ atomic_int value;
+ int hash;
+ atomic<Entry*> next;
+
+ Entry(int h, int k, int v, Entry *n) {
+ this->hash = h;
+ this->key = k;
+ this->value.store(v, relaxed);
+ this->next.store(n, relaxed);
+ }
+};
+
+class Segment {
+ public:
+ int count;
+ mutex segMutex;
+
+ void lock() {
+ segMutex.lock();
+ }
+
+ void unlock() {
+ segMutex.unlock();
+ }
+
+ Segment() {
+ this->count = 0;
+ }
+};
+
+
+class HashMap {
+ public:
+
+/* All other user-defined structs */
+static IntegerMap * __map;
+/* All other user-defined functions */
+/* Definition of interface info struct: Put */
+typedef struct Put_info {
+int __RET__;
+int key;
+int value;
+} Put_info;
+/* End of info struct definition: Put */
+
+/* ID function of interface: Put */
+inline static call_id_t Put_id(void *info, thread_id_t __TID__) {
+ Put_info* theInfo = (Put_info*)info;
+ int __RET__ = theInfo->__RET__;
+ int key = theInfo->key;
+ int value = theInfo->value;
+
+ call_id_t __ID__ = value;
+ return __ID__;
+}
+/* End of ID function: Put */
+
+/* Check action function of interface: Put */
+inline static bool Put_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
+ bool check_passed;
+ Put_info* theInfo = (Put_info*)info;
+ int __RET__ = theInfo->__RET__;
+ int key = theInfo->key;
+ int value = theInfo->value;
+
+ putIntegerMap ( __map , key , value ) ;
+ return true;
+}
+/* End of check action function: Put */
+
+/* Definition of interface info struct: Get */
+typedef struct Get_info {
+int __RET__;
+int key;
+} Get_info;
+/* End of info struct definition: Get */
+
+/* ID function of interface: Get */
+inline static call_id_t Get_id(void *info, thread_id_t __TID__) {
+ Get_info* theInfo = (Get_info*)info;
+ int __RET__ = theInfo->__RET__;
+ int key = theInfo->key;
+
+ call_id_t __ID__ = __RET__;
+ return __ID__;
+}
+/* End of ID function: Get */
+
+/* Check action function of interface: Get */
+inline static bool Get_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
+ bool check_passed;
+ Get_info* theInfo = (Get_info*)info;
+ int __RET__ = theInfo->__RET__;
+ int key = theInfo->key;
+
+ int res = getIntegerMap ( __map , key ) ;
+ check_passed = __RET__ ? res == __RET__ : true;
+ if (!check_passed)
+ return false;
+ return true;
+}
+/* End of check action function: Get */
+
+#define INTERFACE_SIZE 2
+static void** func_ptr_table;
+static hb_rule** hb_rule_table;
+static commutativity_rule** commutativity_rule_table;
+inline static bool CommutativityCondition0(void *info1, void *info2) {
+ Put_info *_info1 = (Put_info*) info1;
+ Put_info *_info2 = (Put_info*) info2;
+ return _info1-> key != _info2-> key;
+}
+inline static bool CommutativityCondition1(void *info1, void *info2) {
+ Put_info *_info1 = (Put_info*) info1;
+ Get_info *_info2 = (Get_info*) info2;
+ return _info1-> key != _info2-> key;
+}
+inline static bool CommutativityCondition2(void *info1, void *info2) {
+ Get_info *_info1 = (Get_info*) info1;
+ Get_info *_info2 = (Get_info*) info2;
+ return true;
+}
+
+/* Initialization of sequential varialbes */
+static void __SPEC_INIT__() {
+ __map = createIntegerMap ( ) ;
+}
+
+/* Cleanup routine of sequential variables */
+static bool __SPEC_CLEANUP__() {
+ if ( __map ) destroyIntegerMap ( __map ) ;
+ return true ;
+}
+
+/* Define function for sequential code initialization */
+inline static void __sequential_init() {
+ /* Init func_ptr_table */
+ func_ptr_table = (void**) malloc(sizeof(void*) * 2 * 2);
+ func_ptr_table[2 * 1] = (void*) &Put_id;
+ func_ptr_table[2 * 1 + 1] = (void*) &Put_check_action;
+ func_ptr_table[2 * 0] = (void*) &Get_id;
+ func_ptr_table[2 * 0 + 1] = (void*) &Get_check_action;
+ /* Put(true) -> Get(true) */
+ struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
+ hbConditionInit0->interface_num_before = 1; // Put
+ hbConditionInit0->hb_condition_num_before = 0; //
+ hbConditionInit0->interface_num_after = 0; // Get
+ hbConditionInit0->hb_condition_num_after = 0; //
+ /* Init hb_rule_table */
+ hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 1);
+ #define HB_RULE_TABLE_SIZE 1
+ hb_rule_table[0] = hbConditionInit0;
+ /* Init commutativity_rule_table */
+ commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 3);
+ commutativity_rule* rule;
+ rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
+ rule->interface_num_before = 1;
+ rule->interface_num_after = 1;
+ rule->rule = "_Method1 . key != _Method2 . key";
+ rule->condition = CommutativityCondition0;
+ commutativity_rule_table[0] = rule;
+ rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
+ rule->interface_num_before = 1;
+ rule->interface_num_after = 0;
+ rule->rule = "_Method1 . key != _Method2 . key";
+ rule->condition = CommutativityCondition1;
+ commutativity_rule_table[1] = rule;
+ rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
+ rule->interface_num_before = 0;
+ rule->interface_num_after = 0;
+ rule->rule = "true";
+ rule->condition = CommutativityCondition2;
+ commutativity_rule_table[2] = rule;
+ /* Pass init info, including function table info & HB rules & Commutativity Rules */
+ struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
+ anno_init->init_func = (void_func_t) __SPEC_INIT__;
+ anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
+ anno_init->func_table = func_ptr_table;
+ anno_init->func_table_size = INTERFACE_SIZE;
+ anno_init->hb_rule_table = hb_rule_table;
+ anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
+ anno_init->commutativity_rule_table = commutativity_rule_table;
+ anno_init->commutativity_rule_table_size = 3;
+ struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ init->type = INIT;
+ init->annotation = anno_init;
+ cdsannotate(SPEC_ANALYSIS, init);
+
+}
+
+/* End of Global construct generation in class */
+
+
+ atomic<Entry*> *table;
+
+ int capacity;
+ int size;
+
+ static const int CONCURRENCY_LEVEL = 4;
+
+ static const int SEGMENT_MASK = CONCURRENCY_LEVEL - 1;
+
+ Segment *segments[CONCURRENCY_LEVEL];
+
+ static const int DEFAULT_INITIAL_CAPACITY = 16;
+
+
+ HashMap() {
+ __sequential_init();
+
+ this->size = 0;
+ this->capacity = DEFAULT_INITIAL_CAPACITY;
+ this->table = new atomic<Entry*>[capacity];
+ for (int i = 0; i < capacity; i++) {
+ atomic_init(&table[i], NULL);
+ }
+ for (int i = 0; i < CONCURRENCY_LEVEL; i++) {
+ segments[i] = new Segment;
+ }
+ }
+
+ int hashKey(int key) {
+ return key;
+ }
+
+
+
+int get(int key) {
+ /* Interface begins */
+ struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
+ interface_begin->interface_num = 0; // Get
+ interface_begin->interface_name = "Get";
+ struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_interface_begin->type = INTERFACE_BEGIN;
+ annotation_interface_begin->annotation = interface_begin;
+ cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
+ int __RET__ = __wrapper__get(key);
+ struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
+ hb_condition->interface_num = 0; // Get
+ hb_condition->hb_condition_num = 0;
+ struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_hb_condition->type = HB_CONDITION;
+ annotation_hb_condition->annotation = hb_condition;
+ cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
+
+ Get_info* info = (Get_info*) malloc(sizeof(Get_info));
+ info->__RET__ = __RET__;
+ info->key = key;
+ struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
+ interface_end->interface_num = 0; // Get
+ interface_end->info = info;
+ struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annoation_interface_end->type = INTERFACE_END;
+ annoation_interface_end->annotation = interface_end;
+ cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
+ return __RET__;
+}
+
+int __wrapper__get(int key) {
+ ASSERT (key);
+ int hash = hashKey(key);
+
+ atomic<Entry*> *tab = table;
+ int index = hash & (capacity - 1);
+ atomic<Entry*> *first = &tab[index];
+ Entry *e;
+ int res = 0;
+
+
+
+ Entry *firstPtr = first->load(acquire);
+
+ e = firstPtr;
+ while (e != NULL) {
+ if (key, e->key) {
+
+ res = e->value.load(seq_cst);
+ /* Automatically generated code for commit point define check: GetReadValue1 */
+
+ if (res != 0) {
+ struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
+ cp_define_check->label_num = 0;
+ cp_define_check->label_name = "GetReadValue1";
+ cp_define_check->interface_num = 0;
+ struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_cp_define_check->type = CP_DEFINE_CHECK;
+ annotation_cp_define_check->annotation = cp_define_check;
+ cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
+ }
+
+ if (res != 0)
+ return res;
+ else
+ break;
+ }
+ e = e->next.load(relaxed);
+ }
+
+ Segment *seg = segments[hash & SEGMENT_MASK];
+ seg->lock();
+ Entry *newFirstPtr = first->load(relaxed);
+ /* Automatically generated code for commit point define check: GetReadEntry */
+
+ if (true) {
+ struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
+ cp_define_check->label_num = 1;
+ cp_define_check->label_name = "GetReadEntry";
+ cp_define_check->interface_num = 0;
+ struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_cp_define_check->type = CP_DEFINE_CHECK;
+ annotation_cp_define_check->annotation = cp_define_check;
+ cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
+ }
+
+ if (e != NULL || firstPtr != newFirstPtr) {
+ e = newFirstPtr;
+ while (e != NULL) {
+ if (key == e->key) {
+ res = e->value.load(relaxed);
+ /* Automatically generated code for commit point define check: GetReadValue2 */
+
+ if (true) {
+ struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
+ cp_define_check->label_num = 2;
+ cp_define_check->label_name = "GetReadValue2";
+ cp_define_check->interface_num = 0;
+ struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_cp_define_check->type = CP_DEFINE_CHECK;
+ annotation_cp_define_check->annotation = cp_define_check;
+ cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
+ }
+
+ seg->unlock(); return res;
+ }
+ e = e->next.load(relaxed);
+ }
+ }
+ seg->unlock(); return 0;
+ }
+
+
+int put(int key, int value) {
+ /* Interface begins */
+ struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
+ interface_begin->interface_num = 1; // Put
+ interface_begin->interface_name = "Put";
+ struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_interface_begin->type = INTERFACE_BEGIN;
+ annotation_interface_begin->annotation = interface_begin;
+ cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
+ int __RET__ = __wrapper__put(key, value);
+ struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
+ hb_condition->interface_num = 1; // Put
+ hb_condition->hb_condition_num = 0;
+ struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_hb_condition->type = HB_CONDITION;
+ annotation_hb_condition->annotation = hb_condition;
+ cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
+
+ Put_info* info = (Put_info*) malloc(sizeof(Put_info));
+ info->__RET__ = __RET__;
+ info->key = key;
+ info->value = value;
+ struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
+ interface_end->interface_num = 1; // Put
+ interface_end->info = info;
+ struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annoation_interface_end->type = INTERFACE_END;
+ annoation_interface_end->annotation = interface_end;
+ cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
+ return __RET__;
+}
+
+int __wrapper__put(int key, int value) {
+ ASSERT (key && value);
+ int hash = hashKey(key);
+ Segment *seg = segments[hash & SEGMENT_MASK];
+ atomic<Entry*> *tab;
+
+ seg->lock(); tab = table;
+ int index = hash & (capacity - 1);
+
+ atomic<Entry*> *first = &tab[index];
+ Entry *e;
+ int oldValue = 0;
+
+ Entry *firstPtr = first->load(relaxed);
+ e = firstPtr;
+ while (e != NULL) {
+ if (key == e->key) {
+ oldValue = e->value.load(relaxed);
+
+
+ e->value.store(value, seq_cst);
+ /* Automatically generated code for commit point define check: PutUpdateValue */
+
+ if (true) {
+ struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
+ cp_define_check->label_num = 3;
+ cp_define_check->label_name = "PutUpdateValue";
+ cp_define_check->interface_num = 1;
+ struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_cp_define_check->type = CP_DEFINE_CHECK;
+ annotation_cp_define_check->annotation = cp_define_check;
+ cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
+ }
+
+ seg->unlock(); return oldValue;
+ }
+ e = e->next.load(relaxed);
+ }
+
+ Entry *newEntry = new Entry(hash, key, value, firstPtr);
+
+
+ first->store(newEntry, release);
+ /* Automatically generated code for commit point define check: PutInsertValue */
+
+ if (true) {
+ struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
+ cp_define_check->label_num = 4;
+ cp_define_check->label_name = "PutInsertValue";
+ cp_define_check->interface_num = 1;
+ struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_cp_define_check->type = CP_DEFINE_CHECK;
+ annotation_cp_define_check->annotation = cp_define_check;
+ cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
+ }
+
+ seg->unlock(); return 0;
+ }
+};
+void** HashMap::func_ptr_table;
+hb_rule** HashMap::hb_rule_table;
+commutativity_rule** HashMap::commutativity_rule_table;
+IntegerMap * HashMap::__map;
+
+
+#endif
+
projects / cdsspec-compiler.git / blobdiff