1 post with tag stacked-borrows

• rust
• unsafe-rust
• miri
• stacked-borrows
• tree-borrows
• aliasing
• undefined-behavior
• data-race
• lock-free
• spsc-queue
• ring-buffer
• testing

How Miri found a data race in a lock-free ring buffer that the compiler had no way to see

A lock-free MPSC ring buffer passed its test suite, a Quint model check, loom, and cargo miri test - and was still undefined behaviour. A silent Deref widened every buffer reference to span the whole allocation, and a retag counts as an access.