Document Open Access Logo

Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Brave New Idea Paper)

Authors Carmen Torres Lopez , Robbert Gurdeep Singh , Stefan Marr , Elisa Gonzalez Boix, Christophe Scholliers

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2019.27.pdf
  • Filesize: 2.11 MB
  • 30 pages

Document Identifiers

Author Details

Carmen Torres Lopez
  • Vrije Universiteit Brussel, Belgium
Robbert Gurdeep Singh
  • Universiteit Gent, Belgium
Stefan Marr
  • School of Computing, University of Kent, United Kingdom
Elisa Gonzalez Boix
  • Vrije Universiteit Brussel, Belgium
Christophe Scholliers
  • Universiteit Gent, Belgium

Funding

  • Torres Lopez, Carmen: Funded by FWO Research Foundation Flanders (FWO), project number G004816N.
  • Gurdeep Singh, Robbert: Doctoral fellowship from the Special Research Fund (BOF) of Ghent University (reference number: BOF18/DOC/327).

Acknowledgements

We would like to thank Thomas Dupriez (ENS Paris-Saclay - RMoD, Inria, Lille-Nord Europe) for an initial implementation of the underlying visualization and reduction code.

Cite As Get BibTex

Carmen Torres Lopez, Robbert Gurdeep Singh, Stefan Marr, Elisa Gonzalez Boix, and Christophe Scholliers. Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Brave New Idea Paper). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 27:1-27:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ECOOP.2019.27

Abstract

Many of today’s software systems are parallel or concurrent. With the rise of Node.js and more generally event-loop architectures, many systems need to handle concurrency. However, its non-deterministic behavior makes it hard to reproduce bugs. Today’s interactive debuggers unfortunately do not support developers in debugging non-deterministic issues. They only allow us to explore a single execution path. Therefore, some bugs may never be reproduced in the debugging session, because the right conditions are not triggered.
As a solution, we propose multiverse debugging, a new approach for debugging non-deterministic programs that allows developers to observe all possible execution paths of a parallel program and debug it interactively. We introduce the concepts of multiverse breakpoints and stepping, which can halt a program in different execution paths, i.e. universes. We apply multiverse debugging to AmbientTalk, an actor-based language, resulting in Voyager, a multiverse debugger implemented on top of the AmbientTalk operational semantics. We provide a proof of non-interference, i.e., we prove that observing the behavior of a program by the debugger does not affect the behavior of that program and vice versa. Multiverse debugging establishes the foundation for debugging non-deterministic programs interactively, which we believe can aid the development of parallel and concurrent systems.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Concurrent programming languages
  • Software and its engineering → Software testing and debugging
Keywords
  • Debugging
  • Parallelism
  • Concurrency
  • Actors
  • Formal Semantics

Metrics

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

Supplementary Materials

References

  1. Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Test Case Generation of Actor Systems. In Bernd Finkbeiner, Geguang Pu, and Lijun Zhang, editors, ATVA, volume 9364 of Lecture Notes in Computer Science, pages 259-275. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-24953-7_21.
  2. Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Systematic testing of actor systems. Softw. Test., Verif. Reliab., 28(3), 2018. URL: http://dx.doi.org/10.1002/stvr.1661.
  3. Thanassis Avgerinos, Alexandre Rebert, Sang Kil Cha, and David Brumley. Enhancing symbolic execution with veritesting. In Pankaj Jalote, Lionel C. Briand, and André van der Hoek, editors, ICSE, pages 1083-1094. ACM, 2014. URL: http://dx.doi.org/10.1145/2568225.2568293.
  4. Thibaut Balabonski, François Pottier, and Jonathan Protzenko. Type Soundness and Race Freedom for Mezzo. In Michael Codish and Eijiro Sumii, editors, Functional and Logic Programming, pages 253-269, Cham, 2014. Springer International Publishing. URL: http://dx.doi.org/10.1007/978-3-319-07151-0_16.
  5. Roberto Baldoni, Emilio Coppa, Daniele Cono D'elia, Camil Demetrescu, and Irene Finocchi. A Survey of Symbolic Execution Techniques. ACM Comput. Surv., 51(3):50:1-50:39, May 2018. URL: http://dx.doi.org/10.1145/3182657.
  6. Earl T. Barr, Mark Marron, Ed Maurer, Dan Moseley, and Gaurav Seth. Time-travel Debugging for JavaScript/Node.Js. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, pages 1003-1007. ACM, 2016. URL: http://dx.doi.org/10.1145/2950290.2983933.
  7. Tom Bergan, Dan Grossman, and Luis Ceze. Symbolic execution of multithreaded programs from arbitrary program contexts. In Andrew P. Black and Todd D. Millstein, editors, OOPSLA, pages 491-506. ACM, 2014. URL: http://dx.doi.org/10.1145/2660193.2660200.
  8. Karen L. Bernstein and Eugene W. Stark. Operational Semantics of a Focusing Debugger. Electronic Notes in Theoretical Computer Science, 1:13-31, 1995. MFPS XI, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference. URL: http://dx.doi.org/10.1016/S1571-0661(04)80002-1.
  9. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic Model Checking Without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS '99, pages 193-207, Berlin, Heidelberg, 1999. Springer-Verlag. URL: http://dx.doi.org/10.1007/3-540-49059-0_14.
  10. Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. Ownership Types for Safe Programming: Preventing Data Races and Deadlocks. In Proceedings of the 17th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA '02, pages 211-230, New York, NY, USA, 2002. ACM. URL: http://dx.doi.org/10.1145/582419.582440.
  11. Gilad Bracha, Peter von der Ahé, Vassili Bykov, Yaron Kashai, William Maddox, and Eliot Miranda. Modules as Objects in Newspeak. In Theo D'Hondt, editor, ECOOP 2010 - Object-Oriented Programming, volume 6183 of LNCS, pages 405-428. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14107-2_20.
  12. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic Model Checking: 10^20 States and Beyond. In LICS, pages 428-439. IEEE Computer Society, 1990. URL: http://dx.doi.org/10.1016/0890-5401(92)90017-A.
  13. Rafael Caballero, Enrique Martin-Martin, Adrián Riesco, and Salvador Tamarit. Declarative debugging of concurrent Erlang programs. Journal of Logical and Algebraic Methods in Programming, 101:22-41, 2018. URL: http://dx.doi.org/10.1016/j.jlamp.2018.07.005.
  14. Cristian Cadar and Koushik Sen. Symbolic Execution for Software Testing: Three Decades Later. Commun. ACM, 56(2):82-90, February 2013. URL: http://dx.doi.org/10.1145/2408776.2408795.
  15. M. Christakis, A. Gotovos, and K. Sagonas. Systematic Testing for Detecting Concurrency Errors in Erlang Programs. In 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation, pages 154-163, March 2013. Google Scholar
  16. Maria Christakis, Alkis Gotovos, and Konstantinos F. Sagonas. Systematic Testing for Detecting Concurrency Errors in Erlang Programs. In ICST, pages 154-163. IEEE Computer Society, 2013. Google Scholar
  17. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Progress on the State Explosion Problem in Model Checking. In Reinhard Wilhelm, editor, Informatics, volume 2000 of Lecture Notes in Computer Science, pages 176-194. Springer, 2001. URL: http://dx.doi.org/10.1007/3-540-44577-3_12.
  18. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. URL: http://dx.doi.org/10.1007/978-3-319-10575-8.
  19. Fabio Q. B. da Silva. Correctness proofs of compilers and debuggers: an approach based on structural operational semantics. PhD thesis, University of Edinburgh, UK, 1992. British Library, EThOS. URL: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.649061.
  20. Emanuele D'Osualdo, Jonathan Kochems, and C. H. Luke Ong. Automatic Verification of Erlang-Style Concurrency. In Francesco Logozzo and Manuel Fähndrich, editors, 20th International Symposium on Static Analysis, SAS 2013, pages 454-476. Springer, June 2013. URL: http://dx.doi.org/10.1007/978-3-642-38856-9_24.
  21. Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo, and Emilio Tuosto. Debugging Distributed Systems with Causal Nets. ECEASST, 14:1-10, 2008. URL: http://dx.doi.org/10.14279/tuj.eceasst.14.190.181.
  22. GianLuigi Ferrari and Emilio Tuosto. A Debugging Calculus for Mobile Ambients. In Proceedings of the 2001 ACM Symposium on Applied Computing, SAC '01, page 2, New York, NY, USA, 2001. ACM. URL: http://dx.doi.org/10.1145/372202.380701.
  23. Cormac Flanagan and Stephen N. Freund. Type-based Race Detection for Java. In Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, PLDI '00, pages 219-232, New York, NY, USA, 2000. ACM. URL: http://dx.doi.org/10.1145/349299.349328.
  24. Lars-Ake Fredlund, Dilian Gurov, Thomas Noll, Mads Dam, Thomas Arts, and Gennady Chugunov. A verification tool for ERLANG. STTT, 4(4):405-420, 2003. URL: http://dx.doi.org/10.1007/s100090100071.
  25. Jason Gait. A probe effect in concurrent programs. Software: Practice and Experience, 16(3):225-233, 1986. URL: http://dx.doi.org/10.1002/spe.4380160304.
  26. Elena Giachino, Carlo A. Grazia, Cosimo Laneve, Michael Lienhardt, and Peter Y. H. Wong. Deadlock Analysis of Concurrent Objects: Theory and Practice. In Einar Broch Johnsen and Luigia Petre, editors, Integrated Formal Methods, pages 394-411, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/978-3-642-38613-8_27.
  27. Elena Giachino, Ivan Lanese, and Claudio Antares Mezzina. Causal-Consistent Reversible Debugging. In Stefania Gnesi and Arend Rensink, editors, FASE, volume 8411 of Lecture Notes in Computer Science, pages 370-384. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54804-8_26.
  28. Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: Directed Automated Random Testing. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '05, pages 213-223, New York, NY, USA, 2005. ACM. URL: http://dx.doi.org/10.1145/1065010.1065036.
  29. Elisa Gonzalez Boix, Carlos Noguera, and Wolfgang De Meuter. Distributed Debugging for Mobile Networks . Journal of Systems and Software, 90:76-90, 2014. URL: http://dx.doi.org/10.1016/j.jss.2013.11.1099.
  30. Shengjian Guo, Markus Kusano, and Chao Wang. Conc-iSE: Incremental Symbolic Execution of Concurrent Software. In Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, pages 531-542, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2970276.2970332.
  31. K. Havelund and T. Pressburger. Model Checking Java Programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2(4), 1998. URL: http://dx.doi.org/10.1007/s100090050043.
  32. Carl Hewitt, Peter Bishop, and Richard Steiger. A Universal Modular ACTOR Formalism for Artificial Intelligence. In IJCAI'73: Proceedings of the 3rd International Joint Conference on Artificial Intelligence, pages 235-245. Morgan Kaufmann, 1973. Google Scholar
  33. Frank Huch. Verification of Erlang Programs Using Abstract Interpretation and Model Checking. In Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming, ICFP '99, pages 261-272, New York, NY, USA, 1999. ACM. URL: http://dx.doi.org/10.1145/317636.317908.
  34. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst., 23(3):396-450, 2001. URL: http://dx.doi.org/10.1145/503502.503505.
  35. Mohammad Mahdi Jaghoori, Frank S. de Boer, Delphine Longuet, Tom Chothia, and Marjan Sirjani. Compositional schedulability analysis of real-time actor-based systems. Acta Inf., 54(4):343-378, 2017. URL: http://dx.doi.org/10.1007/s00236-015-0254-x.
  36. Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. Effective stateless model checking for C/C++ concurrency. PACMPL, 2(POPL):17:1-17:32, 2018. URL: http://dx.doi.org/10.1145/3158105.
  37. Ivan Lanese, Naoki Nishida, Adrián Palacios, and Germán Vidal. CauDEr: A Causal-Consistent Reversible Debugger for Erlang. In John P. Gallagher and Martin Sulzmann, editors, Functional and Logic Programming, volume 10818 of FLOPS'18, pages 247-263, Cham, 2018. Springer. URL: http://dx.doi.org/10.1007/978-3-319-90686-7_16.
  38. Steven Lauterburg, Mirco Dotta, Darko Marinov, and Gul Agha. A Framework for State-Space Exploration of Java-Based Actor Programs. In Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, ASE '09, pages 468-479, Washington, DC, USA, 2009. IEEE Computer Society. URL: http://dx.doi.org/10.1109/ASE.2009.88.
  39. Steven Lauterburg, Rajesh K. Karmani, Darko Marinov, and Gul Agha. Basset: A Tool for Systematic Testing of Actor Programs. In Proceedings of the Eighteenth ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE '10, pages 363-364, New York, NY, USA, 2010. ACM. URL: http://dx.doi.org/10.1145/1882291.1882349.
  40. He Li, Jie Luo, and Wei Li. A formal semantics for debugging synchronous message passing-based concurrent programs. Science China Information Sciences, 57(12):1-18, December 2014. URL: http://dx.doi.org/10.1007/s11432-014-5150-4.
  41. Sihan Li, Farah Hariri, and Gul Agha. Targeted Test Generation for Actor Systems. In Todd D. Millstein, editor, ECOOP, volume 109 of LIPIcs, pages 8:1-8:31. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2018.8.
  42. Yude Lin. Symbolic execution with over-approximation. PhD thesis, The University of Melbourne, 2017. Google Scholar
  43. Yude Lin, Tim Miller, and Harald Søndergaard. Compositional Symbolic Execution: Incremental Solving Revisited. In Alex Potanin, Gail C. Murphy, Steve Reeves, and Jens Dietrich, editors, APSEC, pages 273-280. IEEE Computer Society, 2016. URL: http://dx.doi.org/10.1109/ASWEC.2015.32.
  44. Kasper Søe Luckow, Corina S. Pasareanu, Matthew B. Dwyer, Antonio Filieri, and Willem Visser. Exact and approximate probabilistic symbolic execution for nondeterministic programs. In Ivica Crnkovic, Marsha Chechik, and Paul Grünbacher, editors, ASE, pages 575-586. ACM, 2014. URL: http://dx.doi.org/10.1145/2642937.2643011.
  45. Yong Luo and Olaf Chitil. Proving the correctness of algorithmic debugging for functional programs. In Henrik Nilsson, editor, Trends in Functional Programming, volume 7 of Trends in Functional Programming, pages 19-34. Intellect, 2006. Google Scholar
  46. Stefan Marr, Carmen Torres Lopez, Dominik Aumayr, Elisa Gonzalez Boix, and Hanspeter Mössenböck. A Concurrency-Agnostic Protocol for Multi-Paradigm Concurrent Debugging Tools. In Davide Ancona, editor, Proceedings of the 13th Symposium on Dynamic Languages, pages 3-14. ACM, 2017. URL: http://dx.doi.org/10.1145/3133841.3133842.
  47. John McCarthy. A Basis for a Mathematical Theory of Computation, Preliminary Report. In Papers Presented at the May 9-11, 1961, Western Joint IRE-AIEE-ACM Computer Conference, IRE-AIEE-ACM '61 (Western), pages 225-238, New York, NY, USA, 1961. ACM. URL: http://dx.doi.org/10.1145/1460690.1460715.
  48. Charles E McDowell and David P Helmbold. Debugging concurrent programs. ACM Computing Surveys (CSUR), 21(4):593-622, 1989. URL: http://dx.doi.org/10.1145/76894.76897.
  49. Mark S Miller, E Dean Tribble, and Jonathan Shapiro. Concurrency among strangers. In International Symposium on Trustworthy Global Computing, pages 195-229. Springer, 2005. URL: http://dx.doi.org/10.1007/11580850_12.
  50. Stijn Mostinckx, Tom Van Cutsem, Stijn Timbermont, Elisa Gonzalez Boix, Éric Tanter, and Wolfgang De Meuter. Mirror-based reflection in AmbientTalk. Softw. Pract. Exper., 39(7):661-699, 2009. URL: http://dx.doi.org/10.1002/spe.v39:7.
  51. Madanlal Musuvathi and Shaz Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In Jeanne Ferrante and Kathryn S. McKinley, editors, PLDI, pages 446-455. ACM, 2007. URL: http://dx.doi.org/10.1145/1250734.1250785.
  52. Naoki Nishida, Adrián Palacios, and Germán Vidal. A Reversible Semantics for Erlang. In Manuel V. Hermenegildo and Pedro López-García, editors, LOPSTR, volume 10184 of Lecture Notes in Computer Science, pages 259-274. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-63139-4_15.
  53. Michael Perscheid, Benjamin Siegmund, Marcel Taeumel, and Robert Hirschfeld. Studying the advancement in debugging practice of professional software developers. Software Quality Journal, 25(1):83-110, 2016. URL: http://dx.doi.org/10.1007/s11219-015-9294-2.
  54. Koushik Sen and Gul Agha. Automated Systematic Testing of Open Distributed Programs. In Luciano Baresi and Reiko Heckel, editors, FASE, volume 3922 of Lecture Notes in Computer Science, pages 339-356. Springer, 2006. URL: http://dx.doi.org/10.1007/11693017_25.
  55. Koushik Sen and Gul Agha. CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, pages 419-423, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/11817963_38.
  56. Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An interaction-based language and its typing system. In Costas Halatsis, Dimitrios Maritsas, George Philokyprou, and Sergios Theodoridis, editors, PARLE'94 Parallel Architectures and Languages Europe, pages 398-413, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/3-540-58184-7_118.
  57. Samira Tasharofi, Rajesh K. Karmani, Steven Lauterburg, Axel Legay, Darko Marinov, and Gul Agha. TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs. In Holger Giese and Grigore Rosu, editors, Formal Techniques for Distributed Systems: Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012. Proceedings, pages 219-234. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-30793-5_14.
  58. Stefan Tilkov and Steve Vinoski. Node.js: Using JavaScript to Build High-Performance Network Programs. IEEE Internet Computing, 14(6):80-83, November 2010. URL: http://dx.doi.org/10.1109/MIC.2010.145.
  59. Carmen Torres Lopez, Elisa Gonzalez Boix, Christophe Scholliers, Stefan Marr, and Hanspeter Mössenböck. A Principled Approach Towards Debugging Communicating Event-loops. In Proceedings of the 7th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE!'17, pages 41-49. ACM, October 2017. URL: http://dx.doi.org/10.1145/3141834.3141839.
  60. Carmen Torres Lopez, Stefan Marr, Elisa Gonzalez Boix, and Hanspeter Mössenböck. A Study of Concurrency Bugs and Advanced Development Support for Actor-based Programs, chapter 6, pages 155-185. Springer International Publishing, Cham, 2018. URL: http://dx.doi.org/10.1007/978-3-030-00302-9_6.
  61. Antti Valmari. The state explosion problem, chapter 9, pages 429-528. Springer Berlin Heidelberg, Berlin, Heidelberg, 1998. URL: http://dx.doi.org/10.1007/3-540-65306-6_21.
  62. Tom Van Cutsem, Elisa Gonzalez Boix, Christophe Scholliers, Andoni Lombide Carreton, Dries Harnie, Kevin Pinte, and Wolfgang De Meuter. AmbientTalk: programming responsive mobile peer-to-peer applications with actors. Computer Languages, Systems & Structures, 40(3-4):112-136, 2014. URL: http://dx.doi.org/10.1016/j.cl.2014.05.002.
  63. Simon Van Mierlo and Hans Vangheluwe. Debugging non-determinism: a petrinets modelling, analysis, and debugging tool. In CEUR workshop proceedings, volume 2019, pages 460-462, 2017. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact