X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=chase-lev-deque-bugfix%2Ftestcase2.c;h=f3b22abefbf119c8403bb71d95c703aa1929d29f;hb=d634d19b6134309ed0893c6fd58d815cbafecd16;hp=964d25e9fb76e756470f168744e61497201b62ad;hpb=7af936f607d179d4c9df6fa64df17cf30c6f8e59;p=model-checker-benchmarks.git

diff --git a/chase-lev-deque-bugfix/testcase2.c b/chase-lev-deque-bugfix/testcase2.c
index 964d25e..f3b22ab 100644
--- a/chase-lev-deque-bugfix/testcase2.c
+++ b/chase-lev-deque-bugfix/testcase2.c
@@ -13,6 +13,14 @@ int a;
 int b;
 int c;
 
+/**
+	Making the two fences (w8 & w34) seq_cst; the two steals and the take have the following:
+	t.CAS() (in steal1)          b.store (in take)
+	fence() (in steal2)	         fence() (in take)
+	b.load() (in steal2)         t.load() (in take)
+	neither loads reads the updated value.
+*/
+
 static void task(void * param) {
 	b=steal(q);
 	c=steal(q);