The CDSSpec checker's benchmarks
[model-checker-benchmarks.git] / spsc-bugfix / testcase1.cc
1 #include <threads.h>
2
3 #include "queue.h"
4
5 spsc_queue<int> *q;
6
7 void thread(unsigned thread_index)
8 {
9         if (0 == thread_index)
10         {
11                 enqueue(q, 11);
12         }
13         else
14         {
15                 int d = dequeue(q);
16                 //RL_ASSERT(11 == d);
17         }
18 }
19
20 int user_main(int argc, char **argv)
21 {
22         thrd_t A, B;
23         /** @Entry */
24         q = new spsc_queue<int>();
25
26         thrd_create(&A, (thrd_start_t)&thread, (void *)0);
27         thrd_create(&B, (thrd_start_t)&thread, (void *)1);
28         thrd_join(A);
29         thrd_join(B);
30
31         delete q;
32
33         return 0;
34 }