edits

[cdsspec-compiler.git] / benchmark / mcs-lock / mcs-lock.h

diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h
index a27b37e0431d281934ed1ee9c3ae9d0176de7405..9f4781246e0e2c0cea2c308e2cbc409f9cc281fb 100644 (file)
--- a/benchmark/mcs-lock/mcs-lock.h
+++ b/benchmark/mcs-lock/mcs-lock.h
@@ -54,12 +54,9 @@ public:
                        LANG = CPP;
                        CLASS = mcs_mutex;
                @Global_define:
                        LANG = CPP;
                        CLASS = mcs_mutex;
                @Global_define:

-                       @DeclareVar:
-                               bool _lock_acquired;
-                       @InitVar:
-                               _lock_acquired = false;
-               @Happens_before:
-                       Unlock -> Lock
+                       @DeclareVar: bool _lock_acquired;
+                       @InitVar: _lock_acquired = false;
+               @Happens_before: Unlock -> Lock

                @End
        */
 
                @End
        */
 


@@ -67,10 +64,8 @@ public:
                @Begin
                @Interface: Lock
                @Commit_point_set: Lock_Enqueue_Point1 | Lock_Enqueue_Point2
                @Begin
                @Interface: Lock
                @Commit_point_set: Lock_Enqueue_Point1 | Lock_Enqueue_Point2

-               @Check:
-                       _lock_acquired == false;
-               @Action:
-                       _lock_acquired = true;
+               @Check: _lock_acquired == false;
+               @Action: _lock_acquired = true;

                @End
        */
        void lock(guard * I) {
                @End
        */
        void lock(guard * I) {


@@ -81,6 +76,8 @@ public:
                me->next.store(NULL, std::mo_relaxed );
                me->gate.store(1, std::mo_relaxed );
 
                me->next.store(NULL, std::mo_relaxed );
                me->gate.store(1, std::mo_relaxed );
 

+               /**********  Inadmissible  **********/
+               /** Run this in the -Y mode to expose the HB bug */

                // publish my node as the new tail :
                mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
                /**
                // publish my node as the new tail :
                mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
                /**


@@ -94,8 +91,11 @@ public:
                        // unlock of pred can see me in the tail before I fill next
 
                        // publish me to previous lock-holder :
                        // unlock of pred can see me in the tail before I fill next
 
                        // publish me to previous lock-holder :

-                       // FIXME: detection miss  
+                       // FIXME: detection miss, execution never ends
+                       // If this is relaxed, the store 0 to gate will be read before and
+                       // that lock will never ends.

                        pred->next.store(me, std::mo_release );
                        pred->next.store(me, std::mo_release );

+                       //printf("lock_miss1\n");

 
                        // (*2) pred not touched any more       
 
 
                        // (*2) pred not touched any more       
 


@@ -104,9 +104,10 @@ public:
                        rl::linear_backoff bo;
                        int my_gate = 1;
                        while (my_gate ) {
                        rl::linear_backoff bo;
                        int my_gate = 1;
                        while (my_gate ) {

+                               /**********  Inadmissibility  *********/

                                my_gate = me->gate.load(std::mo_acquire);
                                my_gate = me->gate.load(std::mo_acquire);

-                               if (my_gate == 0)
-                                       printf("lock at gate!\n");
+                               //if (my_gate == 0)
+                                       //printf("lock at gate!\n");

                                /**
                                        @Begin
                                        @Commit_point_define_check: my_gate == 0
                                /**
                                        @Begin
                                        @Commit_point_define_check: my_gate == 0


@@ -121,23 +122,23 @@ public:
        /**
                @Begin
                @Interface: Unlock
        /**
                @Begin
                @Interface: Unlock

-               @Commit_point_set:
-                       Unlock_Point_Success_1 | Unlock_Point_Success_2
-               @Check:
-                       _lock_acquired == true
-               @Action:
-                       _lock_acquired = false;
+               @Commit_point_set: Unlock_Point_Success_1 | Unlock_Point_Success_2
+               @Check: _lock_acquired == true
+               @Action: _lock_acquired = false;

                @End
        */
        void unlock(guard * I) {
                mcs_node * me = &(I->m_node);
 
                @End
        */
        void unlock(guard * I) {
                mcs_node * me = &(I->m_node);
 

-               // FIXME: detection miss  
+               // FIXME: detection miss, execution never ends

                mcs_node * next = me->next.load(std::mo_acquire);
                mcs_node * next = me->next.load(std::mo_acquire);

+               //printf("unlock_miss2\n");

                if ( next == NULL )
                {
                        mcs_node * tail_was_me = me;
                        bool success;
                if ( next == NULL )
                {
                        mcs_node * tail_was_me = me;
                        bool success;

+
+                       /**********  Inadmissible  **********/

                        success = m_tail.compare_exchange_strong(
                                tail_was_me,NULL,std::mo_acq_rel);
                        /**
                        success = m_tail.compare_exchange_strong(
                                tail_was_me,NULL,std::mo_acq_rel);
                        /**


@@ -155,8 +156,9 @@ public:
                        // (*1) catch the race :
                        rl::linear_backoff bo;
                        for(;;) {
                        // (*1) catch the race :
                        rl::linear_backoff bo;
                        for(;;) {

-                               // FIXME: detection miss  
+                               // FIXME: detection miss, execution never ends

                                next = me->next.load(std::mo_acquire);
                                next = me->next.load(std::mo_acquire);

+                               //printf("unlock_miss3\n");

                                if ( next != NULL )
                                        break;
                                thrd_yield();
                                if ( next != NULL )
                                        break;
                                thrd_yield();


@@ -166,6 +168,7 @@ public:
                // (*2) - store to next must be done,
                //  so no locker can be viewing my node any more        
 
                // (*2) - store to next must be done,
                //  so no locker can be viewing my node any more        
 

+               /**********  Inadmissible  **********/

                // let next guy in :
                next->gate.store( 0, std::mo_release );
                /**
                // let next guy in :
                next->gate.store( 0, std::mo_release );
                /**