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 the ideas from the 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 a number of distributed protocols from the literature.

This paper extends our preceeding conference publication (Andersen & Sergey, 2019a) with an exploration of randomized testing for protocols and their implementations, and an additional case study demonstrating bounded model checking of protocols.

The three-continuation approach to coroutine pipelines efficiently represents a large number of connected components. Previous work in this area introduces this alternative encoding but does not shed much light on the underlying principles for deriving this encoding from its specification. This paper gives this missing insight by deriving the three-continuation encoding based on eliminating the mutual recursion in the definition of the connect operation. Using the same derivation steps, we are able to derive a similar encoding for a more general setting, namely bidirectional pipes. Additionally, we evaluate the encoding in an advertisement analytics benchmark where it is as performant as pipes, conduit, and streamly, which are other common Haskell stream processing libraries.