Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 11:42 - 12:04 at Sala II - Separation Logic and Memory Semantics Chair(s): Ilya Sergey

The semantics of pointers and memory objects in C has been a vexed question for many years. C values cannot be treated as either purely abstract or purely 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 WG14 standard leaves much of this unclear, and in some respects differs with de facto standard usage — which itself is difficult to investigate.

In this paper we explore the possible source-language semantics for memory objects and pointers, in ISO C and in C as it is used and implemented in practice, focussing especially on pointer provenance. We aim to, as far as possible, reconcile the ISO C standard, mainstream compiler behaviour, and the semantics relied on by the corpus of existing C code. We present two coherent proposals, tracking provenance via integers and not; both address many design questions. We highlight some pros and cons and open questions, and illustrate the discussion with a library of test cases. We make our semantics executable as a test oracle, integrating it with the Cerberus semantics for much of the rest of C, which we have made substantially more complete and robust, and equipped with a web-interface GUI. This allows us to experimentally assess our proposals on those test cases. To assess their viability with respect to larger bodies of C code, we analyse the changes required and the resulting behaviour for a port of FreeBSD to CHERI, a research architecture supporting hardware capabilities, which (roughly speaking) traps on the memory safety violations which our proposals deem undefined behaviour. We also develop a new runtime instrumentation tool to detect possible provenance violations in normal C code, and apply it to some of the SPEC benchmarks. We compare our proposal with a source-language variant of the twin-allocation LLVM semantics proposal of Lee et al. Finally, we describe ongoing interactions with WG14, exploring how our proposals could be incorporated into the ISO standard.

(slides.pdf)1.21MiB

Thu 17 Jan

POPL-2019-Research-Papers
10:36 - 12:04: Research Papers - Separation Logic and Memory Semantics at Sala II
Chair(s): Ilya SergeyYale-NUS College and National University of Singapore
POPL-2019-Research-Papers10:36 - 10:58
Talk
Aleš BizjakAarhus University, Daniel Gratzer, Robbert KrebbersDelft University of Technology, Lars BirkedalAarhus University
Link to publication DOI Media Attached File Attached
POPL-2019-Research-Papers10:58 - 11:20
Talk
José Fragoso SantosImperial College London, Petar MaksimovićImperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Gabriela SampaioImperial College London, UK, Philippa GardnerImperial College London
Link to publication DOI Media Attached File Attached
POPL-2019-Research-Papers11:20 - 11:42
Talk
Alasdair ArmstrongUniversity of Cambridge, Thomas BauereissUniversity of Cambridge, Brian CampbellUniversity of Edinburgh, Alastair ReidArm Ltd, Kathryn E. GrayUniversity of Cambridge, Robert M. NortonUniversity of Cambridge, Prashanth MundkurSRI International, Mark WassellUniversity of Cambridge, Jon FrenchUniversity of Cambridge, Christopher PulteUniversity of Cambridge, Shaked FlurUniversity of Cambridge, Ian StarkThe University of Edinburgh, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Peter SewellUniversity of Cambridge
Link to publication DOI Media Attached File Attached
POPL-2019-Research-Papers11:42 - 12:04
Talk
Kayvan MemarianUniversity of Cambridge, Victor B. F. GomesUniversity of Cambridge, UK, Brooks DavisSRI International, Stephen KellUniversity of Kent, Alexander RichardsonUniversity of Cambridge, Robert N. M. WatsonUniversity of Cambridge, Peter SewellUniversity of Cambridge
Link to publication DOI Media Attached File Attached