if (get_ptr(next) == 0) { // == NULL
pointer value = MAKE_POINTER(node, get_count(next) + 1);
+
+ // ***********************************
+ // Inference analysis results have two choices here, it either
+ // makes wildcard(6) acq_rel and wildcard(8) relaxed or
+ // wildcard(6) release and wildcard(8) acquire. The
+ // synchronization here is for enqueue() to dequeue(), and
+ // actually either synchronization options will work!!!
success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
&next, value, wildcard(6), wildcard(7)); // release & relaxed
}
if (!success) {
unsigned int ptr =
- get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, wildcard(8))); // acquire
+ get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, wildcard(8))); // acquire
pointer value = MAKE_POINTER(ptr,
get_count(tail) + 1);
atomic_compare_exchange_strong_explicit(&q->tail,
while (!success) {
head = atomic_load_explicit(&q->head, wildcard(13)); // acquire
- // FIXME: SCFence makes this acquire
+ // SCFence makes this acquire, and we actually need an acquire here!!!
tail = atomic_load_explicit(&q->tail, wildcard(14)); // relaxed
next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, wildcard(15)); // acquire
if (atomic_load_explicit(&q->head, wildcard(16)) == head) { // relaxed
} else {
//value = load_32(&q->nodes[get_ptr(next)].value);
value = q->nodes[get_ptr(next)].value;
- // FIXME: SCFence makes this relaxed
success = atomic_compare_exchange_strong_explicit(&q->head,
&head, MAKE_POINTER(get_ptr(next), get_count(head) + 1),
wildcard(19), wildcard(20)); // release & relaxed