一句话：提出“假装同步”方法，将异步分布式程序同步化为等价赋值程序，用Floyd-Hoare验证条件与SMT进行验证。
分布式程序必须异步执行，这为功能正确性验证带来巨大困难。本文提出“假装同步”（pretend synchrony）方法：观察到在验证正确性时，常可可靠地将异步程序视为同步程序。为此，作者计算一个同步化（synchronization），即一个语义等价的程序，其中所有发送、接收和消息缓冲区都被替换为简单赋值，从而可直接使用Floyd-Hoare风格的验证条件与SMT求解器进行验证。该方法被实现为Go语言中编写可验证分布式程序的框架。作者通过四个具有挑战性的案例研究进行评估：经典两阶段提交协议、Raft领导者选举协议、单法令Paxos协议，以及基于Multi-Paxos的分布式键值存储。结果表明，假装同步在保持系统性能的同时，将手动指定的不变式数量减少6倍，并将验证检查时间缩短三个数量级。
We present pretend synchrony , a new approach to verifying distributed systems, based on the observation that while distributed programs must execute asynchronously, we can often soundly treat them as if they were synchronous when verifying their correctness. To do so, we compute a synchronization , a semantically equivalent program where all sends, receives, and message buffers, have been replaced by simple assignments, yielding a program that can be verified using Floyd-Hoare style Verification Conditions and SMT. We implement our approach as a framework for writing verified distributed programs in Go and evaluate it with four challenging case studies— the classic two-phase commit protocol, the Raft leader election protocol, single-decree Paxos protocol, and a Multi-Paxos based distributed key-value store. We find that pretend synchrony allows us to develop performant systems while making verification of functional correctness simpler by reducing manually specified invariants by a factor of 6, and faster , by reducing checking time by three orders of magnitude.
@article{paperbot656,
title = {Pretend synchrony: synchronous verification of asynchronous distributed programs},
author = {Klaus v. Gleissenthall and Rami Gökhan Kıcı and Alexander Bakst and Deian Stefan and Ranjit Jhala},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290372}
}