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

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2018-95

July 30, 2018

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2018/EECS-2018-95.pdf

Real-world distributed systems are rarely built as a monolithic system. Instead, they are a composition of multiple interacting components that together ensure the desired system specification. Programming these systems is challenging as one must deal with both 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 dynamically created 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) testing of distributed systems.

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. Our framework helps implement these systems modularly and validate them via compositional systematic testing. We empirically demonstrate that using abstraction-based compositional reasoning 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.

---

BibTeX citation:

@techreport{Desai:EECS-2018-95,
    Author= {Desai, Ankush and Phanishayee, Amar and Qadeer, Shaz and Seshia, Sanjit A.},
    Title= {Compositional Programming and Testing of Dynamic Distributed Systems},
    Year= {2018},
    Month= {Jul},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2018/EECS-2018-95.html},
    Number= {UCB/EECS-2018-95},
    Abstract= {Real-world distributed systems are rarely built as a monolithic system. Instead, they are a composition of multiple interacting components that together ensure the desired system specification.
Programming these systems is challenging as one must deal with both 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 dynamically created 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) testing of distributed systems.

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.
Our framework helps implement these systems modularly and validate them via compositional systematic testing.
We empirically demonstrate that using abstraction-based compositional reasoning 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.},
}

EndNote citation:

%0 Report
%A Desai, Ankush 
%A Phanishayee, Amar 
%A Qadeer, Shaz 
%A Seshia, Sanjit A. 
%T Compositional Programming and Testing of Dynamic Distributed Systems
%I EECS Department, University of California, Berkeley
%D 2018
%8 July 30
%@ UCB/EECS-2018-95
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2018/EECS-2018-95.html
%F Desai:EECS-2018-95