* [PATCH RFC] tools/memory-model: Fix data race detection for unordered store and load
@ 2019-09-06 20:57 Alan Stern
2019-09-07 15:57 ` Paul E. McKenney
2019-09-17 11:39 ` Andrea Parri
0 siblings, 2 replies; 4+ messages in thread
From: Alan Stern @ 2019-09-06 20:57 UTC (permalink / raw)
To: LKMM Maintainers -- Akira Yokosawa, Andrea Parri, Boqun Feng,
Daniel Lustig, David Howells, Jade Alglave, Luc Maranget,
Nicholas Piggin, Paul E. McKenney, Peter Zijlstra, Will Deacon
Cc: Kernel development list
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>
---
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
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [PATCH RFC] tools/memory-model: Fix data race detection for unordered store and load
2019-09-06 20:57 [PATCH RFC] tools/memory-model: Fix data race detection for unordered store and load Alan Stern
@ 2019-09-07 15:57 ` Paul E. McKenney
2019-09-17 11:39 ` Andrea Parri
1 sibling, 0 replies; 4+ messages in thread
From: Paul E. McKenney @ 2019-09-07 15:57 UTC (permalink / raw)
To: Alan Stern
Cc: LKMM Maintainers -- Akira Yokosawa, Andrea Parri, Boqun Feng,
Daniel Lustig, David Howells, Jade Alglave, Luc Maranget,
Nicholas Piggin, Paul E. McKenney, Peter Zijlstra, Will Deacon,
Kernel development list
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
>
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [PATCH RFC] tools/memory-model: Fix data race detection for unordered store and load
2019-09-06 20:57 [PATCH RFC] tools/memory-model: Fix data race detection for unordered store and load Alan Stern
2019-09-07 15:57 ` Paul E. McKenney
@ 2019-09-17 11:39 ` Andrea Parri
2019-09-18 17:24 ` Paul E. McKenney
1 sibling, 1 reply; 4+ messages in thread
From: Andrea Parri @ 2019-09-17 11:39 UTC (permalink / raw)
To: Alan Stern
Cc: LKMM Maintainers -- Akira Yokosawa, Boqun Feng, Daniel Lustig,
David Howells, Jade Alglave, Luc Maranget, Nicholas Piggin,
Paul E. McKenney, Peter Zijlstra, Will Deacon,
Kernel development list
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>
Thanks,
Andrea
>
> ---
>
> 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
>
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [PATCH RFC] tools/memory-model: Fix data race detection for unordered store and load
2019-09-17 11:39 ` Andrea Parri
@ 2019-09-18 17:24 ` Paul E. McKenney
0 siblings, 0 replies; 4+ messages in thread
From: Paul E. McKenney @ 2019-09-18 17:24 UTC (permalink / raw)
To: Andrea Parri
Cc: Alan Stern, LKMM Maintainers -- Akira Yokosawa, Boqun Feng,
Daniel Lustig, David Howells, Jade Alglave, Luc Maranget,
Nicholas Piggin, Paul E. McKenney, Peter Zijlstra, Will Deacon,
Kernel development list
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
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2019-09-18 17:24 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-09-06 20:57 [PATCH RFC] tools/memory-model: Fix data race detection for unordered store and load Alan Stern
2019-09-07 15:57 ` Paul E. McKenney
2019-09-17 11:39 ` Andrea Parri
2019-09-18 17:24 ` Paul E. McKenney
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).