Document Open Access Logo

API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3

Authors Guillermina Cledou , Luc Edixhoven , Sung-Shik Jongmans , José Proença

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.27.pdf
  • Filesize: 1.16 MB
  • 28 pages

Document Identifiers

Author Details

Guillermina Cledou
  • HASLab, INESC TEC, Porto, Portugal
  • University of Minho, Braga, Portugal
Luc Edixhoven
  • Open University of the Netherlands, Heerlen, The Netherlands
  • NWO-I, Centrum Wiskunde & Informatica, Amsterdam, The Netherlands
Sung-Shik Jongmans
  • Open University of the Netherlands, Heerlen, The Netherlands
  • NWO-I, Centrum Wiskunde & Informatica, Amsterdam, The Netherlands
José Proença
  • CISTER, ISEP, Polytechnic Institute of Porto, Portugal

Funding

G. Cledou and J. Proença: European Regional Development Fund (ERDF), Operational Programme for Competitiveness and Internationalisation (COMPETE 2020): POCI-01-0145-FEDER-029946 (DaVinci). S. Jongmans: Netherlands Organisation of Scientific Research: 016.Veni.192.103. J. Proença: Fundação para a Ciência e a Tecnologia (FCT), within the CISTER Research Unit: UIDP/UIDB/04234/2020. ERDF and FCT, Portugal 2020 Partnership Agreement, Norte Portugal Regional Operational Programme (NORTE 2020): NORTE-01-0145-FEDER-028550 (REASSURE). ECSEL Joint Undertaking (JU): grant agreement No 876852 (VALU3S).

Cite As Get BibTex

Guillermina Cledou, Luc Edixhoven, Sung-Shik Jongmans, and José Proença. API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 27:1-27:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ECOOP.2022.27

Abstract

Construction and analysis of distributed systems is difficult. Multiparty session types (MPST) constitute a method to make it easier. The idea is to use type checking to statically prove deadlock freedom and protocol compliance of communicating processes. In practice, the premier approach to apply the MPST method in combination with mainstream programming languages has been based on API generation. In this paper (pearl), we revisit and revise this approach.
Regarding our "revisitation", using Scala 3, we present the existing API generation approach, which is based on deterministic finite automata (DFA), in terms of both the existing states-as-classes encoding of DFAs as APIs, and a new states-as-type-parameters encoding; the latter leverages match types in Scala 3. Regarding our "revision", also using Scala 3, we present a new API generation approach that is based on sets of pomsets instead of DFAs; it crucially leverages match types, too.  Our fresh perspective allows us to avoid two forms of combinatorial explosion resulting from implementing concurrent subprotocols in the DFA-based approach. We implement our approach in a new API generation tool.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software notations and tools
Keywords
  • Concurrency
  • pomsets (partially ordered multisets)
  • match types
  • Scala 3

Metrics

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

Supplementary Materials

References

  1. Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky. Type-level programming with match types. Proc. ACM Program. Lang., 6(POPL):1-24, 2022. Google Scholar
  2. 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. Google Scholar
  3. Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. A theory of design-by-contract for distributed multiparty interactions. In CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 162-176. Springer, 2010. Google Scholar
  4. Laura Bocchi, Julien Lange, and Nobuko Yoshida. Meeting deadlines together. In CONCUR, volume 42 of LIPIcs, pages 283-296. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. Google Scholar
  5. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323-342, 1983. Google Scholar
  6. Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, and Luca Padovani. On global types and multi-party session. Log. Methods Comput. Sci., 8(1), 2012. Google Scholar
  7. David Castro-Perez, 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):29:1-29:30, 2019. Google Scholar
  8. Guillermina Cledou, Luc Edixhoven, Sung-Shik Jongmans, and José Proença. Api generation for multiparty session types, revisited and revised using scala 3 (full version). Technical Report OUNL-CS-2022-03, Open University of the Netherlands, 2022. Google Scholar
  9. 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. Google Scholar
  10. Pierre-Malo Deniélou and Nobuko Yoshida. Dynamic multirole session types. In POPL, pages 435-446. ACM, 2011. Google Scholar
  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. Google Scholar
  12. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In ICALP (2), volume 7966 of Lecture Notes in Computer Science, pages 174-186. Springer, 2013. Google Scholar
  13. Jay L. Gischer. The equational theory of pomsets. Theor. Comput. Sci., 61:199-224, 1988. Google Scholar
  14. Roberto Guanciale and Emilio Tuosto. Realisability of pomsets. J. Log. Algebraic Methods Program., 108:69-89, 2019. Google Scholar
  15. Roberto Guanciale and Emilio Tuosto. Pomcho: A tool chain for choreographic design. Sci. Comput. Program., 202:102535, 2021. Google Scholar
  16. Ruben Hamers and Sung-Shik Jongmans. Discourje: Runtime verification of communication protocols in clojure. In TACAS (1), volume 12078 of Lecture Notes in Computer Science, pages 266-284. Springer, 2020. Google Scholar
  17. Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay. Multiparty session types for safe runtime adaptation in an actor language. In ECOOP, volume 194 of LIPIcs, pages 10:1-10:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  18. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL, pages 273-284. ACM, 2008. Google Scholar
  19. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1-9:67, 2016. Google Scholar
  20. Raymond Hu and Nobuko Yoshida. Hybrid session verification through endpoint API generation. In FASE, volume 9633 of Lecture Notes in Computer Science, pages 401-418. Springer, 2016. Google Scholar
  21. Raymond Hu and Nobuko Yoshida. Explicit connection actions in multiparty session types. In FASE, volume 10202 of Lecture Notes in Computer Science, pages 116-133. Springer, 2017. Google Scholar
  22. Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty session programming with global protocol combinators. In ECOOP, volume 166 of LIPIcs, pages 9:1-9:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  23. Sung-Shik Jongmans and Nobuko Yoshida. Exploring type-level bisimilarity towards more expressive multiparty session types. In ESOP, volume 12075 of Lecture Notes in Computer Science, pages 251-279. Springer, 2020. Google Scholar
  24. Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, and Fabio Zanasi. On series-parallel pomset languages: Rationality, context-freeness and automata. J. Log. Algebraic Methods Program., 103:130-153, 2019. Google Scholar
  25. Jonathan King, Nicholas Ng, and Nobuko Yoshida. Multiparty session type-safe web development with static linearity. In PLACES@ETAPS, volume 291 of EPTCS, pages 35-46, 2019. Google Scholar
  26. Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. Typechecking protocols with mungo and stmungo: A session type toolchain for java. Sci. Comput. Program., 155:52-75, 2018. Google Scholar
  27. Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Implementing multiparty session types in rust. In COORDINATION, volume 12134 of Lecture Notes in Computer Science, pages 127-136. Springer, 2020. Google Scholar
  28. Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In POPL, pages 221-232. ACM, 2015. Google Scholar
  29. Julien Lange and Nobuko Yoshida. Verifying asynchronous interactions via communicating session automata. In CAV (1), volume 11561 of Lecture Notes in Computer Science, pages 97-117. Springer, 2019. Google Scholar
  30. Kamal Lodaya and Pascal Weil. Series-parallel languages and the bounded-width property. Theor. Comput. Sci., 237(1-2):347-380, 2000. Google Scholar
  31. Anson Miu, Francisco Ferreira, Nobuko Yoshida, and Fangyi Zhou. Communication-safe web programming in typescript with routed multiparty session types. In CC, pages 94-106. ACM, 2021. Google Scholar
  32. Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. Timed runtime monitoring for multiparty conversations. Formal Aspects Comput., 29(5):877-910, 2017. Google Scholar
  33. 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 CC, pages 128-138. ACM, 2018. Google Scholar
  34. Rumyana Neykova and Nobuko Yoshida. Let it recover: multiparty protocol-induced recovery. In CC, pages 98-108. ACM, 2017. Google Scholar
  35. Luca Padovani. A simple library implementation of binary sessions. J. Funct. Program., 27:e4, 2017. Google Scholar
  36. Vaughan R. Pratt. Modeling concurrency with partial orders. Int. J. Parallel Program., 15(1):33-71, 1986. Google Scholar
  37. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A linear decomposition of multiparty sessions for safe distributed programming. In ECOOP, volume 74 of LIPIcs, pages 24:1-24:31. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. Google Scholar
  38. Alceste Scalas and Nobuko Yoshida. Lightweight session programming in scala. In ECOOP, volume 56 of LIPIcs, pages 21:1-21:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  39. 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
  40. Alceste Scalas, Nobuko Yoshida, and Elias Benussi. Effpi: verified message-passing programs in dotty. In SCALA@ECOOP, pages 27-31. ACM, 2019. Google Scholar
  41. Alceste Scalas, Nobuko Yoshida, and Elias Benussi. Verifying message-passing programs with dependent behavioural types. In PLDI, pages 502-516. ACM, 2019. Google Scholar
  42. Jesse A. Tov and Riccardo Pucella. Stateful contracts for affine types. In ESOP, volume 6012 of Lecture Notes in Computer Science, pages 550-569. Springer, 2010. Google Scholar
  43. Emilio Tuosto and Roberto Guanciale. Semantics of global view of choreographies. J. Log. Algebraic Methods Program., 95:17-40, 2018. Google Scholar
  44. A. Laura Voinea, Ornela Dardha, and Simon J. Gay. Typechecking java protocols with [st]mungo. In FORTE, volume 12136 of Lecture Notes in Computer Science, pages 208-224. Springer, 2020. Google Scholar
  45. Nobuko Yoshida, Fangyi Zhou, and Francisco Ferreira. Communicating finite state machines and an extensible toolchain for multiparty session types. In FCT, volume 12867 of Lecture Notes in Computer Science, pages 18-35. Springer, 2021. Google Scholar
  46. Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Statically verified refinements for multiparty protocols. Proc. ACM Program. Lang., 4(OOPSLA):148:1-148:30, 2020. 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