一句话：提出 Must 框架，用最优动态偏序归约在主流语言上建模并验证分布式协议。
分布式系统的建模与自动验证十分困难：现有模型检测器既难以支持多种通信模型，也难以扩展到生产中实际部署的系统。Must 在 Rust 等主流语言之上提供并发 API，支持多种通信模型，并采用一种新的最优动态偏序归约算法，对 API 支持的所有通信模型都保持完备性与最优性。作者用高层系统惯用法（超时、领导者选举、版本化）作为核心 API 的抽象来检验 API 的易用性，并对生产中使用的系统（复制日志、分布式事务管理协议）进行验证，展示了超越以往模型检测器的可扩展性。
We describe the design and implementation of Must, a framework for modeling and automatically verifying distributed systems. Must provides a concurrency API that supports multiple communication models, on top of a mainstream programming language, such as Rust. Given a program using this API, Must verifies it by means of a novel, optimal dynamic partial order reduction algorithm that maintains completeness and optimality for all communication models supported by the API. We use Must to design and verify models of distributed systems in an industrial context. We demonstrate the usability of Must’s API by modeling high-level system idioms (e.g., timeouts, leader election, versioning) as abstractions over the core API, and demonstrate Must’s scalability by verifying systems employed in production (e.g., replicated logs, distributed transaction management protocols), the verification of which lies beyond the capacity of previous model checkers.
@article{EneaGKM24,
title = {Model Checking Distributed Protocols in Must},
author = {Constantin Enea and Dimitra Giannakopoulou and Michalis Kokologiannakis and Rupak Majumdar},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689778}
}