Document Open Access Logo

Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types

Authors Nicolas Lagaillardie , Rumyana Neykova , Nobuko Yoshida

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.4.pdf
  • Filesize: 1.81 MB
  • 29 pages

Document Identifiers

Author Details

Nicolas Lagaillardie
  • Department of Computing, Imperial College London, UK
Rumyana Neykova
  • Department of Computer Science, Brunel University London, UK
Nobuko Yoshida
  • Department of Computing, Imperial College London, UK

Funding

The work is supported by EPSRC EP/T006544/1, EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1, EP/T014709/1 and EP/V000462/1, and NCSS/EPSRC VeTSS.

Acknowledgements

We thank the ECOOP reviewers for their insightful comments and suggestions, and (alphabetical order) Zak Cutner, Wen Kokke, Roland Kuhn, Dimitris Mostrous and Martin Vassor for discussions.

Cite AsGet BibTex

Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECOOP.2022.4

Abstract

Communicating systems comprise diverse software components across networks. To ensure their robustness, modern programming languages such as Rust provide both strongly typed channels, whose usage is guaranteed to be affine (at most once), and cancellation operations over binary channels. For coordinating components to correctly communicate and synchronise with each other, we use the structuring mechanism from multiparty session types, extending it with affine communication channels and implicit/explicit cancellation mechanisms. This new typing discipline, affine multiparty session types (AMPST), ensures cancellation termination of multiple, independently running components and guarantees that communication will not get stuck due to error or abrupt termination. Guided by AMPST, we implemented an automated generation tool (MultiCrusty) of Rust APIs associated with cancellation termination algorithms, by which the Rust compiler auto-detects unsafe programs. Our evaluation shows that MultiCrusty provides an efficient mechanism for communication, synchronisation and propagation of the notifications of cancellation for arbitrary processes. We have implemented several usecases, including popular application protocols (OAuth, SMTP), and protocols with exception handling patterns (circuit breaker, distributed logging).

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software usability
  • Software and its engineering → Concurrent programming languages
  • Theory of computation → Process calculi
Keywords
  • Rust language
  • affine multiparty session types
  • failures
  • cancellation

Metrics

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

Related Versions

Supplementary Materials

References

  1. Davide Ancona, Viviana Bono, and Mario Bravetti. Behavioral Types in Programming Languages. Number 2-3 in Foundations and Trends in Programming Languages. Now Publishers Inc., Hanover, MA, USA, 2016. URL: https://doi.org/10.1561/2500000031.
  2. Stephanie Balzer and Frank Pfenning. Manifest Sharing with Session Types. Proc. ACM Program. Lang., 1(ICFP), August 2017. URL: https://doi.org/10.1145/3110281.
  3. Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. Manifest Deadlock-Freedom for Shared Session Types. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 611-639, Cham, 2019. Springer. URL: https://doi.org/10.1007/978-3-030-17184-1_22.
  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. Luís Caires and Frank Pfenning. Session Types as Intuitionistic Linear Propositions. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, pages 222-236, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-15375-4_16.
  6. 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.
  7. Ruofei Chen and Stephanie Balzer. Ferrite: A Judgmental Embedding of Session Types in Rust. CoRR, abs/2009.13619, 2020. URL: http://arxiv.org/abs/2009.13619.
  8. Tokio Contributors. Crate: Tokio, 2021. Last accessed: July 2021. URL: https://crates.io/crates/tokio.
  9. Wikipedia Contributors. Wikipedia: Flow (psychology), 2021. Last accessed: July 2021. URL: https://en.wikipedia.org/wiki/Flow_(psychology).
  10. 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.
  11. 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.
  12. Romain Demangeon, Kohei Honda, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. FMSD, 46(3):197-225, 2015. URL: https://doi.org/10.1007/s10703-014-0218-8.
  13. Rust Developers. Rust: attempt-catch macro, 2018. Last accessed: July 2021. URL: https://play.integer32.com/?version=stable&mode=debug&edition=2018&gist=95979b17196adbc203c4f563e00d384b.
  14. José Duarte and António Ravara. Retrofitting Typestates into Rust, pages 83-91. Association for Computing Machinery, New York, NY, USA, 2021. URL: https://doi.org/10.1145/3475061.3475082.
  15. 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.
  16. 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.
  17. Simon Gay and António Ravara. Behavioural Types: from Theory to Tools. In Behavioural Types: from Theory to Tools, Automation, Control and Robotics, pages 1-412. Rivers publishers, Alsbjergvej 10, 9260 Gistrup, Denmark, 2017. URL: https://doi.org/10.13052/rp-9788793519817.
  18. Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida. Precise Subtyping for Asynchronous Multiparty Sessions. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434297.
  19. 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.12.
  20. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems, ESOP '98, pages 122-138, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0053567.
  21. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Types. SIGPLAN Not., 43(1):273-284, January 2008. URL: https://doi.org/10.1145/1328897.1328472.
  22. 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.
  23. Raymond Hu and Nobuko Yoshida. Explicit Connection Actions in Multiparty Session Types. In Marieke Huisman and Julia Rubin, editors, Fundamental Approaches to Software Engineering, volume 10202, pages 116-133. Springer Berlin Heidelberg, Berlin, Heidelberg, 2017. Series Title: Lecture Notes in Computer Science. URL: https://doi.org/10.1007/978-3-662-54494-57.
  24. 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.
  25. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a Minimal Core Calculus for Java and GJ. ACM Trans. Program. Lang. Syst., 23(3):396-450, May 2001. URL: https://doi.org/10.1145/503502.503505.
  26. Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty Session Programming With Global Protocol Combinators. In Robert Hirschfeld and Tobias Pape, editors, 34th European Conference on Object-Oriented Programming (ECOOP 2020), volume 166 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:30, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2020.9.
  27. 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.
  28. 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.
  29. Aparicio Jorge. Crate: Criterion, 2021. Last accessed: July 2021. URL: https://crates.io/crates/criterion.
  30. 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.
  31. 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.
  32. Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. Typechecking protocols with Mungo and stmungo: A session type toolchain for Java. Science of Computer Programming, 155:52-75, April 2018. Selected and Extended papers from the International Symposium on Principles and Practice of Declarative Programming 2016. URL: https://doi.org/10.1016/j.scico.2017.10.006.
  33. Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay safe under panic: Affine rust programming with multiparty session types, 2022. URL: https://doi.org/10.48550/ARXIV.2204.13464.
  34. Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From Communicating Machines to Graphical Choreographies. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 221-232, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2676726.2676964.
  35. 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.
  36. Sam Lindley and J. Garrett Morris. A Semantics for Propositions as Sessions. In Jan Vitek, editor, Programming Languages and Systems, pages 560-584, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-46669-8_23.
  37. Sam Lindley and J. Garrett Morris. Talking Bananas: Structural Recursion for Session Types. SIGPLAN Not., 51(9):434-447, September 2016. URL: https://doi.org/10.1145/3022670.2951921.
  38. Anson Miu, Francisco Ferreira, Nobuko Yoshida, and Fangyi Zhou. Generating Interactive WebSocket Applications in TypeScript. Electronic Proceedings in Theoretical Computer Science, 314:12-22, April 2020. URL: https://doi.org/10.4204/EPTCS.314.2.
  39. 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.
  40. 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, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3178372.3179495.
  41. Rumyana Neykova and Nobuko Yoshida. Let It Recover: Multiparty Protocol-Induced Recovery. In Proceedings of the 26th International Conference on Compiler Construction, CC 2017, pages 98-108, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3033019.3033031.
  42. 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.
  43. Nicholas Ng, Jose Gabriel de Figueiredo Coutinho, and Nobuko Yoshida. Protocols by Default. In Björn Franke, editor, Compiler Construction, pages 212-232, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-46663-6_11.
  44. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In Peter Müller, editor, 31st European Conference on Object-Oriented Programming (ECOOP 2017), volume 74 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:31, Dagstuhl, Germany, 2017. Schloss DagstuhlendashLeibnizZentrum fuer Informatik. ISSN: 1868-8969. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2017.24.
  45. Alceste Scalas and Nobuko Yoshida. Lightweight Session Programming in Scala. In Shriram Krishnamurthi and Benjamin S. Lerner, editors, 30th European Conference on Object-Oriented Programming (ECOOP 2016), volume 56 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:28, Dagstuhl, Germany, 2016. Schloss DagstuhlendashLeibnizZentrum fuer Informatik. ISSN: 1868-8969. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2016.21.
  46. Alceste Scalas and Nobuko Yoshida. Less is More: Multiparty Session Types Revisited. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290343.
  47. Authors Scribble. Scribble home page, 2021. URL: http://www.scribble.org.
  48. McArthur Sean. Crate: Hyper, 2021. Last accessed: July 2021. URL: https://crates.io/crates/hyper.
  49. Company StackOverflow. Stackoverflow: 2020 Developer Survey, 2020. Last accessed: July 2021. URL: https://insights.stackoverflow.com/survey/2020.
  50. Tengfei Tu, Xiaoyu Liu, Linhai Song, and Yiying Zhang. Understanding Real-World Concurrency Bugs in Go. In Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '19, pages 865-878, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3297858.3304069.
  51. Vasco T. Vasconcelos, Simon J. Gay, and António Ravara. Type checking a multithreaded functional language with session types. Theoretical Computer Science, 368(1):64-87, 2006. URL: https://doi.org/10.1016/j.tcs.2006.06.028.
  52. 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.
  53. 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. URL: https://doi.org/10.1007/978-3-319-05119-2_3.
  54. 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.
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