The Durable Queue was slightly modified to ignore return value, and so the verifier does not look at this at all.
This bug will not explicitly CLFLUSH the value associated with the node. Within a single verification this bug was caught. The dumped information did show the location of the store.
The bug will not explicitly CLFLUSH the last->next value, making inconsistency possible. Within two verifications, this bug was caught due to the tail not being found while traversing the list.
This bug will not explicitly CLFLUSH the last->next value when a failed enqueue occurs, causing potential for inconsistency if successful thread gets preempted before it can flush it itself. This was not found even after 41600 verifications over the span of 5 minutes. Unfortunately, this is likely due to the specific interleavings required for this bug to come to light. A randomized/stochastic scheduler is required to better randomize the selection of threads, as currently a round-robin scheduler and unfair/biased scheduler is used; the former making this bug easier to be obscured, the latter being slow when stopping the application.
This bug will not explicitly CLFLUSH the last->next value when the queue tail has been detected as being outdated, causing potential for inconsistency if thread repairs the tail and then proceeds to modify the queue, resulting in a node missing in the queue. This requires a very specific interleaving, and so just like Bug #3, is not found.
This bug will not explicitly CLFLUSH the head after CAS'ing it forward. This results in an inconsistency where the head will refer to an outdated node that has already been reclaimed and can contain junk. This bug was found after 16 verifications; likely took longer due to undefined behavior.