mcs-lock/mcs-lock.cc

   1 #include "mcs-lock.h"
   2
   3 void mcs_mutex::lock(guard * I) {
   4         mcs_node * me = &(I->m_node);
   5
   6         // set up my node :
   7         // not published yet so relaxed :
   8         me->next.store(NULL, std::mo_relaxed );
   9         me->gate.store(1, std::mo_relaxed );
  10
  11         /**********  Detected Correctness **********/
  12         /** Run this in the -Y mode to expose the HB bug */
  13         // publish my node as the new tail :
  14         mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
  15         /** @OPDefine: pred == NULL */
  16         if ( pred != NULL ) {
  17                 // (*1) race here
  18                 // unlock of pred can see me in the tail before I fill next
  19
  20                 // FIXME: detection miss, execution never ends
  21                 // If this is relaxed, the store 0 to gate will be read before and
  22                 // that lock will never ends.
  23                 // publish me to previous lock-holder :
  24                 pred->next.store(me, std::mo_release );
  25
  26                 // (*2) pred not touched any more
  27
  28                 // now this is the spin -
  29                 // wait on predecessor setting my flag -
  30                 rl::linear_backoff bo;
  31                 /**********  Detected Correctness *********/
  32             /** Run this in the -Y mode to expose the HB bug */
  33                 while ( me->gate.load(std::mo_acquire) ) {
  34                         thrd_yield();
  35                 }
  36                 /** @OPDefine: true */
  37         }
  38 }
  39
  40 void mcs_mutex::unlock(guard * I) {
  41         mcs_node * me = &(I->m_node);
  42
  43         // FIXME: detection miss, execution never ends
  44         mcs_node * next = me->next.load(std::mo_acquire);
  45         if ( next == NULL )
  46         {
  47                 mcs_node * tail_was_me = me;
  48                 /**********  Detected Correctness **********/
  49             /** Run this in the -Y mode to expose the HB bug */
  50                 if ( m_tail.compare_exchange_strong(
  51                         tail_was_me,NULL,std::mo_acq_rel) ) {
  52                         // got null in tail, mutex is unlocked
  53                         /** @OPDefine: true */
  54                         return;
  55                 }
  56
  57                 // (*1) catch the race :
  58                 rl::linear_backoff bo;
  59                 for(;;) {
  60                         // FIXME: detection miss, execution never ends
  61                         next = me->next.load(std::mo_acquire);
  62                         if ( next != NULL )
  63                                 break;
  64                         thrd_yield();
  65                 }
  66         }
  67
  68         // (*2) - store to next must be done,
  69         //  so no locker can be viewing my node any more
  70
  71         /**********  Detected Correctness **********/
  72         /** Run this in the -Y mode to expose the HB bug */
  73         // let next guy in :
  74         next->gate.store( 0, std::mo_release);
  75         /** @OPDefine: true */
  76 }
  77
  78 // C-callable interface
  79
  80 /** @DeclareState: bool lock;
  81         @Initial: lock = false; */
  82
  83
  84 /** @PreCondition: return STATE(lock) == false;
  85 @Transition: STATE(lock) = true; */
  86 void mcs_lock(mcs_mutex *mutex, CGuard guard) {
  87         mcs_mutex::guard *myGuard = (mcs_mutex::guard*) guard;
  88         mutex->lock(myGuard);
  89 }
  90
  91 /** @PreCondition: return STATE(lock) == true;
  92 @Transition: STATE(lock) = false; */
  93 void mcs_unlock(mcs_mutex *mutex, CGuard guard) {
  94         mcs_mutex::guard *myGuard = (mcs_mutex::guard*) guard;
  95         mutex->unlock(myGuard);
  96 }