Reversibility in Erlang: Imperative Constructs -Technical Report

A relevant application of reversibility is causal-consistent reversible debugging, which allows one to explore concurrent computations backward and forward to find a bug. This approach has been put into practice in CauDEr, a causal-consistent reversible debugger for the Erlang programming language. CauDEr supports the functional, concurrent and distributed fragment of Erlang. However, Erlang also includes imperative features to manage a map (shared among all the processes of a same node) associating process identifiers to names. Here we extend CauDEr and the related theory to support such imperative features. From a theoretical point of view, the added primitives create different causal structures than those derived from the concurrent Erlang fragment previously handled in CauDEr, yet we show that the main results proved for CauDEr are still valid