Monday, December 16th, 2024
- Share
- Share on Facebook
- Share on X
- Share on LinkedIn
Reversibility for Concurrent Memory Models
Abstract:
Reversibility in concurrent programming languages has been extensively studied in message-passing systems, but has not been studied in concurrent shared memory models. In this work, we explore causal consistent reversibility in shared memory models, addressing the challenges of making shared memory reversible, particularly when weak and non-standard memory models are involved. We begin by extending reversible Erlang to handle shared memory constructs, highlighting the difficulties that arise from non-standard memory operations, such as reading entire maps. Next, we propose a structured, two-step approach. First, we introduce a meta-model framework that defines memory models as synchronous products of labeled transition systems (LTSs), incorporating three components: threads, memory, and scheduler. This framework can describe various memory models, including sequential consistency, write buffer, and transactional. Second, we develop a compositional theory to make the product of LTSs reversible, ensuring causal consistency. We apply this theory to a sequential consistency memory model, comparing it to an automatic approach and showing that our method avoids capturing unwanted dependencies.
Date et lieu
Lundi 16 Décembre à 9:00
Grand Amphithéâtre Inria Montbonnot
and visio
Composition du jury
Jean-Bernard Stefani
(INRIA, Grenoble), supervisor
Ivan Lanese
(Univ. Bologna, Italy), supervisor
Daniele Varacca
(Univ. Paris-Est Créteil), reviewer
Irek Ulidowksi
(Univ. Leicester, UK), reviewer
Claudio Mezzina
(Univ. Urbino, Italy), examiner
Gwen Salaun
(UGA), examiner
Cinzia di Giusto
(Univ. Nice), examiner
- Share
- Share on Facebook
- Share on X
- Share on LinkedIn