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     // XXX-injection-#1: Weaken the parameter "mo_acquire" to
  24     // "memory_order_relaxed", run "make" to recompile, and then run:
  25     // "./run.sh ./concurrent-hashmap/testcase2 -m2 -y -u3 -tSPEC"
  26         /**********    Detected UL (testcase2) **********/
  27         Entry *firstPtr = first->load(mo_acquire);
  28
  29         e = firstPtr;
  30         while (e != NULL) {
  31                 if (e->hash == hash && eq(key, e->key)) {
  32             // XXX-injection-#2: Weaken the parameter "mo_seqcst" to
  33             // "memory_order_acq_rel", run "make" to recompile, and then run:
  34             // "./run.sh ./concurrent-hashmap/testcase1 -m2 -y -u3 -tSPEC"
  35                         /**********    Detected Correctness (testcase1) **********/
  36                         res = e->value.load(mo_seqcst);
  37                         /** @OPClearDefine: res != 0 */
  38                         if (res != 0)
  39                                 return res;
  40                         else
  41                                 break;
  42                 }
  43                 // Loading the next entry, this can be relaxed because the
  44                 // synchronization has been established by the load of head
  45                 e = e->next.load(mo_relaxed);
  46         }
  47
  48         // Recheck under synch if key apparently not there or interference
  49         Segment *seg = segments[hash & SEGMENT_MASK];
  50         seg->lock(); // Critical region begins
  51         /** @OPClearDefine: true */
  52         // Not considering resize now, so ignore the reload of table...
  53
  54         // Synchronized by locking, no need to be load acquire
  55         Entry *newFirstPtr = first->load(mo_relaxed);
  56         if (e != NULL || firstPtr != newFirstPtr) {
  57                 e = newFirstPtr;
  58                 while (e != NULL) {
  59                         if (e->hash == hash && eq(key, e->key)) {
  60                                 // Protected by lock, no need to be SC
  61                                 res = e->value.load(mo_relaxed);
  62                                 seg->unlock(); // Critical region ends
  63                                 return res;
  64                         }
  65                         // Synchronized by locking
  66                         e = e->next.load(mo_relaxed);
  67                 }
  68         }
  69         seg->unlock(); // Critical region ends
  70         return 0;
  71 }
  72
  73 int HashMap::put(int key, int value) {
  74         // Don't allow NULL key or value
  75         MODEL_ASSERT (key && value);
  76
  77         int hash = hashKey(key);
  78         Segment *seg = segments[hash & SEGMENT_MASK];
  79         atomic<Entry*> *tab;
  80
  81         seg->lock(); // Critical region begins
  82         tab = table;
  83         int index = hash & (capacity - 1);
  84
  85         atomic<Entry*> *first = &tab[index];
  86         Entry *e;
  87         int oldValue = 0;
  88
  89         // The written of the entry is synchronized by locking
  90         Entry *firstPtr = first->load(mo_relaxed);
  91         e = firstPtr;
  92         while (e != NULL) {
  93                 if (e->hash == hash && eq(key, e->key)) {
  94                         // FIXME: This could be a relaxed (because locking synchronize
  95                         // with the previous put())??  no need to be acquire
  96                         oldValue = e->value.load(relaxed);
  97             // XXX-injection-#3: Weaken the parameter "mo_seqcst" to
  98             // "memory_order_acq_rel", run "make" to recompile, and then run:
  99             // "./run.sh ./concurrent-hashmap/testcase1 -m2 -y -u3 -tSPEC"
 100                         /**********    Detected Correctness (testcase1) **********/
 101                         e->value.store(value, mo_seqcst);
 102                         /** @OPClearDefine: true */
 103                         seg->unlock(); // Don't forget to unlock before return
 104                         return oldValue;
 105                 }
 106                 // Synchronized by locking
 107                 e = e->next.load(mo_relaxed);
 108         }
 109
 110         // Add to front of list
 111         Entry *newEntry = new Entry();
 112         newEntry->hash = hash;
 113         newEntry->key = key;
 114         newEntry->value.store(value, relaxed);
 115         /** @OPClearDefine: true */
 116         newEntry->next.store(firstPtr, relaxed);
 117     // XXX-injection-#4: Weaken the parameter "mo_release" to
 118     // "memory_order_acquire", run "make" to recompile, and then run:
 119     // "./run.sh ./concurrent-hashmap/testcase2 -m2 -y -u3 -tSPEC"
 120         /**********    Detected UL (testcase2) **********/
 121         // Publish the newEntry to others
 122         first->store(newEntry, mo_release);
 123         seg->unlock(); // Critical region ends
 124         return 0;
 125 }
 126
 127 /** @PreCondition: return STATE(map)->get(key) == C_RET; */
 128 int get(HashMap *map, int key) {
 129         return map->get(key);
 130 }
 131
 132 /** @PreCondition: return STATE(map)->get(key) == C_RET;
 133         @Transition: STATE(map)->put(key, value); */
 134 int put(HashMap *map, int key, int value) {
 135         return map->put(key, value);
 136 }
 137