Message-ID: <cda52bac-1c59-4c56-b5e2-937f2008a768@huaweicloud.com>
Date: Thu, 9 Jan 2025 19:35:19 +0100
From: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
To: paulmck@...nel.org
Cc: Alan Stern <stern@...land.harvard.edu>, parri.andrea@...il.com,
 will@...nel.org, peterz@...radead.org, boqun.feng@...il.com,
 npiggin@...il.com, dhowells@...hat.com, j.alglave@....ac.uk,
 luc.maranget@...ia.fr, akiyks@...il.com, dlustig@...dia.com,
 joel@...lfernandes.org, urezki@...il.com, quic_neeraju@...cinc.com,
 frederic@...nel.org, linux-kernel@...r.kernel.org, lkmm@...ts.linux.dev,
 hernan.poncedeleon@...weicloud.com
Subject: Re: [RFC] tools/memory-model: Rule out OOTA



Am 1/9/2025 um 6:54 PM schrieb Paul E. McKenney:
> On Wed, Jan 08, 2025 at 08:17:51PM +0100, Jonas Oberhauser wrote:
>>
>>
>> Am 1/8/2025 um 7:09 PM schrieb Paul E. McKenney:
>>> 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:
>>>>>
>>>> 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:
>>
>>
>> I think this direction of inquiry is a bit misleading. There need not be any
>> speculative store at all:
>>
>>
>>
>> P0(int *a, int *b, int *x, int *y) {
>> 	int r1;
>> 	int r2 = 0;
>> 	r1 = READ_ONCE(*x);
>> 	smp_rmb();
>> 	if (r1 == 1) {
>> 		r2 = *b;
>> 	}
>> 	WRITE_ONCE(*a, r2);
>> 	smp_wmb();
>> 	WRITE_ONCE(*y, 1);
>> }
>>
>> P1(int *a, int *b, int *x, int *y) {
>> 	int r1;
>>
>> 	int r2 = 0;
>>
>> 	r1 = READ_ONCE(*y);
>> 	smp_rmb();
>> 	if (r1 == 1) {
>> 		r2 = *a;
>> 	}
>> 	WRITE_ONCE(*b, r2);
>> 	smp_wmb();
>> 	WRITE_ONCE(*x, 1);
>> }
>>
>>
>> The reason that the WRITE_ONCE helps in the speculative store case is that
>> both its ctrl dependency and the wmb provide ordering, which together
>> creates ordering between *x and *y.
> 
> Ah, and that is because LKMM does not enforce control dependencies past
> the end of the "if" statement.  Cute!
> 
> But memory-barriers.txt requires that the WRITE_ONCE() be within the
> "if" statement for control dependencies to exist, so LKMM is in agreement
> with memory-barriers.txt in this case.  So again, if we change this,
> we need to also change memory-barriers.txt.
 > [...]
 > If we want to respect something containing a control dependency to a
 > WRITE_ONCE() not in the body of the "if" statement, we need to make some
 > change to memory-barriers.txt.

I'm not sure what you denotate by *this* in "if we change this", but 
just to clarify, I am not thinking of claiming that there were a 
(semantic) control dependency to WRITE_ONCE(*b, r2) in this example.

There is however a data dependency from r2 = *a to WRITE_ONCE, and I 
would say that there is a semantic data (not control) dependency from r1 
= READ_ONCE(*y) to WRITE_ONCE(*b, r2), too: depending on the value read 
from *y, the value stored to *b will be different. The latter would be 
enough to avoid OOTA according to the mainline LKMM, but currently this 
semantic dependency is not detected by herd7.


I currently can not come up with an example where there would be a 
(semantic) control dependency from a load to a store that is not in the 
arm of an if statement (or a loop / switch of some form with the branch 
depending on the load).


I think the control dependency is just a red herring. It is only there 
to avoid the data race.

In a hypothetical LKMM where reading in a race is not a data race unless 
the data is used (*1), this would also work:


  	unsigned int r1;
  	unsigned int r2 = 0;
  	r1 = READ_ONCE(*x);
  	smp_rmb();
  	r2 = *b;
  	WRITE_ONCE(*a, (~r1 + 1) & r2);
  	smp_wmb();
  	WRITE_ONCE(*y, 1);


Here in case r1 == 0, the value of r2 is not used, so there is a race 
but there would not be data race in the hypothetical LKMM.

This example would also have OOTA under such a hypothetical LKMM, but 
not with my patch, because in the case where r1 == 1,
  READ_ONCE(*x) is seperated by rmb from the load from *b,
    upon which the store to *a depends,
    which itself is seperated by a wmb from the store to WRITE_ONCE(*y,1)
and this would ensure that READ_ONCE(*x) and WRITE_ONCE(*y,1) can not be 
reordered with each other anymore.


(*1= such a definition is not absurd! One needs to allow such races to 
make sequence locks and other similar datastructures well-defined.)


I currently don't know another way than the if-statement to avoid the 
data race in the program(*2) in the current LKMM, so that's why I rely 
on it, but at least conceptually it is orthogonal to the problem.

(*2=we can avoid the data race flag in herd by using filter, and only 
generating the graphs where r1==1 and there is no data race. But that is 
cheating -- the program is not valid under mainline LKMM.)

>> Please do look at the OO
TA graph generated by herd7 for this one, it looks
>> quite amazing.
> 
> Given the way this morning is going, I must take your word for it...

That sounds awful :(
Technical issues?
With any luck, you can test it on arm's herd7 web interface at 
https://developer.arm.com/herd7 (just don't be like me and type all the 
code first and then change the drop-down selector to Linux - that will 
reset the code window...)

Best wishes,
   jonas

Powered by blists - more mailing lists