Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 38944cdb authored by Glen Mével's avatar Glen Mével
Browse files

ICFP21 paper: shorten the section about contention (because off-topic)

parent 036451a2
......@@ -8,7 +8,7 @@
We now present an implementation of a bounded MPMC queue, that satisfies the specification devised in~\sref{sec:queue:spec}.
For the purpose of the formalization, it is written in an idealized version of the \mocaml{} language which we introduce in~\sref{sec:lang},
before showing the code~(\sref{sec:queue:impl:presentation},~\sref{sec:queue:impl:code})
and giving intuitions about its mode of operation~(\sref{sec:queue:impl:invariants},~\sref{sec:queue:impl:interactions}).
and giving intuitions about its mode of operation~(\sref{sec:queue:impl:invariants},~\sref{sec:queue:impl:contention}).
\input{lang}
......@@ -25,9 +25,9 @@ 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
Items are identified by their \emph{rank} (starting at zero) of insertion in the queue
since its creation. The item of rank~\idx\ is stored in slot
``$\idx \mmod \capacity$'', which we denote as $\modcap\idx$.
``$\idx \mmod \capacity$'', which from now on 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.
......@@ -69,7 +69,9 @@ Let~\head\ and~\tail\ be the value of references \refhead and \reftail,
respectively.
%
At any time, the ranks of items that are stored in the queue---or in the process of being stored---%
range from~\tail\ included to~\head\ excluded. Thus, an invariant
range from~\tail\ included to~\head\ excluded,
and there cannot be more than \capacity\ such items.
Thus, an invariant
property of the queue is:
%
\[
......@@ -191,69 +193,20 @@ still $2\head$ when we overwrite it with $2\head+1$.
Symmetrically, the status is still $2\tail+1$ when a dequeuer overwrites it with
$2(\tail+\capacity)$.
\subsection{Interactions between threads}
\label{sec:queue:impl:interactions}
\subsection{Notes on contention in the queue}
\label{sec:queue:impl:contention}
A noteworthy feature of this implementation is that
most of the time, enqueuers and dequeuers operate on separate references:
it tries to limit competition between enqueuers and dequeuers.
Indeed, enqueuers and dequeuers generally operate on separate references:
enqueuers never access \reftail and dequeuers never access \refhead.
If we are unlucky, they can still interfere on a slot;
%this only happens when the queue appears empty, or appears full.
however, this should be rare. This occurs only in the following situations:
\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 enqueuer continues unaffected,
and the candidate dequeuer fails because the buffer appears empty;
\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 dequeuer continues unaffected,
and the candidate enqueuer fails because the buffer appears full;
\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
competition with that other enqueuer;
\item symmetrically, an 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 competition with that other dequeuer.
\end{itemize}%
Hence in favorable situations%
---when the buffer is neither empty nor full---%
there are no enqueuer-dequeuer competitions
beyond ones between an enqueuer and a dequeuer of the same rank.
A weakness of this implementation, however, is that it is not non-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 fails.
% TODO : citer la thèse de Keir Fraser
%
%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
%dequeue the corresponding item, hence the tail will remain blocked at rank~\idx\
%and the head will remain blocked at $\idx+\capacity$ (the queue will remain
%full forever).
%
%Symmetrically, if a dequeuer halts after it has been attributed a rank~\idx\ but
%before it updates the corresponding slot, then no enqueuer will be able to reuse
%the slot for an item of rank~$\idx+\capacity$, hence the head will remain
%blocked at rank~$\idx+\capacity$ and the tail will remain blocked at
%$\idx+\capacity$ (the queue will remain empty forever).
Markdown is supported
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