FMitF: Track I: Safe, Efficient Persistent Memory Systems

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

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.