Commit 087d2ffa authored by Glen Mével's avatar Glen Mével
Browse files

changes during meeting (excepted regarding linearizability)

parent 9918b04f
......@@ -10,7 +10,7 @@
The syntax of our idealized version \mocaml{} is presented
in~\fref{fig:syntax}. It is equipped with a standard call-by-value,
left-to-right evaluation. The parts of interest are the memory operations.
Their semantics have been described in our earlier paper~\citecosmo;
Their semantics have been described by~\citet{mevel-jourdan-pottier-20};
however, in the present paper,
each location stores an \emph{array} of values, whose cells act as independent
memory cells with respect to the memory model.
......
......@@ -13,7 +13,7 @@ For the purpose of the formalization, it is written in an idealized version of t
\input{lang}
\subsection{Presentation of the data stucture}
\subsection{Overview of the data stucture}
\label{sec:queue:impl:presentation}
\input{figure-queue-impl}
......@@ -49,12 +49,10 @@ meaning that the value it stores is irrelevant.%
%
In addition, for the concurrent queue operations to work properly, we must
remember for which rank each slot was last used.%
%
%% \footnote{%
%% Actually, we need not remember the full rank~\idx:
%% only the cycle, $\idx \div \capacity$, is needed.
%% }
% JH : j'ai viré ce commentaire, qui ne me semble pas apporter d'information intéressante pour la compréhension de l'implémentation. Et c'est un peu confusant dans le flot du texte.
\footnote{%
Actually, we need not remember the full rank~\idx:
only the cycle, $\idx \div \capacity$, is needed.
}
%
The status encodes this information in a single integer, as follows:
......@@ -197,37 +195,12 @@ $2(\tail+\capacity)$.
\subsection{Interactions between threads}
\label{sec:queue:impl:interactions}
%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
% 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.
% JH : tout à fait d'accord avec FP. Moi, j'enlèverais tout simplement
% 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, as long as there is enough lag between enqueuers and dequeuers of the same slot.
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.
Possible situations are:
A noteworthy feature of this implementation is that
most of the time, enqueuers and dequeuers 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}%
......@@ -243,7 +216,7 @@ Possible situations are:
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 is full;
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
......
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