CAREER: Formal Verification of Performance Properties for Distributed Systems

在我们的日常生活中，我们越来越依赖计算机：从我们的电子邮件和工作会议，到社交媒体以及与我们的朋友和家人互动。为我们提供这些服务的计算机系统不仅规模庞大，而且复杂而微妙。单个组件的速度低于预期，可能会导致整个系统出现不可预测和灾难性的行为，导致整个系统长时间不可用，中断依赖于它的所有服务（人工和自动化）。长期以来，研究界一直在努力了解这些复杂系统的性能：部署系统并在许多测试场景中观察其行为。然而，这些系统的复杂性使得不可能彻底测试所有可能出错的地方。不可避免地会出现一些极端情况，这些情况会使我们部署的系统陷入困境，我们会后悔--太晚了--我们的测试不够彻底。该提案提出了一种严格的推理方式，对我们的系统的性能：利用形式推理的最新进展，让程序员系统地开发严格的保证系统的执行时间和速度。该提案旨在巩固我们的未来系统将建立的基础。它使用形式化的推理来提供关于我们的系统在实践中将如何表现的判断而不是期望。对于最终用户来说，这意味着他们每天使用的计算机服务将更具成本效益和更可靠。然而，实现这些好处需要的不仅仅是研究。该提案提出了一个教育计划，通过开设一个关于验证的新课程、一个正在进行的验证暑期学校和一本关于如何将正式验证应用于现实世界系统的书，将验证介绍给当前和未来的工程师，使验证更接近实用。总之，本提案的研究和教育目标旨在使形式推理成为计算的一个组成部分。如果日常用户要信任我们的计算机系统，这些系统需要的不仅仅是测试;他们必须是可证明的正确的。这个奖项反映了NSF的法定使命，并已被认为是值得支持的，通过评估使用基金会的知识价值和更广泛的影响审查标准。

n our daily lives we increasingly depend on computers: from our emails and our work meetings, to social media and interacting with our friends and family. The computer systems that provide us these services are not only vast in size, but also complex and subtle. A single component being slower than expected can drive the entire system into unpredictable and catastrophic behaviors that result into the entire system being unavailable for long periods of time, disrupting all services—human and automated—that depend on it. For the longest time, the research community has been trying to understand the performance of these complex systems in a best-effort way: deploying the system and observing its behavior in a number of test scenarios. The complexity of these systems, however, makes it impossible to thoroughly test everything that can go wrong. Inevitably some corner case emerges which drives our deployed system to its knees and we discover—too late—that our testing was not thorough enough. This proposal puts forward a rigorous way of reasoning about the performance of our systems: leveraging the recent advances in formal reasoning to allow programmers to systematically develop rigorous guarantees about the duration and speed of the system’s executions.This proposal aims to solidify the foundation on which our future systems will be built. It uses formal reasoning to provide guarantees—not expectations—about how our systems will behave in practice. For the end users this means that the computer services they use every day will be more cost-effective and more reliable. Achieving these benefits, however, requires more than research. The proposal puts forth an educational plan for bringing verification closer to practicality by introducing it to current and future engineers by means of a new class on verification, an ongoing verification summer school, and a book on how to apply formal verification to real-world systems. Together, the research and educational objectives of this proposal aim to make formal reasoning an integral part of computing. If the everyday user is to put their trust in our computer systems, those systems need to be more than just tested; they must be provably correct.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.