Document Open Access Logo

Multiparty Session Programming With Global Protocol Combinators

Authors Keigo Imai , Rumyana Neykova , Nobuko Yoshida , Shoji Yuen

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.9.pdf
  • Filesize: 0.9 MB
  • 30 pages

Document Identifiers

Author Details

Keigo Imai
  • Gifu University, Japan
Rumyana Neykova
  • Brunel University London, United Kingdom
Nobuko Yoshida
  • Imperial College London, United Kingdom
Shoji Yuen
  • Nagoya University, Japan

Funding

Our work is partially supported by the first author’s visitor funding to Imperial College London and Brunel University London supported by Gifu University, VeTSS, JSPS KAKENHI Grant Numbers JP17H01722, JP17K19969 and JP17K12662, JSPS Short-term Visiting Fellowship S19068, EPSRC Doctoral Prize Fellowship, and EPSRC EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1, EP/T006544/1 and EP/T014709/1.

Acknowledgements

We thank Jacques Garrigue and Oleg Kiselyov for their comments on an early version of this paper.

Cite As Get BibTex

Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty Session Programming With Global Protocol Combinators. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 9:1-9:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.ECOOP.2020.9

Abstract

Multiparty Session Types (MPST) is a typing discipline for communication protocols. It ensures the absence of communication errors and deadlocks for well-typed communicating processes. The state-of-the-art implementations of the MPST theory rely on (1) runtime linearity checks to ensure correct usage of communication channels and (2) external domain-specific languages for specifying and verifying multiparty protocols.
To overcome these limitations, we propose a library for programming with global combinators - a set of functions for writing and verifying multiparty protocols in OCaml. Local behaviours for all processes in a protocol are inferred at once from a global combinator. We formalise global combinators and prove a sound realisability of global combinators - a well-typed global combinator derives a set of local types, by which typed endpoint programs can ensure type and communication safety. Our approach enables fully-static verification and implementation of the whole protocol, from the protocol specification to the process implementations, to happen in the same language. 
We compare our implementation to untyped and continuation-passing style implementations, and demonstrate its expressiveness by implementing a plethora of protocols. We show our library can interoperate with existing libraries and services, implementing DNS (Domain Name Service) protocol and the OAuth (Open Authentication) protocol.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Concurrent programming structures
  • Theory of computation → Type structures
  • Software and its engineering → Functional languages
  • Software and its engineering → Polymorphism
Keywords
  • Multiparty Session Types
  • Communication Protocol
  • Concurrent and Distributed Programming
  • OCaml

Metrics

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

Related Versions

Supplementary Materials

References

  1. Kristoffer Just Arndal Andersen and Ilya Sergey. Distributed protocol combinators. In Practical Aspects of Declarative Languages - 21th International Symposium, PADL 2019, Lisbon, Portugal, January 14-15, 2019, Proceedings, volume 11372 of Lecture Notes in Computer Science, pages 169-186. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-05998-9_11.
  2. Robert Atkey. Parameterized Notions of Computation. Journal of Functional Programming, 19(3-4):335-376, 2009. URL: https://doi.org/10.1017/S095679680900728X.
  3. Paul Barham, Boris Dragovic, Keir Fraser, Steven Hand, Timothy L. Harris, Alex Ho, Rolf Neugebauer, Ian Pratt, and Andrew Warfield. Xen and the art of virtualization. In Proceedings of the 19th ACM Symposium on Operating Systems Principles 2003, SOSP 2003, Bolton Landing, NY, USA, October 19-22, 2003, pages 164-177, 2003. URL: https://doi.org/10.1145/945445.945462.
  4. Frédéric Bour, Thomas Refis, and Gabriel Scherer. Merlin: a language server for ocaml (experience report). PACMPL, 2(ICFP):103:1-103:15, 2018. URL: https://doi.org/10.1145/3236798.
  5. Edwin Charles Brady. Type driven development of concurrent communicating systems. Computer Science, 18(3), July 2017. URL: https://doi.org/10.7494/csci.2017.18.3.1413.
  6. Luís Caires and Jorge A. Pérez. Multiparty session types within a canonical binary theory, and beyond. In Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings, volume 9688 of Lecture Notes in Computer Science, pages 74-95. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-39570-8_6.
  7. Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. Coherence generalises duality: A logical explanation of multiparty session types. In 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs, pages 33:1-33:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.33.
  8. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: multiparty asynchronous global programming. In 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.
  9. David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. Distributed Programming Using Role Parametric Session Types in Go. In 46th ACM SIGPLAN Symposium on Principles of Programming Languages, volume 3, pages 29:1-29:30. ACM, 2019. Google Scholar
  10. Patrick Chanezon. Docker for mac and windows beta: the simplest way to use docker on your laptop, March 2016. URL: https://blog.docker.com/2016/03/docker-for-mac-windows-beta/.
  11. Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. A gentle introduction to multiparty asynchronous session types. In Formal Methods for Multicore Programming, volume 9104 of LNCS, pages 146-178. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-18941-3_4.
  12. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session Types Revisited. In PPDP '12: Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming, pages 139-150, New York, NY, USA, 2012. ACM. URL: https://doi.org/10.1145/2370776.2370794.
  13. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty session types meet communicating automata. In ESOP, volume 7211 of LNCS, pages 194-213. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28869-2.
  14. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In ICALP, volume 7966 of LNCS, pages 174-186. Springer, 2013. Google Scholar
  15. Fabrice Le Fessant. MLDonkey, 2002. http://mldonkey.sourceforge.net/. Google Scholar
  16. J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Trans. Program. Lang. Syst., 29(3):17, 2007. URL: https://doi.org/10.1145/1232420.1232424.
  17. Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. J. Log. Algebr. Meth. Program., 104:127-173, 2019. URL: https://doi.org/10.1016/j.jlamp.2018.12.002.
  18. Dick Hardt. The OAuth 2.0 Authorization Framework. RFC 6749, October 2012. URL: https://doi.org/10.17487/RFC6749.
  19. Robert Harper and Benjamin C. Pierce. A record calculus based on symmetric concatenation. In Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, Orlando, Florida, USA, January 21-23, 19x91, pages 131-142, 1991. URL: https://doi.org/10.1145/99583.99603.
  20. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL'08, pages 273-284. ACM, 2008. Google Scholar
  21. 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.
  22. Raymond Hu and Nobuko Yoshida. Hybrid session verification through endpoint API generation. In FASE, volume 9633 of LNCS, pages 401-418. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49665-7_24.
  23. Raymond Hu and Nobuko Yoshida. Explicit connection actions in multiparty session types. In FASE, volume 10202 of LNCS, pages 116-133, 2017. URL: https://doi.org/10.1007/978-3-662-54494-5_7.
  24. Keigo Imai and Jacques Garrigue. Lightweight linearly-typed programming with lenses and monads. Journal of Information Processing, 27:431-444, 2019. URL: https://doi.org/10.2197/ipsjjip.27.431.
  25. Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty session programming with global protocol combinators, 2020. URL: http://arxiv.org/abs/2005.06333.
  26. Keigo Imai, Nobuko Yoshida, and Shoji Yuen. Session-ocaml: A session-based library with polarities and lenses. In COORDINATION, volume 10319 of LNCS, pages 99-118. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-59746-1_6.
  27. Keigo Imai, Nobuko Yoshida, and Shoji Yuen. Session-ocaml: a Session-based Library with Polarities and Lenses. Sci. Comput. Program., 172:135-159, 2018. URL: https://doi.org/10.1016/j.scico.2018.08.005.
  28. Shams Imam and Vivek Sarkar. Savina - An Actor Benchmark Suite: Enabling Empirical Evaluation of Actor Libraries. In AGERE, pages 67-80. ACM, 2014. Google Scholar
  29. Oleg Kiselyov. Simple variable-state monad, December 2006. Mailing list message. URL: http://www.haskell.org/pipermail/haskell/2006-December/018917.html.
  30. Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. Typechecking protocols with Mungo and StMungo. In PPDP, pages 146-159, 2016. URL: https://doi.org/10.1145/2967973.2968595.
  31. Sam Lindley and J. Garrett Morris. Embedding Session Types in Haskell. In Haskell 2016: Proceedings of the 9th International Symposium on Haskell, pages 133-145. ACM, 2016. URL: https://doi.org/10.1145/2976002.2976018.
  32. Anil Madhavapeddy. Xen and the art of OCaml. In Commercial Uses of Functional Programming (CUFP), September 2008. Google Scholar
  33. Anil Madhavapeddy and David J. Scott. Unikernels: the rise of the virtual library operating system. Commun. ACM, 57(1):61-69, 2014. URL: https://doi.org/10.1145/2541883.2541895.
  34. Dirk Merkel. Docker: Lightweight linux containers for consistent development and deployment. Linux Journal, 2014(239), March 2014. URL: http://dl.acm.org/citation.cfm?id=2600239.2600241.
  35. Yaron Minsky. OCaml for the Masses. Commun. ACM, 54(11):53-58, 2011. URL: https://doi.org/10.1145/2018396.2018413.
  36. 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, February 24-25, 2018, Vienna, Austria, pages 128-138. ACM, 2018. URL: https://doi.org/10.1145/3178372.3179495.
  37. Rumyana Neykova and Nobuko Yoshida. Featherweight Scribble. In Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, pages 236-259, 2019. URL: https://doi.org/10.1007/978-3-030-21485-2_14.
  38. Nick Benton. Jingle Bells: Solving the Santa Claus Problem in Polyphonic C♯, 2003. Available at URL: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/santa.pdf.
  39. Dominic Orchard and Nobuko Yoshida. Effects as sessions, sessions as effects. In POPL 2016: 43th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 568-581. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837634.
  40. Luca Padovani. A Simple Library Implementation of Binary Sessions. Journal of Functional Programming, 27:e4, 2016. Google Scholar
  41. Luca Padovani. Context-free session type inference. ACM Trans. Program. Lang. Syst., 41(2):9:1-9:37, 2019. URL: https://doi.org/10.1145/3229062.
  42. Matthew Pickering, Jeremy Gibbons, and Nicolas Wu. Profunctor Optics: Modular Data Accessors. The Art, Science, and Engineering of Programming, 1(2):Article 7, 2017. URL: https://doi.org/10.22152/programming-journal.org/2017/1/7.
  43. Riccardo Pucella and Jesse A. Tov. Haskell session types with (almost) no class. In Haskell'08, pages 25-36, New York, NY, USA, 2008. ACM. URL: https://doi.org/10.1145/1411286.1411290.
  44. Gabriel Radanne, Jérôme Vouillon, and Vincent Balat. Eliom: A core ML language for tierless web programming. In Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, pages 377-397, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_20.
  45. John H. Reppy. Concurrent ML: Design, Application and Semantics. In Functional Programming, Concurrency, Simulation and Automated Reasoning: International Lecture Series 1991-1992, McMaster University, Hamilton, Ontario, Canada, pages 165-198, 1993. URL: https://doi.org/10.1007/3-540-56883-2_10.
  46. Davide Sangiorgi and David Walker. The π-Calculus: a Theory of Mobile Processes. Cambridge University Press, 2001. Google Scholar
  47. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In ECOOP, 2017. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2017.24.
  48. Alceste Scalas and Nobuko Yoshida. Lightweight session programming in scala. In ECOOP, volume 56 of LIPIcs, pages 21:1-21:28, 2016. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2016.21.
  49. Alceste Scalas and Nobuko Yoshida. Less Is More: Multiparty Session Types Revisited. In 46th ACM SIGPLAN Symposium on Principles of Programming Languages, pages 1-29. ACM, 2019. Google Scholar
  50. Scribble home page, 2019. URL: http://www.scribble.org.
  51. Ilya Sergey, James R. Wilcox, and Zachary Tatlock. Programming and proving with distributed protocols. PACMPL, 2(POPL):28:1-28:30, 2018. URL: https://doi.org/10.1145/3158116.
  52. António Ravara Simon Gay, editor. Behavioural Types: from Theory to Tools. River Publisher, 2017. URL: https://www.riverpublishers.com/research_details.php?book_id=439.
  53. The Scala Development Team. The Scala Programming Language, 2004. URL: http://scala.epfl.ch/index.html.
  54. Bernardo Toninho, Luís Caires, and Frank Pfenning. Higher-order processes, functions, and sessions: A monadic integration. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7792 of Lecture Notes in Computer Science, pages 350-369. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_20.
  55. Jesse A. Tov and Riccardo Pucella. Stateful contracts for affine types. In Andrew D. Gordon, editor, Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6012 of Lecture Notes in Computer Science, pages 550-569. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-11957-6_29.
  56. Jérôme Vouillon. Lwt: a cooperative thread library. In Proceedings of the ACM Workshop on ML, pages 3-12. ACM, 2008. Available at https://github.com/ocsigen/lwt. URL: https://doi.org/10.1145/1411304.1411307.
  57. Mitchell Wand. Type inference for record concatenation and multiple inheritance. Inf. Comput., 93(1):1-15, 1991. URL: https://doi.org/10.1016/0890-5401(91)90050-C.
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