Am Dienstag, dem 23.05.2023 um 17:34 -0700 schrieb Hans Boehm:
>
>
> On Tue, May 23, 2023 at 9:49 AM Martin Uecker via Liaison <liaison_at_[hidden]> wrote:
> > Am Dienstag, dem 23.05.2023 um 18:21 +0200 schrieb Jₑₙₛ Gustedt via Liaison:
> > > Hello,
> > >
> > > on Mon, 22 May 2023 14:52:10 -0700 you (Hans Boehm via Liaison
> > > <liaison_at_[hidden]>) wrote:
> > >
> > > > 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.
> >
> > Concurrent programs certainly may need a bit more clarification.
> >
> > But can you remind me what is the tricky part? Assuming
> > run-time UB can be clearly associated with a specific
> > operation - which in most cases is already the case),
> > answering the question what observable behavior can be
> > affected does not seem to be a major problem.
> >
>
> I was referring specifically to infinite loops. But one would need to make
> a pass through the standard. I think there are other instances that are
> not well-localized.

Ok, thanks. One possibility to localize it is it to make entering the UB.

For C+ I do not know, but for C I do not think there are other cases
of non-localized run-time UB. The wording for unreachable() may
need some tweaking. The wording for memset_explicit could be
strengthened for concrete UB. In fact, without concrete UB
 memset_explicit has very weak semantics.

> >
> > >
> > > Yes, I also have difficulties to understand what the concept would
> > > mean in the case of race conditions. The text in the C standard says
> > >
> > > The execution of a program contains a data race if it contains two
> > > conflicting actions in different threads, at least one of which is
> > > not atomic, and neither happens before the other. Any such data
> > > race results in undefined behavior.
> > >
> > > So a concrete data race is even defined by the absence of ordering,
> > > and for me it is not clear then which side effects can be considered
> > > to have taken place. (E.g there may be side effects that are strictly
> > > ordered with one of the racing accesses, but not with the other.)
> >
> > It is defined in the absence of ordering for two specific actions.
> > Preferably, I would make both these actions have undefined behavior.
> >
> > One has to think a bit about whether this still gives strong
> > enough semantics for all optimizations, but I think it does.
> >
>
> 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.

Martin




> >
> > Martin
> >
> > >
> > > The difference here is that for parallel programs we don't need
> > >
> > > "this execution has so far not met a racing access to data"
> > >
> > > but we need
> > >
> > > "no execution will ever meet a racing access to data".
> >
> > >
> > > Maybe there is the possibility to extend the notion of race condition
> > > to a concrete interpretation, but I don't think that this obvious, and
> > > I also don't think that just a Note as proposed would be sufficient to
> > > clarify this.
> >
> >
> > 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/1192.php