Freek, all,

On Sat, 10 Oct 2020 at 12:50, Freek Wiedijk via Liaison <
liaison_at_[hidden]> wrote:

> Dear all,
>
> This seems to be the DR451 discussion about "wobbly values"
> all over again.
>
> I think that having a memory model decorated with effective
> types, provenance, wobbliness, and what other decorations
> one can invent, is not the most elegant approach. I'm all
> for Peter's attempt to get the C standard precise (it
> currently isn't), and very much want to support him in this.
> But I don't like the specific proposal of the provenance
> study group. I think it's much too hacky.
>
> I would expect that having a two layer model, in which
> one has an abstract memory model (where values are typed
> and abstract, and in which "uninitialized" is one of the
> possible values, with undefined behavior if you want to
> use it) and a concrete memory model (in which the values
> consists of "object representations", i.e., of a sequences
> of bytes) has much more potential. In such a model those
> two layers should be updated simultaneously and be kept in
> sync all the time, where one side of the model model can
> use information from the other side if it needs it.
>
> Then the effective types, provenance, wobbly values, etc.,
> would just be that the abstract model has precedence,
> and the concrete memory model only comes into play if
> the abstract model doesn't have enough information, and
>

Stepping back, there are several memory-object-model aspects
of the existing specs that need attention, including per-object provenance,
subobject provenance, uninitialised values, padding bytes, and effective
types.
They are inter-related, but it's not been practical to address all of them
simultaneously - we tried that, but there are just too many issues, and not
enough
committee bandwidth. You will remember well that even the model
in Robbert's thesis, which doesn't handle all these in a way that would
work
for ISO C, is pretty complicated... The current proposal is therefore
focussed
only on the first - per-object provenance. It's not attempting to address
uninitialised values or subobject provenance or effective types, and more
work on them
is certainly needed.

For those on the C++ side of this list, you may not have seen that the
per-object
provenance proposal is now written up in this draft Technical Specification
for C,
following the direction approved in principle by WG14 and by the WG21 UB
group:

http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2577.pdf
A Provenance-aware Memory Object Model for C
Jens Gustedt, Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, Martin
Uecker

Within the domain it's addressing, it's doing exactly what Freek suggests:
there is some abstract state, recording provenance info, which "takes
precedence" in the sense that that is what is used for provenance UB
checks, then one falls back to the concrete model when eg reading
a pointer value that has been manipulated bytewise.
Apart from that, it's not maintaining a whole separate abstract state for
abstract values, because in this domain abstract values are completely
determined by the concrete memory + provenance data.
Whether an explicit abstract value state will be desirable or not in the
end,
I'm not sure - but that's really a matter of mathematical style, of how the
model is expressed, rather than of what it is.

best,
Peter




> therefore these notions would not be needed anymore.
>





>
> I think there is a Korean memory model that is a bit like that?
>
> Freek
> _______________________________________________
> Liaison mailing list
> Liaison_at_[hidden]
> Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/liaison
> Link to this post: http://lists.isocpp.org/liaison/2020/10/0209.php
>