Message-ID: <20200302194907.GM2935@paulmck-ThinkPad-P72>
Date:   Mon, 2 Mar 2020 11:49:07 -0800
From:   "Paul E. McKenney" <paulmck@...nel.org>
To:     Andrea Parri <parri.andrea@...il.com>
Cc:     Marco Elver <elver@...gle.com>, linux-kernel@...r.kernel.org,
        kasan-dev@...glegroups.com, stern@...land.harvard.edu,
        will@...nel.org, peterz@...radead.org, boqun.feng@...il.com,
        npiggin@...il.com, dhowells@...hat.com, j.alglave@....ac.uk,
        luc.maranget@...ia.fr, akiyks@...il.com, dlustig@...dia.com,
        joel@...lfernandes.org, linux-arch@...r.kernel.org
Subject: Re: [PATCH v3] tools/memory-model/Documentation: Fix "conflict"
 definition

On Mon, Mar 02, 2020 at 07:52:16PM +0100, Andrea Parri wrote:
> On Mon, Mar 02, 2020 at 06:21:01PM +0100, Marco Elver wrote:
> > The definition of "conflict" should not include the type of access nor
> > whether the accesses are concurrent or not, which this patch addresses.
> > The definition of "data race" remains unchanged.
> > 
> > The definition of "conflict" as we know it and is cited by various
> > papers on memory consistency models appeared in [1]: "Two accesses to
> > the same variable conflict if at least one is a write; two operations
> > conflict if they execute conflicting accesses."
> > 
> > The LKMM as well as the C11 memory model are adaptations of
> > data-race-free, which are based on the work in [2]. Necessarily, we need
> > both conflicting data operations (plain) and synchronization operations
> > (marked). For example, C11's definition is based on [3], which defines a
> > "data race" as: "Two memory operations conflict if they access the same
> > memory location, and at least one of them is a store, atomic store, or
> > atomic read-modify-write operation. In a sequentially consistent
> > execution, two memory operations from different threads form a type 1
> > data race if they conflict, at least one of them is a data operation,
> > and they are adjacent in <T (i.e., they may be executed concurrently)."
> > 
> > [1] D. Shasha, M. Snir, "Efficient and Correct Execution of Parallel
> >     Programs that Share Memory", 1988.
> > 	URL: http://snir.cs.illinois.edu/listed/J21.pdf
> > 
> > [2] S. Adve, "Designing Memory Consistency Models for Shared-Memory
> >     Multiprocessors", 1993.
> > 	URL: http://sadve.cs.illinois.edu/Publications/thesis.pdf
> > 
> > [3] H.-J. Boehm, S. Adve, "Foundations of the C++ Concurrency Memory
> >     Model", 2008.
> > 	URL: https://www.hpl.hp.com/techreports/2008/HPL-2008-56.pdf
> > 
> > Signed-off-by: Marco Elver <elver@...gle.com>
> > Co-developed-by: Alan Stern <stern@...land.harvard.edu>
> > Signed-off-by: Alan Stern <stern@...land.harvard.edu>
> 
> LGTM:
> 
> Acked-by: Andrea Parri <parri.andrea@...il.com>

Applied, and thank you as well!

							Thanx, Paul

> Thank you both,
> 
>   Andrea
> 
> 
> > ---
> > v3:
> > * Apply Alan's suggestion.
> > * s/two race candidates/race candidates/
> > 
> > v2: http://lkml.kernel.org/r/20200302141819.40270-1-elver@google.com
> > * Apply Alan's suggested version.
> >   - Move "from different CPUs (or threads)" from "conflict" to "data
> >     race" definition. Update "race candidate" accordingly.
> > * Add citations to commit message.
> > 
> > v1: http://lkml.kernel.org/r/20200228164621.87523-1-elver@google.com
> > ---
> >  .../Documentation/explanation.txt             | 83 ++++++++++---------
> >  1 file changed, 45 insertions(+), 38 deletions(-)
> > 
> > diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> > index e91a2eb19592a..993f800659c6a 100644
> > --- a/tools/memory-model/Documentation/explanation.txt
> > +++ b/tools/memory-model/Documentation/explanation.txt
> > @@ -1987,28 +1987,36 @@ outcome undefined.
> >  
> >  In technical terms, the compiler is allowed to assume that when the
> >  program executes, there will not be any data races.  A "data race"
> > -occurs when two conflicting memory accesses execute concurrently;
> > -two memory accesses "conflict" if:
> > +occurs when there are two memory accesses such that:
> >  
> > -	they access the same location,
> > +1.	they access the same location,
> >  
> > -	they occur on different CPUs (or in different threads on the
> > -	same CPU),
> > +2.	at least one of them is a store,
> >  
> > -	at least one of them is a plain access,
> > +3.	at least one of them is plain,
> >  
> > -	and at least one of them is a store.
> > +4.	they occur on different CPUs (or in different threads on the
> > +	same CPU), and
> >  
> > -The LKMM tries to determine whether a program contains two conflicting
> > -accesses which may execute concurrently; if it does then the LKMM says
> > -there is a potential data race and makes no predictions about the
> > -program's outcome.
> > +5.	they execute concurrently.
> >  
> > -Determining whether two accesses conflict is easy; you can see that
> > -all the concepts involved in the definition above are already part of
> > -the memory model.  The hard part is telling whether they may execute
> > -concurrently.  The LKMM takes a conservative attitude, assuming that
> > -accesses may be concurrent unless it can prove they cannot.
> > +In the literature, two accesses are said to "conflict" if they satisfy
> > +1 and 2 above.  We'll go a little farther and say that two accesses
> > +are "race candidates" if they satisfy 1 - 4.  Thus, whether or not two
> > +race candidates actually do race in a given execution depends on
> > +whether they are concurrent.
> > +
> > +The LKMM tries to determine whether a program contains race candidates
> > +which may execute concurrently; if it does then the LKMM says there is
> > +a potential data race and makes no predictions about the program's
> > +outcome.
> > +
> > +Determining whether two accesses are race candidates is easy; you can
> > +see that all the concepts involved in the definition above are already
> > +part of the memory model.  The hard part is telling whether they may
> > +execute concurrently.  The LKMM takes a conservative attitude,
> > +assuming that accesses may be concurrent unless it can prove they
> > +are not.
> >  
> >  If two memory accesses aren't concurrent then one must execute before
> >  the other.  Therefore the LKMM decides two accesses aren't concurrent
> > @@ -2171,8 +2179,8 @@ again, now using plain accesses for buf:
> >  	}
> >  
> >  This program does not contain a data race.  Although the U and V
> > -accesses conflict, the LKMM can prove they are not concurrent as
> > -follows:
> > +accesses are race candidates, the LKMM can prove they are not
> > +concurrent as follows:
> >  
> >  	The smp_wmb() fence in P0 is both a compiler barrier and a
> >  	cumul-fence.  It guarantees that no matter what hash of
> > @@ -2326,12 +2334,11 @@ could now perform the load of x before the load of ptr (there might be
> >  a control dependency but no address dependency at the machine level).
> >  
> >  Finally, it turns out there is a situation in which a plain write does
> > -not need to be w-post-bounded: when it is separated from the
> > -conflicting access by a fence.  At first glance this may seem
> > -impossible.  After all, to be conflicting the second access has to be
> > -on a different CPU from the first, and fences don't link events on
> > -different CPUs.  Well, normal fences don't -- but rcu-fence can!
> > -Here's an example:
> > +not need to be w-post-bounded: when it is separated from the other
> > +race-candidate access by a fence.  At first glance this may seem
> > +impossible.  After all, to be race candidates the two accesses must
> > +be on different CPUs, and fences don't link events on different CPUs.
> > +Well, normal fences don't -- but rcu-fence can!  Here's an example:
> >  
> >  	int x, y;
> >  
> > @@ -2367,7 +2374,7 @@ concurrent and there is no race, even though P1's plain store to y
> >  isn't w-post-bounded by any marked accesses.
> >  
> >  Putting all this material together yields the following picture.  For
> > -two conflicting stores W and W', where W ->co W', the LKMM says the
> > +race-candidate stores W and W', where W ->co W', the LKMM says the
> >  stores don't race if W can be linked to W' by a
> >  
> >  	w-post-bounded ; vis ; w-pre-bounded
> > @@ -2380,8 +2387,8 @@ sequence, and if W' is plain then they also have to be linked by a
> >  
> >  	w-post-bounded ; vis ; r-pre-bounded
> >  
> > -sequence.  For a conflicting load R and store W, the LKMM says the two
> > -accesses don't race if R can be linked to W by an
> > +sequence.  For race-candidate load R and store W, the LKMM says the
> > +two accesses don't race if R can be linked to W by an
> >  
> >  	r-post-bounded ; xb* ; w-pre-bounded
> >  
> > @@ -2413,20 +2420,20 @@ is, the rules governing the memory subsystem's choice of a store to
> >  satisfy a load request and its determination of where a store will
> >  fall in the coherence order):
> >  
> > -	If R and W conflict and it is possible to link R to W by one
> > -	of the xb* sequences listed above, then W ->rfe R is not
> > -	allowed (i.e., a load cannot read from a store that it
> > +	If R and W are race candidates and it is possible to link R to
> > +	W by one of the xb* sequences listed above, then W ->rfe R is
> > +	not allowed (i.e., a load cannot read from a store that it
> >  	executes before, even if one or both is plain).
> >  
> > -	If W and R conflict and it is possible to link W to R by one
> > -	of the vis sequences listed above, then R ->fre W is not
> > -	allowed (i.e., if a store is visible to a load then the load
> > -	must read from that store or one coherence-after it).
> > +	If W and R are race candidates and it is possible to link W to
> > +	R by one of the vis sequences listed above, then R ->fre W is
> > +	not allowed (i.e., if a store is visible to a load then the
> > +	load must read from that store or one coherence-after it).
> >  
> > -	If W and W' conflict and it is possible to link W to W' by one
> > -	of the vis sequences listed above, then W' ->co W is not
> > -	allowed (i.e., if one store is visible to a second then the
> > -	second must come after the first in the coherence order).
> > +	If W and W' are race candidates and it is possible to link W
> > +	to W' by one of the vis sequences listed above, then W' ->co W
> > +	is not allowed (i.e., if one store is visible to a second then
> > +	the second must come after the first in the coherence order).
> >  
> >  This is the extent to which the LKMM deals with plain accesses.
> >  Perhaps it could say more (for example, plain accesses might
> > -- 
> > 2.25.0.265.gbab2e86ba0-goog
> > 

Powered by blists - more mailing lists