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 (MPST)). 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 previous values exchanged. Unfortunately, existing refinement theories and implementations are tightly coupled with 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 named refined communicating system (RCS), which is an extension of communicating automata systems 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.

翻译：多参与者消息传递协议因交互失配导致死锁等错误而难以设计。现有协议规范格式（如多参与者会话类型）旨在预防此类错误。为进一步约束协议，可通过细化（即基于先前交换值控制协议行为的逻辑谓词）扩展规范。然而，现有细化理论与实现均与特定规范格式紧密耦合。本文提出支持细化的多参与者消息传递协议框架及其Rust实现。该工作将细化的正确性与底层计算模型解耦，形成了与规范无关的框架。我们的贡献包含三方面：首先，引入刻画有效细化迹的追踪系统，即符合细化约束的发送/接收动作序列。其次，提出名为细化通信系统（RCS）的正确计算模型，这是对带细化的通信自动机系统的扩展。我们证明RCS仅产生有效的细化迹，并展示如何从主流协议规范格式（如细化多参与者会话类型或细化编排自动机）生成RCS。再次，通过开发静态分析技术和动态细化评估的改进计算模型，论证了框架的灵活性。最后，我们为去中心化RMPST提供Rust工具链，通过文献基准测试评估实现效果，观察到细化开销可忽略不计。