f6243f999abf5e807e545130132ad21445c1aa71
[model-checker-benchmarks.git] / ms-queue / testcase3.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 int idx1, idx2;
28
29 static int procs = 4;
30 static void main_task(void *param)
31 {
32         unsigned int val;
33         int pid = *((int *)param);
34         if (pid % 4 == 0) {
35                 atomic_store_explicit(&x[0], 1, memory_order_relaxed);
36                 enqueue(queue, 0);
37         
38                 succ1 = dequeue(queue, &idx1);
39                 if (succ1) {
40                         atomic_load_explicit(&x[idx1], memory_order_relaxed);
41                 }
42         } else if (pid % 4 == 1) {
43                 atomic_store_explicit(&x[1], 1, memory_order_relaxed);
44                 enqueue(queue, 1);
45
46                 succ2 = dequeue(queue, &idx2);
47                 if (succ2) {
48                         atomic_load_explicit(&x[idx2], memory_order_relaxed);
49                 }
50         } else if (pid % 4 == 2) {
51
52         } else if (pid % 4 == 3) {
53         
54         }
55 }
56
57 int user_main(int argc, char **argv)
58 {
59         int i;
60         int *param;
61         unsigned int in_sum = 0, out_sum = 0;
62
63         queue = calloc(1, sizeof(*queue));
64         MODEL_ASSERT(queue);
65
66         num_threads = procs;
67         threads = malloc(num_threads * sizeof(thrd_t));
68         param = malloc(num_threads * sizeof(*param));
69         input = calloc(num_threads, sizeof(*input));
70         output = calloc(num_threads, sizeof(*output));
71
72         atomic_init(&x[0], 0);
73         atomic_init(&x[1], 0);
74         atomic_init(&x[2], 0);
75         init_queue(queue, num_threads);
76         for (i = 0; i < num_threads; i++) {
77                 param[i] = i;
78                 thrd_create(&threads[i], main_task, &param[i]);
79         }
80         for (i = 0; i < num_threads; i++)
81                 thrd_join(threads[i]);
82 /*
83         for (i = 0; i < num_threads; i++) {
84                 in_sum += input[i];
85                 out_sum += output[i];
86         }
87         for (i = 0; i < num_threads; i++)
88                 printf("input[%d] = %u\n", i, input[i]);
89         for (i = 0; i < num_threads; i++)
90                 printf("output[%d] = %u\n", i, output[i]);
91         if (succ1 && succ2)
92                 MODEL_ASSERT(in_sum == out_sum);
93         else
94                 MODEL_ASSERT (false);
95 */
96         free(param);
97         free(threads);
98         free(queue);
99
100         return 0;
101 }