eprintid: 10030738
rev_number: 26
eprint_status: archive
userid: 608
dir: disk0/10/03/07/38
datestamp: 2017-11-08 16:04:33
lastmod: 2020-05-01 02:52:51
status_changed: 2017-11-08 16:04:33
type: proceedings_section
metadata_visibility: show
creators_name: Sergey, I
creators_name: Wilcox, JR
creators_name: Tatlock, Z
title: Programming and Proving with Distributed Protocols
ispublished: pub
divisions: UCL
divisions: A01
divisions: B04
divisions: C05
keywords: distributed systems, program logics, safety verification, dependent types
note: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
abstract: 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.
date: 2018-01-08
date_type: published
publisher: ACM
official_url: https://doi.org/10.1145/3158116
oa_status: green
full_text_type: other
language: eng
primo: open
primo_central: open_green
verified: verified_manual
elements_id: 1505988
doi: 10.1145/3158116
lyricists_name: Sergey, Ilya
lyricists_id: ISERG72
actors_name: Waragoda Vitharana, Nimal
actors_id: NWARR44
actors_role: owner
full_text_status: public
series: Programming and Proving with Distributed Protocols.
publication: Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL
volume: 2
place_of_pub: New York, USA
pagerange: 28
event_title: POPL
event_location: Los Angeles, CA, USA
event_dates: 07 January 2018 - 13 January 2018
institution: POPL
book_title: Proceedings of the Programming and Proving with Distributed Protocols - 2017
citation:        Sergey, I;    Wilcox, JR;    Tatlock, Z;      (2018)    Programming and Proving with Distributed Protocols.                     In:  Proceedings of the Programming and Proving with Distributed Protocols - 2017.  (pp. p. 28).  ACM: New York, USA.       Green open access   
 
document_url: https://discovery.ucl.ac.uk/id/eprint/10030738/1/Sergey_disel.pdf