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 ba8b9bde5c391a27d00d79a62ddde573c73f696f..55238821356416a592399795ebc4d98a0ae6fabd 100644 (file)
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -1,85 +1,145 @@
 #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 void* (*read_func_ptr_t)(void*);
+typedef struct Data {
+       int data1;
+       int data2;
+       int data3;
+} Data;
 
-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;
+atomic<Data*> data;
        
-       public:
+/**
+       @Begin
+       @Global_define:
+               @DeclareVar:
+                       int data1;
+                       int data2;
+                       int data3;
+               @InitVar:
+                       data1 = 0;
+                       data2 = 0;
+                       data3 = 0;
+       @Happens_before:
+               Write -> Read
+               Write -> Write
+       @End
+*/
+
+/**
+       @Begin
+       @Interface: Read
+       @Commit_point_set: Read_Success_Point
+       //@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
+       @Post_check:
+               data1 == __RET__->data1 &&
+               data2 == __RET__->data2 &&
+               data3 == __RET__->data3
+       @End
+*/
+Data* read() {
+       Data *res = data.load(memory_order_acquire);
+       //load_32(&res->data1);
        /**
                @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, %d, %d\n", res->data1, res->data2, res->data3);
+       return res;
+}
+
+/**
+       @Begin
+       @Interface: Write
+       @Commit_point_set: Write_Success_Point
+       @Action:
+               data1 += d1;
+               data2 += d2;
+               data3 += d3;
+       @End
+*/
+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 {
+        //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_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, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
+       return tmp;
+}
+
+
+void threadA(void *arg) {
+       write(1, 0, 0);
+}
+
+void threadB(void *arg) {
+       write(0, 1, 0);
+}
 
+void threadC(void *arg) {
+       write(0, 0, 1);
+}
+
+void threadD(void *arg) {
+       Data *dataC = read();
+}
+
+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 *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_join(t1);
+       thrd_join(t2);
+       //thrd_join(t3);
+       //thrd_join(t4);
+
+       return 0;
+}