Date: Sat, 10 Oct 2020 14:33:42 +0000
Am Samstag, den 10.10.2020, 16:07 +0200 schrieb Martin Uecker:
> Am Samstag, den 10.10.2020, 13:49 +0200 schrieb Freek Wiedijk via Liaison:
...
>
> > 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
> > therefore these notions would not be needed anymore.
I agree, although I do not see it as a contradiction to
the proposed provenance model. The problem is that
the abstract machine with more information and the
run-time behaviour of a naive machine must be perfectly
compatible. This is sometimes tricky, if you want to
1. optimize based on the extended type information
available in the abstract machine (and which the
compiler may use at compile-time)
2. be compatible with run-time behaviour which may
not have this information
3. and still have simple and reasonable semantics and
not surprising UB or unstable values that contradict
basic mathematical/logical properities one might want
to be able to assume.
Best,
Martin
> Am Samstag, den 10.10.2020, 13:49 +0200 schrieb Freek Wiedijk via Liaison:
...
>
> > 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
> > therefore these notions would not be needed anymore.
I agree, although I do not see it as a contradiction to
the proposed provenance model. The problem is that
the abstract machine with more information and the
run-time behaviour of a naive machine must be perfectly
compatible. This is sometimes tricky, if you want to
1. optimize based on the extended type information
available in the abstract machine (and which the
compiler may use at compile-time)
2. be compatible with run-time behaviour which may
not have this information
3. and still have simple and reasonable semantics and
not surprising UB or unstable values that contradict
basic mathematical/logical properities one might want
to be able to assume.
Best,
Martin
Received on 2020-10-10 09:33:51