X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=benchmark%2Fmcs-lock%2Fmcs-lock.h;h=9f4781246e0e2c0cea2c308e2cbc409f9cc281fb;hp=a27b37e0431d281934ed1ee9c3ae9d0176de7405;hb=17e78d57c56a42f19fde853278907d7bf4bb9bec;hpb=aa49c958dfc91fbde45be2a4aa1c5ce2fa5f0c1e

diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h
index a27b37e..9f47812 100644
--- 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:
-			@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
 	*/
 
@@ -67,10 +64,8 @@ public:
 		@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) {
@@ -81,6 +76,8 @@ public:
 		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);
 		/**
@@ -94,8 +91,11 @@ public:
 			// 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 );
+			//printf("lock_miss1\n");
 
 			// (*2) pred not touched any more       
 
@@ -104,9 +104,10 @@ public:
 			rl::linear_backoff bo;
 			int my_gate = 1;
 			while (my_gate ) {
+				/**********  Inadmissibility  *********/
 				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
@@ -121,23 +122,23 @@ public:
 	/**
 		@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);
 
-		// FIXME: detection miss  
+		// FIXME: detection miss, execution never ends
 		mcs_node * next = me->next.load(std::mo_acquire);
+		//printf("unlock_miss2\n");
 		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);
 			/**
@@ -155,8 +156,9 @@ public:
 			// (*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);
+				//printf("unlock_miss3\n");
 				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        
 
+		/**********  Inadmissible  **********/
 		// let next guy in :
 		next->gate.store( 0, std::mo_release );
 		/**