Reversible Gray Debugging of Concurrent Systems

The project tackles gray debugging of concurrent systems. Gray debugging means debugging systems where only part of the source code is accessible (e.g., the system invokes external services such as Google Maps). Debugging concurrent systems (from multiprocessors to Cloud) is notoriously hard. Reversible Causal-Consistent Debugging and Replay (RCCDR) is an innovative approach to this problem, allowing one to log a faulty execution in production environment and replay it in the debugger. There it can be explored backwards and forwards following causality links from the visible misbehavior to the bug causing it. This approach has been implemented in CauDEr, a debugger for the Erlang language.Currently, RCCDR requires access to the whole source code of the target program. To enable gray RCCDR we need to answer the following questions:How can we define RCCDR, and, more generally, reversibility in concurrent systems, in a compositional way, to be able to apply it to systems which are only partially accessible? Are we able to correctly explore backwards and forwards the accessible part? If not, which approximation in the exploration is caused by the missing information about the inaccessible part? Till now RCCDR has only been explored in the concrete setting of Erlang, and gray RCCDR has never been studied. We plan to study gray RCCDR at two levels:1) the abstract level of event structures. Abstraction ensures simpler proofs and generality of the results, making them applicable to many languages;2) the concrete level of Erlang semantics, ensuring applicability in a setting of interest, and allowing to implement it by extending CauDEr and integrating it in the Erlang Solutions environment. As an outcome we will provide the theory to apply the powerful RCCDR approach to concurrent systems which are only partially accessible, as well as exploit it in practice, in the setting of Erlang. This will also enable interaction with IT SMEs and software developers.