5 #include "model-assert.h"
8 typedef unsigned long long pointer;
9 typedef atomic_ullong pointer_t;
11 #define MAKE_POINTER(ptr, count) ((((pointer)count) << 32) | ptr)
12 #define PTR_MASK 0xffffffffLL
13 #define COUNT_MASK (0xffffffffLL << 32)
15 static inline void set_count(pointer *p, unsigned int val) { *p = (*p & ~COUNT_MASK) | ((pointer)val << 32); }
16 static inline void set_ptr(pointer *p, unsigned int val) { *p = (*p & ~PTR_MASK) | val; }
17 static inline unsigned int get_count(pointer p) { return (p & COUNT_MASK) >> 32; }
18 static inline unsigned int get_ptr(pointer p) { return p & PTR_MASK; }
28 node_t nodes[MAX_NODES + 1];
31 void init_queue(queue_t *q, int num_threads);
39 typedef struct tag_elem {
45 list<tag_elem_t> __queue;
48 __queue = list<tag_elem_t>();
49 tag = 1; // Beginning of available id
51 # Only check the happens-before relationship according to the id of the
52 # commit_point_set. For commit_point_set that has same ID, A -> B means
53 # B happens after the previous A.
62 #define relaxed memory_order_relaxed
63 #define release memory_order_release
64 #define acquire memory_order_acquire
66 #define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */
67 #define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */
69 #define POISON_IDX 0x666
71 static unsigned int (*free_lists)[MAX_FREELIST];
73 /* Search this thread's free list for a "new" node */
74 static unsigned int new_node()
77 int t = get_thread_num();
78 for (i = 0; i < MAX_FREELIST; i++) {
79 unsigned int node = load_32(&free_lists[t][i]);
81 store_32(&free_lists[t][i], 0);
85 /* free_list is empty? */
90 /* Place this node index back on this thread's free list */
91 static void reclaim(unsigned int node)
94 int t = get_thread_num();
96 /* Don't reclaim NULL node */
99 for (i = 0; i < MAX_FREELIST; i++) {
100 /* Should never race with our own thread here */
101 unsigned int idx = load_32(&free_lists[t][i]);
103 /* Found empty spot in free list */
105 store_32(&free_lists[t][i], node);
109 /* free list is full? */
113 void init_queue(queue_t *q, int num_threads)
123 /* Initialize each thread's free list with INITIAL_FREE pointers */
124 /* The actual nodes are initialized with poison indexes */
125 free_lists = (unsigned int**) malloc(num_threads * sizeof(*free_lists));
126 for (i = 0; i < num_threads; i++) {
127 for (j = 0; j < INITIAL_FREE; j++) {
128 free_lists[i][j] = 2 + i * MAX_FREELIST + j;
129 atomic_init(&q->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0));
133 /* initialize queue */
134 atomic_init(&q->head, MAKE_POINTER(1, 0));
135 atomic_init(&q->tail, MAKE_POINTER(1, 0));
136 atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0));
142 @Commit_point_set: Enqueue_Success_Point
145 # __ID__ is an internal macro that refers to the id of the current
150 __queue.push_back(elem);
153 void enqueue(queue_t *q, unsigned int val)
162 store_32(&q->nodes[node].value, val);
163 tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
164 set_ptr(&tmp, 0); // NULL
165 atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
168 tail = atomic_load_explicit(&q->tail, acquire);
169 next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
170 if (tail == atomic_load_explicit(&q->tail, relaxed)) {
172 /* Check for uninitialized 'next' */
173 MODEL_ASSERT(get_ptr(next) != POISON_IDX);
175 if (get_ptr(next) == 0) { // == NULL
176 pointer value = MAKE_POINTER(node, get_count(next) + 1);
177 success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
178 &next, value, release, release);
181 unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
182 pointer value = MAKE_POINTER(ptr,
183 get_count(tail) + 1);
184 int commit_success = 0;
185 commit_success = atomic_compare_exchange_strong_explicit(&q->tail,
186 &tail, value, release, release);
189 @Commit_point_define_check: commit_success == true
190 @Label: Enqueue_Success_Point
197 atomic_compare_exchange_strong_explicit(&q->tail,
199 MAKE_POINTER(node, get_count(tail) + 1),
206 @Commit_point_set: Dequeue_Success_Point
207 @ID: __queue.back().id
209 unsigned int _Old_Val = __queue.front().data;
215 unsigned int dequeue(queue_t *q)
224 head = atomic_load_explicit(&q->head, acquire);
225 tail = atomic_load_explicit(&q->tail, relaxed);
226 next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
227 if (atomic_load_explicit(&q->head, relaxed) == head) {
228 if (get_ptr(head) == get_ptr(tail)) {
230 /* Check for uninitialized 'next' */
231 MODEL_ASSERT(get_ptr(next) != POISON_IDX);
233 if (get_ptr(next) == 0) { // NULL
236 atomic_compare_exchange_strong_explicit(&q->tail,
238 MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
242 value = load_32(&q->nodes[get_ptr(next)].value);
243 success = atomic_compare_exchange_strong_explicit(&q->head,
245 MAKE_POINTER(get_ptr(next), get_count(head) + 1),
249 @Commit_point_define_check: success == true
250 @Label: Dequeue_Success_Point
258 reclaim(get_ptr(head));
268 #include "my_queue.h"
269 #include "model-assert.h"
271 static int procs = 2;
272 static queue_t *queue;
273 static thrd_t *threads;
274 static unsigned int *input;
275 static unsigned int *output;
276 static int num_threads;
280 thrd_t curr = thrd_current();
282 for (i = 0; i < num_threads; i++)
283 if (curr.priv == threads[i].priv)
289 static void main_task(void *param)
292 int pid = *((int *)param);
296 enqueue(queue, input[0]);
297 output[0] = dequeue(queue);
300 enqueue(queue, input[1]);
301 output[1] = dequeue(queue);
305 int user_main(int argc, char **argv)
309 unsigned int in_sum = 0, out_sum = 0;
311 queue = (queue_t*) calloc(1, sizeof(*queue));
315 threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t));
316 param = (int*) malloc(num_threads * sizeof(*param));
317 input = (unsigned int*) calloc(num_threads, sizeof(*input));
318 output = (unsigned int*) calloc(num_threads, sizeof(*output));
320 init_queue(queue, num_threads);
321 for (i = 0; i < num_threads; i++) {
323 thrd_create(&threads[i], main_task, ¶m[i]);
325 for (i = 0; i < num_threads; i++)
326 thrd_join(threads[i]);
328 for (i = 0; i < num_threads; i++) {
330 out_sum += output[i];
332 for (i = 0; i < num_threads; i++)
333 printf("input[%d] = %u\n", i, input[i]);
334 for (i = 0; i < num_threads; i++)
335 printf("output[%d] = %u\n", i, output[i]);
336 MODEL_ASSERT(in_sum == out_sum);