As has been pointed out in some similar discussion, it's a bit tricky to
define precisely what it means to "occur before an operation that has UB".
I suspect we mostly mean "strongly happens before", but that leaves
questions about where UB occurs. If I have

volatile int v;
int j= 1, k = 5;
for (unsigned i = 0; i != 317; i += 14) {
  ++j;
}
for (unsigned i = 0; i != 317; i += 14) {
  ++k;
  v = i;
}

and the compiler merges the two loops, as intended, does that violate the
concrete interpretation? The variable v is (incorrectly) updated, (long)
before the first loop fails to terminate, and thus has UB(?)

And if we do mean something like "strongly happens before", we probably
also need some argument that "important" compiler transformations don't
reorder synchronization operations and UB, though I expect that statement
to be as sound as your existing claims.

We presumably also need to be clear that data races "occur" at both
accesses.

Hans


On Sat, May 20, 2023 at 12:09 AM Martin Uecker via Liaison <
liaison_at_[hidden]> wrote:

> Am Samstag, dem 20.05.2023 um 02:53 +1000 schrieb Andrew Tomazos:
> > On Sat, May 20, 2023 at 1:04 AM Martin Uecker <ma.uecker_at_[hidden]>
> wrote:
> > > Am Samstag, dem 20.05.2023 um 00:53 +1000 schrieb Andrew Tomazos:
> > > > Changing to the concrete interpretation would render numerous
> existing practice compiler optimizations non-conformant as N3128 points out.
> > >
> > > N3128 points out the exact opposite: that we are not aware of
> > > any relevant compiler optimization affected by this. The only
> > > exception we know of are some re-ordering of volatile accesses,
> > > which seem undesirable and dangerous.
> > >
> >
> >
> > That was indeed a misinterpretation of the N3128 claim. The
> concrete interpretation optimizations still have the usual latitude to time
> travel via the as-if rule and change unobservable
> > behaviour prior to the undefined operation - that all optimizations
> have. The claim is that under this usual latitude, almost all of those
> optimizations can be performed without resorting
> > to the more powerful assumption of the abstract interpretation. And
> that an insignificant number of optimizations require changing observable
> behavior prior to undefined operations.
>
> Yes, this summarizes it perfectly.
>
> > Has the "generic argument" supporting the claim in section 3:
> >
> > "In portable C code I/O is performed using function calls of the
> standard library. A compiler can generally not assume that a function
> returns to the caller, because the function could call
> > ‘exit’, ‘abort’, ‘longjmp’, or enter an infinite loop. For this reason,
> it is never allowed for a compiler to use any information derived from an
> operation with potential UB that comes
> > after a function call in a way that could affect observable behavior
> before the function call. Consequently, observable behavior that is
> accessed via function calls (i.e. all except
> > volatile accesses) can not be affected by time-traveling optimizations
> even when using the abstract interpretation. In principle, a compiler could
> use special knowledge about C library
> > functions and use the fact that those functions always return to the
> caller, but we are not aware of any compiler which does this (and it hardly
> seems worthwhile)."
> >
> > been peer-reviewed by a significant number of experts?
> > What is the status of this paper within WG14?
>
> This paper is one of the results that came out of dicussions over
> two years in the UB study group of WG14 and also with various
> external people. But it became public just now, so much broader
> feedback is still desirable. If we missed something imporant
> we would definitely like to know.
>
> The paper was unanimously endorsed by the UB study group and is
> now submitted to WG14 for consideration. WG14 is busy with C23
> so I expect that this will not officially be discussed for a while.
> So nothing will be decided soon, but this is sent here so that
> WG21 is aware of it at an early time and also to get more
> feedback.
>
> >
> > The only way it seems to refute it would be to find a significant
> > number of counter-examples. A counter-example would be an
> > optimized program which admits incorrect observable behaviour
> > prior to an undefined operation being executed.
>
> Yes. We found counter examples for volatile accesses (as discussed
> in the paper), but here the study group has the opinion that the
> such behavior is undesirable, especially since volatile's main use
> is to suppress reordering by optimization. But this is an area
> were more feedback is certainly welcome: Are there programs with
> volatile accesses where specific optimizations around those
> accesses are considered very important?
>
> We also found counter examples where compiler did change observable
> behavior before function calls (where it can not look into)
> based on UB afterwards. This is then a bug because it also affects
> programs where the function terminates the program and then there
> is no UB. For one one compiler we found a historical bug that was
> fixed. For another, we got initial confirmation from the compiler
> team that this is bug.
>
> If anybody knows about compilers that exploit specific knowledge
> about standard library I/O function that they must return to the
> ser and then uses this for optimization, then this would also be
> interesting to know.
>
> >
> > If the claim is verified, then it is hard to imagine a reason why WG21
> wouldn't adopt it also. The concrete interpretation seems strictly better
> if the underlying claim is true. That is,
> > unless there are other benefits of the abstract interpretation beyond
> optimization. N3128 does not seem to point out any.
> >
>
> We are not really aware of other benefits. One might be that
> theoreticians might like it more because it is simpler to
> model that a program has no semantics at all instead of
> having a notion of partial correctness. But I do not think
> this is something which needs to concern us.
>
>
> Martin
>
>
>
>
>
> _______________________________________________
> Liaison mailing list
> Liaison_at_[hidden]
> Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/liaison
> Link to this post: http://lists.isocpp.org/liaison/2023/05/1187.php
>