Skip to Main content Skip to Navigation
Conference papers

An Axiomatic Approach to Reversible Computation

Ivan Lanese 1, 2 Iain Phillips 3 Irek Ulidowski 4
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Undoing computations of a concurrent system is beneficial in many situations, e.g., in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation including process calculi such as CCS, languages like Erlang, prime event structures and occurrence nets. However it has not been settled what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between these properties. In particular, we show how they are derivable from a set of axioms. Our intention is that when establishing properties of some formalism it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new notions related to causal consistent reversibility, namely causal safety and causal liveness, and show that they are derivable from our axioms.
Complete list of metadatas

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/hal-03004421
Contributor : Ivan Lanese <>
Submitted on : Friday, November 13, 2020 - 4:13:02 PM
Last modification on : Saturday, November 14, 2020 - 8:23:01 AM

File

published.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Ivan Lanese, Iain Phillips, Irek Ulidowski. An Axiomatic Approach to Reversible Computation. FoSSaCS 2020 - 23rd International Conference on Foundations of Software Science and Computation Structures, Apr 2020, Dublin, Ireland. pp.442 - 461, ⟨10.1007/978-3-030-45231-5_23⟩. ⟨hal-03004421⟩

Share

Metrics

Record views

11

Files downloads

103