From: Peizhao Ou <peizhaoo@uci.edu>
Date: Wed, 18 Nov 2015 03:04:15 +0000 (-0800)
Subject: edits
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=a155ac407f80a2b302aba2c2a2a4eb83f220236c;p=cdsspec-compiler.git
edits
---
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 <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
index 0000000..5c88a76
--- /dev/null
+++ b/benchmark/chase-lev-deque-bugfix/testcase2.c
@@ -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;
+}