Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms

2020-11-06 Thread Boqun Feng
On Fri, Nov 06, 2020 at 10:01:02AM -0800, Paul E. McKenney wrote:
> On Fri, Nov 06, 2020 at 09:47:22AM +0800, Boqun Feng wrote:
> > On Thu, Nov 05, 2020 at 02:00:14PM -0800, paul...@kernel.org wrote:
> > > From: "Paul E. McKenney" 
> > > 
> > > Signed-off-by: Paul E. McKenney 
> > > ---
> > >  tools/memory-model/Documentation/glossary.txt | 155 
> > > ++
> > >  1 file changed, 155 insertions(+)
> > >  create mode 100644 tools/memory-model/Documentation/glossary.txt
> > > 
> > > diff --git a/tools/memory-model/Documentation/glossary.txt 
> > > b/tools/memory-model/Documentation/glossary.txt
> > > new file mode 100644
> > > index 000..036fa28
> > > --- /dev/null
> > > +++ b/tools/memory-model/Documentation/glossary.txt
> > > @@ -0,0 +1,155 @@
> > > +This document contains brief definitions of LKMM-related terms.  Like 
> > > most
> > > +glossaries, it is not intended to be read front to back (except perhaps
> > > +as a way of confirming a diagnosis of OCD), but rather to be searched
> > > +for specific terms.
> > > +
> > > +
> > > +Address Dependency:  When the address of a later memory access is 
> > > computed
> > > + based on the value returned by an earlier load, an "address
> > > + dependency" extends from that load extending to the later access.
> > > + Address dependencies are quite common in RCU read-side critical
> > > + sections:
> > > +
> > > +  1 rcu_read_lock();
> > > +  2 p = rcu_dereference(gp);
> > > +  3 do_something(p->a);
> > > +  4 rcu_read_unlock();
> > > +
> > > +  In this case, because the address of "p->a" on line 3 is computed
> > > +  from the value returned by the rcu_dereference() on line 2, the
> > > +  address dependency extends from that rcu_dereference() to that
> > > +  "p->a".  In rare cases, optimizing compilers can destroy address
> > > +  dependencies.  Please see Documentation/RCU/rcu_dereference.txt
> > > +  for more information.
> > > +
> > > +  See also "Control Dependency".
> > > +
> > > +Acquire:  With respect to a lock, acquiring that lock, for example,
> > > + using spin_lock().  With respect to a non-lock shared variable,
> > > + a special operation that includes a load and which orders that
> > > + load before later memory references running on that same CPU.
> > > + An example special acquire operation is smp_load_acquire(),
> > > + but atomic_read_acquire() and atomic_xchg_acquire() also include
> > > + acquire loads.
> > > +
> > > + When an acquire load returns the value stored by a release store
> > > + to that same variable, then all operations preceding that store
> > 
> > Change this to:
> > 
> > When an acquire load reads-from a release store
> > 
> > , and put a reference to "Reads-from"? I think this makes the document
> > more consistent in that it makes clear "an acquire load returns the
> > value stored by a release store to the same variable" is not a special
> > case, it's simple a "Reads-from".
> > 
> > > + happen before any operations following that load acquire.
> > 
> > Add a reference to the definition of "happen before" in explanation.txt?
> 
> How about as shown below?  I currently am carrying this as a separate
> commit, but I might merge it into this one later on.
> 

Looks good to me, thanks!

Regards,
Boqun

>   Thanx, Paul
> 
> 
> 
> commit 774a52cd3d80d6b657ae6c14c10bd9fc437068f3
> Author: Paul E. McKenney 
> Date:   Fri Nov 6 09:58:01 2020 -0800
> 
> tools/memory-model: Tie acquire loads to reads-from
> 
> This commit explicitly makes the connection between acquire loads and
> the reads-from relation.  It also adds an entry for happens-before,
> and refers to the corresponding section of explanation.txt.
> 
> Reported-by: Boqun Feng 
> Signed-off-by: Paul E. McKenney 
> 
> diff --git a/tools/memory-model/Documentation/glossary.txt 
> b/tools/memory-model/Documentation/glossary.txt
> index 3924aca..383151b 100644
> --- a/tools/memory-model/Documentation/glossary.txt
> +++ b/tools/memory-model/Documentation/glossary.txt
> @@ -33,10 +33,11 @@ Acquire:  With respect to a lock, acquiring that lock, 
> for example,
>   acquire loads.
>  
>   When an acquire load returns the value stored by a release store
> - to that same variable, then all operations preceding that store
> - happen before any operations following that load acquire.
> + to that same variable, (in other words, the acquire load "reads
> + from" the release store), then all operations preceding that
> + store "happen before" any operations following that load acquire.
>  
> - See also "Relaxed" and "Release".
> + See also "Happens-Before", "Reads-From", "Relaxed", and "Release".
>  
>  Coherence (co):  When one CPU's store to a given variable overwrites
>   either the value from another CPU's store or some later value,
> @@ -102,6 +103,11 @@ Fully Orde

Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms

2020-11-06 Thread Alan Stern
On Fri, Nov 06, 2020 at 01:04:13PM -0800, Paul E. McKenney wrote:
> On Fri, Nov 06, 2020 at 03:40:08PM -0500, Alan Stern wrote:
> > Is it really true that data dependencies are so easily destroyed?  I 
> > would expect that a true "semantic" dependency (i.e., one where the 
> > value written really does vary according to the value read) would be 
> > rather hard to second guess.
> 
> The usual optimizations apply, for but one example:
> 
>   r1 = READ_ONCE(x);
>   WRITE_ONCE(y, (r1 + 1) % MAX_ELEMENTS);
> 
> If MAX_ELEMENTS is 1, so long, data dependency!

Sure, but if MAX_ELEMENTS is 1 then the value written will always be 0 
no matter what value r1 has, so it isn't a semantic dependency.  
Presumably a semantic data dependency would be much more robust.

I wonder if it's worth pointing out this distinction to the reader.

> With pointers, the compiler has fewer optimization opportunities,
> but there are still cases where it can break the dependency.
> Or transform it to a control dependency.

Transforming a data dependency into a control dependency wouldn't make 
any important difference; the hardware would still provide the desired 
ordering.

Alan


Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms

2020-11-06 Thread Paul E. McKenney
On Fri, Nov 06, 2020 at 03:40:08PM -0500, Alan Stern wrote:
> On Fri, Nov 06, 2020 at 11:59:12AM -0800, Paul E. McKenney wrote:
> > On Fri, Nov 06, 2020 at 02:23:51PM -0500, Alan Stern wrote:
> > > On Fri, Nov 06, 2020 at 10:04:46AM -0800, Paul E. McKenney wrote:
> > > > On Fri, Nov 06, 2020 at 11:59:30AM -0500, Alan Stern wrote:
> > > > > > +See also "Control Dependency".
> > > > > 
> > > > > There should also be an entry for "Data Dependency", linked from here
> > > > > and from Control Dependency.
> > > > > 
> > > > > > +Marked Access:  An access to a variable that uses an special 
> > > > > > function or
> > > > > > +   macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
> > > > > 
> > > > > How about "r1 = READ_ONCE(x)"?
> > > > 
> > > > Good catches!  I am planning to squash the commit below into the
> > > > original.  Does that cover it?
> > > 
> > > No, because you didn't add a glossary entry for "Data Dependency" and 
> > > there's no link from "Control Dependency" to "Data Dependency".
> > 
> > Sigh.  I was thinking "entry in the list", and didn't even thing to
> > check for an entry in the glossary as a whole.  With the patch below
> > (on top of the one sent earlier), are we good?
> > 
> > Thanx, Paul
> > 
> > 
> > 
> > commit 5a49c32551e83d30e304d6c3fbb660737ba2654e
> > Author: Paul E. McKenney 
> > Date:   Fri Nov 6 11:57:25 2020 -0800
> > 
> > fixup! tools/memory-model: Add a glossary of LKMM terms
> > 
> > Signed-off-by: Paul E. McKenney 
> > 
> > diff --git a/tools/memory-model/Documentation/glossary.txt 
> > b/tools/memory-model/Documentation/glossary.txt
> > index 471bf13..b2da636 100644
> > --- a/tools/memory-model/Documentation/glossary.txt
> > +++ b/tools/memory-model/Documentation/glossary.txt
> > @@ -64,7 +64,7 @@ Control Dependency:  When a later store's execution 
> > depends on a test
> >  fragile, and can be easily destroyed by optimizing compilers.
> >  Please see control-dependencies.txt for more information.
> >  
> > -See also "Address Dependency".
> > +See also "Address Dependency" and "Data Dependency".
> >  
> >  Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the
> > name suggests.  And in a great many cases, a pair of CPUs is all
> > @@ -85,6 +85,23 @@ Cycle:   Memory-barrier pairing is restricted to a pair 
> > of CPUs, as the
> >  
> > See also "Pairing".
> >  
> > +Data Dependency:  When the data written by a later store is computed based
> > +   on the value returned by an earlier load, a "data dependency"
> > +   extends from that load to that later store.  For example:
> > +
> > +1 r1 = READ_ONCE(x);
> > +2 WRITE_ONCE(y, r1 + 1);
> > +
> > +   In this case, the data dependency extends from the READ_ONCE()
> > +   on line 1 to the WRITE_ONCE() on line 2.  Data dependencies are
> > +   fragile and can be easily destroyed by optimizing compilers.
> > +   Because optimizing compilers put a great deal of effort into
> > +   working out what values integer variables might have, this is
> > +   especially true in cases where the dependency is carried through
> > +   an integer.
> > +
> > +   See also "Address Dependency" and "Control Dependency".
> > +
> >  From-Reads (fr):  When one CPU's store to a given variable happened
> > too late to affect the value returned by another CPU's
> > load from that same variable, there is said to be a from-reads
> 
> Yes, this is better.

Thank you for bearing with me on this!

> Is it really true that data dependencies are so easily destroyed?  I 
> would expect that a true "semantic" dependency (i.e., one where the 
> value written really does vary according to the value read) would be 
> rather hard to second guess.

The usual optimizations apply, for but one example:

r1 = READ_ONCE(x);
WRITE_ONCE(y, (r1 + 1) % MAX_ELEMENTS);

If MAX_ELEMENTS is 1, so long, data dependency!

With pointers, the compiler has fewer optimization opportunities,
but there are still cases where it can break the dependency.
Or transform it to a control dependency.

Thanx, Paul


Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms

2020-11-06 Thread Alan Stern
On Fri, Nov 06, 2020 at 11:59:12AM -0800, Paul E. McKenney wrote:
> On Fri, Nov 06, 2020 at 02:23:51PM -0500, Alan Stern wrote:
> > On Fri, Nov 06, 2020 at 10:04:46AM -0800, Paul E. McKenney wrote:
> > > On Fri, Nov 06, 2020 at 11:59:30AM -0500, Alan Stern wrote:
> > > > > +  See also "Control Dependency".
> > > > 
> > > > There should also be an entry for "Data Dependency", linked from here
> > > > and from Control Dependency.
> > > > 
> > > > > +Marked Access:  An access to a variable that uses an special 
> > > > > function or
> > > > > + macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
> > > > 
> > > > How about "r1 = READ_ONCE(x)"?
> > > 
> > > Good catches!  I am planning to squash the commit below into the
> > > original.  Does that cover it?
> > 
> > No, because you didn't add a glossary entry for "Data Dependency" and 
> > there's no link from "Control Dependency" to "Data Dependency".
> 
> Sigh.  I was thinking "entry in the list", and didn't even thing to
> check for an entry in the glossary as a whole.  With the patch below
> (on top of the one sent earlier), are we good?
> 
>   Thanx, Paul
> 
> 
> 
> commit 5a49c32551e83d30e304d6c3fbb660737ba2654e
> Author: Paul E. McKenney 
> Date:   Fri Nov 6 11:57:25 2020 -0800
> 
> fixup! tools/memory-model: Add a glossary of LKMM terms
> 
> Signed-off-by: Paul E. McKenney 
> 
> diff --git a/tools/memory-model/Documentation/glossary.txt 
> b/tools/memory-model/Documentation/glossary.txt
> index 471bf13..b2da636 100644
> --- a/tools/memory-model/Documentation/glossary.txt
> +++ b/tools/memory-model/Documentation/glossary.txt
> @@ -64,7 +64,7 @@ Control Dependency:  When a later store's execution depends 
> on a test
>fragile, and can be easily destroyed by optimizing compilers.
>Please see control-dependencies.txt for more information.
>  
> -  See also "Address Dependency".
> +  See also "Address Dependency" and "Data Dependency".
>  
>  Cycle:   Memory-barrier pairing is restricted to a pair of CPUs, as the
>   name suggests.  And in a great many cases, a pair of CPUs is all
> @@ -85,6 +85,23 @@ Cycle: Memory-barrier pairing is restricted to a pair 
> of CPUs, as the
>  
>   See also "Pairing".
>  
> +Data Dependency:  When the data written by a later store is computed based
> + on the value returned by an earlier load, a "data dependency"
> + extends from that load to that later store.  For example:
> +
> +  1 r1 = READ_ONCE(x);
> +  2 WRITE_ONCE(y, r1 + 1);
> +
> + In this case, the data dependency extends from the READ_ONCE()
> + on line 1 to the WRITE_ONCE() on line 2.  Data dependencies are
> + fragile and can be easily destroyed by optimizing compilers.
> + Because optimizing compilers put a great deal of effort into
> + working out what values integer variables might have, this is
> + especially true in cases where the dependency is carried through
> + an integer.
> +
> + See also "Address Dependency" and "Control Dependency".
> +
>  From-Reads (fr):  When one CPU's store to a given variable happened
>   too late to affect the value returned by another CPU's
>   load from that same variable, there is said to be a from-reads

Yes, this is better.

Is it really true that data dependencies are so easily destroyed?  I 
would expect that a true "semantic" dependency (i.e., one where the 
value written really does vary according to the value read) would be 
rather hard to second guess.

Alan


Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms

2020-11-06 Thread Paul E. McKenney
On Fri, Nov 06, 2020 at 02:23:51PM -0500, Alan Stern wrote:
> On Fri, Nov 06, 2020 at 10:04:46AM -0800, Paul E. McKenney wrote:
> > On Fri, Nov 06, 2020 at 11:59:30AM -0500, Alan Stern wrote:
> > > > +See also "Control Dependency".
> > > 
> > > There should also be an entry for "Data Dependency", linked from here
> > > and from Control Dependency.
> > > 
> > > > +Marked Access:  An access to a variable that uses an special function 
> > > > or
> > > > +   macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
> > > 
> > > How about "r1 = READ_ONCE(x)"?
> > 
> > Good catches!  I am planning to squash the commit below into the
> > original.  Does that cover it?
> 
> No, because you didn't add a glossary entry for "Data Dependency" and 
> there's no link from "Control Dependency" to "Data Dependency".

Sigh.  I was thinking "entry in the list", and didn't even thing to
check for an entry in the glossary as a whole.  With the patch below
(on top of the one sent earlier), are we good?

Thanx, Paul



commit 5a49c32551e83d30e304d6c3fbb660737ba2654e
Author: Paul E. McKenney 
Date:   Fri Nov 6 11:57:25 2020 -0800

fixup! tools/memory-model: Add a glossary of LKMM terms

Signed-off-by: Paul E. McKenney 

diff --git a/tools/memory-model/Documentation/glossary.txt 
b/tools/memory-model/Documentation/glossary.txt
index 471bf13..b2da636 100644
--- a/tools/memory-model/Documentation/glossary.txt
+++ b/tools/memory-model/Documentation/glossary.txt
@@ -64,7 +64,7 @@ Control Dependency:  When a later store's execution depends 
on a test
 fragile, and can be easily destroyed by optimizing compilers.
 Please see control-dependencies.txt for more information.
 
-See also "Address Dependency".
+See also "Address Dependency" and "Data Dependency".
 
 Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the
name suggests.  And in a great many cases, a pair of CPUs is all
@@ -85,6 +85,23 @@ Cycle:   Memory-barrier pairing is restricted to a pair 
of CPUs, as the
 
See also "Pairing".
 
+Data Dependency:  When the data written by a later store is computed based
+   on the value returned by an earlier load, a "data dependency"
+   extends from that load to that later store.  For example:
+
+1 r1 = READ_ONCE(x);
+2 WRITE_ONCE(y, r1 + 1);
+
+   In this case, the data dependency extends from the READ_ONCE()
+   on line 1 to the WRITE_ONCE() on line 2.  Data dependencies are
+   fragile and can be easily destroyed by optimizing compilers.
+   Because optimizing compilers put a great deal of effort into
+   working out what values integer variables might have, this is
+   especially true in cases where the dependency is carried through
+   an integer.
+
+   See also "Address Dependency" and "Control Dependency".
+
 From-Reads (fr):  When one CPU's store to a given variable happened
too late to affect the value returned by another CPU's
load from that same variable, there is said to be a from-reads


Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms

2020-11-06 Thread Alan Stern
On Fri, Nov 06, 2020 at 10:04:46AM -0800, Paul E. McKenney wrote:
> On Fri, Nov 06, 2020 at 11:59:30AM -0500, Alan Stern wrote:
> > > +  See also "Control Dependency".
> > 
> > There should also be an entry for "Data Dependency", linked from here
> > and from Control Dependency.
> > 
> > > +Marked Access:  An access to a variable that uses an special function or
> > > + macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
> > 
> > How about "r1 = READ_ONCE(x)"?
> 
> Good catches!  I am planning to squash the commit below into the
> original.  Does that cover it?

No, because you didn't add a glossary entry for "Data Dependency" and 
there's no link from "Control Dependency" to "Data Dependency".

Alan

>   Thanx, Paul
> 
> 
> 
> commit 27c694f5a049d3edac1f258b888d02650cec936a
> Author: Paul E. McKenney 
> Date:   Fri Nov 6 10:02:41 2020 -0800
> 
> squash! tools/memory-model: Add a glossary of LKMM terms
> 
> [ paulmck: Apply Alan Stern feedback. ]
> Signed-off-by: Paul E. McKenney 
> 
> diff --git a/tools/memory-model/Documentation/glossary.txt 
> b/tools/memory-model/Documentation/glossary.txt
> index 383151b..471bf13 100644
> --- a/tools/memory-model/Documentation/glossary.txt
> +++ b/tools/memory-model/Documentation/glossary.txt
> @@ -22,7 +22,7 @@ Address Dependency:  When the address of a later memory 
> access is computed
>dependencies.  Please see Documentation/RCU/rcu_dereference.txt
>for more information.
>  
> -  See also "Control Dependency".
> +  See also "Control Dependency" and "Data Dependency".
>  
>  Acquire:  With respect to a lock, acquiring that lock, for example,
>   using spin_lock().  With respect to a non-lock shared variable,
> @@ -109,7 +109,7 @@ Happens-Before (hb): A relation between two accesses in 
> which LKMM
>   section of explanation.txt.
>  
>  Marked Access:  An access to a variable that uses an special function or
> - macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
> + macro such as "r1 = READ_ONCE(x)" or "smp_store_release(&a, 1)".
>  
>   See also "Unmarked Access".
>  


Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms

2020-11-06 Thread Paul E. McKenney
On Fri, Nov 06, 2020 at 11:59:30AM -0500, Alan Stern wrote:
> On Thu, Nov 05, 2020 at 02:00:14PM -0800, paul...@kernel.org wrote:
> > From: "Paul E. McKenney" 
> > 
> > Signed-off-by: Paul E. McKenney 
> > ---
> >  tools/memory-model/Documentation/glossary.txt | 155 
> > ++
> >  1 file changed, 155 insertions(+)
> >  create mode 100644 tools/memory-model/Documentation/glossary.txt
> > 
> > diff --git a/tools/memory-model/Documentation/glossary.txt 
> > b/tools/memory-model/Documentation/glossary.txt
> > new file mode 100644
> > index 000..036fa28
> > --- /dev/null
> > +++ b/tools/memory-model/Documentation/glossary.txt
> > @@ -0,0 +1,155 @@
> > +This document contains brief definitions of LKMM-related terms.  Like most
> > +glossaries, it is not intended to be read front to back (except perhaps
> > +as a way of confirming a diagnosis of OCD), but rather to be searched
> > +for specific terms.
> > +
> > +
> > +Address Dependency:  When the address of a later memory access is computed
> > +   based on the value returned by an earlier load, an "address
> > +   dependency" extends from that load extending to the later access.
> > +   Address dependencies are quite common in RCU read-side critical
> > +   sections:
> > +
> > +1 rcu_read_lock();
> > +2 p = rcu_dereference(gp);
> > +3 do_something(p->a);
> > +4 rcu_read_unlock();
> > +
> > +In this case, because the address of "p->a" on line 3 is computed
> > +from the value returned by the rcu_dereference() on line 2, the
> > +address dependency extends from that rcu_dereference() to that
> > +"p->a".  In rare cases, optimizing compilers can destroy address
> > +dependencies.  Please see Documentation/RCU/rcu_dereference.txt
> > +for more information.
> > +
> > +See also "Control Dependency".
> 
> There should also be an entry for "Data Dependency", linked from here
> and from Control Dependency.
> 
> > +Marked Access:  An access to a variable that uses an special function or
> > +   macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
> 
> How about "r1 = READ_ONCE(x)"?

Good catches!  I am planning to squash the commit below into the
original.  Does that cover it?

Thanx, Paul



commit 27c694f5a049d3edac1f258b888d02650cec936a
Author: Paul E. McKenney 
Date:   Fri Nov 6 10:02:41 2020 -0800

squash! tools/memory-model: Add a glossary of LKMM terms

[ paulmck: Apply Alan Stern feedback. ]
Signed-off-by: Paul E. McKenney 

diff --git a/tools/memory-model/Documentation/glossary.txt 
b/tools/memory-model/Documentation/glossary.txt
index 383151b..471bf13 100644
--- a/tools/memory-model/Documentation/glossary.txt
+++ b/tools/memory-model/Documentation/glossary.txt
@@ -22,7 +22,7 @@ Address Dependency:  When the address of a later memory 
access is computed
 dependencies.  Please see Documentation/RCU/rcu_dereference.txt
 for more information.
 
-See also "Control Dependency".
+See also "Control Dependency" and "Data Dependency".
 
 Acquire:  With respect to a lock, acquiring that lock, for example,
using spin_lock().  With respect to a non-lock shared variable,
@@ -109,7 +109,7 @@ Happens-Before (hb): A relation between two accesses in 
which LKMM
section of explanation.txt.
 
 Marked Access:  An access to a variable that uses an special function or
-   macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".
+   macro such as "r1 = READ_ONCE(x)" or "smp_store_release(&a, 1)".
 
See also "Unmarked Access".
 


Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms

2020-11-06 Thread Paul E. McKenney
On Fri, Nov 06, 2020 at 09:47:22AM +0800, Boqun Feng wrote:
> On Thu, Nov 05, 2020 at 02:00:14PM -0800, paul...@kernel.org wrote:
> > From: "Paul E. McKenney" 
> > 
> > Signed-off-by: Paul E. McKenney 
> > ---
> >  tools/memory-model/Documentation/glossary.txt | 155 
> > ++
> >  1 file changed, 155 insertions(+)
> >  create mode 100644 tools/memory-model/Documentation/glossary.txt
> > 
> > diff --git a/tools/memory-model/Documentation/glossary.txt 
> > b/tools/memory-model/Documentation/glossary.txt
> > new file mode 100644
> > index 000..036fa28
> > --- /dev/null
> > +++ b/tools/memory-model/Documentation/glossary.txt
> > @@ -0,0 +1,155 @@
> > +This document contains brief definitions of LKMM-related terms.  Like most
> > +glossaries, it is not intended to be read front to back (except perhaps
> > +as a way of confirming a diagnosis of OCD), but rather to be searched
> > +for specific terms.
> > +
> > +
> > +Address Dependency:  When the address of a later memory access is computed
> > +   based on the value returned by an earlier load, an "address
> > +   dependency" extends from that load extending to the later access.
> > +   Address dependencies are quite common in RCU read-side critical
> > +   sections:
> > +
> > +1 rcu_read_lock();
> > +2 p = rcu_dereference(gp);
> > +3 do_something(p->a);
> > +4 rcu_read_unlock();
> > +
> > +In this case, because the address of "p->a" on line 3 is computed
> > +from the value returned by the rcu_dereference() on line 2, the
> > +address dependency extends from that rcu_dereference() to that
> > +"p->a".  In rare cases, optimizing compilers can destroy address
> > +dependencies.  Please see Documentation/RCU/rcu_dereference.txt
> > +for more information.
> > +
> > +See also "Control Dependency".
> > +
> > +Acquire:  With respect to a lock, acquiring that lock, for example,
> > +   using spin_lock().  With respect to a non-lock shared variable,
> > +   a special operation that includes a load and which orders that
> > +   load before later memory references running on that same CPU.
> > +   An example special acquire operation is smp_load_acquire(),
> > +   but atomic_read_acquire() and atomic_xchg_acquire() also include
> > +   acquire loads.
> > +
> > +   When an acquire load returns the value stored by a release store
> > +   to that same variable, then all operations preceding that store
> 
> Change this to:
> 
>   When an acquire load reads-from a release store
> 
> , and put a reference to "Reads-from"? I think this makes the document
> more consistent in that it makes clear "an acquire load returns the
> value stored by a release store to the same variable" is not a special
> case, it's simple a "Reads-from".
> 
> > +   happen before any operations following that load acquire.
> 
> Add a reference to the definition of "happen before" in explanation.txt?

How about as shown below?  I currently am carrying this as a separate
commit, but I might merge it into this one later on.

Thanx, Paul



commit 774a52cd3d80d6b657ae6c14c10bd9fc437068f3
Author: Paul E. McKenney 
Date:   Fri Nov 6 09:58:01 2020 -0800

tools/memory-model: Tie acquire loads to reads-from

This commit explicitly makes the connection between acquire loads and
the reads-from relation.  It also adds an entry for happens-before,
and refers to the corresponding section of explanation.txt.

Reported-by: Boqun Feng 
Signed-off-by: Paul E. McKenney 

diff --git a/tools/memory-model/Documentation/glossary.txt 
b/tools/memory-model/Documentation/glossary.txt
index 3924aca..383151b 100644
--- a/tools/memory-model/Documentation/glossary.txt
+++ b/tools/memory-model/Documentation/glossary.txt
@@ -33,10 +33,11 @@ Acquire:  With respect to a lock, acquiring that lock, for 
example,
acquire loads.
 
When an acquire load returns the value stored by a release store
-   to that same variable, then all operations preceding that store
-   happen before any operations following that load acquire.
+   to that same variable, (in other words, the acquire load "reads
+   from" the release store), then all operations preceding that
+   store "happen before" any operations following that load acquire.
 
-   See also "Relaxed" and "Release".
+   See also "Happens-Before", "Reads-From", "Relaxed", and "Release".
 
 Coherence (co):  When one CPU's store to a given variable overwrites
either the value from another CPU's store or some later value,
@@ -102,6 +103,11 @@ Fully Ordered:  An operation such as smp_mb() that orders 
all of
that orders all of its CPU's prior accesses, itself, and
all of its CPU's subsequent accesses.
 
+Happens-Before (hb): A relation between two accesses in which LKMM
+   guarantees the first access

Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms

2020-11-06 Thread Alan Stern
On Thu, Nov 05, 2020 at 02:00:14PM -0800, paul...@kernel.org wrote:
> From: "Paul E. McKenney" 
> 
> Signed-off-by: Paul E. McKenney 
> ---
>  tools/memory-model/Documentation/glossary.txt | 155 
> ++
>  1 file changed, 155 insertions(+)
>  create mode 100644 tools/memory-model/Documentation/glossary.txt
> 
> diff --git a/tools/memory-model/Documentation/glossary.txt 
> b/tools/memory-model/Documentation/glossary.txt
> new file mode 100644
> index 000..036fa28
> --- /dev/null
> +++ b/tools/memory-model/Documentation/glossary.txt
> @@ -0,0 +1,155 @@
> +This document contains brief definitions of LKMM-related terms.  Like most
> +glossaries, it is not intended to be read front to back (except perhaps
> +as a way of confirming a diagnosis of OCD), but rather to be searched
> +for specific terms.
> +
> +
> +Address Dependency:  When the address of a later memory access is computed
> + based on the value returned by an earlier load, an "address
> + dependency" extends from that load extending to the later access.
> + Address dependencies are quite common in RCU read-side critical
> + sections:
> +
> +  1 rcu_read_lock();
> +  2 p = rcu_dereference(gp);
> +  3 do_something(p->a);
> +  4 rcu_read_unlock();
> +
> +  In this case, because the address of "p->a" on line 3 is computed
> +  from the value returned by the rcu_dereference() on line 2, the
> +  address dependency extends from that rcu_dereference() to that
> +  "p->a".  In rare cases, optimizing compilers can destroy address
> +  dependencies.  Please see Documentation/RCU/rcu_dereference.txt
> +  for more information.
> +
> +  See also "Control Dependency".

There should also be an entry for "Data Dependency", linked from here
and from Control Dependency.

> +Marked Access:  An access to a variable that uses an special function or
> + macro such as "r1 = READ_ONCE()" or "smp_store_release(&a, 1)".

How about "r1 = READ_ONCE(x)"?

Alan


Re: [PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms

2020-11-05 Thread Boqun Feng
On Thu, Nov 05, 2020 at 02:00:14PM -0800, paul...@kernel.org wrote:
> From: "Paul E. McKenney" 
> 
> Signed-off-by: Paul E. McKenney 
> ---
>  tools/memory-model/Documentation/glossary.txt | 155 
> ++
>  1 file changed, 155 insertions(+)
>  create mode 100644 tools/memory-model/Documentation/glossary.txt
> 
> diff --git a/tools/memory-model/Documentation/glossary.txt 
> b/tools/memory-model/Documentation/glossary.txt
> new file mode 100644
> index 000..036fa28
> --- /dev/null
> +++ b/tools/memory-model/Documentation/glossary.txt
> @@ -0,0 +1,155 @@
> +This document contains brief definitions of LKMM-related terms.  Like most
> +glossaries, it is not intended to be read front to back (except perhaps
> +as a way of confirming a diagnosis of OCD), but rather to be searched
> +for specific terms.
> +
> +
> +Address Dependency:  When the address of a later memory access is computed
> + based on the value returned by an earlier load, an "address
> + dependency" extends from that load extending to the later access.
> + Address dependencies are quite common in RCU read-side critical
> + sections:
> +
> +  1 rcu_read_lock();
> +  2 p = rcu_dereference(gp);
> +  3 do_something(p->a);
> +  4 rcu_read_unlock();
> +
> +  In this case, because the address of "p->a" on line 3 is computed
> +  from the value returned by the rcu_dereference() on line 2, the
> +  address dependency extends from that rcu_dereference() to that
> +  "p->a".  In rare cases, optimizing compilers can destroy address
> +  dependencies.  Please see Documentation/RCU/rcu_dereference.txt
> +  for more information.
> +
> +  See also "Control Dependency".
> +
> +Acquire:  With respect to a lock, acquiring that lock, for example,
> + using spin_lock().  With respect to a non-lock shared variable,
> + a special operation that includes a load and which orders that
> + load before later memory references running on that same CPU.
> + An example special acquire operation is smp_load_acquire(),
> + but atomic_read_acquire() and atomic_xchg_acquire() also include
> + acquire loads.
> +
> + When an acquire load returns the value stored by a release store
> + to that same variable, then all operations preceding that store

Change this to:

When an acquire load reads-from a release store

, and put a reference to "Reads-from"? I think this makes the document
more consistent in that it makes clear "an acquire load returns the
value stored by a release store to the same variable" is not a special
case, it's simple a "Reads-from".

> + happen before any operations following that load acquire.

Add a reference to the definition of "happen before" in explanation.txt?

Regards,
Boqun

> +
> + See also "Relaxed" and "Release".
> +
[...]


[PATCH memory-model 5/8] tools/memory-model: Add a glossary of LKMM terms

2020-11-05 Thread paulmck
From: "Paul E. McKenney" 

Signed-off-by: Paul E. McKenney 
---
 tools/memory-model/Documentation/glossary.txt | 155 ++
 1 file changed, 155 insertions(+)
 create mode 100644 tools/memory-model/Documentation/glossary.txt

diff --git a/tools/memory-model/Documentation/glossary.txt 
b/tools/memory-model/Documentation/glossary.txt
new file mode 100644
index 000..036fa28
--- /dev/null
+++ b/tools/memory-model/Documentation/glossary.txt
@@ -0,0 +1,155 @@
+This document contains brief definitions of LKMM-related terms.  Like most
+glossaries, it is not intended to be read front to back (except perhaps
+as a way of confirming a diagnosis of OCD), but rather to be searched
+for specific terms.
+
+
+Address Dependency:  When the address of a later memory access is computed
+   based on the value returned by an earlier load, an "address
+   dependency" extends from that load extending to the later access.
+   Address dependencies are quite common in RCU read-side critical
+   sections:
+
+1 rcu_read_lock();
+2 p = rcu_dereference(gp);
+3 do_something(p->a);
+4 rcu_read_unlock();
+
+In this case, because the address of "p->a" on line 3 is computed
+from the value returned by the rcu_dereference() on line 2, the
+address dependency extends from that rcu_dereference() to that
+"p->a".  In rare cases, optimizing compilers can destroy address
+dependencies.  Please see Documentation/RCU/rcu_dereference.txt
+for more information.
+
+See also "Control Dependency".
+
+Acquire:  With respect to a lock, acquiring that lock, for example,
+   using spin_lock().  With respect to a non-lock shared variable,
+   a special operation that includes a load and which orders that
+   load before later memory references running on that same CPU.
+   An example special acquire operation is smp_load_acquire(),
+   but atomic_read_acquire() and atomic_xchg_acquire() also include
+   acquire loads.
+
+   When an acquire load returns the value stored by a release store
+   to that same variable, then all operations preceding that store
+   happen before any operations following that load acquire.
+
+   See also "Relaxed" and "Release".
+
+Coherence (co):  When one CPU's store to a given variable overwrites
+   either the value from another CPU's store or some later value,
+   there is said to be a coherence link from the second CPU to
+   the first.
+
+   It is also possible to have a coherence link within a CPU, which
+   is a "coherence internal" (coi) link.  The term "coherence
+   external" (coe) link is used when it is necessary to exclude
+   the coi case.
+
+   See also "From-reads" and "Reads-from".
+
+Control Dependency:  When a later store's execution depends on a test
+   of a value computed from a value returned by an earlier load,
+   a "control dependency" extends from that load to that store.
+   For example:
+
+1 if (READ_ONCE(x))
+2   WRITE_ONCE(y, 1);
+
+Here, the control dependency extends from the READ_ONCE() on
+line 1 to the WRITE_ONCE() on line 2.  Control dependencies are
+fragile, and can be easily destroyed by optimizing compilers.
+Please see control-dependencies.txt for more information.
+
+See also "Address Dependency".
+
+Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the
+   name suggests.  And in a great many cases, a pair of CPUs is all
+   that is required.  In other cases, the notion of pairing must be
+   extended to additional CPUs, and the result is called a "cycle".
+   In a cycle, each CPU's ordering interacts with that of the next:
+
+   CPU 0CPU 1CPU 2  
+   WRITE_ONCE(x, 1);WRITE_ONCE(y, 1);WRITE_ONCE(z, 1);
+   smp_mb();smp_mb();smp_mb();
+   r0 = READ_ONCE(y);   r1 = READ_ONCE(z);   r2 = READ_ONCE(x);
+
+   CPU 0's smp_mb() interacts with that of CPU 1, which interacts
+   with that of CPU 2, which in turn interacts with that of CPU 0
+   to complete the cycle.  Because of the smp_mb() calls between
+   each pair of memory accesses, the outcome where r0, r1, and r2
+   are all equal to zero is forbidden by LKMM.
+
+   See also "Pairing".
+
+From-Reads (fr):  When one CPU's store to a given variable happened
+   too late to affect the value returned by another CPU's
+   load from that same variable, there is said to be a from-reads
+   link from the load to the store.
+
+   It is also possible to have a from-reads link within a CPU, which
+   is a "from-reads internal" (fri) link.  The term "from-reads
+   external" (fre) link is used when it is necessary to exclude
+   the fri case.
+
+   See also "Coherence" and "Reads-from".
+
+Fully Ordered: