THIS REPORT HAS BEEN WITHDRAWN

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

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2017-163
November 21, 2017

Distributed systems are notoriously difficult to get right as they must deal with concurrency and failures. This paper proposes 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 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) 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. Our framework helps implement these systems modularly and validate them via compositional systematic testing. We empirically demonstrate that using abstractions based compositional reasoning helps amplify the coverage during testing. We show that monolithic testing cannot find more than half the critical bugs found using ModP within equivalent time budgets.

Author Comments: I am withdrawing this article as I am updating it with a newer version