#	Pagina
attuale pagina	/open-h2020/projects/215252/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 1 - RCADE (Reversible causally-consistent debugging of concurrent programs)

Teaser

Summary

Modern computing devices execute complex software to provide every-day services and applications. The development of such software is challenging, time-consuming and costly. It involves writing a program code, testing it and debugging it, namely finding an error in the code and correcting it. It is estimated that debugging costs an estimated 312 billion USD a year. The most successful commercial debugging tools are reversible debuggers. They allow the users to undo an execution of a faulty program, to find and correct errors, and then to run the corrected code forwards again. UndoDB by Undo Software is the top reversible debugger currently on the market. However, even the best reversible debuggers are not suited very well to debugging of concurrent programs. Moreover, it is not universally agreed yet how to reverse the code of concurrent or distributed software. This project aims at addressing these shortcomings by exploiting the promising notion of causally- consistent reversibility as the basis for reversible debugging tools. Novel formal models and new techniques for recording, analysis and replay of concurrent programs will be created. An execution engine for the shared-memory and message- passing styles of programs will be developed in a close collaboration with Undo Software and Erlang Solutions, the leading software companies. The scientific outcomes will be turned into an experimental prototype software, called Reversible CAusally-consistent DEbugger (RCADE), which will extend and enhance commercial debugging tools, especially for concurrency.

Work performed

Regarding research, several aspects have been investigated. First, the fellow further extended the tool for the automatic synthesis of reversible Erlang actor from a global protocol specification. Moreover, a first attempt to adapt the developed technology to model Continuous Integration (CI) case studies have been made. Second, a reversible model for true concurrent systems has been developed by providing a novel method to obtain a causally consistent reversible semantics for Place Transitions (P/T) Petri nets. This model has been further developed and the relationship between reversible P/T nets and Reversible Prime Event Structures (RPES) has been studied. Third, the theory of the reversible causal framework of has been further developed, so to capture different causal semantics. Lastly, the fellow started investigating a reversible semantics for a simplified C language with threads, to target shared memory concurrency.

Final results

We started investigating the applicability of automatic syntheses of reversible Erlang code to model Continuous Integration scenarios. If the other results of the project were foreseen and their application to the debugging industry was certain, the application of our results to CI scenarios was not foreseen. Even if this is still preliminary work, we are optimistic that it will pave the way to enhance automatic CI integration in well-established software development tools.