Messages in this thread | ![/](/images/icornerl.gif) | | Date | Tue, 24 Jan 2023 16:11:14 +0100 | Subject | Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) | From | Jonas Oberhauser <> |
| |
On 1/24/2023 3:54 PM, Paul E. McKenney wrote: > On Tue, Jan 24, 2023 at 12:09:48PM +0100, Andrea Parri wrote: >>> There is the one below, but I am (1) not sure that I have it right, >>> (2) not immediately certain that the Linux-kernel implementation would >>> forbid it, (3) not immediately sure that it should be forbidden. >>> >>> In the meantime, thoughts? >> As it stands, P0 to completion, then P1 to completion, then P2 to >> completion should meet the "exists" clause; I guess we want "x=1" >> in the clause (or the values of the stores to "x" exchanged). > OK, so I still don't have it right. ;-) > > Make that x=1. I think. >
If it is x=1, why doesn't LKMM forbid it? Because T1:y=1 is read by T1 before the GP, the whole CS is before the GP, i.e.,
srcu_read_unlock(s, r1); ->rcu-order synchronize_srcu(s);
The GP is furthermore po;prop;strong-fence;prop;po ordered before the unlock, which you can shuffle around to get Wx=2 ->prop;po;rcu-order;po ; prop;strong-fence Wx=2 or Wx=2 ->rb Wx=2 which is forbidden because rb is irreflexive.
Right?
jonas
| ![\](/images/icornerr.gif) |