C provenance semantics: examples

Peter Sewell 1 Kayvan Memarian 1 Victor Gomes 1 Jens Gustedt 2 Martin Uecker 3
2 CAMUS - Compilation pour les Architectures MUlti-coeurS
Inria Nancy - Grand Est, ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
Abstract : This note discusses the design of provenance semantics for C, looking at a series of examples. We consider three variants of the provenance-not-via-integer (PNVI) model: PNVI plain, PNVI address-exposed (PNVI-ae) and PNVI address-exposed user-disambiguation (PNVI-ae-udi), and also the provenance-via-integers (PVI) model. The examples include those of Exploring C Semantics and Pointer Provenance [POPL 2019] (also available as ISO WG14 N2311 http://www.open-std.org/jtc1/sc22/wg14/ www/docs/n2311.pdf), with several additions. This is based on recent discussion in the C memory object model study group. It should be read together with the two companion notes, one giving detailed diffs to the C standard text (N2362), and another giving detailed semantics for these variants (N2364).
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/hal-02089907
Contributor : Jens Gustedt <>
Submitted on : Thursday, April 4, 2019 - 11:47:08 AM
Last modification on : Friday, April 5, 2019 - 1:24:33 AM
Long-term archiving on : Friday, July 5, 2019 - 1:19:05 PM

File

n2363.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02089907, version 1

Citation

Peter Sewell, Kayvan Memarian, Victor Gomes, Jens Gustedt, Martin Uecker. C provenance semantics: examples. [Technical Report] N2363, ISO JCT1/SC22/WG14. 2019. ⟨hal-02089907⟩

Share

Metrics

Record views

60

Files downloads

330