-{
- int success = 0;
- unsigned int node;
- pointer tail;
- pointer next;
- pointer tmp;
-
- node = new_node();
- store_32(&q->nodes[node].value, val);
- tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
- set_ptr(&tmp, 0); // NULL
- atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
-
- while (!success) {
- tail = atomic_load_explicit(&q->tail, acquire);
- next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
- if (tail == atomic_load_explicit(&q->tail, relaxed)) {
-
- /* Check for uninitialized 'next' */
- MODEL_ASSERT(get_ptr(next) != POISON_IDX);
-
- if (get_ptr(next) == 0) { // == NULL
- pointer value = MAKE_POINTER(node, get_count(next) + 1);
- success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
- &next, value, release, release);
- }
- if (!success) {
- unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
- pointer value = MAKE_POINTER(ptr,
- get_count(tail) + 1);
- int commit_success = 0;
- commit_success = atomic_compare_exchange_strong_explicit(&q->tail,
- &tail, value, release, release);
- /**
- @Begin
- @Commit_point_define_check: __ATOMIC_RET__ == true
- @Label: Enqueue_Success_Point
- @End
- */
- thrd_yield();
- }
- }
- }
- atomic_compare_exchange_strong_explicit(&q->tail,
- &tail,
- MAKE_POINTER(node, get_count(tail) + 1),
- release, release);
-}
-
-
-/**
- @Begin
- @Interface_define: Dequeue
- @End
-*/
-unsigned int dequeue(queue_t *q)
-{
- unsigned int value;
- int success = 0;
- pointer head;
- pointer tail;
- pointer next;
-
- while (!success) {
- head = atomic_load_explicit(&q->head, acquire);
- tail = atomic_load_explicit(&q->tail, relaxed);
- next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
- if (atomic_load_explicit(&q->head, relaxed) == head) {
- if (get_ptr(head) == get_ptr(tail)) {
-
- /* Check for uninitialized 'next' */
- MODEL_ASSERT(get_ptr(next) != POISON_IDX);
-
- if (get_ptr(next) == 0) { // NULL
- return 0; // NULL
- }
- atomic_compare_exchange_strong_explicit(&q->tail,
- &tail,
- MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
- release, release);
- thrd_yield();
- } else {
- value = load_32(&q->nodes[get_ptr(next)].value);
- success = atomic_compare_exchange_strong_explicit(&q->head,
- &head,
- MAKE_POINTER(get_ptr(next), get_count(head) + 1),
- release, release);
- /**
- @Begin
- @Commit_point_define_check: __ATOMIC_RET__ == true
- @Label: Dequeue_Success_Point
- @End
- */
- if (!success)
- thrd_yield();
- }
- }
- }
- reclaim(get_ptr(head));
- return value;
-}