From: Peizhao Ou <peizhaoo@uci.edu>
Date: Thu, 20 Mar 2014 22:07:24 +0000 (-0700)
Subject: new rcu
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=9040aa1fca8869bcf9aad4ab3f014aa4de7bfa35

new rcu
---

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index 34deba7..44ce986 100644
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -46,9 +46,14 @@ atomic<Data*> data;
 			return ptr1 == ptr2;
 		}
 
+		bool isOriginalRead(Data *ptr) {
+			return ptr->data1 == 0 &&
+				ptr->data2 == 0 && ptr->data3 == 0;
+		}
+
 	@Happens_before:
 		Write -> Read
-		Write -> Write
+		//Write -> Write
 	@End
 */
 
@@ -56,10 +61,11 @@ atomic<Data*> data;
 	@Begin
 	@Interface: Read
 	@Commit_point_set: Read_Success_Point
+	//@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
 	@Action:
 		Data *_Old_Data = _cur_data;
 	@Post_check:
-		equals(__RET__, _Old_Data)
+		_Old_Data = __RET__
 	@End
 */
 Data* read() {
@@ -70,7 +76,7 @@ Data* read() {
 		@Label: Read_Success_Point
 		@End
 	*/
-	//model_print("Read: %d\n", res);
+	//model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
 	return res;
 }
 
@@ -79,15 +85,29 @@ Data* read() {
 	@Interface: Write
 	@Commit_point_set: Write_Success_Point
 	@Action:
-		_cur_data = new_data;
+		Data *_Old_data = _cur_data;
+		_cur_data = __RET__;
+	@Post_check:
+		_Old_data == NULL ?
+			(__RET__->data1 == d1	&&
+			__RET__->data2 == d2	&&
+			__RET__->data3 == d3)
+			:
+			(__RET__->data1 == _Old_data->data1 + d1 &&
+			__RET__->data2 == _Old_data->data2 + d2	&&
+			__RET__->data3 == _Old_data->data3 + d3)
 	@End
 */
-void write(Data *new_data) {
-	Data *prev = data.load(memory_order_relaxed);
+Data* write(int d1, int d2, int d3) {
+	Data *prev = data.load(memory_order_acquire);
 	bool succ = false;
+	Data *tmp = (Data*) malloc(sizeof(Data));
 	do {
-		succ = data.compare_exchange_strong(prev, new_data,
-			memory_order_acq_rel, memory_order_relaxed); 
+        tmp->data1 = prev->data1 + d1;
+	    tmp->data2 = prev->data2 + d2;
+	    tmp->data3 = prev->data3 + d3;
+        succ = data.compare_exchange_strong(prev, tmp,
+            memory_order_release, memory_order_acquire);
 		/**
 			@Begin
 			@Commit_point_define_check: succ
@@ -95,52 +115,25 @@ void write(Data *new_data) {
 			@End
 		*/
 	} while (!succ);
-	//model_print("Write: %d\n", new_data);
+	//model_print("Write: %d, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
+	return tmp;
 }
 
-/*
-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;
-	dataA->data2 = 2;
-	dataA->data3 = 1;
-	write(dataA);
+	write(1, 0, 0);
 }
 
 void threadB(void *arg) {
-	Data *dataB = read();
-	printf("ThreadB data1: %d\n", dataB->data1);
-	printf("ThreadB data2: %d\n", dataB->data2);
-	printf("ThreadB data3: %d\n", dataB->data3);
+	write(0, 1, 0);
 }
 
 void threadC(void *arg) {
-	Data *dataC = read();
-	printf("ThreadC data1: %d\n", dataC->data1);
-	printf("ThreadC data2: %d\n", dataC->data2);
-	printf("ThreadC data3: %d\n", dataC->data3);
+	write(0, 0, 1);
 }
 
 void threadD(void *arg) {
-	Data *dataD = (Data*) malloc(sizeof(Data));
-	dataD->data1 = -3;
-	dataD->data2 = -2;
-	dataD->data3 = -1;
-	write(dataD);
+	Data *dataC = read();
 }
 
 int user_main(int argc, char **argv) {
@@ -151,21 +144,21 @@ int user_main(int argc, char **argv) {
 	*/
 	
 	thrd_t t1, t2, t3, t4;
-	data.store(NULL, memory_order_relaxed);
-	Data *data_init = (Data*) malloc(sizeof(Data));
-	data_init->data1 = 0;
-	data_init->data2 = 0;
-	data_init->data3 = 0;
-	write(data_init);
+	Data *dataInit = (Data*) malloc(sizeof(Data));
+	dataInit->data1 = 0;
+	dataInit->data2 = 0;
+	dataInit->data3 = 0;
+	atomic_init(&data, dataInit);
+	//write(0, 0, 0);
 
 	thrd_create(&t1, threadA, NULL);
 	thrd_create(&t2, threadB, NULL);
-	thrd_create(&t3, threadC, NULL);
+	//thrd_create(&t3, threadC, NULL);
 	thrd_create(&t4, threadD, NULL);
 
 	thrd_join(t1);
 	thrd_join(t2);
-	thrd_join(t3);
+	//thrd_join(t3);
 	thrd_join(t4);
 
 	return 0;