Imperial College London
Alternate

DrIainPhillips

Faculty of Engineering, Department of Computing

Senior Lecturer - Computing
 
 
 
//

Contact

 

+44 (0)20 7594 8265i.phillips Website

 
 
//

Location

 

427Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Lanese:2024:10.1145/3648474,
author = {Lanese, I and Phillips, I and Ulidowski, I},
doi = {10.1145/3648474},
journal = {ACM Transactions on Computational Logic},
title = {An axiomatic theory for reversible computation},
url = {http://dx.doi.org/10.1145/3648474},
year = {2024}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - 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, and abstract models such as 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 various reversibility properties. In particular, we show how all properties we consider 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 properties related to causal consistent reversibility, namely causal liveness and causal safety, stating, respectively, that an action can be undone if (causal liveness) and only if (causal safety) it is independent from all the following actions. These properties come in three flavours: defined in terms of independent transitions, independent events, or via an ordering on events. Both causal liveness and causal safety are derivable from our axioms.
AU  - Lanese,I
AU  - Phillips,I
AU  - Ulidowski,I
DO  - 10.1145/3648474
PY  - 2024///
SN  - 1529-3785
TI  - An axiomatic theory for reversible computation
T2  - ACM Transactions on Computational Logic
UR  - http://dx.doi.org/10.1145/3648474
UR  - https://dl.acm.org/doi/10.1145/3648474
UR  - http://hdl.handle.net/10044/1/109580
ER  -
Download