On 4/2/19 2:11 AM, Peter Sewell wrote: > Dear all, > > continuing the discussion from the 2018 GNU Tools Cauldron, we > (the WG14 C memory object model study group) now > have a detailed proposal for pointer provenance semantics, refining > the "provenance not via integers (PNVI)" model presented there. > This will be discussed at the ISO WG14 C standards committee at the > end of April, and comments from the GCC community before then would > be very welcome. The proposal reconciles the needs of existing code > and the behaviour of existing compilers as well as we can, but it doesn't > exactly match any of the latter, so we'd especially like to know whether > it would be feasible to implement - our hope is that it would only require > minor changes. It's presented in three documents: > > N2362 Moving to a provenance-aware memory model for C: proposal for C2x > by the memory object model study group. Jens Gustedt, Peter Sewell, > Kayvan Memarian, Victor B. F. Gomes, Martin Uecker. > This introduces the proposal and gives the proposed change to the standard > text, presented as change-highlighted pages of the standard > (though one might want to read the N2363 examples before going into that). > http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2362.pdf > > N2363 C provenance semantics: examples. > Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, Jens Gustedt, Martin > Uecker. > This explains the proposal and its design choices with discussion of a > series of examples. > http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2363.pdf > > N2364 C provenance semantics: detailed semantics. > Peter Sewell, Kayvan Memarian, Victor B. F. Gomes. > This gives a detailed mathematical semantics for the proposal > http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2364.pdf > > In addition, at http://cerberus.cl.cam.ac.uk/cerberus we provide an > executable version of the semantics, with a web interface that > allows one to explore and visualise the behaviour of small test > programs, stepping through and seeing the abstract-machine > memory state including provenance information. N2363 compares > the results of this for the example programs with gcc, clang, and icc > results, though the tests are really intended as tests of the semantics > rather than compiler tests, so one has to interpret this with care. THanks. I just noticed this came up in EuroLLVM as well. Getting some standards clarity in this space would be good.
Richi is in the best position to cover for GCC, but I suspect he's buried with gcc-9 issues as we approach the upcoming release. Hopefully he'll have time to review this once crunch time has past. I think more than anything sanity checking the proposal's requirements vs what can be reasonably implmemented is most important at this stage. Jeff
