SHF: Small: Compositional Certified Concurrent Abstraction Layers

Yale University, New Haven CT

Investigators

Abstract

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.