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

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

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.