CAREER: Assertions for Distributed Applications

Distributing computation on multiple machines is the primary tool used for building software that can operate across multiple computers or despite computer failures. As a result, distributed applications that run on multiple machines lie at the core of most large services such as Google, Netflix, and air-traffic control systems. However, writing correct distributed applications is challenging.

Bugs in distributed applications have resulted in downtime for several services, including Facebook, Netflix, and the United Kingdom's air-traffic control system. This proposal aims to develop techniques to allow distributed applications to detect and respond to bugs at runtime, thus minimizing their impact.

The proposed research has three core thrusts. The first thrust focuses on developing efficient mechanisms to detect distributed application bugs by evaluating logical assertions about application state, and developing efficient techniques to respond to detected bugs. The second thrust focuses on developing techniques to check automatically whether the assertions provided by a programmer are both necessary and sufficient for detecting bugs in the distributed application.

The third thrust focuses on developing techniques to identify the root cause of a bug detected at runtime, thus allowing programmers to fix the underlying issue.

The mechanisms proposed by the project can improve the resilience and trustworthiness of widely used online services and infrastructure. The project will produce an open-source framework that incorporates these mechanisms and produce documentation and tutorials to simplify the adoption of these ideas. Additionally, the proposal plans to develop new programming assignments that use the proposed assertion checking mechanism to allow students to validate their approach to failure handling.

Extending assignments in this way improves distributed systems pedagogy. The proposed project will develop new graduate and undergraduate distributed systems classes built around these assignments. The projects and course materials developed for these classes will be freely available to encourage wider adoption.

All source code, data, papers, documentation, and course materials produced as a part of the proposed work will be available from https://cims.nyu.edu/daf/. All material will remain available for at least five years after the end of this project or five years after publication, whichever is later. All source code will be released under an ISC (Internet Systems Consortium) or similarly permissive license.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.