Visible to the public Cerberus: Towards an Executable Semantics for Sequential and Concurrent C11

Abstract:

C remains central to our computing infrastructure but still lacks a clear and complete semantics. Programmers lack tools to explore the range of behaviours they should expect; compiler development lacks test oracles; and formal verification and analysis must make (explicitly or implicitly) many choices about the specific C they target.

We describe Cerberus, a semantics for a substantial fragment of C11. Its thread-local semantics is factored via an elaboration into a simpler Core language, to make it conceptually and mathematically tractable. This is integrated with an operational model for C11 concurrency, with a mechanised proof of equivalence to the axiomatic C11 model of Batty et al. The front-end includes a parser that closely follows the C11 standard grammar and a typechecker. Cerberus is executable, to explore all behaviours or single paths of test programs, and it supports proof, as shown by a preliminary experiment in translation validation for the front-end of Clang, for very simple programs. This is a step towards a clear, consistent, and unambiguous semantics for C.

License: 
Creative Commons 2.5

Other available formats:

Cerberus: Towards an Executable Semantics for Sequential and Concurrent C11
Switch to experimental viewer