Document Open Access Logo

Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Pearl/Brave New Idea)

Authors Sung-Shik Jongmans, Francisco Ferreira

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.42.pdf
  • Filesize: 1.08 MB
  • 30 pages

Document Identifiers

Author Details

Sung-Shik Jongmans
  • Department of Computer Science, Open University, Heerlen, The Netherlands
  • Centrum Wiskunde & Informatica (CWI), NWO-I, Amsterdam, The Netherlands
Francisco Ferreira
  • Department of Computer Science, Royal Holloway, University of London, UK

Funding

  • Jongmans, Sung-Shik: Netherlands Organisation of Scientific Research: 016.Veni.192.103.

Cite As Get BibTex

Sung-Shik Jongmans and Francisco Ferreira. Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Pearl/Brave New Idea). In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 42:1-42:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ECOOP.2023.42

Abstract

Programming distributed systems is difficult. Multiparty session typing (MPST) is a method to automatically prove safety and liveness of protocol implementations relative to protocol specifications.
In this paper, we introduce two new techniques to significantly improve the expressiveness of the MPST method: projection is based on implicit local types instead of explicit; type checking is based on the operational semantics of implicit local types instead of on the syntax. That is, the reduction relation on implicit local types is used not only "a posteriori" to prove type soundness (as usual), but also "a priori" to define the typing rules - synthetically.
Classes of protocols that can now be specified/implemented/verified for the first time using the MPST method include: recursive protocols in which different roles participate in different branches; protocols in which a receiver chooses the sender of the first communication; protocols in which multiple roles synchronously choose both the sender and the receiver of a next communication, implemented as mixed input/output processes. We present the theory of the new techniques, as well as their future potential, and we demonstrate their present capabilities to effectively support regular expressions as global types (not possible before).

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
Keywords
  • behavioural types
  • multiparty session types
  • choreographies

Metrics

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

Supplementary Materials

References

  1. Luca Aceto, Anna Ingólfsdóttir, and Jirí Srba. The algorithmics of bisimilarity. In Advanced Topics in Bisimulation and Coinduction, volume 52 of Cambridge tracts in theoretical computer science, pages 100-172. Cambridge University Press, 2012. Google Scholar
  2. Bernardo Almeida, Andreia Mordido, Peter Thiemann, and Vasco T. Vasconcelos. Polymorphic lambda calculus with context-free session types. Inf. Comput., 289(Part):104948, 2022. Google Scholar
  3. Bernardo Almeida, Andreia Mordido, and Vasco T. Vasconcelos. Deciding the bisimilarity of context-free session types. In TACAS (2), volume 12079 of Lecture Notes in Computer Science, pages 39-56. Springer, 2020. Google Scholar
  4. Jos C. M. Baeten, Flavio Corradini, and Clemens Grabmayer. A characterization of regular expressions under bisimulation. J. ACM, 54(2):6, 2007. Google Scholar
  5. Jos C. M. Baeten and Sjouke Mauw. Delayed choice: an operator for joining message sequence charts. In FORTE, volume 6 of IFIP Conference Proceedings, pages 340-354. Chapman & Hall, 1994. Google Scholar
  6. 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
  7. J. F. A. K. Van Benthem. Hintikka on analyticity. Journal of Philosophical Logic, 3(4):419-431, 1974. URL: https://doi.org/10.1007/bf00257484.
  8. Laura Bocchi, Julien Lange, and Nobuko Yoshida. Meeting deadlines together. In CONCUR, volume 42 of LIPIcs, pages 283-296. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  9. Laura Bocchi, Hernán C. Melgratti, and Emilio Tuosto. Resolving non-determinism in choreographies. In ESOP, volume 8410 of Lecture Notes in Computer Science, pages 493-512. Springer, 2014. Google Scholar
  10. Laura Bocchi, Weizhen Yang, and Nobuko Yoshida. Timed multiparty session types. In CONCUR, volume 8704 of Lecture Notes in Computer Science, pages 419-434. Springer, 2014. Google Scholar
  11. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323-342, 1983. Google Scholar
  12. Mario Bravetti and Gianluigi Zavattaro. Towards a unifying theory for choreography conformance and contract compliance. In SC@ETAPS, volume 4829 of Lecture Notes in Computer Science, pages 34-50. Springer, 2007. Google Scholar
  13. Mario Bravetti and Gianluigi Zavattaro. Contract compliance and choreography conformance in the presence of message queues. In WS-FM, volume 5387 of Lecture Notes in Computer Science, pages 37-54. Springer, 2008. Google Scholar
  14. Nadia Busi, Roberto Gorrieri, Claudio Guidi, Roberto Lucchi, and Gianluigi Zavattaro. Choreography and orchestration conformance for system design. In COORDINATION, volume 4038 of Lecture Notes in Computer Science, pages 63-81. Springer, 2006. Google Scholar
  15. Sara Capecchi, Ilaria Castellani, and Mariangiola Dezani-Ciancaglini. Typing access control and secure information flow in sessions. Inf. Comput., 238:68-105, 2014. Google Scholar
  16. Sara Capecchi, Ilaria Castellani, and Mariangiola Dezani-Ciancaglini. Information flow safety in multiparty sessions. Mathematical Structures in Computer Science, 26(8):1352-1394, 2016. Google Scholar
  17. Sara Capecchi, Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Tamara Rezk. Session types for access and information flow control. In CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 237-252. Springer, 2010. Google Scholar
  18. Marco Carbone, Nobuko Yoshida, and Kohei Honda. Asynchronous session types: Exceptions and multiparty interactions. In SFM, volume 5569 of Lecture Notes in Computer Science, pages 187-212. Springer, 2009. Google Scholar
  19. Filipe Casal, Andreia Mordido, and Vasco T. Vasconcelos. Mixed sessions. Theor. Comput. Sci., 897:23-48, 2022. Google Scholar
  20. Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, and Luca Padovani. On global types and multi-party session. Logical Methods in Computer Science, 8(1), 2012. Google Scholar
  21. Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. Reversible sessions with flexible choices. Acta Informatica, 56(7-8):553-583, 2019. Google Scholar
  22. Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. Asynchronous sessions with input races. CoRR, abs/2203.12876, 2022. Google Scholar
  23. Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini, and Ross Horne. Global types with internal delegation. Theor. Comput. Sci., 807:128-153, 2020. Google Scholar
  24. Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Jorge A. Pérez. Self-adaptation and secure information flow in multiparty communications. Formal Asp. Comput., 28(4):669-696, 2016. Google Scholar
  25. 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. PACMPL, 3(POPL):29:1-29:30, 2019. Google Scholar
  26. Guillermina Cledou, Luc Edixhoven, Sung-Shik Jongmans, and José Proença. API generation for multiparty session types, revisited and revised using scala 3. In ECOOP, volume 222 of LIPIcs, pages 27:1-27:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  27. Alex Coto, Roberto Guanciale, and Emilio Tuosto. An abstract framework for choreographic testing. J. Log. Algebraic Methods Program., 123:100712, 2021. Google Scholar
  28. Luís Cruz-Filipe, Kim S. Larsen, and Fabrizio Montesi. The paths to choreography extraction. In FoSSaCS, volume 10203 of Lecture Notes in Computer Science, pages 424-440, 2017. Google Scholar
  29. Ugo de'Liguoro, Hernán C. Melgratti, and Emilio Tuosto. Towards refinable choreographies. J. Log. Algebraic Methods Program., 127:100776, 2022. Google Scholar
  30. Pierre-Malo Deniélou and Nobuko Yoshida. Dynamic multirole session types. In POPL, pages 435-446. ACM, 2011. Google Scholar
  31. 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
  32. 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
  33. Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. Logical Methods in Computer Science, 8(4), 2012. Google Scholar
  34. Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida. Design-by-contract for flexible multiparty session protocols. In ECOOP, volume 222 of LIPIcs, pages 8:1-8:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  35. Roberto Guanciale and Emilio Tuosto. Realisability of pomsets. J. Log. Algebraic Methods Program., 108:69-89, 2019. Google Scholar
  36. Ruben Hamers, Erik Horlings, and Sung-Shik Jongmans. The discourje project: run-time verification of communication protocols in clojure. Int. J. Softw. Tools Technol. Transf., 24(5):757-782, 2022. Google Scholar
  37. 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
  38. Jaakko Hintikka. Logic, Language-Games and Information: Kantian Themes in the Philosophy of Logic. Oxford, England: Oxford, Clarendon Press, 1973. Google Scholar
  39. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL, pages 273-284. ACM, 2008. Google Scholar
  40. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1-9:67, 2016. Google Scholar
  41. 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
  42. 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
  43. Sung-Shik Jongmans and Francisco Ferreira. Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Technical Report). Technical Report OUNL-CS-2023-01, Open University of the Netherlands, 2023. Google Scholar
  44. 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
  45. Alex C. Keizer, Henning Basold, and Jorge A. Pérez. Session coalgebras: A coalgebraic view on regular and context-free session types. ACM Trans. Program. Lang. Syst., 44(3):18:1-18:45, 2022. Google Scholar
  46. 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
  47. Christian Koehler and Dave Clarke. Decomposing port automata. In SAC, pages 1369-1373. ACM, 2009. Google Scholar
  48. 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
  49. Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay safe under panic: Affine rust programming with multiparty session types. In ECOOP, volume 222 of LIPIcs, pages 4:1-4:29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  50. Ivan Lanese, Claudio Guidi, Fabrizio Montesi, and Gianluigi Zavattaro. Bridging the gap between interaction- and process-oriented choreographies. In SEFM, pages 323-332. IEEE Computer Society, 2008. Google Scholar
  51. Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In POPL, pages 221-232. ACM, 2015. Google Scholar
  52. 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
  53. Hugo A. López, Eduardo R. B. Marques, Francisco Martins, Nicholas Ng, César Santos, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. Protocol-based verification of message-passing parallel programs. In OOPSLA, pages 280-298. ACM, 2015. Google Scholar
  54. Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey. Generalising projection in asynchronous multiparty session types. In CONCUR, volume 203 of LIPIcs, pages 35:1-35:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  55. Robin Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17(3):348-375, 1978. Google Scholar
  56. 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
  57. Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. Timed runtime monitoring for multiparty conversations. Formal Asp. Comput., 29(5):877-910, 2017. Google Scholar
  58. 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
  59. Nicholas Ng and Nobuko Yoshida. Pabble: parameterised scribble. Service Oriented Computing and Applications, 9(3-4):269-284, 2015. Google Scholar
  60. Luca Padovani. Context-free session type inference. ACM Trans. Program. Lang. Syst., 41(2):9:1-9:37, 2019. Google Scholar
  61. 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 fuer Informatik, 2017. Google Scholar
  62. 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
  63. Peter Thiemann and Vasco T. Vasconcelos. Context-free session types. In ICFP, pages 462-475. ACM, 2016. Google Scholar
  64. Emilio Tuosto and Roberto Guanciale. Semantics of global view of choreographies. J. Log. Algebraic Methods Program., 95:17-40, 2018. Google Scholar
  65. Rob van Glabbeek, Peter Höfner, and Ross Horne. Assuming just enough fairness to make session types complete for lock-freedom. In LICS, pages 1-13. IEEE, 2021. Google Scholar
  66. Rob J. van Glabbeek. The linear time-branching time spectrum (extended abstract). In CONCUR, volume 458 of Lecture Notes in Computer Science, pages 278-297. Springer, 1990. Google Scholar
  67. Rob J. van Glabbeek. The linear time - branching time spectrum II. In CONCUR, volume 715 of Lecture Notes in Computer Science, pages 66-81. Springer, 1993. Google Scholar
  68. Rob J. van Glabbeek and W. P. Weijland. Branching time and abstraction in bisimulation semantics. J. ACM, 43(3):555-600, 1996. Google Scholar
  69. Vasco T. Vasconcelos, Filipe Casal, Bernardo Almeida, and Andreia Mordido. Mixed sessions. In ESOP, volume 12075 of Lecture Notes in Computer Science, pages 715-742. Springer, 2020. Google Scholar
  70. 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
  71. 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