Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                          Salle Lions 1, bâtiment C
                           MERCREDI 12 avril, 11h00

                       Olivier Nicole et Fabrice Buoro
                                   Tarides

         Runtime Data Race Detection in OCaml 5 with ThreadSanitizer

Before OCaml 5, the only form of concurrency available was
interleaving: only one thread could execute OCaml code at a time. With
OCaml 5 comes the possibility of writing truly parallel OCaml code
that runs on multiple cores, and with it the possibility of
introducing parallelism bugs. A subclass of parallelism bugs are data
races. Racy programs have undefined behavior in languages like C; in
OCaml, their impact is more limited [1], but they still can cause
unexpected results, and are notoriously hard to track down.

ThreadSanitizer (TSan) is a runtime detector for data races, initially
developed by Google and now available for many languages (C/C++, Go,
Swift, …). In this talk, we will summarize how TSan detects data
races, what changes to the compiler and runtime are required to relay
the necessary information to the TSan runtime, and what special cases
we had to handle. We will also mention the challenges of using a race
detector based on the C11 memory model, and the “translation” that we
propose to detect data races in the OCaml model.

[1] S. Dolan, K. Sivaramakrishnan, and A. Madhavapeddy,
“Bounding data races in space and time,” in PLDI 2018

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

             Nos séminaires sont accessibles en ligne en direct:
                  https://webconf.math.cnrs.fr/b/fra-ryy-fjn