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

CauDEr: A Causal-Consistent Reversible Debugger for Erlang

  • Conference paper
  • First Online:
Functional and Logic Programming (FLOPS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10818))

Included in the following conference series:

Abstract

Programming languages based on the actor model, such as Erlang, avoid some concurrency bugs by design. However, other concurrency bugs, such as message order violations and livelocks, can still show up in programs. These hard-to-find bugs can be more easily detected by using causal-consistent reversible debugging, a debugging technique that allows one to traverse a computation both forward and backward. Most notably, causal consistency implies that, when going backward, an action can only be undone provided that its consequences, if any, have been undone beforehand. To the best of our knowledge, we present the first causal-consistent reversible debugger for Erlang, which may help programmers to detect and fix various kinds of bugs, including message order violations and livelocks.

This work has been partially supported by MINECO/AEI/FEDER (EU) under grant TIN2016-76843-C4-1-R, by the Generalitat Valenciana under grant PROMETEO-II/2015/013 (SmartLogic), by COST Action IC1405 on Reversible Computation - extending horizons of computing, and by JSPS KAKENHI Grant Number JP17H01722.

A. Palacios—Partially supported by the EU (FEDER) and the Spanish Ayudas para contratos predoctorales para la formación de doctores and Ayudas a la movilidad predoctoral para la realización de estancias breves en centros de I+D, MINECO (SEIDI), under FPI grants BES-2014-069749 and EEBB-I-16-11469.

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.

    Because of lack of space, we are not presenting the rules of \(\xrightarrow {\ell }\) here, but refer the interested reader to [13].

  2. 2.

    Actually, in this work, we only consider a single rollback request at a time, so \(\varPsi \) is always a singleton. Nevertheless, our formalisation considers that \(\varPsi \) is a set for notational convenience and, also, in order to accept multiple rollbacks in the future.

  3. 3.

    Actually, in CauDEr, uniqueness of variable names is enforced via renaming.

References

  1. 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 

  2. Carlsson, R., et al.: Core Erlang 1.0.3 language specification (2004). https://www.it.uu.se/research/group/hipe/cerl/doc/core_erlang-1.0.3.pdf

  3. Claessen, K., et al.: Finding race conditions in Erlang with QuickCheck and PULSE. In: ICFP, pp. 149–160. ACM (2009)

    Google Scholar 

  4. 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 

  5. D’Osualdo, E., Kochems, J., Ong, C.-H.L.: Automatic verification of Erlang-style concurrency. In: Logozzo, F., Fäahndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 454–476. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38856-9_24

    Chapter  Google Scholar 

  6. Fredlund, L.A., Svensson, H.: McErlang: a model checker for a distributed functional programming language. In: ICFP, pp. 125–136. ACM (2007)

    Article  Google Scholar 

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

  8. 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 

  9. Giantsios, A., Papaspyrou, N., Sagonas, K.: Concolic testing for functional languages. In: PPDP, pp. 137–148. ACM (2015)

    Google Scholar 

  10. Gotovos, A., Christakis, M., Sagonas, K.: Test-driven development of concurrent programs using Concuerror. In: 10th ACM SIGPLAN Workshop on Erlang, pp. 51–61. ACM (2011)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  12. Lanese, I., Mezzina, C.A., Tiezzi, F.: Causal-consistent reversibility. Bull. EATCS 114, 19 (2014)

    Google Scholar 

  13. Lanese, I., Nishida, N., Palacios, A., Vidal, G.: A theory of reversibility for Erlang (2017). Submitted for publication. http://users.dsic.upv.es/~gvidal/lnpv17/paper.pdf

  14. 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 

  15. Lindahl, T., Sagonas, K.: Practical type inference based on success typings. In: PPDP, pp. 167–178. ACM Press (2006)

    Google Scholar 

  16. Lopez, C.T., Marr, S., Mössenböck, H., Boix, E.G.: A study of concurrency bugs and advanced development support for actor-based programs. CoRR abs/1706.07372 (2017)

    Google Scholar 

  17. Nishida, N., Palacios, A., Vidal, G.: A reversible semantics for Erlang. In: Hermenegildo, M.V., Lopez-Garcia, P. (eds.) LOPSTR 2016. LNCS, vol. 10184, pp. 259–274. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63139-4_15

    Chapter  Google Scholar 

  18. Papadakis, M., Sagonas, K.: A PropEr integration of types and function specifications with property-based testing. In: 10th ACM SIGPLAN Workshop on Erlang, pp. 39–50. ACM (2011)

    Google Scholar 

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

    Google Scholar 

  20. Stanley, T., Close, T., Miller, M.S.: Causeway: a message-oriented distributed debugger. Technical report, HPL-2009-78 (2009). http://www.hpl.hp.com/techreports/2009/HPL-2009-78.html

  21. Svensson, H., Fredlund, L.A., Earle, C.B.: A unified semantics for future Erlang. In: 9th ACM SIGPLAN Workshop on Erlang, pp. 23–32. ACM (2010)

    Google Scholar 

Download references

Acknowledgements

The authors gratefully acknowledge the anonymous referees for their useful comments and suggestions.

Author information

Authors and Affiliations

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

    Ivan Lanese

  2. Graduate School of Informatics, Nagoya University, Nagoya, Japan

    Naoki Nishida

  3. MiST, DSIC, Universitat Politècnica de València, Valencia, Spain

    Adrián Palacios & Germán Vidal

Authors
  1. Ivan Lanese
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Naoki Nishida
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Adrián Palacios
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Germán Vidal
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Germán Vidal .

Editor information

Editors and Affiliations

  1. Roskilde University, Roskilde, Denmark

    John P. Gallagher

  2. Karlsruhe University of Applied Sciences, Karlsruhe, Germany

    Martin Sulzmann

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lanese, I., Nishida, N., Palacios, A., Vidal, G. (2018). CauDEr: A Causal-Consistent Reversible Debugger for Erlang. In: Gallagher, J., Sulzmann, M. (eds) Functional and Logic Programming. FLOPS 2018. Lecture Notes in Computer Science(), vol 10818. Springer, Cham. https://doi.org/10.1007/978-3-319-90686-7_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-90686-7_16

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation