gistfile1.txt

Note that with Model 1 you can get away with no case distinction in calculating
the number of items by just doing (WritePos - ReadPos) & (SIZE - 1) in unsigned
arithmetic when SIZE is a power of two. 

The real strength of Model 2 is definitely in the simpler invariants and lack of
special cases. From now I'll do all my circular FIFOs this way.

You can retain some advantages of both approaches for a circular FIFO by adding
the invariant ReadPos <= WritePos < 2 * SIZE. Then you can do the modulo reduction
incrementally for a non-power-of-two SIZE and easily deal with empty queues: Enforce
the invariant with if (WritePos >= 2 * SIZE) { ReadPos -= SIZE; WritePos -= SIZE; } and
use Elem[WritePos >= SIZE ? WritePos - SIZE : WritePos] instead of Elem[WritePos % SIZE].
Otherwise the code should be the same as for Model 2.