Refinements for Multiparty Message-Passing Protocols: Specification-agnostic theory and implementation
Multiparty message-passing protocols are notoriously difficult to design, due to interaction mismatches that lead to errors such as deadlocks. Existing protocol specification formats have been developed to prevent such errors (e.g. multiparty session types). In order to further constrain protocols, specifications can be extended with refinements, i.e. logical predicates to control the behaviour of the protocol based on the value of previous values exchanged. Unfortunately, existing refinement theories and implementations are tightly coupled with specific specification formats.
This paper proposes a framework for multiparty message-passing protocols with refinements and its implementation in Rust. Our work decouples correctness of refinements from the underlying model of computation, which results in a specification-agnostic framework.
Our contributions are threefold. First, we introduce a trace system which characterises valid refined traces, i.e. a sequence of sending and receiving actions correct with respect to refinements. Second, we give a correct model of computation refined communicating system (RCS), which is an extension of communicating automata system with refinements. We prove that RCS only produce valid refined traces. We show how to generate RCS from mainstream protocol specification formats, such as refined multiparty session types (RMPST) or refined choreography automata. Third, we illustrate the flexibility of the framework by developing both a static analysis technique and an improved model of computation for dynamic refinement evaluation. Finally, we provide a Rust toolchain for decentralised RMPST, evaluate our implementation with a set of benchmarks from the literature, and observe that refinement overhead is negligible.
Tue 17 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:30 - 17:00 | |||
15:30 15mTalk | InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference Technical Papers Senxi Li The University of Tokyo, Tetsuro Yamazaki University of Tokyo, Shigeru Chiba University of Tokyo | ||
15:45 15mTalk | A Sound Type System for Secure Currency Flow Technical Papers Luca Aceto Reykjavik University, Daniele Gorla Department of Computer Science, Sapienza University of Rome, Stian Lybech Reykjavik University | ||
16:00 15mTalk | Type Tailoring Technical Papers Ashton Wiersdorf University of Utah, Stephen Chang University of Massachusetts Boston, Matthias Felleisen Northeastern University, Ben Greenman University of Utah | ||
16:15 15mTalk | Learning Gradual Typing Performance Technical Papers Mohammad Wahiduzzaman Khan UL Lafayette, Sheng Chen University of Louisiana at Lafayette, Yi He Old Dominion University | ||
16:30 15mTalk | Generalizing Shape Analysis with Gradual Types Technical Papers Zeina Migeed University of California, Los Angeles, James Reed Fireworks AI, Jason Ansel Meta, Jens Palsberg University of California, Los Angeles (UCLA) | ||
16:45 15mTalk | Refinements for Multiparty Message-Passing Protocols: Specification-agnostic theory and implementation Technical Papers |