From: Peizhao Ou <peizhaoo@uci.edu>
Date: Sun, 23 Mar 2014 21:59:17 +0000 (-0700)
Subject: fix rcu spec
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=fefe267c3a874b46fb9621748f3c6dfa239963b3

fix rcu spec
---

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index cc512d6..3d6792f 100644
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -30,27 +30,13 @@ atomic<Data*> data;
 	@Begin
 	@Global_define:
 		@DeclareVar:
-			Data *_cur_data;
+			int data1;
+			int data2;
+			int data3;
 		@InitVar:
-			_cur_data = NULL;
-		
-		@DefineFunc:
-		bool equals(Data *ptr1, Data *ptr2) {
-			//if (ptr1->data1 == ptr2->data1
-			//	&& ptr1->data2 == ptr2->data2
-			//	&& ptr1->data3 == ptr2->data3) {
-			//	return true;
-			//} else {
-			//	return false;
-			//}
-			return ptr1 == ptr2;
-		}
-
-		bool isOriginalRead(Data *ptr) {
-			return ptr->data1 == 0 &&
-				ptr->data2 == 0 && ptr->data3 == 0;
-		}
-
+			data1 = 0;
+			data2 = 0;
+			data3 = 0;
 	@Happens_before:
 		Write -> Read
 		Write -> Write
@@ -62,14 +48,15 @@ atomic<Data*> data;
 	@Interface: Read
 	@Commit_point_set: Read_Success_Point
 	//@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
-	@Action:
-		Data *_Old_Data = _cur_data;
 	@Post_check:
-		_Old_Data = __RET__
+		data1 == __RET__->data1 &&
+		data2 == __RET__->data2 &&
+		data3 == __RET__->data3
 	@End
 */
 Data* read() {
 	Data *res = data.load(memory_order_acquire);
+	load_32(&res->data1);
 	/**
 		@Begin
 		@Commit_point_define_check: true
@@ -85,17 +72,9 @@ Data* read() {
 	@Interface: Write
 	@Commit_point_set: Write_Success_Point
 	@Action:
-		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)
+		data1 += d1;
+		data2 += d2;
+		data3 += d3;
 	@End
 */
 Data* write(int d1, int d2, int d3) {
@@ -103,7 +82,8 @@ Data* write(int d1, int d2, int d3) {
 	bool succ = false;
 	Data *tmp = (Data*) malloc(sizeof(Data));
 	do {
-        tmp->data1 = prev->data1 + d1;
+        store_32(&tmp->data1, prev->data1 + d1);
+        //tmp->data1 = prev->data1 + d1;
 	    tmp->data2 = prev->data2 + d2;
 	    tmp->data3 = prev->data3 + d3;
         succ = data.compare_exchange_strong(prev, tmp,
@@ -153,12 +133,12 @@ int user_main(int argc, char **argv) {
 
 	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;