The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Certified Concurrent Abstraction Layers

Last modified: Mon Jun 4 19:39:48 2018 GMT.

Authors

Ronghui Gu
Zhong Shao
Jieung Kim
Newman Wu
Jérémie Koenig
Vilhelm Sjöberg
Hao Chen
David Costanzo
Tahina Ramananandro

Abstract

Concurrent abstraction layers are ubiquitous in modern computer systems because of the pervasiveness of multithreaded programming and multicore hardware. Abstraction layers are used to hide the implementation details (e.g., fine-grained synchronization) and reduce the complex dependencies among components at different levels of abstraction. Despite their obvious importance, concurrent abstraction layers have not been treated formally. This severely limits the applicability of layer-based techniques and makes it difficult to scale verification across multiple concurrent layers.

In this paper, we present CCAL---a fully mechanized programming toolkit developed under the CertiKOS project---for specifying, composing, compiling, and linking certified concurrent abstraction layers. CCAL consists of three technical novelties: a new game-theoretical, strategy-based compositional semantic model for concurrency (and its associated program verifiers), a set of formal linking theorems for composing multithreaded and multicore concurrent layers, and a new CompCertX compiler that supports certified thread-safe compilation and linking. The CCAL toolkit is implemented in Coq and supports layered concurrent programming in both C and assembly. It has been successfully applied to build a fully certified concurrent OS kernel with fine-grained locking.

Published

In Proc. 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'18), Philadelphia, PA, pages 646-661, June 2018.
  • Conference Paper [PDF]

  • Copyright © 1996-2019 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon