一句话：提出基于消息链的自动簿记方法，在消息传递抽象层简化异步分布式系统的验证。
异步分布式程序的验证十分困难，因为消息交错与故障会产生大量控制路径，难以推理。本文提出一种基于消息链的自动簿记方法。消息链能够揭示异步分布式系统执行中的结构，帮助程序员在消息传递这一抽象层次上验证系统。作者为 P 编程语言构建了集成消息链的验证原型，并用它验证了 16 个来自相关工作的基准、1 个体现其方法所关注系统类型的新基准以及 2 个工业基准。实验表明，消息链能够简化现有证明，且原型在运行时间上与现有工作相当。作者还将工作扩展到支持规约挖掘，发现消息链提供了足够结构，使现有学习与程序合成工具仅凭执行样例即可自动推断出有意义的规约。
Verification of asynchronous distributed programs is challenging due to the need to reason about numerous control paths resulting from the myriad interleaving of messages and failures. In this paper, we propose an automated bookkeeping method based on message chains. Message chains reveal structure in asynchronous distributed system executions and can help programmers verify their systems at the message passing level of abstraction. To evaluate our contributions empirically we build a verification prototype for the P programming language that integrates message chains. We use it to verify 16 benchmarks from related work, one new benchmark that exemplifies the kinds of systems our method focuses on, and two industrial benchmarks. We find that message chains are able to simplify existing proofs and our prototype performs comparably to existing work in terms of runtime. We extend our work with support for specification mining and find that message chains provide enough structure to allow existing learning and program synthesis tools to automatically infer meaningful specifications using only execution examples.
@article{paperbot1830,
title = {Message Chains for Distributed System Verification},
author = {Federico Mora and Ankush Desai and Elizabeth Polgreen and Sanjit A. Seshia},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622876}
}