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