The CDSSpec checker's benchmarks
[model-checker-benchmarks.git] / ms-queue / main.c
1 #include <stdlib.h>
2 #include <stdio.h>
3 #include <threads.h>
4
5 #include "queue.h"
6 #include "model-assert.h"
7
8 static queue_t *queue;
9 static thrd_t *threads;
10 static unsigned int *input;
11 static unsigned int *output;
12 static int num_threads;
13
14 int get_thread_num()
15 {
16         thrd_t curr = thrd_current();
17         int i;
18         for (i = 0; i < num_threads; i++)
19                 if (curr.priv == threads[i].priv)
20                         return i;
21         MODEL_ASSERT(0);
22         return -1;
23 }
24
25 bool succ1, succ2;
26 atomic_int x[3];
27 unsigned int idx1, idx2;
28 unsigned int reclaimNode;
29
30 static int procs = 2;
31 static void main_task(void *param)
32 {
33         unsigned int val;
34         int pid = *((int *)param);
35         if (pid % 2 == 0) {
36                 enqueue(queue, 0, 0);
37                 succ1 = dequeue(queue, &idx1, &reclaimNode);
38         } else {
39                 enqueue(queue, 1, 0);
40                 succ2 = dequeue(queue, &idx2, &reclaimNode);
41         }
42 }
43
44 int user_main(int argc, char **argv)
45 {
46         int i;
47         int *param;
48         unsigned int in_sum = 0, out_sum = 0;
49
50         /** @Entry */
51         queue = (queue_t*) calloc(1, sizeof(*queue));
52         MODEL_ASSERT(queue);
53
54         num_threads = procs;
55         threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t));
56         param = (int*) malloc(num_threads * sizeof(*param));
57         input = (unsigned int *) calloc(num_threads, sizeof(*input));
58         output = (unsigned int *) calloc(num_threads, sizeof(*output));
59
60         init_queue(queue, num_threads);
61         for (i = 0; i < num_threads; i++) {
62                 param[i] = i;
63                 thrd_create(&threads[i], main_task, &param[i]);
64         }
65         for (i = 0; i < num_threads; i++)
66                 thrd_join(threads[i]);
67 /*
68         for (i = 0; i < num_threads; i++) {
69                 in_sum += input[i];
70                 out_sum += output[i];
71         }
72         for (i = 0; i < num_threads; i++)
73                 printf("input[%d] = %u\n", i, input[i]);
74         for (i = 0; i < num_threads; i++)
75                 printf("output[%d] = %u\n", i, output[i]);
76         if (succ1 && succ2)
77                 MODEL_ASSERT(in_sum == out_sum);
78         else
79                 MODEL_ASSERT (false);
80 */
81         free(param);
82         free(threads);
83         free(queue);
84
85         return 0;
86 }