minor fix

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index ba8b9bde5c391a27d00d79a62ddde573c73f696f..75f470b2ee53b5c764d06cb3bb7c887b649957f0 100644 (file)
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -1,4 +1,10 @@
 #include <atomic>
 #include <atomic>

+#include <threads.h>
+#include <stdatomic.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+#include "librace.h"

 
 using namespace std;
 
 
 using namespace std;
 


@@ -7,79 +13,119 @@ using namespace std;
        read-copy-update synchronization mechanism.
 */
 
        read-copy-update synchronization mechanism.
 */
 

-// Properties to check: 
-
-
-typedef void* (*read_func_ptr_t)(void*);
-
-template <typename Type>
-class rcu {
-       /**
-               @Begin
-               @Global_define:
-                       Type *__cur_data;
+typedef struct Data {
+       int data1;
+       int data2;
+       int data3;
+} Data;

 
 

-                       static bool equals(void *ptr1, void *ptr2) {
-                               // ...
-                               // Return if the two data instances pointed to equals to each
-                               // other
+atomic<Data*> data;
+       
+/**
+       @Begin
+       @Global_define:
+               @DeclareVar:
+                       Data *_cur_data;
+               @InitVar:
+                       _cur_data = NULL;
+               
+               @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;

                        }
                        }

+               }

 
 

-               @Happens-before:
-                       Write -> Read
-                       Write -> Write
-               @End
-       */
-private:
-       atomic<Type*> _data;
-       
-       public:
+       @Happens_before:
+               Write -> Read
+               Write -> Write
+       @End
+*/
+
+/**
+       @Begin
+       @Interface: Read
+       @Commit_point_set: Read_Success_Point
+       @Action:
+               Data *_Old_Data = _cur_data;
+       @Post_check:
+               equals(__RET__, _Old_Data)
+       @End
+*/
+Data* read() {
+       Data *res = data.load(memory_order_acquire);

        /**
                @Begin
        /**
                @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
        */
                @End
        */

-       void* read() {
-               void *res = NULL;
-               Type *cur_data_ptr = _data.load(memory_order_acquire);
+       return res;
+}
+
+/**
+       @Begin
+       @Interface: Write
+       @Commit_point_set: Write_Success_Point
+       @Action:
+               _cur_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); 

                /**
                        @Begin
                /**
                        @Begin

-                       @Commit_point_check_define: true
-                       @Label: Read_Success_Point
+                       @Commit_point_define_check: succ == true
+                       @Label: Write_Success_Point

                        @End
                */
                        @End
                */

-               res = cur_data_ptr->read();
-               return res;
+               if (succ) {
+                       break;
+               }

        }
        }

+}
+
+void threadA(void *arg) {
+       Data *dataA = (Data*) malloc(sizeof(Data));
+       dataA->data1 = 3;
+       dataA->data2 = 2;
+       dataA->data3 = 1;
+       write(dataA);
+}
+
+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);
+}

 
 

+int user_main(int argc, char **argv) {

        /**
                @Begin
        /**
                @Begin

-               @Interface: Write
-               @Commit_point_set: Write_Success_Point
-               @Action:
-                       @Code:
-                       __cur_data = new_data;
+               @Entry_point

                @End
        */
                @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;
+       Data *data_init = (Data*) malloc(sizeof(Data));
+       data_init->data1 = 1;
+       data_init->data2 = 2;
+       data_init->data3 = 3;
+       write(data_init);
+
+       thrd_create(&t1, threadA, NULL);
+       thrd_create(&t2, threadB, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+
+       return 0;
+}

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 4ed57ba5c20879dff5268abdb3d53ef1d56a545a..e68c27d666f4fd29d3c4ebdf90e0ebd71df254c4 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -230,7 +230,7 @@ public class CodeGenerator {
                HashSet<String> headers = CodeVariables.getAllHeaders(_semantics);
                ArrayList<String> headerCode = new ArrayList<String>(headers.size());
                for (String header : headers) {
                HashSet<String> headers = CodeVariables.getAllHeaders(_semantics);
                ArrayList<String> headerCode = new ArrayList<String>(headers.size());
                for (String header : headers) {

-                       headerCode.add("#include " + header + ";");
+                       headerCode.add("#include " + header);

                }
                for (File file : codeAdditions.keySet()) {
                        ArrayList<CodeAddition> additions = codeAdditions.get(file);
                }
                for (File file : codeAdditions.keySet()) {
                        ArrayList<CodeAddition> additions = codeAdditions.get(file);


@@ -254,18 +254,17 @@ public class CodeGenerator {
        public static void main(String[] argvs) {
                String homeDir = Environment.HOME_DIRECTORY;
                File[] srcFiles = {
        public static void main(String[] argvs) {
                String homeDir = Environment.HOME_DIRECTORY;
                File[] srcFiles = {

-                               // new File(Environment.MODEL_CHECKER_TEST_DIR +
-                               // "/backup_linuxrwlocks.c") };

 //                              new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c")
 //                              };
                                // new File(homeDir
                                // +
                                // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
                                // };
 //                              new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c")
 //                              };
                                // new File(homeDir
                                // +
                                // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
                                // };

-                               new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
-                               new File(homeDir + "/benchmark/ms-queue/main.c"),
-                               new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
-               // new File(homeDir + "/benchmark/test/test.c") };
+//                             new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
+//                             new File(homeDir + "/benchmark/ms-queue/main.c"),
+//                             new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
+               
+                new File(homeDir + "/benchmark/read-copy-update/rcu.cc") };

                CodeGenerator gen = new CodeGenerator(srcFiles);
                gen.generateCode();
        }
                CodeGenerator gen = new CodeGenerator(srcFiles);
                gen.generateCode();
        }