Document Open Access Logo

Fearless Asynchronous Communications with Timed Multiparty Session Protocols

Authors Ping Hou , Nicolas Lagaillardie , Nobuko Yoshida

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.19.pdf
  • Filesize: 1.58 MB
  • 30 pages

Document Identifiers

Author Details

Ping Hou
  • University of Oxford, UK
Nicolas Lagaillardie
  • Imperial College London, UK
Nobuko Yoshida
  • University of Oxford, UK

Funding

Work 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 thank the anonymous reviewers for their useful comments and suggestions.

Cite As Get BibTex

Ping Hou, Nicolas Lagaillardie, and Nobuko Yoshida. Fearless Asynchronous Communications with Timed Multiparty Session Protocols. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 19:1-19:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ECOOP.2024.19

Abstract

Session types using affinity and exception handling mechanisms have been developed to ensure the communication safety of protocols implemented in concurrent and distributed programming languages. Nevertheless, current affine session types are inadequate for specifying real-world asynchronous protocols, as they are usually imposed by time constraints which enable timeout exceptions to prevent indefinite blocking while awaiting valid messages. This paper proposes the first formal integration of affinity, time constraints, timeouts, and time-failure handling based on multiparty session types for supporting reliability in asynchronous distributed systems. With this theory, we statically guarantee that asynchronous timed communication is deadlock-free, communication safe, while being fearless - never hindered by timeout errors or abrupt terminations. 
To implement our theory, we introduce MultiCrusty^T, a Rust toolchain designed to facilitate the implementation of safe affine timed protocols. MultiCrusty^T leverages generic types and the time library to handle timed communications, integrated with optional types for affinity. We evaluate MultiCrusty^T by extending diverse examples from the literature to incorporate time and timeouts. We also showcase the correctness by construction of our approach by implementing various real-world use cases, including protocols from the Internet of Remote Things domain and real-time systems.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software usability
  • Software and its engineering → Concurrent programming languages
  • Theory of computation → Process calculi
Keywords
  • Session Types
  • Concurrency
  • Time Failure Handling
  • Affinity
  • Timeout
  • Rust

Metrics

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

Related Versions

Supplementary Materials

References

  1. Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  2. Android. Motion Sensors, 2009. URL: https://developer.android.com/guide/topics/sensors/sensors_motion.
  3. Laura Bocchi, Maurizio Murgia, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. Asynchronous timed session types. In Luís Caires, editor, Programming Languages and Systems, pages 583-610, Cham, 2019. Springer International Publishing. Google Scholar
  4. Laura Bocchi, Weizhen Yang, and Nobuko Yoshida. Timed multiparty session types. In Paolo Baldan and Daniele Gorla, editors, CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, volume 8704 of Lecture Notes in Computer Science, pages 419-434. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44584-6_29.
  5. David Castro, Raymond Hu, SungShik Jongmans, Nicholas Ng, and Nobuko Yoshida. Distributed Programming Using Role-Parametric Session Types in Go: Statically-Typed Endpoint APIs for Dynamically-Instantiated Communication Structures. Proc. ACM Program. Lang., 3(POPL), January 2019. Place: New York, NY, USA Publisher: Association for Computing Machinery. URL: https://doi.org/10.1145/3290342.
  6. Ruo Fei Chen, Stephanie Balzer, and Bernardo Toninho. Ferrite: A Judgmental Embedding of Session Types in Rust. 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 22:1-22:28, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2022.22.
  7. Yingying Chen, Minghu Zhang, Xin Li, Tao Che, Rui Jin, Jianwen Guo, Wei Yang, Baosheng An, and Xiaowei Nie. Satellite-enabled internet of remote things network transmits field data from the most remote areas of the tibetan plateau. Sensors, 22(10):3713, 2022. URL: https://doi.org/10.3390/S22103713.
  8. Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global progress for dynamically interleaved multiparty sessions. Mathematical Structures in Computer Science, 26(2):238-302, 2016. URL: https://doi.org/10.1017/S0960129514000188.
  9. The Developers of Crossbeam. Crate: Crossbeam channel, 2022. Last accessed: October 2022. URL: https://crates.io/crates/crossbeam-channel.
  10. Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-Free Asynchronous Message Reordering in Rust with Multiparty Session Types. In 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, volume abs/2112.12693 of PPoPP '22, pages 261-246. ACM, 2022. URL: https://doi.org/10.1145/3503221.3508404.
  11. 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.
  12. José Duarte and António Ravara. Taming stateful computations in rust with typestates. Journal of Computer Languages, 72:101154, 2022. URL: https://doi.org/10.1016/j.cola.2022.101154.
  13. Roy Fielding and Julian Reschke. Hypertext Transfer Protocol (HTTP/1.1): Message Syntax and Routing. Technical Report RFC7230, RFC Editor, June 2014. URL: https://doi.org/10.17487/rfc7230.
  14. Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. Exceptional Asynchronous Session Types: Session Types Without Tiers. Proc. ACM Program. Lang., 3(POPL):28:1-28:29, January 2019. Place: New York, NY, USA Publisher: ACM. URL: https://doi.org/10.1145/3290341.
  15. Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay. Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming (ECOOP 2021), volume 194 of Leibniz International Proceedings in Informatics (LIPIcs), page 30, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2021.10.
  16. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFB0053567.
  17. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 273-284. ACM, 2008. Full version in [Honda et al., 2016]. URL: https://doi.org/10.1145/1328438.1328472.
  18. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Types. J. ACM, 63(1), 2016. URL: https://doi.org/10.1145/2827695.
  19. Ping Hou, Nicolas Lagaillardie, and Nobuko Yoshida. Fearless asynchronous communications with timed multiparty session protocols, 2024. URL: https://arxiv.org/abs/2406.19541.
  20. Raymond Hu and Nobuko Yoshida. Hybrid Session Verification Through Endpoint API Generation. In Perdita Stevens and Andrzej Wasowski, editors, Fundamental Approaches to Software Engineering, volume 9633, pages 401-418. Springer Berlin Heidelberg, Berlin, Heidelberg, 2016. URL: https://doi.org/10.1007/978-3-662-49665-724.
  21. Raymond Hu, Nobuko Yoshida, and Kohei Honda. Session-Based Distributed Programming in Java. In Jan Vitek, editor, ECOOP'08, volume 5142 of LNCS, pages 516-541, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-70592-5_22.
  22. Grant Iraci, Cheng-En Chuang, Raymond Hu, and Lukasz Ziarek. Validating iot devices with rate-based session types. Proc. ACM Program. Lang., 7(OOPSLA2):1589-1617, 2023. URL: https://doi.org/10.1145/3622854.
  23. 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, WGP 2015, pages 13-22, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2808098.2808100.
  24. Limin Jia, Hannah Gommerstadt, and Frank Pfenning. Monitors and Blame Assignment for Higher-Order Session Types. SIGPLAN Not., 51(1):582-594, January 2016. URL: https://doi.org/10.1145/2914770.2837662.
  25. Wen Kokke. Rusty Variation: Deadlock-free Sessions with Failure in Rust. Electronic Proceedings in Theoretical Computer Science, 304:48-60, September 2019. URL: https://doi.org/10.4204/eptcs.304.4.
  26. Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. Typechecking Protocols with Mungo and stmungo. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP '16, pages 146-159, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2967973.2968595.
  27. Pavel Krcál and Wang Yi. Communicating timed automata: The more synchronous, the more difficult to verify. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 249-262. Springer, 2006. URL: https://doi.org/10.1007/11817963_24.
  28. 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. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2022.4.
  29. Julien Lange and Nobuko Yoshida. Verifying Asynchronous Interactions via Communicating Session Automata. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, volume 11561 of Lecture Notes in Computer Science, pages 97-117, Cham, 2019. Springer. URL: https://doi.org/10.1007/978-3-030-25540-4_6.
  30. Matthew Alan Le Brun and Ornela Dardha. MAGπ: Types for Failure-Prone Communication. In Thomas Wies, editor, Programming Languages and Systems, pages 363-391, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-30044-8_14.
  31. Dimitris Mostrous and Vasco T. Vasconcelos. Affine Sessions. Logical Methods in Computer Science ; Volume 14, 8459:Issue 4 ; 18605974, 2018. Medium: PDF Publisher: Episciences.org. URL: https://doi.org/10.23638/LMCS-14(4:14)2018.
  32. Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. Timed runtime monitoring for multiparty conversations. Formal Aspects of Computing, 29(5):877-910, 2017. Google Scholar
  33. Rumyana Neykova, Nobuko Yoshida, and Raymond Hu. Spy: Local Verification of Global Protocols. In Axel Legay and Saddek Bensalem, editors, Runtime Verification, volume 8174 of LNCS, pages 358-363, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-40787-1_25.
  34. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  35. Pine64. PineTime, 2019. URL: https://www.pine64.org/pinetime/.
  36. Jonathan Postel. Rfc0821: Simple mail transfer protocol, 1982. Google Scholar
  37. Alceste Scalas and Nobuko Yoshida. Less is more: multiparty session types revisited. Proc. ACM Program. Lang., 3(POPL):30:1-30:29, 2019. URL: https://doi.org/10.1145/3290343.
  38. Servo. Servo Web Browser commit, 2015. URL: https://github.com/servo/servo/commit/434a5f1d8b7fa3e2abd36d832f16381337885e3d.
  39. Developers Rust of the library Time. Module std::time documentation, 2023. URL: https://doc.rust-lang.org/std/time/index.html.
  40. Malte Viering, Raymond Hu, Patrick Eugster, and Lukasz Ziarek. A multiparty session typing discipline for fault-tolerant event-driven distributed programming. Proceedings of the ACM on Programming Languages, 5(OOPSLA):1-30, October 2021. URL: https://doi.org/10.1145/3485501.
  41. Lennert Wouters, Eduard Marin, Tomer Ashur, Benedikt Gierlichs, and Bart Preneel. Fast, furious and insecure: Passive keyless entry and start systems in modern supercars. IACR Transactions on Cryptographic Hardware and Embedded Systems, 2019(3):66-85, 2019. URL: https://doi.org/10.13154/TCHES.V2019.I3.66-85.
  42. Nobuko Yoshida, Fangyi Zhou, and Francisco Ferreira. Communicating finite state machines and an extensible toolchain for multiparty session types. In Evripidis Bampis and Aris Pagourtzis, editors, Fundamentals of Computation Theory, pages 18-35, Cham, 2021. Springer International Publishing. Google Scholar
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