changes with lines of spec counted

[cdsspec-compiler.git] / benchmark / read-copy-update / rcu.cc

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index 3b495592a5f3a726d57793655af7fcd7466d7eea..55238821356416a592399795ebc4d98a0ae6fabd 100644 (file)
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -30,22 +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;
-                       //}
-                       return ptr1 == ptr2;
-               }
-
+                       data1 = 0;
+                       data2 = 0;
+                       data3 = 0;
        @Happens_before:
                Write -> Read
                Write -> Write
@@ -56,21 +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\n", res);
+       //model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
        return res;
 }
 
@@ -79,15 +72,22 @@ 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) {
-       Data *prev = data.load(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 {
-               succ = data.compare_exchange_strong(prev, new_data,
-                       memory_order_acq_rel, memory_order_relaxed); 
+        //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
@@ -95,37 +95,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;
 }
 
+
 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) {
@@ -136,22 +124,22 @@ 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(&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;
 }