From 2aaf563ff863189d7774f01dc86c19d69c12c930 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Tue, 14 Jan 2014 23:42:12 -0800 Subject: [PATCH] minor fix --- benchmark/read-copy-update/rcu.cc | 164 +++++++++++------- .../codeGenerator/CodeGenerator.java | 13 +- 2 files changed, 111 insertions(+), 66 deletions(-) diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc index ba8b9bd..75f470b 100644 --- a/benchmark/read-copy-update/rcu.cc +++ b/benchmark/read-copy-update/rcu.cc @@ -1,4 +1,10 @@ #include +#include +#include +#include +#include + +#include "librace.h" using namespace std; @@ -7,79 +13,119 @@ using namespace std; read-copy-update synchronization mechanism. */ -// Properties to check: - - -typedef void* (*read_func_ptr_t)(void*); - -template -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; + +/** + @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 _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 - @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); + 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 - @Commit_point_check_define: true - @Label: Read_Success_Point + @Commit_point_define_check: succ == true + @Label: Write_Success_Point @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 - @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; + 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 4ed57ba..e68c27d 100644 --- 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 headers = CodeVariables.getAllHeaders(_semantics); ArrayList headerCode = new ArrayList(headers.size()); for (String header : headers) { - headerCode.add("#include " + header + ";"); + headerCode.add("#include " + header); } for (File file : codeAdditions.keySet()) { ArrayList additions = codeAdditions.get(file); @@ -254,18 +254,17 @@ public class CodeGenerator { 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/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(); } -- 2.34.1