Commit 9ac3aa9d authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Comments.

parent a606ece2
......@@ -30,7 +30,7 @@ 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
faster than they are dequeued; in this situation, a bounded queue has no risk of
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.
% TODO: ref for bounded pools/queues: Herlihy & Shavit 10.1
......@@ -39,7 +39,7 @@ enqueuing will either block or fail.
% ref: https://github.com/rigtorp/MPMCQueue
\fref{fig:queue:impl} shows the
implementation of the bounded MRMW queue in \mocaml{}. It uses a circular buffer of
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$
included to~$\capacity$ excluded), the buffer thus stores a \emph{status} in an
......@@ -69,7 +69,7 @@ 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 space leak.
a stale pointer could cause a memory leak.
}
%
In addition, for the concurrent queue operations to work properly, we must
......@@ -93,15 +93,14 @@ The status encodes this information in a single integer, as follows:
\end{itemize}%
The function~\enqueue repeatedly calls \tryenqueue until it succeeds.
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.%
%
\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.
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.%
%
......@@ -126,6 +125,10 @@ happens-before relationship from a dequeuer to an enqueuer.
% 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).
\subsubsection{Explanation of \tryenqueue and \trydequeue}
The function~\tryenqueue first reads the current value of the reference~\refhead, getting
......@@ -162,10 +165,12 @@ nonatomic write to \refelements has taken place. Thus, a thread which dequeues t
(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.%
%
\footnote{%
Overwriting the extracted value with a unit value~$\Unit$ is unnecessary for
functional correctness but, as mentioned in~\fnref{fn:memleak}, it prevents
space leaks.
memory leaks.
}
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