一句话：提出 Performal，用形式化验证为真实分布式系统证明严格延迟上界，并发现性能缺陷。
分布式系统性能问题难以理解与调试，传统日志、追踪和基准测试通常需完整部署，且多在性能缺陷显现后才能发现。本文提出 Performal，将形式化证明与执行环境解耦，形式化定义延迟性质，并在真实分布式实现上证明其延迟上界。作者用 Performal 为分布式锁、ZooKeeper 和基于 MultiPaxos 的状态机复制系统证明严格的延迟上界；实验表明这些上界能较好代理部署系统行为，并可用于识别真实系统中的性能缺陷。
Understanding and debugging the performance of distributed systems is a notoriously hard task, but a critical one. Traditional techniques like logging, tracing, and benchmarking represent a best-effort way to find performance bugs, but they either require a full deployment to be effective or can only find bugs after they manifest. Even with such techniques in place, real deployments often exhibit performance bugs that cause unwanted behavior. In this paper, we present Performal, a novel methodology that leverages the recent advances in formal verification to provide rigorous latency guarantees for real, complex distributed systems. The task is not an easy one: it requires carefully decoupling the formal proofs from the execution environment, formally defining latency properties, and proving them on real, distributed implementations. We used Performal to prove rigorous upper bounds for the latency of three applications: a distributed lock, ZooKeeper and a MultiPaxos-based State Machine Replication system. Our experimental evaluation shows that these bounds are a good proxy for the behavior of the deployed system and can be used to identify performance bugs in real-world systems.
@article{paperbot2015,
title = {Performal: Formal Verification of Latency Properties for Distributed Systems},
author = {Tony Nuda Zhang and Upamanyu Sharma and Manos Kapritsos},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591235}
}