df419c113297956537e6cd14c5bb9590c974a402
[model-checker-benchmarks.git] / chase-lev-deque-bugfix / testcase7.c
1 #include <stdlib.h>
2 #include <assert.h>
3 #include <stdio.h>
4 #include <threads.h>
5 #include <stdatomic.h>
6
7 #include "model-assert.h"
8
9 #include "deque.h"
10
11 Deque *q;
12 int a;
13 int b;
14 int c;
15
16 static void task1(void * param) {
17         b=steal(q);
18 }
19
20 static void task2(void * param) {
21         b=steal(q);
22         c=steal(q);
23 }
24
25 int user_main(int argc, char **argv)
26 {
27         thrd_t t1, t2;
28         q=create();
29
30         push(q, 1);
31         push(q, 2);
32         thrd_create(&t1, task1, 0);
33         thrd_create(&t2, task2, 0);
34         //push(q, 3);
35         a=take(q);
36         //c=take(q);
37         thrd_join(t1);
38         thrd_join(t2);
39
40 /*
41         bool correct=true;
42         if (a!=1 && a!=2 && a!=4 && a!= EMPTY)
43                 correct=false;
44         if (b!=1 && b!=2 && b!=4 && b!= EMPTY)
45                 correct=false;
46         if (c!=1 && c!=2 && c!=4 && a!= EMPTY)
47                 correct=false;
48         if (a!=EMPTY && b!=EMPTY && c!=EMPTY && (a+b+c)!=7)
49                 correct=false;
50         //if (!correct)
51                 printf("a=%d b=%d c=%d\n",a,b,c);
52         MODEL_ASSERT(correct);
53         */
54
55         return 0;
56 }