Commit 6f4b0989 authored by Glen Mével's avatar Glen Mével
Browse files

avoid futur tense when possible

parent cff7d97b
......@@ -31,8 +31,8 @@ enqueue and dequeue.
In addition, this queue is \emph{bounded}, that is, it occupies no more than a
fixed memory size. A motivation for that trait is that items may be enqueued
more frequently than they are dequeued; in this situation, a bounded queue has no risk of
exhausting system memory; instead, if the maximum size has been reached,
enqueuing will either block or fail.
exhausting system memory; instead, if the maximum size is reached,
enqueuing either blocks or fails.
% TODO: ref for bounded pools/queues: Herlihy & Shavit 10.1
% TODO: find where this implementation was first described
......@@ -46,13 +46,17 @@ included to~$\capacity$ excluded), the buffer thus stores a \emph{status} in an
atomic field and an \emph{item} in a nonatomic field. The data~structure also
has two integers stored in atomic references, \refhead and \reftail.
We know give an intuition as to how the code operates and why it is correct. We
state some properties, but the full proof of them being invariant is deferred
until~\sref{sec:queue:proof}.
Items are identified by their \emph{rank} (starting at zero) in the queue
since its creation. The item of rank~\idx\ is stored in slot
``$\idx \mmod \capacity$'', which we denote as $\modcap\idx$.
%
The reference~\refhead stores the number of items that have been enqueued since
the creation of the queue, including those that have since been dequeued.
In other words, it is the rank of the next item that will be enqueued.
In other words, it is the rank of the next item to be enqueued.
%
Similarly, \reftail stores the number of items that have been dequeued since
the creation of the queue.
......@@ -98,8 +102,7 @@ Let~\head\ and~\tail\ be the value of references \refhead and \reftail,
respectively.
%
At any time, the ranks of items that are stored (or in the process of being stored)
in the queue range from~\tail\ included to~\head\ excluded. As will be verified
when we will be proving the correctness of the implementation, an invariant
in the queue range from~\tail\ included to~\head\ excluded. An invariant
property of the queue is:
%
\[
......@@ -184,7 +187,7 @@ to~$\head+1$.
If the CAS fails, we fail (it is again because of a competing enqueuer).
If the CAS succeeds, then we are attributed rank~\head\ and can proceed to
inserting an item into slot~$\modcap\head$. As explained early, its status has
inserting an item into slot~$\modcap\head$. As explained earlier, its status has
not changed since we read it: the slot is still available.
%
We write the new item, then we update the status accordingly. This update must
......@@ -296,7 +299,7 @@ Hence competition happens only between enqueuers, or between dequeuers.
A weakness of this implementation, however, is that it is blocking:
if an enqueuer or a dequeuer halts after it has been attributed a rank but before
it updates the corresponding slot, then after some time, any other thread trying
to enqueue or dequeue will fail.
to enqueue or dequeue fails.
%
%Specifically, if an enqueuer halts after it has been attributed a rank~\idx\ but
%before it updates the corresponding slot, then no dequeuer will be able to
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment