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.