Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
复制标题
具有排名功能的分布式协议的活性属性的自动验证
DOI：
10.1145/3632877
复制
发表时间：
2024
影响因子：
--
通讯作者：
Nieh, Jason
中科院分区：
文献类型：
--
作者：
Yao, Jianan;Tao, Runzhou;Gu, Ronghui;Nieh, Jason
分布式协议长期以来都是根据其安全性和活性特性制定的。最近的许多工作都集中在自动验证分布式协议的安全属性上，但这样做的活性属性仍然是一个具有挑战性的、未解决的问题。我们推出了 LVR，这是第一个可以自动验证分布式协议的活跃属性的框架。我们的主要见解是，借助排序函数，分布式协议的大多数活跃属性可以简化为一组安全属性。实际分布式协议的此类排序函数具有某些属性，使它们易于综合，这与传统观点相反。我们证明验证活性属性可以简化为验证一组安全属性的更简单的问题，即排名函数对于任何协议状态转换都是严格递减且非负的，并且不存在死锁。 LVR 通过制定整数协议变量的参数化函数，静态分析变量的下限和上限以及它们在每次状态转换时可以改变的程度，然后将约束输入 SMT 求解器来确定排序函数的系数，从而自动合成排序函数。然后，它使用现成的验证工具来查找归纳不变量，以验证排序函数和死锁自由度的安全属性。我们证明，LVR 可以在有限的用户指导下自动验证多种分布式协议（包括各种版本的 Paxos）的活跃属性。
Distributed protocols have long been formulated in terms of their safety and liveness properties. Much recent work has focused on automatically verifying the safety properties of distributed protocols, but doing so for liveness properties has remained a challenging, unsolved problem. We present LVR, the first framework that can mostly automatically verify liveness properties for distributed protocols. Our key insight is that most liveness properties for distributed protocols can be reduced to a set of safety properties with the help of ranking functions. Such ranking functions for practical distributed protocols have certain properties that make them straightforward to synthesize, contrary to conventional wisdom. We prove that verifying a liveness property can then be reduced to a simpler problem of verifying a set of safety properties, namely that the ranking function is strictly decreasing and nonnegative for any protocol state transition, and there is no deadlock. LVR automatically synthesizes ranking functions by formulating a parameterized function of integer protocol variables, statically analyzing the lower and upper bounds of the variables as well as how much they can change on each state transition, then feeding the constraints to an SMT solver to determine the coefficients of the ranking function. It then uses an off-the-shelf verification tool to find inductive invariants to verify safety properties for both ranking functions and deadlock freedom. We show that LVR can mostly automatically verify the liveness properties of several distributed protocols, including various versions of Paxos, with limited user guidance.
登录
查看更多内容
多层次的线程模块化：组合验证中的一颗明珠
DOI：
10.1145/3009837.3009893
发表时间：
2017
期刊：
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
影响因子：
--
作者：
Jochen Hoenicke;R. Majumdar;A. Podelski
通讯作者：
A. Podelski
DOI：
10.4230/lipics.concur.2020.15
发表时间：
2020
期刊：
--
影响因子：
--
作者：
E. Neumann;Joël Ouaknine;J. Worrell
通讯作者：
E. Neumann;Joël Ouaknine;J. Worrell
通用不变量的属性导向推理或证明它们的不存在
DOI：
--
发表时间：
2015
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
Aleksandr Karbyshev;Nikolaj S. Bjørner;Shachar Itzhaky;N. Rinetzky;Sharon Shoham
通讯作者：
Sharon Shoham
计算机辅助推理
DOI：
10.1007/978-1-4757-3188-0
发表时间：
2000
期刊：
The journal of physical chemistry. A
影响因子：
--
作者：
M. Hinchey
通讯作者：
M. Hinchey
检测多线程程序中的公平非终止
DOI：
10.1007/978-3-642-31424-7_19
发表时间：
2012
期刊：
The journal of physical chemistry. A
影响因子：
--
作者：
M. Atig;A. Bouajjani;M. Emmi;A. Lal
通讯作者：
A. Lal