Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                           Lundi 18 novembre, 10h30

                                  ----------
                                  Glen Mével
                                  ----------

                                 Inria Paris

               ===============================================
               	Towards a separation logic for Multicore OCaml
               ===============================================

Separation logic[1] has proven an effective way of reasoning about
functional correctness of imperative programs. In the last decade, tools
such as CFML[2] brought its expressiveness to deductive program
verification for a meaningful fragment of the OCaml language.

However, to this day, mainstream OCaml does not support true
shared-memory concurrency, and neither does CFML.

With the anticipated advent of Multicore OCaml[3], there is now a need
for reasoning principles for concurrent programs. Such concerns have
been addressed by extensions to separation logic[4]. Of the many
“Concurrent Separation Logics” that resulted, Iris[5] stands out as a
highly flexible framework, with a Coq mechanization. It has been shown
recently[6] how Iris could be used to reason about executions in a weak
memory model, namely, the release-acquire fragment of C11.

In our work, we use Iris to derive a program logic for Multicore OCaml,
based on its proposed weak memory model[7]. This memory model is simpler
than that of C11, and we argue that our system exhibits primitive
reasoning principles that are easier to deal with than what was possible
for C11. Using simple examples, we show how the invariant associated
with the correctness of a concurrent data structure under sequential
consistency, extends to the weak memory model of Multicore OCaml.

[1]: Reynolds, J.C.: "Separation Logic: A Logic for Shared Mutable Data
Structures" (2002)
[2]: Charguéraud, A.: "Characteristic formulae for the verification of
imperative programs" (2011)
[3]: https://github.com/ocaml-multicore/ocaml-multicore/wiki
[4]: O'Hearn, P.: "Resources, Concurrency and Local Reasoning" (2007)
[5]: Jung, R. et al.: "Iris: Monoids and invariants as an orthogonal
basis for concurrent reasoning" (2015)
[6]: Kaiser, J.-O. et al.: "Strong logic for weak memory: Reasoning
about release-acquire consistency in Iris" (2017)
[7]: Dolan, S. et al.: "Bounding data races in space and time" (2018)