Programming distributed system is challenging as one must deal with both concurrency and failures. Real-world distributed systems are rarely implemented as a monolithic system. Instead, they are a composition of multiple complex interacting components that together ensure the desired system-level specification.

We present ModP, a programming system that implements a module system to enable compositional reasoning (assume-guarantee) of distributed systems. Our module system based on the theory of compositional trace refinement for actor programs consisting of asynchronously-communicating state machines, where state machines can be dynamically created and communication topology of the existing state machines can change at runtime.

We demonstrate the efficacy of our framework by building two practical distributed systems, a fault-tolerant transaction-commit service and a fault-tolerant replicated hash-table. ModP helps implement these systems modularly and validate them via compositional systematic-testing. Our evaluation demonstrates that the abstraction-based compositional reasoning approach helps amplify the coverage during testing and scale it to real-world distributed systems. The distributed services built using ModP achieve performance comparable to open-source equivalents.