4 /** @DeclareState: IntMap *map; */
6 int HashMap::get(int key) {
8 int hash = hashKey(key);
10 // Try first without locking...
11 atomic<Entry*> *tab = table;
12 int index = hash & (capacity - 1);
13 atomic<Entry*> *first = &tab[index];
17 // Should be a load acquire
18 // This load action here makes it problematic for the SC analysis, what
19 // we need to do is as follows: if the get() method ever acquires the
20 // lock, we ignore this operation for the SC analysis, and otherwise we
21 // take it into consideration
23 /********** Detected UL (testcase2) **********/
24 Entry *firstPtr = first->load(mo_acquire);
28 if (e->hash == hash && eq(key, e->key)) {
29 /********** Detected Correctness (testcase1) **********/
30 res = e->value.load(mo_seqcst);
31 /** @OPClearDefine: res != 0 */
37 // Loading the next entry, this can be relaxed because the
38 // synchronization has been established by the load of head
39 e = e->next.load(mo_relaxed);
42 // Recheck under synch if key apparently not there or interference
43 Segment *seg = segments[hash & SEGMENT_MASK];
44 seg->lock(); // Critical region begins
45 /** @OPClearDefine: true */
46 // Not considering resize now, so ignore the reload of table...
48 // Synchronized by locking, no need to be load acquire
49 Entry *newFirstPtr = first->load(mo_relaxed);
50 if (e != NULL || firstPtr != newFirstPtr) {
53 if (e->hash == hash && eq(key, e->key)) {
54 // Protected by lock, no need to be SC
55 res = e->value.load(mo_relaxed);
56 seg->unlock(); // Critical region ends
59 // Synchronized by locking
60 e = e->next.load(mo_relaxed);
63 seg->unlock(); // Critical region ends
67 int HashMap::put(int key, int value) {
68 // Don't allow NULL key or value
69 MODEL_ASSERT (key && value);
71 int hash = hashKey(key);
72 Segment *seg = segments[hash & SEGMENT_MASK];
75 seg->lock(); // Critical region begins
77 int index = hash & (capacity - 1);
79 atomic<Entry*> *first = &tab[index];
83 // The written of the entry is synchronized by locking
84 Entry *firstPtr = first->load(mo_relaxed);
87 if (e->hash == hash && eq(key, e->key)) {
88 // FIXME: This could be a relaxed (because locking synchronize
89 // with the previous put())?? no need to be acquire
90 oldValue = e->value.load(relaxed);
91 /********** Detected Correctness (testcase1) **********/
92 e->value.store(value, mo_seqcst);
93 /** @OPClearDefine: true */
94 seg->unlock(); // Don't forget to unlock before return
97 // Synchronized by locking
98 e = e->next.load(mo_relaxed);
101 // Add to front of list
102 Entry *newEntry = new Entry();
103 newEntry->hash = hash;
105 newEntry->value.store(value, relaxed);
106 /** @OPClearDefine: true */
107 newEntry->next.store(firstPtr, relaxed);
108 /********** Detected UL (testcase2) **********/
109 // Publish the newEntry to others
110 first->store(newEntry, mo_release);
111 seg->unlock(); // Critical region ends
115 /** @PreCondition: return STATE(map)->get(key) == C_RET; */
116 int get(HashMap *map, int key) {
117 return map->get(key);
120 /** @PreCondition: return STATE(map)->get(key) == C_RET;
121 @Transition: STATE(map)->put(key, value); */
122 int put(HashMap *map, int key, int value) {
123 return map->put(key, value);