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 272af0de3d581c2c24b9d64c4f67a94cfdde8b78..f54d934dca5f1ccf2fab8867b3bbed0674331732 100644 (file)
--- a/chase-lev-deque-bugfix/note.txt
+++ b/chase-lev-deque-bugfix/note.txt
@@ -12,17 +12,63 @@ wildcard34 -> sc (fence in steal())
 wildcard39 -> sc (update of top in steal())
 
 #1:
 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.
 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
 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.
+!!! 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
+