Weak memory concurrency and optimisation of C11 programs

In this work we are considering the relaxed memory model for concurrency of the C11/C++11 standard, and characterizing families of optimisations that are sound with respect to the low-level atomics of C11 and their synchronization effects.

This is joint work with Francesco Zappa Nardelli and Robin Morisset from ENS, and Viktor Vafeiadis and Soham Chakraborty from MPI-SWS.

Documents

Separation logic and data races

The language Mezzo is a programming language in the ML tradition, which places strong emphasis on the control of aliasing and access to mutable memory. Its type system can be thought of as "Reynold's separation logic turned into a type system".

The language has been designed by Fran├žois Pottier and Jonathan Protzenko, and I participated in baking shared-memory concurrency into the kernel of Mezzo, and proving the soundness of its type system in the Coq proof assistant.

Documents

Geometric interpretation of concurrency

Collaboration with Emmanuel Haucourt on the analysis of independence of processes in a concurrent program by geometrical means.

Documents

Lazy strategies

I'm working with Delia Kesner on various aspects of optimal reduction in the framework of weak reduction, and on the sharing of subterms. Some of my targets are: the lambda-calculus, higher-order rewriting, and pattern matching calculi. I also study how weak reduction gives to higher-order rewriting a "first-order" behavior.

Documents

Pattern matching-oriented calculi

Exploring the weirdnesses of the evaluation of pattern matching, especially when the patterns are dynamic or when we give up Berry's stability property.

Documents