Date: Wed, 24 May 2023 09:35:10 +0200
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.
- 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.
In general this problem space concerns all asynchronous execution:
signal handlers, unsequenced expressions and threads.
Thanks
Jₑₙₛ
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.
- 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.
In general this problem space concerns all asynchronous execution:
signal handlers, unsequenced expressions and threads.
Thanks
Jₑₙₛ
-- :: ICube :::::::::::::::::::::::::::::: deputy director :: :: Université de Strasbourg :::::::::::::::::::::: ICPS :: :: INRIA Nancy Grand Est :::::::::::::::::::::::: Camus :: :: :::::::::::::::::::::::::::::::::::: ☎ +33 368854536 :: :: https://icube-icps.unistra.fr/index.php/Jens_Gustedt ::
Received on 2023-05-24 07:35:14