SHF: Small: Compositional Certified Concurrent Abstraction Layers

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

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.