Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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

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

scope and guarantees

The paper embeds affine multiparty session types (AMPST) in Rust through the MultiCrusty library. It targets communication safety when channels or processes fail, are cancelled, or panic. The abstract says AMPST “ensures cancellation termination of multiple, independently running components and guarantees that communication will not get stuck due to error or abrupt termination.” (Abstract, p. 1). The paper proves session fidelity (Theorem 3.18), deadlock-freedom (Theorem 3.20), liveness (Theorem 3.21), and cancellation termination (Theorem 3.27) for its π-calculus. The Rust library is described as “a shallow embedding of the theory into Rust” (Introduction, p. 2); the paper gives no mechanized proof of the library code itself. Inference: the paper does not address application-level data invariants, so those are outside what it establishes.

The design combines global protocols (top-down Scribble) or local binary session types checked for compatibility (bottom-up k-MC). The authors identify the practical problem: MPST assumes a session runs to completion, while Rust channels are affine and may be dropped. Their implementation claim is that “multiparty communication safety can be realised by the native Rust type system (without external validation tools).” (Introduction, p. 2). Deadlock-freedom is not covered by that claim: “This is insufficient to guarantee deadlock-freedom, which is why we utilise Scribble or bounded model checking, i.e., k-MC, as an additional verification step.” (Section 4.2, p. 18). The paper says “we assume fair scheduling as in the theory” (Section 4.3, p. 20); Remark 3.29 (p. 17) leaves total termination under fair scheduling as future work.

technique: affine meshed channels

An affine meshed channel is a typed struct with three ingredients: “(1) a list of separate binary channels (one binary channel for each pair of participants); (2) a stack that imposes the ordering between the binary channels; and (3) the name of the role” (Section 4.2, p. 18). In the 3-role example the struct has fields session1, session2, stack, name (Figure 5, p. 18). The stack, not the binary types, says which binary channel is used next. The macro gen_mpst!(MeshedChannelsThree, A, C, S) generates the struct and communication primitives at compile time (Section 2, pp. 4–5). A binary type such as Send<T, Recv<U, End>> states the current action and continuation (Section 4.3, p. 20). Each primitive rebinds s to a new meshed channel returned by the call (Section 2, p. 6); the generated send consumes self and consumes the head of the stack (Appendix B.2, Figure 14, p. 42).

How to use it:

  1. Specify a global Scribble protocol, or write local binary types for each role (Sections 2 and 4.3, pp. 4–5, 20–21).
  2. Invoke gen_mpst! with the role names to generate a meshed-channel data type and generic send/receive/choice operations (Section 2, p. 5).
  3. Declare each endpoint function with its session type, e.g. fn auth(s: RecA<i32>) -> R in Figure 2b (p. 4), and rebind s to the returned continuation at each communication step.
  4. Use choice macros (choose_c!, offer_mpst!) to transmit a branch label and continue with the branch-specific meshed type (Section 2, p. 6; Table 1, p. 7).
  5. Close with close() after the protocol’s End state; the paper says it “safely and cleanly closes all binary channels” and that “the only primitive implemented for such meshed channels is close()” (Section 2, p. 6).

Verus form (Inference): model each endpoint as a Rust struct carrying a ghost protocol-state token. Each operation consumes the old token and returns a token for the continuation; requires checks the current state and ensures establishes the next state and message effect. A ghost state machine can track channel ownership and role stacks. Verus can prove these contracts for a fixed API, but it will not derive global-protocol projection or duality automatically. The paper’s affine discipline relies on Rust’s type system (“using channel s twice (without rebinding) will be detected by the compiler”, Section 2, p. 6), which remains outside a Verus functional proof.

Evidence: Theorem 3.18 (p. 15) establishes session fidelity for the calculus; the library checks that pairs of binary types are dual statically (Section 4.3, p. 20). Inference: this is a type-safety result for the calculus plus a design argument for the library, not an empirical bug rate.

technique: explicit and implicit cancellation

The paper lists three reasons a session is cancelled: “(1) an error affecting the computation aspects of the program, as in Figure 2c; (2) an error during communication, e.g., a timeout on a channel, as in Figure 2b; or (3) a premature drop of the affine meshed channel due to incorrect implementation, as in Figure 2a.” (Section 2, p. 8). Communication primitives return a Result (e.g. recv() returns Result<(T, S), Box<dyn Error>>). The ? operator propagates an Err; attempt! { 
 } catch(e) { 
 } handles errors across several actions (Section 4.4, p. 21). Explicit cancel(s) “cancels all binary channels that are a part of the meshed channel” (Section 4.4, p. 22). Implicit cancellation happens when a communication fails and the library cancels the channel (Section 2, p. 7; Section 4.4, p. 22), or when the channel is dropped (Section 4.4, p. 22).

Apply it as follows:

  1. Use the ? operator on every communication primitive (Result-returning); on an Err, either call cancel(s) or let ? return it (Section 4.4, pp. 21–22, Figure 7).
  2. For a multi-action failure region, wrap actions in attempt! and handle the catch branch; the paper calls it “syntactic sugar” and says attempt! M catch N “reduces to its failing clause N if an error occurs in any of the statements in M” (Section 4.4, p. 21).
  3. The library customises Drop for the meshed channel: “We have customised this method by implementing the Drop trait, which explicitly calls cancel().” So an out-of-scope value is cancelled, including on panic! or a forgotten explicit cancel (Section 4.4, p. 22).
  4. On cancellation, all binary channels of the meshed channel are cancelled; a peer that then reads from them gets an error and closes its own channels (Section 4.4, item 4 “Cancel propagation”, p. 22).
  5. A second cancellation is ignored; the calculus models this by structural congruence on kill processes (s | s ≡ s) (Section 4.4, item 3, p. 22).

The authors summarize the safety boundary: “once a cancellation happens, all processes in the same session terminate with an error” (Section 2, p. 8, citing Theorem 3.27). The formal statement is weaker: Remark 3.29 (p. 17) says “there always exists a path which leads to 0; and an initial program might not terminate even if it contains a process with” a kill. Theorem 3.27 applies to “initial programs” (Definition 3.22, p. 16), which require each recursive definition to be of the form try Q0 catch P00 with no process call in the catch part. The paper says an incorrectly implemented role whose channel is dropped prematurely is also covered (Section 2, p. 7).

Verus form (Inference): use a Verus state machine whose state includes an active/cancelled flag and a set of channel endpoints. A transition lemma can prove cancellation is idempotent and that no send/recv transition is enabled after cancellation. Rust Drop itself is executable infrastructure; the proof must specify the library’s destructor behavior or wrap channels in a verified API. Panic unwinding, scheduler fairness, and crossbeam behavior are assumptions unless separately modeled.

technique: protocol compatibility and bounded model checking

Top-down use starts with Scribble, generates local types, and then implements endpoints. Bottom-up use writes local types and uses a MultiCrusty macro that “rewrites all Rust types to CFSMs and invokes the k-MC tool at compile time” (Section 4.3, p. 21). k-MC checks the progress property and the eventual reception property for executions where each channel holds at most k messages (Section 4.3, p. 21). The authors say “well-formed global protocols correspond to the class of 1-MC safe systems”, that they restricted k-MC to 1-MC systems “to stay close to the theory”, and that “the developer can specify the bound as an argument” (Section 4.3, p. 21). If types are generated from Scribble, “they are guaranteed to be compatible, hence no k-MC-check is required” (p. 21).

Steps:

  1. Generate or write all local binary types.
  2. The MultiCrusty library checks pairwise duality statically (“checks statically that all pairs of binary types are dual to each other”, Section 4.3, p. 20; Section 4.2, p. 18); a mismatch is a compile-time error.
  3. If using bottom-up types, the macro invokes k-MC at compile time on the CFSM translation; check its progress and eventual-reception verdict for the chosen bound (Section 4.3, p. 21).
  4. Implement role functions with the generated continuation types; the paper says protocol violations such as swapping two actions or using a wrong payload type are compile-time errors (Section 2, p. 6).

Verus form (Inference): encode each CFSM state and channel queue as ghost state, then prove transition preservation and a bounded progress lemma. k-MC can find counterexamples but is not an unbounded Verus proof; a product should report the bound and fairness assumptions explicitly.

evidence, measurements, and limits

The formal results are Theorems 3.18 (session fidelity, p. 15), 3.20 (deadlock-freedom, p. 16), 3.21 (liveness, p. 16), and 3.27 (cancellation termination, p. 17), proved for AMPST’s multiparty π-calculus (Section 3, pp. 15–17; proofs in Appendix A, pp. 34–37). Liveness requires the condition live+(Γ) on the typing context (Theorem 3.21). Performance experiments compare MultiCrusty MPST, AMPST with cancellation, binary channels (BC), and untyped crossbeam channels (Bare). Setup: AMD Opteron 6282 SE @ 1.30 GHz, 32 cores/64 threads, 128 GB RAM, Ubuntu 20.04, Rust cargo 1.56.0; each benchmark ran 10000 times, reporting the average with a 95% confidence interval (Section 5.1, p. 23). The authors state they “have not considered performance as a primary consideration in the current implementation” (Section 5, p. 23).

The summary claim is “MultiCrusty has only a negligible overhead when compared to the built-in unsafe Rust channels, provided by crossbeam-channel, and up to two-fold runtime improvement to binary sessions in protocols with high-degree of synchronisation.” (Section 5, p. 23). The paper’s own measurements are less favourable against Bare: “MPST is about 2.5 times slower than BC and about 6.5 times slower than Bare for 500 iterations” (ping-pong, p. 24); “MPST becomes almost 2 times slower than BC for 10 participants and almost 3.25 times slower for 20 participants” (ring, p. 24); “MPST is about 2.3 times faster than BC, and about 11 times slower than Bare for 10 participants” (full-mesh, p. 24), and about 12 times slower than Bare at 20 participants (p. 25). What is negligible is the cancellation cost: “AMPST adds a negligible running time due to the simple checking of the status of the binary channels.” (p. 25). Compilation: up to 40% increase for full-mesh and 11% for ring (p. 25). Inference: the “negligible overhead” claim applies to cancellation checks, not to the whole library versus raw crossbeam; the speed-up over BC is measured only on these three microbenchmarks.

Use cases include OAuth, SMTP, circuit breaker, and distributed logging (Section 5.2, Table 2, p. 26; Section C, pp. 44–46). Table 2 reports that “All protocols are type-checked within 27 seconds, while the basic compilations range between 36s and 41s and the optimised compilations vary between 80s and 97s.” (p. 26). Protocols with more than 5 participants are not considered (Section 5.2, p. 25). The macros are demonstrated for three hard-coded roles; the paper says generators for an arbitrary number of roles exist (Appendix D.2, p. 47).

Trusted or assumed (Inference, with paper support where noted): Rust’s compiler and destructor semantics, crossbeam channels (the transport, Appendix B.2, p. 41), generated macro expansion, fair scheduling (Section 4.3, p. 20), and the correctness of the Scribble/k-MC toolchain. The paper says “Our library uses only the safe fragment of Rust.” (Section 2, p. 8).

techniques for the catalog

  • affine meshed channels: store typed binary channels and consume endpoint values to enforce the next legal multiparty action
  • typed cancellation propagation: combine Result, ?, catch macros, explicit cancel, and Drop to propagate cancellation to every session participant
  • top-down/bottom-up protocol checking: generate local types from Scribble or check local CFSMs with k-MC compatibility and progress bounds
  • cancellation termination proof: model errors and drops in an affine π-calculus and prove that after a cancellation a reduction path to the terminated process exists (not that all paths terminate)

Last edited: