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 21639067d65ebb32c508a07e4e233295ba78d553..f3b22abefbf119c8403bb71d95c703aa1929d29f 100644 (file)
--- a/chase-lev-deque-bugfix/testcase2.c
+++ b/chase-lev-deque-bugfix/testcase2.c
@@ -13,21 +13,32 @@ 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) {
-       a=steal(q);
+       b=steal(q);
+       c=steal(q);
 }
 
 int user_main(int argc, char **argv)
 {
-       thrd_t t;
-       q=create();
-       thrd_create(&t, task, 0);
+       thrd_t t1, t2;
+       q=create_size(4);
        push(q, 1);
        push(q, 2);
-       //push(q, 4);
-       b=take(q);
-       c=take(q);
-       thrd_join(t);
+       push(q, 3);
+       thrd_create(&t1, task, 0);
+       //thrd_create(&t2, task, 0);
+       a=take(q);
+       //c=take(q);
+       thrd_join(t1);
+       //thrd_join(t2);
 
 /*
        bool correct=true;