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

["Paul E. McKenney" <paulmck@kernel.org>]

On Wed, Jan 08, 2025 at 06:39:12PM +0100, Jonas Oberhauser wrote:
> 
> 
> 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.

Fair point, no data race is flagged.

On the other hand, Documentation/memory-barriers.txt says the following:

------------------------------------------------------------------------

However, stores are not speculated.  This means that ordering -is- provided
for load-store control dependencies, as in the following example:

	q = READ_ONCE(a);
	if (q) {
		WRITE_ONCE(b, 1);
	}

Control dependencies pair normally with other types of barriers.
That said, please note that neither READ_ONCE() nor WRITE_ONCE()
are optional! Without the READ_ONCE(), the compiler might combine the
load from 'a' with other loads from 'a'.  Without the WRITE_ONCE(),
the compiler might combine the store to 'b' with other stores to 'b'.
Either can result in highly counterintuitive effects on ordering.

------------------------------------------------------------------------

If I change the two plain assignments to use WRITE_ONCE() as required
by memory-barriers.txt, OOTA is avoided:

------------------------------------------------------------------------

C jonas

{}

P0(int *a, int *b, int *x, int *y) {
	int r1;

	r1 = READ_ONCE(*x);
	smp_rmb();
	if (r1 == 1) {
		WRITE_ONCE(*a, *b);
	}
	smp_wmb();
	WRITE_ONCE(*y, 1);
}

P1(int *a, int *b, int *x, int *y) {
	int r1;

	r1 = READ_ONCE(*y);
	smp_rmb();
	if (r1 == 1) {
		WRITE_ONCE(*b, *a);
	}
	smp_wmb();
	WRITE_ONCE(*x, 1);
}

exists b=42

------------------------------------------------------------------------

$ herd7 -conf linux-kernel.cfg /tmp/jonas.litmus
Test jonas Allowed
States 1
[b]=0;
No
Witnesses
Positive: 0 Negative: 3
Condition exists ([b]=42)
Observation jonas Never 0 3
Time jonas 0.01
Hash=39c0c230bd221b2f54fc88be6771372a

------------------------------------------------------------------------

If LKMM is to allow plain assignments in this case, we need to also update
memory-barriers.txt.  I am reluctant to do this because the community
needs to trust plain C-language assignments less rather than more,
especially given that compilers are continuing to become more aggressive.

Yes, in your example, the "if" and the two explicit barriers should
prevent compilers from being too clever, but these sorts of things are
more fragile than one might think given future code changes.

Thoughts?

							Thanx, Paul