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
Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change

09:00 - 11:00: REMS-DeepSpec 2020 - REM-DeepSpec Session 3 at REMS/DeepSpec live stream
rems-deepspec-202009:00 - 09:40
Kayvan MemarianUniversity of Cambridge, Victor B. F. GomesUniversity of Cambridge, UK, Stella Lau, Jean Pichon-PharabodUniversity of Cambridge, UK, Justus MatthiesenUniversity of Cambridge, Peter SewellUniversity of Cambridge
rems-deepspec-202009:50 - 10:30
Andrew AppelPrinceton