Finally, tying everything together, Prod(q) and Cons(q)
assert bounded knowledge about the states of the PP and
CP protocols, thus enforcing the fundamental invariant of
circular buffers:
The absolute writer index is at least 0 and less than N cells ahead of the absolute reader index.
Now, the reader (of this paper, not the buffer) may rightly
wonder: how can this fundamental invariant possibly be
enforced in the weak memory setting, given that it concerns the states of two separate cells being updated by different threads? The answer is that, although neither the producer nor the consumer can fully assume or maintain this invariant themselves, they are each able to enforce a piece of it sufficient to verify their own correctness. In particular, the
consumer controls the progress of the reader index, and can therefore assume and maintain the invariant that the reader index never overtakes the writer index (the “at least 0” part), while the producer controls the progress of the writer index, and can therefore assume and maintain the invariant that the writer index never leaves the reader index more than N − 1 cells behind (the “less than N ” part). Together, these piecemeal enforcements of the fundamental invariant are enough to perform the full verification.
