Document Open Access Logo

Ferrite: A Judgmental Embedding of Session Types in Rust

Authors Ruo Fei Chen , Stephanie Balzer, Bernardo Toninho

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.22.pdf
  • Filesize: 1.05 MB
  • 28 pages

Document Identifiers

Author Details

Ruo Fei Chen
  • Independent Researcher, Leipzig, Germany
Stephanie Balzer
  • Carnegie Mellon University, Pittsburgh, PA, USA
Bernardo Toninho
  • NOVA LINCS, Nova University Lisbon, Portugal

Funding

  • Balzer, Stephanie: National Science Foundation Award No. CCF-1718267.
  • Toninho, Bernardo: FCT/MCTES grant NOVALINCS/BASE UIDB/04516/2020.

Cite As Get BibTex

Ruo Fei Chen, Stephanie Balzer, and Bernardo Toninho. Ferrite: A Judgmental Embedding of Session Types in Rust. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 22:1-22:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ECOOP.2022.22

Abstract

Session types have proved viable in expressing and verifying the protocols of message-passing systems. While message passing is a dominant concurrency paradigm in practice, real world software is written without session types. A limitation of existing session type libraries in mainstream languages is their restriction to linear session types, precluding application scenarios that demand sharing and thus aliasing of channel references. This paper introduces Ferrite, a shallow embedding of session types in Rust that supports both linear and shared sessions. The formal foundation of Ferrite constitutes the shared session type calculus SILL_𝖲, which Ferrite encodes via a novel judgmental embedding technique. The fulcrum of the embedding is the notion of a typing judgment that allows reasoning about shared and linear resources to type a session. Typing rules are then encoded as functions over judgments, with a valid typing derivation manifesting as a well-typed Rust program. This Rust program generated by Ferrite serves as a certificate, ensuring that the application will proceed according to the protocol defined by the session type. The paper details the features and implementation of Ferrite and includes a case study on implementing Servo’s canvas component in Ferrite.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Type theory
  • Software and its engineering → Domain specific languages
  • Software and its engineering → Concurrent programming languages
Keywords
  • Session Types
  • Rust
  • DSL

Metrics

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

Related Versions

Supplementary Materials

References

  1. Stephanie Balzer and Frank Pfenning. Manifest sharing with session types. Proceedings of the ACM on Programming Languages (PACMPL), 1(ICFP):37:1-37:29, 2017. Google Scholar
  2. Stephanie Balzer, Frank Pfenning, and Bernardo Toninho. A universal session type for untyped asynchronous communication. In 29th International Conference on Concurrency Theory (CONCUR), LIPIcs, pages 30:1-30:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  3. Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. Manifest deadlock-freedom for shared session types. In 28th European Symposium on Programming (ESOP), volume 11423 of Lecture Notes in Computer Science, pages 611-639. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_22.
  4. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In 21st International Conference on Concurrency Theory (CONCUR), pages 222-236. Springer, 2010. Google Scholar
  5. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Mathematical Structures in Computer Science, 26(3):367-423, 2016. Google Scholar
  6. Ruo Fei Chen, Stephanie Balzer, and Bernardo Toninho. Ferrite project website. URL: https://github.com/ferrite-rs/ferrite.
  7. Ruofei Chen, Stephanie Balzer, and Bernardo Toninho. Ferrite: A judgmental embedding of session types in rust. CoRR, abs/2009.13619, 2022. URL: http://arxiv.org/abs/2009.13619.
  8. 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.
  9. Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-free asynchronous message reordering in rust with multiparty session types. CoRR, abs/2112.12693, 2021. URL: http://arxiv.org/abs/2112.12693.
  10. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. In Principles and Practice of Declarative Programming (PPDP), pages 139-150, 2012. Google Scholar
  11. J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Trans. Program. Lang. Syst., 29(3):17, 2007. URL: https://doi.org/10.1145/1232420.1232424.
  12. Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. Exceptional asynchronous session types: Session types without tiers. Proceedings of the ACM on Programming Languages, 3(POPL):28:1-28:29, 2019. URL: https://doi.org/10.1145/3290341.
  13. Andrew Gerrand. The go blog: Share memory by communicating, 2010. URL: https://blog.golang.org/share-memory-by-communicating.
  14. Kohei Honda. Types for dyadic interaction. In 4th International Conference on Concurrency Theory (CONCUR), pages 509-523. Springer, 1993. Google Scholar
  15. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In 7th European Symposium on Programming (ESOP), pages 122-138. Springer, 1998. Google Scholar
  16. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328472.
  17. Raymond Hu, Dimitrios Kouzapas, Olivier Pernet, Nobuko Yoshida, and Kohei Honda. Type-safe eventful sessions in Java. In 24th European Conference on Object-Oriented Programming (ECOOP), volume 6183 of Lecture Notes in Computer Science, pages 329-353. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14107-2_16.
  18. Raymond Hu, Nobuko Yoshida, and Kohei Honda. Session-based distributed programming in Java. In 22nd European Conference on Object-Oriented Programming (ECOOP), volume 5142 of Lecture Notes in Computer Science, pages 516-541. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70592-5_22.
  19. Keigo Imai, Nobuko Yoshida, and Shoji Yuen. Session-ocaml: a session-based library with polarities and lenses. Science of Computer Programming, 172:135-159, 2019. URL: https://doi.org/10.1016/j.scico.2018.08.005.
  20. Keigo Imai, Shoji Yuen, and Kiyoshi Agusa. Session type inference in haskell. In 3rd Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES) 2010, Paphos, Cyprus, 21st March 201, volume 69 of EPTCS, pages 74-91, 2010. URL: https://doi.org/10.4204/EPTCS.69.6.
  21. Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. Session types for Rust. In 11th ACM SIGPLAN Workshop on Generic Programming (WGP), 2015. URL: https://doi.org/10.1145/2808098.2808100.
  22. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. RustBelt: Securing the foundations of the Rust programming language. Proceedings of the ACM on Programming Languages, 2(POPL):66:1-66:34, 2018. URL: https://doi.org/10.1145/3158154.
  23. Oleg Kiselyov, Ralf Lämmel, and Keean Schupke. Strongly typed heterogeneous collections. In Henrik Nilsson, editor, Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2004, Snowbird, UT, USA, September 22-22, 2004, pages 96-107. ACM, 2004. URL: https://doi.org/10.1145/1017472.1017488.
  24. Naoki Kobayashi. Type systems for concurrent programs. In Bernhard K. Aichernig and T. S. E. Maibaum, editors, Formal Methods at the Crossroads. From Panacea to Foundational Support, 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18-20, 2002, Revised Papers, volume 2757 of Lecture Notes in Computer Science, pages 439-453. Springer, 2002. URL: https://doi.org/10.1007/978-3-540-40007-3_26.
  25. Wen Kokke. Rusty variation: Deadlock-free sessions with failure in rust. In 12th Interaction and Concurrency Experience, ICE 2019, pages 48-60, 2019. Google Scholar
  26. Sam Lindley and J. Garrett Morris. A semantics for propositions as sessions. In 24th European Symposium on Programming (ESOP), volume 9032 of Lecture Notes in Computer Science, pages 560-584, 2015. URL: https://doi.org/10.1007/978-3-662-46669-8_23.
  27. Sam Lindley and J. Garrett Morris. Embedding session types in Haskell. In 9th International Symposium on Haskell, pages 133-145. ACM, 2016. URL: https://doi.org/10.1145/2976002.2976018.
  28. J. Garrett Morris. Variations on variants. In Ben Lippmeier, editor, Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015, pages 71-81. ACM, 2015. URL: https://doi.org/10.1145/2804302.2804320.
  29. Mozilla. Servo, the Parallel Browser Engine Project. https://servo.org/, 2012.
  30. Mozilla. Servo source code - canvas paint thread, 2021. URL: https://github.com/servo/servo/blob/d13a9355b8e66323e666dde7e82ced7762827d93/components/canvas/canvas_paint_thread.rs.
  31. Dominic A. Orchard and Nobuko Yoshida. Effects as sessions, sessions as effects. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 568-581. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837634.
  32. Luca Padovani. A simple library implementation of binary sessions. J. Funct. Program., 27:e4, 2017. URL: https://doi.org/10.1017/S0956796816000289.
  33. Matthew Pickering, Jeremy Gibbons, and Nicolas Wu. Profunctor optics: Modular data accessors. Programming Journal, 1(2):7, 2017. URL: https://doi.org/10.22152/programming-journal.org/2017/1/7.
  34. Riccardo Pucella and Jesse A. Tov. Haskell session types with (almost) no class. In 1st ACM SIGPLAN Symposium on Haskell, pages 25-36. ACM, 2008. URL: https://doi.org/10.1145/1411286.1411290.
  35. Zesen Qian, G. A. Kavvos, and Lars Birkedal. Client-server sessions in linear logic. CoRR, abs/2010.13926, 2020. URL: http://arxiv.org/abs/2010.13926.
  36. John C. Reynolds. Definitional interpreters for higher-order programming languages. In ACM Annual Conference, volume 2, pages 717-740. ACM, 1972. URL: https://doi.org/10.1145/800194.805852.
  37. Pedro Rocha and Luís Caires. Propositions-as-types and shared state. Proc. ACM Program. Lang., 5(ICFP):1-30, 2021. Google Scholar
  38. Matthew Sackman and Susan Eisenbach. Session types in haskell: Updating message passing for the 21st century. Technical report, Imperial College, 2008. URL: http://hdl.handle.net/10044/1/5918.
  39. Alceste Scalas and Nobuko Yoshida. Lightweight session programming in Scala. In 30th European Conference on Object-Oriented Programming (ECOOP), volume 56 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:28. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  40. Josef Svenningsson and Emil Axelsson. Combining deep and shallow embedding for EDSL. In Hans-Wolfgang Loidl and Ricardo Peña, editors, Trends in Functional Programming - 13th International Symposium, TFP 2012, St. Andrews, UK, June 12-14, 2012, Revised Selected Papers, volume 7829 of Lecture Notes in Computer Science, pages 21-36. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-40447-4_2.
  41. Tokio. Tokio Homepage. https://tokio.rs/, 2021.
  42. Bernardo Toninho. A Logical Foundation for Session-based Concurrent Computation. PhD thesis, Carnegie Mellon University and New University of Lisbon, 2015. Google Scholar
  43. Bernardo Toninho, Luís Caires, and Frank Pfenning. Higher-order processes, functions, and sessions: a monadic integration. In 22nd European Symposium on Programming (ESOP), pages 350-369. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_20.
  44. Philip Wadler. Propositions as sessions. In 17th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 273-286. ACM, 2012. Google Scholar
  45. WebKit. MotionMark Homepage. https://browserbench.org/MotionMark/, 2021.
  46. Jeremy Yallop and Leo White. Lightweight higher-kinded polymorphism. In Functional and Logic Programming - 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings, pages 119-135, 2014. URL: https://doi.org/10.1007/978-3-319-07151-0_8.
  47. Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, and Derek Dreyer. Ghostcell: separating permissions from data in rust. Proc. ACM Program. Lang., 5(ICFP):1-30, 2021. URL: https://doi.org/10.1145/3473597.
  48. 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 - 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers, volume 8358 of Lecture Notes in Computer Science, pages 22-41. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-05119-2_3.
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