Commit 2a53c3d2 authored by Glen Mével's avatar Glen Mével
Browse files

rework section about impl

  - "offset" --> "slot"
  - "race" --> "competition" (there are no data races per se, as implied
    locations are atomic)
  - clarify thread interference
  - clarify explanation of try_enqueue
parent a0820485
......@@ -41,19 +41,19 @@ enqueuing will either block or fail.
\fref{fig:queue:impl} shows the
implementation of the bounded MRMW queue in our \mocaml{} fragment. It uses a circular buffer of
fixed capacity~$\capacity \geq 1$. The buffer is represented by two arrays of
length~\capacity, \refstatuses and \refelements; at each offset (from~$0$
length~\capacity, \refstatuses and \refelements; in each slot (whose offset ranges from~$0$
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.
Items are identified by their \emph{rank} (starting at zero) in the queue
since its creation. The item of rank~\idx\ is stored in the buffer at offset
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.
%
Similarly, \reftail stores 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.
......@@ -61,19 +61,20 @@ In other words, it is the rank of the next item to be dequeued.
% GLEN: j’écris "each offset" et non "each cell" car on a en fait deux tableaux,
% donc deux "cells" au sens du langage de programmation.
% Je prends soin de distinguer ces termes:
% - "offset" (indice relatif au buffer, donc entre 0 et \capacity);
% - "rank" (indice depuis la création de la queue, donc entre 0 et \head).
Each buffer offset is in one of two states: either it is \emph{occupied},
% - "offset" (indice d’un "slot", relatif au buffer, donc entre 0 et \capacity);
% - "rank" (indice d’un "item" depuis la création de la queue, donc entre 0 et \head).
Each slot 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.%
%
\footnote{\label{fn:memleak}%
In that case, we store a unit value $\Unit$ in that cell; indeed, keeping
a stale pointer could cause a memory leak.
Technically, the slot stores a unit value~$\Unit$; indeed, keeping a stale
pointer could cause a memory leak.
}
%
In addition, for the concurrent queue operations to work properly, we must
remember at which rank each offset was last used.%
remember for which rank each slot was last used.%
%
\footnote{%
% FP je pense qu'on peut supprimer cette remarque technique?
% Glen: je la passe en footnote.
......@@ -85,31 +86,51 @@ The status encodes this information in a single integer, as follows:
\begin{itemize}%
\item an even status $2\idx$ indicates that offset~$\modcap\idx$ is available
\item an even status $2\idx$ indicates that slot~$\modcap\idx$ is available
for storing a future item of rank~\idx;
\item an odd status $2\idx+1$ indicates that offset~$\modcap\idx$ is currently
\item an odd status $2\idx+1$ indicates that slot~$\modcap\idx$ is currently
occupied by the item of rank~\idx.
\end{itemize}%
Let~\head\ and~\tail\ be the value of references \refhead and \reftail,
respectively. We say that the buffer is \emph{full} when slot~$\modcap\head$ has
a status less than $2\head$; in other words, the next slot at which to enqueue
is still in use for a rank less than~\head\
%
(in fact, either the slot has status $2(\head-\capacity)$ and some thread
is in the process of enqueuing the item of rank~$\head-\capacity$,
or it has status $2(\head-\capacity)+1$ and is occupied by that item).
%
This implies that $\head = \tail+\capacity$.
We say that the buffer is \emph{empty} when slot~$\modcap\tail$ has a status
less than $2\tail+1$; in other words, the next slot from which to dequeue is
still in use for a rank less than~\tail\
%
(in fact, either the slot has status $2(\tail-\capacity)+1$ and some thread
is in the process of dequeuing the item of rank~$\tail-\capacity$,
or it has status $2\tail$ and is available for a future item of rank~\tail).
%
This implies that $\head = \tail$.
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.%
the latter can fail either because the buffer is full or because of a competing enqueuer.%
%
\footnote{\label{fn:distinguishfail}%
We currently do not distinguish between these two causes, 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.%
the latter can fail either because the buffer is empty or because of a competing dequeuer.%
%
\footref{fn:distinguishfail}
A noteworthy feature of this implementation is that the head and tail are
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.
%A noteworthy feature of this implementation is that the head and tail are
%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
......@@ -129,45 +150,102 @@ happens-before relationship from a dequeuer to an enqueuer.
% ce paragraphe. Ça me semble un peu faux, et pas à sa place ici
% (puisqu'on a pas encore présenté la spec).
% GLEN: un meilleur texte, j’espère (peut-être inutile et trop long):
A noteworthy feature of this implementation is that it avoids competition
between enqueuers and dequeuers. They operate on separate references: enqueuers
never access \reftail and dequeuers never access \refhead.
%
It can happen that an enqueuer and a dequeuer operate concurrently on a same
slot, but arguably they are not ``competing''. % ``interfering''
Possible situations are:
\begin{itemize}%
\item a candidate dequeuer checking whether the item of rank~\tail\ is ready
to be dequeued from slot~$\modcap\tail$ while the corresponding enqueuer is
not done yet;
%
%in that case the candidate dequeuer does not interfere with the enqueuer,
in that case the enqueuer continues unaffected,
%and the candidate dequeuer fails because of the enqueuer being too slow,
and the candidate dequeuer fails because the buffer is empty
(it would fail just as well if there was no enqueuer at all);
\item symmetrically, a candidate enqueuer checking whether slot~$\modcap\head$
is available for storing an item of rank~\head\ while a dequeuer is still in
the process of dequeuing the item of rank~$\head-\capacity$;
%
%in that case the candidate enqueuer does not interfere with the dequeuer,
in that case the dequeuer continues unaffected,
%and the candidate enqueuer fails because of the dequeuer being too slow,
and the candidate enqueuer fails because the buffer is full
(it would fail just as well if there was no dequeuer at all);
\item a dequeuer dequeuing the item of rank~$\idx + r\capacity$
(with $r \geq 0$) while a candidate enqueuer is still checking whether
slot~$\modcap\idx$ is available for storing an item of rank~\idx;
%
in that case, the dequeuer continues unaffected;
the candidate enqueuer fails, but the existence of a dequeuer for a rank at
least \idx\ implies that another enqueuer has been attributed rank~\idx\
before the candidate enqueuer, hence we can connect its failure to the
competition with that other enqueuer;
\item symmetrically, a enqueuer enqueuing an item of rank~$\idx + r\capacity$
(with $r \geq 1$) while a candidate dequeuer is still checking whether
the item of rank~\idx\ is ready to be dequeued from slot~$\modcap\idx$;
%
in that case, the enqueuer continues unaffected;
the candidate dequeuer fails, but the existence of a enqueuer for a rank at
least $\idx+\capacity$ implies that another dequeuer has been attributed
rank~\idx\ before the candidate dequeuer, hence we can connect its failure
to the competition with that other dequeuer;
\end{itemize}%
\subsubsection{Explanation of \tryenqueue and \trydequeue}
The function~\tryenqueue first reads the current value of the reference~\refhead, getting
a value~\head. We have seen that the item to insert should have rank~\head. To check
that offset~$\modcap\head$ is indeed available for rank~\head, the function
reads its status: it should be equal to~$2\head$.
%
If it is not, we fail (a status less than~$2\head$ indicates that the cell is
still used for an earlier rank: that is, the buffer is full; a status greater
than~$2\head$ indicates that the offset has been filled and possibly emptied,
possibly several times, since we read \refhead: that is, we have lost
a race against other enqueuers).
If the status is $2\head$, then we try to acquire rank~\head.
%
``Acquiring'' rank~\head\ means successfully incrementing
the atomic counter~\refhead from~\head\ to $\head+1$, using
a compare-and-set operation. If this operation fails, then again we have lost a race against
other enqueuers, so the function fails. If it succeeds, we now have unique
control of offset~$\modcap\head$, and we know that its status has not changed.
% FP: au début tu parles d'acquérir un rang,
% mais ensuite tu parles de contrôle unique d'un offset.
% il faudrait sans doute clarifier le lien entre posséder un rang
% et posséder un offset. Les deux vont ensemble je suppose?
%
% TODO: vague:
Indeed, enqueuing an item with rank~\head\ is the only way to change it.
%
Hence the offset is still available, and we can fill it with the new item, and
update the status accordingly. Notice that, under weak memory, the order of
these two writes matters: the atomic write to \refstatuses must propagate the
information that the
nonatomic write to \refelements has taken place. Thus, a thread which dequeues this item
(after reading its status) is certain to read a correct value from the array \refelements.
This is a typical release/acquire idiom.
When calling \tryenqueue, we start by reading the current value~\head\ of the
reference~\refhead. To check that slot~$\modcap\head$ is available for
rank~\head, we read its status.
%
If it differs from~$2\head$, we fail
%
(a status less than~$2\head$ indicates that the buffer is full;
%a status greater than~$2\head$ indicates that the slot has been filled, then
%possibly emptied, possibly several times, since we read \refhead: that is, we
%have lost a race against other enqueuers).
a status greater than~$2\head$ indicates that someone has increased the status
since we read \refhead, and as explained further on, only an enqueuer that has
been attributed rank~\head\ before we have is permitted to do so).
If the status is $2\head$, then we try to increment the atomic counter~\refhead
from~\head\ to~$\head+1$, using a compare-and-set operation.
%
Note that this is the only place in the implementation where \refhead is modified,
hence that counter is monotonic.
%
If the CAS fails, it is again because of a competing enqueuer;
in that case, we fail.
If the CAS succeeds, then no other enqueuer can successfully perform the same
increment, so we can regard this achievement as attributing us rank~\head, and
giving us an unique permission to write an item into slot~$\modcap\head$.
No one else has got that permission since we initially read \refhead,
so this slot’s status has not changed: it is still available.
%
We write the new item, then update the status accordingly.
Notice that, under weak memory, the order of these two writes matters: the
atomic write to \refstatuses must propagate the information that the nonatomic
write to \refelements has taken place. Thus, a thread which dequeues this item
(after reading its status) is certain to read a correct value from the array
\refelements. This is a typical release/acquire idiom.
% TODO : JH : Ok, mais c'est aussi nécessaire dasn un modèle SC, puisque l'écriture du statut correspond au relacheemnt du lock : si on s'amusait à remplir la cellule après écrire dasn statut, alors le dequeuer pourrait commencer à lire le contenu de la cellule avant que celle-ci ait été remplie, non ? Pour moi, c'est une meilleure justification pour l'odre des opérations. Les questions de mémoire faible sont plus subtiles et nécessitent d'avoir compris un peu la spec.
Function~\trydequeue works analogously.%
The function~\trydequeue works analogously.%
%
\footnote{%
Overwriting the extracted value with a unit value~$\Unit$ is unnecessary for
......
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