%0 Generic
%A Sergey, I
%A Wilcox, JR
%A Tatlock, Z
%C New York, USA
%D 2018
%F discovery:10030738
%I ACM
%K distributed systems, program logics, safety verification, dependent types
%P 28
%T Programming and Proving with Distributed Protocols
%U https://discovery.ucl.ac.uk/id/eprint/10030738/
%V 2
%X 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.
%Z This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.