changes

[model-checker-benchmarks.git] / chase-lev-deque-bugfix / testcase2.c

diff --git a/chase-lev-deque-bugfix/testcase2.c b/chase-lev-deque-bugfix/testcase2.c
index 964d25e9fb76e756470f168744e61497201b62ad..fe77b178342953450f089ad6536b9d7595d21231 100644 (file)
--- 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 w39 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);