Document Open Access Logo

A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming

Authors Alceste Scalas, Ornela Dardha, Raymond Hu, Nobuko Yoshida

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.24.pdf
  • Filesize: 0.94 MB
  • 31 pages

Document Identifiers

Author Details

Alceste Scalas
Ornela Dardha
Raymond Hu
Nobuko Yoshida

Cite AsGet BibTex

Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 24:1-24:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ECOOP.2017.24

Abstract

Multiparty Session Types (MPST) is a typing discipline for message-passing distributed processes that can ensure properties such as absence of communication errors and deadlocks, and protocol conformance. Can MPST provide a theoretical foundation for concurrent and distributed programming in "mainstream" languages? We address this problem by (1) developing the first encoding of a full-fledged multiparty session pi-calculus into linear pi-calculus, and (2) using the encoding as the foundation of a practical toolchain for safe multiparty programming in Scala. Our encoding is type-preserving and operationally sound and complete. Crucially, it keeps the distributed choreographic nature of MPST, illuminating that the safety properties of multiparty sessions can be precisely represented with a decomposition into binary linear channels. Previous works have only studied the relation between (limited) multiparty and binary sessions via centralised orchestration means. We exploit these results to implement an automated generation of Scala APIs for multiparty sessions, abstracting existing libraries for binary communication channels. This allows multiparty systems to be safely implemented over binary message transports, as commonly found in practice. Our implementation is the first to support distributed multiparty delegation: our encoding yields it for free, via existing mechanisms for binary delegation.
Keywords
  • process calculi
  • session types
  • concurrent programming
  • Scala

Metrics

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

Supplementary Materials

References

  1. Giovanni Bernardi and Matthew Hennessy. Using higher-order contracts to model session types (extended abstract). In CONCUR, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44584-6_27.
  2. Giovanni Bernardi and Matthew Hennessy. Using higher-order contracts to model session types. Logical Methods in Computer Science, 12(2), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(2:10)2016.
  3. Lorenzo Bettini, Mario Coppo, Loris D'Antoni, Marco De Luca, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. Global progress in dynamically interleaved multiparty sessions. In CONCUR, 2008. URL: http://dx.doi.org/10.1007/978-3-540-85361-9_33.
  4. Laura Bocchi, Julien Lange, and Nobuko Yoshida. Meeting Deadlines Together. In CONCUR, 2015. URL: http://dx.doi.org/http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.283.
  5. Laura Bocchi, Julien Lange, and Nobuko Yoshida. Meeting Deadlines Together (long version). Technical report, 2015. Long version of [4]. URL: http://mrg.doc.ic.ac.uk/publications/meeting-deadlines-together/long.pdf.
  6. Viviana Bono and Luca Padovani. Typing copyless message passing. Logical Methods in Computer Science, 8(1), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(1:17)2012.
  7. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM, 30(2), April 1983. URL: http://dx.doi.org/10.1145/322374.322380.
  8. Luís Caires and Jorge A. Pérez. Multiparty session types within a canonical binary theory, and beyond. In FORTE, 2016. URL: http://dx.doi.org/10.1007/978-3-319-39570-8_6.
  9. Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. Coherence generalises duality: A logical explanation of multiparty session types. In CONCUR, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.33.
  10. Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. Inference of global progress properties for dynamically interleaved multiparty sessions. In COORDINATION, 2013. URL: http://dx.doi.org/10.1007/978-3-642-38493-6_4.
  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, 2015. URL: http://dx.doi.org/10.1007/978-3-319-18941-3_4.
  12. Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global Progress for Dynamically Interleaved Multiparty Sessions. Mathematical Structures in Computer Science, 760, 2015. URL: http://dx.doi.org/10.1017/S0960129514000188.
  13. Ornela Dardha. Recursive session types revisited. In BEAT, 2014. URL: http://dx.doi.org/10.4204/EPTCS.162.4.
  14. Ornela Dardha. Type Systems for Distributed Programs: Components and Sessions, volume 7 of Atlantis Studies in Computing. Atlantis Press, July 2016. URL: http://dx.doi.org/10.2991/978-94-6239-204-5.
  15. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. In PPDP, 2012. URL: http://dx.doi.org/10.1145/2370776.2370794.
  16. Romain Demangeon and Kohei Honda. Full abstraction in a subtyped pi-calculus with linear types. In CONCUR, 2011. URL: http://dx.doi.org/10.1007/978-3-642-23217-6_19.
  17. 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 in System Design, 2015. URL: http://dx.doi.org/10.1007/s10703-014-0218-8.
  18. Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. Logical Methods in Computer Science, 8(4), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(4:6)2012.
  19. Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. In PLACES, pages 29-43, 2015. URL: http://dx.doi.org/10.4204/EPTCS.203.3.
  20. Simon Fowler. An Erlang implementation of multiparty session actors. In ICE, 2016. URL: http://dx.doi.org/10.4204/EPTCS.223.3.
  21. Simon J. Gay, Nils Gesbert, and António Ravara. Session types as generic process types. In EXPRESS/SOS, 2014. URL: http://dx.doi.org/10.4204/EPTCS.160.9.
  22. Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2-3), 2005. URL: http://dx.doi.org/10.1007/s00236-005-0177-z.
  23. Daniele Gorla. Towards a unified approach to encodability and separation results for process calculi. Inf. Comput., 208(9), 2010. URL: http://dx.doi.org/10.1016/j.ic.2010.05.002.
  24. Philipp Haller and Alexander Loiko. LaCasa: lightweight affinity and object capabilities in Scala. In OOPSLA, 2016. URL: http://dx.doi.org/10.1145/2983990.2984042.
  25. Philipp Haller and Martin Odersky. Capabilities for uniqueness and borrowing. In ECOOP, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14107-2_17.
  26. Kohei Honda, Vasco Vasconcelos, and Makoto Kubo. Language primitives and type disciplines for structured communication-based programming. In ESOP, 1998. URL: http://dx.doi.org/10.1007/BFb0053567.
  27. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL, 2008. Full version in [28]. URL: http://dx.doi.org/10.1145/1328438.1328472.
  28. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1), March 2016. URL: http://dx.doi.org/10.1145/2827695.
  29. Raymond Hu and Nobuko Yoshida. Hybrid session verification through endpoint API generation. In FASE, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49665-7_24.
  30. Raymond Hu, Nobuko Yoshida, and Kohei Honda. Session-based distributed programming in java. In ECOOP, 2008. URL: http://dx.doi.org/10.1007/978-3-540-70592-5_22.
  31. Atsushi Igarashi and Naoki Kobayashi. A generic type system for the pi-calculus. Theo. Comput. Sci., 311(1-3), 2004. URL: http://dx.doi.org/10.1016/S0304-3975(03)00325-6.
  32. Keigo Imai, Shoji Yuen, and Kiyoshi Agusa. Session type inference in Haskell. In PLACES, 2010. URL: http://dx.doi.org/10.4204/EPTCS.69.6.
  33. Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. Session types for Rust. In WGP@ICFP, 2015. URL: http://dx.doi.org/10.1145/2808098.2808100.
  34. Naoki Kobayashi. Type systems for concurrent programs. In 10th Anniversary Colloquium of UNU/IIST, 2002. URL: http://dx.doi.org/10.1007/978-3-540-40007-3_26.
  35. Naoki Kobayashi. A new type system for deadlock-free processes. In CONCUR, 2006. URL: http://dx.doi.org/10.1007/11817949_16.
  36. Naoki Kobayashi. Type systems for concurrent programs. Extended version of [34], Tohoku University, 2007. URL: http://www.kb.ecei.tohoku.ac.jp/~koba/papers/tutorial-type-extended.pdf.
  37. Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst., 21(5), September 1999. URL: http://dx.doi.org/10.1145/330249.330251.
  38. Naoki Kobayashi and Davide Sangiorgi. A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst., 32(5), 2010. Google Scholar
  39. Dimitrios Kouzapas and Nobuko Yoshida. Globally governed session semantics. In CONCUR, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40184-8_28.
  40. Dimitrios Kouzapas and Nobuko Yoshida. Globally governed session semantics. Logical Methods in Computer Science, 10(4), 2014. URL: http://dx.doi.org/10.2168/LMCS-10(4:20)2014.
  41. Lightbend, Inc. The Akka framework, 2017. URL: http://akka.io/.
  42. Sam Lindley and J. Garrett Morris. Embedding session types in Haskell. In Haskell, 2016. URL: http://dx.doi.org/10.1145/2976002.2976018.
  43. Sam Lindley and J. Garrett Morris. Talking bananas: Structural recursion for session types. In ICFP, 2016. URL: http://dx.doi.org/10.1145/2951913.2951921.
  44. Links homepage. http://links-lang.org/. S. Fowler and D. Hillerström and S. Lindley and G. Morris and P. Wadler.
  45. Barbara H. Liskov and Jeannette M. Wing. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst., 16(6), November 1994. URL: http://dx.doi.org/10.1145/197320.197383.
  46. Hugo A. Lopez, Eduardo R. B. Marques, Francisco Martins, Nicholas Ng, Casar Santos, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. Protocol-based verification of message-passing parallel programs. In OOPSLA, 2015. URL: http://dx.doi.org/10.1145/2814270.2814302.
  47. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, parts I and II. Inf. Comput., 100(1), 1992. URL: http://dx.doi.org/10.1016/0890-5401(92)90008-4.
  48. Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. Timed Runtime Monitoring for Multiparty Conversations. In BEAT, volume 162. EPTCS, 2014. Full version in [49]. URL: http://dx.doi.org/10.4204/EPTCS.162.3.
  49. Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. Timed runtime monitoring for multiparty conversations. Formal Aspects of Computing, 2017. URL: http://dx.doi.org/10.1007/s00165-017-0420-8.
  50. Rumyana Neykova and Nobuko Yoshida. Let It Recover: Multiparty Protocol-Induced Recovery. In CC, 2017. URL: http://dx.doi.org/10.1145/3033019.3033031.
  51. Rumyana Neykova and Nobuko Yoshida. Multiparty Session Actors. Logical Methods in Computer Science, 13(1), March 2017. URL: http://dx.doi.org/10.23638/LMCS-13(1:17)2017.
  52. Dominic A. Orchard and Nobuko Yoshida. Effects as sessions, sessions as effects. In POPL, 2016. URL: http://dx.doi.org/10.1145/2837614.2837634.
  53. Luca Padovani. Deadlock and lock freedom in the linear π-calculus. Online version of [54], January 2014. URL: https://hal.inria.fr/hal-00932356.
  54. Luca Padovani. Deadlock and lock freedom in the linear π-calculus. In CSL-LICS. ACM, 2014. URL: http://dx.doi.org/10.1145/2603088.2603116.
  55. Luca Padovani. A simple library implementation of binary sessions. Journal of Functional Programming, 27, 2017. Website: http://www.di.unito.it/~padovani/Software/FuSe/FuSe.html. URL: http://dx.doi.org/10.1017/S0956796816000289.
  56. Benjamin C. Pierce. Types and programming languages. MIT Press, MA, USA, 2002. Google Scholar
  57. Riccardo Pucella and Jesse A. Tov. Haskell session types with (almost) no class. In Haskell, 2008. URL: http://dx.doi.org/10.1145/1411286.1411290.
  58. Lukas Rytz, Martin Odersky, and Philipp Haller. Lightweight polymorphic effects. In ECOOP, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31057-7_13.
  59. Davide Sangiorgi and David Walker. The π-calculus: a Theory of Mobile Processes. Cambridge University Press, 2001. Google Scholar
  60. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A linear decomposition of multiparty sessions for safe distributed programming. Technical Report 2, Imperial College London, 2017. URL: https://www.doc.ic.ac.uk/research/technicalreports/2017/#2.
  61. Alceste Scalas and Nobuko Yoshida. Lightweight session programming in scala. In ECOOP, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2016.21.
  62. Alceste Scalas and Nobuko Yoshida. Lightweight Session Programming in Scala (Artifact). Dagstuhl Artifacts Series, 2(1), 2016. URL: http://dx.doi.org/http://dx.doi.org/10.4230/DARTS.2.1.11.
  63. Scribble homepage. URL: http://www.scribble.org.
  64. K. C. Sivaramakrishnan, Karthik Nagaraj, Lukasz Ziarek, and Patrick Eugster. Efficient session type guided distributed interaction. In COORDINATION, 2010. URL: http://dx.doi.org/10.1007/978-3-642-13414-2_11.
  65. Matías Toro and Éric Tanter. Customizable gradual polymorphic effects for Scala. In OOPSLA, 2015. URL: http://dx.doi.org/10.1145/2814270.2814315.
  66. TYPICAL. Type-based static analyzer for the pi-calculus. URL: http://www-kb.is.s.u-tokyo.ac.jp/~koba/typical/.
  67. Nobuko Yoshida, Pierre-Malo Deniélou, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. In FOSSACS, 2010. URL: http://dx.doi.org/10.1007/978-3-642-12032-9_10.
  68. Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. The Scribble protocol language. In TGC, 2013. URL: http://dx.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 Imprint Privacy Contact