Collaborative Research: SHF: Small: RUI: Keystone: Modular Concurrent Software Verification

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

Multi-core processors are ubiquitous across computing infrastructure, from cell phones to data centers. Writing correct multi-threaded software that efficiently utilizes this multi-core hardware is notoriously difficult. Over the past several decades, the field of sequential software verification has achieved enormous advances. Current state-of-the-art tools are capable of verifying sophisticated systems such as compilers and Operating System (OS) kernels. This project aims to achieve similar advances in multi-threaded software verification. The project's novelties address the fundamental challenge of concurrent software verification: specifying and reasoning about thread interference. The project leverages a new specification notation for thread interference and will embed those specifications into a new program logic, called Mover Logic, and a new verification tool called KeyStone. The project's impacts are better tools for developing and verifying large multi-threaded software systems and, ultimately, improved reliability and security for the nation's computing infrastructure. The broader impacts of the project include education and research mentoring activities, with a particular emphasis on students from groups traditionally under-represented in computer science. The starting point for this project is the observation that, in a multi-threaded system, a procedure’s execution is non-deterministically interleaved with steps of other threads, making it difficult to disentangle the effect of the procedure from the effects of those interleaved effects of other threads. For example, rely-guarantee reasoning uses procedure specifications in which the effects of the procedure and other threads remain entangled. As a result, specifications are tightly-coupled to what other threads may do, limiting their reuse in other contexts. Lipton’s theory of reduction disentangles a procedure’s specification from other threads via a commuting argument, but existing reduction-based verifiers require programmers to write multiple, increasingly refined, variants of the system. This project uses a specification notation for thread interference that focuses on the commuting properties of program operations, thereby enabling more natural and compositional reduction proofs without the current limitations of either rely-guarantee or reduction-based approaches.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.