Abstract
Non-determinism in a concurrent or distributed setting may lead to many different runs or executions of a program. This paper presents a method to reproduce a specific run for non-deterministic actor or active object systems. The method is based on recording traces of events reflecting local transitions at so-called stable states during execution; i.e., states in which local execution depends on interaction with the environment. The paper formalizes trace recording and replay for a basic active object language, to show that such local traces suffice to obtain global reproducibility of runs; during replay different objects may operate fairly independently of each other and in parallel, yet a program under replay has guaranteed deterministic outcome. We then show that the method extends to the other forms of non-determinism as found in richer active object languages. Following the proposed method, we have implemented a tool to record and replay runs, and to visualize the communication and scheduling decisions of a recorded run, for Real-Time ABS, a formally defined, rich active object language for modeling timed, resource-aware behavior in distributed systems.
Chapter PDF
Similar content being viewed by others
References
Chen, Y., Zhang, S., Guo, Q., Li, L., Wu, R., Chen, T.: Deterministic replay: A survey. ACM Comput. Surv. 48(2) (September 2015) 17:1–17:47
de Boer, F., Serbanescu, V., Hähnle, R., Henrio, L., Rochas, J., Din, C.C., Johnsen, E.B., Sirjani, M., Khamespanah, E., Fernandez-Reyes, K., Yang, A.M.: A survey of active object languages. ACM Comput. Surv. 50(5) (October 2017) 76:1–76:39
Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: A core language for abstract behavioral specification. In Aichernig, B., de Boer, F.S., Bonsangue, M.M., eds.: Proc. 9th Intl. Symp. on Formal Methods for Components and Objects (FMCO 2010). Volume 6957 of Lecture Notes in Computer Science., Springer (2011) 142–164
Brandauer, S., Castegren, E., Clarke, D., Fernandez-Reyes, K., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L., Wrigstad, T., Yang, A.M.: Parallel objects for multicores: A glimpse at the parallel language encore. In: Formal Methods for Multicore Programming (SFM 2015). Volume 9104 of Lecture Notes in Computer Science., Springer (2015) 1–56
Schäfer, J., Poetzsch-Heffter, A.: JCoBox: Generalizing active objects to concurrent components. In D’Hondt, T., ed.: Proc. 24th European Conference on Object-Oriented Programming (ECOOP 2010). Volume 6183 of Lecture Notes in Computer Science., Springer (2010) 275–299
Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L.: Integrating deployment architectures and resource consumption in timed object-oriented models. J. Log. Algebr. Meth. Program. 84(1) (2015) 67–91
Albert, E., de Boer, F.S., Hähnle, R., Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L., Wong, P.Y.H.: Formal modeling and analysis of resource management for cloud architectures: an industrial case study using real-time ABS. Service Oriented Computing and Applications 8(4) (2014) 323–339
Kamburjan, E., Hähnle, R., Schön, S.: Formal modeling and analysis of railway operations with active objects. Sci. Comput. Program. 166 (2018) 167–193
Din, C.C., Tapia Tarifa, S.L., Hähnle, R., Johnsen, E.B.: History-based specification and verification of scalable concurrent and distributed systems. In: Proc. 17th Intl. Conf. on Formal Engineering Methods (ICFEM 2015). Volume 9407 of Lecture Notes in Computer Science., Springer (2015) 217–233
Bezirgiannis, N., de Boer, F.S., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L.: Implementing SOS with active objects: A case study of a multicore memory system. In: Proc. 22nd Intl. Conf. on Fundamental Approaches to Software Engineering (FASE 2019). Volume 11424 of Lecture Notes in Computer Science., Springer (2019) 332–350
Armstrong, J.: Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf Series. Pragmatic Bookshelf (2007)
Din, C.C., Owe, O.: A sound and complete reasoning system for asynchronous communication with shared futures. J. Log. Algebr. Meth. Program. 83(5-6) (2014) 360–383
Mazurkiewicz, A.W.: Trace theory. In Brauer, W., Reisig, W., Rozenberg, G., eds.: Advances in Petri Nets 1986. Volume 255 of Lecture Notes in Computer Science., Springer (1987) 279–324
Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Software and Systems Modeling 6(1) (2007) 39–58
Albert, E., Genaim, S., Gómez-Zamalloa, M., Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L.: Simulating concurrent behaviors with worst-case cost bounds. In Butler, M.J., Schulte, W., eds.: Proc. 17th International Symposium on Formal Methods (FM 2011). Volume 6664 of Lecture Notes in Computer Science., Springer (2011) 353–368
Bjørk, J., de Boer, F.S., Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L.: User-defined schedulers for real-time concurrent objects. Innovations in Systems and Software Engineering 9(1) (2013) 29–43
Schlatte, R., Johnsen, E.B., Mauro, J., Tapia Tarifa, S.L., Yu, I.C.: Release the beasts: When formal methods meet real world data. In: It’s All About Coordination - Essays to Celebrate the Lifelong Scientific Achievements of Farhad Arbab. Volume 10865 of Lecture Notes in Computer Science., Springer (2018) 107–121
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7) (1978) 558–565
Ronsse, M., Kranzlmüller, D.: Rolt\({}^{\text{mp}}\)-replay of Lamport timestamps for message passing systems. In: Proc. 6th Euromicro Workshop on Parallel and Distributed Processing (PDP’98), IEEE (1998) 87–93
Albert, E., Correas, J., Johnsen, E.B., Pun, V.K.I., Román-DÃez, G.: Parallel cost analysis. ACM Trans. Comput. Log. 19(4) (2018) 31:1–31:37
Albert, E., Gómez-Zamalloa, M., Isabel, M.: SYCO: a systematic testing tool for concurrent objects. In Zaks, A., Hermenegildo, M.V., eds.: Proc. 25th Intl. Conf. on Compiler Construction (CC 2016), ACM (2016) 269–270
LeBlanc, T.J., Mellor-Crummey, J.M.: Debugging parallel programs with instant replay. IEEE Trans. Computers 36(4) (1987) 471–482
Ronsse, M., Bosschere, K.D., de Kergommeaux, J.C.: Execution replay and debugging. In: AADEBUG. (2000)
Shibanai, K., Watanabe, T.: Actoverse: a reversible debugger for actors. In Koster, J.D., Bergenti, F., eds.: Proc. 7th Intl. Workshop on Programming Based on Actors, Agents, and Decentralized Control (AGERE 2017), ACM (2017) 50–57
Barr, E.T., Marron, M., Maurer, E., Moseley, D., Seth, G.: Time-travel debugging for javascript/node.js. In Zimmermann, T., Cleland-Huang, J., Su, Z., eds.: Proc. 24th Intl. Symp. on Foundations of Software Engineering (FSE 2016), ACM (2016) 1003–1007
Burg, B., Bailey, R., Ko, A.J., Ernst, M.D.: Interactive record/replay for web application debugging. In Izadi, S., Quigley, A.J., Poupyrev, I., Igarashi, T., eds.: Proc. 26th Symp. on User Interface Software and Technology (UIST’13), ACM (2013) 473–484
Aumayr, D., Marr, S., Béra, C., Boix, E.G., Mössenböck, H.: Efficient and deterministic record & replay for actor languages. In Tilevich, E., Mössenböck, H., eds.: Proc. 15th Intl. Conf. on Managed Languages & Runtimes (ManLang’18), ACM (2018) 15:1–15:14
de Kergommeaux, J.C., Ronsse, M., Bosschere, K.D.: MPL*: Efficient record/play of nondeterministic features of message passing libraries. In Dongarra, J.J., Luque, E., Margalef, T., eds.: Recent Advances in Parallel Virtual Machine and Message Passing Interface, proc. 6th European PVM/MPI Users’ Group Meeting. Volume 1697 of Lecture Notes in Computer Science., Springer (1999) 141–148
Netzer, R.H.B., Miller, B.P.: Optimal tracing and replay for debugging message-passing parallel programs. The Journal of Supercomputing 8(4) (1995) 371–388
Lanese, I., Palacios, A., Vidal, G.: Causal-consistent replay debugging for message passing programs. In Pérez, J.A., Yoshida, N., eds.: Proc. 39th Intl. Conf. on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2019). Volume 11535 of Lecture Notes in Computer Science., Springer (2019) 167–184
Lanese, I., Nishida, N., Palacios, A., Vidal, G.: Cauder: A causal-consistent reversible debugger for erlang. In Gallagher, J.P., Sulzmann, M., eds.: Proc. 14th Intl. Symp. on Functional and Logic Programming (FLOPS 2018). Volume 10818 of Lecture Notes in Computer Science., Springer (2018) 247–263
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In Palsberg, J., Abadi, M., eds.: Proc. 32nd Symp. on Principles of Programming Languages (POPL 2005), ACM (2005) 110–121
Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In Jagannathan, S., Sewell, P., eds.: Proc. 41st Symposium on Principles of Programming Languages (POPL’14), ACM (2014) 373–384
Albert, E., Arenas, P., de la Banda, M.G., Gómez-Zamalloa, M., Stuckey, P.J.: Context-sensitive dynamic partial order reduction. In Majumdar, R., Kuncak, V., eds.: Proc. 29th Intl. Conf. on Computer Aided Verification (CAV 2017). Volume 10426 of Lecture Notes in Computer Science., Springer (2017) 526–543
Godefroid, P.: Model checking for programming languages using Verisoft. In Lee, P., Henglein, F., Jones, N.D., eds.: Proc. 24th Symp. on Principles of Programming Languages (POPL 1997), ACM (1997) 174–186
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Tveito, L., Johnsen, E.B., Schlatte, R. (2020). Global Reproducibility Through Local Control for Distributed Active Objects. In: Wehrheim, H., Cabot, J. (eds) Fundamental Approaches to Software Engineering. FASE 2020. Lecture Notes in Computer Science(), vol 12076. Springer, Cham. https://doi.org/10.1007/978-3-030-45234-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-45234-6_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45233-9
Online ISBN: 978-3-030-45234-6
eBook Packages: Computer ScienceComputer Science (R0)