Collaborative Research: FMitF: Track I: Simplifying End-to-End Verification of High-Performance Distributed Systems

该项目旨在简化和自动化高性能分布式系统的验证，即在多台计算机上运行的系统，以提高可靠性和/或性能。这样的系统对我们的社会同样至关重要，因为它们既复杂又微妙。这使它们成为正式验证的主要目标，这是一种可以从分布式系统中消除许多类错误的技术。然而，现有的验证方法是不切实际的：它们需要不合理的人力努力和直觉，或者依赖于关于它们正在验证的系统的不切实际的假设。该项目将做出一些贡献，使正式验证更接近实际，目标是现实世界中的高性能实现，包括那些依赖多线程的实现。这个项目将开发消息不变量，这是一种对分布式系统进行推理的新方法，就像它是一个集中系统一样，从而简化了所需的人力和直觉。它还将探索所有权类型：分布式系统通常涉及所有权或唯一性的概念；例如，当传递锁时，或者当将密钥从一个系统移动到另一个系统时。目前，这样的推理是由开发人员手动进行的，而且是煞费苦心的。拟议的工作将形式化分布式所有权类型，使类型检查器能够快速和自动地履行许多此类义务，从而简化开发人员的推理。这个项目的最终目的是使分布式系统的正式验证成为当前尽力而为的测试方法的实际替代方法，这种方法在保护当今的大型系统免受软件错误的影响时具有根本的局限性。通过自动化验证真实世界的高性能分布式系统-不受现有自动化方法的限制-该项目旨在确保正式验证不会仍然是学术上的好奇，而是将被实践者积极采用。从今天的尽力而为的测试技术转向正式验证的软件将带来一个未来，在那里，社会所依赖的软件产品将真正可靠和健壮，并得到机器检查的正确性数学证明的支持。该研究计划将得到综合教育和外展计划的补充，包括一年一度的暑期学校和专注于扩大对计算的参与的活动。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

This project aims to simplify and automate the verification of high-performance distributed systems, i.e., systems that run on multiple computers to improve reliability and/or performance. Such systems are as crucial for our society as they are complex and subtle. This makes them a prime target for formal verification, a technique that can eliminate many classes of bugs from distributed systems. Existing verification approaches, however, are impractical: They require an unreasonable amount of human effort and intuition or rely on unrealistic assumptions about the systems they are verifying. This project will make a number of contributions to bring formal verification closer to practicality, targeting real-world, high-performance implementations, including those that rely on multi-threading. This project will develop Message Invariants, a new way to reason about a distributed system as if it were a centralized system, thus simplifying the human effort and intuition required. It will also explore Ownership Types: Distributed systems often involve concepts of ownership or uniqueness; e.g., when passing a lock around, or when moving keys from one system to another. Currently, such reasoning is done manually—and painstakingly—by the developer. The proposed work will formalize distributed Ownership Types to enable a type checker to quickly and automatically discharge many such obligations, thus simplifying the reasoning for developers. The ultimate aim of this project is to make formal verification of distributed systems a practical alternative to the current, best-effort approach of testing, an approach that has fundamental limitations when safeguarding today's large-scale systems from software errors. By automating the verification of real-world, high-performance distributed systems—unfettered by the limitations that come with existing automated approaches—this project aims to ensure that formal verification will not remain an academic curiosity, but will instead be actively adopted by practitioners. A shift from today's best-effort testing techniques to formally verified software will lead to a future where the software products that society depends on will be truly reliable and robust, backed by machine-checked mathematical proofs of correctness. The research program will be complemented by integrated education and outreach initiatives, including an annual summer school and activities focused on broadening participation in computing.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.