Cosmo: a concurrent separation logic for the weak memory of Multicore OCaml
by Glen Mével
Wednesday 14 December 2022 at 2pm
Inria Paris,. 2 rue Simone Iff, Paris, Salle Lions 1, and online
Abstract: Multicore OCaml extends OCaml with support for shared-memory concurrency. It is equipped with a weak memory model, for which an operational semantics has been published. This begs the question: what reasoning rules can one rely upon while writing or verifying Multicore OCaml code?
To answer it, we instantiate Iris, a modern descendant of Concurrent Separation Logic, for Multicore OCaml. This yields a low-level program logic whose reasoning rules expose the details of the memory model. On top of it, we build a higher-level logic, Cosmo, which trades off some expressive power in return for a simple set of reasoning rules that allow accessing non-atomic locations in a data-race-free manner, exploiting the sequentially-consistent behavior of atomic locations, and exploiting the release/acquire behavior of atomic locations. Cosmo allows both low-level reasoning, where the details of the Multicore OCaml memory model are apparent, and high-level reasoning, which is independent of this memory model.
We illustrate this claim via a number of case studies. We verify several implementations of locks with respect to a classic specification. We also specify and verify a realistic, sophisticated concurrent data structure: namely, a multiple-producer multiple-consumer concurrent queue. In each case, the specification describes the memory behavior of the data structure independently of its implementation---and of the underlying memory model. We achieve this through the joint use of so-called ``logically atomic triples'' and of Cosmo’s views. Thus, Cosmo’s approach to verification is modular with respect to the memory model: a coarse-grained application that uses these data structures as the sole means of synchronization can be verified without any knowledge of the weak memory model.
Jury:
- Aleks Nanevski, IMDEA, Madrid (reviewer)
- Mark Batty, University of Kent (reviewer)
- Azalea Raad, Imperial College, London
- Stephen Dolan, Jane Street, London
- Ralf Treinen, Université Paris-Cité
- François Pottier, Inria (co-supervisor)
- Jacques-Henri Jourdan, LMF (co-supervisor)