Commit 5b9bc76a authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Small English fixes, and comments.

parent d260f4ba
......@@ -11,16 +11,18 @@
Let~$\capacity \geq 1$ be a fixed integer. \fref{fig:queue:impl} shows an
implementation of a concurrent queue in \mocaml{} using a circular buffer of
fixed capacity~\capacity. The buffer is represented by two arrays of the same
fixed capacity~\capacity. The buffer is represented by two arrays of
length~\capacity, \refstatuses and \refelements; each offset of 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
fields, \refhead and \reftail.
Items will be identified by their \emph{rank} (starting at zero) in the queue
since its creation. The item of rank~\idx\ will be stored at offset $\idx \mmod
\capacity$ of the buffer, which from now on we will denote as $\modcap\idx$.
Items are identified by their \emph{rank} (starting at zero) in the queue
since its creation. The item of rank~\idx\ is stored at offset ``$\idx \mmod
\capacity$'' of the buffer, which we denote as $\modcap\idx$.
% FP quand tu écris "the head", cela signifie "le contenu de la référence \refhead"?
% préciser; idem pour tail
The \emph{head} is 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.
......@@ -29,40 +31,56 @@ Similarly, the \emph{tail} is the number of items that have been dequeued since
the creation of the queue.
In other words, it is the rank of the next item to be dequeued.
Each offset of the buffer is in one of two states: either it is \emph{occupied},
Each cell in the buffer is in one of two states: either it is \emph{occupied},
meaning that it stores some item of the queue; or it is \emph{available},
meaning that the value it stores is irrelevant (we use the unit value, $\Unit$,
for garbage collection concerns). In addition, the proper functioning of the
concurrent queue operations also requires to remember at which rank each offset
was last used. The status encodes these informations in a single integer, as
follows:
meaning that the value it stores is irrelevant (in that case, we store a unit
value $\Unit$ in that cell; indeed, keeping a stale pointer could cause a
space leak). In addition, for the concurrent queue operations to work
properly, we must remember at which rank each offset was last used. The status
encodes this information in a single integer, as follows:
\begin{itemize}%
\item a status worth $2\idx$ indicates that offset~$\modcap\idx$ is available
for storing the future item of rank~\idx;
\item an even status $2\idx$ indicates that offset~$\modcap\idx$ is available
for storing a future item of rank~\idx;
\item a status worth $2\idx+1$ indicates that offset~$\modcap\idx$ is occupied
for storing the item of rank~\idx.
\item an odd status $2\idx+1$ indicates that offset~$\modcap\idx$ is currently
occupied by the item of rank~\idx.
\end{itemize}%
(Actually, the status needs not encode the full rank~\idx, only the cycle,
$\idx \div \capacity$, is needed.)
% FP je pense qu'on peut supprimer cette remarque technique?
% (Actually, the status need not encode the full rank~\idx. Only the cycle,
% $\idx \div \capacity$, is needed.)
Function~\enqueue repeatedly calls \tryenqueue untils it succeeds. The latter
can fail either because the buffer is full or because of a race with another
enqueuer (we do not distinguish between the two events, but this is feasible).
The function~\enqueue repeatedly calls \tryenqueue until it succeeds.
\tryenqueue can fail either because the buffer is full or because of a race
with another enqueuer. (We currently do not distinguish between these two
causes, but this is feasible.)
Similarly, function~\dequeue repeatedly calls \trydequeue untils it succeeds.
The latter can fail either because the buffer is empty or because of a race with
another dequeuer (we do not distinguish between the two events, but this is
feasible).
Similarly, \dequeue repeatedly calls \trydequeue untils it succeeds.
\trydequeue can fail either because the buffer is empty or because of a race
with another dequeuer. (Again, we currently do not distinguish between these
two causes, but this is feasible).
A noteworthy feature of this implementation is that the head and tail are
independent of each other, so that enqueuers and dequeuers never race against.
This is why the data structure does not guarantee any happens-before
relationship from a dequeuer to an enqueuer.
independent of each other, so that an enqueuer and a dequeuer never race
against each other. This is why the data structure does not guarantee any
happens-before relationship from a dequeuer to an enqueuer.
% FP ce dernier paragraphe n'est pas clair. Si je comprends bien, ce design
% est choisi pour éliminer (une grande partie de) la contention entre
% enqueuers et dequeuers; les uns font CAS sur head, les autres sur tail, donc
% pas de race possible entre les uns et les autres. Il reste tout de même
% qu'un enqueuer et un dequeuer peuvent être dans une race sur une case du
% tableau statuses, je crois. (Seulement quand la file est vide ou pleine?) Ce
% serait à clarifier. Enfin, ce qui n'est pas clair dans le paragraphe
% ci-dessus, c'est qu'on passe d'un fait symétrique (an enqueuer and a
% dequeuer never race against each other) à un fait dissymétrique (no
% happens-before relationship from a dequeuer to an enqueuer). Naïvement, on
% devrait aussi avoir la conclusion symétrique (no happens-before relationship
% from an enqueuer to a dequeuer); or ce n'est pas vrai, donc il faut
% clarifier l'argument.
\subsubsection{Explanation of \tryenqueue and \trydequeue}
......
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