TY  - GEN
N1  - This version is the author accepted manuscript. For information on re-use, please refer to the publisher?s terms and conditions.
Y1  - 2018/01/08/
AV  - public
TI  - Programming and Proving with Distributed Protocols
T3  - Programming and Proving with Distributed Protocols.
A1  - Sergey, I
A1  - Wilcox, JR
A1  - Tatlock, Z
KW  - distributed systems
KW  -  program logics
KW  -  safety verification
KW  -  dependent types
CY  - New York, USA
PB  - ACM
UR  - https://doi.org/10.1145/3158116
N2  - 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.
ID  - discovery10030738
ER  -