From: Peizhao Ou <peizhaoo@uci.edu>
Date: Mon, 24 Mar 2014 02:07:34 +0000 (-0700)
Subject: save
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=8c57e2fa7111492857dab6ed3faf4c27a6533470

save
;
;
---

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index 1ebeb13..9fbc426 100644
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -24,6 +24,7 @@ int take(Deque *q) {
 	size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
 	Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
 	atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
+	/**** detected correctness ****/
 	atomic_thread_fence(memory_order_seq_cst);
 	size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
 	/**
@@ -79,7 +80,7 @@ void resize(Deque *q) {
 	for(i=top; i < bottom; i++) {
 		atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
 	}
-	/**** FIXME: detected failure ****/
+	/**** detected UL ****/
 	atomic_store_explicit(&q->array, new_a, memory_order_release);
 	printf("resize\n");
 }
@@ -91,7 +92,7 @@ void resize(Deque *q) {
 */
 void push(Deque *q, int x) {
 	size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
-	/**** FIXME: detected correctness ****/
+	/**** detected correctness ****/
 	size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
 	Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
 	if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ {
@@ -107,6 +108,7 @@ void push(Deque *q, int x) {
 		@Label: Push_Point
 		@End
 	*/
+	/**** correctness error ****/
 	atomic_thread_fence(memory_order_release);
 	
 	atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
@@ -121,7 +123,9 @@ void push(Deque *q, int x) {
 int steal(Deque *q) {
 	//FIXME: weaken the following acquire causes no spec problem
 	size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
+	//FIXME: remove the fence causes no error and fewer executions..
 	atomic_thread_fence(memory_order_seq_cst);
+	/**** detected UL ****/
 	size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
 	/**
 		@Begin
@@ -132,6 +136,7 @@ int steal(Deque *q) {
 	int x = EMPTY;
 	if (t < b) {
 		/* Non-empty queue. */
+		/**** detected UL ****/
 		Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
 		int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 		x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
@@ -141,7 +146,7 @@ int steal(Deque *q) {
 			@Label: Potential_Steal
 			@End
 		*/
-		
+		/**** detected correctness failure ****/ 
 		bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
 			memory_order_seq_cst, memory_order_relaxed);
 		/**
diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h
index 6bb4698..8a3e857 100644
--- a/benchmark/chase-lev-deque-bugfix/deque.h
+++ b/benchmark/chase-lev-deque-bugfix/deque.h
@@ -47,11 +47,17 @@ typedef struct {
             }
         @DefineFunc:
             call_id_t get_id(void *wrapper) {
-                return ((tag_elem_t*) wrapper)->id;
+				tag_elem_t *res = (tag_elem_t*) wrapper;
+				if (res == NULL) {
+					//model_print("wrong id here\n");
+					return 0;
+				}
+                return res->id;
             }
         @DefineFunc:
             int get_data(void *wrapper) {
-                return ((tag_elem_t*) wrapper)->data;
+				tag_elem_t *res = (tag_elem_t*) wrapper;
+                return res->data;
             }
     @Happens_before:
         Push -> Steal
diff --git a/benchmark/chase-lev-deque-bugfix/main.c b/benchmark/chase-lev-deque-bugfix/main.c
index 782539e..1906f1d 100644
--- a/benchmark/chase-lev-deque-bugfix/main.c
+++ b/benchmark/chase-lev-deque-bugfix/main.c
@@ -15,6 +15,7 @@ int c;
 
 static void task(void * param) {
 	a=steal(q);
+	a=steal(q);
 }
 
 int user_main(int argc, char **argv)
diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h
index ff5d9c3..645531f 100644
--- a/benchmark/cliffc-hashtable/cliffc_hashtable.h
+++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h
@@ -259,7 +259,7 @@ friend class CHM;
 			kvs_data *desired = (kvs_data*) NULL;
 			kvs_data *expected = (kvs_data*) newkvs; 
 			if (!_newkvs.compare_exchange_strong(desired, expected, memory_order_release,
-					memory_order_release)) {
+					memory_order_relaxed)) {
 				// Should clean the allocated area
 				delete newkvs;
 				newkvs = _newkvs.load(memory_order_acquire);
@@ -283,7 +283,7 @@ friend class CHM;
 					copyidx = _copy_idx.load(memory_order_acquire);
 					while (copyidx < (oldlen << 1) &&
 						!_copy_idx.compare_exchange_strong(copyidx, copyidx +
-							min_copy_work, memory_order_release, memory_order_release))
+							min_copy_work, memory_order_release, memory_order_relaxed))
 						copyidx = _copy_idx.load(memory_order_relaxed);
 					if (!(copyidx < (oldlen << 1)))
 						panic_start = copyidx;
@@ -332,7 +332,7 @@ friend class CHM;
 				topmap->_kvs.load(memory_order_acquire) == oldkvs) {
 				kvs_data *newkvs = _newkvs.load(memory_order_acquire);
 				topmap->_kvs.compare_exchange_strong(oldkvs, newkvs, memory_order_release,
-					memory_order_release);
+					memory_order_relaxed);
 			}
 		}
 	
@@ -648,7 +648,7 @@ friend class CHM;
 	// inserted keys
 	static inline bool CAS_key(kvs_data *kvs, int idx, void *expected, void *desired) {
 		return kvs->_data[2 * idx + 2].compare_exchange_strong(expected,
-			desired, memory_order_release, memory_order_release);
+			desired, memory_order_release, memory_order_relaxed);
 	}
 
 	/**
@@ -660,7 +660,7 @@ friend class CHM;
 	static inline bool CAS_val(kvs_data *kvs, int idx, void *expected, void
 		*desired) {
 		bool res =  kvs->_data[2 * idx + 3].compare_exchange_strong(expected,
-			desired, memory_order_release, memory_order_release);
+			desired, memory_order_release, memory_order_relaxed);
 		/**
 			# If it is a successful put instead of a copy or any other internal
 			# operantions, expected != NULL
diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h
index 4714567..a165437 100644
--- a/benchmark/mcs-lock/mcs-lock.h
+++ b/benchmark/mcs-lock/mcs-lock.h
@@ -96,6 +96,7 @@ public:
 			// publish me to previous lock-holder :
 			// FIXME: detection miss, don't think it's necessary  
 			pred->next.store(me, std::mo_release );
+			printf("lock_miss1\n");
 
 			// (*2) pred not touched any more       
 
@@ -134,6 +135,7 @@ public:
 
 		// FIXME: detection miss, don't think it's necessary
 		mcs_node * next = me->next.load(std::mo_acquire);
+		printf("unlock_miss2\n");
 		if ( next == NULL )
 		{
 			mcs_node * tail_was_me = me;
@@ -157,6 +159,7 @@ public:
 			for(;;) {
 				// FIXME: detection miss, don't think it's necessary
 				next = me->next.load(std::mo_acquire);
+				printf("unlock_miss3\n");
 				if ( next != NULL )
 					break;
 				thrd_yield();
diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h
index d482c9e..e6d5485 100644
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -81,8 +81,8 @@ 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
@@ -143,6 +143,7 @@ public:
 		@End
 	*/
 	void read_consume(t_element *bin) {
+		/**** FIXME: miss ****/
 		m_read.fetch_add(1,mo_release);
 		/**
 			@Begin
@@ -167,8 +168,8 @@ 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
@@ -230,6 +231,7 @@ public:
 	*/
 	void write_publish(t_element *bin)
 	{
+		/**** hb violation ****/
 		m_written.fetch_add(1,mo_release);
 		/**
 			@Begin
diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index c8d160b..12cf32e 100644
--- a/benchmark/ms-queue/main.c
+++ b/benchmark/ms-queue/main.c
@@ -36,7 +36,9 @@ static void main_task(void *param)
 	} else {
 		input[1] = 37;
 		enqueue(queue, input[1]);
-		output[1] = dequeue(queue);
+		//output[1] = dequeue(queue);
+		output[0] = dequeue(queue);
+		output[0] = dequeue(queue);
 	}
 }
 
diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 2b90fe5..0d64ed8 100644
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -101,7 +101,7 @@ void enqueue(queue_t *q, unsigned int val)
 	atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
 
 	while (!success) {
-		/****FIXME: detected UL ****/
+		/**** detected UL ****/
 		tail = atomic_load_explicit(&q->tail, acquire);
 		/****FIXME: miss ****/
 		next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
@@ -113,7 +113,7 @@ void enqueue(queue_t *q, unsigned int val)
 
 			if (get_ptr(next) == 0) { // == NULL
 				pointer value = MAKE_POINTER(node, get_count(next) + 1);
-				/****FIXME: first release UL ****/
+				/**** detected UL ****/
 				// Second release can be just relaxed
 				success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
 						&next, value, release, relaxed);
@@ -126,12 +126,12 @@ void enqueue(queue_t *q, unsigned int val)
 			}
 			if (!success) {
 				// This routine helps the other enqueue to update the tail
-				/****FIXME: detected UL ****/
+				/**** detected UL ****/
 				unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
 				pointer value = MAKE_POINTER(ptr,
 						get_count(tail) + 1);
 				/****FIXME: miss ****/
-				// Seconde release can be just relaxed
+				// Second release can be just relaxed
 				bool succ = false;
 				succ = atomic_compare_exchange_strong_explicit(&q->tail,
 						&tail, value, release, relaxed);
@@ -143,7 +143,7 @@ void enqueue(queue_t *q, unsigned int val)
 			}
 		}
 	}
-	/****FIXME: first UL ****/
+	/**** dectected UL ****/
 	// Second release can be just relaxed
 	atomic_compare_exchange_strong_explicit(&q->tail,
 			&tail,
@@ -165,7 +165,7 @@ unsigned int dequeue(queue_t *q)
 	pointer next;
 
 	while (!success) {
-		/****FIXME: detected correctness error ****/
+		/**** detected correctness error ****/
 		head = atomic_load_explicit(&q->head, acquire);
 		tail = atomic_load_explicit(&q->tail, relaxed);
 		/****FIXME: miss ****/
@@ -187,7 +187,7 @@ unsigned int dequeue(queue_t *q)
 					return 0; // NULL
 				}
 				/****FIXME: miss (not reached) ****/
-				// Seconde release can be just relaxed
+				// Second release can be just relaxed
 				bool succ = false;
 				succ = atomic_compare_exchange_strong_explicit(&q->tail,
 						&tail,