The CDSSpec checker's benchmarks

[model-checker-benchmarks.git] / mcs-lock / mcs-lock.h

diff --git a/mcs-lock/mcs-lock.h b/mcs-lock/mcs-lock.h
index 4b808f7c3c9b9bbc7effe6b4e6c570f2712e5232..012d04c95a9deef38556977d9f2acb85d4509134 100644 (file)
--- a/mcs-lock/mcs-lock.h
+++ b/mcs-lock/mcs-lock.h
@@ -1,8 +1,16 @@
 // mcs on stack
 
+#ifndef _MCS_LOCK_H
+#define _MCS_LOCK_H
+
 #include <stdatomic.h>
+#include <threads.h>
 #include <unrelacy.h>
 
+// Forward declaration
+struct mcs_node;
+struct mcs_mutex;
+
 struct mcs_node {
        std::atomic<mcs_node *> next;
        std::atomic<int> gate;
@@ -13,6 +21,12 @@ struct mcs_node {
        }
 };
 
+// C-callable interface
+typedef void *CGuard;
+void mcs_lock(mcs_mutex *mutex, CGuard guard);
+
+void mcs_unlock(mcs_mutex *mutex, CGuard guard);
+
 struct mcs_mutex {
 public:
        // tail is null when lock is not held
@@ -22,72 +36,22 @@ public:
                m_tail.store( NULL );
        }
        ~mcs_mutex() {
-               ASSERT( m_tail.load() == NULL );
+               RL_ASSERT( m_tail.load() == NULL );
        }
 
        class guard {
        public:
                mcs_mutex * m_t;
                mcs_node    m_node; // node held on the stack
-
-               guard(mcs_mutex * t) : m_t(t) { t->lock(this); }
-               ~guard() { m_t->unlock(this); }
+               
+               // Call the wrapper (instrument every lock/unlock)
+               guard(mcs_mutex * t) : m_t(t) { mcs_lock(t, this); }
+               ~guard() { mcs_unlock(m_t, this); }
        };
 
-       void lock(guard * I) {
-               mcs_node * me = &(I->m_node);
-
-               // set up my node :
-               // not published yet so relaxed :
-               me->next.store(NULL, std::mo_relaxed );
-               me->gate.store(1, std::mo_relaxed );
-
-               // publish my node as the new tail :
-               mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
-               if ( pred != NULL ) {
-                       // (*1) race here
-                       // unlock of pred can see me in the tail before I fill next
-
-                       // publish me to previous lock-holder :
-                       pred->next.store(me, std::mo_release );
-
-                       // (*2) pred not touched any more       
+       void lock(guard * I);
 
-                       // now this is the spin -
-                       // wait on predecessor setting my flag -
-                       rl::linear_backoff bo;
-                       while ( me->gate.load(std::mo_acquire) ) {
-                               thrd_yield();
-                       }
-               }
-       }
-
-       void unlock(guard * I) {
-               mcs_node * me = &(I->m_node);
-
-               mcs_node * next = me->next.load(std::mo_acquire);
-               if ( next == NULL )
-               {
-                       mcs_node * tail_was_me = me;
-                       if ( m_tail.compare_exchange_strong( tail_was_me,NULL,std::mo_acq_rel) ) {
-                               // got null in tail, mutex is unlocked
-                               return;
-                       }
-
-                       // (*1) catch the race :
-                       rl::linear_backoff bo;
-                       for(;;) {
-                               next = me->next.load(std::mo_acquire);
-                               if ( next != NULL )
-                                       break;
-                               thrd_yield();
-                       }
-               }
-
-               // (*2) - store to next must be done,
-               //  so no locker can be viewing my node any more        
-
-               // let next guy in :
-               next->gate.store( 0, std::mo_release );
-       }
+       void unlock(guard * I);
 };
+
+#endif