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

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.

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

> 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