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

On Tue, Jan 07, 2025 at 11:09:55AM -0500, Alan Stern wrote:
> On Mon, Jan 06, 2025 at 10:40:03PM +0100, Jonas Oberhauser wrote:
> > The current LKMM allows out-of-thin-air (OOTA), as evidenced in the following
> > example shared on this list a few years ago:
> > 
> >   P0(int *a, int *b, int *x, int *y) {
> >   	int r1;
> > 
> >   	r1 = READ_ONCE(*x);
> >   	smp_rmb();
> >   	if (r1 == 1) {
> >   		*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) {
> >   		*b = *a;
> >   	}
> >   	smp_wmb();
> >   	WRITE_ONCE(*x, 1);
> >   }
> > 
> >   exists b=42
> > 
> > The root cause is an interplay between plain accesses and rw-fences, i.e.,
> > smp_rmb() and smp_wmb(): while smp_rmb() and smp_wmb() provide sufficient
> > ordering for plain accesses to rule out data races, they do not in the current
> > formalization generally actually order the plain accesses, allowing, e.g., the
> > load and stores to *b to proceed in any order even if P1 reads from P0; and in
> > particular, the marked accesses around those plain accesses are also not
> > ordered, which causes this OOTA.
> 
> That's right.  The memory model deliberately tries to avoid placing 
> restrictions on plain accesses, whenever it can.
> 
> In the example above, for instance, I think it's more interesting to ask
> 
> 	exists 0:r1=1 /\ 1:r1=1
> 
> than to concentrate on a and b.
> 
> OOTA is a very difficult subject.  It can be approached only by making 
> the memory model take all sorts of compiler optimizations into account, 
> and doing this for all possible optimizations is not feasible.

Mark Batty and his students believe otherwise, but I am content to let
them make that argument.  As in I agree with you rather than them.  At
least unless and until they make their argument.  ;-)

> (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.

In case there is interest, that presentation may be found here:

https://drive.google.com/file/d/1ZeJlUJfH90S2uf2wRvNXQvM4jNVSlZI8/view?usp=sharing

The most recent version of the working paper may be found here:

https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3064r2.pdf

							Thanx, Paul

> > In this patch, we choose the rather conservative approach of forcing only the
> > order of these marked accesses, specifically, when a marked read r is
> > separated from a plain read r' by an smp_rmb() (or r' has an address
> > dependency on r or is r'), on which a write w' depends, and w' is either plain
> > and seperated by a subsequent write w by an smp_wmb() (or w' is w), then r
> > precedes w in ppo.
> 
> Is this really valid?  In the example above, if there were no other 
> references to a or b in the rest of the program, the compiler could 
> eliminate them entirely.  (Whether the result could count as OOTA is 
> open to question, but that's not the point.)  Is it not possible that a 
> compiler might find other ways to defeat your intentions?
> 
> In any case, my feeling is that memory models for higher languages 
> (i.e., anything above the assembler level) should not try very hard to 
> address the question of OOTA.  And for LKMM, OOTA involving _plain_ 
> accesses is doubly out of bounds.
> 
> Your proposed change seems to add a significant complication to the 
> memory model for a not-very-clear benefit.
> 
> Alan