11 #include <cdsannotate.h>
12 #include <specannotation.h>
13 #include <model_memory.h>
19 #define relaxed memory_order_relaxed
20 #define release memory_order_release
21 #define acquire memory_order_acquire
22 #define acq_rel memory_order_acq_rel
23 #define seq_cst memory_order_seq_cst
28 For the sake of simplicity, we map Integer -> Integer.
38 Entry(int h, int k, int v, Entry *n) {
41 this->value.store(v, relaxed);
42 this->next.store(n, relaxed);
81 __map = createIntegerMap();
84 destroyIntegerMap(__map);
86 @Happens_before: Put -> Get
87 @Commutativity: Put <-> Put: _Method1.key != _Method2.key
88 @Commutativity: Put <-> Get: _Method1.key != _Method2.key
89 @Commutativity: Get <-> Get: true
93 atomic<Entry*> *table;
98 static const int CONCURRENCY_LEVEL = 4;
100 static const int SEGMENT_MASK = CONCURRENCY_LEVEL - 1;
102 Segment *segments[CONCURRENCY_LEVEL];
104 static const int DEFAULT_INITIAL_CAPACITY = 16;
106 // Not gonna consider resize now...
115 this->capacity = DEFAULT_INITIAL_CAPACITY;
116 this->table = new atomic<Entry*>[capacity];
117 for (int i = 0; i < capacity; i++) {
118 atomic_init(&table[i], NULL);
120 for (int i = 0; i < CONCURRENCY_LEVEL; i++) {
121 segments[i] = new Segment;
125 int hashKey(int key) {
133 @Commit_point_set: GetReadValue1 | GetReadEntry | GetReadValue2
136 int res = getIntegerMap(__map, key);
137 //model_print("Get: key=%d, res=%d\n", key, res);
139 @Post_check: __RET__ ? res == __RET__: true
144 int hash = hashKey(key);
146 // Try first without locking...
147 atomic<Entry*> *tab = table;
148 int index = hash & (capacity - 1);
149 atomic<Entry*> *first = &tab[index];
153 // Should be a load acquire
154 // This load action here makes it problematic for the SC analysis, what
155 // we need to do is as follows: if the get() method ever acquires the
156 // lock, we ignore this operation for the SC analysis, and otherwise we
157 // take it into consideration
160 Entry *firstPtr = first->load(acquire);
165 /**** inadmissible ****/
166 res = e->value.load(seq_cst);
169 @Commit_point_define_check: res != 0
170 @Label: GetReadValue1
178 // Loading the next entry, this can be relaxed because the
179 // synchronization has been established by the load of head
180 e = e->next.load(relaxed);
183 // Recheck under synch if key apparently not there or interference
184 Segment *seg = segments[hash & SEGMENT_MASK];
185 seg->lock(); // Critical region begins
186 // Not considering resize now, so ignore the reload of table...
188 // Synchronized by locking, no need to be load acquire
189 Entry *newFirstPtr = first->load(relaxed);
192 @Commit_point_define_check: true
196 if (e != NULL || firstPtr != newFirstPtr) {
200 // Protected by lock, no need to be SC
201 res = e->value.load(relaxed);
204 @Commit_point_define_check: true
205 @Label: GetReadValue2
208 seg->unlock(); // Critical region ends
211 // Synchronized by locking
212 e = e->next.load(relaxed);
215 seg->unlock(); // Critical region ends
222 @Commit_point_set: PutUpdateValue | PutInsertValue
225 putIntegerMap(__map, key, value);
226 //model_print("Put: key=%d, val=%d\n", key, value);
229 int put(int key, int value) {
230 ASSERT (key && value);
231 int hash = hashKey(key);
232 Segment *seg = segments[hash & SEGMENT_MASK];
235 seg->lock(); // Critical region begins
237 int index = hash & (capacity - 1);
239 atomic<Entry*> *first = &tab[index];
243 // The written of the entry is synchronized by locking
244 Entry *firstPtr = first->load(relaxed);
248 // This could be a relaxed (because locking synchronize
249 // with the previous put()), no need to be acquire
250 oldValue = e->value.load(relaxed);
252 /**** inadmissible ****/
253 e->value.store(value, seq_cst);
256 @Commit_point_define_check: true
257 @Label: PutUpdateValue
260 seg->unlock(); // Don't forget to unlock before return
263 // Synchronized by locking
264 e = e->next.load(relaxed);
267 // Add to front of list
268 Entry *newEntry = new Entry(hash, key, value, firstPtr);
271 // Publish the newEntry to others
272 first->store(newEntry, release);
275 @Commit_point_define_check: true
276 @Label: PutInsertValue
279 seg->unlock(); // Critical region ends