changes with lines of spec counted
[cdsspec-compiler.git] / benchmark / read-copy-update / rcu.cc
index 44ce9862bd7cc713fd0fdbc60f9b57be7f26e416..55238821356416a592399795ebc4d98a0ae6fabd 100644 (file)
@@ -30,30 +30,16 @@ 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;
-               }
-
-               bool isOriginalRead(Data *ptr) {
-                       return ptr->data1 == 0 &&
-                               ptr->data2 == 0 && ptr->data3 == 0;
-               }
-
+                       data1 = 0;
+                       data2 = 0;
+                       data3 = 0;
        @Happens_before:
                Write -> Read
-               //Write -> Write
+               Write -> Write
        @End
 */
 
@@ -62,14 +48,15 @@ atomic<Data*> data;
        @Interface: Read
        @Commit_point_set: Read_Success_Point
        //@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
-       @Action:
-               Data *_Old_Data = _cur_data;
        @Post_check:
-               _Old_Data = __RET__
+               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
@@ -85,24 +72,17 @@ Data* read() {
        @Interface: Write
        @Commit_point_set: Write_Success_Point
        @Action:
-               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)
+               data1 += d1;
+               data2 += d2;
+               data3 += d3;
        @End
 */
 Data* write(int d1, int d2, int d3) {
-       Data *prev = data.load(memory_order_acquire);
        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;
@@ -149,17 +129,17 @@ int user_main(int argc, char **argv) {
        dataInit->data2 = 0;
        dataInit->data3 = 0;
        atomic_init(&data, dataInit);
-       //write(0, 0, 0);
+       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(&t4, threadD, NULL);
 
        thrd_join(t1);
        thrd_join(t2);
        //thrd_join(t3);
-       thrd_join(t4);
+       //thrd_join(t4);
 
        return 0;
 }