X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=benchmark%2Fmpmc-queue%2Fmpmc-queue.h;h=aa1012976ee8501596d27cc7852f9006ea0e1e0c;hp=d482c9e9790b62d430637b1ec9c222a386199b4a;hb=7f2fd73fe54a04e0f795e7b8f6e28b3a7708df03;hpb=635b0659aadff512de8d0ca508ecd98cce4f845c

diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h
index d482c9e..aa10129 100644
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -48,20 +48,23 @@ public:
 			LANG = CPP;
 			CLASS = mpmc_boundq_1_alt;
 		@Global_define:
-		@DeclareStruct:
-			typedef struct elem {
-				t_element *pos;
-				bool written;
-				thread_id_t tid;
-				thread_id_t fetch_tid;
-				call_id_t id;
-			} elem;
-		@DeclareVar:
-			spec_list *list;
+		//@DeclareStruct:
+			//typedef struct elem {
+			//	t_element *pos;
+			//	bool written;
+			//	thread_id_t tid;
+			//	thread_id_t fetch_tid;
+			//	call_id_t id;
+		//	} elem;
+	//	@DeclareVar:
+	//		spec_list *list;
 			//id_tag_t *tag;
-		@InitVar:
-			list = new_spec_list();
+	//	@InitVar:
+	//		list = new_spec_list();
 			//tag = new_id_tag();
+	//	@Cleanup:
+//			if (list)
+//				free_spec_list();
 	@Happens_before:
 		Publish -> Fetch
 		Consume -> Prepare
@@ -73,7 +76,7 @@ public:
 	/**
 		@Begin
 		@Interface: Fetch
-		@Commit_point_set: Fetch_Empty_Point | Fetch_Succ_Point
+		@Commit_point_set: Fetch_RW_Load_Empty | Fetch_RW_RMW | Fetch_W_Load
 		@ID: (call_id_t) __RET__
 		//@Check:
 			//__RET__ == NULL || has_elem(list, __RET__)
@@ -81,12 +84,12 @@ public:
 	*/
 	t_element * read_fetch() {
 		// Try this new weaker semantics
-		//unsigned int rdwr = m_rdwr.load(mo_acquire);
-		unsigned int rdwr = m_rdwr.load(mo_relaxed);
+		unsigned int rdwr = m_rdwr.load(mo_acquire);
+		//unsigned int rdwr = m_rdwr.load(mo_relaxed);
 		/**
 			@Begin
 			@Potential_commit_point_define: true
-			@Label: Fetch_Potential_Point
+			@Label: Fetch_Potential_RW_Load
 			@End
 		*/
 		unsigned int rd,wr;
@@ -99,8 +102,8 @@ public:
 				/**
 					@Begin
 					@Commit_point_define: true
-					@Potential_commit_point_label: Fetch_Potential_Point 
-					@Label: Fetch_Empty_Point
+					@Potential_commit_point_label: Fetch_Potential_RW_Load
+					@Label: Fetch_RW_Load_Empty
 					@End
 				*/
 
@@ -110,8 +113,8 @@ public:
 			bool succ = m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
 			/**
 				@Begin
-				@Commit_point_define_check: succ == true
-				@Label: Fetch_Succ_Point
+				@Commit_point_define_check: succ
+				@Label: Fetch_RW_RMW
 				@End
 			*/
 			if (succ)
@@ -122,9 +125,28 @@ public:
 
 		// (*1)
 		rl::backoff bo;
-		while ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) {
-			thrd_yield();
+		while (true) {
+			int written = m_written.load(mo_acquire);
+			/**
+				@Begin
+				@Potential_commit_point_define: true
+				@Label: Fetch_Potential_W_Load
+				@End
+			*/
+			if ((written & 0xFFFF) != wr) {
+				thrd_yield();
+			} else {
+				break;
+			}
 		}
+		
+		/**
+			@Begin
+			@Commit_point_define: true
+			@Potential_commit_point_label: Fetch_Potential_W_Load
+			@Label: Fetch_W_Load
+			@End
+		*/
 
 		t_element * p = & ( m_array[ rd % t_size ] );
 		
@@ -134,7 +156,7 @@ public:
 	/**
 		@Begin
 		@Interface: Consume
-		@Commit_point_set: Consume_Point
+		@Commit_point_set: Consume_R_RMW
 		@ID: (call_id_t) bin 
 		//@Check:
 		//	consume_check(__TID__)
@@ -143,11 +165,12 @@ public:
 		@End
 	*/
 	void read_consume(t_element *bin) {
+		/**** FIXME: miss ****/
 		m_read.fetch_add(1,mo_release);
 		/**
 			@Begin
 			@Commit_point_define_check: true
-			@Label: Consume_Point
+			@Label: Consume_R_RMW
 			@End
 		*/
 	}
@@ -157,7 +180,7 @@ public:
 	/**
 		@Begin
 		@Interface: Prepare 
-		@Commit_point_set: Prepare_Full_Point | Prepare_Succ_Point
+		@Commit_point_set: Prepare_RW_Load_Full | Prepare_RW_RMW | Prepare_R_Load
 		@ID: (call_id_t) __RET__
 		//@Check:
 			//prepare_check(__RET__, __TID__)
@@ -167,12 +190,12 @@ public:
 	*/
 	t_element * write_prepare() {
 		// Try weaker semantics
-		//unsigned int rdwr = m_rdwr.load(mo_acquire);
-		unsigned int rdwr = m_rdwr.load(mo_relaxed);
+		unsigned int rdwr = m_rdwr.load(mo_acquire);
+		//unsigned int rdwr = m_rdwr.load(mo_relaxed);
 		/**
 			@Begin
 			@Potential_commit_point_define: true
-			@Label: Prepare_Potential_Point
+			@Label: Prepare_Potential_RW_Load
 			@End
 		*/
 		unsigned int rd,wr;
@@ -185,8 +208,8 @@ public:
 				/**
 					@Begin
 					@Commit_point_define: true
-					@Potential_commit_point_label: Prepare_Potential_Point 
-					@Label: Prepare_Full_Point
+					@Potential_commit_point_label: Prepare_Potential_RW_Load
+					@Label: Prepare_RW_Load_Full
 					@End
 				*/
 				return NULL;
@@ -196,8 +219,8 @@ public:
 				((wr+1)&0xFFFF),mo_acq_rel);
 			/**
 				@Begin
-				@Commit_point_define_check: succ == true
-				@Label: Prepare_Succ_Point
+				@Commit_point_define_check: succ
+				@Label: Prepare_RW_RMW
 				@End
 			*/
 			if (succ)
@@ -208,10 +231,28 @@ public:
 
 		// (*1)
 		rl::backoff bo;
-		while ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) {
-			thrd_yield();
+		while (true) {
+			int read = m_read.load(mo_acquire);
+			/**
+				@Begin
+				@Potential_commit_point_define: true
+				@Label: Prepare_Potential_R_Load
+				@End
+			*/
+			if ((read & 0xFFFF) != rd)
+				thrd_yield();
+			else
+				break;
 		}
 
+		/**
+			@Begin
+			@Commit_point_define: true
+			@Potential_commit_point_label: Prepare_Potential_R_Load
+			@Label: Prepare_R_Load
+			@End
+		*/
+
 		t_element * p = & ( m_array[ wr % t_size ] );
 
 		return p;
@@ -220,7 +261,7 @@ public:
 	/**
 		@Begin
 		@Interface: Publish 
-		@Commit_point_set: Publish_Point
+		@Commit_point_set: Publish_W_RMW
 		@ID: (call_id_t) bin 
 		//@Check:
 			//publish_check(__TID__)
@@ -230,11 +271,12 @@ public:
 	*/
 	void write_publish(t_element *bin)
 	{
+		/**** hb violation ****/
 		m_written.fetch_add(1,mo_release);
 		/**
 			@Begin
 			@Commit_point_define_check: true
-			@Label: Publish_Point
+			@Label: Publish_W_RMW
 			@End
 		*/
 	}