save

[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 75f470b2ee53b5c764d06cb3bb7c887b649957f0..3b495592a5f3a726d57793655af7fcd7466d7eea 100644 (file)
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -4,9 +4,14 @@
 #include <stdlib.h>
 #include <stdio.h>
 
 #include <stdlib.h>
 #include <stdio.h>
 

-#include "librace.h"
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h" 

 
 

-using namespace std;
+#include "librace.h"

 
 /**
        This is an example about how to specify the correctness of the
 
 /**
        This is an example about how to specify the correctness of the


@@ -31,13 +36,14 @@ atomic<Data*> data;
                
                @DefineFunc:
                bool equals(Data *ptr1, Data *ptr2) {
                
                @DefineFunc:
                bool equals(Data *ptr1, Data *ptr2) {

-                       if (ptr1->data1 == ptr2->data2
-                               && 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:
                }
 
        @Happens_before:


@@ -64,6 +70,7 @@ Data* read() {
                @Label: Read_Success_Point
                @End
        */
                @Label: Read_Success_Point
                @End
        */

+       //model_print("Read: %d\n", res);

        return res;
 }
 
        return res;
 }
 


@@ -76,20 +83,19 @@ Data* read() {
        @End
 */
 void write(Data *new_data) {
        @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 *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
                /**
                        @Begin

-                       @Commit_point_define_check: succ == true
+                       @Commit_point_define_check: succ

                        @Label: Write_Success_Point
                        @End
                */
                        @Label: Write_Success_Point
                        @End
                */

-               if (succ) {
-                       break;
-               }
-       }
+       } while (!succ);
+       //model_print("Write: %d\n", new_data);

 }
 
 void threadA(void *arg) {
 }
 
 void threadA(void *arg) {


@@ -107,6 +113,21 @@ void threadB(void *arg) {
        printf("ThreadB data3: %d\n", dataB->data3);
 }
 
        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
 int user_main(int argc, char **argv) {
        /**
                @Begin


@@ -114,18 +135,23 @@ int user_main(int argc, char **argv) {
                @End
        */
        
                @End
        */
        

-       thrd_t t1, t2;
+       thrd_t t1, t2, t3, t4;
+       data.store(NULL, memory_order_relaxed);

        Data *data_init = (Data*) malloc(sizeof(Data));
        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);
        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(t1);
        thrd_join(t2);

+       thrd_join(t3);
+       thrd_join(t4);

 
        return 0;
 }
 
        return 0;
 }