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.