In a language with a reversible semantics, computation steps can be undone: a program can perform standard forward steps, but also backward steps. Reversibility is at the heart of mechanisms in program debugging, error recovery, and compensation handling in transactions.

Reversing a sequential program is easy: it suffices to have a memory that records information about forward steps in case we wish to return to a prior state using a backward step. Reversing a concurrent program is much more difficult: since control may simultaneously reside in more than one point, memories should record information about the steps performed in each thread, but also about the causal dependencies between steps from different threads.

The subtleties of reversibility in a concurrent setting motivate the definition of reversible semantics which are causally consistent, i.e., that ensure that backward steps lead to states that could been have reached by performing forward steps only. A causally consistent semantics never leads to states that are not reachable through forward steps.

This talk will discuss the challenges of reversible concurrency from theoretical and practical standpoints. It will be based on two recent papers (PPDP’17 and TFP’18).

On the theoretical side (PPDP’17), we will present a process model of multiparty protocols with reversibility. This formal model relies on pi-calculus processes that exchange (higher-order) messages following choreographies, as defined by multiparty session types that specify intended protocol executions. The model is equipped with a reversible operational semantics which is causally consistent.

On the practical side (TFP’18), we have developed a Haskell implementation of the reversible operational semantics in the PPDP’17 paper. We exploit algebraic data types to faithfully represent three core ingredients: a process calculus, multiparty session types, and forward/backward reduction semantics. Our implementation bears witness to the convenience of pure functional programming for implementing reversible languages.