Commit 216bd465 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

A pass on the first half of the intro.

parent 1f038b43
\section{Introduction}
\label{sec:intro}
Advances in multicore hardware during the last two decades asks for powerful tools for writing efficient multicore software which we can trust.
Advances in multicore hardware during the last two decades have created a need for powerful tools for writing efficient and trustworthy multicore software.
These tools include well-designed programming languages and their compilers, efficient thread-safe libraries, and expressive program logics for proving programs using multicore features.
While some of these already exist, we can only now start to use verification tools for modularly and precisely specifying and proving correct realistic libraries supporting fine-grained shared-memory concurrency.
% FP suggestion: "programs using multicore features" -> "the correctness of these libraries and of the applications that exploit them"
While some such verification tools already exist,
researchers are only now beginning
to explore whether and how these tools can be exploited to
modularly specify and verify realistic libraries
that support fine-grained shared-memory concurrency.
Most programming languages supporting multicore features make the choice of presenting shared memory as a primitive mean of communication between threads.
Although this choice brings flexibility for writing efficient programs, this comes at an important cost: in order to be efficient in practice, shared-memory concurrency cannot follow an intuitive \emph{sequentially consistent}~\cite{lamport-79} semantics, where every thread immediately sees all the memory accesses of other threads in the same order.
Instead, these programming languages usually come with a subtly defined \emph{weak memory model} precisely defining how the memory accesses of the different threads may interact with each other.
This is, for example, the case of Rust, C and C++, sharing the same so-called \emph{C11 memory model}~\cite{c11mm,rc11}, of Java and languages based on the JVM~\cite{jmm,lochbihler-jmm-12,bender-palsberg-19} and of the multicore extension of the OCaml programming language~\cite{dolan-18,mocaml,ocaml}.
Most of the programming languages that support multicore programming
present shared memory as the primitive means of communication between threads.
Although this design choice offers the greatest flexibility for writing efficient programs,
it comes at an important cost: in order to achieve maximal efficiency, % in practice?
shared-memory concurrency cannot follow an intuitive \emph{sequentially consistent} semantics~\cite{lamport-79},
where all threads have the same view of memory at every time.
% FP: ça me semblait plus simple que la version plus longue ci-dessous:
% where every thread immediately sees all of the memory updates performed by other threads,
% and where these updates are visible to all threads in the same order.
%
Instead, these programming languages usually come with a subtle \emph{weak memory model},
which defines precisely how the memory accesses performed by different threads may interact with each other.
This is the case, for example, of Rust, C and C++, which share the \emph{C11 memory model}~\cite{c11mm,rc11};
of Java and of the languages based on the JVM~\cite{jmm,lochbihler-jmm-12,bender-palsberg-19};
and of the Multicore extension of the OCaml programming language~\cite{dolan-18,mocaml}.
Not only its semantics is subtle, but shared memory concurrency causes interesting challenges in modular program verification: recently, a large variety of concurrent separation logics tried to address the issue of formally verifying programs using shared-memory concurrency.
Notably, \citet{brookes-ohearn-16} introduced the Concurrent Separation Logic, supporting coarse-grain resource sharing through mutexes only.
Their approach was gradually improved over the years, leading to expressive, higher-order separation logics such as Iris~\cite{iris,iris-15}, able to express complex concurrent protocols through \emph{ghost state} and \emph{invariants}, and supporting reasoning on fine-grained concurrency using atomic memory accesses instead of mutexes.
Yet, pure Iris is restricted to sequentially consistent semantics, it does not support weak memory models.
A new generation of logics lifted this restriction for various memory models.
GPS~\cite{turon-vafeiadis-dreyer-14}, iGPS~\cite{kaiser-17} and iRC11~\cite{dang-20} targeted fragments of the C11 memory models, while \hlog{}~\cite{mevel-jourdan-pottier-20} targeted the \mocaml{} memory model.
Because its semantics is subtle, shared-memory concurrency naturally creates
difficult and interesting challenges in modular program verification.
% FP peut-être rappeler que le problème (dans un cadre SC) a été étudié depuis
% 50 ans (Owicki-Gries, 1976, par exemple), mais qu'il est encore un objet
% d'études itenses et que la démocratisation du multicore et de la mémoire
% faible renforce son intérêt et sa difficulté.
Just in the past fifteen years, a large variety of concurrent separation logics have
been designed in order to meet the challenge of formally specifying and
verifying programs that exploit shared-memory concurrency.
\citet{brookes-04} and \citet{ohearn-07}
introduced Concurrent Separation Logic~\cite{brookes-ohearn-16},
% FP: j'ai changé les citations parce que l'ancien texte donnait
% l'impression que CSL datait de 2016.
which supported coarse-grain sharing of resources via mutexes.
Their approach was gradually improved over the years, leading to expressive,
higher-order separation logics, such as Iris~\cite{iris-15,iris}.
Iris is able to express complex concurrent protocols, thanks to
mechanisms such as \emph{ghost state} and \emph{invariants},
and supports reasoning about fine-grain concurrency,
at the level of individual memory accesses.
Concurrent data structures, such as mutexes,
need not be considered primitive any more;
they can be implemented and verified.
Still, plain Iris is restricted to sequentially consistent semantics: it does not support weak memory models.
A new generation of logics remove this restriction, for various memory models:
GPS~\cite{turon-vafeiadis-dreyer-14}, iGPS~\cite{kaiser-17} and iRC11~\cite{dang-20}
target fragments of the C11 memory model,
while \cosmo~\cite{mevel-jourdan-pottier-20} targets the \mocaml memory model.
iGPS, iRC11 and \cosmo are based on Iris.
These logics are nice pieces of work, but they can only be really useful tools if they allow the modular verification of realistic multicore programs.
In particular, they must be able to precisely specify and prove correct concurrent data structure libraries.
Concurrent queues are an archetypal example of such a data structure which we want to formally verify: they are widely used in practice, for example in order to manage tasks which are generated and handled by different threads. % TODO : citations
Nevertheless, while an implementation based on a simple mutex guarding a naive queue implementation would certainly be correct, more efficient implementations based on subtle fine-grained atomic memory accesses do exist and allow for better performances in the context of an intensive use.
Unfortunately, these implementations are delicate and use subtle properties of the memory model: informal proofs may be unconvincing by their lack of attention to the many details one needs to consider.
These logics are nice pieces of work, but can become practically useful tools only
if it is demonstrated that they allow the modular verification of realistic multicore programs.
In particular, they must enable their users to precisely specify and verify concurrent data structure implementations.
A concurrent queue is an archetypal example of such a data structure:
it is widely used in practice, for example
to manage a sequence of tasks that are generated and handled by different threads. % TODO : citations
While a coarse-grained implementation (that is, a sequential queue implementation,
protected by a single lock)
would certainly be correct,
there exist more efficient implementations,
based on subtle fine-grained memory accesses,
which yield better performance, especially under heavy contention.
% FP dans la phrase précédente, on dit deux fois que c'est plus efficace
Unfortunately, these implementations are delicate and
often rely on subtle properties of the memory model.
An informal correctness argument is difficult, and is likely
to be unconvincing and unreliable.
Thus, concurrent data structures are prime candidates for formal
verification. In fact, many machine-checked proofs of concurrent
data structures have appeared in the literature already, % TODO citations
% Bornat et O'Hearn, pour remonter un peu loin
% citer un survey serait bien...
but relatively few verification efforts take place
in a weak-memory setting, % TODO citations
and fewer still rely on a modular methodology,
where a proof of a concurrent data structure
and a proof of its client (perhaps a concurrent application,
or another concurrent data structure)
can be modularly combined.
In this paper, we propose to specify and give the formal verification of such a concurrent queue implementation.
While other such formalizations already exist% TODO : citations
In this paper, we present a specification of a concurrent queue, in a weak-memory setting,
and we formally that a particular concurrent queue implementation satisfies this specification.
While other such formalizations already exist% TODO : citations, e.g. la queue Michael-Scott de Vindum
, we consider a more realistic setting where memory does not obey sequential consistency but is rather described by a more subtle weak memory model.
Such a formalization 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 \hlog{}~\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}.
\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 \hlog{}.
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.
......
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