Programming and proving with distributed protocols
Programming and proving with distributed protocols
复制标题
DOI：
10.1145/3158116
复制
发表时间：
2017-12
影响因子：
--
通讯作者：
Ilya Sergey;James R. Wilcox;Zachary Tatlock
中科院分区：
文献类型：
--
作者：
Ilya Sergey;James R. Wilcox;Zachary Tatlock
分布式系统在现代基础设施中起着至关重要的作用，但众所周知，难以正确实施。这个困难源于两个主要挑战：（a）正确实现核心系统组件（例如，两阶段提交），因此所有内部不变性都保持；（b）正确地构成独立的系统组件来运行可信赖的应用程序（例如，持久存储构建在两个阶段提交实例之上）。最近的工作已经通过机械验证核心分布式组件的实现来解决（a）的几种方法，但是不存在通过将这些经过验证的组件组合到较大的经过验证的应用程序中来解决（b）。结果，对关键系统组件的昂贵验证工作不容易重复使用，这阻碍了进一步的验证工作。在本文中，我们介绍了Disel，这是分布式系统及其客户的实施和组成验证的第一个框架，所有框架都属于COQ证明助手的机械化基础背景。在DISEL中，用户使用特定于域的特定语言实现了分布式系统，该语言浅层嵌入了COQ中，并提供了高级编程结构以及低水平的通信原始系统。复合系统的组件在DISEL中指定为协议，从实现细节中捕获系统特定的逻辑和DISENTANGLE系统定义。借助Disel的依赖类型系统，实现良好的实现总是满足其协议的不变性，并且永远不会出错，允许用户使用Disel的Hoare式程序逻辑进行交互性验证系统实现，该逻辑扩展了最先进的技巧，以扩展一致性的一致性。验证分布式设置。借助Disel逻辑提供的替换原理和框架规则，可以组成系统组件，从而导致可重复使用的验证的分布式系统。我们描述了DiSel，说明了它在一系列示例中的使用，概述了其逻辑和元数据，并报告了我们使用它作为实施，指定和验证分布式系统的框架的经验。
Distributed systems play a crucial role in modern infrastructure, but are notoriously difficult to implement correctly. This difficulty arises from two main challenges: (a) correctly implementing core system components (e.g., two-phase commit), so all their internal invariants hold, and (b) correctly composing standalone system components into functioning trustworthy applications (e.g., persistent storage built on top of a two-phase commit instance). Recent work has developed several approaches for addressing (a) by means of mechanically verifying implementations of core distributed components, but no methodology exists to address (b) by composing such verified components into larger verified applications. As a result, expensive verification efforts for key system components are not easily reusable, which hinders further verification efforts. In this paper, we present Disel, the first framework for implementation and compositional verification of distributed systems and their clients, all within the mechanized, foundational context of the Coq proof assistant. In Disel, users implement distributed systems using a domain specific language shallowly embedded in Coq and providing both high-level programming constructs as well as low-level communication primitives. Components of composite systems are specified in Disel as protocols, which capture system-specific logic and disentangle system definitions from implementation details. By virtue of Disel's dependent type system, well-typed implementations always satisfy their protocols' invariants and never go wrong, allowing users to verify system implementations interactively using Disel's Hoare-style program logic, which extends state-of-the-art techniques for concurrency verification to the distributed setting. By virtue of the substitution principle and frame rule provided by Disel's logic, system components can be composed leading to modular, reusable verified distributed systems. We describe Disel, illustrate its use with a series of examples, outline its logic and metatheory, and report on our experience using it as a framework for implementing, specifying, and verifying distributed systems.