new rcu

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index 34deba7e857aca5c85c8705a80d49e98e2d0791e..44ce9862bd7cc713fd0fdbc60f9b57be7f26e416 100644 (file)
--- 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;