Start with , , and immutable labels. Perform
enqueue(A), enqueue(B), dequeue(), enqueue(C), enqueue(D), dequeue(), enqueue(E), enqueue(F), enqueue(G). The removals return and . The interleaved insertions and removals make the front advance before the array fills; slot reuse does not require waiting for the FIFO queue to become empty.
An interleaved capacity-five FIFO queue trace branches at a full insertion
. The table follows completed sequential calls. At step 10, rejecting retains ; overwriting accepts and discards . Step 11 therefore returns different labels. The lower bars show membership lifetimes for and at operation boundaries, not elapsed times or programming-language object lifetimes. Details.
At step 7, occupies physical slot and the next-write array index wraps to . At step 8, reuses slot , giving the physical layout in the preceding diagram. At step 9, replaces the stale contents of slot : the physical array is but the logical sequence is . Now , yet makes the state full rather than empty.
The displayed values are related by after every call. They are shown together to explain the invariant; an implementation need store only two. For the rejecting FIFO queue, every successful removal returns the earliest accepted label not already removed. The representation independence example supplies the general proof through its abstraction function; this trace makes the wrapped physical storage visible.
Articles by others on the same topic
There are currently no matching articles.