Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                          Salle Lions 1, bâtiment C
                           Lundi 27 novembre, 10h30

                               Alexandre Moine
                                 Inria Paris

                DisLog: A Separation Logic for Disentanglement

Disentanglement is a property of parallel programs asserting that
parallel tasks remain oblivious to each other's allocations. Making
use of disentanglement, the MPL (MaPLe) compiler for parallel ML
equips programs with a blazingly fast, task-local, garbage collector.
However, prior work on disentanglement has focused on the design of
optimizations, relying on runtime instrumentation for detecting and
managing entanglement.

In this talk, we shift our attention to static verification. We
present DisLog, an Iris-powered separation logic for
disentanglement. DisLog enriches separation logic with the notions
necessary for reasoning about the fork-join structure of parallel
programs, allowing the user to verify that memory accesses are
effectively disentangled.

A large class of programs, including race-free programs, exhibit
memory access patterns that are disentangled "by construction". To
reason about these patterns, we distill from DisLog an almost
standard concurrent separation logic called DisLog+. In this
high-level logic, no specific reasoning about memory accesses is
needed: functional correctness proofs entail disentanglement.

This is joint work with Sam Westrick and Stephanie Balzer.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.