From a155ac407f80a2b302aba2c2a2a4eb83f220236c Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Tue, 17 Nov 2015 19:04:15 -0800 Subject: [PATCH] edits --- benchmark/chase-lev-deque-bugfix/Makefile | 8 +- benchmark/chase-lev-deque-bugfix/deque.c | 22 +++-- benchmark/chase-lev-deque-bugfix/deque.h | 88 +++++++------------- benchmark/chase-lev-deque-bugfix/testcase1.c | 78 +++++++++++++++++ benchmark/chase-lev-deque-bugfix/testcase2.c | 82 ++++++++++++++++++ 5 files changed, 207 insertions(+), 71 deletions(-) create mode 100644 benchmark/chase-lev-deque-bugfix/testcase1.c create mode 100644 benchmark/chase-lev-deque-bugfix/testcase2.c diff --git a/benchmark/chase-lev-deque-bugfix/Makefile b/benchmark/chase-lev-deque-bugfix/Makefile index 91ff999..3980f68 100644 --- a/benchmark/chase-lev-deque-bugfix/Makefile +++ b/benchmark/chase-lev-deque-bugfix/Makefile @@ -1,14 +1,14 @@ include ../benchmarks.mk -TESTNAME = main +TESTNAME = main testcase1 testcase2 HEADERS = deque.h -OBJECTS = main.o deque.o +OBJECTS = deque.o all: $(TESTNAME) -$(TESTNAME): $(HEADERS) $(OBJECTS) - $(CC) -o $@ $(OBJECTS) $(CPPFLAGS) $(LDFLAGS) +$(TESTNAME): % : %.c $(OBJECTS) + $(CC) -o $@ $^ $(CPPFLAGS) $(LDFLAGS) %.o: %.c $(CC) -c -o $@ $< $(CPPFLAGS) diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c index 854091f..010704c 100644 --- a/benchmark/chase-lev-deque-bugfix/deque.c +++ b/benchmark/chase-lev-deque-bugfix/deque.c @@ -36,7 +36,7 @@ int take(Deque *q) { @End */ atomic_store_explicit(&q->bottom, b, memory_order_relaxed); - /**** detected correctness ****/ + /**** SPEC (sequential) (testcase1.c) ****/ atomic_thread_fence(memory_order_seq_cst); size_t t = atomic_load_explicit(&q->top, memory_order_relaxed); /** @@ -111,13 +111,14 @@ void resize(Deque *q) { */ void push(Deque *q, int x) { size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed); - /**** detected correctness ****/ + /**** SPEC (sequential) ****/ size_t t = atomic_load_explicit(&q->top, memory_order_acquire); Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ { resize(q); + // CDSSpec can actually detect the same bug if we avoid the UL error //Bug in paper...should have next line... - a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); + //a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); /** //@Begin @Commit_point_define_check: true @@ -134,16 +135,18 @@ void push(Deque *q, int x) { @Label: Push_Update_Buffer @End */ - /**** detected HB error (run with -u100 to avoid the uninitialized bug) ****/ + /**** SPEC (Sync) (run with -u100 to avoid the uninitialized bug) ****/ atomic_thread_fence(memory_order_release); - - atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); + // Watch out!!! We need to specifiy the fence as the commit point because + // the synchronization in C11 actually is established at the fence. /** @Begin @Commit_point_define_check: true @Label: Push_Update_Bottom @End */ + atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); + } /** @@ -152,7 +155,8 @@ void push(Deque *q, int x) { @End */ int steal(Deque *q) { - //FIXME: weaken the following acquire causes no spec problem + //Watch out: actually on need to be an acquire (don't count it) + // An old bug size_t t = atomic_load_explicit(&q->top, memory_order_acquire); /** //@Begin @@ -162,7 +166,7 @@ int steal(Deque *q) { */ //FIXME: remove the fence causes no error and fewer executions.. atomic_thread_fence(memory_order_seq_cst); - /**** detected HB error (run with -u100 to avoid the uninitialized bug) ****/ + /**** SPEC & UL ****/ size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire); /** @Begin @@ -197,7 +201,7 @@ int steal(Deque *q) { @Label: Steal_Potential_Read_Buffer @End */ - /**** detected correctness failure ****/ + /**** SPEC (sequential) ****/ bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed); /** diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h index 837df89..82560f1 100644 --- a/benchmark/chase-lev-deque-bugfix/deque.h +++ b/benchmark/chase-lev-deque-bugfix/deque.h @@ -26,52 +26,23 @@ typedef struct { @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; + IntegerList *__deque; @InitVar: - __deque = new_spec_list(); - //model_print("init_list\n"); - tag = new_id_tag(); // Beginning of available id - //@Cleanup: - //if (__deque) { - //free_spec_list(__deque); - //model_print("free_list\n"); - //} - //if (tag) - //free_id_tag(tag); - @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) { - //tag_elem_t *res = (tag_elem_t*) wrapper; - return res == NULL ? 0 : ((tag_elem_t*) wrapper)->id; - //if (res == NULL) { - //model_print("wrong id here\n"); - //return 0; - //} - //return res->id; - } - @DefineFunc: - int get_data(void *wrapper) { - //tag_elem_t *res = (tag_elem_t*) wrapper; - //return res->data; - return ((tag_elem_t*) wrapper)->data; - } + __deque = createIntegerList(); + @Finalize: + if (__deque) + destroyIntegerList(__deque); + return true; + @DefineFunc: + bool succ(int res) { + return res != EMPTY && res != ABORT; + } @Happens_before: Push -> Steal - Push -> Take + @Commutativity: Push <-> Steal: true + @Commutativity: Take <-> Steal: true + @End */ @@ -82,16 +53,16 @@ void resize(Deque *q); /** @Begin @Interface: Take - //@Commit_point_set: Take_Read_Bottom | Take_CAS_Top | Take_Additional_Point @Commit_point_set: Take_Read_Bottom | Take_Additional_Point - @ID: __RET__ == EMPTY ? DEFAULT_CALL_ID : get_id(back(__deque)) + @ID: succ(__RET__) ? __RET__ : DEFAULT_CALL_ID @Action: - int _Old_Val = EMPTY; - if (__RET__ != EMPTY && size(__deque) > 0) { - _Old_Val = get_data(back(__deque)); - pop_back(__deque); + int elem = 0; + if (succ(__RET__)) { + elem = back(__deque); + pop_back(__deque); + //model_print("take: elem=%d, __RET__=%d\n", elem, __RET__); } - @Post_check: _Old_Val == __RET__ + @Post_check: succ(__RET__) ? __RET__ == elem : true @End */ int take(Deque *q); @@ -100,8 +71,10 @@ int take(Deque *q); @Begin @Interface: Push @Commit_point_set: Push_Update_Bottom - @ID: get_and_inc(tag); - @Action: push_back(__deque, new_tag_elem(__ID__, x)); + @ID: x + @Action: + push_back(__deque, x); + //model_print("push: elem=%d\n", x); @End */ void push(Deque *q, int x); @@ -109,17 +82,16 @@ void push(Deque *q, int x); /** @Begin @Interface: Steal - //@Commit_point_set: Steal_Read_Bottom | Steal_CAS_Top | Steal_Additional_Point @Commit_point_set: Steal_Read_Bottom | Steal_Additional_Point - @ID: (__RET__ == EMPTY || __RET__ == ABORT) ? DEFAULT_CALL_ID : get_id(front(__deque)) + @ID: succ(__RET__) ? __RET__ : DEFAULT_CALL_ID @Action: - int _Old_Val = EMPTY; - if (__RET__ != EMPTY && __RET__ != ABORT && size(__deque) > 0) { - _Old_Val = get_data(front(__deque)); + int elem = 0; + if (succ(__RET__)) { + elem = front(__deque); pop_front(__deque); + //model_print("steal: elem=%d, __RET__=%d\n", elem, __RET__); } - @Post_check: - _Old_Val == __RET__ || __RET__ == EMPTY || __RET__ == ABORT + @Post_check: succ(__RET__) ? __RET__ == elem : true @End */ int steal(Deque *q); diff --git a/benchmark/chase-lev-deque-bugfix/testcase1.c b/benchmark/chase-lev-deque-bugfix/testcase1.c new file mode 100644 index 0000000..e09efde --- /dev/null +++ b/benchmark/chase-lev-deque-bugfix/testcase1.c @@ -0,0 +1,78 @@ +#include +#include +#include +#include +#include + +#include "model-assert.h" + +#include "deque.h" + +Deque *q; +int a; +int b; +int c; +int x; + +static void task(void * param) { + a=steal(q); + if (a == ABORT) { + printf("Steal NULL\n"); + } else { + printf("Steal %d\n", a); + } + + x=steal(q); + if (x == ABORT) { + printf("Steal NULL\n"); + } else { + printf("Steal %d\n", x); + } +} + +int user_main(int argc, char **argv) +{ + /** + @Begin + @Entry_point + @End + */ + thrd_t t; + q=create(); + thrd_create(&t, task, 0); + push(q, 1); + printf("Push 1\n"); + push(q, 2); + printf("Push 2\n"); + push(q, 4); + printf("Push 4\n"); + b=take(q); + if (b == EMPTY) { + printf("Take NULL\n"); + } else { + printf("Take %d\n", b); + } + c=take(q); + if (c == EMPTY) { + printf("Take NULL\n"); + } else { + printf("Take %d\n", c); + } + thrd_join(t); +/* + bool correct=true; + if (a!=1 && a!=2 && a!=4 && a!= EMPTY) + correct=false; + if (b!=1 && b!=2 && b!=4 && b!= EMPTY) + correct=false; + if (c!=1 && c!=2 && c!=4 && a!= EMPTY) + correct=false; + if (a!=EMPTY && b!=EMPTY && c!=EMPTY && (a+b+c)!=7) + correct=false; + if (!correct) + printf("a=%d b=%d c=%d\n",a,b,c); + */ + //MODEL_ASSERT(correct); + + return 0; +} diff --git a/benchmark/chase-lev-deque-bugfix/testcase2.c b/benchmark/chase-lev-deque-bugfix/testcase2.c new file mode 100644 index 0000000..5c88a76 --- /dev/null +++ b/benchmark/chase-lev-deque-bugfix/testcase2.c @@ -0,0 +1,82 @@ +#include +#include +#include +#include +#include + +#include "model-assert.h" + +#include "deque.h" + +Deque *q; +int a; +int b; +int c; +int x; + +static void task(void * param) { + a=steal(q); + if (a == ABORT) { + printf("Steal NULL\n"); + } else { + printf("Steal %d\n", a); + } + /* + x=steal(q); + if (x == ABORT) { + printf("Steal NULL\n"); + } else { + printf("Steal %d\n", x); + } + */ +} + +int user_main(int argc, char **argv) +{ + /** + @Begin + @Entry_point + @End + */ + thrd_t t; + q=create(); + push(q, 1); + printf("Push 1\n"); + push(q, 2); + printf("Push 2\n"); + push(q, 4); + printf("Push 4\n"); + push(q, 5); + printf("Push 5\n"); + thrd_create(&t, task, 0); + + b=take(q); + if (b == EMPTY) { + printf("Take NULL\n"); + } else { + printf("Take %d\n", b); + } + c=take(q); + if (c == EMPTY) { + printf("Take NULL\n"); + } else { + printf("Take %d\n", c); + } + thrd_join(t); +/* + bool correct=true; + if (a!=1 && a!=2 && a!=4 && a!= EMPTY) + correct=false; + if (b!=1 && b!=2 && b!=4 && b!= EMPTY) + correct=false; + if (c!=1 && c!=2 && c!=4 && a!= EMPTY) + correct=false; + if (a!=EMPTY && b!=EMPTY && c!=EMPTY && (a+b+c)!=7) + correct=false; + if (!correct) + printf("a=%d b=%d c=%d\n",a,b,c); + */ + //MODEL_ASSERT(correct); + + return 0; +} -- 2.34.1