From: Peizhao Ou <peizhaoo@uci.edu>
Date: Tue, 17 Mar 2015 19:59:17 +0000 (-0700)
Subject: changes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=390a6072c0cd601ab6b1dac8a1322741fc02c144;p=model-checker-benchmarks.git

changes
---

diff --git a/chase-lev-deque-bugfix/note.txt b/chase-lev-deque-bugfix/note.txt
index 88183f8..1a38a48 100644
--- a/chase-lev-deque-bugfix/note.txt
+++ b/chase-lev-deque-bugfix/note.txt
@@ -53,3 +53,10 @@ 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(). However, since fence (w34) is SC, w33 MAY be
 relaxed.
+!!! w33 can be relaxed since w34 is an SC fence. Probably w12 doesn't have to be
+release since w8 is an SC fence too, so it will have establish hb between the
+fences.
+
+##################################################
+testcase5.c is a testcase that has 2 threads, 1 of which has 1 steal() and the
+other has 3 push() followed by 2 take().
diff --git a/chase-lev-deque-bugfix/testcase5.c b/chase-lev-deque-bugfix/testcase5.c
index f171a39..0d6d3e4 100644
--- a/chase-lev-deque-bugfix/testcase5.c
+++ b/chase-lev-deque-bugfix/testcase5.c
@@ -27,9 +27,9 @@ int user_main(int argc, char **argv)
 	thrd_create(&t1, task, 0);
 	//thrd_create(&t2, task, 0);
 	push(q, 2);
-	//push(q, 3);
-	//a=take(q);
-	//c=take(q);
+	push(q, 3);
+	a=take(q);
+	c=take(q);
 	thrd_join(t1);
 	//thrd_join(t2);