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.
This work has been partially supported by COST Action IC1405 on Reversible Computation - Extending Horizons of Computing. The first author has also been partially supported by French ANR project DCore ANR-18-CE25-0007 and by INdAM as a member of GNCS (Gruppo Nazionale per il Calcolo Scientifico).
Chapter PDF
Similar content being viewed by others
Keywords
References
Barylska, K., Koutny, M., Mikulski, Ł., Pia̧tkowski, M.: Reversible computation vs. reversibility in Petri nets. Science of Computer Programming 151, 48–60 (2018)
Bennett, C.H.: Logical reversibility of computation. IBM Journal of Research and Development 17(6), 525–532 (1973)
Bernadet, A., Lanese, I.: A modular formalization of reversibility for concurrent models and languages. In: Bartoletti, M., Henrio, L., Knight, S., Vieira, H.T. (eds.) ICE. EPTCS, vol. 223, pp. 98–112 (2016)
Carothers, C.D., Perumalla, K.S., Fujimoto, R.: Efficient optimistic parallel simulations using reverse computation. ACM Transactions on Modeling and Computer Simulation 9(3), 224–253 (1999)
Cristescu, I., Krivine, J., Varacca, D.: A compositional semantics for the reversible pi-calculus. In: LICS. pp. 388–397. IEEE Computer Society (2013)
Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR. LNCS, vol. 3170, pp. 292–307. Springer (2004)
Danos, V., Krivine, J.: Transactions in RCCS. In: Abadi, M., de Alfaro, L. (eds.) CONCUR. LNCS, vol. 3653, pp. 398–412. Springer (2005)
Danos, V., Krivine, J., Sobociński, P.: General reversibility. In: Amadio, R.M., Phillips, I. (eds.) EXPRESS. ENTCS, vol. 175(3), pp. 75–86. Elsevier (2006)
de Frutos Escrig, D., Koutny, M., Mikulski, Ł.: Reversing steps in Petri nets. In: Donelli, S., Haar, S. (eds.) Petri Nets. LNCS, vol. 11522. Springer (2019)
Giachino, E., Lanese, I., Mezzina, C.A.: Causal-consistent reversible debugging. In: Gnesi, S., Rensink, A. (eds.) FASE. LNCS, vol. 8411, pp. 370–384. Springer (2014)
Giachino, E., Lanese, I., Mezzina, C.A., Tiezzi, F.: Causal-consistent rollback in a tuple-based language. Journal of Logical and Algebraic Methods in Programming 88, 99–120 (2017)
van Glabbeek, R., Vaandrager, F.: The difference between splitting in \(n\) and \(n+1\). Information and Computation 136(2), 109–142 (1997)
Kari, J.: Reversible cellular automata: From fundamental classical results to recent developments. New Generation Computing 36(3), 145–172 (2018)
Kuhn, S., Ulidowski, I.: Local reversibility in a Calculus of Covalent Bonding. Science of Computer Programming 151, 18–47 (2018)
Landauer, R.: Irreversibility and heat generated in the computing process. IBM Journal of Research and Development 5, 183–191 (1961)
Lanese, I., Phillips, I., Ulidowski, I.: An axiomatic approach to reversible computation (TR) (2020), http://www.cs.unibo.it/~lanese/work/axrev-TR.pdf
Lanese, I., Mezzina, C.A., Schmitt, A., Stefani, J.: Controlling reversibility in higher-order pi. In: Katoen, J., König, B. (eds.) CONCUR. LNCS, vol. 6901, pp. 297–311. Springer (2011)
Lanese, I., Mezzina, C.A., Stefani, J.: Reversibility in the higher-order \(\pi \)-calculus. Theoretical Computer Science 625, 25–84 (2016)
Lanese, I., Mezzina, C.A., Tiezzi, F.: Causal-consistent reversibility. Bulletin of the EATCS 114 (2014)
Lanese, I., Nishida, N., Palacios, A., Vidal, G.: A theory of reversibility for Erlang. Journal of Logical and Algebraic Methods in Programming 100, 71–97 (2018)
Laursen, J.S., Schultz, U.P., Ellekilde, L.: Automatic error recovery in robot assembly operations using reverse execution. In: IROS. pp. 1785–1792. IEEE (2015)
Lienhardt, M., Lanese, I., Mezzina, C.A., Stefani, J.: A reversible abstract machine and its space overhead. In: Giese, H., Rosu, G. (eds.) FMOODS/FORTE. LNCS, vol. 7273, pp. 1–17. Springer (2012)
McNellis, J., Mola, J., Sykes, K.: Time travel debugging: Root causing bugs in commercial scale software. CppCon talk, https://www.youtube.com/watch?v=l1YJTg_A914 (2017)
Melgratti, H.C., Mezzina, C.A., Ulidowski, I.: Reversing Place Transition nets. arXiv 1910, 04266 (2019)
Melgratti, H.C., Mezzina, C.A., Ulidowski, I.: Reversing P/T nets. In: Nielson, H.R., Tuosto, E. (eds.) COORDINATION. LNCS, vol. 11533, pp. 19–36. Springer (2019)
Mezzina, C.A.: On reversibility and broadcast. In: Kari, J., Ulidowski, I. (eds.) RC 2018. LNCS, vol. 11106, pp. 67–83. Springer (2018)
Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. In: Aceto, L., Ingólfsdóttir, A. (eds.) FoSSaCS. LNCS, vol. 3921, pp. 246–260. Springer (2006)
Phillips, I., Ulidowski, I.: Reversibility and models for concurrency. In: Hennessy, M., van Glabbeek, R. (eds.) SOS. ENTCS, vol. 192(1), pp. 93–108. Elsevier (2007)
Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. Journal of Logic and Algebraic Programming 73(1-2), 70–96 (2007)
Phillips, I., Ulidowski, I.: Reversibility and asymmetric conflict in event structures. Journal of Logical and Algebraic Methods in Programming 84, 781–805 (2015)
Phillips, I., Ulidowski, I., Yuen, S.: A reversible process calculus and the modelling of the ERK signalling pathway. In: Glück, R., Yokoyama, T. (eds.) RC. LNCS, vol. 7581, pp. 218–232. Springer (2012)
Pin, J.: On the language accepted by finite reversible automata. In: Ottmann, T. (ed.) ICALP. LNCS, vol. 267, pp. 237–249. Springer (1987)
Sassone, V., Nielsen, M., Winskel, G.: Models of concurrency: Towards a classification. Theoretical Computer Science 170(1–2), 297–348 (1996)
Ulidowski, I., Phillips, I., Yuen, S.: Reversing event structures. New Generation Computing 36(3), 281–306 (2018)
Yokoyama, T., Glück, R.: A reversible programming language and its invertible self-interpreter. In: Ramalingam, G., Visser, E. (eds.) ACM SIGPLAN PEMP. pp. 144–153. ACM (2007)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Lanese, I., Phillips, I., Ulidowski, I. (2020). An Axiomatic Approach to Reversible Computation. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_23
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)