Thu 11 Jan 2018 11:45 - 12:10 at Bunker Hill - Consistency Chair(s): Xinyu Feng

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.

Thu 11 Jan

POPL-2018-papers
10:30 - 12:10: Research Papers - Consistency at Bunker Hill
Chair(s): Xinyu FengUniversity of Science and Technology of China
POPL-2018-papers10:30 - 10:55
Talk
Michael EmmiNokia Bell Labs, Constantin EneaUniversité Paris Diderot
POPL-2018-papers10:55 - 11:20
Talk
Oded PadonTel Aviv University, Jochen HoenickeUniversität Freiburg, Giuliano LosaUniversity of California at Los Angeles, USA, Andreas PodelskiUniversity of Freiburg, Germany, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university
POPL-2018-papers11:20 - 11:45
Talk
Gowtham KakiPurdue University, Kartik NagarPurdue University, Mahsa NajafzadehPurdue University, Suresh JagannathanPurdue University
POPL-2018-papers11:45 - 12:10
Talk
Ilya SergeyUniversity College London, James R. WilcoxUniversity of Washington, Zachary TatlockUniversity of Washington
DOI Pre-print