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

reorganize sections: put reminder of syntax just before description of code,...

reorganize sections: put reminder of syntax just before description of code, lift queue.{spec,impl,proof} up by 1 level
parent 8f047ba8
% ------------------------------------------------------------------------------
% Reminders on the programming language and program logic
% Reminders on the programming language.
\section{Multicore OCaml}
\subsection{Multicore OCaml}
\label{sec:lang}
\input{figure-lang-syntax}
......
......@@ -102,7 +102,6 @@
% ------------------------------------------------------------------------------
\input{intro}
\input{lang}
\input{queue}
\input{pipeline}
\input{related}
......
......@@ -2,9 +2,11 @@
% Overview of the implementation of the bounded queue with a ring buffer.
\subsection{Implementation of a Bounded MRMW Queue Using a Ring Buffer}
\section{Implementation of a Bounded MRMW Queue Using a Ring Buffer}
\label{sec:queue:impl}
\input{lang}
\input{figure-queue-impl}
% TODO: find where this implementation was first described
......@@ -121,7 +123,7 @@ This is implied by, but is weaker than, the equation $\head = \tail$.%
% il se peut que d’autres cases plus loin aient déjà été vidées (idem pour
% "vide").
\subsubsection{Some invariants of the queue}
\subsection{Some invariants of the queue}
Once the queue has been created, the reference~\refhead is only accessed from
function~\tryenqueue. The only place where it is modified is the compare-and-set
......@@ -147,7 +149,7 @@ still $2\head$ when we overwrite it with $2\head+1$.
Symmetrically, the status is still $2\tail+1$ when a dequeuer overwrites it with
$2(\tail+\capacity)$.
\subsubsection{Explanation of the code}
\subsection{Explanation of the code}
The function~\enqueue repeatedly calls \tryenqueue until it succeeds;
the latter can fail either because the buffer is full or because of a competing enqueuer.%
......@@ -201,7 +203,7 @@ and can fail either because the buffer is empty or because of a competing dequeu
%
\footref{fn:distinguishfail}
\subsubsection{Interactions between threads}
\subsection{Interactions between threads}
%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
......
......@@ -2,7 +2,7 @@
% Proof of the bounded queue.
\subsection{Proof of the Specification for the Ring Buffer}
\section{Proof of the Specification for the Ring Buffer}
\label{sec:queue:proof}
\input{figure-queue-invariant}
......@@ -45,7 +45,7 @@ of the memory).
% - Lattice: lat → cmra
% - Lattice: botlat → ucmra
\subsubsection{Public state}
\subsection{Public state}
The assertion $\isQueue\tview\hview\elemViewList$ exposes to the user the public
state of the queue. This public state, as motivated in \sref{sec:queue:spec:weak},
......@@ -111,7 +111,7 @@ CMRA: $\authm(\exm(-))$. In this way, there cannot be more than one fragment
(and, in fact, the authority and the fragment play symmetrical roles).
This makes the representation predicate exclusive.
\subsubsection{Internal invariant}
\subsection{Internal invariant}
Along with the exclusive representation predicate $\isQueue\tview\hview\elemViewList$,
we provide the user with the persistent assertion $\queueInv$. It contains the
......@@ -154,7 +154,7 @@ the authority on all three ghost variables, $\gqueue$, $\gmonos$ and $\gtokens$.
The authority of $\gqueue$ is simple: it simply ties internal values to the
public state of the queue, as explained earlier.
\subsubsection{Monotonicity of statuses}
\subsection{Monotonicity of statuses}
The purpose of the ghost variable~$\gmonos$ is to reflect the fact that statuses
are monotonic.
......@@ -275,7 +275,7 @@ we get the following:
Thus this assertion acts as a reminder that, at some point, the status of
slot~\offset\ stored the value~$\status$ and the view~$\sview$.
\subsubsection{Description of slots}
\subsection{Description of slots}
The last two lines of the invariant describe the state of each slot.
For clarity, we introduce two abbreviations:
......
\subsubsection{Specification under sequential consistency}
\subsection{Specification under sequential consistency}
\label{sec:queue:spec:sc}
We now consider the situation where several threads can access the queue concurrently.
......
\subsubsection{Specification in a sequential setting}
\subsection{Specification in a sequential setting}
\label{sec:queue:spec:seq}
Let us start by assuming a sequential setting. We can then use standard
......
\subsubsection{Specification under weak memory}
\subsection{Specification under weak memory}
\label{sec:queue:spec:weak}
\input{figure-queue-spec}
......
......@@ -2,9 +2,40 @@
% Specification of queues in CSL.
\subsection{Specification of Queues in a Concurrent Separation Logic}
\section{Specification of a MRMW Queue in a Concurrent Separation Logic}
\label{sec:queue:spec}
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
an 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.
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
more frequently than they are dequeued; in this situation, a bounded queue has no risk of
exhausting system memory; instead, if the maximum size is reached,
enqueuing either blocks or fails.
% TODO: ref for bounded pools/queues: Herlihy & Shavit 10.1
% FP ce n'est pas seulement une question de limiter l'occupation mémoire
% de la file, mais aussi une façon de forcer les producteurs à attendre
% une fois que la file est pleine; donc c'est un mécanisme de contrôle
% de flux.
\input{queue-spec-seq}
\input{queue-spec-sc}
\input{queue-spec-weak}
\section{A Bounded MRMW Queue}
\label{sec:queue}
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
an 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.
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
more frequently than they are dequeued; in this situation, a bounded queue has no risk of
exhausting system memory; instead, if the maximum size is reached,
enqueuing either blocks or fails.
% TODO: ref for bounded pools/queues: Herlihy & Shavit 10.1
% FP ce n'est pas seulement une question de limiter l'occupation mémoire
% de la file, mais aussi une façon de forcer les producteurs à attendre
% une fois que la file est pleine; donc c'est un mécanisme de contrôle
% de flux.
%\section{A Bounded MRMW Queue}
%\label{sec:queue}
\input{queue-spec}
\input{queue-impl}
......
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