Compositional Reasoning for Dynamic Distributed Systems


Ankush Desai, Amar Phanishayee, Shaz Qadeer and Sanjit A. Seshia

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2017-154
September 10, 2017

Fault-tolerant distributed systems are difficult to get right because they must deal with concurrency and failures. Despite decades of research, current approaches for a more rigorous way of building distributed systems are unsatisfactory. This paper proposes new techniques for building reliable distributed systems with two central contributions: (1) We propose a module system based on the theory of compositional trace refinement for dynamic systems consisting of asynchronously-communicating state machines, where state machines can be created dynamically and the communication topology of the existing state machines can change at runtime; (2) We present ModP, a programming system that implements our module system to enable compositional (assume-guarantee) and hierarchical (refinement) reasoning of distributed systems.

We demonstrate the efficacy of our methodology by building two practical distributed systems, a fault-tolerant transaction-commit service and fault-tolerant distributed data structures. Each system uses state machine replication (SMR) protocols for fault-tolerance. Our framework helps build these systems modularly and validates them via compositional systematic testing. We empirically show that using abstractions based compositional reasoning helps amplify the coverage during testing. We find that monolithic testing based on existing search prioritization techniques cannot find more than half the bugs found using ModP within equivalent time budgets.

Author Comments: Would like to upload a new version