Commit a97b594c authored by POTTIER Francois's avatar POTTIER Francois
Browse files

A pass on the second half of the intro.

parent 087d2ffa
......@@ -93,24 +93,54 @@ setting~\cite{vindum-birkedal-21,vindum-frumin-birkedal-21}, % TODO : more citat
we consider a weak-memory setting.
Such a formalization effort is innovative and challenging in several aspects:
\begin{itemize}
\item Weak memory models are infamously known for the subtlety of the reasoning they impose. We choose to use \cosmo~\cite{mevel-jourdan-pottier-20}, a recently developed concurrent separation logic based on Iris supporting the weak memory model of \mocaml{}~\cite{mocaml,dolan-18}.
We believe it is a good balance between the ease of reasoning in the logic and the flexibility and performance of the underlying memory model.
\item In our quest for applicability, we desired to target a concrete queue implementation, which could be used in real-world programs.
Since \mocaml{} is still experimental, we decided to provide a new concurrent queue library to \mocaml{} based on a well-established algorithm~\cite{TODO} used in production.
\item The specification of a concurrent library should state that the concurrent queue behaves as if all the operations acted atomically on a common shared state even though, of course, these operations touch distinct pieces of state and consist of several operations.
To address this challenge, we used the recently developed concept of \emph{logical atomicty}~\cite{iris-15,jung-slides-2019,da2014tada} which we adapted to \cosmo.
\item To the best of our knowledge, this is the first use of logical atomicity in a weakly consistent setting.
This triggered interesting new questions: even though accesses to the queue are totally ordered, the queue specification is not as strong as would be a naive implementation protected with a lock.
Indeed, in the context of a weak memory model, the specification does not only describe the results of the function calls to the library: it also describes the synchronizations (i.e., \emph{happens-before} relationships) between these calls.
These additional properties gives guarantees for memory accesses happening outside of the queue.
They are crucial, for example, if the queue is used for transferring the ownership of a data structure that lives outside of the queue: the receiver needs to synchronize with the emitter to make sure that accesses to the data structure stay valid after the transfer.
Interestingly, our specification is able to describe the subtle behavior of the queue with respect to happens-before relationships: it establishes \emph{some} relationships, but, even though accesses are totally ordered by logical atomicity, no two accesses are ordered by happens-before.
\item In order to keep a high level of trust, we used to Coq proof assistant~\cite{coq} to formally verify our proofs.
\item Weak memory models are infamous for the subtlety of the reasoning that they impose.
We choose to use \cosmo~\cite{mevel-jourdan-pottier-20}, a recently-developed concurrent separation logic
that is based on Iris and that supports the weak memory model of \mocaml{}~\cite{mocaml,dolan-18}.
We believe that this memory model and program logic strike
a good balance between the ease of reasoning offered by the logic and the flexibility and performance allowed by the memory model.
\item In our quest for applicability, we wish to propose a realistic queue implementation, which could be used in real-world programs.
Since \mocaml is still at an experimental stage and does not yet offer
a wide variety of concurrent data structures,
we implement a new concurrent queue library for \mocaml.
We take inspiration from a well-established algorithm~\cite{rigtorp} that has been used in production in several applications.
\item The specification of our data structure should indicate that the concurrent queue behaves
as if all operations acted atomically on a common shared state,
even though in reality these operations access distinct parts of the memory and require many machine instructions.
To address this challenge, we use the recently-developed concept of \emph{logical atomicity}~\cite{iris-15,jung-slides-2019,da2014tada},
which we transport to the setting of \cosmo.
\item To the best of our knowledge, this is the first use of logical atomicity in a weak-memory setting.
This raises new questions: for instances, even though all operations on the queue are totally ordered,
our specification and implementation offer strictly weaker guarantees than
would be offered by
a coarse-grained implementation.
% (a sequential data structure protected with a lock). % déjà dit
Indeed, in the context of a weak memory model, the specification of a concurrent data structure
must describe not only the result of every operation,
but also the manner in which these operations are synchronized,
that is, the \emph{happens-before} relationships that exist between these operations.
This additional information allows reasoning about accesses to areas of memory \emph{outside} of the queue data structure.
It is crucial, for example,
if the queue is used to transfer the ownership of a piece of memory
from an enqueuer to a dequeuer:
there must exist a happens-before relationship between the \enqueue
operation and the corresponding \dequeue operation,
so as to ensure that the dequeuer acquires the enqueuer's view of this piece of memory.
Our specification is able to describe the subtle behavior of our queue implementation with respect to happens-before relationships:
indeed, our implementation establishes \emph{some} happens-before relationships,
but, even though accesses are totally ordered by logical atomicity,
not all accesses are ordered by happens-before.
% FP: il y avait écrit "no two" (aucun), mais je crois que c'est "not all" (pas tous)
\item We use the Coq proof assistant~\cite{coq} to formally verify our proofs.
Our development is available as an appendix of this paper. % TODO : adapter dans la version finale
\end{itemize}
% TODO : d'autres challenges/contributions à faire figurer ici ?
We start by explaining in detail in \sref{sec:queue:spec} the specification we chose for our concurrent queue.
Then, in \sref{sec:queue:impl}, we detail our implementation in \mocaml{}, and, in \sref{sec:queue:proof} we explain our proof of correctness.
Finally, in \sref{sec:pipeline}, we demonstrate that our specifications are indeed useful in the context of a larger library by formally verifying the correctness of a simple pipeline library using the concurrent queue.
The paper concludes with related work in \sref{sec:related}.
The paper begins with a detailed explanation of the specification
of our concurrent queue (\sref{sec:queue:spec}).
Then, we present our implementation of
the queue in \mocaml{} (\sref{sec:queue:impl}), and explain our proof of correctness (\sref{sec:queue:proof}).
Next (\sref{sec:pipeline}), we demonstrate that our specification is indeed usable,
by exploiting it in the context of a simple piece of client code,
where the concurrent queue is used to establish a pipeline between
a set of producers and a set of consumers.
The paper ends with a review of the related work (\sref{sec:related}).
......@@ -54,3 +54,10 @@
year = 2021,
note = {\url{https://cs.au.dk/~birke/papers/mpmc-queue.pdf}},
}
@Misc{rigtorp,
author = {Erik Rigtorp},
title = {MPMCQueue},
month = mar,
year = 2021,
note = {\url{https://github.com/rigtorp/MPMCQueue}}}
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