Messages in this thread | | | Date | Wed, 18 Sep 2019 10:24:10 -0700 | From | "Paul E. McKenney" <> | Subject | Re: [PATCH RFC] tools/memory-model: Fix data race detection for unordered store and load |
| |
On Tue, Sep 17, 2019 at 01:39:59PM +0200, Andrea Parri wrote: > On Fri, Sep 06, 2019 at 04:57:22PM -0400, Alan Stern wrote: > > Currently the Linux Kernel Memory Model gives an incorrect response > > for the following litmus test: > > > > C plain-WWC > > > > {} > > > > P0(int *x) > > { > > WRITE_ONCE(*x, 2); > > } > > > > P1(int *x, int *y) > > { > > int r1; > > int r2; > > int r3; > > > > r1 = READ_ONCE(*x); > > if (r1 == 2) { > > smp_rmb(); > > r2 = *x; > > } > > smp_rmb(); > > r3 = READ_ONCE(*x); > > WRITE_ONCE(*y, r3 - 1); > > } > > > > P2(int *x, int *y) > > { > > int r4; > > > > r4 = READ_ONCE(*y); > > if (r4 > 0) > > WRITE_ONCE(*x, 1); > > } > > > > exists (x=2 /\ 1:r2=2 /\ 2:r4=1) > > > > The memory model says that the plain read of *x in P1 races with the > > WRITE_ONCE(*x) in P2. > > > > The problem is that we have a write W and a read R related by neither > > fre or rfe, but rather W ->coe W' ->rfe R, where W' is an intermediate > > write (the WRITE_ONCE() in P0). In this situation there is no > > particular ordering between W and R, so either a wr-vis link from W to > > R or an rw-xbstar link from R to W would prove that the accesses > > aren't concurrent. > > > > But the LKMM only looks for a wr-vis link, which is equivalent to > > assuming that W must execute before R. This is not necessarily true > > on non-multicopy-atomic systems, as the WWC pattern demonstrates. > > > > This patch changes the LKMM to accept either a wr-vis or a reverse > > rw-xbstar link as a proof of non-concurrency. > > > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu> > > Acked-by: Andrea Parri <parri.andrea@gmail.com>
Applied, thank you both!
Thanx, Paul
| |