From 010b0488385988be23280784a128f5ba778e193a Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Wed, 15 Jan 2014 16:25:28 -0800 Subject: [PATCH] add deque --- benchmark/chase-lev-deque-bugfix/deque.c | 76 +++++++++++++++- benchmark/chase-lev-deque-bugfix/deque.h | 89 ++++++++++++++++++- benchmark/chase-lev-deque-bugfix/main.c | 5 ++ benchmark/ms-queue/main.c | 2 +- benchmark/ms-queue/my_queue.h | 2 +- .../codeGenerator/CodeGenerator.java | 14 +-- 6 files changed, 176 insertions(+), 12 deletions(-) diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c index 6328446..2cfbb76 100644 --- a/benchmark/chase-lev-deque-bugfix/deque.c +++ b/benchmark/chase-lev-deque-bugfix/deque.c @@ -14,21 +14,55 @@ Deque * create() { return q; } + +/** + @Begin + @Interface_define: Take + @End +*/ int take(Deque *q) { size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1; Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); atomic_store_explicit(&q->bottom, b, memory_order_relaxed); atomic_thread_fence(memory_order_seq_cst); size_t t = atomic_load_explicit(&q->top, memory_order_relaxed); + /** + @Begin + @Commit_point_define_check: t > b + @Label: Take_Point_1 + @End + */ int x; if (t <= b) { /* Non-empty queue. */ x = atomic_load_explicit(&a->buffer[b % atomic_load_explicit(&a->size,memory_order_relaxed)], memory_order_relaxed); + /** + @Begin + @Commit_point_define_check: t != b + @Label: Take_Point2 + @End + */ if (t == b) { /* Single last element in queue. */ - if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed)) + bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + + 1, memory_order_seq_cst, memory_order_relaxed); + /** + @Begin + @Commit_point_define_check: succ == true + @Label: Take_Point3 + @End + */ + + /** + @Begin + @Commit_point_define_check: succ == false + @Label: Take_Point4 + @End + */ + if (!succ) { /* Failed race. */ x = EMPTY; + } atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); } } else { /* Empty queue. */ @@ -54,6 +88,11 @@ void resize(Deque *q) { printf("resize\n"); } +/** + @Begin + @Interface_define: Push + @End +*/ void push(Deque *q, int x) { size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed); size_t t = atomic_load_explicit(&q->top, memory_order_acquire); @@ -65,21 +104,54 @@ void push(Deque *q, int x) { } atomic_store_explicit(&a->buffer[b % atomic_load_explicit(&a->size, memory_order_relaxed)], x, memory_order_relaxed); atomic_thread_fence(memory_order_release); + /** + @Begin + @Commit_point_define_check: true + @Label: Push_Point + @End + */ atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); } +/** + @Begin + @Interface_define: Steal + @End +*/ int steal(Deque *q) { size_t t = atomic_load_explicit(&q->top, memory_order_acquire); atomic_thread_fence(memory_order_seq_cst); size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire); + /** + @Begin + @Commit_point_define_check: t >= b + @Label: Steal_Point1 + @End + */ int x = EMPTY; if (t < b) { /* Non-empty queue. */ Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire); x = atomic_load_explicit(&a->buffer[t % atomic_load_explicit(&a->size, memory_order_relaxed)], memory_order_relaxed); - if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed)) + bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, + memory_order_seq_cst, memory_order_relaxed); + /** + @Begin + @Commit_point_define_check: succ == true + @Label: Steal_Point2 + @End + */ + + /** + @Begin + @Commit_point_define_check: succ == false + @Label: Steal_Point3 + @End + */ + if (!succ) { /* Failed race. */ return ABORT; + } } return x; } diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h index bc670e7..fa76d8d 100644 --- a/benchmark/chase-lev-deque-bugfix/deque.h +++ b/benchmark/chase-lev-deque-bugfix/deque.h @@ -11,12 +11,95 @@ typedef struct { atomic_uintptr_t array; /* Atomic(Array *) */ } Deque; +#define EMPTY 0xffffffff +#define ABORT 0xfffffffe + +/** + @Begin + @Options: + LANG = C; + @Global_define: + @DeclareStruct: + typedef struct tag_elem { + call_id_t id; + int data; + } tag_elem_t; + + @DeclareVar: + spec_list *__deque; + id_tag_t *tag; + @InitVar: + __deque= new_spec_list(); + tag = new_id_tag(); // Beginning of available id + @DefineFunc: + tag_elem_t* new_tag_elem(call_id_t id, int data) { + tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t)); + e->id = id; + e->data = data; + return e; + } + @DefineFunc: + call_id_t get_id(void *wrapper) { + return ((tag_elem_t*) wrapper)->id; + } + @DefineFunc: + int get_data(void *wrapper) { + return ((tag_elem_t*) wrapper)->data; + } + @Happens_before: + Push -> Steal + Push -> Take + @End +*/ + + Deque * create(); -int take(Deque *q); void resize(Deque *q); + +/** + @Begin + @Interface: Take + @Commit_point_set: Take_Point1 | Take_Point2 | Take_Point3 | Take_Point4 + @ID: size(__deque) == 0 ? DEFAULT_CALL_ID : get_id(back(__deque)) + @Action: + int _Old_Val = EMPTY; + if (size(__deque) > 0) { + _Old_Val = get_data(back(__deque)); + pop_back(__deque); + } + @Post_check: + _Old_Val == __RET__ + @End +*/ +int take(Deque *q); + +/** + @Begin + @Interface: Push + @Commit_point_set: Push_Point + @ID: get_and_inc(tag); + @Action: + tag_elem_t *elem = new_tag_elem(__ID__, x); + push_back(__deque, elem); + @End +*/ void push(Deque *q, int x); -#define EMPTY 0xffffffff -#define ABORT 0xfffffffe +/** + @Begin + @Interface: Steal + @Commit_point_set: Steal_Point1 | Steal_Point2 | Steal_Point3 + @ID: size(__deque) == 0 ? DEFAULT_CALL_ID : get_id(front(__deque)) + @Action: + int _Old_Val = EMPTY; + if (size(__deque) > 0) { + _Old_Val = get_data(front(__deque)); + pop_front(__deque); + } + @Post_check: + _Old_Val == __RET__ + @End +*/ +int steal(Deque *q); #endif diff --git a/benchmark/chase-lev-deque-bugfix/main.c b/benchmark/chase-lev-deque-bugfix/main.c index f2e8dca..481f3da 100644 --- a/benchmark/chase-lev-deque-bugfix/main.c +++ b/benchmark/chase-lev-deque-bugfix/main.c @@ -19,6 +19,11 @@ static void task(void * param) { int user_main(int argc, char **argv) { + /** + @Begin + @Entry_point + @End + */ thrd_t t; q=create(); thrd_create(&t, task, 0); diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c index 8fc3136..0346c1d 100644 --- a/benchmark/ms-queue/main.c +++ b/benchmark/ms-queue/main.c @@ -75,7 +75,7 @@ int user_main(int argc, char **argv) printf("input[%d] = %u\n", i, input[i]); for (i = 0; i < num_threads; i++) printf("output[%d] = %u\n", i, output[i]); - MODEL_ASSERT(in_sum == out_sum); + //MODEL_ASSERT(in_sum == out_sum); free(param); free(threads); diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h index ff3d42d..883a13d 100644 --- a/benchmark/ms-queue/my_queue.h +++ b/benchmark/ms-queue/my_queue.h @@ -94,7 +94,7 @@ void enqueue(queue_t *q, unsigned int val); @Begin @Interface: Dequeue @Commit_point_set: Dequeue_Success_Point | Dequeue_Empty_Point - @ID: get_id(back(__queue)) + @ID: get_id(front(__queue)) @Action: unsigned int _Old_Val = get_data(front(__queue)); pop_front(__queue); diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index 84ba735..1e22706 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -252,7 +252,6 @@ public class CodeGenerator { // Write it back to file ParserUtils.write2File(file, finalContent); } - } public static void main(String[] argvs) { @@ -264,11 +263,16 @@ public class CodeGenerator { // + // "/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/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") }; +// new File(homeDir + "/benchmark/read-copy-update/rcu.cc") }; + +// new File(homeDir + "/benchmark/chase-lev-deque-bugfix/deque.c"), +// new File(homeDir + "/benchmark/chase-lev-deque-bugfix/main.c"), +// new File(homeDir + "/benchmark/chase-lev-deque-bugfix/deque.h") }; + CodeGenerator gen = new CodeGenerator(srcFiles); gen.generateCode(); } -- 2.34.1