一句话：提出 Multris 分离逻辑，用多参与方协议一致性验证消息传递与共享内存并发程序的功能正确性。
本文提出 Multris，一个用于验证同时包含多参与方消息传递与共享内存并发的程序功能正确性的分离逻辑。其核心是新定义的多参与方协议一致性，保证各方遵循各自协议时通信安全。该概念受自底向上多参与方会话类型启发，但在分离逻辑而非类型系统中处理，从而支持隐式知识传递与隐式资源传递等更强机制。作者还开发了自动验证协议一致性及推理消息传递操作的策略。评估涵盖经典两方与三方买家协议，以及基于 Chang-Roberts 环领导者选举的新基准。最后，使用 Coq 中 Iris 框架对 Multris 相对于底层通道语义的可靠性进行了机器化证明。
We introduce Multris, a separation logic for verifying functional correctness of programs that combine multiparty message-passing communication with shared-memory concurrency. The foundation of our work is a novel concept of multiparty protocol consistency , which guarantees safe communication among a set of parties, provided each party adheres to its prescribed protocol. Our concept of protocol consistency is inspired by the bottom-up approach for multiparty session types. However, by considering it in the context of separation logic instead of a type system, we go further in terms of generality by supporting new notions of implicit transfer of knowledge and implicit transfer of resources . We develop tactics for automatically verifying protocol consistency and for reasoning about message-passing operations in Multris. We evaluate Multris on a range of examples, including the well-known two- and three-buyer protocols, as well as a new verification benchmark based on Chang and Roberts's ring leader election protocol. To ensure the reliability of our work, we prove soundness of Multris w.r.t. a low-level channel semantics using the Iris framework in Coq.
@article{HinrichsenJK24,
title = {Multris: Functional Verification of Multiparty Message Passing in Separation Logic},
author = {Jonas Kastberg Hinrichsen and Jules Jacobs and Robbert Krebbers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689762}
}