benchmark/mcs-lock/mcs-lock.h

   1 // mcs on stack
   2
   3 #include <stdatomic.h>
   4 #include <unrelacy.h>
   5
   6 #include <spec_lib.h>
   7 #include <stdlib.h>
   8 #include <cdsannotate.h>
   9 #include <specannotation.h>
  10 #include <model_memory.h>
  11 #include "common.h"
  12
  13 struct mcs_node {
  14         std::atomic<mcs_node *> next;
  15         std::atomic<int> gate;
  16
  17         mcs_node() {
  18                 next.store(0);
  19                 gate.store(0);
  20         }
  21 };
  22
  23
  24 struct mcs_mutex {
  25 public:
  26         // tail is null when lock is not held
  27         std::atomic<mcs_node *> m_tail;
  28
  29         mcs_mutex() {
  30                 /**
  31                         @Begin
  32                 @Entry_point
  33                         @End
  34                 */
  35                 m_tail.store( NULL );
  36         }
  37         ~mcs_mutex() {
  38                 //ASSERT( m_tail.load() == NULL );
  39         }
  40
  41         // Each thread will have their own guard.
  42         class guard {
  43         public:
  44                 mcs_mutex * m_t;
  45                 mcs_node    m_node; // node held on the stack
  46
  47                 guard(mcs_mutex * t) : m_t(t) { t->lock(this); }
  48                 ~guard() { m_t->unlock(this); }
  49         };
  50
  51         /**
  52                 @Begin
  53                 @Options:
  54                         LANG = CPP;
  55                         CLASS = mcs_mutex;
  56                 @Global_define:
  57                         @DeclareVar: bool _lock_acquired;
  58                         @InitVar: _lock_acquired = false;
  59                 @Happens_before: Unlock -> Lock
  60                 @End
  61         */
  62
  63         /**
  64                 @Begin
  65                 @Interface: Lock
  66                 @Commit_point_set: Lock_Enqueue_Point1 | Lock_Enqueue_Point2
  67                 @Check: _lock_acquired == false;
  68                 @Action: _lock_acquired = true;
  69                 @End
  70         */
  71         void lock(guard * I) {
  72                 mcs_node * me = &(I->m_node);
  73
  74                 // set up my node :
  75                 // not published yet so relaxed :
  76                 me->next.store(NULL, std::mo_relaxed );
  77                 me->gate.store(1, std::mo_relaxed );
  78
  79                 /**********  Inadmissible  **********/
  80                 /** Run this in the -Y mode to expose the HB bug */
  81                 // publish my node as the new tail :
  82                 mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
  83                 /**
  84                         @Begin
  85                         @Commit_point_define_check: pred == NULL
  86                         @Label: Lock_Enqueue_Point1
  87                         @End
  88                 */
  89                 if ( pred != NULL ) {
  90                         // (*1) race here
  91                         // unlock of pred can see me in the tail before I fill next
  92
  93                         // publish me to previous lock-holder :
  94                         // FIXME: detection miss, execution never ends
  95                         // If this is relaxed, the store 0 to gate will be read before and
  96                         // that lock will never ends.
  97                         pred->next.store(me, std::mo_release );
  98                         //printf("lock_miss1\n");
  99
 100                         // (*2) pred not touched any more
 101
 102                         // now this is the spin -
 103                         // wait on predecessor setting my flag -
 104                         rl::linear_backoff bo;
 105                         int my_gate = 1;
 106                         while (my_gate ) {
 107                                 /**********  Inadmissibility  *********/
 108                                 my_gate = me->gate.load(std::mo_acquire);
 109                                 //if (my_gate == 0)
 110                                         //printf("lock at gate!\n");
 111                                 /**
 112                                         @Begin
 113                                         @Commit_point_define_check: my_gate == 0
 114                                         @Label: Lock_Enqueue_Point2
 115                                         @End
 116                                 */
 117                                 thrd_yield();
 118                         }
 119                 }
 120         }
 121
 122         /**
 123                 @Begin
 124                 @Interface: Unlock
 125                 @Commit_point_set: Unlock_Point_Success_1 | Unlock_Point_Success_2
 126                 @Check: _lock_acquired == true
 127                 @Action: _lock_acquired = false;
 128                 @End
 129         */
 130         void unlock(guard * I) {
 131                 mcs_node * me = &(I->m_node);
 132
 133                 // FIXME: detection miss, execution never ends
 134                 mcs_node * next = me->next.load(std::mo_acquire);
 135                 //printf("unlock_miss2\n");
 136                 if ( next == NULL )
 137                 {
 138                         mcs_node * tail_was_me = me;
 139                         bool success;
 140
 141                         /**********  Inadmissible  **********/
 142                         success = m_tail.compare_exchange_strong(
 143                                 tail_was_me,NULL,std::mo_acq_rel);
 144                         /**
 145                                 @Begin
 146                                 @Commit_point_define_check: success == true
 147                                 @Label: Unlock_Point_Success_1
 148                                 @End
 149                         */
 150                         if (success) {
 151
 152                                 // got null in tail, mutex is unlocked
 153                                 return;
 154                         }
 155
 156                         // (*1) catch the race :
 157                         rl::linear_backoff bo;
 158                         for(;;) {
 159                                 // FIXME: detection miss, execution never ends
 160                                 next = me->next.load(std::mo_acquire);
 161                                 //printf("unlock_miss3\n");
 162                                 if ( next != NULL )
 163                                         break;
 164                                 thrd_yield();
 165                         }
 166                 }
 167
 168                 // (*2) - store to next must be done,
 169                 //  so no locker can be viewing my node any more
 170
 171                 /**********  Inadmissible  **********/
 172                 // let next guy in :
 173                 next->gate.store( 0, std::mo_release );
 174                 /**
 175                         @Begin
 176                         @Commit_point_define_check: true
 177                         @Label: Unlock_Point_Success_2
 178                         @End
 179                 */
 180         }
 181 };
 182 /**
 183         @Begin
 184         @Class_end
 185         @End
 186 */