From 4248575daeca107e83ab40cff5a0a9e4ec1d72d0 Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Tue, 25 Mar 2014 05:01:49 -0700
Subject: [PATCH] reset mpmc spec

---
 benchmark/mpmc-queue/mpmc-queue.cc |  17 +-
 benchmark/mpmc-queue/mpmc-queue.h  | 251 +++++------------------------
 2 files changed, 50 insertions(+), 218 deletions(-)

diff --git a/benchmark/mpmc-queue/mpmc-queue.cc b/benchmark/mpmc-queue/mpmc-queue.cc
index cfa82f2..ca063e9 100644
--- a/benchmark/mpmc-queue/mpmc-queue.cc
+++ b/benchmark/mpmc-queue/mpmc-queue.cc
@@ -12,8 +12,9 @@ void threadA(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
 {
 	int32_t *bin = queue->write_prepare();
 	store_32(bin, 1);
+	*bin = 1;
 	printf("write_bin %d, val %d\n", bin, 1);
-	queue->write_publish();
+	queue->write_publish(bin);
 }
 
 void threadB(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
@@ -22,7 +23,8 @@ void threadB(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
 	while (bin = queue->read_fetch()) {
 		printf("Read: %d\n", load_32(bin));
 		printf("read_bin %d, val %d\n", bin, load_32(bin));
-		queue->read_consume();
+		printf("Read: %d\n", *bin);
+		queue->read_consume(bin);
 	}
 }
 
@@ -30,11 +32,13 @@ void threadC(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
 {
 	int32_t *bin = queue->write_prepare();
 	store_32(bin, 1);
-	queue->write_publish();
+	*bin = 1;
+	queue->write_publish(bin);
 
 	while (bin = queue->read_fetch()) {
 		printf("Read: %d\n", load_32(bin));
-		queue->read_consume();
+		printf("Read: %d\n", *bin);
+		queue->read_consume(bin);
 	}
 }
 
@@ -104,7 +108,7 @@ void process_params(int argc, char **argv)
 
 int user_main(int argc, char **argv)
 {
-	struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> queue;
+	struct mpmc_boundq_1_alt<int32_t, 2> queue;
 	thrd_t A[MAXWRITERS], B[MAXREADERS], C[MAXRDWR];
 
 	/* Note: optarg() / optind is broken in model-checker - workaround is
@@ -116,8 +120,9 @@ int user_main(int argc, char **argv)
 	printf("Adding initial element\n");
 	int32_t *bin = queue.write_prepare();
 	store_32(bin, 17);
+	*bin, 17;
 	printf("init_write_bin %d, val %d\n", bin, 17);
-	queue.write_publish();
+	queue.write_publish(bin);
 #endif
 
 	printf("Start threads\n");
diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h
index ee3950d..e6d5485 100644
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -2,6 +2,12 @@
 #include <unrelacy.h>
 #include <common.h>
 
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+
 /**
 	@Begin
 	@Class_begin
@@ -52,199 +58,13 @@ public:
 			} elem;
 		@DeclareVar:
 			spec_list *list;
-			id_tag_t *tag;
+			//id_tag_t *tag;
 		@InitVar:
 			list = new_spec_list();
-			tag = new_id_tag();
-		@DefineFunc:
-			elem* new_elem(t_element *pos, call_id_t id, thread_id_t tid) {
-				elem *e = (elem*) MODEL_MALLOC(sizeof(elem));
-				e->pos = pos;
-				e->written = false;
-				e->id = id;
-				e->tid = tid;
-				e->fetch_tid = -1;
-			}
-		@DefineFunc:
-			elem* get_elem_by_pos(t_element *pos) {
-				for (int i = 0; i < size(list); i++) {
-					elem *e = (elem*) elem_at_index(list, i);
-					if (e->pos == pos) {
-						return e;
-					}
-				}
-				return NULL;
-			}
-		@DefineFunc:
-			void show_list() {
-				//model_print("Status:\n");
-				for (int i = 0; i < size(list); i++) {
-					elem *e = (elem*) elem_at_index(list, i);
-					//model_print("%d: pos %d, written %d, tid %d, fetch_tid %d, call_id %d\n", i, e->pos, e->written, e->tid, e->fetch_tid, e->id); 
-				}
-			}
-		@DefineFunc:
-			elem* get_elem_by_tid(thread_id_t tid) {
-				for (int i = 0; i < size(list); i++) {
-					elem *e = (elem*) elem_at_index(list, i);
-					if (e->tid== tid) {
-						return e;
-					}
-				}
-				return NULL;
-			}
-		@DefineFunc:
-			elem* get_elem_by_fetch_tid(thread_id_t fetch_tid) {
-				for (int i = 0; i < size(list); i++) {
-					elem *e = (elem*) elem_at_index(list, i);
-					if (e->fetch_tid== fetch_tid) {
-						return e;
-					}
-				}
-				return NULL;
-			}
-		@DefineFunc:
-			int elem_idx_by_pos(t_element *pos) {
-				for (int i = 0; i < size(list); i++) {
-					elem *existing = (elem*) elem_at_index(list, i);
-					if (pos == existing->pos) {
-						return i;
-					}
-				}
-				return -1;
-			}
-		@DefineFunc:
-			int elem_idx_by_tid(thread_id_t tid) {
-				for (int i = 0; i < size(list); i++) {
-					elem *existing = (elem*) elem_at_index(list, i);
-					if (tid == existing->tid) {
-						return i;
-					}
-				}
-				return -1;
-			}
-		@DefineFunc:
-			int elem_idx_by_fetch_tid(thread_id_t fetch_tid) {
-				for (int i = 0; i < size(list); i++) {
-					elem *existing = (elem*) elem_at_index(list, i);
-					if (fetch_tid == existing->fetch_tid) {
-						return i;
-					}
-				}
-				return -1;
-			}
-		@DefineFunc:
-			int elem_num(t_element *pos) {
-				int cnt = 0;
-				for (int i = 0; i < size(list); i++) {
-					elem *existing = (elem*) elem_at_index(list, i);
-					if (pos == existing->pos) {
-						cnt++;
-					}
-				}
-				return cnt;
-			}
-		@DefineFunc:
-			call_id_t prepare_id() {
-				call_id_t res = get_and_inc(tag);
-				//model_print("prepare_id: %d\n", res);
-				return res;
-			}
-		@DefineFunc:
-			bool prepare_check(t_element *pos, thread_id_t tid) {
-				show_list();
-				elem *e = get_elem_by_pos(pos);
-				//model_print("prepare_check: e %d\n", e);
-				return NULL == e;
-			}
-		@DefineFunc:
-			void prepare(call_id_t id, t_element *pos, thread_id_t tid) {
-				//model_print("prepare: id %d, pos %d, tid %d\n", id, pos, tid);
-				elem *e = new_elem(pos, id, tid);
-				push_back(list, e);
-			}
-		@DefineFunc:
-			call_id_t publish_id(thread_id_t tid) {
-				elem *e = get_elem_by_tid(tid);
-				//model_print("publish_id: id %d\n", e == NULL ? 0 : e->id);
-				if (NULL == e)
-					return DEFAULT_CALL_ID;
-				return e->id;
-			}
-		@DefineFunc:
-			bool publish_check(thread_id_t tid) {
-				show_list();
-				elem *e = get_elem_by_tid(tid);
-				//model_print("publish_check: tid %d\n", tid);
-				if (NULL == e)
-					return false;
-				if (elem_num(e->pos) > 1)
-					return false;
-				return !e->written;
-			}
-		@DefineFunc:
-			void publish(thread_id_t tid) {
-				//model_print("publish: tid %d\n", tid);
-				elem *e = get_elem_by_tid(tid);
-				e->written = true;
-			}
-		@DefineFunc:
-			call_id_t fetch_id(t_element *pos) {
-				elem *e = get_elem_by_pos(pos);
-				//model_print("fetch_id: id %d\n", e == NULL ? 0 : e->id);
-				if (NULL == e)
-					return DEFAULT_CALL_ID;
-				return e->id;
-			}
-		@DefineFunc:
-			bool fetch_check(t_element *pos) {
-				show_list();
-				if (pos == NULL) return true;
-				elem *e = get_elem_by_pos(pos);
-				//model_print("fetch_check: pos %d, e %d\n", pos, e);
-				if (e == NULL) return false;
-				if (elem_num(e->pos) > 1)
-					return false;
-				return true;
-			}
-		@DefineFunc:
-			void fetch(t_element *pos, thread_id_t tid) {
-				if (pos == NULL) return;
-				elem *e = (elem*) get_elem_by_pos(pos);
-				//model_print("fetch: pos %d, tid %d\n", pos, tid);
-				// Remember the thread that fetches the position
-				e->fetch_tid = tid;
-			}
-		@DefineFunc:
-			bool consume_check(thread_id_t tid) {
-				show_list();
-				elem *e = get_elem_by_fetch_tid(tid);
-				//model_print("consume_check: tid %d, e %d\n", tid, e);
-				if (NULL == e)
-					return false;
-				if (elem_num(e->pos) > 1)
-					return false;
-				return e->written;
-			}
-		@DefineFunc:
-			call_id_t consume_id(thread_id_t tid) {
-				elem *e = get_elem_by_fetch_tid(tid);
-				//model_print("consume_id: id %d\n", e == NULL ? 0 : e->id);
-				if (NULL == e)
-					return DEFAULT_CALL_ID;
-				return e->id;
-			}
-		@DefineFunc:
-			void consume(thread_id_t tid) {
-				//model_print("consume: tid %d\n", tid);
-				int idx = elem_idx_by_fetch_tid(tid);
-				if (idx == -1)
-					return;
-				remove_at_index(list, idx);
-			}
+			//tag = new_id_tag();
 	@Happens_before:
-		Prepare -> Fetch
-		Publish -> Consume
+		Publish -> Fetch
+		Consume -> Prepare
 	@End
 	*/
 
@@ -254,15 +74,15 @@ public:
 		@Begin
 		@Interface: Fetch
 		@Commit_point_set: Fetch_Empty_Point | Fetch_Succ_Point
-		@ID: fetch_id(__RET__)
-		@Check:
-			fetch_check(__RET__)
-		@Action:
-			fetch(__RET__, __TID__);
+		@ID: (call_id_t) __RET__
+		//@Check:
+			//__RET__ == NULL || has_elem(list, __RET__)
 		@End
 	*/
 	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);
 		/**
 			@Begin
 			@Potential_commit_point_define: true
@@ -275,6 +95,7 @@ public:
 			wr = rdwr & 0xFFFF;
 
 			if ( wr == rd ) { // empty
+
 				/**
 					@Begin
 					@Commit_point_define: true
@@ -282,6 +103,7 @@ public:
 					@Label: Fetch_Empty_Point
 					@End
 				*/
+
 				return false;
 			}
 			
@@ -313,14 +135,15 @@ public:
 		@Begin
 		@Interface: Consume
 		@Commit_point_set: Consume_Point
-		@ID: consume_id(__TID__)
-		@Check:
-			consume_check(__TID__)
-		@Action:
-			consume(__TID__);
+		@ID: (call_id_t) bin 
+		//@Check:
+		//	consume_check(__TID__)
+		//@Action:
+			//consume(__TID__);
 		@End
 	*/
-	void read_consume() {
+	void read_consume(t_element *bin) {
+		/**** FIXME: miss ****/
 		m_read.fetch_add(1,mo_release);
 		/**
 			@Begin
@@ -336,15 +159,17 @@ public:
 		@Begin
 		@Interface: Prepare 
 		@Commit_point_set: Prepare_Full_Point | Prepare_Succ_Point
-		@ID: prepare_id()
-		@Check:
-			prepare_check(__RET__, __TID__)
-		@Action:
-			prepare(__ID__, __RET__, __TID__);
+		@ID: (call_id_t) __RET__
+		//@Check:
+			//prepare_check(__RET__, __TID__)
+		//@Action:
+			//push_back(list, __RET__);
 		@End
 	*/
 	t_element * write_prepare() {
+		// Try weaker semantics
 		unsigned int rdwr = m_rdwr.load(mo_acquire);
+		//unsigned int rdwr = m_rdwr.load(mo_relaxed);
 		/**
 			@Begin
 			@Potential_commit_point_define: true
@@ -357,6 +182,7 @@ public:
 			wr = rdwr & 0xFFFF;
 
 			if ( wr == ((rd + t_size)&0xFFFF) ) { // full
+
 				/**
 					@Begin
 					@Commit_point_define: true
@@ -396,15 +222,16 @@ public:
 		@Begin
 		@Interface: Publish 
 		@Commit_point_set: Publish_Point
-		@ID: publish_id(__TID__)
-		@Check:
-			publish_check(__TID__)
-		@Action:
-			publish(__TID__);
+		@ID: (call_id_t) bin 
+		//@Check:
+			//publish_check(__TID__)
+		//@Action:
+			//publish(__TID__);
 		@End
 	*/
-	void write_publish()
+	void write_publish(t_element *bin)
 	{
+		/**** hb violation ****/
 		m_written.fetch_add(1,mo_release);
 		/**
 			@Begin
-- 
2.34.1