Award Abstract # 1836712

ABSTRACT

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.

Please report errors in award information by writing to: awardsearch@nsf.gov.