Document Open Access Logo

A Sound Algorithm for Asynchronous Session Subtyping

Authors Mario Bravetti , Marco Carbone , Julien Lange , Nobuko Yoshida , Gianluigi Zavattaro

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.38.pdf
  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Author Details

Mario Bravetti
  • University of Bologna, Italy
  • INRIA FoCUS Team
Marco Carbone
  • IT University of Copenhagen, Denmark
Julien Lange
  • University of Kent, UK
Nobuko Yoshida
  • Imperial College London, UK
Gianluigi Zavattaro
  • University of Bologna, Italy
  • INRIA FoCUS Team

Funding

H2020-MSCA-RISE Project 778233 (BEHAPI); EPSRC EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1, and EP/N028201/1.

Cite AsGet BibTex

Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A Sound Algorithm for Asynchronous Session Subtyping. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 38:1-38:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.38

Abstract

Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of system, where a program has not precisely the expected behavior but a similar one. Unfortunately, recent work has shown that subtyping for session types in an asynchronous setting is undecidable. To cope with this negative result, the only approaches we are aware of either restrict the syntax of session types or limit communication (by considering forms of bounded asynchrony). Both approaches are too restrictive in practice, hence we proceed differently by presenting an algorithm for checking subtyping which is sound, but not complete (in some cases it terminates without returning a decisive verdict). The algorithm is based on a tree representation of the coinductive definition of asynchronous subtyping; this tree could be infinite, and the algorithm checks for the presence of finite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements our algorithm and we apply it to many examples that cannot be managed with the previous approaches.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
Keywords
  • Session types
  • Concurrency
  • Subtyping
  • Algorithm

Metrics

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

Related Versions

References

  1. Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson. On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels. In CAV 1998, pages 305-318, 1998. URL: https://doi.org/10.1007/BFb0028754.
  2. Parosh Aziz Abdulla and Bengt Jonsson. Verifying Programs with Unreliable Channels. In (LICS 1993), pages 160-170, 1993. URL: https://doi.org/10.1109/LICS.1993.287591.
  3. Roberto M. Amadio and Luca Cardelli. Subtyping Recursive Types. ACM Trans. Program. Lang. Syst., 15(4):575-631, 1993. URL: https://doi.org/10.1145/155183.155231.
  4. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages, 3(2-3):95-230, 2016. URL: https://doi.org/10.1561/2500000031.
  5. The Authors. A sound algorithm for asynchronous session subtyping. https://github.com/julien-lange/asynchronous-subtyping, 2019.
  6. Daniel Brand and Pitro Zafiropulo. On Communicating Finite-State Machines. J. ACM, 30(2):323-342, 1983. URL: https://doi.org/10.1145/322374.322380.
  7. Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. Undecidability of asynchronous session subtyping. Inf. Comput., 256:300-320, 2017. Google Scholar
  8. Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci., 722:19-51, 2018. URL: https://doi.org/10.1016/j.tcs.2018.02.010.
  9. Gérard Cécé, Alain Finkel, and S. Purushothaman Iyer. Unreliable Channels are Easier to Verify Than Perfect Channels. Inf. Comput., 124(1):20-31, 1996. URL: https://doi.org/10.1006/inco.1996.0003.
  10. Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. On the Preciseness of Subtyping in Session Types. Logical Methods in Computer Science, 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:12)2017.
  11. Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. On the Preciseness of Subtyping in Session Types. In PPDP 2014, pages 146-135. ACM Press, 2014. Google Scholar
  12. Lorenzo Clemente, Frédéric Herbreteau, and Grégoire Sutre. Decidable Topologies for Communicating Automata with FIFO and Bag Channels. In CONCUR 2014, pages 281-296, 2014. URL: https://doi.org/10.1007/978-3-662-44584-6_20.
  13. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty Session Types Meet Communicating Automata. In ESOP 2012, pages 194-213, 2012. URL: https://doi.org/10.1007/978-3-642-28869-2_10.
  14. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In ICALP 2013, pages 174-186, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_18.
  15. N. Dilley and J. Lange. An Empirical Study of Messaging Passing Concurrency in Go Projects. In 2019 IEEE 26th International Conference on Software Analysis, Evolution and Reengineering (SANER), pages 377-387, February 2019. URL: https://doi.org/10.1109/SANER.2019.8668036.
  16. Simon J. Gay and Malcolm Hole. Types and Subtypes for Client-Server Interactions. In ESOP 1999, pages 74-90, 1999. URL: https://doi.org/10.1007/3-540-49099-X_6.
  17. Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Inf., 42(2-3):191-225, 2005. URL: https://doi.org/10.1007/s00236-005-0177-z.
  18. Blaise Genest, Dietrich Kuske, and Anca Muscholl. On Communicating Automata with Bounded Channels. Fundam. Inform., 80(1-3):147-167, 2007. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-09.
  19. Raymond Hu and Nobuko Yoshida. Hybrid Session Verification Through Endpoint API Generation. In FASE 2016, pages 401-418, 2016. URL: https://doi.org/10.1007/978-3-662-49665-7_24.
  20. Petr Jancar and Faron Moller. Techniques for Decidability and Undecidability of Bisimilarity. In CONCUR 1999, pages 30-45, 1999. URL: https://doi.org/10.1007/3-540-48320-9_5.
  21. Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient Recursive Subtyping. Mathematical Structures in Computer Science, 5(1):113-125, 1995. URL: https://doi.org/10.1017/S0960129500000657.
  22. Salvatore La Torre, P. Madhusudan, and Gennaro Parlato. Context-Bounded Analysis of Concurrent Queue Systems. In TACAS 2008, pages 299-314, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_21.
  23. Julien Lange and Nobuko Yoshida. Characteristic Formulae for Session Types. In TACAS, volume 9636 of Lecture Notes in Computer Science, pages 833-850. Springer, 2016. Google Scholar
  24. Julien Lange and Nobuko Yoshida. On the Undecidability of Asynchronous Session Subtyping. In FoSSaCS, volume 10203 of Lecture Notes in Computer Science, pages 441-457, 2017. Google Scholar
  25. Sam Lindley and J. Garrett Morris. Embedding session types in Haskell. In Haskell 2016, pages 133-145, 2016. URL: https://doi.org/10.1145/2976002.2976018.
  26. Dimitris Mostrous and Nobuko Yoshida. Session typing and asynchronous subtyping for the higher-order π-calculus. Inf. Comput., 241:227-263, 2015. URL: https://doi.org/10.1016/j.ic.2015.02.002.
  27. Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. Global Principal Typing in Partially Commutative Asynchronous Sessions. In ESOP 2009, pages 316-332, 2009. URL: https://doi.org/10.1007/978-3-642-00590-9_23.
  28. Rumyana Neykova, Raymond Hu, Nobuko Yoshida, and Fahd Abdeljallal. A Session Type Provider: Compile-time API Generation for Distributed Protocols with Interaction Refinements in F♯. In CC 2018. ACM, 2018. Google Scholar
  29. Dominic A. Orchard and Nobuko Yoshida. Effects as sessions, sessions as effects. In POPL 2016, pages 568-581, 2016. URL: https://doi.org/10.1145/2837614.2837634.
  30. Luca Padovani. A simple library implementation of binary sessions. J. Funct. Program., 27:e4, 2017. URL: https://doi.org/10.1017/S0956796816000289.
  31. Wuxu Peng and S. Purushothaman. Analysis of a Class of Communicating Finite State Machines. Acta Inf., 29(6/7):499-522, 1992. URL: https://doi.org/10.1007/BF01185558.
  32. Alceste Scalas and Nobuko Yoshida. Lightweight Session Programming in Scala. In ECOOP 2016, pages 21:1-21:28, 2016. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2016.21.
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