From: Peizhao Ou <peizhaoo@uci.edu>
Date: Sat, 28 Feb 2015 01:25:05 +0000 (-0800)
Subject: changes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6a44dcf8aca9f70cd302d5f0929de2471fb3267f;p=model-checker-benchmarks.git

changes
---

diff --git a/chase-lev-deque-bugfix/Makefile b/chase-lev-deque-bugfix/Makefile
index 91ff999..d8e9eb4 100644
--- 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
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
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;
+}