From: Brian Demsky Date: Thu, 7 Mar 2013 03:06:26 +0000 (-0800) Subject: deque: wrong bug fix before...now the correct one X-Git-Tag: oopsla2013-final~27^2~2 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker-benchmarks.git;a=commitdiff_plain;h=d1991f77986f3c19631073acbaf4d74a2dbd906b deque: wrong bug fix before...now the correct one --- diff --git a/chase-lev-deque/main.c b/chase-lev-deque/main.c index 77ea5a8..ee69867 100644 --- a/chase-lev-deque/main.c +++ b/chase-lev-deque/main.c @@ -11,7 +11,9 @@ int a; int b; static void task(void * param) { - a=steal(q); + do { + a=steal(q); + } while(a==EMPTY); } int user_main(int argc, char **argv) @@ -21,9 +23,7 @@ int user_main(int argc, char **argv) thrd_create(&t, task, 0); push(q, 1); push(q, 2); - do { - b=take(q); - } while(b==EMPTY); + b=take(q); thrd_join(t); if (a+b!=3) printf("a=%d b=%d\n",a,b);