Collaborative Research: FMitF: Track I: Composable Verification of Crash-Safe Distributed Systems with Grove

分布式系统在计算机系统基础设施中起着至关重要的作用。然而，开发可靠的分布式系统是具有挑战性的，因为需要处理机器之间的并发性、每台机器内部的并发性、可能延迟或丢弃消息的不可靠网络，以及如果一台或多台机器崩溃并重新启动而其他机器继续运行时出现部分故障。因此，分布式系统容易出错，细微的错误可能导致严重的中断。传统的测试方法不足以消除所有这样的错误。这个项目的新颖之处在于，它提供了一种对分布式系统进行正式验证的新方法，允许以模块化的方式验证组件。它允许在出现崩溃时对分布式系统进行验证。这个项目的影响包括提高分布式系统的可靠性和正确性，避免代价高昂的中断。此外，系统验证课程的新实验作业正在开发中，重点放在分布式系统上。该技术方法解决了两个特定的挑战：对分布式系统中的崩溃恢复进行推理，以及用较小的组件组合分布式系统。崩溃恢复具有挑战性，因为单个节点可能崩溃并重新启动。一旦某个节点重新开始运行，它可能不再与系统中没有崩溃的其余部分保持一致。这意味着节点可能在崩溃时丢失了所有内存内容，但可能在磁盘上持久地保留了一些状态。第二个挑战在于组合分布式系统（例如键值存储）的规范和证明，这些系统由较小的组件（例如配置服务、锁服务或单个节点的实现）构建而成。分布式系统的扩展验证需要证明来反映这种模块化。例如，对使用锁服务的应用程序的推理不应该需要对锁服务本身发送的网络消息进行推理。它应该完全使用锁服务客户机存根的规范来完成。该项目使用并发分离逻辑解决了这些挑战，并发分离逻辑为组合多个组件的证明提供了一种自然的方法，并使用前置/后用条件规范抽象了实现细节。该项目使用分布式系统推理技术扩展了早期的工作，包括与全局不变量（即使某些节点崩溃也必须保持）相对的新类型的每节点不变量（可能需要在崩溃时修复）。此外，该项目还提供了在不可靠的计算机网络和跨多台机器的锁之上对远程过程调用（RPC）的精确一次语义进行推理的技术。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Distributed systems play a crucial role in computer systems infrastructure. Nevertheless, developing reliable distributed systems is challenging due to the need to contend with concurrency across machines, concurrency within each machine, unreliable networks that can delay or drop messages, and partial failures if one or more machines crash and reboot while others continue running. As a result, distributed systems are error-prone and subtle bugs can lead to significant outages. Traditional testing approaches are insufficient to eliminate all such bugs. This project's novelty is a new approach to formal verification of distributed systems that allows verifying components in a modular fashion. It allows for verification of distributed systems in the presence of crashes. This project's impact is intended to include improving the reliability and correctness of distributed systems and avoid costly outages. In addition, new lab assignments for systems-verification classes are being developed, focused on distributed systems.The technical approach addresses two specific challenges: reasoning about crash recovery in distributed systems, as well as composing distributed systems from smaller components. Crash recovery is challenging because individual nodes can crash and reboot. Once a node starts running again, it might no longer be consistent with the rest of the system that did not crash. This means the node may have lost all of its memory contents on crash but may have kept some state durably on disk. The second challenge lies in composing specifications and proofs of distributed systems (such as a key-value store) that are built out of smaller components (such as a configuration service, a lock service, or the implementation of an individual node). Scaling verification of distributed systems requires the proof to reflect this modularity. For example, reasoning about an application that uses a lock service should not require reasoning about the network messages sent by the lock service itself. It should be done purely using the specifications for the lock service client stubs. This project tackles these challenges using concurrent separation logic, which provides a natural approach for composing proofs about multiple components, as well as abstracting away implementation details with a pre/post-condition specification. This project extends earlier work with techniques for distributed system reasoning, including new kinds of per-node invariants (which might need to be repaired on crash) as opposed to global invariants (which must hold even if some nodes have crashed). In addition, the project provides techniques for reasoning about exactly-once semantics of Remote Procedure Calls (RPC) on top of unreliable computer networks and locks that span multiple machines.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.