Re: [RFC] tools/memory-model: Rule out OOTA

[Jonas Oberhauser]

Am 1/7/2025 um 7:47 PM schrieb Paul E. McKenney:
> On Tue, Jan 07, 2025 at 11:09:55AM -0500, Alan Stern wrote:
>
> > (For example, in a presentation to the C++ working group last year, Paul
> > and I didn't try to show how to extend the C++ memory model to exclude
> > OOTA [other than by fiat, as it does now].  Instead we argued that with
> > the existing memory model, no reasonable compiler would ever produce an
> > executable that could exhibit OOTA and so the memory model didn't need
> > to be changed.)
>
> Furthermore, the LKMM design choice was that if a given litmus test was
> flagged as having a data race, anything might happen, including OOTA.

Note that there is no data race in this litmus test.
There is a race condition on plain accesses according to LKMM,
but LKMM also says that this is *not* a data race.

The patch removes the (actually non-existant) race condition by saying 
that a critical section that is protected from having a data race with 
address dependency or rmb/wmb (which LKMM already says works for 
avoiding data races), is in fact also ordered and therefore has no race 
condition either.

As a side effect :), this happens to fix OOTA in general in LKMM.

Best wishes,
  jonas