This is the mail archive of the
mailing list for the GCC project.
Re: C provenance semantics proposal
- From: Jeff Law <law at redhat dot com>
- To: Peter dot Sewell at cl dot cam dot ac dot uk, gcc at gcc dot gnu dot org
- Cc: cl-c-memory-object-model <cl-c-memory-object-model at lists dot cam dot ac dot uk>
- Date: Fri, 12 Apr 2019 08:50:58 -0600
- Subject: Re: C provenance semantics proposal
- References: <CAHWkzRTd-AsOxOckRaDAbyqWQf_tytFACubN9wpi=NG6=ha_jA@mail.gmail.com>
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).
> 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.
> N2364 C provenance semantics: detailed semantics.
> Peter Sewell, Kayvan Memarian, Victor B. F. Gomes.
> This gives a detailed mathematical semantics for the proposal
> 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.