The CDSSpec checker's benchmarks
[model-checker-benchmarks.git] / blocking-mpmc-example / main.cc
1 #include <stdlib.h>
2 #include <stdio.h>
3 #include <threads.h>
4 #include "queue.h"
5
6 static int procs = 3;
7 Queue *q;
8
9 int idx1, idx2;
10 unsigned int a, b;
11
12
13 atomic_int x[3];
14
15 static void main_task(void *param)
16 {
17         unsigned int val;
18         int pid = *((int *)param);
19         if (pid % 3 == 0) {
20                 enq(q, 2);
21         } else if (pid % 3 == 1) {
22                 deq(q);
23         } else if (pid % 3 == 2) {
24                 deq(q);
25         }
26 }
27
28 int user_main(int argc, char **argv)
29 {
30         int i;
31         int *param;
32
33         atomic_init(&x[1], 0);
34         atomic_init(&x[2], 0);
35         
36         /** @Entry */
37         q = new Queue;
38
39         int num_threads = 3;
40
41         param = new int[num_threads];
42         thrd_t *threads = new thrd_t[num_threads];
43
44         for (i = 0; i < num_threads; i++) {
45                 param[i] = i;
46                 thrd_create(&threads[i], main_task, &param[i]);
47         }
48         for (i = 0; i < num_threads; i++)
49                 thrd_join(threads[i]);
50
51         delete param;
52         delete threads;
53         delete q;
54         
55         return 0;
56 }