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

合作研究：FMitF：第一轨：使用 Grove 对崩溃安全分布式系统进行可组合验证

• 批准号: 2318722
• 负责人: Joseph Tassarotti
• 金额: $ 25万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-03-15 至 2026-05-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2318722&HistoricalAwards=false
• 关键词: Collaborative; Research; FMitF; Track; Composable

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.

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

项目成果

Verifying vMVCC, a high-performance transaction library using multi-version concurrency control

验证使用多版本并发控制的高性能事务库vMVCC

• 发表时间: 2023
• 期刊: Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI
• 作者: Chang, Yun-Sheng;Jung, Ralf;Sharma, Upamanyu;Tassarotti, Joseph;Kaashoek, M. Frans;Zeldovich, Nickolai
• 通讯作者: Zeldovich, Nickolai

Grove: a Separation-Logic Library for Verifying Distributed Systems

• DOI: 10.1145/3600006.3613172
• 发表时间: 2023-09
• 期刊: Proceedings of the 29th Symposium on Operating Systems Principles
• 作者: Upamanyu Sharma;Ralf Jung;Joseph Tassarotti;Frans Kaashoek;Nickolai Zeldovich