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

从手机到数据中心，多核处理器在计算基础设施中无处不在。编写正确的多线程软件来有效地利用这种多核硬件是非常困难的。在过去的几十年里，顺序软件验证领域取得了巨大的进步。 目前最先进的工具能够验证复杂的系统，如编译器和操作系统（OS）内核。 该项目旨在实现多线程软件验证的类似进展。该项目的新颖性解决了并发软件验证的基本挑战：指定和推理线程干扰。 该项目利用了一种新的线程干扰规范表示法，并将这些规范嵌入到一种新的程序逻辑（称为Mover Logic）和一种新的验证工具（称为KeyStone）中。该项目的影响是开发和验证大型多线程软件系统的更好工具，并最终提高了国家计算基础设施的可靠性和安全性。 该项目更广泛的影响包括教育和研究指导活动，特别强调传统上在计算机科学中代表性不足的群体的学生。这个项目的出发点是观察到，在多线程系统中，过程的执行与其他线程的步骤非确定性地交错，使得很难将过程的效果与其他线程的交错效果的效果分开。例如，可靠保证推理使用过程规范，其中过程和其他线程的效果仍然纠缠在一起。因此，规范与其他线程可能做的事情紧密耦合，限制了它们在其他上下文中的重用。利普顿的归约理论通过一个交换参数将一个过程的规范从其他线程中解脱出来，但是现有的基于归约的验证器需要程序员编写多个越来越精细的系统变体。 这个项目使用了一个规范符号的线程干扰，侧重于程序操作的交换属性，从而使更多的自然和成分的减少证明，没有目前的限制，无论是可靠的保证或减少为基础的approaches.This奖项反映了NSF的法定使命，并已被认为是值得的支持，通过评估使用基金会的智力价值和更广泛的影响审查标准。

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.