Programming reversible recoverable systems
The REVER project aims to develop semantically well-founded and composable abstractions for dependable distributed computing on the basis of a reversible programming model, where reversibility means the ability to undo any program execution and to revert it to a state consistent with the past execution. The critical assumption behind REVER is that by combining reversibility with notions of compensation and modularity, one can develop systematic and composable abstractions for dependable programming. The REVER workprogramme is articulated around three major objectives: - To investigate the semantics of reversible concurrent processes. - To study the combination of reversibility with notions of compensation, isolation and modularity in a concurrent and distributed setting. - To investigate how to support these features in a practi

Scientific advances from REVER should include:

– New models for causality in distributed systems, providing the foundations for a causal semantics of reversible systems.

– New topological and categorical models for the semantics of reversible systems and languages.

– A new REVER process calculus featuring controlled reversibility, compensation for irreversible actions, and distributed localities.

– A comprehensive behavioral theory for the REVER calculus, including proof techniques to reason about reversible distributed systems in presence of failures.

– A new theory of behavioral contracts for reversible and recoverable components.

– Technological advances from REVER should include:

– The definition of new programming language primitives for the construction of recoverable and dependable systems;

– Their integration in a practical (object-oriented, functional) programming language (the REVER language).

– The formal specification, proof of correctness and prototype implementation of an abstract machine for the REVER programming language.

– A discrete-event simulator for distributed reversible systems to aid in the specification of recoverable distributed systems using the REVER calculus.

– A formal analysis of version control software using the semantical models developed by REVER

The REVER project has started on Dec. 1, 2011.