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

ICFP21 paper: rename MRMW queue to MPMC queue

parent b63d980b
......@@ -123,8 +123,6 @@ systems (if any), generally, outside the specific support for weak memory."
RELECTURE:
- MRMW queue -> MPMC queue ? semble être le nom canonique dans la littérature
intro:
- ref: "other such formalizations already exist in SC [Vindum]"
-> mentionner que c’est la même implé ? dit dans le related work
......
We use Cosmo, a modern concurrent separation logic, to formally specify and verify
an implementation of a multiple-writer multiple-reader concurrent queue in the
an implementation of a multiple-producer multiple-consumer concurrent queue in the
setting of the Multicore OCaml weak memory model. We view this result as a demonstration and experimental verification of the manner in
which Cosmo allows modular and formal reasoning about advanced concurrent data structures. In particular, we show how the joint use of
logically atomic triples and of Cosmo's views makes it possible to describe precisely in the specification the interaction between the queue library and
......
......@@ -2,10 +2,10 @@
% Overview of the implementation of the bounded queue with a ring buffer.
\section{Implementation of a Bounded MRMW Queue Using a Ring Buffer}
\section{Implementation of a Bounded MPMC Queue Using a Ring Buffer}
\label{sec:queue:impl}
We now present an implementation of a bounded MRMW queue, that satisfies the specification devised in~\sref{sec:queue:spec}.
We now present an implementation of a bounded MPMC queue, that satisfies the specification devised in~\sref{sec:queue:spec}.
For the purpose of the formalization, it is written in an idealized version of the \mocaml{} language which we introduce in~\sref{sec:lang},
% GLEN: j’enlève "with a rigorously defined formal semantics" car la phrase
% laissait penser qu’on présentait ladite sémantique dans la section liée,
......
......@@ -27,7 +27,7 @@ and it also creates some contention on the use of the queue.
%
These costs are often unnecessary, as many data~structures are designed
specifically to support concurrent accesses. In this paper, as stated, we wish
to prove the correctness of a MRMW~queue implementation, which should thus
to prove the correctness of a MPMC~queue implementation, which should thus
ensure, by itself, thread safety.
%
Hence we can achieve finer-grain concurrency, where operating on a queue does
......
......@@ -2,7 +2,7 @@
% Specification of queues in CSL.
\section{Specification of a MRMW Queue in a Concurrent Separation Logic}
\section{Specification of a MPMC 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
......@@ -14,15 +14,15 @@ 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),
(single~producer), or allowing only one thread to dequeue (single~consumer),
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.
%% work~stealing, for example, is commonly achieved using multiple-consumer,
%% single-producer 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
In this paper we study an implementation of a \emph{multiple-producer, multiple-consumer}
(MPMC) 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
......
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