input[0] = 17;
//enqueue(queue, input[0]);
enqueue(queue, input[0]);
- output[0] = dequeue(queue);
+ //output[0] = dequeue(queue);
} else {
input[1] = 37;
- enqueue(queue, input[1]);
+ //enqueue(queue, input[1]);
//output[1] = dequeue(queue);
//output[0] = dequeue(queue);
- output[0] = dequeue(queue);
+ bool succ = dequeue(queue, &output[0]);
}
}
@Interface_define: Dequeue
@End
*/
-unsigned int dequeue(queue_t *q)
+bool dequeue(queue_t *q, unsigned int *retVal)
{
unsigned int value;
int success = 0;
while (!success) {
/**** detected correctness error ****/
head = atomic_load_explicit(&q->head, acquire);
+ // FIXME: This must be acquire otherwise we have a bug with 1 enqueue &
+ // 1 dequeue
tail = atomic_load_explicit(&q->tail, relaxed);
/****FIXME: miss ****/
next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
@Label: Dequeue_Empty_Point
@End
*/
- return 0; // NULL
+ return false; // NULL
}
/****FIXME: miss (not reached) ****/
// Second release can be just relaxed
//printf("miss4_dequeue\n");
thrd_yield();
} else {
- value = load_32(&q->nodes[get_ptr(next)].value);
+ *retVal = load_32(&q->nodes[get_ptr(next)].value);
//value = q->nodes[get_ptr(next)].value;
/****FIXME: correctness error ****/
// Seconde release can be just relaxed
}
}
reclaim(get_ptr(head));
- return value;
+ return true;
}
_Old_Val = 0;
}
@Post_check:
- _Old_Val == __RET__
+ _Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
@End
*/
-unsigned int dequeue(queue_t *q);
+bool dequeue(queue_t *q, unsigned int *retVal);
int get_thread_num();
#endif