PI: Ilya Sergey, University College London, Co-I: Nikos Gorogiannis, Facebook and University of Middlesex
- A domain-specific language (DSL) for concurrent implementation of distributed protocols.
- Prototype DSL implementations of consensus protocols: Two-PhaseCommit, Paxos, Multi-Paxos.
- An extension of Disel, a higher-order separation logic for distributed systems to handle concurrent per-node implementations of distributed protocols.
We have developed Distributed Protocol Combinators (DPC), a declarative programming framework that aims to bridge the gap between specifications and runnable implementations of distributed systems, as well as facilitate their modelling, testing, and execution. DPC builds on the ideas from the state-of-the art logics for compositional systems verification. DPC contributes with a novel family of program-level primitives, which allows construction of larger distributed systems from smaller components, streamlining the usage of the most common asynchronous message-passing communication patterns, and providing machinery for testing and user-friendly dynamic verification of systems. The approach has been implemented in a form of a reusable Haskell library, as well as a tool for visual debugging of asynchronous systems.
Declarative programming over distributed proto-cols is possible and could lead to new insights, such as better understanding on how to structure systems implementations. Even though there are several known limitations to the design of DPC due to the chosen linguistic foundations (i.e., Haskell), we consider our approach beneficial and illuminating for the purposes of prototyping, exploration, and teaching distributed system design. In future, we will explore the opportu-nities, opened by DPC, for randomised protocol testing and lightweight verification with refinement types.
The funding was used to host Kristoffer Just Andersen as a visiting student at the CS department of UCL, where he has worked under our supervision on the applications of techniques for logic-based reasoning about concurrency to the verification of distributed systems with internal multi-threaded parallelism. The project thus naturally evolved from the initially proposed research, elaborating and extending it for the distributed setting. The artefacts produced to date include the runnable prototype (in Haskell) as well as a (partially) mechanised logical development for the verification of multithreaded distributed programs. During Andersen’s stay at UCL, Sergey and Andersen developed a domain-specific language for specifying, implementing, randomised testing and visual debugging of distributed protocols.
PUBLICATIONS. [1] K. J. A. Andersen, I. Sergey, “Distributed Protocol Combinators”, PADL’19. [2] N. Polikarpova, I. Sergey. “Structuring the Synthesis of Heap-Manipulating Programs”, POPL’19. [3] K. J. A. Andersen, I. Sergey, “Protocol Combinators for Modelling, Testing, and Execution of Distributed Systems”, J. Funct. Program. 2021.
RELATED GRANTS. Dr Ilya Sergey, EPSRC Grant “Program Logics for Compositional Specification and Verification of Distributed Systems”, 01/2017-11/2018, £101,009. Dr. Ilya Sergey, Google Faculty Research Award, “Distributed System Optimisations as Network Semantics Transformations”, 2018.
