Reversibility for concurrent memory models

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.