X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=benchmark%2Fread-copy-update%2Frcu.cc;h=3b495592a5f3a726d57793655af7fcd7466d7eea;hp=ba8b9bde5c391a27d00d79a62ddde573c73f696f;hb=f4f705b64671cdfae4d4cf8997e64a81ddce201d;hpb=0a040a5b619952d29338f73db8f685d7367178fc

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index ba8b9bd..3b49559 100644
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -1,85 +1,157 @@
 #include <atomic>
+#include <threads.h>
+#include <stdatomic.h>
+#include <stdlib.h>
+#include <stdio.h>
 
-using namespace std;
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h" 
+
+#include "librace.h"
 
 /**
 	This is an example about how to specify the correctness of the
 	read-copy-update synchronization mechanism.
 */
 
-// Properties to check: 
+typedef struct Data {
+	int data1;
+	int data2;
+	int data3;
+} Data;
 
+atomic<Data*> data;
+	
+/**
+	@Begin
+	@Global_define:
+		@DeclareVar:
+			Data *_cur_data;
+		@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;
+		}
 
-typedef void* (*read_func_ptr_t)(void*);
+	@Happens_before:
+		Write -> Read
+		Write -> Write
+	@End
+*/
 
-template <typename Type>
-class rcu {
-	/**
-		@Begin
-		@Global_define:
-			Type *__cur_data;
-
-			static bool equals(void *ptr1, void *ptr2) {
-				// ...
-				// Return if the two data instances pointed to equals to each
-				// other
-			}
-
-		@Happens-before:
-			Write -> Read
-			Write -> Write
-		@End
-	*/
-private:
-	atomic<Type*> _data;
-	
-	public:
+/**
+	@Begin
+	@Interface: Read
+	@Commit_point_set: Read_Success_Point
+	@Action:
+		Data *_Old_Data = _cur_data;
+	@Post_check:
+		equals(__RET__, _Old_Data)
+	@End
+*/
+Data* read() {
+	Data *res = data.load(memory_order_acquire);
 	/**
 		@Begin
-		@Interface: Read
-		@Commit_point_set: Read_Success_Point
-		@Action:
-			@Code:
-			void *_Old_Data = __cur_data;
-		@Post_check:
-			equals(__RET__, _Old_Data->read())
+		@Commit_point_define_check: true
+		@Label: Read_Success_Point
 		@End
 	*/
-	void* read() {
-		void *res = NULL;
-		Type *cur_data_ptr = _data.load(memory_order_acquire);
+	//model_print("Read: %d\n", res);
+	return res;
+}
+
+/**
+	@Begin
+	@Interface: Write
+	@Commit_point_set: Write_Success_Point
+	@Action:
+		_cur_data = new_data;
+	@End
+*/
+void write(Data *new_data) {
+	Data *prev = data.load(memory_order_relaxed);
+	bool succ = false;
+	do {
+		succ = data.compare_exchange_strong(prev, new_data,
+			memory_order_acq_rel, memory_order_relaxed); 
 		/**
 			@Begin
-			@Commit_point_check_define: true
-			@Label: Read_Success_Point
+			@Commit_point_define_check: succ
+			@Label: Write_Success_Point
 			@End
 		*/
-		res = cur_data_ptr->read();
-		return res;
-	}
+	} 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);
+}
+
+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);
+}
+
+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);
+}
 
+void threadD(void *arg) {
+	Data *dataD = (Data*) malloc(sizeof(Data));
+	dataD->data1 = -3;
+	dataD->data2 = -2;
+	dataD->data3 = -1;
+	write(dataD);
+}
+
+int user_main(int argc, char **argv) {
 	/**
 		@Begin
-		@Interface: Write
-		@Commit_point_set: Write_Success_Point
-		@Action:
-			@Code:
-			__cur_data = new_data;
+		@Entry_point
 		@End
 	*/
-	void write(Type *new_data) {
-		while (true) {
-			Type *prev = _data.load(memory_order_acquire);
-			if (_data.compare_exchange_weak(prev, new_data,
-				memory_order_release, memory_order_release)) {
-				/**
-					@Begin
-					@Commit_point_check_define: __ATOMIC_RET__ == true
-					@Label: Write_Success_Point
-					@End
-				*/
-				break;
-			}
-		}
-	}
-};
+	
+	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);
+
+	thrd_create(&t1, threadA, NULL);
+	thrd_create(&t2, threadB, NULL);
+	thrd_create(&t3, threadC, NULL);
+	thrd_create(&t4, threadD, NULL);
+
+	thrd_join(t1);
+	thrd_join(t2);
+	thrd_join(t3);
+	thrd_join(t4);
+
+	return 0;
+}