The CDSSpec checker's benchmarks
[model-checker-benchmarks.git] / concurrent-hashmap / hashmap.cc
1 #include "unrelacy.h" 
2 #include "hashmap.h" 
3
4 /** @DeclareState: IntMap *map; */
5
6 int HashMap::get(int key) {
7         MODEL_ASSERT (key);
8         int hash = hashKey(key);
9
10         // Try first without locking...
11         atomic<Entry*> *tab = table;
12         int index = hash & (capacity - 1);
13         atomic<Entry*> *first = &tab[index];
14         Entry *e;
15         int res = 0;
16
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
22         
23         /**********    Detected UL (testcase2) **********/
24         Entry *firstPtr = first->load(mo_acquire);
25
26         e = firstPtr;
27         while (e != NULL) {
28                 if (e->hash == hash && eq(key, e->key)) {
29                         /**********    Detected Correctness (testcase1) **********/
30                         res = e->value.load(mo_seqcst);
31                         /** @OPClearDefine: res != 0 */
32                         if (res != 0)
33                                 return res;
34                         else
35                                 break;
36                 }
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);
40         }
41
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...
47
48         // Synchronized by locking, no need to be load acquire
49         Entry *newFirstPtr = first->load(mo_relaxed);
50         if (e != NULL || firstPtr != newFirstPtr) {
51                 e = newFirstPtr;
52                 while (e != NULL) {
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
57                                 return res;
58                         }
59                         // Synchronized by locking
60                         e = e->next.load(mo_relaxed);
61                 }
62         }
63         seg->unlock(); // Critical region ends
64         return 0;
65 }
66
67 int HashMap::put(int key, int value) {
68         // Don't allow NULL key or value
69         MODEL_ASSERT (key && value);
70
71         int hash = hashKey(key);
72         Segment *seg = segments[hash & SEGMENT_MASK];
73         atomic<Entry*> *tab;
74
75         seg->lock(); // Critical region begins
76         tab = table;
77         int index = hash & (capacity - 1);
78
79         atomic<Entry*> *first = &tab[index];
80         Entry *e;
81         int oldValue = 0;
82
83         // The written of the entry is synchronized by locking
84         Entry *firstPtr = first->load(mo_relaxed);
85         e = firstPtr;
86         while (e != NULL) {
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
95                         return oldValue;
96                 }
97                 // Synchronized by locking
98                 e = e->next.load(mo_relaxed);
99         }
100
101         // Add to front of list
102         Entry *newEntry = new Entry();
103         newEntry->hash = hash;
104         newEntry->key = key;
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
112         return 0;
113 }
114
115 /** @PreCondition: return STATE(map)->get(key) == C_RET; */
116 int get(HashMap *map, int key) {
117         return map->get(key);
118 }
119
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);
124 }
125