X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=benchmark%2Fmcs-lock%2Fmcs-lock.h;fp=benchmark%2Fmcs-lock%2Fmcs-lock.h;h=0000000000000000000000000000000000000000;hb=d2ea20dfe024fdf297e6776d56bc9066cb040f38;hp=9f4781246e0e2c0cea2c308e2cbc409f9cc281fb;hpb=facdc9fd49c05b968c55c54deb21ba5d3a673f52;p=cdsspec-compiler.git

diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h
deleted file mode 100644
index 9f47812..0000000
--- a/benchmark/mcs-lock/mcs-lock.h
+++ /dev/null
@@ -1,186 +0,0 @@
-// mcs on stack
-
-#include <stdatomic.h>
-#include <unrelacy.h>
-
-#include <spec_lib.h>
-#include <stdlib.h>
-#include <cdsannotate.h>
-#include <specannotation.h>
-#include <model_memory.h>
-#include "common.h" 
-
-struct mcs_node {
-	std::atomic<mcs_node *> next;
-	std::atomic<int> gate;
-
-	mcs_node() {
-		next.store(0);
-		gate.store(0);
-	}
-};
-
-
-struct mcs_mutex {
-public:
-	// tail is null when lock is not held
-	std::atomic<mcs_node *> m_tail;
-
-	mcs_mutex() {
-		/**
-			@Begin
-	        @Entry_point
-			@End
-		*/
-		m_tail.store( NULL );
-	}
-	~mcs_mutex() {
-		//ASSERT( m_tail.load() == NULL );
-	}
-
-	// Each thread will have their own guard.
-	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); }
-	};
-
-	/**
-		@Begin
-		@Options:
-			LANG = CPP;
-			CLASS = mcs_mutex;
-		@Global_define:
-			@DeclareVar: bool _lock_acquired;
-			@InitVar: _lock_acquired = false;
-		@Happens_before: Unlock -> Lock
-		@End
-	*/
-
-	/**
-		@Begin
-		@Interface: Lock
-		@Commit_point_set: Lock_Enqueue_Point1 | Lock_Enqueue_Point2
-		@Check: _lock_acquired == false;
-		@Action: _lock_acquired = true;
-		@End
-	*/
-	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 );
-
-		/**********  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);
-		/**
-			@Begin
-			@Commit_point_define_check: pred == NULL
-			@Label: Lock_Enqueue_Point1
-			@End
-		*/
-		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 :
-			// 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       
-
-			// now this is the spin -
-			// wait on predecessor setting my flag -
-			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");
-				/**
-					@Begin
-					@Commit_point_define_check: my_gate == 0
-					@Label: Lock_Enqueue_Point2
-					@End
-				*/
-				thrd_yield();
-			}
-		}
-	}
-
-	/**
-		@Begin
-		@Interface: Unlock
-		@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, 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);
-			/**
-				@Begin
-				@Commit_point_define_check: success == true
-				@Label: Unlock_Point_Success_1
-				@End
-			*/
-			if (success) {
-				
-				// got null in tail, mutex is unlocked
-				return;
-			}
-
-			// (*1) catch the race :
-			rl::linear_backoff bo;
-			for(;;) {
-				// FIXME: detection miss, execution never ends
-				next = me->next.load(std::mo_acquire);
-				//printf("unlock_miss3\n");
-				if ( next != NULL )
-					break;
-				thrd_yield();
-			}
-		}
-
-		// (*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 );
-		/**
-			@Begin
-			@Commit_point_define_check: true
-			@Label: Unlock_Point_Success_2
-			@End
-		*/
-	}
-};
-/**
-	@Begin
-	@Class_end
-	@End
-*/