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

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index 449463f..6f79126 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"
 
 /**
@@ -29,13 +36,14 @@ atomic<Data*> data;
 		
 		@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;
-			}
+			//if (ptr1->data1 == ptr2->data1
+			//	&& ptr1->data2 == ptr2->data2
+			//	&& ptr1->data3 == ptr2->data3) {
+			//	return true;
+			//} else {
+			//	return false;
+			//}
+			return ptr1 == ptr2;
 		}
 
 	@Happens_before:
@@ -62,6 +70,7 @@ Data* read() {
 		@Label: Read_Success_Point
 		@End
 	*/
+	//model_print("Read: %d\n", res);
 	return res;
 }
 
@@ -74,20 +83,19 @@ Data* read() {
 	@End
 */
 void write(Data *new_data) {
-	while (true) {
-		Data *prev = data.load(memory_order_relaxed);
-		bool succ = data.compare_exchange_strong(prev, new_data,
+	Data *prev = data.load(memory_order_relaxed);
+	bool succ = false;
+	do {
+		succ = data.compare_exchange_strong(prev, new_data,
 			memory_order_release, memory_order_relaxed); 
 		/**
 			@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\n", new_data);
 }
 
 void threadA(void *arg) {
@@ -130,20 +138,20 @@ 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;
+	data_init->data1 = 0;
+	data_init->data2 = 0;
+	data_init->data3 = 0;
 	write(data_init);
 
 	thrd_create(&t1, threadA, NULL);
 	thrd_create(&t2, threadB, NULL);
-	//thrd_create(&t3, threadC, NULL);
-	//thrd_create(&t4, threadD, NULL);
+	thrd_create(&t3, threadC, NULL);
+	thrd_create(&t4, threadD, NULL);
 
 	thrd_join(t1);
 	thrd_join(t2);
-	//thrd_join(t3);
-	//thrd_join(t4);
+	thrd_join(t3);
+	thrd_join(t4);
 
 	return 0;
 }