• Ilya Sergey – Programming and Proving with Distributed Protocols (26 July, 2017)

    by  • September 8, 2017 • DSG Research Seminars: Logic and Programming Languages

    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 my talk, I will 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.