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