From: Peizhao Ou <peizhaoo@uci.edu>
Date: Wed, 19 Mar 2014 15:40:56 +0000 (-0700)
Subject: save
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=7a77931bb0107ba11c874485309c9f38f5bec967

save
---

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index 2cfbb76..b556460 100644
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -35,7 +35,11 @@ int take(Deque *q) {
 	int x;
 	if (t <= b) {
 		/* Non-empty queue. */
-		x = atomic_load_explicit(&a->buffer[b % atomic_load_explicit(&a->size,memory_order_relaxed)], memory_order_relaxed);
+		int size = atomic_load_explicit(&a->size, memory_order_relaxed);
+		if (size == 0) 
+			model_print("take: size == 0\n");
+		// TODO: size can be zero here!!
+		x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
 		/**
 			@Begin
 			@Commit_point_define_check: t != b
@@ -82,6 +86,10 @@ void resize(Deque *q) {
 	atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed);
 	size_t i;
 	for(i=top; i < bottom; i++) {
+		if (new_size == 0)
+			model_print("resize: new_size == 0\n");
+		if (size == 0)
+			model_print("resize: size == 0\n");
 		atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
 	}
 	atomic_store_explicit(&q->array, new_a, memory_order_release);
@@ -102,7 +110,10 @@ void push(Deque *q, int x) {
 		//Bug in paper...should have next line...
 		a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
 	}
-	atomic_store_explicit(&a->buffer[b % atomic_load_explicit(&a->size, memory_order_relaxed)], x, memory_order_relaxed);
+	int size = atomic_load_explicit(&a->size, memory_order_relaxed);
+	if (size == 0) 
+		model_print("push: size == 0\n");
+	atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
 	atomic_thread_fence(memory_order_release);
 	/**
 		@Begin
@@ -132,7 +143,10 @@ int steal(Deque *q) {
 	if (t < b) {
 		/* Non-empty queue. */
 		Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
-		x = atomic_load_explicit(&a->buffer[t % atomic_load_explicit(&a->size, memory_order_relaxed)], memory_order_relaxed);
+		int size = atomic_load_explicit(&a->size, memory_order_relaxed);
+		if (size == 0) 
+			model_print("steal: size == 0\n");
+		x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
 		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 8ddcdb6..b046cc7 100644
--- a/benchmark/chase-lev-deque-bugfix/deque.h
+++ b/benchmark/chase-lev-deque-bugfix/deque.h
@@ -5,6 +5,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h"
 
 typedef struct {
 	atomic_size_t size;
diff --git a/benchmark/chase-lev-deque-bugfix/main.c b/benchmark/chase-lev-deque-bugfix/main.c
index 481f3da..a67be6e 100644
--- a/benchmark/chase-lev-deque-bugfix/main.c
+++ b/benchmark/chase-lev-deque-bugfix/main.c
@@ -13,10 +13,14 @@ int a;
 int b;
 int c;
 
-static void task(void * param) {
+static void task1(void * param) {
 	a=steal(q);
 }
 
+static void task2(void * param) {
+	a=take(q);
+}
+
 int user_main(int argc, char **argv)
 {
 	/**
@@ -24,15 +28,17 @@ int user_main(int argc, char **argv)
 		@Entry_point
 		@End
 	*/
-	thrd_t t;
+	thrd_t t1, t2;
 	q=create();
-	thrd_create(&t, task, 0);
 	push(q, 1);
 	push(q, 2);
+	thrd_create(&t1, task1, 0);
+	thrd_create(&t2, task2, 0);
 	push(q, 4);
 	b=take(q);
 	c=take(q);
-	thrd_join(t);
+	thrd_join(t1);
+	thrd_join(t2);
 
 	bool correct=true;
 	if (a!=1 && a!=2 && a!=4 && a!= EMPTY)
@@ -45,7 +51,7 @@ int user_main(int argc, char **argv)
 		correct=false;
 	if (!correct)
 		printf("a=%d b=%d c=%d\n",a,b,c);
-	MODEL_ASSERT(correct);
+	//MODEL_ASSERT(correct);
 
 	return 0;
 }
diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h
index c3cea0d..536f1c4 100644
--- a/benchmark/cliffc-hashtable/cliffc_hashtable.h
+++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h
@@ -16,6 +16,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h" 
 
 using namespace std;
 
diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index eaae816..6341c4c 100644
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -7,6 +7,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h"
 
 #include "librace.h"
 
diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h
index 27ce180..e08a0e7 100644
--- a/benchmark/mcs-lock/mcs-lock.h
+++ b/benchmark/mcs-lock/mcs-lock.h
@@ -8,6 +8,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h" 
 
 struct mcs_node {
 	std::atomic<mcs_node *> next;
@@ -34,7 +35,7 @@ public:
 		m_tail.store( NULL );
 	}
 	~mcs_mutex() {
-		ASSERT( m_tail.load() == NULL );
+		//ASSERT( m_tail.load() == NULL );
 	}
 
 	// Each thread will have their own guard.
diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h
index d78ff6c..cd9d430 100644
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -7,6 +7,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h" 
 
 /**
 	@Begin
diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index 0346c1d..200ae45 100644
--- a/benchmark/ms-queue/main.c
+++ b/benchmark/ms-queue/main.c
@@ -19,7 +19,7 @@ int get_thread_num()
 	for (i = 0; i < num_threads; i++)
 		if (curr.priv == threads[i].priv)
 			return i;
-	MODEL_ASSERT(0);
+	//MODEL_ASSERT(0);
 	return -1;
 }
 
diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index 9ef2d63..0d83392 100644
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -8,6 +8,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h" 
 
 #define MAX_NODES			0xf
 
diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index 3b49559..34deba7 100644
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -98,6 +98,21 @@ void write(Data *new_data) {
 	//model_print("Write: %d\n", new_data);
 }
 
+/*
+Data *prev = data.load(memory_order_acquire);
+bool succ = false;
+Data *tmp = malloc(sizeof(Data));
+do {
+        tmp->data1=prev->data1+new_data->data1;
+        tmp->data2=prev->data2+new_data->data2;
+        tmp->data3=prev->data3+new_data->data3;
+        succ = data.compare_exchange_strong(prev, tmp,
+                           memory_order_release, memory_order_acquire);
+           } while (!succ);
+           //model_print("Write: %d\n", new_data);
+}
+*/
+
 void threadA(void *arg) {
 	Data *dataA = (Data*) malloc(sizeof(Data));
 	dataA->data1 = 3;
diff --git a/benchmark/spsc-bugfix/queue.h b/benchmark/spsc-bugfix/queue.h
index 76c5200..b47452e 100644
--- a/benchmark/spsc-bugfix/queue.h
+++ b/benchmark/spsc-bugfix/queue.h
@@ -9,6 +9,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h" 
 
 #include "eventcount.h"
 
diff --git a/benchmark/spsc-bugfix/spsc-queue.cc b/benchmark/spsc-bugfix/spsc-queue.cc
index f8528a8..e3a4a6d 100644
--- a/benchmark/spsc-bugfix/spsc-queue.cc
+++ b/benchmark/spsc-bugfix/spsc-queue.cc
@@ -13,7 +13,7 @@ spsc_queue<int> *q;
 		else
 		{
 			int d = q->dequeue();
-			RL_ASSERT(11 == d);
+			//RL_ASSERT(11 == d);
 		}
 	}