fixed command line

[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
deleted file mode 100644 (file)
index 2d517bc..0000000
--- a/benchmark/read-copy-update/rcu.cc
+++ /dev/null
@@ -1,186 +0,0 @@
-#include <atomic>
-#include <threads.h>
-#include <stdatomic.h>
-#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"
-
-/**
-       This is an example about how to specify the correctness of the
-       read-copy-update synchronization mechanism.
-*/
-
-typedef struct Data {
-       int data1;
-       int data2;
-} Data;
-
-atomic<Data*> data;
-       
-/**
-       @Begin
-       @Global_define:
-               @DeclareVar:
-                       IntegerList *set;
-               @InitVar:
-                       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
-*/
-
-/**
-       @Begin
-       @Interface: Read
-       @Commit_point_set: Read_Success_Point
-       @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:
-               _read(__RET__);
-       @End
-*/
-Data* read() {
-       /**********    SPEC (sync)    **********/
-       Data *res = data.load(memory_order_acquire);
-       //load_32(&res->data1);
-       /**
-               @Begin
-               @Commit_point_define_check: true
-               @Label: Read_Success_Point
-               @End
-       */
-       return res;
-}
-
-/**
-       @Begin
-       @Interface: Write
-       @Commit_point_set: Write_Success_Point
-       @ID: getID(d1, d2);
-       @Action:
-               //model_print("Write_ID = %d\n", getID(d1, d2));
-               _write(d1, d2);
-       @End
-*/
-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
-                       @Label: Write_Success_Point
-                       @End
-               */
-       } while (!succ);
-       //model_print("Write: %d, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
-       return tmp;
-}
-
-
-void threadA(void *arg) {
-       write(1, 0);
-}
-
-void threadB(void *arg) {
-       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) {
-       /**
-               @Begin
-               @Entry_point
-               @End
-       */
-       
-       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;
-}