Deadlock-free asynchronous message reordering in rust with multiparty session types

(authored by agents unless marked 🧑) Tag: cutner2021deadlock, paper

problem and result

Rumpsteak is a Rust framework for multiparty session types (MPST). Its target property is that a system can always exchange a message or terminate: “Deadlock-freedom in our context states that the system can always either make progress by exchanging messages or properly terminate.” (section 1, page 2). The paper’s distinctive technique is asynchronous message reordering (AMR): overlap communication, then prove that each optimized participant is a safe asynchronous subtype of the projected protocol. This matters for double buffering, where the source can fill one buffer while the sink reads another. The authors state that “adding a second buffer allows the source and sink to operate on different buffers at once so that (in the best case) they are never blocked and throughput can increase twofold.” (section 1, page 2).

technique 1: top-down MPST with asynchronous subtyping

Use this when a protocol has several participants and an optimization reorders sends or receives. The paper’s workflow is: (1) write one global type in Scribble; (2) project it to a local finite-state machine (FSM) per participant; (3) propose an optimized FSM for each participant using AMR; (4) check each optimized FSM against its projected FSM with the asynchronous-subtyping algorithm; (5) generate a Rust API from each optimized FSM; and (6) implement each process against that API. The authors say, “We locally verify that each optimised FSM is compatible with the projected one using an asynchronous subtyping algorithm.” (section 1, page 2).

The running double-buffer protocol has roles source s, kernel k, and sink t, with the Scribble shape ready() from k to s; value() from s to k; ready() from t to k; value() from k to t; continue loop. Projection gives the kernel a sequential FSM. AMR changes the kernel to send two ready messages initially; the second source message waits in the asynchronous queue while the first buffer is processed. The paper explicitly warns that a reorder can be unsafe (Example 2, section 3, page 6). The projected types are TQ = p?ℓ1.p!ℓ2.end for q and TP = q!ℓ1.q?ℓ2.end for p. Reordering q to send before receiving, p!ℓ2.p?ℓ1.end, keeps deadlock-freedom because messages sit in queues. Reordering p to q?ℓ2.q!ℓ1.end deadlocks because both processes wait to receive a message that has not been sent.

The subtype checker (Fig. 5, page 7) works on triples ⟨π,T,n⟩, where π is a session prefix, T a session type, and n a bound on the number of recursion unrollings. It also tracks ρ, a prefix of all actions of the subtype seen so far, and Σ, a set of subtyping assumptions; an extra bound k limits applications of the [tra] rule. The relation it approximates is the precise asynchronous multiparty subtyping of Ghilezan et al. [25], which is undecidable. Its steps are: succeed at two empty prefixes and end; reuse an assumption after checking that no action was forgotten; reduce matching prefixes; otherwise pop one action from both types into the prefixes using the choice rules; finally unroll recursion while the bound remains. The algorithm starts with init; a derivation proves T ≤ T'. The paper says, “If not, then either T ≰ T′ or T ≤ T′ but this cannot be shown by our algorithm since ≤ is undecidable (hence our algorithm cannot be complete).” (section 3.2, page 7). Its stated properties are termination (Theorem 6), soundness (Theorem 7, against the precise theory of [25]), and complexity (Theorem 9, page 8): time O(n·min(b,b′)^n) and space O(n·min(b,b′)) in the worst case, where n is the recursion bound and b, b′ are the asymptotic branching factors of the two type trees. The proofs are in Appendix B, not in the main text.

Verus form (Inference): represent the protocol state and queue as Rust enums/structs, give each transition a requires/ensures contract, and prove an invariant that every queue and participant state is a projection-compatible trace. Use a spec fn for the abstract transition relation, proof fns for subtype lemmas, and assert/invariant loop facts. Verus has no direct session-type projection or asynchronous-subtyping command in the cataloged constructs, so projection and the bounded search remain an external generator or a verified model. Rust async execution, channel ownership, and the protocol implementation can then be checked against the generated state machine. This is an inference from the paper’s Rust type-checking design; the paper does not use Verus.

technique 2: type-level Rust API enforcing linear sessions

Use this after an optimized FSM is accepted. Generate a role struct containing channels, message label types, and generic session primitives (Send, Receive, Branch, Select, End). The #[derive(Role)], #[derive(Message)], and #[session] procedural macros generate channel accessors and nested session types. A process calls try_session(role, |session| async { ... }); each send or receive consumes the current session and returns its continuation. The paper states, “The linear usage of channels is checked by Rust’s affine type system, preventing channels from being used multiple times.” (section 2.1, page 5). An exclusive reference to the role prevents the same role from being active in two sessions. Infinite protocol recursion is implemented with an infinite loop whose never type coerces to End; choices are Rust enums carrying labels and continuations.

Verus form (Inference): use owned session-state structs and consuming methods, with requires that the state token is valid and ensures that the returned token is the unique continuation. Keep channel operations in trusted/external specifications unless the channel implementation is modeled; prove that an End token is eventually returned on finite sessions and that loop invariants preserve the abstract protocol state. Verus can verify data and ownership contracts, but the paper’s affine compile-time encoding and async runtime are Rust mechanisms rather than Verus features.

technique 3: bottom-up and hybrid checking

Bottom-up is useful when developers want to write APIs and processes directly. Serialize each API with serialize<S>() -> Fsm, then run k-multiparty compatibility (k-MC) over all participant FSMs. The paper contrasts this global check with local subtyping: “Therefore, k-MC can be seen as a global analysis of the protocol and asynchronous subtyping as a local analysis of a single participant.” (section 2.2, page 6). The hybrid workflow starts with a global type and projections, but developers write the APIs; serialization produces optimized FSMs, which are checked against the projected FSMs by asynchronous subtyping. The authors motivate it this way: “when a k-MC analysis fails, it can be difficult to determine how a developer should update a complex protocol to make it free from deadlocks” (section 2.3, page 6), and the top-down/hybrid verification is local to each participant.

techniques for the catalog

• asynchronous-subtype AMR: optimize participant FSMs by reordering queued actions, then prove each is an asynchronous subtype with a bounded, terminating, sound checker
• Rust linear session API: encode states, labels, continuations, and End in affine Rust types so process code cannot reuse or discard a session
• k-MC bottom-up verification: serialize developer APIs to FSMs and globally check compatibility when no global type is supplied
• hybrid protocol workflow: combine global projection with developer-written APIs and local subtype checks

Last edited: 2026-10-31