Messages in this thread | | | Date | Sat, 7 Sep 2019 08:57:06 -0700 | From | "Paul E. McKenney" <> | Subject | Re: [PATCH RFC] tools/memory-model: Fix data race detection for unordered store and load |
| |
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>
Queued and pushed for review and testing, thank you very much!
Thanx, Paul
> --- > > tools/memory-model/linux-kernel.cat | 2 +- > 1 file changed, 1 insertion(+), 1 deletion(-) > > Index: usb-devel/tools/memory-model/linux-kernel.cat > =================================================================== > --- usb-devel.orig/tools/memory-model/linux-kernel.cat > +++ usb-devel/tools/memory-model/linux-kernel.cat > @@ -197,7 +197,7 @@ empty (wr-incoh | rw-incoh | ww-incoh) a > (* Actual races *) > let ww-nonrace = ww-vis & ((Marked * W) | rw-xbstar) & ((W * Marked) | wr-vis) > let ww-race = (pre-race & co) \ ww-nonrace > -let wr-race = (pre-race & (co? ; rf)) \ wr-vis > +let wr-race = (pre-race & (co? ; rf)) \ wr-vis \ rw-xbstar^-1 > let rw-race = (pre-race & fr) \ rw-xbstar > > flag ~empty (ww-race | wr-race | rw-race) as data-race >
| |