&tail,
MAKE_POINTER(node, get_count(tail) + 1),
release, relaxed);
- /**
- //@Begin
- @Commit_point_define_check: succ
- @Label: Enqueue_UpdateOrLoad_Tail
- @End
- */
}
/**
*/
bool dequeue(queue_t *q, int *retVal)
{
- unsigned int value;
+ unsigned int value = 0;
int success = 0;
pointer head;
pointer tail;
@Label: Dequeue_Read_Head
@End
*/
+ /** A new bug has been found here!!! It should be acquire instead of
+ * relaxed (it introduces a bug when there's two dequeuers and one
+ * enqueuer)
+ */
tail = atomic_load_explicit(&q->tail, acquire);
/**
@Begin
//printf("miss4_dequeue\n");
thrd_yield();
} else {
- /**
- @Begin
- @Commit_point_define: true
- @Potential_commit_point_label: Dequeue_Potential_LoadNext
- @Label: Dequeue_LoadNext
- @End
- */
value = load_32(&q->nodes[get_ptr(next)].value);
- *retVal = value;
//value = q->nodes[get_ptr(next)].value;
/****FIXME: correctness error ****/
success = atomic_compare_exchange_strong_explicit(&q->head,
&head,
MAKE_POINTER(get_ptr(next), get_count(head) + 1),
release, relaxed);
+ /**
+ @Begin
+ @Commit_point_define: success
+ @Potential_commit_point_label: Dequeue_Potential_LoadNext
+ @Label: Dequeue_LoadNext
+ @End
+ */
if (!success)
thrd_yield();
}
}
}
reclaim(get_ptr(head));
+ *retVal = value;
return true;
}