X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=benchmark%2Fread-copy-update%2Frcu.cc;h=55238821356416a592399795ebc4d98a0ae6fabd;hb=7f2fd73fe54a04e0f795e7b8f6e28b3a7708df03;hp=449463f16716f17f5927138bf109d38231a7d97f;hpb=fbe8969c916f7532c5d0aebee40ae96854496f3d;p=cdsspec-compiler.git

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index 449463f..5523882 100644
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -4,6 +4,13 @@
 #include <stdlib.h>
 #include <stdio.h>
 
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h" 
+
 #include "librace.h"
 
 /**
@@ -23,21 +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;
-			}
-		}
-
+			data1 = 0;
+			data2 = 0;
+			data3 = 0;
 	@Happens_before:
 		Write -> Read
 		Write -> Write
@@ -48,20 +47,23 @@ atomic<Data*> data;
 	@Begin
 	@Interface: Read
 	@Commit_point_set: Read_Success_Point
-	@Action:
-		Data *_Old_Data = _cur_data;
+	//@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
 	@Post_check:
-		equals(__RET__, _Old_Data)
+		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
 		@Label: Read_Success_Point
 		@End
 	*/
+	//model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
 	return res;
 }
 
@@ -70,54 +72,48 @@ Data* read() {
 	@Interface: Write
 	@Commit_point_set: Write_Success_Point
 	@Action:
-		_cur_data = new_data;
+		data1 += d1;
+		data2 += d2;
+		data3 += d3;
 	@End
 */
-void write(Data *new_data) {
-	while (true) {
-		Data *prev = data.load(memory_order_relaxed);
-		bool succ = data.compare_exchange_strong(prev, new_data,
-			memory_order_release, memory_order_relaxed); 
+Data* write(int d1, int d2, int d3) {
+	bool succ = false;
+	Data *tmp = (Data*) malloc(sizeof(Data));
+	Data *prev = data.load(memory_order_acquire);
+	do {
+        //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,
+            memory_order_release, memory_order_acquire);
 		/**
 			@Begin
-			@Commit_point_define_check: succ == true
+			@Commit_point_define_check: succ
 			@Label: Write_Success_Point
 			@End
 		*/
-		if (succ) {
-			break;
-		}
-	}
+	} while (!succ);
+	//model_print("Write: %d, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
+	return tmp;
 }
 
+
 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) {
@@ -128,12 +124,12 @@ 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 = 1;
-	data_init->data2 = 2;
-	data_init->data3 = 3;
-	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);