+++ /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