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 ---一个完全机械化的编程工具包（IN COQ），用于建筑认证的同时抽象层。他们还将其应用于构建经认证的OS内核（Certikos），这是世界上第一个完全认证的并发操作系统（OS）内核。但是，CCAL不支持可线化并发对象的一般组成。它着重于原子性，但许多并发库没有顺序原子规范。这显着限制了CCAL在验证现实的并发OS内核方面的功能和适用性。该项目旨在开发一种新颖的线性化构图理论和一个新的CCAL工具包，以解决所有以前的缺点。该项目的新颖性还包括新的语义模型和正式框架，用于支持构图规范，抽象和并发程序的完善。该项目的影响包括一套新的技术，用于构建可靠的并发操作系统，这反过来促进了大规模安全的系统基础架构的构建，并改善了我们社会的网络安全性，更具体地说，该项目将对有关线性的理论和实践进行多个相关的科学贡献，以构成对物体的合成性和辅助对象的理论标准。首先，它将贡献一种新颖且显着概括的线性化构成理论，它超出了原子能，并且可以支持现实的线程模型（包含多个中央处理单元（CPU）核心，内核/用户级线程，以及带有中断的硬件设备），易用推理，崩溃的相一致性和弱点。其次，基于这些新的构图语义模型，它将开发和实施各种组成程序逻辑，以验证并发对象的安全性和进度属性，并支持阻止并发，系统崩溃和弱内存模型。第三，它将将新的理论和程序逻辑实施并集成到新的CCAL工具包中，并将其应用于验证高级内核同步库，并构建现实的构图并发同时发生的OS内核和管理程序。在教育方面，该项目将开发有关认证系统软件和正式验证的新课程。该项目产生的工件将被开源以确保快速传播思想。该奖项反映了NSF的法定任务，并使用基金会的知识分子优点和更广泛的影响评估标准，被认为值得通过评估来获得支持。