[PATCH 3/3] tools: memory-model: Improve data-race detection

[PATCH 3/3] tools: memory-model: Improve data-race detection

[Alan Stern]

Herbert Xu recently reported a problem concerning RCU and compiler
barriers.  In the course of discussing the problem, he put forth a
litmus test which illustrated a serious defect in the Linux Kernel
Memory Model's data-race-detection code.

The defect was that the LKMM assumed visibility and executes-before
ordering of plain accesses had to be mediated by marked accesses.  In
Herbert's litmus test this wasn't so, and the LKMM claimed the litmus
test was allowed and contained a data race although neither is true.

In fact, plain accesses can be ordered by fences even in the absence
of marked accesses.  In most cases this doesn't matter, because most
fences only order accesses within a single thread.  But the rcu-fence
relation is different; it can order (and induce visibility between)
accesses in different threads -- events which otherwise might be
concurrent.  This makes it relevant to data-race detection.

This patch makes two changes to the memory model to incorporate the
new insight:

	If a store is separated by a fence from another access,
	the store is necessarily visible to the other access (as
	reflected in the ww-vis and wr-vis relations).  Similarly,
	if a load is separated by a fence from another access then
	the load necessarily executes before the other access (as
	reflected in the rw-xbstar relation).

	If a store is separated by a strong fence from a marked access
	then it is necessarily visible to any access that executes
	after the marked access (as reflected in the ww-vis and wr-vis
	relations).

With these changes, the LKMM gives the desired result for Herbert's
litmus test and other related ones.

Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Reported-by: Herbert Xu <herbert@gondor.apana.org.au>

---


 tools/memory-model/linux-kernel.cat |    8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

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
@@ -181,9 +181,11 @@ let r-post-bounded = (nonrw-fence | ([~N
 	[Marked]
 
 (* Visibility and executes-before for plain accesses *)
-let ww-vis = w-post-bounded ; vis ; w-pre-bounded
-let wr-vis = w-post-bounded ; vis ; r-pre-bounded
-let rw-xbstar = r-post-bounded ; xbstar ; w-pre-bounded
+let ww-vis = fence | (strong-fence ; xbstar ; w-pre-bounded) |
+	(w-post-bounded ; vis ; w-pre-bounded)
+let wr-vis = fence | (strong-fence ; xbstar ; r-pre-bounded) |
+	(w-post-bounded ; vis ; r-pre-bounded)
+let rw-xbstar = fence | (r-post-bounded ; xbstar ; w-pre-bounded)
 
 (* Potential races *)
 let pre-race = ext & ((Plain * M) | ((M \ IW) * Plain))

Re: [PATCH 3/3] tools: memory-model: Improve data-race detection

[Andrea Parri]

On Thu, Jun 20, 2019 at 11:55:58AM -0400, Alan Stern wrote:
> Herbert Xu recently reported a problem concerning RCU and compiler
> barriers.  In the course of discussing the problem, he put forth a
> litmus test which illustrated a serious defect in the Linux Kernel
> Memory Model's data-race-detection code.
> 
> The defect was that the LKMM assumed visibility and executes-before
> ordering of plain accesses had to be mediated by marked accesses.  In
> Herbert's litmus test this wasn't so, and the LKMM claimed the litmus
> test was allowed and contained a data race although neither is true.
> 
> In fact, plain accesses can be ordered by fences even in the absence
> of marked accesses.  In most cases this doesn't matter, because most
> fences only order accesses within a single thread.  But the rcu-fence
> relation is different; it can order (and induce visibility between)
> accesses in different threads -- events which otherwise might be
> concurrent.  This makes it relevant to data-race detection.
> 
> This patch makes two changes to the memory model to incorporate the
> new insight:
> 
> 	If a store is separated by a fence from another access,
> 	the store is necessarily visible to the other access (as
> 	reflected in the ww-vis and wr-vis relations).  Similarly,
> 	if a load is separated by a fence from another access then
> 	the load necessarily executes before the other access (as
> 	reflected in the rw-xbstar relation).
> 
> 	If a store is separated by a strong fence from a marked access
> 	then it is necessarily visible to any access that executes
> 	after the marked access (as reflected in the ww-vis and wr-vis
> 	relations).
> 
> With these changes, the LKMM gives the desired result for Herbert's
> litmus test and other related ones.
> 
> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> Reported-by: Herbert Xu <herbert@gondor.apana.org.au>

For the entire series:

Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>

Two nits, but up to Paul AFAIAC:

 - This is a first time for "tools: memory-model:" in Subject; we were
   kind of converging to "tools/memory-model:"...

 - The report preceded the patch; we might as well reflect this in the
   order of the tags.

Thanks,

  Andrea

Re: [PATCH 3/3] tools: memory-model: Improve data-race detection

[Alan Stern]

On Fri, 21 Jun 2019, Andrea Parri wrote:

> On Thu, Jun 20, 2019 at 11:55:58AM -0400, Alan Stern wrote:
> > Herbert Xu recently reported a problem concerning RCU and compiler
> > barriers.  In the course of discussing the problem, he put forth a
> > litmus test which illustrated a serious defect in the Linux Kernel
> > Memory Model's data-race-detection code.
> > 
> > The defect was that the LKMM assumed visibility and executes-before
> > ordering of plain accesses had to be mediated by marked accesses.  In
> > Herbert's litmus test this wasn't so, and the LKMM claimed the litmus
> > test was allowed and contained a data race although neither is true.
> > 
> > In fact, plain accesses can be ordered by fences even in the absence
> > of marked accesses.  In most cases this doesn't matter, because most
> > fences only order accesses within a single thread.  But the rcu-fence
> > relation is different; it can order (and induce visibility between)
> > accesses in different threads -- events which otherwise might be
> > concurrent.  This makes it relevant to data-race detection.
> > 
> > This patch makes two changes to the memory model to incorporate the
> > new insight:
> > 
> > 	If a store is separated by a fence from another access,
> > 	the store is necessarily visible to the other access (as
> > 	reflected in the ww-vis and wr-vis relations).  Similarly,
> > 	if a load is separated by a fence from another access then
> > 	the load necessarily executes before the other access (as
> > 	reflected in the rw-xbstar relation).
> > 
> > 	If a store is separated by a strong fence from a marked access
> > 	then it is necessarily visible to any access that executes
> > 	after the marked access (as reflected in the ww-vis and wr-vis
> > 	relations).
> > 
> > With these changes, the LKMM gives the desired result for Herbert's
> > litmus test and other related ones.
> > 
> > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > Reported-by: Herbert Xu <herbert@gondor.apana.org.au>
> 
> For the entire series:
> 
> Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
> 
> Two nits, but up to Paul AFAIAC:
> 
>  - This is a first time for "tools: memory-model:" in Subject; we were
>    kind of converging to "tools/memory-model:"...

Yeah, sure.  That's the sort of detail I have a hard time remembering.

>  - The report preceded the patch; we might as well reflect this in the
>    order of the tags.

Either way is okay with me.

Alan

Re: [PATCH 3/3] tools: memory-model: Improve data-race detection

[Paul E. McKenney]

On Fri, Jun 21, 2019 at 10:25:23AM -0400, Alan Stern wrote:
> On Fri, 21 Jun 2019, Andrea Parri wrote:
> 
> > On Thu, Jun 20, 2019 at 11:55:58AM -0400, Alan Stern wrote:
> > > Herbert Xu recently reported a problem concerning RCU and compiler
> > > barriers.  In the course of discussing the problem, he put forth a
> > > litmus test which illustrated a serious defect in the Linux Kernel
> > > Memory Model's data-race-detection code.
> > > 
> > > The defect was that the LKMM assumed visibility and executes-before
> > > ordering of plain accesses had to be mediated by marked accesses.  In
> > > Herbert's litmus test this wasn't so, and the LKMM claimed the litmus
> > > test was allowed and contained a data race although neither is true.
> > > 
> > > In fact, plain accesses can be ordered by fences even in the absence
> > > of marked accesses.  In most cases this doesn't matter, because most
> > > fences only order accesses within a single thread.  But the rcu-fence
> > > relation is different; it can order (and induce visibility between)
> > > accesses in different threads -- events which otherwise might be
> > > concurrent.  This makes it relevant to data-race detection.
> > > 
> > > This patch makes two changes to the memory model to incorporate the
> > > new insight:
> > > 
> > > 	If a store is separated by a fence from another access,
> > > 	the store is necessarily visible to the other access (as
> > > 	reflected in the ww-vis and wr-vis relations).  Similarly,
> > > 	if a load is separated by a fence from another access then
> > > 	the load necessarily executes before the other access (as
> > > 	reflected in the rw-xbstar relation).
> > > 
> > > 	If a store is separated by a strong fence from a marked access
> > > 	then it is necessarily visible to any access that executes
> > > 	after the marked access (as reflected in the ww-vis and wr-vis
> > > 	relations).
> > > 
> > > With these changes, the LKMM gives the desired result for Herbert's
> > > litmus test and other related ones.
> > > 
> > > Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
> > > Reported-by: Herbert Xu <herbert@gondor.apana.org.au>
> > 
> > For the entire series:
> > 
> > Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
> > 
> > Two nits, but up to Paul AFAIAC:
> > 
> >  - This is a first time for "tools: memory-model:" in Subject; we were
> >    kind of converging to "tools/memory-model:"...
> 
> Yeah, sure.  That's the sort of detail I have a hard time remembering.
> 
> >  - The report preceded the patch; we might as well reflect this in the
> >    order of the tags.
> 
> Either way is okay with me.

I applied Andrea's acks and edited as called out above, thank you both!

						Thanx, Paul

Re: [PATCH 3/3] tools: memory-model: Improve data-race detection

[Akira Yokosawa]

Hi Paul and Alan,

On 2019/06/22 8:54, Paul E. McKenney wrote:
> On Fri, Jun 21, 2019 at 10:25:23AM -0400, Alan Stern wrote:
>> On Fri, 21 Jun 2019, Andrea Parri wrote:
>>
>>> On Thu, Jun 20, 2019 at 11:55:58AM -0400, Alan Stern wrote:
>>>> Herbert Xu recently reported a problem concerning RCU and compiler
>>>> barriers.  In the course of discussing the problem, he put forth a
>>>> litmus test which illustrated a serious defect in the Linux Kernel
>>>> Memory Model's data-race-detection code.

I was not involved in the mail thread and wondering what the litmus test
looked like. Some searching of the archive has suggested that Alan presented
a properly formatted test based on Herbert's idea in [1].

[1]: https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/

If this is the case, adding the link (or message id) in the change
log would help people see the circumstances, I suppose.
Paul, can you amend the change log?

I ran herd7 on said litmus test at both "lkmm" and "dev" of -rcu and
confirmed that this patch fixes the result.

So,

Tested-by: Akira Yokosawa <akiyks@gmail.com>

        Thanks, Akira

>>>>
>>>> The defect was that the LKMM assumed visibility and executes-before
>>>> ordering of plain accesses had to be mediated by marked accesses.  In
>>>> Herbert's litmus test this wasn't so, and the LKMM claimed the litmus
>>>> test was allowed and contained a data race although neither is true.
>>>>
>>>> In fact, plain accesses can be ordered by fences even in the absence
>>>> of marked accesses.  In most cases this doesn't matter, because most
>>>> fences only order accesses within a single thread.  But the rcu-fence
>>>> relation is different; it can order (and induce visibility between)
>>>> accesses in different threads -- events which otherwise might be
>>>> concurrent.  This makes it relevant to data-race detection.
>>>>
>>>> This patch makes two changes to the memory model to incorporate the
>>>> new insight:
>>>>
>>>> 	If a store is separated by a fence from another access,
>>>> 	the store is necessarily visible to the other access (as
>>>> 	reflected in the ww-vis and wr-vis relations).  Similarly,
>>>> 	if a load is separated by a fence from another access then
>>>> 	the load necessarily executes before the other access (as
>>>> 	reflected in the rw-xbstar relation).
>>>>
>>>> 	If a store is separated by a strong fence from a marked access
>>>> 	then it is necessarily visible to any access that executes
>>>> 	after the marked access (as reflected in the ww-vis and wr-vis
>>>> 	relations).
>>>>
>>>> With these changes, the LKMM gives the desired result for Herbert's
>>>> litmus test and other related ones.
>>>>
>>>> Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
>>>> Reported-by: Herbert Xu <herbert@gondor.apana.org.au>
>>>
>>> For the entire series:
>>>
>>> Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
>>>
>>> Two nits, but up to Paul AFAIAC:
>>>
>>>  - This is a first time for "tools: memory-model:" in Subject; we were
>>>    kind of converging to "tools/memory-model:"...
>>
>> Yeah, sure.  That's the sort of detail I have a hard time remembering.
>>
>>>  - The report preceded the patch; we might as well reflect this in the
>>>    order of the tags.
>>
>> Either way is okay with me.
> 
> I applied Andrea's acks and edited as called out above, thank you both!
> 
> 						Thanx, Paul
> 

Re: [PATCH 3/3] tools: memory-model: Improve data-race detection

[Alan Stern]

On Sun, 23 Jun 2019, Akira Yokosawa wrote:

> Hi Paul and Alan,
> 
> On 2019/06/22 8:54, Paul E. McKenney wrote:
> > On Fri, Jun 21, 2019 at 10:25:23AM -0400, Alan Stern wrote:
> >> On Fri, 21 Jun 2019, Andrea Parri wrote:
> >>
> >>> On Thu, Jun 20, 2019 at 11:55:58AM -0400, Alan Stern wrote:
> >>>> Herbert Xu recently reported a problem concerning RCU and compiler
> >>>> barriers.  In the course of discussing the problem, he put forth a
> >>>> litmus test which illustrated a serious defect in the Linux Kernel
> >>>> Memory Model's data-race-detection code.
> 
> I was not involved in the mail thread and wondering what the litmus test
> looked like. Some searching of the archive has suggested that Alan presented
> a properly formatted test based on Herbert's idea in [1].
> 
> [1]: https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/

Yes, that's it.  The test is also available at:

https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus

Alan

> If this is the case, adding the link (or message id) in the change
> log would help people see the circumstances, I suppose.
> Paul, can you amend the change log?
> 
> I ran herd7 on said litmus test at both "lkmm" and "dev" of -rcu and
> confirmed that this patch fixes the result.
> 
> So,
> 
> Tested-by: Akira Yokosawa <akiyks@gmail.com>
> 
>         Thanks, Akira

Re: [PATCH 3/3] tools: memory-model: Improve data-race detection

[Paul E. McKenney]

On Sun, Jun 23, 2019 at 11:15:06AM -0400, Alan Stern wrote:
> On Sun, 23 Jun 2019, Akira Yokosawa wrote:
> 
> > Hi Paul and Alan,
> > 
> > On 2019/06/22 8:54, Paul E. McKenney wrote:
> > > On Fri, Jun 21, 2019 at 10:25:23AM -0400, Alan Stern wrote:
> > >> On Fri, 21 Jun 2019, Andrea Parri wrote:
> > >>
> > >>> On Thu, Jun 20, 2019 at 11:55:58AM -0400, Alan Stern wrote:
> > >>>> Herbert Xu recently reported a problem concerning RCU and compiler
> > >>>> barriers.  In the course of discussing the problem, he put forth a
> > >>>> litmus test which illustrated a serious defect in the Linux Kernel
> > >>>> Memory Model's data-race-detection code.
> > 
> > I was not involved in the mail thread and wondering what the litmus test
> > looked like. Some searching of the archive has suggested that Alan presented
> > a properly formatted test based on Herbert's idea in [1].
> > 
> > [1]: https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/
> 
> Yes, that's it.  The test is also available at:
> 
> https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus
> 
> Alan
> 
> > If this is the case, adding the link (or message id) in the change
> > log would help people see the circumstances, I suppose.
> > Paul, can you amend the change log?
> > 
> > I ran herd7 on said litmus test at both "lkmm" and "dev" of -rcu and
> > confirmed that this patch fixes the result.
> > 
> > So,
> > 
> > Tested-by: Akira Yokosawa <akiyks@gmail.com>

Thank you both!  I will apply these changes tomorrow morning, Pacific Time.

							Thanx, Paul

Re: [PATCH 3/3] tools: memory-model: Improve data-race detection

[Paul E. McKenney]

On Sun, Jun 23, 2019 at 09:34:55PM -0700, Paul E. McKenney wrote:
> On Sun, Jun 23, 2019 at 11:15:06AM -0400, Alan Stern wrote:
> > On Sun, 23 Jun 2019, Akira Yokosawa wrote:
> > 
> > > Hi Paul and Alan,
> > > 
> > > On 2019/06/22 8:54, Paul E. McKenney wrote:
> > > > On Fri, Jun 21, 2019 at 10:25:23AM -0400, Alan Stern wrote:
> > > >> On Fri, 21 Jun 2019, Andrea Parri wrote:
> > > >>
> > > >>> On Thu, Jun 20, 2019 at 11:55:58AM -0400, Alan Stern wrote:
> > > >>>> Herbert Xu recently reported a problem concerning RCU and compiler
> > > >>>> barriers.  In the course of discussing the problem, he put forth a
> > > >>>> litmus test which illustrated a serious defect in the Linux Kernel
> > > >>>> Memory Model's data-race-detection code.
> > > 
> > > I was not involved in the mail thread and wondering what the litmus test
> > > looked like. Some searching of the archive has suggested that Alan presented
> > > a properly formatted test based on Herbert's idea in [1].
> > > 
> > > [1]: https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/
> > 
> > Yes, that's it.  The test is also available at:
> > 
> > https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus
> > 
> > Alan
> > 
> > > If this is the case, adding the link (or message id) in the change
> > > log would help people see the circumstances, I suppose.
> > > Paul, can you amend the change log?
> > > 
> > > I ran herd7 on said litmus test at both "lkmm" and "dev" of -rcu and
> > > confirmed that this patch fixes the result.
> > > 
> > > So,
> > > 
> > > Tested-by: Akira Yokosawa <akiyks@gmail.com>
> 
> Thank you both!  I will apply these changes tomorrow morning, Pacific Time.

And done.  Please see below for the updated commit.

							Thanx, Paul

------------------------------------------------------------------------

commit 46a020e9464aff884df56e5fd483134c8801e39f
Author: Alan Stern <stern@rowland.harvard.edu>
Date:   Thu Jun 20 11:55:58 2019 -0400

    tools/memory-model: Improve data-race detection
    
    Herbert Xu recently reported a problem concerning RCU and compiler
    barriers.  In the course of discussing the problem, he put forth a
    litmus test which illustrated a serious defect in the Linux Kernel
    Memory Model's data-race-detection code [1].
    
    The defect was that the LKMM assumed visibility and executes-before
    ordering of plain accesses had to be mediated by marked accesses.  In
    Herbert's litmus test this wasn't so, and the LKMM claimed the litmus
    test was allowed and contained a data race although neither is true.
    
    In fact, plain accesses can be ordered by fences even in the absence
    of marked accesses.  In most cases this doesn't matter, because most
    fences only order accesses within a single thread.  But the rcu-fence
    relation is different; it can order (and induce visibility between)
    accesses in different threads -- events which otherwise might be
    concurrent.  This makes it relevant to data-race detection.
    
    This patch makes two changes to the memory model to incorporate the
    new insight:
    
            If a store is separated by a fence from another access,
            the store is necessarily visible to the other access (as
            reflected in the ww-vis and wr-vis relations).  Similarly,
            if a load is separated by a fence from another access then
            the load necessarily executes before the other access (as
            reflected in the rw-xbstar relation).
    
            If a store is separated by a strong fence from a marked access
            then it is necessarily visible to any access that executes
            after the marked access (as reflected in the ww-vis and wr-vis
            relations).
    
    With these changes, the LKMM gives the desired result for Herbert's
    litmus test and other related ones [2].
    
    [1]     https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/
    
    [2]     https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-1.litmus
            https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus
            https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-3.litmus
            https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-4.litmus
    
    Reported-by: Herbert Xu <herbert@gondor.apana.org.au>
    Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
    Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com>
    Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
    Tested-by: Akira Yokosawa <akiyks@gmail.com>

diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index ca2f4297b4e6..ea2ff4b94074 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -179,9 +179,11 @@ let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ;
 	[Marked]
 
 (* Visibility and executes-before for plain accesses *)
-let ww-vis = w-post-bounded ; vis ; w-pre-bounded
-let wr-vis = w-post-bounded ; vis ; r-pre-bounded
-let rw-xbstar = r-post-bounded ; xbstar ; w-pre-bounded
+let ww-vis = fence | (strong-fence ; xbstar ; w-pre-bounded) |
+	(w-post-bounded ; vis ; w-pre-bounded)
+let wr-vis = fence | (strong-fence ; xbstar ; r-pre-bounded) |
+	(w-post-bounded ; vis ; r-pre-bounded)
+let rw-xbstar = fence | (r-post-bounded ; xbstar ; w-pre-bounded)
 
 (* Potential races *)
 let pre-race = ext & ((Plain * M) | ((M \ IW) * Plain))

Re: [PATCH 3/3] tools: memory-model: Improve data-race detection

[Alan Stern]

On Mon, 24 Jun 2019, Paul E. McKenney wrote:

> On Sun, Jun 23, 2019 at 09:34:55PM -0700, Paul E. McKenney wrote:
> > On Sun, Jun 23, 2019 at 11:15:06AM -0400, Alan Stern wrote:
> > > On Sun, 23 Jun 2019, Akira Yokosawa wrote:
> > > 
> > > > Hi Paul and Alan,
> > > > 
> > > > On 2019/06/22 8:54, Paul E. McKenney wrote:
> > > > > On Fri, Jun 21, 2019 at 10:25:23AM -0400, Alan Stern wrote:
> > > > >> On Fri, 21 Jun 2019, Andrea Parri wrote:
> > > > >>
> > > > >>> On Thu, Jun 20, 2019 at 11:55:58AM -0400, Alan Stern wrote:
> > > > >>>> Herbert Xu recently reported a problem concerning RCU and compiler
> > > > >>>> barriers.  In the course of discussing the problem, he put forth a
> > > > >>>> litmus test which illustrated a serious defect in the Linux Kernel
> > > > >>>> Memory Model's data-race-detection code.
> > > > 
> > > > I was not involved in the mail thread and wondering what the litmus test
> > > > looked like. Some searching of the archive has suggested that Alan presented
> > > > a properly formatted test based on Herbert's idea in [1].
> > > > 
> > > > [1]: https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/
> > > 
> > > Yes, that's it.  The test is also available at:
> > > 
> > > https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus
> > > 
> > > Alan
> > > 
> > > > If this is the case, adding the link (or message id) in the change
> > > > log would help people see the circumstances, I suppose.
> > > > Paul, can you amend the change log?
> > > > 
> > > > I ran herd7 on said litmus test at both "lkmm" and "dev" of -rcu and
> > > > confirmed that this patch fixes the result.
> > > > 
> > > > So,
> > > > 
> > > > Tested-by: Akira Yokosawa <akiyks@gmail.com>
> > 
> > Thank you both!  I will apply these changes tomorrow morning, Pacific Time.
> 
> And done.  Please see below for the updated commit.
> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit 46a020e9464aff884df56e5fd483134c8801e39f
> Author: Alan Stern <stern@rowland.harvard.edu>
> Date:   Thu Jun 20 11:55:58 2019 -0400
> 
>     tools/memory-model: Improve data-race detection
>     
>     Herbert Xu recently reported a problem concerning RCU and compiler
>     barriers.  In the course of discussing the problem, he put forth a
>     litmus test which illustrated a serious defect in the Linux Kernel
>     Memory Model's data-race-detection code [1].
>     
>     The defect was that the LKMM assumed visibility and executes-before
>     ordering of plain accesses had to be mediated by marked accesses.  In
>     Herbert's litmus test this wasn't so, and the LKMM claimed the litmus
>     test was allowed and contained a data race although neither is true.
>     
>     In fact, plain accesses can be ordered by fences even in the absence
>     of marked accesses.  In most cases this doesn't matter, because most
>     fences only order accesses within a single thread.  But the rcu-fence
>     relation is different; it can order (and induce visibility between)
>     accesses in different threads -- events which otherwise might be
>     concurrent.  This makes it relevant to data-race detection.
>     
>     This patch makes two changes to the memory model to incorporate the
>     new insight:
>     
>             If a store is separated by a fence from another access,
>             the store is necessarily visible to the other access (as
>             reflected in the ww-vis and wr-vis relations).  Similarly,
>             if a load is separated by a fence from another access then
>             the load necessarily executes before the other access (as
>             reflected in the rw-xbstar relation).
>     
>             If a store is separated by a strong fence from a marked access
>             then it is necessarily visible to any access that executes
>             after the marked access (as reflected in the ww-vis and wr-vis
>             relations).
>     
>     With these changes, the LKMM gives the desired result for Herbert's
>     litmus test and other related ones [2].
>     
>     [1]     https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/
>     
>     [2]     https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-1.litmus
>             https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus
>             https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-3.litmus
>             https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-4.litmus

Please add:

https://github.com/paulmckrcu/litmus/blob/master/manual/plain/strong-vis.litmus

Alan

Re: [PATCH 3/3] tools: memory-model: Improve data-race detection

[Paul E. McKenney]

On Mon, Jun 24, 2019 at 11:39:23AM -0400, Alan Stern wrote:
> On Mon, 24 Jun 2019, Paul E. McKenney wrote:
> 
> > On Sun, Jun 23, 2019 at 09:34:55PM -0700, Paul E. McKenney wrote:
> > > On Sun, Jun 23, 2019 at 11:15:06AM -0400, Alan Stern wrote:
> > > > On Sun, 23 Jun 2019, Akira Yokosawa wrote:
> > > > 
> > > > > Hi Paul and Alan,
> > > > > 
> > > > > On 2019/06/22 8:54, Paul E. McKenney wrote:
> > > > > > On Fri, Jun 21, 2019 at 10:25:23AM -0400, Alan Stern wrote:
> > > > > >> On Fri, 21 Jun 2019, Andrea Parri wrote:
> > > > > >>
> > > > > >>> On Thu, Jun 20, 2019 at 11:55:58AM -0400, Alan Stern wrote:
> > > > > >>>> Herbert Xu recently reported a problem concerning RCU and compiler
> > > > > >>>> barriers.  In the course of discussing the problem, he put forth a
> > > > > >>>> litmus test which illustrated a serious defect in the Linux Kernel
> > > > > >>>> Memory Model's data-race-detection code.
> > > > > 
> > > > > I was not involved in the mail thread and wondering what the litmus test
> > > > > looked like. Some searching of the archive has suggested that Alan presented
> > > > > a properly formatted test based on Herbert's idea in [1].
> > > > > 
> > > > > [1]: https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/
> > > > 
> > > > Yes, that's it.  The test is also available at:
> > > > 
> > > > https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus
> > > > 
> > > > Alan
> > > > 
> > > > > If this is the case, adding the link (or message id) in the change
> > > > > log would help people see the circumstances, I suppose.
> > > > > Paul, can you amend the change log?
> > > > > 
> > > > > I ran herd7 on said litmus test at both "lkmm" and "dev" of -rcu and
> > > > > confirmed that this patch fixes the result.
> > > > > 
> > > > > So,
> > > > > 
> > > > > Tested-by: Akira Yokosawa <akiyks@gmail.com>
> > > 
> > > Thank you both!  I will apply these changes tomorrow morning, Pacific Time.
> > 
> > And done.  Please see below for the updated commit.
> > 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > commit 46a020e9464aff884df56e5fd483134c8801e39f
> > Author: Alan Stern <stern@rowland.harvard.edu>
> > Date:   Thu Jun 20 11:55:58 2019 -0400
> > 
> >     tools/memory-model: Improve data-race detection
> >     
> >     Herbert Xu recently reported a problem concerning RCU and compiler
> >     barriers.  In the course of discussing the problem, he put forth a
> >     litmus test which illustrated a serious defect in the Linux Kernel
> >     Memory Model's data-race-detection code [1].
> >     
> >     The defect was that the LKMM assumed visibility and executes-before
> >     ordering of plain accesses had to be mediated by marked accesses.  In
> >     Herbert's litmus test this wasn't so, and the LKMM claimed the litmus
> >     test was allowed and contained a data race although neither is true.
> >     
> >     In fact, plain accesses can be ordered by fences even in the absence
> >     of marked accesses.  In most cases this doesn't matter, because most
> >     fences only order accesses within a single thread.  But the rcu-fence
> >     relation is different; it can order (and induce visibility between)
> >     accesses in different threads -- events which otherwise might be
> >     concurrent.  This makes it relevant to data-race detection.
> >     
> >     This patch makes two changes to the memory model to incorporate the
> >     new insight:
> >     
> >             If a store is separated by a fence from another access,
> >             the store is necessarily visible to the other access (as
> >             reflected in the ww-vis and wr-vis relations).  Similarly,
> >             if a load is separated by a fence from another access then
> >             the load necessarily executes before the other access (as
> >             reflected in the rw-xbstar relation).
> >     
> >             If a store is separated by a strong fence from a marked access
> >             then it is necessarily visible to any access that executes
> >             after the marked access (as reflected in the ww-vis and wr-vis
> >             relations).
> >     
> >     With these changes, the LKMM gives the desired result for Herbert's
> >     litmus test and other related ones [2].
> >     
> >     [1]     https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/
> >     
> >     [2]     https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-1.litmus
> >             https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus
> >             https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-3.litmus
> >             https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-4.litmus
> 
> Please add:
> 
> https://github.com/paulmckrcu/litmus/blob/master/manual/plain/strong-vis.litmus

Done, and calling this version final.  Thank you all again!

							Thanx, Paul