HN Theater @HNTheaterMonth

http://llvm.org/devmtg/2018-04/
—
The Cerberus Memory Object Semantics for ISO and De Facto C - Peter Sewell, University of Cambridge

Slides: Coming Soon
—
The semantics of pointers and memory objects in C has been a vexed question for many years. C values cannot be treated as simple abstract or concrete entities: the language exposes their representations, but compiler optimisations rely on analyses that reason about provenance and initialisation status, not just runtime representations. The ISO standard leaves much of this unclear, and in some aspects differs with de facto standard usage - which itself is difficult to investigate.

This talk will describe our candidate source-language semantics for memory objects and pointers in C, as it is used and implemented in practice. Focussing on provenance and uninitialised values, we propose a coherent set of choices for a host of design questions, based on discussion with the ISO WG14 C standards committee and previous surveys of C experts. This should also inform design of the LLVM internal language semantics, and it seems that our source-language proposal and the LLVM proposal by Lopes, Hur, et al. can be made compatible.

Our semantics is integrated with the Cerberus semantics for much of the rest of C, with a clean translation of C into a Core intermediate language. Together, the two make C undefined behaviours explicit. Cerberus has a web-interface GUI in which one can explore all the allowed behaviours of small test programs, and which also identifies the clauses of the C standard relevant to typechecking and translating each test. Work-in-progress URL: http://svr-pes20-cerberus.cl.cam.ac.uk/

We also describe detailed proposals to WG14, showing how the semantics can be incorporated into the ISO standard.
—
Videos Filmed & Edited by Bash Films: http://www.BashFilms.com