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

协作研究：SHF：小型：RUI：Keystone：模块化并发软件验证

• 批准号: 2243637
• 负责人: Cormac Flanagan
• 金额: $ 34万
• 依托单位: University of California-Santa Cruz
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2026-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2243637&HistoricalAwards=false
• 关键词: Collaborative; Research; SHF; Small; RUI

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.

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