changes

[model-checker-benchmarks.git] / chase-lev-deque-bugfix / note.txt

diff --git a/chase-lev-deque-bugfix/note.txt b/chase-lev-deque-bugfix/note.txt
index 88183f8283485c49ce7a84251e5607eddb3fb6c2..f54d934dca5f1ccf2fab8867b3bbed0674331732 100644 (file)
--- a/chase-lev-deque-bugfix/note.txt
+++ b/chase-lev-deque-bugfix/note.txt
@@ -53,3 +53,22 @@ 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().
+
+
+By running our testcases from 1-6, it took:
+0m0.013s (testcase1)
+0m0.028s (testcase2)
+0m6.264s (testcase3)
+0m0.824s (testcase4)
+0m0.054s (testcase5)
+9m19.887s (testcase6)
+
+In total: 9m27.02s
+