We present a unification of refinement and Hoare-style reasoning in a foundational mechanized higher-order distributed separation logic. This unification enables us to prove formally in the Coq proof assistant that concrete implementations of challenging distributed systems refine more abstract models and to combine refinement-style reasoning with Hoare-style program verification. We use our logic to prove correctness of concrete implementations of two-phase commit and single-decree Paxos by showing that they refine their abstract TLA+ specifications. We further use our notion of refinement to transfer fairness assumptions on program executions to model traces and then transfer liveness properties of fair model traces back to program executions, which enables us to prove liveness properties such as strong eventual consistency of a concrete implementation of a Conflict-Free Replicated Data Type and fair termination of a concurrent program.


翻译:我们在一个基础性机械化的更高秩序的分布式分离逻辑中统一了完善和Hoare式推理。这种统一使我们能够在Coq验证助理中正式证明,具有挑战性的分布式系统的具体实施将改进更抽象的模式,并将完善式推理与Hoare式程序核查相结合。我们用我们的逻辑来证明两阶段承诺和单层和平的具体实施是正确的,表明它们完善了抽象的TLA+规格。我们进一步利用我们的推理概念,将关于方案执行的公平假设转换为模拟痕迹,然后将公平模型的活性特性追溯到方案执行,从而使我们能够证明具体实施一个冲突重复的数据类型和公平终止一个同时的方案最终具有很强的一致性。

0
下载
关闭预览

相关内容

【干货书】机器学习速查手册,135页pdf
专知会员服务
125+阅读 · 2020年11月20日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
78+阅读 · 2020年7月26日
Python分布式计算,171页pdf,Distributed Computing with Python
专知会员服务
107+阅读 · 2020年5月3日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
194+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
分布式并行架构Ray介绍
CreateAMind
9+阅读 · 2019年8月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
Disentangled的假设的探讨
CreateAMind
9+阅读 · 2018年12月10日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
分布式TensorFlow入门指南
机器学习研究会
4+阅读 · 2017年11月28日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Implicit Maximum Likelihood Estimation
Arxiv
7+阅读 · 2018年9月24日
Arxiv
4+阅读 · 2018年1月15日
VIP会员
相关资讯
分布式并行架构Ray介绍
CreateAMind
9+阅读 · 2019年8月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
Disentangled的假设的探讨
CreateAMind
9+阅读 · 2018年12月10日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
分布式TensorFlow入门指南
机器学习研究会
4+阅读 · 2017年11月28日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Top
微信扫码咨询专知VIP会员