Commit 7d705ec1 authored by Glen Mével's avatar Glen Mével
Browse files

clarify "offset" vs "rank", use k for ranks

parent 49ba9caf
......@@ -632,7 +632,7 @@
\newcommand{\status}{\ensuremath{s}}
\newcommand{\tail}{\ensuremath{t}}
\newcommand{\head}{\ensuremath{h}}
\newcommand{\idx}{\ensuremath{i}}
\newcommand{\idx}{\ensuremath{k}}
\newcommand{\nbelems}{\ensuremath{n}}
%\newcommand{\sview}{\view}
%\newcommand{\tview}{\ensuremath{\view_t}}
......
......@@ -12,26 +12,29 @@
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
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.
length~\capacity, \refstatuses and \refelements; at each offset (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 at offset ``$\idx \mmod
\capacity$'' of the buffer, which we denote as $\modcap\idx$.
since its creation. The item of rank~\idx\ is stored in the buffer at offset
``$\idx \mmod \capacity$'', which we denote as $\modcap\idx$.
% FP quand tu écris "the head", cela signifie "le contenu de la référence \refhead"?
% préciser (plus loin, il s'appelle $\head$); 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.
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, the \emph{tail} is the number of items that have been dequeued since
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.
Each cell in the buffer is in one of two states: either it is \emph{occupied},
% 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},
meaning that it stores some item of the queue; or it is \emph{available},
meaning that the value it stores is irrelevant.%
%
......@@ -96,7 +99,7 @@ happens-before relationship from a dequeuer to an enqueuer.
\subsubsection{Explanation of \tryenqueue and \trydequeue}
The function~\tryenqueue first reads the current value of the field~\refhead, getting
The function~\tryenqueue first reads the current value of the reference~\refhead, getting
a value~\head. We have seen that the new item 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$.
......
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