From: Peizhao Ou <peizhaoo@uci.edu>
Date: Sat, 22 Mar 2014 22:33:58 +0000 (-0700)
Subject: mcslock
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=aa49c958dfc91fbde45be2a4aa1c5ce2fa5f0c1e

mcslock
---

diff --git a/benchmark/mcs-lock/mcs-lock.cc b/benchmark/mcs-lock/mcs-lock.cc
index 00817ee..d436894 100644
--- a/benchmark/mcs-lock/mcs-lock.cc
+++ b/benchmark/mcs-lock/mcs-lock.cc
@@ -12,25 +12,25 @@ static uint32_t shared;
 void threadA(void *arg)
 {
 	mcs_mutex::guard g(mutex);
-	printf("store: %d\n", 17);
-	//store_32(&shared, 17);
-	shared = 17;
+	//printf("store: %d\n", 17);
+	store_32(&shared, 17);
+	//shared = 17;
 	mutex->unlock(&g);
 	mutex->lock(&g);
-	//printf("load: %u\n", load_32(&shared));
-	printf("load: %u\n", shared);
+	printf("load: %u\n", load_32(&shared));
+	//printf("load: %u\n", shared);
 }
 
 void threadB(void *arg)
 {
 	mcs_mutex::guard g(mutex);
-	//printf("load: %u\n", load_32(&shared));
-	printf("load: %u\n", shared);
+	printf("load: %u\n", load_32(&shared));
+	//printf("load: %u\n", shared);
 	mutex->unlock(&g);
 	mutex->lock(&g);
 	printf("store: %d\n", 17);
-	shared = 17;
-	//store_32(&shared, 17);
+	//shared = 17;
+	store_32(&shared, 17);
 }
 
 int user_main(int argc, char **argv)
diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h
index af31894..a27b37e 100644
--- a/benchmark/mcs-lock/mcs-lock.h
+++ b/benchmark/mcs-lock/mcs-lock.h
@@ -82,7 +82,6 @@ public:
 		me->gate.store(1, std::mo_relaxed );
 
 		// publish my node as the new tail :
-		// FIXME: Only weakening the mo_acq_rel cause the spec error
 		mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
 		/**
 			@Begin
@@ -95,6 +94,7 @@ public:
 			// unlock of pred can see me in the tail before I fill next
 
 			// publish me to previous lock-holder :
+			// FIXME: detection miss  
 			pred->next.store(me, std::mo_release );
 
 			// (*2) pred not touched any more       
@@ -105,6 +105,8 @@ public:
 			int my_gate = 1;
 			while (my_gate ) {
 				my_gate = me->gate.load(std::mo_acquire);
+				if (my_gate == 0)
+					printf("lock at gate!\n");
 				/**
 					@Begin
 					@Commit_point_define_check: my_gate == 0
@@ -130,12 +132,12 @@ public:
 	void unlock(guard * I) {
 		mcs_node * me = &(I->m_node);
 
+		// FIXME: detection miss  
 		mcs_node * next = me->next.load(std::mo_acquire);
 		if ( next == NULL )
 		{
 			mcs_node * tail_was_me = me;
 			bool success;
-			// FIXME: Only weakening the mo_acq_rel cause the spec error
 			success = m_tail.compare_exchange_strong(
 				tail_was_me,NULL,std::mo_acq_rel);
 			/**
@@ -153,6 +155,7 @@ public:
 			// (*1) catch the race :
 			rl::linear_backoff bo;
 			for(;;) {
+				// FIXME: detection miss  
 				next = me->next.load(std::mo_acquire);
 				if ( next != NULL )
 					break;