Document Open Access Logo

Multiparty Session Types for Safe Runtime Adaptation in an Actor Language

Authors Paul Harvey , Simon Fowler , Ornela Dardha , Simon J. Gay

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2021.10.pdf
  • Filesize: 1.19 MB
  • 30 pages

Document Identifiers

Author Details

Paul Harvey
  • Rakuten Mobile Innovation Studio, Tokyo, Japan
Simon Fowler
  • School of Computing Science, University of Glasgow, Scotland, UK
Ornela Dardha
  • School of Computing Science, University of Glasgow, Scotland, UK
Simon J. Gay
  • School of Computing Science, University of Glasgow, Scotland, UK

Funding

Supported by EPSRC grants EP/T014628/1 (STARDUST), EP/K034413/1 (ABCD), EP/L01503X/1 (CDT in Pervasive Parallelism), ERC Consolidator Grant Skye (682315), and by the EU HORIZON 2020 MSCA RISE project 778233 (BehAPI).

Acknowledgements

Thanks to Phil Trinder for helpful comments and discussions, and to the anonymous reviewers for exceptionally detailed reviews.

Cite As Get BibTex

Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay. Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 10:1-10:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ECOOP.2021.10

Abstract

Human fallibility, unpredictable operating environments, and the heterogeneity of hardware devices are driving the need for software to be able to adapt as seen in the Internet of Things or telecommunication networks. Unfortunately, mainstream programming languages do not readily allow a software component to sense and respond to its operating environment, by discovering, replacing, and communicating with components that are not part of the original system design, while maintaining static correctness guarantees. In particular, if a new component is discovered at runtime, there is no guarantee that its communication behaviour is compatible with existing components.
We address this problem by using multiparty session types with explicit connection actions, a type formalism used to model distributed communication protocols. By associating session types with software components, the discovery process can check protocol compatibility and, when required, correctly replace components without jeopardising safety.
We present the design and implementation of EnsembleS, the first actor-based language with adaptive features and a static session type system, and apply it to a case study based on an adaptive DNS server. We formalise the type system of EnsembleS and prove the safety of well-typed programs, making essential use of recent advances in non-classical multiparty session types.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Concurrent programming languages
Keywords
  • Concurrency
  • session types
  • adaptation

Metrics

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

Related Versions

Supplementary Materials

References

  1. Gul A. Agha. ACTORS - a model of concurrent computation in distributed systems. MIT Press series in artificial intelligence. MIT Press, 1990. Google Scholar
  2. Gabrielle Anderson and Julian Rathke. Dynamic software update for message passing programs. In Ranjit Jhala and Atsushi Igarashi, editors, Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings, volume 7705 of Lecture Notes in Computer Science, pages 207-222. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-35182-2_15.
  3. Robert Atkey. Parameterised notions of computation. Journal of Functional Programming, 19(3-4):335-376, 2009. Google Scholar
  4. Mehdi Bagherzadeh and Hridesh Rajan. Order types: static reasoning about message races in asynchronous message passing concurrency. In AGERE!@SPLASH, pages 21-30. ACM, 2017. Google Scholar
  5. Massimo Bartoletti, Ilaria Castellani, Pierre-Malo Deniélou, Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Jovanka Pantovic, Jorge A. Pérez, Peter Thiemann, Bernardo Toninho, and Hugo Torres Vieira. Combining behavioural types with security analysis. Journal of Logical and Algebraic Methods in Programming, 84(6):763-780, 2015. URL: https://doi.org/10.1016/j.jlamp.2015.09.003.
  6. J. Baumann, F. Hohl, K. Rothermel, and M. Straßer. MOLE — Concepts of Mobile Agent System, page 535–554. ACM Press/Addison-Wesley Publishing Co., USA, 1999. Google Scholar
  7. G. Bouabene, C. Jelger, C. Tschudin, S. Schmid, A. Keller, and M. May. The autonomic network architecture (ANA). IEEE Journal on Selected Areas in Communications, 28(1):4-14, 2010. URL: https://doi.org/10.1109/JSAC.2010.100102.
  8. Mario Bravetti, Cinzia Di Giusto, Jorge A. Pérez, and Gianluigi Zavattaro. Adaptable processes. Logical Methods in Computer Science, 8(4), 2012. URL: https://doi.org/10.2168/LMCS-8(4:13)2012.
  9. Mario Bravetti, Cinzia Di Giusto, Jorge A. Pérez, and Gianluigi Zavattaro. Towards the verification of adaptable processes. In Proceedings (Part I) of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), volume 7609 of Lecture Notes in Computer Science, pages 269-283. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-34026-0_20.
  10. Callum Cameron, Paul Harvey, and Joseph Sventek. A virtual machine for the Insense language. In Proceedings of the International Conference on Mobile Wireless Middleware, Operating Systems and Applications (Mobilware), pages 1-10. IEEE, 2013. URL: https://doi.org/10.1109/Mobilware.2013.17.
  11. Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Jorge A. Pérez. Self-adaptation and secure information flow in multiparty communications. Formal Aspects of Computing, 28(4):669-696, 2016. URL: https://doi.org/10.1007/s00165-016-0381-3.
  12. Francesco Cesarini and Steve Vinoski. Designing for Scalability with Erlang/OTP: Implement Robust, Fault-Tolerant Systems. O'Reilly Media, Inc., 1st edition, 2016. Google Scholar
  13. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Self-adaptive multiparty sessions. Service Oriented Computing and Applications, 9(3-4):249-268, 2015. URL: https://doi.org/10.1007/s11761-014-0171-9.
  14. Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global progress for dynamically interleaved multiparty sessions. Mathematical Structures in Computer Science, 26(2):238-302, 2016. Google Scholar
  15. Frank S. de Boer, Dave Clarke, and Einar Broch Johnsen. A complete guide to the future. In ESOP, volume 4421 of Lecture Notes in Computer Science, pages 316-330. Springer, 2007. Google Scholar
  16. Ugo de'Liguoro and Luca Padovani. Mailbox types for unordered interactions. In ECOOP, volume 109 of LIPIcs, pages 15:1-15:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  17. Romain Demangeon and Kohei Honda. Nested protocols in session types. In CONCUR, volume 7454 of Lecture Notes in Computer Science, pages 272-286. Springer, 2012. Google Scholar
  18. Cinzia Di Giusto and Jorge A. Pérez. Disciplined structured communications with disciplined runtime adaptation. Science of Computer Programming, 97:235-265, 2015. URL: https://doi.org/10.1016/j.scico.2014.04.017.
  19. Cinzia Di Giusto and Jorge A. Pérez. An event-based approach to runtime adaptation in communication-centric systems. In Proceedings of the 11th and 12th International Workshops on Web Services, Formal Methods and Behavioural Types (WS-FM 2014, WS-FM/BEAT 2015), Lecture Notes in Computer Science, pages 67-85. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-33612-1_5.
  20. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In PLDI, pages 237-247. ACM, 1993. Google Scholar
  21. Simon Fowler. An Erlang implementation of multiparty session actors. In Proceedings of the 9th Interaction and Concurrency Experience (ICE), volume 223 of Electronic Proceedings in Theoretical Computer Science, pages 36-50. Open Publishing Association, 2016. URL: https://doi.org/10.4204/EPTCS.223.3.
  22. Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. Exceptional asynchronous session types: session types without tiers. Proc. ACM Program. Lang., 3(POPL):28:1-28:29, 2019. Google Scholar
  23. Colin S. Gordon. Lifting sequential effects to control operators. In ECOOP, volume 166 of LIPIcs, pages 23:1-23:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  24. T. Gu, H. K. Pung, and D. Q. Zhang. Toward an OSGi-based infrastructure for context-aware applications. IEEE Pervasive Computing, 3(4):66-74, 2004. URL: https://doi.org/10.1109/MPRV.2004.19.
  25. Paul Harvey. A linguistic approach to concurrent, distributed, and adaptive programming across heterogeneous platforms. PhD thesis, School of Computing Science, University of Glasgow, 2015. URL: http://theses.gla.ac.uk/6749/.
  26. Paul Harvey and Joseph Sventek. Adaptable actors: just what the world needs. In Proceedings of the 9th Workshop on Programming Languages and Operating Systems (PLOS), pages 22-28. ACM, 2017. URL: https://doi.org/10.1145/3144555.3144559.
  27. Richard Hayton, Michael Bursell, Douglas I. Donaldson, W. Harwood, and Andrew Herbert. Mobile Java objects. Distributed Syst. Eng., 6(1):51, 1999. URL: https://doi.org/10.1088/0967-1846/6/1/306.
  28. Carl Hewitt, Peter Boehler Bishop, and Richard Steiger. A universal modular ACTOR formalism for artificial intelligence. In Proceedings of the 3rd international joint conference on Artificial intelligence, pages 235-245, San Francisco, CA, USA, 1973. Morgan Kaufmann Publishers Inc. URL: http://dl.acm.org/citation.cfm?id=1624775.1624804.
  29. Kohei Honda. Types for dyadic interaction. In CONCUR '93, 4th International Conference on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  30. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567.
  31. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), volume 43, pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328897.1328472.
  32. Raymond Hu and Nobuko Yoshida. Explicit connection actions in multiparty session types. In Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE), Lecture Notes in Computer Science, pages 116-133. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54494-5_7.
  33. Danny Hughes, Klaas Thoelen, Wouter Horré, Nelson Matthys, Javier Del Cid, Sam Michiels, Christophe Huygens, and Wouter Joosen. LooCI: a loosely-coupled component infrastructure for networked embedded systems. In Proceedings of the 7th International Conference on Advances in Mobile Computing and Multimedia (MoMM), pages 195-203. ACM, 2009. URL: https://doi.org/10.1145/1821748.1821787.
  34. Jonathan W. Hui and David Culler. The dynamic behavior of a data dissemination protocol for network programming at scale. In Proceedings of the 2nd International Conference on Embedded Networked Sensor Systems (SenSys), pages 81-94. ACM, 2004. URL: https://doi.org/10.1145/1031495.1031506.
  35. Atsushi Igarashi and Naoki Kobayashi. A generic type system for the pi-calculus. Theor. Comput. Sci., 311(1-3):121-163, 2004. Google Scholar
  36. Atsushi Igarashi, Benjamin C Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems, 23(3):396-450, 2001. Google Scholar
  37. Antonio J Jara, Pedro Martinez-Julia, and Antonio Skarmeta. Light-weight multicast DNS and DNS-SD (lmDNS-SD): IPv6-based resource and service discovery for the web of things. In 2012 Sixth international conference on innovative mobile and internet services in ubiquitous computing, pages 731-738. IEEE, 2012. Google Scholar
  38. Einar Broch Johnsen, Reiner Hähnle, Jan Schäfer, Rudolf Schlatte, and Martin Steffen. ABS: A core language for abstract behavioral specification. In FMCO, volume 6957 of Lecture Notes in Computer Science, pages 142-164. Springer, 2010. Google Scholar
  39. Eduard Kamburjan, Crystal Chang Din, and Tzu-Chun Chen. Session-based compositional analysis for actor-based languages using futures. In ICFEM, volume 10009 of Lecture Notes in Computer Science, pages 296-312, 2016. Google Scholar
  40. Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. Typechecking protocols with Mungo and StMungo: a session type toolchain for Java. Science of Computer Programming, 155:52-75, 2018. URL: https://doi.org/10.1016/j.scico.2017.10.006.
  41. Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Information and Computation, 185(2):182-210, 2003. Google Scholar
  42. Robin Milner. Communicating and mobile systems - the Pi-calculus. Cambridge University Press, 1999. Google Scholar
  43. Paul V Mockapetris. RFC 1035: Domain names - implementation and specification, 1987. Google Scholar
  44. Fabrizio Montesi, Claudio Guidi, and Gianluigi Zavattaro. Composing services with JOLIE. In ECOWS, pages 13-22. IEEE Computer Society, 2007. Google Scholar
  45. Dimitris Mostrous and Vasco T. Vasconcelos. Affine sessions. Log. Methods Comput. Sci., 14(4), 2018. Google Scholar
  46. Dimitris Mostrous and Vasco Thudichum Vasconcelos. Session typing for a featherweight Erlang. In Proceedings of the 13th International Conference on Coordination Models and Languages (COORDINATION), volume 6721 of Lecture Notes in Computer Science, pages 95-109. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21464-6_7.
  47. Rumyana Neykova and Nobuko Yoshida. Multiparty session actors. In Proceedings of the 16th IFIP WG 6.1 Conference on Coordination Models and Languages (COORDINATION), volume 8459 of Lecture Notes in Computer Science, pages 131-146. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43376-8_9.
  48. Rumyana Neykova and Nobuko Yoshida. Let it recover: multiparty protocol-induced recovery. In Proceedings of the 26th International Conference on Compiler Construction (CC), pages 98-108. ACM, 2017. URL: http://dl.acm.org/citation.cfm?id=3033031.
  49. Rumyana Neykova and Nobuko Yoshida. Multiparty session actors. Logical Methods in Computer Science, 13(1:17):1-30, 2017. URL: https://doi.org/10.23638/LMCS-13(1:17)2017.
  50. Barry Porter, Matthew Grieves, Roberto Rodrigues Filho, and David Leslie. REX: A development platform and online learning approach for runtime emergent software systems. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 333-348. USENIX Association, 2016. URL: https://www.usenix.org/conference/osdi16/technical-sessions/presentation/porter.
  51. Mila Dalla Preda, Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Jacopo Mauro. Dynamic choreographies: Theory and implementation. Logical Methods in Computer Science, 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:1)2017.
  52. Jan S Rellermeyer, Gustavo Alonso, and Timothy Roscoe. R-OSGi: distributed applications through software modularization. In ACM/IFIP/USENIX International Conference on Distributed Systems Platforms and Open Distributed Processing, pages 1-20. Springer, 2007. Google Scholar
  53. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A linear decomposition of multiparty sessions for safe distributed programming. In Proceedings of the 31st European Conference on Object-Oriented Programming (ECOOP), volume 74 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:31, 2017. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2017.24.
  54. Alceste Scalas and Nobuko Yoshida. Less is more: multiparty session types revisited. Proc. ACM Program. Lang., 3(POPL):30:1-30:29, 2019. Google Scholar
  55. Filippo Visintainer, Leandro D'Orazio, Marco Darin, and Luciano Altomare. Cooperative systems in motorway environment: The example of Trento test site in Italy. In Jan Fischer-Wolfarth and Gereon Meyer, editors, Advanced Microsystems for Automotive Applications 2013, pages 147-158, Heidelberg, 2013. Springer International Publishing. Google Scholar
  56. Feng Xia, Laurence T. Yang, Lizhe Wang, and Alexey V. Vinel. Internet of things. International Journal of Communication Systems, 25(9):1101-1102, 2012. URL: https://doi.org/10.1002/dac.2417.
  57. Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. The Scribble protocol language. In Proceedings of the 8th International Symposium on Trustworthy Global Computing (TGC), volume 8358, pages 22-41. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-05119-2_3.
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