Over the last few years, some of us in the WG14 Memory Object Model study group have explored a range of issues in the C memory object model, focussing especially on pointer provenance semantics. We now have concrete proposals (especially the "PNVI-ae-udi" and "PNVI-plain" alternatives) that seem to handle many subtle cases in reasonable ways, including casts between pointers and integers, and representation-byte accesses to pointer bytes. Much of this is not specific to C; it really relates to the behaviour of compiler alias analysis, and should be largely harmonised between C and C++. It would therefore be very useful to discuss it in detail with the appropriate parts of WG21.
Below are the relevant papers from a recent WG14 meeting, and an additional collection of effective-type and subobject examples (they are phrased w.r.t. C, but the issues about the underlying semantics should be similar for C++).
N2378: C provenance semantics: slides (extracts from N2363), Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, Jens Gustedt, and Martin Uecker.
These slides are the best place to start, introducing some of the key examples and our proposed models for provenance semantics.
N2363: C provenance semantics: examples, Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, Jens Gustedt, and Martin Uecker.
This gives a more detailed collection of examples.
Cerberus web interface, Kayvan Memarian, Victor B. F. Gomes, and Peter Sewell.
This is a web interface to our Cerberus executable C semantics, that lets one interactively explore and visualise the behaviour of small examples in each of the proposed models.
N2362: Moving to a provenance-aware memory object model for C, Jens Gustedt, Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, and Martin Uecker
This gives proposed C standard text diff, corresponding to the ``PNVI-ae-udi'' model developed above. Jens Gustedt is working on an updated version of this, following the April 2019 London WG14 meeting.
N2364: C provenance semantics: detailed semantics (for PNVI-plain, PNVI address-exposed, PNVI address-exposed user-disambiguation, and PVI models), Peter Sewell, Kayvan Memarian, and Victor B. F. Gomes.
This, for the mathematically inclined only, gives precise semantics for the various alternative models.
Effective types:examples (P1796R0), Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, Jens Gustedt, and Hubert Tong
This is a collection of examples exploring the semantics that should be allowed for objects and subobjects in allocated regions -- especially, where the defined/undefined-behaviour boundary should be.
Related, Paul McKenney, Maged Michael, and others have recently observed that the ISO C specification that ``all pointers to an object become indeterminate values at the end of its lifetime'' is incompatible with idioms in widely used concurrent algorithms. Paul is working on an updated paper for WG21 Cologne.