edits
authorPeizhao Ou <peizhaoo@uci.edu>
Wed, 18 Nov 2015 03:04:15 +0000 (19:04 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Wed, 18 Nov 2015 03:04:15 +0000 (19:04 -0800)
benchmark/chase-lev-deque-bugfix/Makefile
benchmark/chase-lev-deque-bugfix/deque.c
benchmark/chase-lev-deque-bugfix/deque.h
benchmark/chase-lev-deque-bugfix/testcase1.c [new file with mode: 0644]
benchmark/chase-lev-deque-bugfix/testcase2.c [new file with mode: 0644]

index 91ff999..3980f68 100644 (file)
@@ -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)
index 854091f..010704c 100644 (file)
@@ -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);
                /**
index 837df89..82560f1 100644 (file)
@@ -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 (file)
index 0000000..e09efde
--- /dev/null
@@ -0,0 +1,78 @@
+#include <stdlib.h>
+#include <assert.h>
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#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 (file)
index 0000000..5c88a76
--- /dev/null
@@ -0,0 +1,82 @@
+#include <stdlib.h>
+#include <assert.h>
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#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;
+}