Document Open Access Logo

Completeness of Asynchronous Session Tree Subtyping in Coq

Authors Burak Ekici , Nobuko Yoshida

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.13.pdf
  • Filesize: 1.05 MB
  • 20 pages

Document Identifiers

Author Details

Burak Ekici
  • Department of Computer Science, University of Oxford, UK
Nobuko Yoshida
  • Department of Computer Science, University of Oxford, UK

Funding

This work is partially supported by EPSRC EP/T006544/2, EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/2, EP/N028201/1, EP/T014709/2, EP/V000462/1, EP/X015955/1, NCSS/EPSRC VeTSS, and Horizon EU TaRDIS 101093006.

Acknowledgements

We would like to thank Dawit Tirore, Marco Giunti and Mukesh Tiwari for their feedback on the previous versions of this paper; Jovanka Vanja Pantovic and Alceste Scalas for a comprehensive discussion on the negation of the refinement relation. We also thank anonymous referees for their constructive input.

Cite AsGet BibTex

Burak Ekici and Nobuko Yoshida. Completeness of Asynchronous Session Tree Subtyping in Coq. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.13

Abstract

Multiparty session types (MPST) serve as a foundational framework for formally specifying and verifying message passing protocols. Asynchronous subtyping in MPST allows for typing optimised programs preserving type safety and deadlock freedom under asynchronous interactions where the message order is preserved and sending is non-blocking. The optimisation is obtained by message reordering, which allows for sending messages earlier or receiving them later. Sound subtyping algorithms have been extensively studied and implemented as part of various programming languages and tools including C, Rust and C-MPI. However, formalising all such permutations under sequencing, selection, branching and recursion in session types is an intricate task. Additionally, checking asynchronous subtyping has been proven to be undecidable. This paper introduces the first formalisation of asynchronous subtyping in MPST within the Coq proof assistant. We first decompose session types into session trees that do not involve branching and selection, and then establish a coinductive refinement relation over them to govern subtyping. To showcase our formalisation, we prove example subtyping schemas that appear in the literature, all of which cannot be verified, at the same time, by any of the existing decidable sound algorithms. Additionally, we take the (inductive) negation of the refinement relation from a prior work by Ghilezan et al. [Ghilezan et al., 2023] and re-implement it, significantly reducing the number of rules (from eighteen to eight). We establish the completeness of subtyping with respect to its negation in Coq, addressing the issues concerning the negation rules outlined in the previous work [Ghilezan et al., 2023]. In the formalisation, we use the greatest fixed point of the least fixed point technique, facilitated by the paco library, to define coinductive predicates. We employ parametrised coinduction to prove their properties. The formalisation consists of roughly 10K lines of Coq code, accessible at: https://github.com/ekiciburak/sessionTreeST/tree/itp2024.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Concurrent computing methodologies
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
  • Theory of computation → Proof theory
Keywords
  • asynchronous multiparty session types
  • session trees
  • subtyping
  • Coq

Metrics

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

Supplementary Materials

References

  1. Alexander Bagnall, Gordon Stewart, and Anindya Banerjee. Inductive reasoning for coinductive types. CoRR, abs/2301.09802, 2023. URL: https://doi.org/10.48550/arXiv.2301.09802.
  2. Laura Bocchi, Andy King, and Maurizio Murgia. Asynchronous subtyping by trace relaxation. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14570 of Lecture Notes in Computer Science, pages 207-226. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57246-3_12.
  3. Edwin C. Brady. Type-driven development of concurrent communicating systems. Comput. Sci., 18(3), 2017. URL: https://doi.org/10.7494/CSCI.2017.18.3.1413.
  4. 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.
  5. Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A Sound Algorithm for Asynchronous Session Subtyping and its Implementation. Logical Methods in Computer Science, Volume 17, Issue 1, March 2021. URL: https://doi.org/10.23638/LMCS-17(1:20)2021.
  6. Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. Undecidability of asynchronous session subtyping. Inf. Comput., 256:300-320, 2017. Google Scholar
  7. 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.
  8. Mario Bravetti, Julien Lange, and Gianluigi Zavattaro. Fair refinement for asynchronous session types. In FoSSaCS, Lecture Notes in Computer Science, 2021. Google Scholar
  9. David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, and Nobuko Yoshida. Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. In Stephen N. Freund and Eran Yahav, editors, PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, pages 237-251. ACM, 2021. URL: https://doi.org/10.1145/3453483.3454041.
  10. David Castro-Perez and Nobuko Yoshida. CAMP: cost-aware multiparty session protocols. Proc. ACM Program. Lang., 4(OOPSLA):155:1-155:30, 2020. URL: https://doi.org/10.1145/3428223.
  11. Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. On the Preciseness of Subtyping in Session Types. LMCS, 13:1-62, 2017. Google Scholar
  12. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. A formal theory of choreographic programming. J. Autom. Reason., 67(2):21, 2023. URL: https://doi.org/10.1007/S10817-023-09665-3.
  13. Zak Cutner and Nobuko Yoshida. Safe Session-Based Asynchronous Coordination in Rust. In Ferruccio Damiani and Ornela Dardha, editors, Coordination Models and Languages - 23rd IFIP WG 6.1 International Conference, COORDINATION 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, volume 12717 of Lecture Notes in Computer Science, pages 80-89. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-78142-2_5.
  14. Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-free asynchronous message reordering in Rust with multiparty session types. In Jaejin Lee, Kunal Agrawal, and Michael F. Spear, editors, PPoPP '22: 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Seoul, Republic of Korea, April 2 - 6, 2022, pages 246-261. ACM, 2022. URL: https://doi.org/10.1145/3503221.3508404.
  15. Romain Demangeon and Kohei Honda. Full Abstraction in a Subtyped pi-Calculus with Linear Types. In 22nd International Conference on Concurrency Theory, volume 6901 of LNCS, pages 280-296. Springer, 2011. Google Scholar
  16. Romain Demangeon and Kohei Honda. Nested protocols in session types. In Maciej Koutny and Irek Ulidowski, editors, CONCUR 2012 - Concurrency Theory - 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings, volume 7454 of Lecture Notes in Computer Science, pages 272-286. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32940-1_20.
  17. Burak Ekici and Nobuko Yoshida. https://github.com/ekiciburak/sessionTreeST/tree/localtype. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:33823a0054801bcf4ea95f2dffe733579cbd53c8;origin=https://github.com/ekiciburak/sessionTreeST;visit=swh:1:snp:e36eb4662d8731a175e95b8081f861339f588412;anchor=swh:1:rev:a8aafb319882c90f11b2b43032ce9faabace5f95 (visited on 2024-08-20). URL: https://github.com/ekiciburak/sessionTreeST/tree/itp2024.
  18. 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.
  19. Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19-50, 2010. URL: https://doi.org/10.1017/S0956796809990268.
  20. Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. JLAMP, 104:127-173, 2019. Google Scholar
  21. Silvia Ghilezan, Jovanka Pantovic, Ivan Prokic, Alceste Scalas, and Nobuko Yoshida. Precise Subtyping for Asynchronous Multiparty Sessions. Proc. ACM Program. Lang., 5:16:1-16:28, January 2021. Google Scholar
  22. Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for asynchronous multiparty sessions. ACM Trans. Comput. Logic, 24(2), November 2023. URL: https://doi.org/10.1145/3568422.
  23. Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers. Actris: session-type based reasoning in separation logic. Proc. ACM Program. Lang., 4(POPL):6:1-6:30, 2020. URL: https://doi.org/10.1145/3371074.
  24. Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers. Actris 2.0: Asynchronous session-type based reasoning in separation logic. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/LMCS-18(2:16)2022.
  25. Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson. Machine-checked semantic session typing. In Catalin Hritcu and Andrei Popescu, editors, CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 178-198. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439914.
  26. Andrew K. Hirsch and Deepak Garg. Pirouette: higher-order typed functional choreographies. Proc. ACM Program. Lang., 6(POPL):1-27, 2022. URL: https://doi.org/10.1145/3498684.
  27. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP 1998, pages 122-138, 1998. URL: https://doi.org/10.1007/BFb0053567.
  28. Kohei Honda, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. Type-Directed Compilation for Multicore Programming. ENTCS, 241:101-111, 2009. Google Scholar
  29. Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The power of parameterization in coinductive proof. In Roberto Giacobazzi and Radhia Cousot, editors, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pages 193-206. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429093.
  30. Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Multiparty GV: functional multiparty session types with certified deadlock freedom. Proc. ACM Program. Lang., 6(ICFP):466-495, 2022. URL: https://doi.org/10.1145/3547638.
  31. Jules Jacobs, Jonas Kastberg Hinrichsen, and Robbert Krebbers. Deadlock-free separation logic: Linearity yields progress for dependent higher-order message passing. Proc. ACM Program. Lang., 8(POPL):1385-1417, 2024. URL: https://doi.org/10.1145/3632889.
  32. 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
  33. Nicholas Ng, Jose G.F. Coutinho, and Nobuko Yoshida. Protocols by Default: Safe MPI Code Generation based on Session Types. In 24th International Conference on Compiler Construction, volume 9031 of LNCS, pages 212-232. Springer, 2015. Google Scholar
  34. Nicholas Ng, Nobuko Yoshida, and Kohei Honda. Multiparty Session C: Safe Parallel Programming with Message Optimisation. In 50th International Conference on Objects, Models, Components, Patterns, volume 7304 of LNCS, pages 202-218. Springer, 2012. Google Scholar
  35. Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, and Michael Norrish. Kalas: A verified, end-to-end compiler for a choreographic language. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, volume 237 of LIPIcs, pages 27:1-27:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.ITP.2022.27.
  36. Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An interaction-based language and its typing system. In PARLE 1994, pages 398-413, 1994. URL: https://doi.org/10.1007/3-540-58184-7_118.
  37. Joseph Tassarotti, Ralf Jung, and Robert Harper. A higher-order logic for concurrent termination-preserving refinement. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 909-936. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_34.
  38. The Coq Development Team. The Coq reference manual - release 8.18.0. https://coq.inria.fr/doc/V8.18.0/refman, 2023.
  39. Peter Thiemann. Intrinsically-typed mechanized semantics for session types. In Ekaterina Komendantskaya, editor, Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, October 7-9, 2019, pages 19:1-19:15. ACM, 2019. URL: https://doi.org/10.1145/3354166.3354184.
  40. Dawit Legesse Tirore, Jesper Bengtson, and Marco Carbone. A sound and complete projection for global types. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, volume 268 of LIPIcs, pages 28:1-28:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.ITP.2023.28.
  41. Nobuko Yoshida and Lorenzo Gheri. A very gentle introduction to multiparty session types. In Dang Van Hung and Meenakshi D'Souza, editors, Distributed Computing and Internet Technology - 16th International Conference, ICDCIT 2020, Bhubaneswar, India, January 9-12, 2020, Proceedings, volume 11969 of Lecture Notes in Computer Science, pages 73-93. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-36987-3_5.
  42. Nobuko Yoshida, Vasco Thudichum Vasconcelos, Hervé Paulino, and Kohei Honda. Session-based compilation framework for multicore programming. In FMCO 2008, pages 226-246, 2008. URL: https://doi.org/10.1007/978-3-642-04167-9_12.
  43. Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic. An equational theory for weak bisimulation via generalized parameterized coinduction. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 71-84. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373813.
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