Performal: Formal Verification of Latency Properties for Distributed Systems
Performal: Formal Verification of Latency Properties for Distributed Systems
复制标题
表演：分布式系统延迟属性的形式验证
DOI：
10.1145/3591235
复制
发表时间：
2023
影响因子：
--
通讯作者：
Kapritsos, Manos
中科院分区：
文献类型：
--
作者：
Zhang, Tony Nuda;Sharma, Upamanyu;Kapritsos, Manos
理解和调试分布式系统的性能是一项非常困难的任务，但也是一项关键的任务。日志记录、跟踪和基准测试等传统技术代表了查找性能错误的最佳方法，但它们要么需要全面部署才能有效，要么只能在错误出现后才能找到。即使这样的技术到位，真实的部署往往表现出性能缺陷，导致不必要的behavior.In本文中，我们提出了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.
登录
查看更多内容
云分布式系统性能故障的部署前检测
DOI：
--
发表时间：
2015
期刊：
USENIX Workshop on Hot Topics in Cloud Computing
影响因子：
--
作者：
Riza O. Suminto;Agung Laksono;A. Satria;Thanh Do;Haryadi S. Gunawi
通讯作者：
Haryadi S. Gunawi
验证实时软件不合理（今天） - 特邀演讲摘要
DOI：
--
发表时间：
2012
期刊：
Haifa Verification Conference
影响因子：
--
作者：
Edward A. Lee
通讯作者：
Edward A. Lee
执行时间配置文件
DOI：
--
发表时间：
2007
期刊：
影响因子：
--
作者：
Stefan M. Petters
通讯作者：
Stefan M. Petters
DOI：
--
发表时间：
2010
期刊：
--
影响因子：
--
作者：
B. Sigelman;L. Barroso;M. Burrows;Patrick Stephenson;Manoj Plakal;Donald Beaver;Saul Jaspan;C. Shanbh
通讯作者：
B. Sigelman;L. Barroso;M. Burrows;Patrick Stephenson;Manoj Plakal;Donald Beaver;Saul Jaspan;C. Shanbh
影响因子：
1.3
作者：
Thomas Sewell;Felix Kam;Gernot Heiser
通讯作者：
Gernot Heiser