A General Approach to Derive Uncontrolled Reversible Semantics

Authors Ivan Lanese , Doriana Medić



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.33.pdf
  • Filesize: 0.69 MB
  • 24 pages

Document Identifiers

Author Details

Ivan Lanese
  • Focus Team, University of Bologna/Inria, Bologna, Italy
Doriana Medić
  • Focus Team, University of Bologna/Inria, Sophia Antipolis, France

Acknowledgements

The authors thank the reviewers for their helpful comments and suggestions.

Cite AsGet BibTex

Ivan Lanese and Doriana Medić. A General Approach to Derive Uncontrolled Reversible Semantics. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 33:1-33:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.33

Abstract

Reversible computing is a paradigm where programs can execute backward as well as in the usual forward direction. Reversible computing is attracting interest due to its applications in areas as different as biochemical modelling, simulation, robotics and debugging, among others. In concurrent systems the main notion of reversible computing is called causal-consistent reversibility, and it allows one to undo an action if and only if its consequences, if any, have already been undone. This paper presents a general and automatic technique to define a causal-consistent reversible extension for given forward models. We support models defined using a reduction semantics in a specific format and consider a causality relation based on resources consumed and produced. The considered format is general enough to fit many formalisms studied in the literature on causal-consistent reversibility, notably Higher-Order π-calculus and Core Erlang, an intermediate language in the Erlang compilation. Reversible extensions of these models in the literature are ad hoc, while we build them using the same general technique. This also allows us to show in a uniform way that a number of relevant properties, causal-consistency in particular, hold in the reversible extensions we build. Our technique also allows us to go beyond the reversible models in the literature: we cover a larger fragment of Core Erlang, including remote error handling based on links, which has never been considered in the reversibility literature.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Computing methodologies → Concurrent computing methodologies
Keywords
  • Reversible computing
  • causality
  • process calculi
  • Erlang

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Joe Armstrong. Erlang - software for a concurrent world. In Erik Ernst, editor, ECOOP 2007 - Object-Oriented Programming, 21st European Conference, Berlin, Germany, July 30 - August 3, Proceedings, volume 4609 of Lecture Notes in Computer Science, page 1. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73589-2_1.
  2. Giorgio Bacci, Vincent Danos, and Ohad Kammar. On the statistical thermodynamics of reversible communicating processes. In Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO, Winchester, UK, August 30 - September 2, 2011. Proceedings, volume 6859 of Lecture Notes in Computer Science, pages 1-18. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22944-2_1.
  3. Kamila Barylska, Evgeny Erofeev, Maciej Koutny, Lukasz Mikulski, and Marcin Piatkowski. Reversing transitions in bounded Petri nets. Fundam. Inform., 157(4):341-357, 2018. URL: https://doi.org/10.3233/FI-2018-1631.
  4. Alexis Bernadet and Ivan Lanese. A modular formalization of reversibility for concurrent models and languages. In Proceedings 9th Interaction and Concurrency Experience, ICE 2016, Heraklion, Greece, 8-9, pages 98-112, 2016. URL: https://doi.org/10.4204/EPTCS.223.7.
  5. Bob Boothe. Efficient algorithms for bidirectional debugging. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Vancouver, British Columbia, Canada, June 18-21, PLDI '00, pages 299-310, New York, NY, USA, 2000. ACM. URL: https://doi.org/10.1145/349299.349339.
  6. Luca Cardelli and Cosimo Laneve. Reversible structures. In Computational Methods in Systems Biology, 9th International Conference, CMSB 2011, Paris, France, September 21-23. Proceedings, pages 131-140, 2011. URL: https://doi.org/10.1145/2037509.2037529.
  7. Richard Carlsson, Björn Gustavsson, Erik Johansson, Thomas Lindgren, Sven-Olof Nyström, Mikael Pettersson, and Robert Virding. Core Erlang 1.0.3. Language specification, 2004. URL: https://www.it.uu.se/research/group/hipe/cerl/doc/core_erlang-1.0.3.pdf.
  8. Christopher D. Carothers, Kalyan S. Perumalla, and Richard Fujimoto. Efficient optimistic parallel simulations using reverse computation. ACM TOMACS, 9(3):224-253, 1999. URL: https://doi.org/10.1145/347823.347828.
  9. Ioana Cristescu, Jean Krivine, and Daniele Varacca. A compositional semantics for the reversible pi-calculus. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, pages 388-397. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.45.
  10. Vincent Danos and Jean Krivine. Reversible communicating systems. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, Proceedings, volume 3170 of Lecture Notes in Computer Science, pages 292-307. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-28644-8_19.
  11. Vincent Danos and Jean Krivine. Transactions in RCCS. In CONCUR 2005 - Concurrency Theory, 16th International Conference, San Francisco, CA, USA, August 23-26, Proceedings, volume 3653 of Lecture Notes in Computer Science, pages 398-412. Springer, 2005. URL: https://doi.org/10.1007/11539452_31.
  12. Vincent Danos and Jean Krivine. Formal molecular biology done in CCS-R. Electr. Notes Theor. Comput. Sci., 180(3):31-49, 2007. URL: https://doi.org/10.1016/j.entcs.2004.01.040.
  13. Vincent Danos, Jean Krivine, and Paweł Sobociński. General reversibility. In Proceedings of the 13th International Workshop on Expressiveness in Concurrency, EXPRESS 2006, Bonn, Germany, August 26, pages 75-86, 2006. URL: https://doi.org/10.1016/j.entcs.2006.07.036.
  14. Rolf Drechsler and Robert Wille. From truth tables to programming languages: Progress in the design of reversible circuits. In IEEE International Symposium on Multiple-Valued Logic, ISMVL, pages 78-85, 2011. URL: https://doi.org/10.1109/ISMVL.2011.40.
  15. Erlang website. URL: https://www.erlang.org/.
  16. Elena Giachino, Ivan Lanese, and Claudio Antares Mezzina. Causal-consistent reversible debugging. In Fundamental Approaches to Software Engineering - 17th International Conference, FASE 2014, Proceedings, pages 370-384, 2014. URL: https://doi.org/10.1007/978-3-642-54804-8_26.
  17. Elena Giachino, Ivan Lanese, Claudio Antares Mezzina, and Francesco Tiezzi. Causal-consistent rollback in a tuple-based language. J. Log. Algebraic Methods Program., 88:99-120, 2017. URL: https://doi.org/10.1016/j.jlamp.2016.09.003.
  18. Eva Graversen, Iain Phillips, and Nobuko Yoshida. Event structure semantics of (controlled) reversible CCS. In Reversible Computation - 10th International Conference, RC 2018, Leicester, UK, September 12-14. Proceedings, volume 11106 of Lecture Notes in Computer Science, pages 102-122. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99498-7_7.
  19. Stefan Kuhn and Irek Ulidowski. Local reversibility in a calculus of covalent bonding. Sci. Comput. Program., 151:18-47, 2018. URL: https://doi.org/10.1016/j.scico.2017.09.008.
  20. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558-565, 1978. URL: https://doi.org/10.1145/359545.359563.
  21. Rolf Landauer. Irreversibility and heat generation in the computing process. IBM J. Res. Dev., 5:183-191, 1961. URL: https://doi.org/10.1147/rd.53.0183.
  22. Ivan Lanese. From reversible semantics to reversible debugging. In Reversible Computation - 10th International Conference, RC 2018, Leicester, UK, September 12-14, Proceedings, volume 11106 of Lecture Notes in Computer Science, pages 34-46. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99498-7_2.
  23. Ivan Lanese and Doriana Medić. A general approach to derive uncontrolled reversible semantics (TR). Available at URL: https://hal.archives-ouvertes.fr/hal-02902204.
  24. Ivan Lanese, Claudio Antares Mezzina, Alan Schmitt, and Jean-Bernard Stefani. Controlling reversibility in higher-order pi. In CONCUR 2011 - Concurrency Theory - 22nd International Conference, Aachen, Germany, September 6-9. Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 297-311. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_20.
  25. Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. Controlled reversibility and compensations. In Reversible Computation, 4th International Workshop, RC 2012, Copenhagen, Denmark, July 2-3. Revised Papers, volume 7581 of Lecture Notes in Computer Science, pages 233-240. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-36315-3_19.
  26. Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. Reversibility in the higher-order π-calculus. Theor. Comput. Sci., 625:25-84, 2016. URL: https://doi.org/10.1016/j.tcs.2016.02.019.
  27. Ivan Lanese, Claudio Antares Mezzina, and Francesco Tiezzi. Causal-consistent reversibility. Bulletin of the EATCS, 114, 2014. URL: http://eatcs.org/beatcs/index.php/beatcs/article/view/305.
  28. Ivan Lanese, Naoki Nishida, Adrián Palacios, and Germán Vidal. Cauder: A causal-consistent reversible debugger for Erlang. In Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, Proceedings, volume 10818 of Lecture Notes in Computer Science, pages 247-263. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-90686-7_16.
  29. Ivan Lanese, Naoki Nishida, Adrián Palacios, and Germán Vidal. A theory of reversibility for Erlang. J. Log. Algebraic Methods Program., 100:71-97, 2018. URL: https://doi.org/10.1016/j.jlamp.2018.06.004.
  30. Ivan Lanese, Adrián Palacios, and Germán Vidal. Causal-consistent replay debugging for message passing programs. In Technical report, DSIC, Universitat Politecnica de Valencia, 2019. URL: http://personales.upv.es/gvidal/german/forte19tr/paper.pdf.
  31. Ivan Lanese, Adrián Palacios, and Germán Vidal. Causal-consistent replay debugging for message passing programs. In Formal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17-21, Proceedings, pages 167-184, 2019. URL: https://doi.org/10.1007/978-3-030-21759-4_10.
  32. Ivan Lanese, Iain C. C. Phillips, and Irek Ulidowski. An axiomatic approach to reversible computation. In Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, Proceedings, pages 442-461, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_23.
  33. Ivan Lanese, Davide Sangiorgi, and Gianluigi Zavattaro. Playing with bisimulation in Erlang. In Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, pages 71-91, 2019. URL: https://doi.org/10.1007/978-3-030-21485-2_6.
  34. Johan Sund Laursen, Ulrik Pagh Schultz, and Lars-Peter Ellekilde. Automatic error recovery in robot assembly operations using reverse execution. In 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2015, Hamburg, Germany, September 28 - October 2, pages 1785-1792. IEEE, 2015. URL: https://doi.org/10.1109/IROS.2015.7353609.
  35. Christopher Lutz. Janus: a time-reversible language. Letter to R. Landauer., 1986. URL: http://tetsuo.jp/ref/janus.html.
  36. James McNellis, Jordi Mola, and Ken Sykes. Time travel debugging: Root causing bugs in commercial scale software. CppCon talk, https://www.youtube.com/watch?v=l1YJTg_A914, 2017.
  37. Hernán C. Melgratti, Claudio Antares Mezzina, and Irek Ulidowski. Reversing P/T nets. In Hanne Riis Nielson and Emilio Tuosto, editors, Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17-21, Proceedings, volume 11533 of Lecture Notes in Computer Science, pages 19-36. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-22397-7_2.
  38. Claudio Antares Mezzina. On reversibility and broadcast. In Reversible Computation - 10th International Conference, RC 2018, Leicester, UK, September 12-14. Proceedings, volume 11106 of Lecture Notes in Computer Science, pages 67-83. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99498-7_5.
  39. Claudio Antares Mezzina and Jorge A. Pérez. Causally consistent reversible choreographies: a monitors-as-memories approach. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 - 11, 2017, pages 127-138. ACM, 2017. URL: https://doi.org/10.1145/3131851.3131864.
  40. Anna Philippou and Kyriaki Psara. Reversible computation in Petri nets. In Reversible Computation - 10th International Conference, RC 2018, Leicester, UK, September 12-14, Proceedings, pages 84-101, 2018. URL: https://doi.org/10.1007/978-3-319-99498-7_6.
  41. Iain Phillips, Irek Ulidowski, and Shoji Yuen. A reversible process calculus and the modelling of the ERK signalling pathway. In Reversible Computation, 4th International Workshop, RC 2012, Copenhagen, Denmark, July 2-3. Revised Papers, pages 218-232, 2012. URL: https://doi.org/10.1007/978-3-642-36315-3_18.
  42. Iain C. C. Phillips and Irek Ulidowski. Reversing algebraic process calculi. J. Log. Algebraic Methods Program., 73(1-2):70-96, 2007. URL: https://doi.org/10.1016/j.jlap.2006.11.002.
  43. Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebraic Methods Program., 60-61:17-139, 2004. Google Scholar
  44. Davide Sangiorgi. Bisimulation for higher-order process calculi. Inf. Comput., 131(2):141-178, 1996. URL: https://doi.org/10.1006/inco.1996.0096.
  45. Vladimiro Sassone, Mogens Nielsen, and Glynn Winskel. Models of concurrency: Towards a classification. Theoretical Computer Science, 170(1-2):297-348, 1996. URL: https://doi.org/10.1016/S0304-3975(96)80710-9.
  46. Ulrik Pagh Schultz. Reversible object-oriented programming with region-based memory management - work-in-progress report. In RC, volume 11106 of Lecture Notes in Computer Science, pages 322-328. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99498-7_22.
  47. Irek Ulidowski, Iain Phillips, and Shoji Yuen. Reversing event structures. New Generation Comput., 36(3):281-306, 2018. URL: https://doi.org/10.1007/s00354-018-0040-8.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail