Rusty Variation: Deadlock-free Sessions with Failure in Rust
Wen Kokke (University of Edinburgh)
TL;DR
Rusty Variation (RV) is a Rust library that ensures session-typed communication protocols are correctly implemented at compile time, guaranteeing deadlock and race freedom for reliable concurrent programs.
Contribution
This paper introduces RV, a novel Rust library that enforces protocol adherence and deadlock-freedom through compile-time checks in session-typed communication.
Findings
RV guarantees protocol correctness at compile time
Programs using RV are deadlock-free and race-free
RV simplifies writing reliable concurrent Rust applications
Abstract
Rusty Variation (RV) is a library for session-typed communication in Rust which offers strong compile-time correctness guarantees. Programs written using RV are guaranteed to respect a specified protocol, and are guaranteed to be free from deadlocks and races.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDistributed systems and fault tolerance · Formal Methods in Verification · Logic, programming, and type systems