Distributed Protocol Combinators
Distributed systems are hard to get right, model, test, debug, and teach. Their textbook definitions, typically given in a form of replicated state machines, are concise, yet prone to introducing programming errors if naïvely translated into runnable implementations.
In this work, we present Distributed Protocol Combinators (DPC), a declarative programming framework that aims to bridge the gap between specifications and runnable implementations of distributed systems, and facilitate their modeling, testing, and execution. DPC builds on ideas from state-of-the art logics for compositional systems verification. The contribution of DPC is a novel family of program-level primitives, which facilitates 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.
This paper describes the main ideas behind the design of the framework and presents its implementation in Haskell. We introduce DPC through a series of characteristic examples and showcase it on on a number of distributed protocols from the literature.
Mon 14 Jan
|16:00 - 16:30|
|16:30 - 17:00|
Kristoffer Just Arndal AndersenAarhus University, Ilya SergeyYale-NUS College and National University of SingaporePre-print
|17:00 - 17:30|
Alejandro SerranoUtrecht University, Netherlands, Victor Cacciari MiraldoUtrecht University, NetherlandsLink to publication DOI File Attached