edits

[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 8aad9d19b56be3bfb439156f84e15ff08ec10690..2d517bcf4f06ab110e18d10479d0e2c068878038 100644 (file)
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -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"
 
 /**
@@ -14,7 +21,6 @@
 typedef struct Data {
        int data1;
        int data2;
-       int data3;
 } Data;
 
 atomic<Data*> data;
@@ -23,24 +29,56 @@ atomic<Data*> data;
        @Begin
        @Global_define:
                @DeclareVar:
-                       Data *_cur_data;
+                       IntegerList *set;
                @InitVar:
-                       _cur_data = NULL;
-               
-               @DefineFunc:
-               bool equals(Data *ptr1, Data *ptr2) {
-                       if (ptr1->data1 == ptr2->data1
-                               && ptr1->data2 == ptr2->data2
-                               && ptr1->data3 == ptr2->data3) {
+                       set = createIntegerList();
+                       Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
+                       d->data1 = 0;
+                       d->data2 = 0;
+                       push_back(set, (int64_t) d);
+               @Finalize:
+                       if (set)
+                               destroyIntegerList(set);
+                       return true;
+       @DefineFunc:
+               // This is a trick to get unique id
+               // The testcase should have a unique sum
+               call_id_t getID(int64_t d1, int64_t d2) {
+                       return d1 + d2;
+               }
+       @DefineFunc:
+               bool print(int64_t p) {
+                       Data *d = (Data*) p;
+                       model_print("Elem-> d1 = %d, d2 = %d\n", d->data1, d->data2);
+               }
+               bool equal(int64_t p1, int64_t p2) {
+                       if (!p1 || !p2)
+                               return false;
+                       Data *d1 = (Data*) p1;
+                       Data *d2 = (Data*) p2;
+                       if (d1->data1 == d2->data1 &&
+                               d1->data2 == d2->data2) {
                                return true;
                        } else {
                                return false;
                        }
                }
-
+       @DefineFunc:
+               void _write(int64_t d1, int64_t d2) {
+                       Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
+                       d->data1 = d1;
+                       d->data2 = d2;
+                       push_back(set, (int64_t) d);
+               }
+       @DefineFunc:
+               bool _read(Data *res) {
+                       bool hasElem = has_elem_by_value(set, (int64_t) res, &equal);
+                       return hasElem;
+               }
        @Happens_before:
                Write -> Read
                Write -> Write
+       @Commutativity: Write <-> Read: true
        @End
 */
 
@@ -48,14 +86,19 @@ atomic<Data*> data;
        @Begin
        @Interface: Read
        @Commit_point_set: Read_Success_Point
-       @Action:
-               Data *_Old_Data = _cur_data;
+       @ID: getID(__RET__->data1, __RET__->data2)
+       //@Action:
+               //model_print("Read_ID = %d, d1 = %d, d2 = %d\n", getID(__RET__->data1,
+               //      __RET__->data2), __RET__->data1, __RET__->data2);
+               //do_by_value(set, &print);
        @Post_check:
-               equals(__RET__, _Old_Data)
+               _read(__RET__);
        @End
 */
 Data* read() {
+       /**********    SPEC (sync)    **********/
        Data *res = data.load(memory_order_acquire);
+       //load_32(&res->data1);
        /**
                @Begin
                @Commit_point_define_check: true
@@ -69,40 +112,51 @@ Data* read() {
        @Begin
        @Interface: Write
        @Commit_point_set: Write_Success_Point
+       @ID: getID(d1, d2);
        @Action:
-               _cur_data = new_data;
+               //model_print("Write_ID = %d\n", getID(d1, d2));
+               _write(d1, d2);
        @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) {
+       bool succ = false;
+       Data *tmp = (Data*) malloc(sizeof(Data));
+       do {
+        //store_32(&tmp->data1, prev->data1 + d1);
+               /**********   Inadmissibility    **********/
+               Data *prev = data.load(memory_order_acquire);
+        tmp->data1 = d1;
+           tmp->data2 = d2;
+               /**********   Inadmissibility    **********/
+        succ = data.compare_exchange_strong(prev, tmp,
+            memory_order_release, memory_order_relaxed);
                /**
                        @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);
 }
 
 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, 2);
+}
+
+void threadC(void *arg) {
+       write(2, 2);
+}
+
+void threadD(void *arg) {
+       Data *d = read();
+       printf("ThreadD: d1=%d, d2=%d\n", d->data1, d->data2);
 }
 
 int user_main(int argc, char **argv) {
@@ -112,19 +166,21 @@ int user_main(int argc, char **argv) {
                @End
        */
        
-       thrd_t t1, t2;
-       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);
+       thrd_t t1, t2, t3, t4;
+       Data *dataInit = (Data*) malloc(sizeof(Data));
+       dataInit->data1 = 0;
+       dataInit->data2 = 0;
+       atomic_init(&data, dataInit);
 
        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;
 }