Commit 6cd958a1 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files


parent 5f517054
This diff is collapsed.
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.
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.
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}.
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.
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.
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.
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
......@@ -65,7 +65,7 @@
\author{Glen Mével}
\institution{Inria, Université Paris-Saclay, CNRS, Laboratoire de méthodes formelles}
\institution{Inria, Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire des méthodes formelles}
......@@ -74,19 +74,19 @@
\author{Jacques-Henri Jourdan}
\institution{Université Paris-Saclay, CNRS, Laboratoire de méthodes formelles}
\institution{Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire des méthodes formelles}
\author{François Pottier}
%% \author{François Pottier}
%% \affiliation{%
%% \institution{Inria}
%% \country{France}
%% }
%% \email{}
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