+++ /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;
-
-/**
- For the sake of simplicity, we map Integer -> Integer.
-*/
-
-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;
- }
-};
-
-/**
- @Begin
- @Class_begin
- @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;
- 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;
-
- // Not gonna consider resize now...
-
- HashMap() {
- /**
- @Begin
- @Entry_point
- @End
- */
- 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;
- }
-
-
- /**
- @Begin
- @Interface: Get
- @Commit_point_set: GetReadValue1 | GetReadValue2 | GetReadNothing
- @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);
-
- // Try first without locking...
- atomic<Entry*> *tab = table;
- int index = hash & (capacity - 1);
- atomic<Entry*> *first = &tab[index];
- Entry *e;
- int res = 0;
-
- // Should be a load acquire
- // This load action here makes it problematic for the SC analysis, what
- // we need to do is as follows: if the get() method ever acquires the
- // lock, we ignore this operation for the SC analysis, and otherwise we
- // take it into consideration
-
- /**** UL (main.cc) ****/
- Entry *firstPtr = first->load(acquire);
-
- e = firstPtr;
- while (e != NULL) {
- if (key, e->key) {
- /**** inadmissible (testcase1.cc) ****/
- res = e->value.load(seq_cst);
- /**
- @Begin
- @Commit_point_define_check: res != 0
- @Label: GetReadValue1
- @End
- */
- if (res != 0)
- return res;
- else
- break;
- }
- // Loading the next entry, this can be relaxed because the
- // synchronization has been established by the load of head
- e = e->next.load(relaxed);
- }
-
- // Recheck under synch if key apparently not there or interference
- Segment *seg = segments[hash & SEGMENT_MASK];
- seg->lock(); // Critical region begins
- // Not considering resize now, so ignore the reload of table...
-
- // Synchronized by locking, no need to be load acquire
- Entry *newFirstPtr = first->load(relaxed);
- 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;
- }
- // Synchronized by locking
- e = e->next.load(relaxed);
- }
- }
- seg->unlock(); // Critical region ends
- /**
- @Begin
- @Commit_point_define_check: true
- @Label: GetReadNothing
- @End
- */
- 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);
- Segment *seg = segments[hash & SEGMENT_MASK];
- atomic<Entry*> *tab;
-
- seg->lock(); // Critical region begins
- tab = table;
- int index = hash & (capacity - 1);
-
- atomic<Entry*> *first = &tab[index];
- Entry *e;
- int oldValue = 0;
-
- // The written of the entry is synchronized by locking
- Entry *firstPtr = first->load(relaxed);
- e = firstPtr;
- while (e != NULL) {
- if (key == e->key) {
- // This could be a relaxed (because locking synchronize
- // with the previous put()), no need to be acquire
- oldValue = e->value.load(relaxed);
-
- /**** inadmissible (testcase1.cc) ****/
- 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;
- }
- // Synchronized by locking
- e = e->next.load(relaxed);
- }
-
- // Add to front of list
- Entry *newEntry = new Entry(hash, key, value, firstPtr);
-
- /**** UL (main.cc) ****/
- // Publish the newEntry to others
- first->store(newEntry, release);
- /**
- @Begin
- @Commit_point_clear: true
- @Label: PutClear
- @End
- */
-
- /**
- @Begin
- @Commit_point_define_check: true
- @Label: PutInsertValue
- @End
- */
- seg->unlock(); // Critical region ends
- return 0;
- }
-};
-/**
- @Begin
- @Class_end
- @End
-*/
-
-#endif
projects / cdsspec-compiler.git / blobdiff