Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

From Reversible Semantics to Reversible Debugging

  • Conference paper
  • First Online:
Reversible Computation (RC 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11106))

Included in the following conference series:

Abstract

This paper presents a line of research in reversible computing for concurrent systems. This line of research started in 2004 with the definition of the first reversible extensions for concurrent process calculi such as CCS, and is currently heading to the production of practical reversible debuggers for concurrent languages such as Erlang. Main questions that had to be answered during the research include the following. Which is the correct notion of reversibility for concurrent systems? Which history information needs to be stored? How to control the basic reversibility mechanism? How to exploit reversibility for debugging? How to apply reversible debugging to real languages?

This work has been partially supported by COST Action IC1405 on Reversible Computation - extending horizons of computing. We thank Germán Vidal, Adrián Palacios and Irek Ulidowski for their useful comments and help.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    We use the term process to denote a sequential flow of execution, actually referring to both processes and/or threads.

  2. 2.

    Concurrency alone is not enough. If the natural notion of switchability, allowing one to switch all pairs of concurrent actions, is chosen then all possible traces are causal equivalent.

References

  1. Actoverse website. https://github.com/45deg/Actoverse

  2. Akgul, T., Mooney III, V.J.: Assembly instruction level reverse execution for debugging. ACM Trans. Softw. Eng. Methodol. 13(2), 149–198 (2004)

    Article  Google Scholar 

  3. Akka. http://akka.io/

  4. Altenkirch, T., Grattage, J.: A functional quantum programming language. In: LICS, pp. 249–258. IEEE Computer Society (2005)

    Google Scholar 

  5. Boreale, M., Sangiorgi, D.: A fully abstract semantics for causality in the pi-calculus. Acta Inf. 35(5), 353–400 (1998)

    Article  Google Scholar 

  6. Britton, T., Jeng, L., Carver, G., Cheak, P., Katzenellenbogen, T.: Reversible debugging software - quantify the time and cost saved using reversible debuggers (2012). http://www.roguewave.com

  7. Caballero, R., Martin-Martin, E., Riesco, A., Tamarit, S.: EDD: a declarative debugger for sequential Erlang programs. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 581–586. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_49

    Chapter  Google Scholar 

  8. Cardelli, L., Laneve, C.: Reversible structures. In: CMSB, pp. 131–140. ACM (2011)

    Google Scholar 

  9. Carlsson, R., Gustavsson, B., Johansson, E., Lindgren, T., Nyström, S.O., Pettersson, M., Virding, R.: Core Erlang 1.0.3. Language specification (2004). https://www.it.uu.se/research/group/hipe/cerl/doc/core_erlang-1.0.3.pdf

  10. Carothers, C.D., Perumalla, K.S., Fujimoto, R.: Efficient optimistic parallel simulations using reverse computation. ACM Trans. Model. Comput. Simul. 9(3), 224–253 (1999)

    Article  Google Scholar 

  11. Cingolani, D., Pellegrini, A., Quaglia, F.: Transparently mixing undo logs and software reversibility for state recovery in optimistic PDES. In: PADS, pp. 211–222. ACM (2015)

    Google Scholar 

  12. Cristescu, I.D., Krivine, J., Varacca, D.: A compositional semantics for the reversible pi-calculus. In: LICS, pp. 388–397. IEEE Press (2013)

    Google Scholar 

  13. Cristescu, I.D., Krivine, J., Varacca, D.: Rigid families for CCS and the \(\pi \)-calculus. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 223–240. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25150-9_14

    Chapter  Google Scholar 

  14. Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 292–307. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_19

    Chapter  Google Scholar 

  15. Degano, P., Priami, C.: Non-interleaving semantics for mobile processes. Theor. Comput. Sci. 216(1–2), 237–270 (1999)

    Article  MathSciNet  Google Scholar 

  16. Frank, M.P.: Introduction to reversible computing: motivation, progress, and challenges. In: 2nd Conference on Computing Frontiers, pp. 385–390. ACM (2005)

    Google Scholar 

  17. Giachino, E., Lanese, I., Mezzina, C.A.: CaReDeb. http://www.cs.unibo.it/caredeb

  18. Giachino, E., Lanese, I., Mezzina, C.A.: Causal-consistent reversible debugging. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 370–384. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54804-8_26

    Chapter  Google Scholar 

  19. Giachino, E., Lanese, I., Mezzina, C.A., Tiezzi, F.: Causal-consistent rollback in a tuple-based language. J. Log. Algebr. Meth. Program. 88, 99–120 (2017)

    Article  MathSciNet  Google Scholar 

  20. Haulund, T., Mogensen, T.Æ., Glück, R.: Implementing reversible object-oriented language features on reversible machines. In: Phillips, I., Rahaman, H. (eds.) RC 2017. LNCS, vol. 10301, pp. 66–73. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-59936-6_5

    Chapter  MATH  Google Scholar 

  21. Hewitt, C., Bishop, P.B., Steiger, R.: A universal modular ACTOR formalism for artificial intelligence. In: IJCAI, pp. 235–245. William Kaufmann (1973)

    Google Scholar 

  22. Hoey, J., Ulidowski, I., Yuen, S.: Reversing imperative parallel programs. In: EXPRESS/SOS. EPTCS, vol. 255, pp. 51–66 (2017)

    Google Scholar 

  23. Huang, J., Zhang, C.: Debugging concurrent software: advances and challenges. J. Comput. Sci. Technol. 31(5), 861–868 (2016)

    Article  Google Scholar 

  24. Landauer, R.: Irreversibility and heat generated in the computing process. IBM J. Res. Dev. 5, 183–191 (1961)

    Article  Google Scholar 

  25. Lanese, I., Lienhardt, M., Mezzina, C.A., Schmitt, A., Stefani, J.-B.: Concurrent flexible reversibility. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 370–390. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_21

    Chapter  Google Scholar 

  26. Lanese, I., Mezzina, C.A., Schmitt, A., Stefani, J.-B.: Controlling reversibility in higher-order Pi. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 297–311. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23217-6_20

    Chapter  Google Scholar 

  27. Lanese, I., Mezzina, C.A., Stefani, J.-B.: Controlled reversibility and compensations. In: Glück, R., Yokoyama, T. (eds.) RC 2012. LNCS, vol. 7581, pp. 233–240. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36315-3_19

    Chapter  Google Scholar 

  28. Lanese, I., Mezzina, C.A., Stefani, J.B.: Reversibility in the higher-order \(\pi \)-calculus. Theor. Comput. Sci. 625, 25–84 (2016)

    Article  MathSciNet  Google Scholar 

  29. Lanese, I., Nishida, N., Palacios, A., Vidal, G.: CauDEr. https://github.com/mistupv/cauder

  30. Lanese, I., Nishida, N., Palacios, A., Vidal, G.: CauDEr: a causal-consistent reversible debugger for Erlang. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 247–263. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-90686-7_16

    Chapter  Google Scholar 

  31. Lanese, I., Nishida, N., Palacios, A., Vidal, G.: A theory of reversibility for Erlang. J. Logical Algebraic Methods Program. 100, 71–97 (2018)

    Article  Google Scholar 

  32. 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)

    Google Scholar 

  33. Lienhardt, M., Lanese, I., Mezzina, C.A., Stefani, J.-B.: A reversible abstract machine and its space overhead. In: Giese, H., Rosu, G. (eds.) FMOODS/FORTE -2012. LNCS, vol. 7273, pp. 1–17. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30793-5_1

    Chapter  Google Scholar 

  34. 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)

  35. Mezzina, C.A.: On reversibility and broadcast. In: Kari, J., Ulidowski, I. (eds.) RC 2018. LNCS, vol. 11106, pp. 67–83. Springer, Cham (2018)

    Google Scholar 

  36. Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. J. Logic Algebraic Program. 73(1–2), 70–96 (2007)

    Article  Google Scholar 

  37. 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 2012. LNCS, vol. 7581, pp. 218–232. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36315-3_18

    Chapter  MATH  Google Scholar 

  38. Schordan, M., Jefferson, D., Barnes, P., Oppelstrup, T., Quinlan, D.: Reverse code generation for parallel discrete event simulation. In: Krivine, J., Stefani, J.-B. (eds.) RC 2015. LNCS, vol. 9138, pp. 95–110. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20860-2_6

    Chapter  Google Scholar 

  39. Shibanai, K., Watanabe, T.: Actoverse: a reversible debugger for actors. In: AGERE@SPLASH, pp. 50–57. ACM (2017)

    Google Scholar 

  40. Sutter, H.: The free lunch is over: a fundamental turn toward concurrency in software. Dr. Dobbs J. 30(3), 202–210 (2005)

    Google Scholar 

  41. TCP example from EDD github repository. https://github.com/tamarit/edd/tree/master/examples/Concurrency/tcp

  42. Undo Software: Undodb, commercial reversible debugger. http://undo-software.com/

  43. Undo Software: Increasing software development productivity with reversible debugging (2014). http://undo-software.com/wp-content/uploads/2014/10/Increasing-software-development-productivity-with-reversible-debugging.pdf

  44. Yokoyama, T., Axelsen, H.B., Glück, R.: Towards a reversible functional language. In: De Vos, A., Wille, R. (eds.) RC 2011. LNCS, vol. 7165, pp. 14–29. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29517-1_2

    Chapter  MATH  Google Scholar 

  45. Yokoyama, T., Glück, R.: A reversible programming language and its invertible self-interpreter. In: PEPM, pp. 144–153. ACM (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Focus Team, University of Bologna/Inria, Bologna, Italy

    Ivan Lanese

Authors
  1. Ivan Lanese
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ivan Lanese .

Editor information

Editors and Affiliations

  1. University of Turku, Turku, Finland

    Jarkko Kari

  2. University of Leicester, Leicester, United Kingdom

    Irek Ulidowski

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lanese, I. (2018). From Reversible Semantics to Reversible Debugging. In: Kari, J., Ulidowski, I. (eds) Reversible Computation. RC 2018. Lecture Notes in Computer Science(), vol 11106. Springer, Cham. https://doi.org/10.1007/978-3-319-99498-7_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-99498-7_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-99497-0

  • Online ISBN: 978-3-319-99498-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation