It did not see the proof of the correctness of circular buffers? one consumer, one producer, parallel execution, 2 atomic pointers, one read pointer, one write pointer and the cycle bits.