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