FMitF: Verifying Concurrent System Software with Cspec

FMITF：使用 Cspec 验证并发系统软件

• 批准号: 1836712
• 负责人: Nickolai Zeldovich
• 金额: $ 75万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-11-01 至 2022-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1836712&HistoricalAwards=false
• 关键词: FMitF; Verifying; Concurrent; System; Software

Most computer systems involve concurrency---multiple threads, cores, or computers executing at the same time and interacting with one another. Developing concurrent software is error-prone, because the concurrent threads can interact in many unexpected ways, and it is easy for developers to overlook subtle corner-case interactions. This project will tackle this problem through the use of machine-checked proofs for concurrent software: that is, it will focus on helping developers to provide a mathematical proof that the software will execute according to its specification, for any possible interaction among the concurrent threads. As a driving example, this project will develop a verified concurrent multicore file system. This project's novelty lies in its approach for specifying and proving concurrent software that reduces the number of thread interactions that the developer must reason about, while still providing a full proof of correctness. The expected impact of this project will be a set of ideas, techniques, and tools for specifying and proving concurrent systems software. Since concurrent software plays such a critical role in computer systems, being able to verify correctness of key software components will improve reliability and security of many systems.The specific research contributions of this project will center around CSPEC, a framework for formal verification of concurrent software, which will help developers ensure that no corner cases are missed. The key challenge faced by CSPEC is to reduce the number of interactions, or interleavings, that developers must consider in their proofs. CSPEC addresses this challenge using so-called mover types to reorder commutative operations. Mover types enable developers to reason about largely sequential executions rather than all possible interleavings. CSPEC also provides a library of proof patterns for common styles of concurrency, including retry loops, state partitioning, and cooperative enforcement of rules between threads or processes. In the process of developing a verified concurrent file system on top of CSPEC, the investigators will address additional research challenges, such as formulating a specification for a POSIX file system under concurrency, integrating reasoning about crash safety and concurrency, managing the complexity of proving a sophisticated concurrent file system, and generating efficient concurrent code to achieve high performance while preserving correctness. As part of this project, the research team will also develop a course focused on formal reasoning about computer systems, which includes concurrency, reliability, and fault-tolerance.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.

大多数计算机系统涉及并发性-多个同时执行并相互交互的线程、核心或计算机。开发并发软件很容易出错，因为并发线程可以以许多意想不到的方式进行交互，并且开发人员很容易忽略细微的角例交互。这个项目将通过使用并发软件的机器检查证明来解决这个问题：也就是说，它将专注于帮助开发人员提供软件将根据其规范执行的数学证明，对于并发线程之间任何可能的交互。作为一个驱动示例，该项目将开发一个经过验证的并发多核文件系统。这个项目的新奇之处在于它指定和证明并发软件的方法，这种方法减少了开发人员必须推理的线程交互的数量，同时仍然提供了完全的正确性证明。该项目的预期影响将是一套用于指定和证明并发系统软件的想法、技术和工具。由于并发软件在计算机系统中起着至关重要的作用，能够验证关键软件组件的正确性将提高许多系统的可靠性和安全性。本项目的具体研究贡献将围绕并发软件的形式化验证框架CSPEC来进行，它将帮助开发人员确保不会遗漏任何角落案例。CSPEC面临的关键挑战是减少开发人员在证明中必须考虑的交互或交错的数量。CSPEC使用所谓的移动器类型来重新排序交换操作，以解决这一挑战。Mover类型使开发人员能够在很大程度上推理顺序执行，而不是所有可能的交错。CSPEC还为常见的并发样式提供了一个证明模式库，包括重试循环、状态分区以及线程或进程之间规则的协作实施。在CSPEC上开发验证并发文件系统的过程中，研究人员将解决其他研究挑战，如制定并发下的POSIX文件系统规范，集成关于崩溃安全和并发的推理，管理复杂并发文件系统证明的复杂性，以及生成高效的并发代码以在保持正确性的情况下实现高性能。作为该项目的一部分，研究团队还将开发一门专注于计算机系统的形式推理的课程，其中包括并发性、可靠性和容错性。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Argosy: verifying layered storage systems with recovery refinement

• DOI: 10.1145/3314221.3314585
• 发表时间: 2019-06
• 期刊: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
• 作者: Tej Chajed;Joseph Tassarotti;M. Kaashoek;Nickolai Zeldovich

GoJournal: a verified, concurrent, crash-safe journaling system

GoJournal：经过验证、并发、防崩溃的日志系统

• 发表时间: 2021
• 期刊: Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation
• 作者: Chajed, Tej;Tassarotti, Joseph;Theng, Mark;Jung, Ralf;Kaashoek, M. Frans;Zeldovich, Nickolai
• 通讯作者: Zeldovich, Nickolai

Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning

使用顺序推理验证 DaisyNFS 并发和崩溃安全文件系统

• 发表时间: 2022
• 期刊: Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022
• 作者: Chajed, Tej;Tassarotti, Joseph;Theng, Mark;Kaashoek, M. Frans;Zeldovich, Nickolai
• 通讯作者: Zeldovich, Nickolai

Verifying concurrent, crash-safe systems with Perennial

使用 Perennial 验证并发、防碰撞系统

• DOI: 10.1145/3341301.3359632
• 发表时间: 2019
• 期刊: Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP
• 作者: Chajed, Tej;Tassarotti, Joseph;Kaashoek, Frans;Zeldovich, Nickolai
• 通讯作者: Zeldovich, Nickolai