Am Mittwoch, dem 24.05.2023 um 09:35 +0200 schrieb Jₑₙₛ Gustedt:
> Hi,
>
> on Wed, 24 May 2023 08:05:21 +0200 you (Martin Uecker via Liaison
> <liaison_at_[hidden]>) wrote:
>
> > Am Mittwoch, dem 24.05.2023 um 07:17 +0200 schrieb Martin Uecker:
> > > Am Dienstag, dem 23.05.2023 um 17:34 -0700 schrieb Hans Boehm:
> > >
> > >
> > >
> > >
> > ...
> > [...]
> > [...]
> > [...]
> > > >
> > > > Agreed. I think any observable behavior that you can count on has
> > > > to strongly happen before all accesses that can participate in a
> > > > data race. But the compiler implications are a bit subtle, since
> > > > the compiler may be able to infer something about concurrent
> > > > execution based on the absence of a data race later in the
> > > > program.
> > >
> > > My expecation is that it is not a problem for any existing compiler,
> > > because they do not explicitely reason about concurrency. Instead,
> > > that the optimizations they do perform should also work for
> > > concurrent programs further restricts what they can do (e.g.
> > > not create sprurious accesses to neighboring data).
> > >
> > > But I think discussing what concrete UB means for concurrent
> > > programs warrants another paper.
>
> Hm, I don't think that this should be separated from the general
> discussion of UB.
>
> > Just some thoughts: The definition of data race is already tied
> > to a concrete definition of having conflicting accesses in two
> > two threads for a actual execution.
>
> And there are already at least two problems with that
>
> - It doesn't say at all what guarantees for side effects in unrelated
> (detached) threads we would be able to make. The current definition
> of UB has it that the whole execution goes down the drain.

This is - in C - not the current definition of UB as it does not
follow from the definition we currently have in the standard.
But it is a common interpretation .

I think it is relatively clear what guarantees for observable behavior
(not side effects) we can make in other threads: Those which happen-before
the operation with UB are guaranteed to happen before.

Or is there another problem you see here?

>
> - Usually you want to have proofs of race freeness of a *program*.
> So this implies the possibility to argue about all executions of a
> program. Perhaps this kind of arguing has no effect on optimization
> (but I'd like to see proof of this) but our execution model also
> serves other purposses than just to regulate optimization.

It certainly makes things simpler, but I think in the context
of C "whole program" is not the most usefull notion. For a system
programming language such as C and C++ usually some parts of the
program are not known to the compiler. I am not aware of any
production compiler that works under the assumption that it can
see and analyze the whole program (and LTO does not change this,
even with LTO some parts are external to the part which is
optimized.) So a semantic notion that only makes sense for whole
programs is not really that interesting anyway and this is also
one reason why I think we need to move away from it.

> In general this problem space concerns all asynchronous execution:
> signal handlers, unsequenced expressions and threads.

I will write down some arguments and I hope I can get
support from you and others. We have plenty of time now for
thinking about such things.

Martin