FMitF: Track I: Safe, Efficient Persistent Memory Systems

点击翻译按钮获取中文摘要

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.