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

Merge branch 'arrays' of gitlab.inria.fr:gmevel/cosmo into arrays

parents 3943533c 0e325b5b
......@@ -42,5 +42,8 @@ $\CAS\loc{\val_1}{\val_2}$ performs compare-and-set at offset~zero.
% JH : TODO :
% - ne serait-il pas pertinent de mettre un at aussi pour le CAS des tableaux ?
% - en OCaml, c'est <- pour les tableaux et := pour les référence. Pourquoi fait-on l'inverse ici ?
% GLEN: le problème est qu’on ne peut pas faire l’analogue pour CAS sur une
% référence, "CAS e_at e e" ou "CAS !at e e e" sont trop bizarres.
% par contre on pourrait écrire "CAS_at e e e"…
% - Il y a une ambiguïté dans la syntaxe des CAS pour les tableaux "CAS a[b] c d" peut à la fois parler du CAS dans un tableau mais aussi du CAS d'une référence stockée dans un tableau
% GLEN: cette ambiguïté existe seulement si CAS a une annotation "at". :-)
......@@ -204,7 +204,7 @@
%\newcommand{\Read@op}[1]{\TextOrMath{\texttt{!#1}}{\mathop{!#1}}}
%\newcommand{\Write@op}[1]{\TextOrMath{\texttt{:=#1}}{\mathrel{\coloneqq#1}}}
\newcommand{\Read@op}[1]{\TextOrMath{\texttt{!#1}}{\mathop{!#1}}}
\newcommand{\Write@op}[1]{\TextOrMath{\texttt{<-#1}}{\mathrel{\leftarrow#1}}}
\newcommand{\Write@op}[1]{\TextOrMath{\texttt{:=#1}}{\mathrel{\coloneqq#1}}}
\newcommand{\ReadNA}[1]{\Read@op\NA #1}
\newcommand{\ReadAT}[1]{\Read@op\AT #1}
\newcommand{\ReadANY}[1]{\Read@op\ACCMODEANY #1}
......@@ -219,7 +219,7 @@
%\newcommand{\ArrayWriteNA}[3]{#1[#2] \Write@op\NA #3}
%\newcommand{\ArrayWriteAT}[3]{#1[#2] \Write@op\AT #3}
%\newcommand{\ArrayWriteANY}[3]{#1[#2] \Write@op\ACCMODEANY #3}
\newcommand{\ArrayWrite@op}{\TextOrMath{\texttt{:=}}{\mathrel{\coloneqq}}}
\newcommand{\ArrayWrite@op}{\TextOrMath{\texttt{<-}}{\mathrel{\leftarrow}}}
\newcommand{\ArrayReadNA}[2]{#1[#2]\NA}
\newcommand{\ArrayReadAT}[2]{#1[#2]\AT}
\newcommand{\ArrayReadANY}[2]{#1[#2]\ACCMODEANY}
......
......@@ -2,16 +2,45 @@
% Overview of the implementation of the bounded queue with a circular buffer.
\subsection{Implementation of the Bounded Queue}
\subsection{An Implementation of the Bounded MRMW Queue Using a Circular Buffer}
\label{sec:queue:impl}
\input{figure-queue-impl}
A queue is a first-in first-out container data~structure. At any time, it holds
an ordered list of items. It supports two main operations: \enqueue inserts
a provided item at one extremity of the queue (the \emph{head}); \dequeue extracts
an item ---~if there is one~--- from the other extremity (the \emph{tail}).
In a concurrent setting, a legitimate question is whether several threads can
operate the queue safely. The answer depends on the implementation.
%
Possible restrictions include allowing only one thread to enqueue
(single~writer), or allowing only one thread to dequeue (single~reader),
or both.
% digression:
Despite not being fully general, such implementations have use cases:
work~stealing, for example, is commonly achieved using multiple-reader,
single-writer queues.
In this paper we study an implementation of a \emph{multiple-reader, multiple-writer}
(MRMW) queue, that is, a queue in which any number of threads are allowed to
enqueue and dequeue.
% TODO: motivation for MRMW queues?
%
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
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
% TODO: find where this implementation was first described
% ref: https://github.com/rigtorp/MPMCQueue
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
\fref{fig:queue:impl} shows the
implementation of the bounded MRMW queue in \mocaml{}. 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
atomic field and an \emph{item} in a nonatomic field. The data~structure also
......@@ -100,7 +129,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 reference~\refhead, getting
a value~\head. We have seen that the new item should have rank~\head. To check
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$.
%
......@@ -123,7 +152,7 @@ control of offset~$\modcap\head$, and we know that its status has not changed.
% et posséder un offset. Les deux vont ensemble je suppose?
%
% TODO: vague:
Indeed, enqueueing an item with rank~\head\ is the only way to change it.
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
......
......@@ -7,11 +7,6 @@
\subsubsection{Specification in a sequential setting}
A queue is a first-in first-out container data~structure. At any time, it holds
an ordered list of items. It supports two main operations: \enqueue inserts
a provided item at one extremity of the queue (the \emph{head}); \dequeue extracts
an item ---~if there is one~--- from the other extremity (the \emph{tail}).
A queue holding $\nbelems$ items \(\elemList*\), where the left extremity
of the list is the tail and the right extremity is the head,
is represented in separation logic with a representation predicate:
......
\section{A Bounded Queue With a Circular Buffer}
\section{A Bounded MRMW Queue}
\label{sec:queue}
\input{queue-spec}
\input{queue-impl}
\input{queue-spec}
\input{queue-proof}
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