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

分布式系统在计算机系统基础设施中起着至关重要的作用。 然而，开发可靠的分布式系统是具有挑战性的，因为需要处理跨机器的并发性，每台机器内的并发性，可能延迟或丢弃消息的不可靠网络，以及如果一台或多台机器崩溃并重新启动而其他机器继续运行时的部分故障。 因此，分布式系统容易出错，细微的错误可能导致严重的停机。 传统的测试方法不足以消除所有这些错误。 这个项目的新奇是一种新的方法来正式验证分布式系统，允许验证组件的模块化的方式。 它允许在出现崩溃的情况下验证分布式系统。该项目的影响旨在包括提高分布式系统的可靠性和正确性，并避免代价高昂的停机。此外，新的系统验证类的实验作业正在开发中，集中在分布式systems.The技术方法解决两个具体的挑战：推理有关崩溃恢复分布式系统，以及组成分布式系统从较小的组件。 崩溃恢复具有挑战性，因为单个节点可能会崩溃并重新启动。 一旦一个节点重新开始运行，它可能不再与没有崩溃的系统的其余部分保持一致。这意味着节点可能在崩溃时丢失了所有内存内容，但可能在磁盘上持久保留了一些状态。 第二个挑战在于编写分布式系统（例如键值存储）的规范和证明，这些系统是由较小的组件（例如配置服务，锁服务或单个节点的实现）构建的。 分布式系统的扩展验证需要证明来反映这种模块性。 例如，对使用锁服务的应用程序进行推理不应要求对锁服务本身发送的网络消息进行推理。 它应该完全使用锁服务客户端存根的规范来完成。该项目使用并发分离逻辑来解决这些挑战，该逻辑提供了一种自然的方法来组成关于多个组件的证明，以及使用前/后条件规范抽象实现细节。 该项目扩展了早期的分布式系统推理技术，包括新的每节点不变量（可能需要在崩溃时修复），而不是全局不变量（即使某些节点崩溃也必须保持不变）。 此外，该项目还提供了在不可靠的计算机网络和跨多台机器的锁上对远程过程调用（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.