Date: Tue, 23 May 2023 18:49:23 +0200
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.
>
> 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.
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
> 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.
>
> 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.
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
Received on 2023-05-23 16:49:27