SHF: Small: Compositional Certified Concurrent Abstraction Layers

SHF：小型：组合认证的并发抽象层

• 批准号: 2313433
• 负责人: Zhong Shao
• 金额: $ 54万
• 依托单位: Yale University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2026-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2313433&HistoricalAwards=false
• 关键词: SHF; Small; Compositional; Certified; Concurrent

Concurrent abstraction layers (CCAL) are ubiquitous in modern computer systems because of the pervasiveness of multithreaded programming and multicore hardware. Despite their obvious importance, concurrent abstraction layers have not been treated formally. In 2016, the investigator and his team developed CCAL---a fully mechanized programming toolkit (in Coq) for building certified concurrent abstraction layers. They also applied it to build Certified OS Kernels (CertiKOS), the world's first fully certified concurrent Operating System (OS) kernel. CCAL, however, does not support the general composition of linearizable concurrent objects. It focuses on atomicity but many concurrent libraries do not have sequential atomic specification. This significantly limits CCAL's power and applicability in verifying realistic concurrent OS kernels. This project aims to develop a novel compositional theory of linearizability and a new CCAL toolkit that addresses all of the previous shortcomings. The project's novelties also include new semantic models and formal frameworks for supporting compositional specification, abstraction, and refinement of concurrent programs. The project's impacts include a new set of technologies for building reliable concurrent operating systems, which in turn facilitates the construction of large-scale secure system infrastructures and improves the cybersecurity of our society in general.More specifically, the project will make several related scientific contributions regarding the theory and practice of linearizability, the gold standard for reasoning about correctness of concurrent objects and supporting compositional verification of concurrent programs. First, it will contribute a novel and significantly generalized compositional theory of linearizability that goes much beyond atomicity and can support realistic threading models (containing multiple Central Processing Unit (CPU) cores, kernel/user-level threads, and hardware devices with interrupts), liveness reasoning, crash-safe concurrency, and weak consistency models. Second, basing upon these new compositional semantic models, it will develop and implement various compositional program logics to verify both the safety and progress properties of concurrent objects with support to blocking concurrency, system crashes, and weak memory models. Third, it will implement and integrate the new theory and program logics into the new CCAL toolkit and apply it to verify advanced kernel synchronization libraries and build realistic compositional concurrent OS kernels and hypervisors. On the educational side, this project will develop new courses on certified system software and formal verification. Artifacts resulting from the project will be made open source to ensure rapid dissemination of ideas.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.

由于多线程编程和多核硬件的普及，并发抽象层(CCAL)在现代计算机系统中无处不在。尽管并发抽象层很重要，但它们还没有被正式对待。2016年，研究人员和他的团队开发了CCAL-一个用于构建经过认证的并发抽象层的全机械化编程工具包(Coq)。他们还将其应用于构建经过认证的OS内核，这是世界上第一个完全经过认证的并发操作系统(OS)内核。然而，CCAL不支持可线性化并发对象的一般组合。它关注原子性，但许多并发库没有顺序的原子规范。这极大地限制了CCAL在验证真实并发操作系统内核方面的能力和适用性。该项目旨在开发一种新的可线性化合成理论和一个新的CCAL工具包，以解决所有以前的缺点。该项目的新颖性还包括用于支持并发程序的组合规范、抽象和精化的新语义模型和形式化框架。该项目的影响包括一套用于构建可靠的并发操作系统的新技术，这反过来又促进了大规模安全系统基础设施的建设，并总体上提高了我们社会的网络安全。更具体地说，该项目将在线性化理论和实践方面做出一些相关的科学贡献，线性化是推理并发对象正确性的金标准，并支持并发程序的组成验证。首先，它将贡献一种新的、显著推广的线性化组合理论，该理论远远超出原子性，可以支持现实的线程模型(包含多个中央处理单元(CPU)核心、内核/用户级线程和具有中断的硬件设备)、活跃性推理、崩溃安全并发和弱一致性模型。其次，基于这些新的组合语义模型，它将开发和实现各种组合程序逻辑，以验证并发对象的安全性和进步性，并支持阻塞并发、系统崩溃和弱内存模型。第三，它将实现新的理论和程序逻辑并将其集成到新的CCAL工具包中，并将其应用于验证高级内核同步库和构建现实的构件式并发操作系统内核和管理程序。在教育方面，该项目将开发关于认证系统软件和正式验证的新课程。该项目产生的文物将被开源，以确保想法的快速传播。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。