Am Freitag, den 04.03.2022, 21:14 +0100 schrieb Jens Maurer:
> On 04/03/2022 21.01, Uecker, Martin wrote:
> > Am Freitag, den 04.03.2022, 20:48 +0100 schrieb Jens Maurer:
> > Wasn't there also something specifically about
> > the possible effects on previous observable
> > behavior or do I misremember this?
>
> Yes, there's more in the abstract machine description:
>
> Certain other operations are described in this document as undefined (for example, the effect of
> attempting
> to modify a const object).
> [Note 1 : This document imposes no requirements on the behavior of programs that contain undefined
> behavior.
> — end note]
>
> A conforming implementation executing a well-formed program shall produce the same observable
> behavior as
> one of the possible executions of the corresponding instance of the abstract machine with the same
> program
> and the same input. However, if any such execution contains an undefined operation, this document
> places
> no requirement on the implementation executing that program with that input (not even with regard
> to
> operations preceding the first undefined operation).

Right. My suggestion would be to remove this
and to strengthen the definition to UB so
that previous observable behavior can not
be affected. For I/O this is mostly already
the case because most I/O is done by function
calls and traps can not be moved across them
(clang seems to do this before 3.4.1 or so
and then apparently was fixed).

The remaining cases of interest are volatile
and atomics.

For atomics the paper from Hans seems to imply
that strenghtenen UB is required to prevent
even more out-of-thin-air problems.

For volatile it is very difficult to see that
time-travel is important for optimization
(volatile is either used for I/O or to prevent
optimizations). I would even say that those
optimizations are dangerous (think about a
machine controlled by volatile accesses).


You are of course right that people have
other optimizations in mind when talking
about time travel. But since those do not
affect observable behavior, they can all
be justified by the "as-if" rule without
time travel.


Martin