Commit 13e8bcc6 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Intro

parent 0a3d8195
......@@ -3,20 +3,49 @@
Advances in multicore hardware during the last two decades asks for powerful tools for writing efficient multicore software which we can trust.
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 specifying and proving correct realistic libraries supporting fine-grained shared-memory concurrency.
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.
Most programming languages supporting multicore features make the choice of presenting shared memory as a primitive mean of communication between threads.
Although this choices brings flexibility for writing efficient programs, it comes at an important cost: first, in order to be efficient in practice, shared memory 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.
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 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{mocaml,ocaml}.
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}.
Not only its semantics is subtle, but shared memory concurrency causes interesting challenges in program verification: recently, a large variety of concurrent separation logics tried to address the issue of formally verifying programs using shared-memory concurrency.
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}, allowing to express complex concurrent protocols through \emph{ghost state} and \emph{invariants}, and supporting fine-grained sharing protocols using atomic memory accesses.
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.
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.
These logics are niece pieces of work, but they can only be really useful tools if they allow the modular verification of realistic multicore programs.
In particular, it is important to specify and prove correct concurrent data structure libraries in these logics.
The concept of \emph{logically atomic triple} gives a practical
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.
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
, 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}.
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{}.
\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.
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}.
......@@ -36,3 +36,12 @@
howpublished = {\url{https://gitlab.inria.fr/gmevel/cosmo}},
year = "2020",
}
@inproceedings{da2014tada,
title={TaDA: A logic for time and data abstraction},
author={da Rocha Pinto, Pedro and Dinsdale-Young, Thomas and Gardner, Philippa},
booktitle={European Conference on Object-Oriented Programming},
pages={207--231},
year={2014},
organization={Springer}
}
\section{Related Work}
\section{Related Work and conclusion}
\label{sec:related}
% Constantin Enea, "Verifying Visibility-Based Weak Consistency".
......
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