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

从手机到数据中心，多核处理器在整个计算基础设施中无处不在。编写有效利用这种多核硬件的正确多线程软件是出了名的困难。在过去的几十年里，顺序软件验证的fi领域取得了巨大的进步。当前最先进的工具能够验证复杂的系统，如编译器和操作系统(OS)内核。该项目旨在实现多线程软件验证方面的类似进展。该项目的新颖性解决了并发软件验证的根本挑战：说明和推理线程干扰。该项目利用了一种用于线程干扰的新的规范fi阳离子表示法，并将这些规范fi阳离子嵌入到名为移动逻辑的新程序逻辑和名为Keystone的新验证fi阳离子工具中。该项目的影响是开发和验证大型多线程软件系统的更好工具，并最终提高国家计算基础设施的可靠性和安全性。该项目的更广泛影响包括教育和研究指导活动，特别强调来自传统上在计算机科学中代表性不足的群体的学生。这个项目的出发点是观察到，在多线程系统中，过程的执行与其他线程的步骤不确定地交织在一起，这使得很难将过程的效果与其他线程的这些交织效果的影响分开。例如，依赖保证推理使用过程规范，其中过程和其他线程的效果仍然纠缠在一起。因此，规范与其他线程可能做的事情紧密耦合，限制了它们在其他上下文中的重用。利普顿的约简理论通过交换参数将过程的规范从其他线程中分离出来，但现有的基于约简的验证器需要程序员编写系统的多个日益精炼的变体。该项目使用了线程干扰的规范符号，侧重于程序操作的通勤属性，从而实现了更自然和成分减少的证明，而不受当前依赖保证或基于减少的方法的限制。该奖项反映了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.