CAREER: Assertions for Distributed Applications

在多台机器上进行分布式计算是用于构建可以跨多台计算机运行或不受计算机故障影响的软件的主要工具。因此，在多台机器上运行的分布式应用程序是b谷歌、Netflix和空中交通管制系统等大多数大型服务的核心。然而，编写正确的分布式应用程序是具有挑战性的。分布式应用程序中的漏洞导致了多个服务的停机，包括Facebook、Netflix和英国的空中交通管制系统。本提案旨在开发允许分布式应用程序在运行时检测和响应错误的技术，从而最大限度地减少其影响。拟议中的研究有三个核心重点。第一个重点是开发有效的机制，通过评估关于应用程序状态的逻辑断言来检测分布式应用程序错误，并开发有效的技术来响应检测到的错误。第二个重点是开发自动检查程序员提供的断言对于检测分布式应用程序中的错误是否必要和充分的技术。第三个重点是开发技术，以确定在运行时检测到的错误的根本原因，从而允许程序员修复潜在的问题。该项目提出的机制可以提高广泛使用的在线服务和基础设施的弹性和可信度。该项目将生成一个包含这些机制的开源框架，并生成文档和教程，以简化这些想法的采用。此外，该提案计划开发新的编程作业，使用所建议的断言检查机制，以允许学生验证他们的故障处理方法。以这种方式扩展作业可以改进分布式系统的教学方法。拟议的项目将围绕这些作业开发新的研究生和本科生分布式系统课程。为这些课程开发的项目和课程材料将免费提供，以鼓励更广泛的采用。所有的源代码、数据、论文、文档和课程材料都可以从https://cims.nyu.edu/daf/获得。所有材料将在本项目结束后或出版后至少五年内保持可用，以较晚者为准。所有源代码将在ISC（互联网系统联盟）或类似的许可下发布。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.