Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Mon 15 Jun 2020 09:00 - 09:40 at REMS/DeepSpec live stream - REM-DeepSpec Session 3

The C programming language is notionally defined by an ISO standard, however over time the “de facto” usage of the language has diverged from that standard semantics. The main point of disagreement concerns the memory object model, and in particular the semantics of pointers. While system programmers often rely on a very concrete view of pointers (sometimes even more concrete than what the ISO standard describes), compiler implementers take a more abstract view. Some compiler optimisations, in particular those based on alias-analysis, reason about the provenance of pointers: how pointer values are constructed during the program execution, instead of only considering their representations and types.

In this talk, we present Cerberus: an executable semantics for a substantial fragment of C capturing that ISO specification, while reconciling the concrete and abstract views of the C memory model with a notion of pointer provenance that admits many systems-programming idioms and compiler optimisations, and which has been approved in principle by the WG14 and WG21 C/C++ ISO standards committees. The model is defined by elaboration into a intermediate language, Core, while retaining some level of implementation agnosticism. Being executable, Cerberus can be used as an oracle for exploring the range of behaviours that one should expect for reasonably sized programs, including all the C undefined behaviours. Web interfaces support interactive exploration and bounded model-checking: https://cerberus.cl.cam.ac.uk/cerberus and https://cerberus.cl.cam.ac.uk/bmc.html.

Mon 15 Jun

Displayed time zone: Pacific Time (US & Canada) change

09:00 - 11:00
REM-DeepSpec Session 3REMS-DeepSpec at REMS/DeepSpec live stream
09:00
40m
Talk
Cerberus: executable reference semantics and memory object models for ISO and de facto C
REMS-DeepSpec
P: Kayvan Memarian University of Cambridge, Victor B. F. Gomes University of Cambridge, UK, Stella Lau , Jean Pichon-Pharabod University of Cambridge, UK, Justus Matthiesen University of Cambridge, Peter Sewell University of Cambridge
09:50
40m
Talk
Verified Software Toolchain: a powerful and practical tool
REMS-DeepSpec
Andrew Appel Princeton