nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

CauDEr: A Causal-Consistent Reversible Debugger for Erlang

verfasst von : Ivan Lanese, Naoki Nishida, Adrián Palacios, Germán Vidal

Erschienen in: Functional and Logic Programming

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel A Common Framework Using Expected Types for Several Type Debugging Approaches

Nächstes Kapitel Cheap Remarks About Concurrent Programs

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

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.

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

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_49CrossRef

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

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

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_19CrossRef

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_24CrossRef

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

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_26CrossRef

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)MathSciNetCrossRef

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

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)

11.

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

12.

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

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_1CrossRef

15.

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

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)

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_15CrossRef

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)

19.

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

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)

Titel: CauDEr: A Causal-Consistent Reversible Debugger for Erlang
verfasst von: Ivan Lanese
Naoki Nishida
Adrián Palacios
Germán Vidal
Verlag: Springer International Publishing
Buch: Functional and Logic Programming
Print ISBN: 978-3-319-90685-0

Electronic ISBN: 978-3-319-90686-7

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-90686-7_16

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner