6 #include "model-assert.h"
9 static thrd_t *threads;
10 static unsigned int *input;
11 static unsigned int *output;
12 static int num_threads;
16 thrd_t curr = thrd_current();
18 for (i = 0; i < num_threads; i++)
19 if (curr.priv == threads[i].priv)
28 unsigned int reclaimNode1, reclaimNode2;
33 /** This testcase can infer w2->release & w4->acquire.
34 The initial node that Head and Tail points to is 1, so when T3 enqueue with
35 node 2, and dequeue(get node 1), and enqueue node 1 again, the second time
36 it enqueues node 1 it actually first initialize node1->next. At the same
37 time in T2, it reads that node1->next (because it reads the old Tail at the
38 very beginning), then loads the Tail agian (w4), it can actully reads an old
39 value. And this is a bug because if node 1 is again dequeued, then for T2 to
40 update node1->next, it can potentially contaminate the memory...
43 static void main_task(void *param)
46 int pid = *((int *)param);
49 } else if (pid % 4 == 1) {
51 succ1 = dequeue(queue, &idx1, &reclaimNode1);
53 //succ1 = dequeue(queue, &idx1, &reclaimNode1);
54 //enqueue(queue, 1, false, 2);
55 } else if (pid % 4 == 2) {
57 } else if (pid % 4 == 3) {
62 int user_main(int argc, char **argv)
66 unsigned int in_sum = 0, out_sum = 0;
68 queue = calloc(1, sizeof(*queue));
72 threads = malloc(num_threads * sizeof(thrd_t));
73 param = malloc(num_threads * sizeof(*param));
74 input = calloc(num_threads, sizeof(*input));
75 output = calloc(num_threads, sizeof(*output));
77 atomic_init(&x[0], 0);
78 atomic_init(&x[1], 0);
79 atomic_init(&x[2], 0);
80 init_queue(queue, num_threads);
81 for (i = 0; i < num_threads; i++) {
83 thrd_create(&threads[i], main_task, ¶m[i]);
85 for (i = 0; i < num_threads; i++)
86 thrd_join(threads[i]);
88 for (i = 0; i < num_threads; i++) {
92 for (i = 0; i < num_threads; i++)
93 printf("input[%d] = %u\n", i, input[i]);
94 for (i = 0; i < num_threads; i++)
95 printf("output[%d] = %u\n", i, output[i]);
97 MODEL_ASSERT(in_sum == out_sum);