Document Open Access Logo

Design-By-Contract for Flexible Multiparty Session Protocols

Authors Lorenzo Gheri , Ivan Lanese , Neil Sayers , Emilio Tuosto , Nobuko Yoshida

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.8.pdf
  • Filesize: 1.35 MB
  • 28 pages

Document Identifiers

Author Details

Lorenzo Gheri
  • Imperial College London, UK
Ivan Lanese
  • Focus Team, University of Bologna, Italy
  • Focus Team, INRIA, Sophia Antipolis, France
Neil Sayers
  • Imperial College London, UK
  • Coveo Solutions Inc., Canada
Emilio Tuosto
  • Gran Sasso Science Institute, L'Aquila, Italy
Nobuko Yoshida
  • Imperial College London, UK

Funding

Research partly supported by the EU H2020 RISE programme under the Marie SkłodowskaCurie grant agreement No 778233. Work partially funded by MIUR project PRIN 2017FTXR7S IT MATTERS (Methods and Tools for Trustworthy Smart Systems). Lanese and Tuosto are partially supported by INdAM as members of GNCS (Gruppo Nazionale per il Calcolo Scientifico). The work is partially supported by EPSRC EP/T006544/1, EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1, EP/T014709/1 and EP/V000462/1, and NCSS/EPSRC VeTSS.

Acknowledgements

We thank the anonymous reviewers for their useful comments and suggestions. We thank Franco Barbanera for contributing to this work in its early stages. We thank Fangyi Zhou for their help with building our artifact on top of their software, νScr.

Cite AsGet BibTex

Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida. Design-By-Contract for Flexible Multiparty Session Protocols. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 8:1-8:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECOOP.2022.8

Abstract

Choreographic models support a correctness-by-construction principle in distributed programming. Also, they enable the automatic generation of correct message-based communication patterns from a global specification of the desired system behaviour. In this paper we extend the theory of choreography automata, a choreographic model based on finite-state automata, with two key features. First, we allow participants to act only in some of the scenarios described by the choreography automaton. While this seems natural, many choreographic approaches in the literature, and choreography automata in particular, forbid this behaviour. Second, we equip communications with assertions constraining the values that can be communicated, enabling a design-by-contract approach. We provide a toolchain allowing to exploit the theory above to generate APIs for TypeScript web programming. Programs communicating via the generated APIs follow, by construction, the prescribed communication pattern and are free from communication errors such as deadlocks.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Software and its engineering → Formal software verification
Keywords
  • Choreography automata
  • design by contract
  • deadlock freedom
  • Communicating Finite State Machines
  • TypeScript programming

Metrics

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

Related Versions

Supplementary Materials

References

  1. Marco Autili, Paola Inverardi, and Massimo Tivoli. Automated synthesis of service choreographies. IEEE Softw., 32(1):50-57, 2015. URL: https://doi.org/10.1109/MS.2014.131.
  2. Franco Barbanera, Ivan Lanese, and Emilio Tuosto. Choreography automata. In COORDINATION, volume 12134 of Lecture Notes in Computer Science, pages 86-106. Springer, 2020. Google Scholar
  3. Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. A theory of design-by-contract for distributed multiparty interactions. In Paul Gastin and François Laroussinie, editors, Concur 2010, volume 6269 of LNCS, pages 162-176. Springer, 2010. Google Scholar
  4. Jonas Bonér. Reactive Microsystems - The Evolution Of Microservices At Scale. O'Reilly, 2018. Google Scholar
  5. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323-342, 1983. Google Scholar
  6. Tevfik Bultan and Xiang Fu. Specification of realizable service conversations using collaboration diagrams. Service Oriented Computing and Applications, 2(1):27-39, 2008. URL: https://doi.org/10.1007/s11761-008-0022-7.
  7. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: multiparty asynchronous global programming. In Roberto Giacobazzi and Radhia Cousot, editors, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pages 263-274. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429101.
  8. David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. Distributed programming using role-parametric session types in Go: Statically-typed endpoint APIs for dynamically-instantiated communication structures. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290342.
  9. 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
  10. Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-Free Asynchronous Message Reordering in Rust with Multiparty Session Types. In 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, volume abs/2112.12693 of PPoPP '22, pages 261-246. ACM, 2022. URL: https://doi.org/10.1145/3503221.3508404.
  11. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty session types meet communicating automata. In ESOP, volume 7211 of Lecture Notes in Computer Science, pages 194-213. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28869-2_10.
  12. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In Fedor V. Fomin, Rūsiņš Freivalds, Marta Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming, pages 174-186, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  13. Ian Fette and Alexey Melnikov. The websocket protocol, 2011. URL: https://www.rfc-editor.org/info/rfc6455.
  14. Robert W. Floyd. Assigning meaning to programs. In Proc. Symp. in Applied Mathematics, volume 19, 1967. Google Scholar
  15. Leonardo Frittelli, Facundo Maldonado, Hernán C. Melgratti, and Emilio Tuosto. A choreography-driven approach to APIs: The OpenDXL case study. In Simon Bliudze and Laura Bocchi, editors, Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings, volume 12134 of Lecture Notes in Computer Science, pages 107-124. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-50029-0_7.
  16. Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida. Design-by-contract for Flexible multiparty session protocols - extended version. Technical report, Focus Team, University of Bologna/INRIA (Italy) and Gran Sasso Science Institute (Italy) and Imperial College (UK), May 2022. Full version of the ECOOP 2022 paper. URL: http://mrg.doc.ic.ac.uk/publications/design-by-contract-for-flexible-multiparty-session-protocols/.
  17. Roberto Guanciale and Emilio Tuosto. Realisability of pomsets. J. Log. Algebraic Methods Program., 108:69-89, 2019. Google Scholar
  18. Dick Hardt. The OAuth 2.0 Authorization Framework. RFC 6749, October 2012. URL: https://doi.org/10.17487/RFC6749.
  19. Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay. Multiparty session types for safe runtime adaptation in an actor language. In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming (ECOOP 2021), volume 194 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1-10:30, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2021.10.
  20. Tony Hoare. An axiomatic basis of computer programming. CACM, 12, 1969. Google Scholar
  21. Kohei Honda, Aybek Mukhamedov, Gary Brown, Tzu-Chun Chen, and Nobuko Yoshida. Scribbling interactions with a formal foundation. In Raja Natarajan and Adegboyega Ojo, editors, Distributed Computing and Internet Technology, pages 55-75, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-19056-8_4.
  22. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In George C. Necula and Philip Wadler, editors, POPL, pages 273-284. ACM Press, 2008. Google Scholar
  23. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1-9:67, 2016. URL: https://doi.org/10.1145/2827695.
  24. Raymond Hu and Nobuko Yoshida. Hybrid session verification through endpoint API generation. In Perdita Stevens and Andrzej Wąsowski, editors, Fundamental Approaches to Software Engineering, pages 401-418, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg. Google Scholar
  25. 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 - Volume 10202, pages 116-133, Berlin, Heidelberg, 2017. Springer-Verlag. URL: https://doi.org/10.1007/978-3-662-54494-5_7.
  26. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1):3:1-3:36, 2016. Google Scholar
  27. Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty session programming with global protocol combinators. In Robert Hirschfeld and Tobias Pape, editors, 34th European Conference on Object-Oriented Programming (ECOOP 2020), volume 166 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:30, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2020.9.
  28. Nickolas Kavantzas, Davide Burdett, Gregory Ritzinger, Tony Fletcher, and Yves Lafon. Web services choreography description language version 1.0. http://www.w3.org/TR/2004/WD-ws-cdl-10-20041217. Working Draft 17 December 2004.
  29. Kerberos 5. https://web.mit.edu/kerberos/krb5-1.19/. Accessed: 14/02/2022.
  30. Kickstarter. https://www.kickstarter.com/about. Accessed: 14/02/2022.
  31. Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. Typechecking protocols with Mungo and StMungo. In PPDP, pages 146-159, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2967973.2968595.
  32. Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe under Panic: Affine Rust Programming with Multiparty Session Types. In 36th European Conference on Object-Oriented Programming, LIPIcs, 2022. in this volume. Google Scholar
  33. Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 221-232. ACM, 2015. Google Scholar
  34. Elliot Mendelson. Introduction to Mathematical Logic. Wadsworth Inc., 1987. Google Scholar
  35. Bertrand Meyer. Applying "Design by Contract". Computer, 25(10):40-51, 1992. URL: https://doi.org/10.1109/2.161279.
  36. Anson Miu, Francisco Ferreira, Nobuko Yoshida, and Fangyi Zhou. Communication-safe web programming in typescript with routed multiparty session types. In Proceedings of the 30th ACM SIGPLAN International Conference on Compiler Construction, CC 2021, pages 94-106, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3446804.3446854.
  37. Rumyana Neykova, Raymond Hu, Nobuko Yoshida, and Fahd Abdeljallal. A session type provider: Compile-time API generation of distributed protocols with refinements in F#. In Proceedings of the 27th International Conference on Compiler Construction, CC 2018, pages 128-138, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3178372.3179495.
  38. Rumyana Neykova and Nobuko Yoshida. Featherweight Scribble, volume 11665 of LNCS, pages 236-259. Springer, Cham, 2019. URL: https://doi.org/10.1007/978-3-030-21485-2_14.
  39. Rumyana Neykova, Nobuko Yoshida, and Raymond Hu. Spy: Local verification of global protocols. In Axel Legay and Saddek Bensalem, editors, Runtime Verification, pages 358-363, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  40. Object Management Group. Business Process Model and Notation. http://www.bpmn.org.
  41. Zongyan Qiu, Xiangpeng Zhao, Chao Cai, and Hongli Yang. Towards the theoretical foundation of choreography. In Proceedings of the 16th International Conference on World Wide Web, WWW 2007, pages 973-982, 2007. URL: https://doi.org/10.1145/1242572.1242704.
  42. Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011. Google Scholar
  43. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A linear decomposition of multiparty sessions for safe distributed programming. In Peter Müller, editor, 31st European Conference on Object-Oriented Programming (ECOOP 2017), volume 74 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:31, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2017.24.
  44. Alceste Scalas and Nobuko Yoshida. Less is more: multiparty session types revisited. PACMPL, 3(POPL):30:1-30:29, 2019. Google Scholar
  45. Paula Severi and Mariangiola Dezani-Ciancaglini. Observational equivalence for multiparty sessions. Fundamenta Informaticae, 170:267-305, 2019. URL: http://www.di.unito.it/~dezani/papers/sd19.pdf.
  46. Emilio Tuosto and Roberto Guanciale. Semantics of global view of choreographies. J. Log. Algebr. Meth. Program., 95:17-40, 2018. Google Scholar
  47. Malte Viering, Raymond Hu, Patrick Eugster, and Lukasz Ziarek. A multiparty session typing discipline for fault-tolerant event-driven distributed programming. Proc. ACM Program. Lang., 5(OOPSLA), October 2021. URL: https://doi.org/10.1145/3485501.
  48. Nobuko Yoshida, Fangyi Zhou, and Francisco Ferreira. Communicating finite state machines and an extensible toolchain for multiparty session types. In Evripidis Bampis and Aris Pagourtzis, editors, Fundamentals of Computation Theory, pages 18-35, Cham, 2021. Springer International Publishing. Google Scholar
  49. Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Statically verified refinements for multiparty protocols. In OOPSLA 2020: Conference on Object-Oriented Programming Systems, Languages and Applications, number OOPSLA (Article 148) in PACMPL, page 30 pages, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3428216.
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