changes

diff --git a/chase-lev-deque-bugfix/Makefile b/chase-lev-deque-bugfix/Makefile
index 91ff999c9d5163e3d22e0f4754b3a1cdc08bcc0e..d8e9eb45382b86cf5c67d6f6636bec8697869497 100644 (file)
--- a/chase-lev-deque-bugfix/Makefile
+++ b/chase-lev-deque-bugfix/Makefile
@@ -1,17 +1,26 @@
 include ../benchmarks.mk
 
-TESTNAME = main
+BENCH := deque
 
-HEADERS = deque.h
-OBJECTS = main.o deque.o
+NORMAL_TESTS := testcase1 testcase2
 
-all: $(TESTNAME)
+WILDCARD_TESTS := $(patsubst %, %_wildcard, $(NORMAL_TESTS))
 
-$(TESTNAME): $(HEADERS) $(OBJECTS)
-       $(CC) -o $@ $(OBJECTS) $(CPPFLAGS) $(LDFLAGS)
+TESTS := $(NORMAL_TESTS) $(WILDCARD_TESTS)
 
-%.o: %.c
-       $(CC) -c -o $@ $< $(CPPFLAGS)
+all: $(TESTS)
+
+$(BENCH).o : $(BENCH).c $(BENCH).h
+       $(CC) -o $@ $< $(CFLAGS) -c $(LDFLAGS)
+
+$(BENCH)_wildcard.o : $(BENCH)_wildcard.c $(BENCH).h
+       $(CC) -o $@ $< $(CFLAGS) -c $(LDFLAGS)
+
+$(WILDCARD_TESTS): %_wildcard : %.c $(BENCH)_wildcard.o 
+       $(CC) -o $@ $^ $(CFLAGS) $(LDFLAGS)
+
+$(NORMAL_TESTS): % : %.c $(BENCH).o
+       $(CC) -o $@ $^ $(CFLAGS) $(LDFLAGS)
 
 clean:
-       rm -f $(TESTNAME) *.o
+       rm -f *.o *.d $(TESTS)

diff --git a/chase-lev-deque-bugfix/note.txt b/chase-lev-deque-bugfix/note.txt
new file mode 100644 (file)
index 0000000..272af0d
--- /dev/null
+++ b/chase-lev-deque-bugfix/note.txt
@@ -0,0 +1,28 @@
+#1: Ordering parameters
+
+wildcard8 -> sc (fence in take())
+wildcard12 -> sc (update of top in take())
+*wildcard23 -> release (update of array in resize())
+wildcard25 -> acquire (load of top in push())
+*wildcard31 -> release (fence in push())
+wildcard33 -> acquire (load of top in steal())
+wildcard34 -> sc (fence in steal())
+*wildcard35 -> acquire (load of bottom in steal())
+*wildcard36 -> acquire (load of array in steal())
+wildcard39 -> sc (update of top in steal())
+
+#1:
+wildcard23 -> release
+wildcard36 -> acquire
+Update of array in resize(), should be release; since only steal() need to
+establish hb, so in steal wildcard36 should be acquire.
+
+wildcard31 -> release (fence) 
+wildcard35 -> acquire
+Establish hb between push() and steal() via the variable bottom. 
+
+wildcard33 -> acquire
+wildcard12 -> release (at least)
+Establish hb between take() and steal() when there's only one element in the
+deque, and take() gets the last element. The hb ensures that the steal() will
+see the updated bottom in take().

diff --git a/chase-lev-deque-bugfix/testcase2.c b/chase-lev-deque-bugfix/testcase2.c
new file mode 100644 (file)
index 0000000..2163906
--- /dev/null
+++ b/chase-lev-deque-bugfix/testcase2.c
@@ -0,0 +1,48 @@
+#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;
+
+static void task(void * param) {
+       a=steal(q);
+}
+
+int user_main(int argc, char **argv)
+{
+       thrd_t t;
+       q=create();
+       thrd_create(&t, task, 0);
+       push(q, 1);
+       push(q, 2);
+       //push(q, 4);
+       b=take(q);
+       c=take(q);
+       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;
+}