This is the mail archive of the gcc@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

Re: C provenance semantics proposal


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


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]