Document Open Access Logo

Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation

Authors Martin Vassor , Nobuko Yoshida

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.41.pdf
  • Filesize: 1.15 MB
  • 29 pages

Document Identifiers

Author Details

Martin Vassor
  • University of Oxford, UK
Nobuko Yoshida
  • University of Oxford, UK

Funding

Work supported by: EPSRC EP/T00006544/2, EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/2, EP/N028201/1, EP/T014709/2, EP/V000462, EP/X015955/1n NCSS/EPSRC VeTSS, and Horizon EU TaRDIS 101093006.

Acknowledgements

We thank B. Ekici, M. Giunti, P. Hou, A. Suresh, and F. Zhou.

Cite AsGet BibTex

Martin Vassor and Nobuko Yoshida. Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 41:1-41:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.41

Abstract

Multiparty message-passing protocols are notoriously difficult to design, due to interaction mismatches that lead to errors such as deadlocks. Existing protocol specification formats have been developed to prevent such errors (e.g. multiparty session types (MPST)). In order to further constrain protocols, specifications can be extended with refinements, i.e. logical predicates to control the behaviour of the protocol based on previous values exchanged. Unfortunately, existing refinement theories and implementations are tightly coupled with specification formats. This paper proposes a framework for multiparty message-passing protocols with refinements and its implementation in Rust. Our work decouples correctness of refinements from the underlying model of computation, which results in a specification-agnostic framework. Our contributions are threefold. First, we introduce a trace system which characterises valid refined traces, i.e. a sequence of sending and receiving actions correct with respect to refinements. Second, we give a correct model of computation named refined communicating system (RCS), which is an extension of communicating automata systems with refinements. We prove that RCS only produce valid refined traces. We show how to generate RCS from mainstream protocol specification formats, such as refined multiparty session types (RMPST) or refined choreography automata. Third, we illustrate the flexibility of the framework by developing both a static analysis technique and an improved model of computation for dynamic refinement evaluation. Finally, we provide a Rust toolchain for decentralised RMPST, evaluate our implementation with a set of benchmarks from the literature, and observe that refinement overhead is negligible.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Specification languages
  • Theory of computation → Assertions
  • Theory of computation → Concurrency
Keywords
  • Message-Passing Concurrency
  • Session Types
  • Specification

Metrics

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

Supplementary Materials

References

  1. Franco Barbanera, Ivan Lanese, and Emilio Tuosto. Choreography automata. In Simon Bliudze and Laura Bocchi, editors, Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings, volume 12134 of Lecture Notes in Computer Science, pages 86-106. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-50029-0_6.
  2. Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida. Monitoring networks through multiparty session types. Theoretical Computer Science, 669:33-58, 2017. URL: https://doi.org/10.1016/j.tcs.2017.02.009.
  3. Laura Bocchi, Romain Demangeon, and Nobuko Yoshida. A Multiparty Multi-Session Logic. In 7th International Symposium on Trustworthy Global Computing, volume 8191 of LNCS, pages 111-97. Springer, 2012. Google Scholar
  4. Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. A Theory of Design-by-Contract for Distributed Multiparty Interactions. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, Lecture Notes in Computer Science, pages 162-176, Berlin, Heidelberg, 2010. Springer. URL: https://doi.org/10.1007/978-3-642-15375-4_12.
  5. Daniel Brand and Pitro Zafiropulo. On Communicating Finite-State Machines. Journal of the ACM, 30(2):323-342, April 1983. URL: https://doi.org/10.1145/322374.322380.
  6. Ruofei Chen and Stephanie Balzer. Ferrite: A Judgmental Embedding of Session Types in Rust, 2021. (repository is found at https://github.com/ferrite-rs/ferrite). URL: https://arxiv.org/abs/2009.13619.
  7. Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-free asynchronous message reordering in rust with multiparty session types. In Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '22, pages 246-261, New York, NY, USA, April 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3503221.3508404.
  8. Gérard Cécé and Alain Finkel. Verification of programs with half-duplex communication. Information and Computation, 202(2):166-190, November 2005. URL: https://doi.org/10.1016/j.ic.2005.05.006.
  9. Ankush Das and Frank Pfenning. Session Types with Arithmetic Refinements. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1-13:18, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.13.
  10. Ankush Das and Frank Pfenning. Rast: A Language for Resource-Aware Session Types. Logical Methods in Computer Science, Volume 18, Issue 1, January 2022. URL: https://doi.org/10.46298/lmcs-18(1:9)2022.
  11. Brady Dean and Joey Ezechiëls. refinement crate, 2021. (repository is found at https://github.com/2bdkid/refinement).
  12. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty Session Types Meet Communicating Automata. In 21st European Symposium on Programming, volume 7211 of LNCS, pages 194-213. Springer, 2012. Google Scholar
  13. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In 40th International Colloquium on Automata, Languages and Programming, volume 7966 of LNCS, pages 174-186, Berlin, Heidelberg, 2013. Springer. URL: https://doi.org/10.1007/978-3-642-39212-2_18.
  14. José Duarte and António Ravara. Retrofitting Typestates into Rust. In 25th Brazilian Symposium on Programming Languages, pages 83-91, Joinville Brazil, September 2021. ACM. URL: https://doi.org/10.1145/3475061.3475082.
  15. Francisco Ferreira, Fangyi Zhou, Simon Castellan, and Benito Echarren. NuScr, 2019. URL: https://github.com/nuscr/nuscr.
  16. Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida. Design-By-Contract for Flexible Multiparty Session Protocols. In Karim Ali and Jan Vitek, editors, 36th European Conference on Object-Oriented Programming (ECOOP 2022), volume 222 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1-8:28, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2022.8.
  17. Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers. Actris: Session-type based reasoning in separation logic. Proceedings of the ACM on Programming Languages, 4(POPL):1-30, January 2020. URL: https://doi.org/10.1145/3371074.
  18. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. ACM SIGPLAN Notices, 43(1):273-284, January 2008. URL: https://doi.org/10.1145/1328897.1328472.
  19. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Types. Journal of the ACM, 63(1):9:1-9:67, March 2016. URL: https://doi.org/10.1145/2827695.
  20. Raymond Hu, Dimitrios Kouzapas, Olivier Pernet, Nobuko Yoshida, and Kohei Honda. Type-safe eventful sessions in java. In Proceedings of the 24th European conference on Object-oriented programming, ECOOP'10, pages 329-353, Berlin, Heidelberg, June 2010. Springer-Verlag. Google Scholar
  21. Raymond Hu and Nobuko Yoshida. Hybrid Session Verification Through Endpoint API Generation. In Perdita Stevens and Andrzej Wąsowski, editors, Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, pages 401-418, Berlin, Heidelberg, 2016. Springer. URL: https://doi.org/10.1007/978-3-662-49665-7_24.
  22. Raymond Hu and Nobuko Yoshida. Explicit Connection Actions in Multiparty Session Types. In Marieke Huisman and Julia Rubin, editors, Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, pages 116-133, Berlin, Heidelberg, 2017. Springer. URL: https://doi.org/10.1007/978-3-662-54494-5_7.
  23. Raymond Hu, Nobuko Yoshida, and Kohei Honda. Session-Based Distributed Programming in Java. In Jan Vitek, editor, ECOOP 2008 – Object-Oriented Programming, Lecture Notes in Computer Science, pages 516-541, Berlin, Heidelberg, 2008. Springer. URL: https://doi.org/10.1007/978-3-540-70592-5_22.
  24. International Telecommunication Union. Z.120 : Message Sequence Chart (MSC), February 2011. Google Scholar
  25. Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. Session types for Rust. In Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, pages 13-22, Vancouver BC Canada, August 2015. ACM. URL: https://doi.org/10.1145/2808098.2808100.
  26. Wen Kokke. Rusty Variation: Deadlock-free Sessions with Failure in Rust. Electronic Proceedings in Theoretical Computer Science, 304:48-60, 2019. (repository is found at https://github.com/wenkokke/sesh). URL: https://doi.org/10.4204/eptcs.304.4.
  27. Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types. In Karim Ali and Jan Vitek, editors, 36th European Conference on Object-Oriented Programming (ECOOP 2022), volume 222 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1-4:29, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. ISSN: 1868-8969. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2022.4.
  28. Bertrand Meyer. Design by Contract. Advances in Object-Oriented Software Engineering, pages 1-35, 1991. Google Scholar
  29. 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, pages 128-138, New York, NY, USA, February 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3178372.3179495.
  30. Davide Sangiorgi. An Introduction to Bisimulation and Coinduction. Cambridge University Press, Cambridge ; New York, 2012. Google Scholar
  31. Alceste Scalas and Nobuko Yoshida. Less is more: multiparty session types revisited. Proceedings of the ACM on Programming Languages, 3(POPL):30:1-30:29, January 2019. URL: https://doi.org/10.1145/3290343.
  32. Felix Stutz. Asynchronous Multiparty Session Type Implementability is Decidable - Lessons Learned from Message Sequence Charts. In DROPS-IDN/v2/Document/10.4230/LIPIcs.ECOOP.2023.32. Schloss-Dagstuhl - Leibniz Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2023.32.
  33. Peter Thiemann and Vasco T. Vasconcelos. Label-dependent session types. Proceedings of the ACM on Programming Languages, 4(POPL):1-29, January 2020. URL: https://doi.org/10.1145/3371135.
  34. Bernardo Toninho, Luís Caires, and Frank Pfenning. Dependent session types via intuitionistic linear type theory. In Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming, pages 161-172, Odense Denmark, July 2011. ACM. URL: https://doi.org/10.1145/2003476.2003499.
  35. Martin Vassor and Nobuko Yoshida. Refinements for multiparty message-passing protocols: Specification-agnostic theory and implementation, 2024. Full version on Arxiv. Google Scholar
  36. Niki Vazou. Liquid Haskell: Haskell as a Theorem Prover. PhD thesis, University of California, San Diego, USA, 2016. URL: http://www.escholarship.org/uc/item/8dm057ws.
  37. Jules Villard. Heaps and Hops. PhD thesis, Laboratoire Spécification et Vérification, École Normale Supérieure de Cachan, France, February 2011. Google Scholar
  38. 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, Lecture Notes in Computer Science, pages 73-93, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-36987-3_5.
  39. Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. The scribble protocol language. In Martín Abadi and Alberto Lluch Lafuente, editors, Trustworthy Global Computing, pages 22-41, Cham, 2014. Springer International Publishing. Google Scholar
  40. Erik Zhang. Crepe, 2022. URL: https://crates.io/crates/crepe.
  41. Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Statically Verified Refinements for Multiparty Protocols. Proc. ACM Program. Lang., 4(OOPSLA), November 2020. URL: https://doi.org/10.1145/3428216.
  42. Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Statically Verified Refinements for Multiparty Protocols. arXiv:2009.06541 [cs], September 2020. arXiv: 2009.06541. URL: https://arxiv.org/abs/2009.06541.
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