On Fri, 12 Apr 2019 at 15:51, Jeff Law wrote:
>
> 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.
Indeed. We talked with him at the GNU cauldron, without uncovering
any serious problems, but more detailed review from an implementability
point of view would be great. For the UB mailing list we just made
a brief plain-text summary of the proposal (leaving out all the examples
and standards diff, and glossing over some details). I'll paste that
in below in case it's helpful. The next WG14 meeting is the week of
April 29; comments before then would be particularly useful if that's possible.
best,
Peter
C pointer values are typically represented at runtime as simple
concrete numeric values, but mainstream compilers routinely exploit
information about the "provenance" of pointers to reason that they
cannot alias, and hence to justify optimisations. This is
long-standing practice, but exactly what it means (what programmers
can rely on, and what provenance-based alias analysis is allowed to
do), has never been nailed down. That's what the proposal does.
The basic idea is to associate a *provenance* with every pointer
value, identifying the original storage instance (or allocation, in
other words) that the pointer is derived from. In more detail:
- We take abstract-machine pointer values to be pairs (pi,a), adding a
provenance pi, either @i where i is a storage instance ID, or the
*empty* provenance, to their concrete address a.
- On every storage instance creation (of objects with static, thread,
automatic, and allocated storage duration), the abstract machine
nondeterministically chooses a fresh storage instance ID i (unique
across the entire execution), and the resulting pointer value
carries that single storage instance ID as its provenance @i.
- Provenance is preserved by pointer arithmetic that adds or subtracts
an integer to a pointer.
- At any access via a pointer value, its numeric address must be
consistent with its provenance, with undefined behaviour
otherwise. In particular:
-- access via a pointer value which has provenance a single storage
instance ID @i mu
