save
[cdsspec-compiler.git] / benchmark / read-copy-update / rcu.cc
index ebe36a9..cc512d6 100644 (file)
@@ -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,19 @@ 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;
+               }
+
+               bool isOriginalRead(Data *ptr) {
+                       return ptr->data1 == 0 &&
+                               ptr->data2 == 0 && ptr->data3 == 0;
                }
 
        @Happens_before:
@@ -48,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() {
@@ -62,6 +76,7 @@ Data* read() {
                @Label: Read_Success_Point
                @End
        */
+       //model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
        return res;
 }
 
@@ -70,54 +85,55 @@ 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) {
-       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) {
+       Data *prev = data.load(memory_order_acquire);
+       bool succ = false;
+       Data *tmp = (Data*) malloc(sizeof(Data));
+       do {
+        tmp->data1 = prev->data1 + d1;
+           tmp->data2 = prev->data2 + d2;
+           tmp->data3 = prev->data3 + d3;
+        succ = data.compare_exchange_strong(prev, tmp,
+            memory_order_acq_rel, 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 +144,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);