Cerberus: Towards an Executable Semantics for Sequential and Concurrent C11

Presented as part of the 2015 HCSS conference.

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.