Increase size of bootstrap bytes as some Linux distributions need more space.
[satcheck.git] / test / ms-queue-freelist.c
1 #include "threads.h"
2 #include <stdlib.h>
3 // #include "librace.h"
4 // #include "model-assert.h"
5
6 #include "ms-queue-freelist.h"
7 #include "libinterface.h"
8
9 #define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */
10 #define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */
11
12 #define POISON_IDX 0x666
13
14 static unsigned int (*free_lists)[MAX_FREELIST];
15
16 /* Search this thread's free list for a "new" node */
17 static unsigned int new_node()
18 {
19         int i;
20         int t = get_thread_num();
21         for (i = 0; i < MAX_FREELIST; i++) {
22                 unsigned int node = load_32(&free_lists[t][i]);
23                 if (node) {
24                         store_32(&free_lists[t][i], 0);
25                         return node;
26                 }
27         }
28         /* free_list is empty? */
29         // MODEL_ASSERT(0);
30         return 0;
31 }
32
33 /* Place this node index back on this thread's free list */
34 static void reclaim(unsigned int node)
35 {
36         int i;
37         int t = get_thread_num();
38
39         /* Don't reclaim NULL node */
40         // MODEL_ASSERT(node);
41
42         for (i = 0; i < MAX_FREELIST; i++) {
43                 /* Should never race with our own thread here */
44                 unsigned int idx = load_32(&free_lists[t][i]);
45
46                 /* Found empty spot in free list */
47                 if (idx == 0) {
48                         store_32(&free_lists[t][i], node);
49                         return;
50                 }
51         }
52         /* free list is full? */
53         // MODEL_ASSERT(0);
54 }
55
56 void init_queue(queue_t *q, int num_threads)
57 {
58         int i, j;
59
60         /* Initialize each thread's free list with INITIAL_FREE pointers */
61         /* The actual nodes are initialized with poison indexes */
62         free_lists = malloc(num_threads * sizeof(*free_lists));
63         for (i = 0; i < num_threads; i++) {
64                 for (j = 0; j < INITIAL_FREE; j++) {
65                         free_lists[i][j] = 2 + i * MAX_FREELIST + j;
66                         store_32(&q->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0));
67                 }
68         }
69
70         /* initialize queue */
71         store_32(&q->head, MAKE_POINTER(1, 0));
72         store_32(&q->tail, MAKE_POINTER(1, 0));
73         store_32(&q->nodes[1].next, MAKE_POINTER(0, 0));
74 }
75
76 void enqueue(queue_t *q, unsigned int val)
77 {
78         int success = 0;
79         unsigned int node;
80         pointer tail;
81         pointer next;
82         pointer tmp;
83
84         node = new_node();
85         store_32(&q->nodes[node].value, val);
86         tmp = load_32(&q->nodes[node].next);
87         // manually inlined macro: set_ptr(&tmp, 0); // NULL
88         tmp = (tmp & ~PTR_MASK);
89         store_32(&q->nodes[node].next, tmp);
90
91         while (!success) {
92                 pointer_t * qt = &q->tail;
93                 tail = load_32(qt);
94                 pointer_t * qn = &q->nodes[tail & PTR_MASK].next;
95                 next = load_32(qn);
96                 if (tail == load_32(&q->tail)) {
97
98                         /* Check for uninitialized 'next' */
99                         // MODEL_ASSERT(get_ptr(next) != POISON_IDX);
100
101                         if ((next & PTR_MASK) == 0) { // == NULL
102                                 pointer value = MAKE_POINTER(node, ((next & COUNT_MASK) >> 32) + 1);
103                                 success = rmw_32(CAS, &q->nodes[tail & PTR_MASK].next,
104                                                 (uint32_t)&next, value);
105                         }
106                         if (!success) {
107                                 unsigned int ptr = (load_32(&q->nodes[tail & PTR_MASK].next) & PTR_MASK);
108                                 pointer value = MAKE_POINTER(ptr,
109                                              ((tail & COUNT_MASK) >> 32) + 1);
110                                 rmw_32(CAS, &q->tail,
111                                                 (uint32_t)&tail, value);
112                                 thrd_yield();
113                         }
114                 }
115         }
116         rmw_32(CAS, &q->tail,
117                    (uint32_t)&tail,
118                    MAKE_POINTER(node, ((tail & COUNT_MASK) >> 32) + 1));
119 }
120
121 bool dequeue(queue_t *q, unsigned int *retVal)
122 {
123         int success = 0;
124         pointer head;
125         pointer tail;
126         pointer next;
127
128         while (!success) {
129                 head = load_32(&q->head);
130                 tail = load_32(&q->tail);
131                 next = load_32(&q->nodes[(head & PTR_MASK)].next);
132                 if (load_32(&q->head) == head) {
133                         if ((head & PTR_MASK) == (tail & PTR_MASK)) {
134
135                                 /* Check for uninitialized 'next' */
136                                 // MODEL_ASSERT(get_ptr(next) != POISON_IDX);
137
138                                 if (get_ptr(next) == 0) { // NULL
139                                         return false; // NULL
140                                 }
141                                 rmw_32(CAS, &q->tail,
142                                            (uint32_t)&tail,
143                                            MAKE_POINTER((next & PTR_MASK), ((tail & COUNT_MASK) >> 32) + 1));
144                                 thrd_yield();
145                         } else {
146                                 *retVal = load_32(&q->nodes[(next & PTR_MASK)].value);
147                                 success = rmw_32(CAS, &q->head,
148                                                                 (uint32_t)&head,
149                                             MAKE_POINTER((next & PTR_MASK), ((head & COUNT_MASK) >> 32) + 1));
150                                 if (!success)
151                                         thrd_yield();
152                         }
153                 }
154         }
155         reclaim((head & PTR_MASK));
156         return true;
157 }
158
159 /* ms-queue-main */
160 static int procs = 2;
161 static queue_t *queue;
162 static thrd_t *threads;
163 static unsigned int *input;
164 static unsigned int *output;
165 static int num_threads;
166
167 int get_thread_num()
168 {
169         thrd_t curr = thrd_current();
170         int i;
171         for (i = 0; i < num_threads; i++)
172                 if (curr.priv == threads[i].priv)
173                         return i;
174         /* MODEL_ASSERT(0); */
175         return -1;
176 }
177
178 bool succ1, succ2;
179
180 static void main_task(void *param)
181 {
182         unsigned int val;
183         int pid = *((int *)param);
184         if (!pid) {
185                 input[0] = 17;
186                 enqueue(queue, input[0]);
187                 succ1 = dequeue(queue, &output[0]);
188                 //printf("Dequeue: %d\n", output[0]);
189         } else {
190                 input[1] = 37;
191                 enqueue(queue, input[1]);
192                 succ2 = dequeue(queue, &output[1]);
193         }
194 }
195
196 int user_main(int argc, char **argv)
197 {
198         int i;
199         int *param;
200         unsigned int in_sum = 0, out_sum = 0;
201
202         queue = calloc(1, sizeof(*queue));
203         // MODEL_ASSERT(queue);
204
205         num_threads = procs;
206         threads = malloc(num_threads * sizeof(thrd_t));
207         param = malloc(num_threads * sizeof(*param));
208         input = calloc(num_threads, sizeof(*input));
209         output = calloc(num_threads, sizeof(*output));
210
211         init_queue(queue, num_threads);
212         for (i = 0; i < num_threads; i++) {
213                 param[i] = i;
214                 thrd_create(&threads[i], main_task, &param[i]);
215         }
216         for (i = 0; i < num_threads; i++)
217                 thrd_join(threads[i]);
218
219         for (i = 0; i < num_threads; i++) {
220                 in_sum += input[i];
221                 out_sum += output[i];
222         }
223         for (i = 0; i < num_threads; i++)
224                 printf("input[%d] = %u\n", i, input[i]);
225         for (i = 0; i < num_threads; i++)
226                 printf("output[%d] = %u\n", i, output[i]);
227         /* if (succ1 && succ2) */
228         /*      MODEL_ASSERT(in_sum == out_sum); */
229         /* else */
230         /*      MODEL_ASSERT (false); */
231
232         free(param);
233         free(threads);
234         free(queue);
235
236         return 0;
237 }