edits

[cdsspec-compiler.git] / output / chase-lev-deque-bugfix / testcase2.c

diff --git a/output/chase-lev-deque-bugfix/testcase2.c b/output/chase-lev-deque-bugfix/testcase2.c
new file mode 100644 (file)
index 0000000..dc28d1b
--- /dev/null
+++ b/output/chase-lev-deque-bugfix/testcase2.c
@@ -0,0 +1,60 @@
+#include <stdlib.h>
+#include <assert.h>
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#include "model-assert.h"
+
+#include "deque.h"
+
+Deque *q;
+int a;
+int b;
+int c;
+int x;
+
+static void task(void * param) {
+       a=steal(q);
+       if (a == ABORT) {
+               printf("Steal NULL\n");
+       } else {
+               printf("Steal %d\n", a);
+       }
+       
+}
+
+int user_main(int argc, char **argv)
+{
+       __sequential_init();
+       
+       thrd_t t;
+       q=create();
+       push(q, 1);
+       printf("Push 1\n");
+       push(q, 2);
+       printf("Push 2\n");
+       push(q, 4);
+       printf("Push 4\n");
+       push(q, 5);
+       printf("Push 5\n");
+       thrd_create(&t, task, 0);
+
+       b=take(q);
+       if (b == EMPTY) {
+               printf("Take NULL\n");
+       } else {
+               printf("Take %d\n", b);
+       }
+       c=take(q);
+       if (c == EMPTY) {
+               printf("Take NULL\n");
+       } else {
+               printf("Take %d\n", c);
+       }
+       thrd_join(t);
+
+       
+       return 0;
+}
+