FMitF: Track I: Safe, Efficient Persistent Memory Systems

FMITF：第一轨：安全、高效的持久内存系统

• 批准号: 2220410
• 负责人: Brian Demsky
• 金额: $ 75万
• 依托单位: University of California-Irvine
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2220410&HistoricalAwards=false
• 关键词: FMitF; Track; Safe; Efficient; Persistent

Emerging persistent-memory technologies provide the performance of current random-access computer memories while preserving data even in the presence of power outages. Unfortunately, developing software that uses persistent memory is challenging – a key challenge is ensuring that software fails consistently (called crash-consistent software) or, in other words, that software produces correct results even when the system suffers a power failure. Crash-consistency software errors can be difficult to find during the testing phase of software development and may only be revealed when production systems lose important data. Existing software tools can only find such errors that reveal themselves during testing and cannot ensure correctness for other executions of the same piece of software. The project's novelties are (1) the development of a verification system that can guarantee that software is crash-consistent, (2) the development of novel software that uses persistent memory, and (3) the application of the verification tools to ensure the correctness of these software. The project's broader significance and importance are: (1) the development of tools that can protect society from the harms of software errors in future persistent-memory systems and (2) training of a new generation of computer scientists to build verified systems.This project is building the RustPM verification infrastructure for persistent-memory systems that guarantees crash-consistency. The basic approach has two components: (1) verify that a program correctly uses flush and fence operations and (2) verify that the data-structure operations are failure-atomic. The project is developing case studies in the domains of fast and reliable network-attached storage and efficient network middleboxes. A key focus of these systems is to use persistent memory to enable them to survive and recover from power outages. These systems have stringent performance requirements and use log-free persistent data structures to meet these requirements. The project is using RustPM's verification to ensure that these log-free data structures are crash-consistent. The needs of the two systems drives the development of the RustPM verification system and serves as a platform to evaluate the flexibility of RustPM.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.

新兴的持久内存技术提供了当前随机访问计算机内存的性能，同时即使在断电的情况下也能保留数据。不幸的是，开发使用持久内存的软件具有挑战性 - 一个关键挑战是确保软件始终失败（称为崩溃一致软件），或者换句话说，即使系统发生电源故障，软件也能产生正确的结果。 在软件开发的测试阶段很难发现崩溃一致性软件错误，只有当生产系统丢失重要数据时才会被发现。现有的软件工具只能发现在测试过程中暴露出来的错误，并且不能确保同一软件的其他执行的正确性。 该项目的新颖之处在于（1）开发能够保证软件崩溃一致的验证系统，（2）开发使用持久内存的新颖软件，以及（3）应用验证工具来确保这些软件的正确性。该项目更广泛的意义和重要性在于：(1) 开发能够保护社会免受未来持久性内存系统软件错误危害的工具；(2) 培训新一代计算机科学家来构建经过验证的系统。该项目正在为持久性内存系统构建 RustPM 验证基础设施，以保证崩溃一致性。 基本方法有两个组成部分：(1) 验证程序是否正确使用刷新和栅栏操作；(2) 验证数据结构操作是否是故障原子的。 该项目正在开发快速可靠的网络附加存储和高效网络中间盒领域的案例研究。 这些系统的一个重点是使用持久内存来使它们能够在断电时生存并恢复。这些系统具有严格的性能要求，并使用无日志持久数据结构来满足这些要求。 该项目正在使用 RustPM 的验证来确保这些无日志数据结构是崩溃一致的。 这两个系统的需求推动了 RustPM 验证系统的开发，并作为评估 RustPM 灵活性的平台。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。