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

impl before spec

parent f1ead547
......@@ -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}
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