Document Open Access Logo

Locally Static, Globally Dynamic Session Types for Active Objects

Authors Reiner Hähnle , Anton W. Haubner, Eduard Kamburjan

PDF
Thumbnail PDF

File

OASIcs.Gabbrielli.1.pdf
  • Filesize: 0.71 MB
  • 24 pages

Document Identifiers

Author Details

Reiner Hähnle
  • Technical University Darmstadt, Germany
Anton W. Haubner
  • Technical University Darmstadt, Germany
Eduard Kamburjan
  • Technical University Darmstadt, Germany

Funding

This research is supported by the Constraint-Based Operational Consistency of Evolving Software Systems (COCoS) project, funded by the DFG as project 351097374.

Cite AsGet BibTex

Reiner Hähnle, Anton W. Haubner, and Eduard Kamburjan. Locally Static, Globally Dynamic Session Types for Active Objects. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/OASIcs.Gabbrielli.1

Abstract

Active object languages offer an attractive trade-off between low-level, preemptive concurrency and fully distributed actors: syntactically identifiable atomic code segments and asynchronous calls are the basis of cooperative concurrency, still permitting interleaving, but nevertheless being mechanically analyzable. The challenge is to reconcile local static analysis of atomic segments with the global scheduling constraints it depends on. Here, we propose an approximate, hybrid approach; At compile-time we perform a local static analysis: later, any run not complying to a global specification is excluded via runtime checks. That specification is expressed in a type-theoretic language inspired by session types. The approach reverses the usual (first global, then local) order of analysis and, thereby, supports analysis of open distributed systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Theory of computation → Object oriented constructs
  • Theory of computation → Type structures
Keywords
  • Session Types
  • Active Objects
  • Runtime Verification
  • Static Verification

Metrics

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

References

  1. Wolfgang Ahrendt, Jesús Mauricio Chimento, Gordon J. Pace, and Gerardo Schneider. Verifying data- and control-oriented properties combining static and runtime verification: theory and tools. Formal Methods Syst. Des., 51(1):200-265, 2017. Google Scholar
  2. Wolfgang Ahrendt, Marieke Huisman, Giles Reger, and Kristin Yvonne Rozier. A broader view on verification: From static to runtime and back (track summary). In ISoLA (2), volume 11245 of Lecture Notes in Computer Science, pages 3-7. Springer, 2018. Google Scholar
  3. Elvira Albert, Puri Arenas, Antonio Flores-Montoya, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, German Puebla, and Guillermo Román-Díez. SACO: static analyzer for concurrent objects. In Erika Ábrahám and Klaus Havelund, editors, TACAS 2014, volume 8413 of Lecture Notes in Computer Science, pages 562-567. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54862-8_46.
  4. Henry G. Baker and Carl E. Hewitt. The incremental garbage collection of processes. In Proceeding of the Symposium on Artificial Intelligence Programming Languages, number 12 in SIGPLAN Notices, page 11, August 1977. Google Scholar
  5. Joakim Bjørk, Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, and Silvia Lizeth Tapia Tarifa. User-defined schedulers for real-time concurrent objects. ISSE, 9(1):29-43, 2013. Google Scholar
  6. Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida. Monitoring networks through multiparty session types. Theor. Comput. Sci., 669:33-58, 2017. URL: https://doi.org/10.1016/j.tcs.2017.02.009.
  7. Benedikt Bollig, Peter Habermehl, Martin Leucker, and Benjamin Monmege. A fresh approach to learning register automata. In Marie-Pierre Béal and Olivier Carton, editors, Developments in Language Theory: 17th Intl. Conf. DLT, Marne-la-Vallée, France, volume 7907 of LNCS, pages 118-130. Springer, 2013. Google Scholar
  8. Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst., 34(2):8:1-8:78, 2012. URL: https://doi.org/10.1145/2220365.2220367.
  9. Jesús Mauricio Chimento, Wolfgang Ahrendt, Gordon J. Pace, and Gerardo Schneider. Starvoors: A tool for combined static and runtime verification of java. In Ezio Bartocci and Rupak Majumdar, editors, RV 2015, volume 9333 of Lecture Notes in Computer Science, pages 297-305. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23820-3_21.
  10. Dave Clarke, Radu Muschevici, José Proença, Ina Schaefer, and Rudolf Schlatte. Variability modelling in the ABS language. In Bernhard K. Aichernig, Frank S. de Boer, and Marcello M. Bonsangue, editors, FMCO 2010, volume 6957 of Lecture Notes in Computer Science, pages 204-224. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-25271-6_11.
  11. Frank S. de Boer, Vlad Serbanescu, Reiner Hähnle, Ludovic Henrio, Justine Rochas, Crystal Chang Din, Einar Broch Johnsen, Marjan Sirjani, Ehsan Khamespanah, Kiko Fernandez-Reyes, and Albert Mingkun Yang. A survey of active object languages. ACM Comput. Surv., 50(5):76:1-76:39, 2017. URL: https://doi.org/10.1145/3122848.
  12. Romain Demangeon, Kohei Honda, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Practical interruptible conversations: distributed dynamic verification with multiparty session types and python. Formal Methods Syst. Des., 46(3):197-225, 2015. URL: https://doi.org/10.1007/s10703-014-0218-8.
  13. Crystal Chang Din, Richard Bubel, and Reiner Hähnle. Key-abs: A deductive verification tool for the concurrent modelling language ABS. In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 517-526. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_35.
  14. Crystal Chang Din, Reiner Hähnle, Einar Broch Johnsen, Ka I Pun, and Silvia Lizeth Tapia Tarifa. Locally abstract, globally concrete semantics of concurrent programming languages. In TABLEAUX, volume 10501 of Lecture Notes in Computer Science, pages 22-43. Springer, 2017. Google Scholar
  15. Antonio Flores-Montoya, Elvira Albert, and Samir Genaim. May-happen-in-parallel based deadlock analysis for concurrent objects. In FMOODS/FORTE, volume 7892 of LNCS, pages 273-288. Springer, 2013. Google Scholar
  16. Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Jacopo Mauro. Guess who’s coming: Runtime inclusion of participants in choreographies. In Mário S. Alvim, Kostas Chatzikokolakis, Carlos Olarte, and Frank Valencia, editors, The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, volume 11760 of Lecture Notes in Computer Science, pages 118-138. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31175-9_8.
  17. Rosita Gerbo and Luca Padovani. Concurrent typestate-oriented programming in java. In Francisco Martins and Dominic Orchard, editors, Proceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES@ETAPS 2019, Prague, Czech Republic, 7th April 2019, volume 291 of EPTCS, pages 24-34, 2019. URL: https://doi.org/10.4204/EPTCS.291.3.
  18. Elena Giachino, Cosimo Laneve, and Michael Lienhardt. A framework for deadlock detection in core ABS. Software and Systems Modeling, 15(4):1013-1048, 2016. URL: https://doi.org/10.1007/s10270-014-0444-y.
  19. Dilian Gurov, Reiner Hähnle, and Eduard Kamburjan. Who carries the burden of modularity? In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation, 9th Intl. Symp., ISoLA 2020, Rhodes, Greece, LNCS. Springer, October 2020. Google Scholar
  20. Anton W Haubner. Semi-dynamic session types for ABS. Bachelor thesis, Technical University of Darmstadt, 2019. Available at URL: https://github.com/ahbnr/SessionTypeABS/blob/master/thesis/thesis_final_pdfa.pdf.
  21. Carl Hewitt, Peter Bishop, and Richard Steiger. A universal modular ACTOR formalism for artificial intelligence. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence, IJCAI'73, pages 235-245. Morgan Kaufmann Publishers Inc., 1973. URL: http://dl.acm.org/citation.cfm?id=1624775.1624804.
  22. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328472.
  23. Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, and Philip Wadler. Gradual session types. Proc. ACM Program. Lang., 1(ICFP):38:1-38:28, 2017. URL: https://doi.org/10.1145/3110282.
  24. Einar Broch Johnsen, Reiner Hähnle, Jan Schäfer, Rudolf Schlatte, and Martin Steffen. ABS: A core language for abstract behavioral specification. In Bernhard K. Aichernig, Frank S. de Boer, and Marcello M. Bonsangue, editors, FMCO 2010, volume 6957 of Lecture Notes in Computer Science, pages 142-164. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-25271-6_8.
  25. Eduard Kamburjan. Detecting deadlocks in formal system models with condition synchronization. ECEASST, 76, 2018. URL: https://doi.org/10.14279/tuj.eceasst.76.1070.
  26. Eduard Kamburjan. Behavioral program logic. In TABLEAUX, volume 11714 of Lecture Notes in Computer Science, pages 391-408. Springer, 2019. Google Scholar
  27. Eduard Kamburjan. Modular Verification of a Modular Specification: Behavioral Types as Program Logics. PhD thesis, Technische Universität Darmstadt, 2020. Google Scholar
  28. Eduard Kamburjan and Tzu-Chun Chen. Stateful behavioral types for active objects. In Carlo A. Furia and Kirsten Winter, editors, iFM 2018, volume 11023 of Lecture Notes in Computer Science, pages 214-235. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98938-9_13.
  29. Eduard Kamburjan, Crystal Chang Din, and Tzu-Chun Chen. Session-based compositional analysis for actor-based languages using futures. In Kazuhiro Ogata, Mark Lawford, and Shaoying Liu, editors, ICFEM 2016, volume 10009 of Lecture Notes in Computer Science, pages 296-312, 2016. URL: https://doi.org/10.1007/978-3-319-47846-3_19.
  30. Eduard Kamburjan, Crystal Chang Din, Reiner Hähnle, and Einar Broch Johnsen. Asynchronous cooperative contracts for cooperative scheduling. In SEFM, volume 11724 of Lecture Notes in Computer Science, pages 48-66. Springer, 2019. Google Scholar
  31. Eduard Kamburjan, Reiner Hähnle, and Sebastian Schön. Formal modeling and analysis of railway operations with active objects. Sci. Comput. Program., 166:167-193, 2018. URL: https://doi.org/10.1016/j.scico.2018.07.001.
  32. Eduard Kamburjan, Stefan Mitsch, Martina Kettenbach, and Reiner Hähnle. Modeling and verifying cyber-physical systems with hybrid active objects. CoRR, abs/1906.05704, 2019. URL: http://arxiv.org/abs/1906.05704.
  33. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. URL: https://doi.org/10.1016/0304-3975(94)90242-9.
  34. Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. Timed runtime monitoring for multiparty conversations. Formal Asp. Comput., 29(5):877-910, 2017. Google Scholar
  35. Rumyana Neykova and Nobuko Yoshida. Multiparty session actors. Logical Methods in Computer Science, 13(1), 2017. Google Scholar
  36. Mila Dalla Preda, Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Jacopo Mauro. Dynamic choreographies - safe runtime updates of distributed applications. In Tom Holvoet and Mirko Viroli, editors, COORDINATION 2015, volume 9037 of Lecture Notes in Computer Science, pages 67-82. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-19282-6_5.
  37. Mila Dalla Preda, Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Jacopo Mauro. Dynamic choreographies: Theory and implementation. Log. Methods Comput. Sci., 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:1)2017.
  38. Alceste Scalas and Nobuko Yoshida. Lightweight session programming in scala. In Shriram Krishnamurthi and Benjamin S. Lerner, editors, 30th European Conference on Object-Oriented Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy, volume 56 of LIPIcs, pages 21:1-21:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2016.21.
  39. Rudolf Schlatte and abstools Contributors. Modified branch of the abstools compiler version 1.8.1 - github source repository. https://github.com/ahbnr/abstools/tree/thisDestiny. Accessed: 2019-10-29.
  40. Rudolf Schlatte, Einar Broch Johnsen, Jacopo Mauro, Silvia Lizeth Tapia Tarifa, and Ingrid Chieh Yu. Release the beasts: When formal methods meet real world data. In Frank S. de Boer, Marcello M. Bonsangue, and Jan Rutten, editors, It’s All About Coordination - Essays to Celebrate the Lifelong Scientific Achievements of Farhad Arbab, volume 10865 of Lecture Notes in Computer Science, pages 107-121. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-90089-6_8.
  41. Robert E. Strom and Shaula Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng., 12(1):157-171, 1986. URL: https://doi.org/10.1109/TSE.1986.6312929.
  42. Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. Gradual typestate. In Mira Mezini, editor, ECOOP 2011 - Object-Oriented Programming - 25th European Conference, Lancaster, UK, July 25-29, 2011 Proceedings, volume 6813 of Lecture Notes in Computer Science, pages 459-483. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22655-7_22.
  43. Peter Y. H. Wong, Elvira Albert, Radu Muschevici, José Proença, Jan Schäfer, and Rudolf Schlatte. The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. STTT, 14(5):567-588, 2012. 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 Imprint Privacy Contact