Certified concurrent abstraction layers

35Citations
Citations of this article
23Readers
Mendeley users who have this article in their library.

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.

References Powered by Scopus

An axiomatic basis for computer programming

3594Citations
N/AReaders
Get full text

Linearizability: A Correctness Condition for Concurrent Objects

2278Citations
N/AReaders
Get full text

Concurrency and automata on infinite sequences

1370Citations
N/AReaders
Get full text

Cited by Powered by Scopus

A secure and formally verified linux KVM hypervisor

45Citations
N/AReaders
Get full text

An abstract stack based approach to verified compositional compilation to machine code

30Citations
N/AReaders
Get full text

Inductive sequentialization of asynchronous programs

25Citations
N/AReaders
Get full text

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Cite

CITATION STYLE

APA

Gu, R., Shao, Z., Kim, J., Wu, X., Koenig, J., Sjöberg, V., … Ramananandro, T. (2018). Certified concurrent abstraction layers. ACM SIGPLAN Notices, 53(4), 646–661. https://doi.org/10.1145/3192366.3192381

Readers' Seniority

Tooltip

PhD / Post grad / Masters / Doc 14

78%

Researcher 2

11%

Professor / Associate Prof. 1

6%

Lecturer / Post doc 1

6%

Readers' Discipline

Tooltip

Computer Science 18

95%

Engineering 1

5%

Save time finding and organizing research with Mendeley

Sign up for free