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的法规任务，并认为通过基金会的知识优点和广泛的criter scritia criter criter criter criter criter criter criter criter criter crietia criteria crietia criteria criter criteria criteria criteria crietia croperia cromitia cribitia均值得一提。