SHF: Small: Compositional Certified Concurrent Abstraction Layers

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

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.