From 7af936f607d179d4c9df6fa64df17cf30c6f8e59 Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Mon, 16 Mar 2015 18:34:41 -0700
Subject: [PATCH] changes

---
 chase-lev-deque-bugfix/Makefile         |   2 +-
 chase-lev-deque-bugfix/Makefile1        |  26 ++++
 chase-lev-deque-bugfix/deque.c          |  32 +++--
 chase-lev-deque-bugfix/deque.h          |   1 +
 chase-lev-deque-bugfix/deque_backup.c   |  85 +++++++++++++
 chase-lev-deque-bugfix/deque_wildcard.c | 105 ++++++++++++++++
 chase-lev-deque-bugfix/note.txt         |  37 +++++-
 chase-lev-deque-bugfix/result.txt       |  28 +++++
 chase-lev-deque-bugfix/result1.txt      |  27 ++++
 chase-lev-deque-bugfix/result2.txt      | 110 ++++++++++++++++
 chase-lev-deque-bugfix/result3.txt      |  75 +++++++++++
 chase-lev-deque-bugfix/result4.txt      | 159 ++++++++++++++++++++++++
 chase-lev-deque-bugfix/standard.txt     |  39 ++++++
 chase-lev-deque-bugfix/testcase1.c      |  55 ++++++++
 chase-lev-deque-bugfix/testcase2.c      |  19 +--
 chase-lev-deque-bugfix/testcase3.c      |  52 ++++++++
 chase-lev-deque-bugfix/testcase4.c      |  51 ++++++++
 chase-lev-deque-bugfix/testcase5.c      |  52 ++++++++
 18 files changed, 931 insertions(+), 24 deletions(-)
 create mode 100644 chase-lev-deque-bugfix/Makefile1
 create mode 100644 chase-lev-deque-bugfix/deque_backup.c
 create mode 100644 chase-lev-deque-bugfix/deque_wildcard.c
 create mode 100644 chase-lev-deque-bugfix/result.txt
 create mode 100644 chase-lev-deque-bugfix/result1.txt
 create mode 100644 chase-lev-deque-bugfix/result2.txt
 create mode 100644 chase-lev-deque-bugfix/result3.txt
 create mode 100644 chase-lev-deque-bugfix/result4.txt
 create mode 100644 chase-lev-deque-bugfix/standard.txt
 create mode 100644 chase-lev-deque-bugfix/testcase1.c
 create mode 100644 chase-lev-deque-bugfix/testcase3.c
 create mode 100644 chase-lev-deque-bugfix/testcase4.c
 create mode 100644 chase-lev-deque-bugfix/testcase5.c

diff --git a/chase-lev-deque-bugfix/Makefile b/chase-lev-deque-bugfix/Makefile
index d8e9eb4..f061d64 100644
--- a/chase-lev-deque-bugfix/Makefile
+++ b/chase-lev-deque-bugfix/Makefile
@@ -2,7 +2,7 @@ include ../benchmarks.mk
 
 BENCH := deque
 
-NORMAL_TESTS := testcase1 testcase2
+NORMAL_TESTS := testcase1 testcase2 testcase3 testcase4 testcase5
 
 WILDCARD_TESTS := $(patsubst %, %_wildcard, $(NORMAL_TESTS))
 
diff --git a/chase-lev-deque-bugfix/Makefile1 b/chase-lev-deque-bugfix/Makefile1
new file mode 100644
index 0000000..55a4edb
--- /dev/null
+++ b/chase-lev-deque-bugfix/Makefile1
@@ -0,0 +1,26 @@
+include ../benchmarks.mk
+
+BENCH := queue
+
+NORMAL_TESTS := testcase1 testcase2 testcase3
+
+WILDCARD_TESTS := $(patsubst %, %_wildcard, $(NORMAL_TESTS))
+
+TESTS := $(NORMAL_TESTS) $(WILDCARD_TESTS)
+
+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 *.o *.d $(TESTS)
diff --git a/chase-lev-deque-bugfix/deque.c b/chase-lev-deque-bugfix/deque.c
index 6328446..8694045 100644
--- a/chase-lev-deque-bugfix/deque.c
+++ b/chase-lev-deque-bugfix/deque.c
@@ -4,6 +4,16 @@
 #include <stdlib.h>
 #include <stdio.h>
 
+Deque * create_size(int size) {
+	Deque * q = (Deque *) calloc(1, sizeof(Deque));
+	Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int));
+	atomic_store_explicit(&q->array, a, memory_order_relaxed);
+	atomic_store_explicit(&q->top, 0, memory_order_relaxed);
+	atomic_store_explicit(&q->bottom, 0, memory_order_relaxed);
+	atomic_store_explicit(&a->size, size, memory_order_relaxed);
+	return q;
+}
+
 Deque * create() {
 	Deque * q = (Deque *) calloc(1, sizeof(Deque));
 	Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int));
@@ -18,7 +28,7 @@ int take(Deque *q) {
 	size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
 	Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
 	atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
-	atomic_thread_fence(memory_order_seq_cst);
+	atomic_thread_fence(memory_order_relaxed); // sc
 	size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
 	int x;
 	if (t <= b) {
@@ -26,7 +36,8 @@ int take(Deque *q) {
 		x = atomic_load_explicit(&a->buffer[b % atomic_load_explicit(&a->size,memory_order_relaxed)], memory_order_relaxed);
 		if (t == b) {
 			/* Single last element in queue. */
-			if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed))
+			if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
+				memory_order_acquire, memory_order_relaxed)) // sc
 				/* Failed race. */
 				x = EMPTY;
 			atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
@@ -50,13 +61,13 @@ void resize(Deque *q) {
 	for(i=top; i < bottom; i++) {
 		atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
 	}
-	atomic_store_explicit(&q->array, new_a, memory_order_release);
+	atomic_store_explicit(&q->array, new_a, memory_order_relaxed); // release
 	printf("resize\n");
 }
 
 void push(Deque *q, int x) {
 	size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
-	size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
+	size_t t = atomic_load_explicit(&q->top, memory_order_relaxed); // 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);
@@ -64,20 +75,21 @@ void push(Deque *q, int x) {
 		a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
 	}
 	atomic_store_explicit(&a->buffer[b % atomic_load_explicit(&a->size, memory_order_relaxed)], x, memory_order_relaxed);
-	atomic_thread_fence(memory_order_release);
+	atomic_thread_fence(memory_order_relaxed); // release
 	atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
 }
 
 int steal(Deque *q) {
-	size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
-	atomic_thread_fence(memory_order_seq_cst);
-	size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
+	size_t t = atomic_load_explicit(&q->top, memory_order_relaxed); // acquire
+	atomic_thread_fence(memory_order_relaxed); // sc
+	size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed); // acquire
 	int x = EMPTY;
 	if (t < b) {
 		/* Non-empty queue. */
-		Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
+		Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); // acquire
 		x = atomic_load_explicit(&a->buffer[t % atomic_load_explicit(&a->size, memory_order_relaxed)], memory_order_relaxed);
-		if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed))
+		if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
+			memory_order_release, memory_order_relaxed)) // sc
 			/* Failed race. */
 			return ABORT;
 	}
diff --git a/chase-lev-deque-bugfix/deque.h b/chase-lev-deque-bugfix/deque.h
index f474355..3bb1058 100644
--- a/chase-lev-deque-bugfix/deque.h
+++ b/chase-lev-deque-bugfix/deque.h
@@ -11,6 +11,7 @@ typedef struct {
 	atomic_uintptr_t array; /* Atomic(Array *) */
 } Deque;
 
+Deque * create_size(int size);
 Deque * create();
 int take(Deque *q);
 void resize(Deque *q);
diff --git a/chase-lev-deque-bugfix/deque_backup.c b/chase-lev-deque-bugfix/deque_backup.c
new file mode 100644
index 0000000..6328446
--- /dev/null
+++ b/chase-lev-deque-bugfix/deque_backup.c
@@ -0,0 +1,85 @@
+#include <stdatomic.h>
+#include <inttypes.h>
+#include "deque.h"
+#include <stdlib.h>
+#include <stdio.h>
+
+Deque * create() {
+	Deque * q = (Deque *) calloc(1, sizeof(Deque));
+	Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int));
+	atomic_store_explicit(&q->array, a, memory_order_relaxed);
+	atomic_store_explicit(&q->top, 0, memory_order_relaxed);
+	atomic_store_explicit(&q->bottom, 0, memory_order_relaxed);
+	atomic_store_explicit(&a->size, 2, memory_order_relaxed);
+	return q;
+}
+
+int take(Deque *q) {
+	size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
+	Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+	atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
+	atomic_thread_fence(memory_order_seq_cst);
+	size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
+	int x;
+	if (t <= b) {
+		/* Non-empty queue. */
+		x = atomic_load_explicit(&a->buffer[b % atomic_load_explicit(&a->size,memory_order_relaxed)], memory_order_relaxed);
+		if (t == b) {
+			/* Single last element in queue. */
+			if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed))
+				/* Failed race. */
+				x = EMPTY;
+			atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
+		}
+	} else { /* Empty queue. */
+		x = EMPTY;
+		atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
+	}
+	return x;
+}
+
+void resize(Deque *q) {
+	Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+	size_t size=atomic_load_explicit(&a->size, memory_order_relaxed);
+	size_t new_size=size << 1;
+	Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array));
+	size_t top=atomic_load_explicit(&q->top, memory_order_relaxed);
+	size_t bottom=atomic_load_explicit(&q->bottom, memory_order_relaxed);
+	atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed);
+	size_t i;
+	for(i=top; i < bottom; i++) {
+		atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
+	}
+	atomic_store_explicit(&q->array, new_a, memory_order_release);
+	printf("resize\n");
+}
+
+void push(Deque *q, int x) {
+	size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
+	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);
+		//Bug in paper...should have next line...
+		a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+	}
+	atomic_store_explicit(&a->buffer[b % atomic_load_explicit(&a->size, memory_order_relaxed)], x, memory_order_relaxed);
+	atomic_thread_fence(memory_order_release);
+	atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
+}
+
+int steal(Deque *q) {
+	size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
+	atomic_thread_fence(memory_order_seq_cst);
+	size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
+	int x = EMPTY;
+	if (t < b) {
+		/* Non-empty queue. */
+		Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
+		x = atomic_load_explicit(&a->buffer[t % atomic_load_explicit(&a->size, memory_order_relaxed)], memory_order_relaxed);
+		if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed))
+			/* Failed race. */
+			return ABORT;
+	}
+	return x;
+}
diff --git a/chase-lev-deque-bugfix/deque_wildcard.c b/chase-lev-deque-bugfix/deque_wildcard.c
new file mode 100644
index 0000000..b31f574
--- /dev/null
+++ b/chase-lev-deque-bugfix/deque_wildcard.c
@@ -0,0 +1,105 @@
+#include <stdatomic.h>
+#include <inttypes.h>
+#include "deque.h"
+#include <stdlib.h>
+#include <stdio.h>
+#include "wildcard.h"
+
+Deque * create_size(int size) {
+	Deque * q = (Deque *) calloc(1, sizeof(Deque));
+	Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int));
+	atomic_store_explicit(&q->array, a, wildcard(1));
+	atomic_store_explicit(&q->top, 0, wildcard(2));
+	atomic_store_explicit(&q->bottom, 0, wildcard(3));
+	atomic_store_explicit(&a->size, size, wildcard(4));
+	return q;
+}
+
+Deque * create() {
+	Deque * q = (Deque *) calloc(1, sizeof(Deque));
+	Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int));
+	atomic_store_explicit(&q->array, a, wildcard(1));
+	atomic_store_explicit(&q->top, 0, wildcard(2));
+	atomic_store_explicit(&q->bottom, 0, wildcard(3));
+	atomic_store_explicit(&a->size, 2, wildcard(4));
+	return q;
+}
+
+int take(Deque *q) {
+	size_t b = atomic_load_explicit(&q->bottom, wildcard(5)) - 1;
+	Array *a = (Array *) atomic_load_explicit(&q->array, wildcard(6));
+	atomic_store_explicit(&q->bottom, b, wildcard(7));
+	atomic_thread_fence(wildcard(8)); // seq_cst
+	size_t t = atomic_load_explicit(&q->top, wildcard(9));
+	int x;
+	if (t <= b) {
+		/* Non-empty queue. */
+		x = atomic_load_explicit(&a->buffer[b %
+		atomic_load_explicit(&a->size,wildcard(10))], wildcard(11));
+		if (t == b) {
+			/* Single last element in queue. */
+			if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
+				wildcard(12), wildcard(13))) // 12 -> seq_cst
+				/* Failed race. */
+				x = EMPTY;
+			atomic_store_explicit(&q->bottom, b + 1, wildcard(14));
+		}
+	} else { /* Empty queue. */
+		x = EMPTY;
+		atomic_store_explicit(&q->bottom, b + 1, wildcard(15));
+	}
+	return x;
+}
+
+void resize(Deque *q) {
+	Array *a = (Array *) atomic_load_explicit(&q->array, wildcard(16));
+	size_t size=atomic_load_explicit(&a->size, wildcard(17));
+	size_t new_size=size << 1;
+	Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array));
+	size_t top=atomic_load_explicit(&q->top, wildcard(18));
+	size_t bottom=atomic_load_explicit(&q->bottom, wildcard(19));
+	atomic_store_explicit(&new_a->size, new_size, wildcard(20));
+	size_t i;
+	for(i=top; i < bottom; i++) {
+		atomic_store_explicit(&new_a->buffer[i % new_size],
+		atomic_load_explicit(&a->buffer[i % size], wildcard(21)), wildcard(22));
+	}
+	atomic_store_explicit(&q->array, new_a, wildcard(23)); // release
+	printf("resize\n");
+}
+
+void push(Deque *q, int x) {
+	size_t b = atomic_load_explicit(&q->bottom, wildcard(24));
+	size_t t = atomic_load_explicit(&q->top, wildcard(25)); // acquire
+	Array *a = (Array *) atomic_load_explicit(&q->array, wildcard(26));
+	if (b - t > atomic_load_explicit(&a->size, wildcard(27)) - 1) /* Full queue. */ {
+		resize(q);
+		//Bug in paper...should have next line...
+		a = (Array *) atomic_load_explicit(&q->array, wildcard(28));
+	}
+	atomic_store_explicit(&a->buffer[b % atomic_load_explicit(&a->size,
+	wildcard(29))], x, wildcard(30));
+	atomic_thread_fence(wildcard(31)); // release
+	//atomic_thread_fence(release); // release
+	atomic_store_explicit(&q->bottom, b + 1, wildcard(32));
+}
+
+int steal(Deque *q) {
+	size_t t = atomic_load_explicit(&q->top, wildcard(33)); // acquire
+	atomic_thread_fence(wildcard(34)); // seq_cst
+	size_t b = atomic_load_explicit(&q->bottom, wildcard(35)); // acquire
+	int x = EMPTY;
+	if (t < b) {
+		/* Non-empty queue. */
+		// acquire
+		Array *a = (Array *) atomic_load_explicit(&q->array, wildcard(36));
+		x = atomic_load_explicit(&a->buffer[t % atomic_load_explicit(&a->size,
+		wildcard(37))], wildcard(38));
+		// seq_cst
+		if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
+			wildcard(39), wildcard(40)))
+			/* Failed race. */
+			return ABORT;
+	}
+	return x;
+}
diff --git a/chase-lev-deque-bugfix/note.txt b/chase-lev-deque-bugfix/note.txt
index 272af0d..88183f8 100644
--- a/chase-lev-deque-bugfix/note.txt
+++ b/chase-lev-deque-bugfix/note.txt
@@ -12,17 +12,44 @@ wildcard34 -> sc (fence in steal())
 wildcard39 -> sc (update of top in steal())
 
 #1:
+wildcard31 -> release (fence) 
+wildcard35 -> acquire
+Establish hb between push() and steal() via the variable bottom.
+**************** testcase1.c ****************
+
+#2:
+wildcard8 -> sc (fence)
+wildcard34 -> sc (fence)
+When there are two consecutive steal() in the same thread, and another take() in
+another thread. The first steal() updates the top, and then gets the
+fence(wildcard34) in the second steal(), then it loads bottom (wildcard35). At
+the same time, in take() it first updates bottom (wildcard7), gets the fence (
+wildcard8) and then loads the top (wildcard9), as follows.
+
+t.CAS (w39 in first steal())         b.store (w7 in take())
+fence (w34 in second steal())        fence (w8 in take())
+b.load (w35 in second steal())       t.load (w9 in take())
+Both loads can reads old value, so it makes both fences seq_cst.
+**************** testcase2.c ****************
+
+#3:
 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.
+**************** testcase4.c ****************
 
-wildcard31 -> release (fence) 
-wildcard35 -> acquire
-Establish hb between push() and steal() via the variable bottom. 
+#5:
+wildcard25 -> acquire
+wildcard39 -> release (at least)
+Establish hb between steal() and push() when steal() loads bottom (w35) and uses
+CAS (w39) to update the top, and push() reads the top (w25) and updates bottom
+(w32). If not, w35 can read from w39 (future value).
+**************** testcase5.c ****************
 
-wildcard33 -> acquire
+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().
+see the updated bottom in take(). However, since fence (w34) is SC, w33 MAY be
+relaxed.
diff --git a/chase-lev-deque-bugfix/result.txt b/chase-lev-deque-bugfix/result.txt
new file mode 100644
index 0000000..033f197
--- /dev/null
+++ b/chase-lev-deque-bugfix/result.txt
@@ -0,0 +1,28 @@
+Result 0:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_relaxed
+wildcard 4 -> memory_order_relaxed
+wildcard 8 -> memory_order_seq_cst
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_relaxed
+wildcard 18 -> memory_order_relaxed
+wildcard 19 -> memory_order_relaxed
+wildcard 20 -> memory_order_relaxed
+wildcard 23 -> memory_order_relaxed
+wildcard 24 -> memory_order_relaxed
+wildcard 25 -> memory_order_relaxed
+wildcard 26 -> memory_order_relaxed
+wildcard 27 -> memory_order_relaxed
+wildcard 28 -> memory_order_relaxed
+wildcard 29 -> memory_order_relaxed
+wildcard 30 -> memory_order_relaxed
+wildcard 31 -> memory_order_release
+wildcard 32 -> memory_order_relaxed
+wildcard 33 -> memory_order_relaxed
+wildcard 34 -> memory_order_seq_cst
+wildcard 35 -> memory_order_acquire
+wildcard 36 -> memory_order_relaxed
+wildcard 37 -> memory_order_relaxed
+wildcard 38 -> memory_order_relaxed
+wildcard 39 -> memory_order_relaxed
diff --git a/chase-lev-deque-bugfix/result1.txt b/chase-lev-deque-bugfix/result1.txt
new file mode 100644
index 0000000..46078a8
--- /dev/null
+++ b/chase-lev-deque-bugfix/result1.txt
@@ -0,0 +1,27 @@
+Result 0:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_relaxed
+wildcard 4 -> memory_order_relaxed
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_relaxed
+wildcard 18 -> memory_order_relaxed
+wildcard 19 -> memory_order_relaxed
+wildcard 20 -> memory_order_relaxed
+wildcard 23 -> memory_order_relaxed
+wildcard 24 -> memory_order_relaxed
+wildcard 25 -> memory_order_relaxed
+wildcard 26 -> memory_order_relaxed
+wildcard 27 -> memory_order_relaxed
+wildcard 28 -> memory_order_relaxed
+wildcard 29 -> memory_order_relaxed
+wildcard 30 -> memory_order_relaxed
+wildcard 31 -> memory_order_release
+wildcard 32 -> memory_order_relaxed
+wildcard 33 -> memory_order_relaxed
+wildcard 34 -> memory_order_relaxed
+wildcard 35 -> memory_order_acquire
+wildcard 36 -> memory_order_relaxed
+wildcard 37 -> memory_order_relaxed
+wildcard 38 -> memory_order_relaxed
+wildcard 39 -> memory_order_relaxed
diff --git a/chase-lev-deque-bugfix/result2.txt b/chase-lev-deque-bugfix/result2.txt
new file mode 100644
index 0000000..637352b
--- /dev/null
+++ b/chase-lev-deque-bugfix/result2.txt
@@ -0,0 +1,110 @@
+Result 0:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_relaxed
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_relaxed
+wildcard 7 -> memory_order_relaxed
+wildcard 8 -> memory_order_seq_cst
+wildcard 9 -> memory_order_relaxed
+wildcard 10 -> memory_order_relaxed
+wildcard 11 -> memory_order_relaxed
+wildcard 12 -> memory_order_relaxed
+wildcard 14 -> memory_order_release
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_relaxed
+wildcard 18 -> memory_order_relaxed
+wildcard 19 -> memory_order_relaxed
+wildcard 20 -> memory_order_relaxed
+wildcard 23 -> memory_order_relaxed
+wildcard 24 -> memory_order_relaxed
+wildcard 25 -> memory_order_relaxed
+wildcard 26 -> memory_order_relaxed
+wildcard 27 -> memory_order_relaxed
+wildcard 28 -> memory_order_relaxed
+wildcard 29 -> memory_order_relaxed
+wildcard 30 -> memory_order_relaxed
+wildcard 31 -> memory_order_release
+wildcard 32 -> memory_order_relaxed
+wildcard 33 -> memory_order_relaxed
+wildcard 34 -> memory_order_seq_cst
+wildcard 35 -> memory_order_acquire
+wildcard 36 -> memory_order_relaxed
+wildcard 37 -> memory_order_relaxed
+wildcard 38 -> memory_order_relaxed
+wildcard 39 -> memory_order_relaxed
+
+Result 1:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_relaxed
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_relaxed
+wildcard 7 -> memory_order_relaxed
+wildcard 8 -> memory_order_seq_cst
+wildcard 9 -> memory_order_acquire
+wildcard 10 -> memory_order_relaxed
+wildcard 11 -> memory_order_relaxed
+wildcard 12 -> memory_order_relaxed
+wildcard 14 -> memory_order_relaxed
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_relaxed
+wildcard 18 -> memory_order_relaxed
+wildcard 19 -> memory_order_relaxed
+wildcard 20 -> memory_order_relaxed
+wildcard 23 -> memory_order_relaxed
+wildcard 24 -> memory_order_relaxed
+wildcard 25 -> memory_order_relaxed
+wildcard 26 -> memory_order_relaxed
+wildcard 27 -> memory_order_relaxed
+wildcard 28 -> memory_order_relaxed
+wildcard 29 -> memory_order_relaxed
+wildcard 30 -> memory_order_relaxed
+wildcard 31 -> memory_order_release
+wildcard 32 -> memory_order_relaxed
+wildcard 33 -> memory_order_relaxed
+wildcard 34 -> memory_order_seq_cst
+wildcard 35 -> memory_order_acquire
+wildcard 36 -> memory_order_relaxed
+wildcard 37 -> memory_order_relaxed
+wildcard 38 -> memory_order_relaxed
+wildcard 39 -> memory_order_release
+
+Result 2:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_relaxed
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_relaxed
+wildcard 7 -> memory_order_relaxed
+wildcard 8 -> memory_order_seq_cst
+wildcard 9 -> memory_order_relaxed
+wildcard 10 -> memory_order_relaxed
+wildcard 11 -> memory_order_relaxed
+wildcard 12 -> memory_order_acquire
+wildcard 14 -> memory_order_relaxed
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_relaxed
+wildcard 18 -> memory_order_relaxed
+wildcard 19 -> memory_order_relaxed
+wildcard 20 -> memory_order_relaxed
+wildcard 23 -> memory_order_relaxed
+wildcard 24 -> memory_order_relaxed
+wildcard 25 -> memory_order_relaxed
+wildcard 26 -> memory_order_relaxed
+wildcard 27 -> memory_order_relaxed
+wildcard 28 -> memory_order_relaxed
+wildcard 29 -> memory_order_relaxed
+wildcard 30 -> memory_order_relaxed
+wildcard 31 -> memory_order_release
+wildcard 32 -> memory_order_relaxed
+wildcard 33 -> memory_order_relaxed
+wildcard 34 -> memory_order_seq_cst
+wildcard 35 -> memory_order_acquire
+wildcard 36 -> memory_order_relaxed
+wildcard 37 -> memory_order_relaxed
+wildcard 38 -> memory_order_relaxed
+wildcard 39 -> memory_order_release
diff --git a/chase-lev-deque-bugfix/result3.txt b/chase-lev-deque-bugfix/result3.txt
new file mode 100644
index 0000000..61623bc
--- /dev/null
+++ b/chase-lev-deque-bugfix/result3.txt
@@ -0,0 +1,75 @@
+Result 0:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_relaxed
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_relaxed
+wildcard 7 -> memory_order_relaxed
+wildcard 8 -> memory_order_seq_cst
+wildcard 9 -> memory_order_relaxed
+wildcard 10 -> memory_order_relaxed
+wildcard 11 -> memory_order_relaxed
+wildcard 12 -> memory_order_acquire
+wildcard 14 -> memory_order_relaxed
+wildcard 15 -> memory_order_relaxed
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_relaxed
+wildcard 18 -> memory_order_relaxed
+wildcard 19 -> memory_order_relaxed
+wildcard 20 -> memory_order_relaxed
+wildcard 23 -> memory_order_relaxed
+wildcard 24 -> memory_order_relaxed
+wildcard 25 -> memory_order_relaxed
+wildcard 26 -> memory_order_relaxed
+wildcard 27 -> memory_order_relaxed
+wildcard 28 -> memory_order_relaxed
+wildcard 29 -> memory_order_relaxed
+wildcard 30 -> memory_order_relaxed
+wildcard 31 -> memory_order_release
+wildcard 32 -> memory_order_relaxed
+wildcard 33 -> memory_order_relaxed
+wildcard 34 -> memory_order_seq_cst
+wildcard 35 -> memory_order_acquire
+wildcard 36 -> memory_order_relaxed
+wildcard 37 -> memory_order_relaxed
+wildcard 38 -> memory_order_relaxed
+wildcard 39 -> memory_order_release
+
+Result 1:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_relaxed
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_relaxed
+wildcard 7 -> memory_order_relaxed
+wildcard 8 -> memory_order_seq_cst
+wildcard 9 -> memory_order_relaxed
+wildcard 10 -> memory_order_relaxed
+wildcard 11 -> memory_order_relaxed
+wildcard 12 -> memory_order_relaxed
+wildcard 14 -> memory_order_release
+wildcard 15 -> memory_order_relaxed
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_relaxed
+wildcard 18 -> memory_order_relaxed
+wildcard 19 -> memory_order_relaxed
+wildcard 20 -> memory_order_relaxed
+wildcard 23 -> memory_order_relaxed
+wildcard 24 -> memory_order_relaxed
+wildcard 25 -> memory_order_relaxed
+wildcard 26 -> memory_order_relaxed
+wildcard 27 -> memory_order_relaxed
+wildcard 28 -> memory_order_relaxed
+wildcard 29 -> memory_order_relaxed
+wildcard 30 -> memory_order_relaxed
+wildcard 31 -> memory_order_release
+wildcard 32 -> memory_order_relaxed
+wildcard 33 -> memory_order_relaxed
+wildcard 34 -> memory_order_seq_cst
+wildcard 35 -> memory_order_acquire
+wildcard 36 -> memory_order_relaxed
+wildcard 37 -> memory_order_relaxed
+wildcard 38 -> memory_order_relaxed
+wildcard 39 -> memory_order_relaxed
diff --git a/chase-lev-deque-bugfix/result4.txt b/chase-lev-deque-bugfix/result4.txt
new file mode 100644
index 0000000..f34eab1
--- /dev/null
+++ b/chase-lev-deque-bugfix/result4.txt
@@ -0,0 +1,159 @@
+Result 0:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_relaxed
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_relaxed
+wildcard 7 -> memory_order_relaxed
+wildcard 8 -> memory_order_seq_cst
+wildcard 9 -> memory_order_relaxed
+wildcard 10 -> memory_order_relaxed
+wildcard 11 -> memory_order_relaxed
+wildcard 12 -> memory_order_relaxed
+wildcard 14 -> memory_order_release
+wildcard 15 -> memory_order_relaxed
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_relaxed
+wildcard 18 -> memory_order_relaxed
+wildcard 19 -> memory_order_relaxed
+wildcard 20 -> memory_order_relaxed
+wildcard 21 -> memory_order_relaxed
+wildcard 22 -> memory_order_relaxed
+wildcard 23 -> memory_order_release
+wildcard 24 -> memory_order_relaxed
+wildcard 25 -> memory_order_relaxed
+wildcard 26 -> memory_order_relaxed
+wildcard 27 -> memory_order_relaxed
+wildcard 28 -> memory_order_relaxed
+wildcard 29 -> memory_order_relaxed
+wildcard 30 -> memory_order_release
+wildcard 31 -> memory_order_release
+wildcard 32 -> memory_order_relaxed
+wildcard 33 -> memory_order_relaxed
+wildcard 34 -> memory_order_seq_cst
+wildcard 35 -> memory_order_acquire
+wildcard 36 -> memory_order_acquire
+wildcard 37 -> memory_order_relaxed
+wildcard 38 -> memory_order_acquire
+wildcard 39 -> memory_order_relaxed
+
+Result 1:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_relaxed
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_relaxed
+wildcard 7 -> memory_order_relaxed
+wildcard 8 -> memory_order_seq_cst
+wildcard 9 -> memory_order_relaxed
+wildcard 10 -> memory_order_relaxed
+wildcard 11 -> memory_order_relaxed
+wildcard 12 -> memory_order_relaxed
+wildcard 14 -> memory_order_release
+wildcard 15 -> memory_order_relaxed
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_relaxed
+wildcard 18 -> memory_order_relaxed
+wildcard 19 -> memory_order_relaxed
+wildcard 20 -> memory_order_relaxed
+wildcard 21 -> memory_order_relaxed
+wildcard 22 -> memory_order_relaxed
+wildcard 23 -> memory_order_release
+wildcard 24 -> memory_order_relaxed
+wildcard 25 -> memory_order_acquire
+wildcard 26 -> memory_order_relaxed
+wildcard 27 -> memory_order_relaxed
+wildcard 28 -> memory_order_relaxed
+wildcard 29 -> memory_order_relaxed
+wildcard 30 -> memory_order_relaxed
+wildcard 31 -> memory_order_release
+wildcard 32 -> memory_order_relaxed
+wildcard 33 -> memory_order_relaxed
+wildcard 34 -> memory_order_seq_cst
+wildcard 35 -> memory_order_acquire
+wildcard 36 -> memory_order_acquire
+wildcard 37 -> memory_order_relaxed
+wildcard 38 -> memory_order_relaxed
+wildcard 39 -> memory_order_release
+
+Result 2:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_relaxed
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_relaxed
+wildcard 7 -> memory_order_relaxed
+wildcard 8 -> memory_order_seq_cst
+wildcard 9 -> memory_order_relaxed
+wildcard 10 -> memory_order_relaxed
+wildcard 11 -> memory_order_relaxed
+wildcard 12 -> memory_order_acquire
+wildcard 14 -> memory_order_relaxed
+wildcard 15 -> memory_order_relaxed
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_relaxed
+wildcard 18 -> memory_order_relaxed
+wildcard 19 -> memory_order_relaxed
+wildcard 20 -> memory_order_relaxed
+wildcard 21 -> memory_order_relaxed
+wildcard 22 -> memory_order_relaxed
+wildcard 23 -> memory_order_release
+wildcard 24 -> memory_order_relaxed
+wildcard 25 -> memory_order_relaxed
+wildcard 26 -> memory_order_relaxed
+wildcard 27 -> memory_order_relaxed
+wildcard 28 -> memory_order_relaxed
+wildcard 29 -> memory_order_relaxed
+wildcard 30 -> memory_order_release
+wildcard 31 -> memory_order_release
+wildcard 32 -> memory_order_relaxed
+wildcard 33 -> memory_order_relaxed
+wildcard 34 -> memory_order_seq_cst
+wildcard 35 -> memory_order_acquire
+wildcard 36 -> memory_order_acquire
+wildcard 37 -> memory_order_relaxed
+wildcard 38 -> memory_order_acquire
+wildcard 39 -> memory_order_release
+
+Result 3:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_relaxed
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_relaxed
+wildcard 7 -> memory_order_relaxed
+wildcard 8 -> memory_order_seq_cst
+wildcard 9 -> memory_order_relaxed
+wildcard 10 -> memory_order_relaxed
+wildcard 11 -> memory_order_relaxed
+wildcard 12 -> memory_order_acquire
+wildcard 14 -> memory_order_relaxed
+wildcard 15 -> memory_order_relaxed
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_relaxed
+wildcard 18 -> memory_order_relaxed
+wildcard 19 -> memory_order_relaxed
+wildcard 20 -> memory_order_relaxed
+wildcard 21 -> memory_order_relaxed
+wildcard 22 -> memory_order_relaxed
+wildcard 23 -> memory_order_release
+wildcard 24 -> memory_order_relaxed
+wildcard 25 -> memory_order_acquire
+wildcard 26 -> memory_order_relaxed
+wildcard 27 -> memory_order_relaxed
+wildcard 28 -> memory_order_relaxed
+wildcard 29 -> memory_order_relaxed
+wildcard 30 -> memory_order_relaxed
+wildcard 31 -> memory_order_release
+wildcard 32 -> memory_order_relaxed
+wildcard 33 -> memory_order_relaxed
+wildcard 34 -> memory_order_seq_cst
+wildcard 35 -> memory_order_acquire
+wildcard 36 -> memory_order_acquire
+wildcard 37 -> memory_order_relaxed
+wildcard 38 -> memory_order_relaxed
+wildcard 39 -> memory_order_release
diff --git a/chase-lev-deque-bugfix/standard.txt b/chase-lev-deque-bugfix/standard.txt
new file mode 100644
index 0000000..58f73f0
--- /dev/null
+++ b/chase-lev-deque-bugfix/standard.txt
@@ -0,0 +1,39 @@
+Result 0:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_relaxed
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_relaxed
+wildcard 7 -> memory_order_relaxed
+wildcard 8 -> memory_order_seq_cst
+wildcard 9 -> memory_order_relaxed
+wildcard 10 -> memory_order_relaxed
+wildcard 11 -> memory_order_relaxed
+wildcard 12 -> memory_order_seq_cst
+wildcard 14 -> memory_order_relaxed
+wildcard 15 -> memory_order_relaxed
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_relaxed
+wildcard 18 -> memory_order_relaxed
+wildcard 19 -> memory_order_relaxed
+wildcard 20 -> memory_order_relaxed
+wildcard 21 -> memory_order_relaxed
+wildcard 22 -> memory_order_relaxed
+wildcard 23 -> memory_order_release
+wildcard 24 -> memory_order_relaxed
+wildcard 25 -> memory_order_acquire
+wildcard 26 -> memory_order_relaxed
+wildcard 27 -> memory_order_relaxed
+wildcard 28 -> memory_order_relaxed
+wildcard 29 -> memory_order_relaxed
+wildcard 30 -> memory_order_relaxed
+wildcard 31 -> memory_order_release
+wildcard 32 -> memory_order_relaxed
+wildcard 33 -> memory_order_acquire
+wildcard 34 -> memory_order_seq_cst
+wildcard 35 -> memory_order_acquire
+wildcard 36 -> memory_order_acquire
+wildcard 37 -> memory_order_relaxed
+wildcard 38 -> memory_order_relaxed
+wildcard 39 -> memory_order_seq_cst
diff --git a/chase-lev-deque-bugfix/testcase1.c b/chase-lev-deque-bugfix/testcase1.c
new file mode 100644
index 0000000..026d20f
--- /dev/null
+++ b/chase-lev-deque-bugfix/testcase1.c
@@ -0,0 +1,55 @@
+#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;
+
+atomic_int x[2];
+
+static void task(void * param) {
+	a=steal(q);
+	printf("a=%d\n", a);
+	if (a != EMPTY && a != ABORT)
+		atomic_load_explicit(&x[a], memory_order_relaxed);
+}
+
+int user_main(int argc, char **argv)
+{
+	thrd_t t;
+	atomic_store_explicit(&x[0], 0,  memory_order_relaxed);
+	atomic_store_explicit(&x[1], 0,  memory_order_relaxed);
+	q=create_size(4);
+	thrd_create(&t, task, 0);
+	//atomic_store_explicit(&x[1], 37,  memory_order_relaxed);
+	push(q, 1);
+	//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;
+}
diff --git a/chase-lev-deque-bugfix/testcase2.c b/chase-lev-deque-bugfix/testcase2.c
index 2163906..964d25e 100644
--- a/chase-lev-deque-bugfix/testcase2.c
+++ b/chase-lev-deque-bugfix/testcase2.c
@@ -14,20 +14,23 @@ int b;
 int c;
 
 static void task(void * param) {
-	a=steal(q);
+	b=steal(q);
+	c=steal(q);
 }
 
 int user_main(int argc, char **argv)
 {
-	thrd_t t;
-	q=create();
-	thrd_create(&t, task, 0);
+	thrd_t t1, t2;
+	q=create_size(4);
 	push(q, 1);
 	push(q, 2);
-	//push(q, 4);
-	b=take(q);
-	c=take(q);
-	thrd_join(t);
+	push(q, 3);
+	thrd_create(&t1, task, 0);
+	//thrd_create(&t2, task, 0);
+	a=take(q);
+	//c=take(q);
+	thrd_join(t1);
+	//thrd_join(t2);
 
 /*
 	bool correct=true;
diff --git a/chase-lev-deque-bugfix/testcase3.c b/chase-lev-deque-bugfix/testcase3.c
new file mode 100644
index 0000000..92f33ec
--- /dev/null
+++ b/chase-lev-deque-bugfix/testcase3.c
@@ -0,0 +1,52 @@
+#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);
+	printf("steal a=%d\n", a);
+}
+
+int user_main(int argc, char **argv)
+{
+	thrd_t t1, t2;
+	q=create();
+	push(q, 1);
+	thrd_create(&t1, task, 0);
+	//thrd_create(&t2, task, 0);
+	//push(q, 2);
+	//push(q, 4);
+	b=take(q);
+	printf("take b=%d\n", b);
+	//c=take(q);
+	thrd_join(t1);
+	//thrd_join(t2);
+
+/*
+	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/chase-lev-deque-bugfix/testcase4.c b/chase-lev-deque-bugfix/testcase4.c
new file mode 100644
index 0000000..af332bf
--- /dev/null
+++ b/chase-lev-deque-bugfix/testcase4.c
@@ -0,0 +1,51 @@
+#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) {
+	b=steal(q);
+}
+
+int user_main(int argc, char **argv)
+{
+	thrd_t t1, t2;
+	q=create();
+
+	push(q, 1);
+	push(q, 2);
+	thrd_create(&t1, task, 0);
+	push(q, 3);
+	//thrd_create(&t2, task, 0);
+	//a=take(q);
+	//c=take(q);
+	thrd_join(t1);
+	//thrd_join(t2);
+
+/*
+	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/chase-lev-deque-bugfix/testcase5.c b/chase-lev-deque-bugfix/testcase5.c
new file mode 100644
index 0000000..f171a39
--- /dev/null
+++ b/chase-lev-deque-bugfix/testcase5.c
@@ -0,0 +1,52 @@
+#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) {
+	b=steal(q);
+	//c=steal(q);
+}
+
+int user_main(int argc, char **argv)
+{
+	thrd_t t1, t2;
+	q=create();
+
+	push(q, 1);
+	thrd_create(&t1, task, 0);
+	//thrd_create(&t2, task, 0);
+	push(q, 2);
+	//push(q, 3);
+	//a=take(q);
+	//c=take(q);
+	thrd_join(t1);
+	//thrd_join(t2);
+
+/*
+	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