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-100...@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 <aki...@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 <st...@rowland.harvard.edu> >>>> Reported-by: Herbert Xu <herb...@gondor.apana.org.au> >>> >>> For the entire series: >>> >>> Acked-by: Andrea Parri <andrea.pa...@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 >