[PATCH] memory-model: fix cheat sheet typo

[PATCH] memory-model: fix cheat sheet typo

[Paolo Bonzini]

"RWM" should be "RMW", and that's more or less the extent to which I
can claim to change the document. :)  In particular, "Self" is not
documented and the difference between "Self" and "SV" is not clear
to me.

Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>
---
 tools/memory-model/Documentation/cheatsheet.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/memory-model/Documentation/cheatsheet.txt b/tools/memory-model/Documentation/cheatsheet.txt
index 956b1ae4aafb..c0eafdaddfa4 100644
--- a/tools/memory-model/Documentation/cheatsheet.txt
+++ b/tools/memory-model/Documentation/cheatsheet.txt
@@ -1,6 +1,6 @@
                                   Prior Operation     Subsequent Operation
                                   ---------------  ---------------------------
-                               C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
+                               C  Self  R  W  RMW  Self  R  W  DR  DW  RMW  SV
                               --  ----  -  -  ---  ----  -  -  --  --  ---  --
 
 Store, e.g., WRITE_ONCE()            Y                                       Y
-- 
1.8.3.1

Re: [PATCH] memory-model: fix cheat sheet typo

[Paul E. McKenney]

On Mon, Apr 09, 2018 at 06:50:15PM +0200, Paolo Bonzini wrote:
> "RWM" should be "RMW", and that's more or less the extent to which I
> can claim to change the document. :)  In particular, "Self" is not
> documented and the difference between "Self" and "SV" is not clear
> to me.
> 
> Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>

Applied, though without the questions.  ;-)

"Self" is for things like smp_load_acquire() and smp_store_release()
that order themselves against later and earlier accesses, respectively.
This ordering applies to later/earlier access to all variables, not
just the one that smp_load_acquire()/smp_store_release() accessed.
In contrast, things like smp_mb() order only other accesses, not
themselves.  Or at least it is impossible to proves whether or not they
order themselves because they are not separately visible to other CPUs.

"SV" is "same variable", which applies to pretty much anything that
accesses a variable, but not to things like smp_mb() which do not.

Does that help?

							Thanx, Paul

> ---
>  tools/memory-model/Documentation/cheatsheet.txt | 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
> 
> diff --git a/tools/memory-model/Documentation/cheatsheet.txt b/tools/memory-model/Documentation/cheatsheet.txt
> index 956b1ae4aafb..c0eafdaddfa4 100644
> --- a/tools/memory-model/Documentation/cheatsheet.txt
> +++ b/tools/memory-model/Documentation/cheatsheet.txt
> @@ -1,6 +1,6 @@
>                                    Prior Operation     Subsequent Operation
>                                    ---------------  ---------------------------
> -                               C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
> +                               C  Self  R  W  RMW  Self  R  W  DR  DW  RMW  SV
>                                --  ----  -  -  ---  ----  -  -  --  --  ---  --
> 
>  Store, e.g., WRITE_ONCE()            Y                                       Y
> -- 
> 1.8.3.1
> 

Re: [PATCH] memory-model: fix cheat sheet typo

[Paul E. McKenney]

On Mon, Apr 09, 2018 at 11:42:58AM -0700, Paul E. McKenney wrote:
> On Mon, Apr 09, 2018 at 06:50:15PM +0200, Paolo Bonzini wrote:
> > "RWM" should be "RMW", and that's more or less the extent to which I
> > can claim to change the document. :)  In particular, "Self" is not
> > documented and the difference between "Self" and "SV" is not clear
> > to me.
> > 
> > Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>
> 
> Applied, though without the questions.  ;-)
> 
> "Self" is for things like smp_load_acquire() and smp_store_release()
> that order themselves against later and earlier accesses, respectively.
> This ordering applies to later/earlier access to all variables, not
> just the one that smp_load_acquire()/smp_store_release() accessed.
> In contrast, things like smp_mb() order only other accesses, not
> themselves.  Or at least it is impossible to proves whether or not they
> order themselves because they are not separately visible to other CPUs.
> 
> "SV" is "same variable", which applies to pretty much anything that
> accesses a variable, but not to things like smp_mb() which do not.
> 
> Does that help?

On the perhaps naive assumption that silence means assent, how about
the following patch?

							Thanx, Paul

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

commit 818e46e8db6cacb099b8640b7f2945a3151c00ab
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date:   Tue Apr 10 13:24:19 2018 -0700

    tools/memory-order: Improve key for SELF and SV
    
    The key for "SELF" was missing completely and the key for "SV" was
    a bit obtuse.  This commit therefore adds a key for "SELF" and improves
    the one for "SV".
    
    Reported-by: Paolo Bonzini <pbonzini@redhat.com>
    Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

diff --git a/tools/memory-model/Documentation/cheatsheet.txt b/tools/memory-model/Documentation/cheatsheet.txt
index c0eafdaddfa4..d502993ac7d2 100644
--- a/tools/memory-model/Documentation/cheatsheet.txt
+++ b/tools/memory-model/Documentation/cheatsheet.txt
@@ -26,4 +26,5 @@ Key:	C:	Ordering is cumulative
 	DR:	Dependent read (address dependency)
 	DW:	Dependent write (address, data, or control dependency)
 	RMW:	Atomic read-modify-write operation
-	SV	Same-variable access
+	SELF:	Orders self, as opposed to accesses both before and after
+	SV:	Orders later accesses to the same variable

Re: [PATCH] memory-model: fix cheat sheet typo

[Paolo Bonzini]

On 10/04/2018 22:32, Paul E. McKenney wrote:
> On Mon, Apr 09, 2018 at 11:42:58AM -0700, Paul E. McKenney wrote:
>> On Mon, Apr 09, 2018 at 06:50:15PM +0200, Paolo Bonzini wrote:
>>> "RWM" should be "RMW", and that's more or less the extent to which I
>>> can claim to change the document. :)  In particular, "Self" is not
>>> documented and the difference between "Self" and "SV" is not clear
>>> to me.
>>>
>>> Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>
>>
>> Applied, though without the questions.  ;-)
>>
>> "Self" is for things like smp_load_acquire() and smp_store_release()
>> that order themselves against later and earlier accesses, respectively.
>> This ordering applies to later/earlier access to all variables, not
>> just the one that smp_load_acquire()/smp_store_release() accessed.
>> In contrast, things like smp_mb() order only other accesses, not
>> themselves.  Or at least it is impossible to proves whether or not they
>> order themselves because they are not separately visible to other CPUs.
>>
>> "SV" is "same variable", which applies to pretty much anything that
>> accesses a variable, but not to things like smp_mb() which do not.
>>
>> Does that help?
> 
> On the perhaps naive assumption that silence means assent, how about
> the following patch?

Silence meant "I tried thinking of a patch myself, and hadn't come up
yet with a fully satisfactory one"; that's some kind of assent I guess. :)

Your patch is certainly an improvement!

Thanks,

Paolo

> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit 818e46e8db6cacb099b8640b7f2945a3151c00ab
> Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> Date:   Tue Apr 10 13:24:19 2018 -0700
> 
>     tools/memory-order: Improve key for SELF and SV
>     
>     The key for "SELF" was missing completely and the key for "SV" was
>     a bit obtuse.  This commit therefore adds a key for "SELF" and improves
>     the one for "SV".
>     
>     Reported-by: Paolo Bonzini <pbonzini@redhat.com>
>     Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> 
> diff --git a/tools/memory-model/Documentation/cheatsheet.txt b/tools/memory-model/Documentation/cheatsheet.txt
> index c0eafdaddfa4..d502993ac7d2 100644
> --- a/tools/memory-model/Documentation/cheatsheet.txt
> +++ b/tools/memory-model/Documentation/cheatsheet.txt
> @@ -26,4 +26,5 @@ Key:	C:	Ordering is cumulative
>  	DR:	Dependent read (address dependency)
>  	DW:	Dependent write (address, data, or control dependency)
>  	RMW:	Atomic read-modify-write operation
> -	SV	Same-variable access
> +	SELF:	Orders self, as opposed to accesses both before and after
> +	SV:	Orders later accesses to the same variable
> 

Re: [PATCH] memory-model: fix cheat sheet typo

[Paul E. McKenney]

On Tue, Apr 10, 2018 at 11:10:06PM +0200, Paolo Bonzini wrote:
> On 10/04/2018 22:32, Paul E. McKenney wrote:
> > On Mon, Apr 09, 2018 at 11:42:58AM -0700, Paul E. McKenney wrote:
> >> On Mon, Apr 09, 2018 at 06:50:15PM +0200, Paolo Bonzini wrote:
> >>> "RWM" should be "RMW", and that's more or less the extent to which I
> >>> can claim to change the document. :)  In particular, "Self" is not
> >>> documented and the difference between "Self" and "SV" is not clear
> >>> to me.
> >>>
> >>> Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>
> >>
> >> Applied, though without the questions.  ;-)
> >>
> >> "Self" is for things like smp_load_acquire() and smp_store_release()
> >> that order themselves against later and earlier accesses, respectively.
> >> This ordering applies to later/earlier access to all variables, not
> >> just the one that smp_load_acquire()/smp_store_release() accessed.
> >> In contrast, things like smp_mb() order only other accesses, not
> >> themselves.  Or at least it is impossible to proves whether or not they
> >> order themselves because they are not separately visible to other CPUs.
> >>
> >> "SV" is "same variable", which applies to pretty much anything that
> >> accesses a variable, but not to things like smp_mb() which do not.
> >>
> >> Does that help?
> > 
> > On the perhaps naive assumption that silence means assent, how about
> > the following patch?
> 
> Silence meant "I tried thinking of a patch myself, and hadn't come up
> yet with a fully satisfactory one"; that's some kind of assent I guess. :)

;-) ;-) ;-)

> Your patch is certainly an improvement!

Glad it helps, and I have queued it for the next merge window.  Of course,
if a further improvement comes to mind, please do not keep it a secret.  ;-)

							Thanx, Paul

> Thanks,
> 
> Paolo
> 
> > 							Thanx, Paul
> > 
> > ------------------------------------------------------------------------
> > 
> > commit 818e46e8db6cacb099b8640b7f2945a3151c00ab
> > Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > Date:   Tue Apr 10 13:24:19 2018 -0700
> > 
> >     tools/memory-order: Improve key for SELF and SV
> >     
> >     The key for "SELF" was missing completely and the key for "SV" was
> >     a bit obtuse.  This commit therefore adds a key for "SELF" and improves
> >     the one for "SV".
> >     
> >     Reported-by: Paolo Bonzini <pbonzini@redhat.com>
> >     Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > 
> > diff --git a/tools/memory-model/Documentation/cheatsheet.txt b/tools/memory-model/Documentation/cheatsheet.txt
> > index c0eafdaddfa4..d502993ac7d2 100644
> > --- a/tools/memory-model/Documentation/cheatsheet.txt
> > +++ b/tools/memory-model/Documentation/cheatsheet.txt
> > @@ -26,4 +26,5 @@ Key:	C:	Ordering is cumulative
> >  	DR:	Dependent read (address dependency)
> >  	DW:	Dependent write (address, data, or control dependency)
> >  	RMW:	Atomic read-modify-write operation
> > -	SV	Same-variable access
> > +	SELF:	Orders self, as opposed to accesses both before and after
> > +	SV:	Orders later accesses to the same variable
> > 
> 

Re: [PATCH] memory-model: fix cheat sheet typo

[Paolo Bonzini]

On 10/04/2018 23:34, Paul E. McKenney wrote:
> Glad it helps, and I have queued it for the next merge window.  Of course,
> if a further improvement comes to mind, please do not keep it a secret.  ;-)

Yes, there are several changes that could be included:

- SV could be added to the prior operation case as well?  It should be
symmetric

- The *_relaxed() case also applies to void RMW

- smp_store_mb() is missing

- smp_rmb() orders prior reads fully against subsequent RMW because SV
applies between the two parts of the RMW; likewise smp_wmb() orders prior
RMW fully against subsequent writes


I am going submit these changes separately, but before doing that I can show
also my rewrite of the cheat sheet.

The advantage is that, at least to me, it's clearer (and gets rid of
"Self" :)).

The disadvantage is that it's much longer---almost twice the lines, even if
you discount the splitting out of cumulative/propagating to a separate table
(which in turn is because to me it's a different level of black magic).

---------------------
Memory operations are listed in this document as follows:

	R:	Read portion of RMW
	W:	Write portion of RMW
	DR:	Dependent read (address dependency)
	DW:	Dependent write (address, data, or control dependency)
	RMW:	Atomic read-modify-write operation
	SV	Other accesses to the same variable


Memory access operations order other memory operations against themselves as
follows:

                                   Prior Operation   Subsequent Operation
                                   ---------------   ---------------------
                                   R  W  RMW  SV     R  W  DR  DW  RMW  SV
                                   -  -  ---  --     -  -  --  --  ---  --
Store, e.g., WRITE_ONCE()                      Y                         Y
Load, e.g., READ_ONCE()                        Y            Y   Y        Y
Unsuccessful RMW operation                     Y            Y   Y        Y
*_relaxed() or void RMW operation              Y            Y   Y        Y
rcu_dereference()                              Y            Y   Y        Y
Successful *_acquire()                         Y      r  r  r   r    r   Y
Successful *_release()             w  w    w   Y                         Y
smp_store_mb()                     Y  Y    Y   Y      Y  Y   Y   Y   Y   Y
Successful full non-void RMW       Y  Y    Y   Y      Y  Y   Y   Y   Y   Y

Key:	Y:	Memory operation provides ordering
	r:	Cannot move past the read portion of the *_acquire()
	w:	Cannot move past the write portion of the *_release()


Memory barriers order prior memory operations against subsequent memory
operations.  Two operations are ordered if both have non-empty cells in
the following table:

                                   Prior Operation   Subsequent Operation
                                   ---------------   --------------------
                                   R  W  RMW         R  W  DR  DW  RMW
                                   -  -  ---         -  -  --  --  ---
smp_rmb()                          Y      r          Y      Y       Y
smp_wmb()                             Y   Y             Y       Y   w
smp_mb() & synchronize_rcu()       Y  Y   Y          Y  Y   Y   Y   Y
smp_mb__before_atomic()            Y  Y   Y          a  a   a   a   Y
smp_mb__after_atomic()             a  a   Y          Y  Y   Y   Y


Key:	Y:	Barrier provides ordering
	r:	Barrier provides ordering against the read portion of RMW
	w:	Barrier provides ordering against the write portion of RMW
	a:	Barrier provides ordering given intervening RMW atomic operation


Finally the following describes which operations provide cumulative and
propagating fences:

                                     Cumulative         Propagates
                                     ----------         ----------
Store, e.g., WRITE_ONCE()
Load, e.g., READ_ONCE()
Unsuccessful RMW operation
*_relaxed() or void RMW operation
rcu_dereference()
Successful *_acquire()
Successful *_release()                   Y
smp_store_mb()                           Y                  Y
Successful full non-void RMW             Y                  Y
smp_rmb()
smp_wmb()
smp_mb() & synchronize_rcu()             Y                  Y
smp_mb__before_atomic()                  Y                  Y
smp_mb__after_atomic()                   Y                  Y
----------

Perhaps you can see some obvious improvements.  Otherwise I'll send patches
for the above issues.

Thanks,

Paolo

Re: [PATCH] memory-model: fix cheat sheet typo

[Paul E. McKenney]

On Wed, Apr 11, 2018 at 01:15:58PM +0200, Paolo Bonzini wrote:
> On 10/04/2018 23:34, Paul E. McKenney wrote:
> > Glad it helps, and I have queued it for the next merge window.  Of course,
> > if a further improvement comes to mind, please do not keep it a secret.  ;-)
> 
> Yes, there are several changes that could be included:
> 
> - SV could be added to the prior operation case as well?  It should be
> symmetric
> 
> - The *_relaxed() case also applies to void RMW
> 
> - smp_store_mb() is missing
> 
> - smp_rmb() orders prior reads fully against subsequent RMW because SV
> applies between the two parts of the RMW; likewise smp_wmb() orders prior
> RMW fully against subsequent writes
> 
> 
> I am going submit these changes separately, but before doing that I can show
> also my rewrite of the cheat sheet.
> 
> The advantage is that, at least to me, it's clearer (and gets rid of
> "Self" :)).
> 
> The disadvantage is that it's much longer---almost twice the lines, even if
> you discount the splitting out of cumulative/propagating to a separate table
> (which in turn is because to me it's a different level of black magic).
> 
> ---------------------
> Memory operations are listed in this document as follows:
> 
> 	R:	Read portion of RMW
> 	W:	Write portion of RMW
> 	DR:	Dependent read (address dependency)
> 	DW:	Dependent write (address, data, or control dependency)
> 	RMW:	Atomic read-modify-write operation
> 	SV	Other accesses to the same variable
> 
> 
> Memory access operations order other memory operations against themselves as
> follows:
> 
>                                    Prior Operation   Subsequent Operation
>                                    ---------------   ---------------------
>                                    R  W  RMW  SV     R  W  DR  DW  RMW  SV
>                                    -  -  ---  --     -  -  --  --  ---  --
> Store, e.g., WRITE_ONCE()                      Y                         Y
> Load, e.g., READ_ONCE()                        Y            Y   Y        Y
> Unsuccessful RMW operation                     Y            Y   Y        Y
> *_relaxed() or void RMW operation              Y            Y   Y        Y
> rcu_dereference()                              Y            Y   Y        Y
> Successful *_acquire()                         Y      r  r  r   r    r   Y
> Successful *_release()             w  w    w   Y                         Y
> smp_store_mb()                     Y  Y    Y   Y      Y  Y   Y   Y   Y   Y
> Successful full non-void RMW       Y  Y    Y   Y      Y  Y   Y   Y   Y   Y
> 
> Key:	Y:	Memory operation provides ordering
> 	r:	Cannot move past the read portion of the *_acquire()
> 	w:	Cannot move past the write portion of the *_release()
> 
> 
> Memory barriers order prior memory operations against subsequent memory
> operations.  Two operations are ordered if both have non-empty cells in
> the following table:
> 
>                                    Prior Operation   Subsequent Operation
>                                    ---------------   --------------------
>                                    R  W  RMW         R  W  DR  DW  RMW
>                                    -  -  ---         -  -  --  --  ---
> smp_rmb()                          Y      r          Y      Y       Y
> smp_wmb()                             Y   Y             Y       Y   w
> smp_mb() & synchronize_rcu()       Y  Y   Y          Y  Y   Y   Y   Y
> smp_mb__before_atomic()            Y  Y   Y          a  a   a   a   Y
> smp_mb__after_atomic()             a  a   Y          Y  Y   Y   Y
> 
> 
> Key:	Y:	Barrier provides ordering
> 	r:	Barrier provides ordering against the read portion of RMW
> 	w:	Barrier provides ordering against the write portion of RMW
> 	a:	Barrier provides ordering given intervening RMW atomic operation
> 
> 
> Finally the following describes which operations provide cumulative and
> propagating fences:
> 
>                                      Cumulative         Propagates
>                                      ----------         ----------
> Store, e.g., WRITE_ONCE()
> Load, e.g., READ_ONCE()
> Unsuccessful RMW operation
> *_relaxed() or void RMW operation
> rcu_dereference()
> Successful *_acquire()
> Successful *_release()                   Y
> smp_store_mb()                           Y                  Y
> Successful full non-void RMW             Y                  Y
> smp_rmb()
> smp_wmb()
> smp_mb() & synchronize_rcu()             Y                  Y
> smp_mb__before_atomic()                  Y                  Y
> smp_mb__after_atomic()                   Y                  Y
> ----------
> 
> Perhaps you can see some obvious improvements.  Otherwise I'll send patches
> for the above issues.

Splitting it as you have done might indeed have some advantages.  What do
others think?

On the last table, would it make sense to leave out the rows having neither
"Cumulative" nor "Propagates"?

							Thanx, Paul

Re: [PATCH] memory-model: fix cheat sheet typo

[Peter Zijlstra]

On Wed, Apr 11, 2018 at 09:19:56AM -0700, Paul E. McKenney wrote:

> > 
> >                                    Prior Operation   Subsequent Operation
> >                                    ---------------   ---------------------
> >                                    R  W  RMW  SV     R  W  DR  DW  RMW  SV
> >                                    -  -  ---  --     -  -  --  --  ---  --

> > smp_store_mb()                     Y  Y    Y   Y      Y  Y   Y   Y   Y   Y

I'm not sure about that, the generic version of that reads:

include/asm-generic/barrier.h:#define __smp_store_mb(var, value)  do { WRITE_ONCE(var, value); __smp_mb(); } while (0)

Which doesn't not have an smp_mb() before, so it doesn't actually order
prior; or I'm failing to read the table wrong.

Re: [PATCH] memory-model: fix cheat sheet typo

[Paolo Bonzini]

On 11/04/2018 18:31, Peter Zijlstra wrote:
>>>                                    Prior Operation   Subsequent Operation
>>>                                    ---------------   ---------------------
>>>                                    R  W  RMW  SV     R  W  DR  DW  RMW  SV
>>>                                    -  -  ---  --     -  -  --  --  ---  --
>>> smp_store_mb()                     Y  Y    Y   Y      Y  Y   Y   Y   Y   Y
> I'm not sure about that, the generic version of that reads:
> 
> include/asm-generic/barrier.h:#define __smp_store_mb(var, value)
>     do { WRITE_ONCE(var, value); __smp_mb(); } while (0)
> 
> Which doesn't not have an smp_mb() before, so it doesn't actually order
> prior; or I'm failing to read the table wrong.

You're not, even better reason to document it. :)  I was going from
memory for the x86 version.

I'll start tomorrow on fixes to the current document, while we discuss
the split format and what to do about cumulativity and propagation.

Paolo

Re: [PATCH] memory-model: fix cheat sheet typo

[Boqun Feng]

[-- Attachment #1: Type: text/plain, Size: 1315 bytes --]

On Wed, Apr 11, 2018 at 07:06:36PM +0200, Paolo Bonzini wrote:
> On 11/04/2018 18:31, Peter Zijlstra wrote:
> >>>                                    Prior Operation   Subsequent Operation
> >>>                                    ---------------   ---------------------
> >>>                                    R  W  RMW  SV     R  W  DR  DW  RMW  SV
> >>>                                    -  -  ---  --     -  -  --  --  ---  --
> >>> smp_store_mb()                     Y  Y    Y   Y      Y  Y   Y   Y   Y   Y
> > I'm not sure about that, the generic version of that reads:
> > 
> > include/asm-generic/barrier.h:#define __smp_store_mb(var, value)
> >     do { WRITE_ONCE(var, value); __smp_mb(); } while (0)
> > 
> > Which doesn't not have an smp_mb() before, so it doesn't actually order
> > prior; or I'm failing to read the table wrong.
> 
> You're not, even better reason to document it. :)  I was going from
> memory for the x86 version.
> 
> I'll start tomorrow on fixes to the current document, while we discuss
> the split format and what to do about cumulativity and propagation.
> 

Besides, since smp_store_mb() is a store, so there is no DR or DW for
the subsequent operations I think, because dependencies come from a read
rather than a write.

Regards,
Boqun

> Paolo

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]

Re: [PATCH] memory-model: fix cheat sheet typo

[Andrea Parri]

On Wed, Apr 11, 2018 at 01:15:58PM +0200, Paolo Bonzini wrote:
> On 10/04/2018 23:34, Paul E. McKenney wrote:
> > Glad it helps, and I have queued it for the next merge window.  Of course,
> > if a further improvement comes to mind, please do not keep it a secret.  ;-)
> 
> Yes, there are several changes that could be included:

Thank you for looking into this and for the suggestions.


> 
> - SV could be added to the prior operation case as well?  It should be
> symmetric

Seems reasonable to me.


> 
> - The *_relaxed() case also applies to void RMW

Indeed. *_relaxed() and void RMW do present some semantics differences
(c.f., e.g., 'Noreturn' in the definition of 'rmb' from the .cat file),
but the cheat sheet seems to be already 'cheating' here. ;-)


> 
> - smp_store_mb() is missing

Good point. In fact, we could add this to the model as well: following
Peter's remark/the generic implementation,

diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index 397e4e67e8c84..acf86f6f360a7 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -14,6 +14,7 @@ smp_store_release(X,V) { __store{release}(*X,V); }
 smp_load_acquire(X) __load{acquire}(*X)
 rcu_assign_pointer(X,V) { __store{release}(X,V); }
 rcu_dereference(X) __load{once}(X)
+smp_store_mb(X,V) { __store{once}(X,V); __fence{mb}; }
 
 // Fences
 smp_mb() { __fence{mb} ; }

... unless I'm missing something here: I'll send a patch with this.


> 
> - smp_rmb() orders prior reads fully against subsequent RMW because SV
> applies between the two parts of the RMW; likewise smp_wmb() orders prior
> RMW fully against subsequent writes

It could be argued that this ordering is the result of the combination
of two 'mechanisms' (barrier+SV/atomicity), and that it makes sense to
distinguish them... But either way would be fine for me.


> 
> 
> I am going submit these changes separately, but before doing that I can show
> also my rewrite of the cheat sheet.
> 
> The advantage is that, at least to me, it's clearer (and gets rid of
> "Self" :)).
> 
> The disadvantage is that it's much longer---almost twice the lines, even if
> you discount the splitting out of cumulative/propagating to a separate table
> (which in turn is because to me it's a different level of black magic).

Yeah, those 'Ordering is cumulative', 'Ordering propagates' could mean
different things to different readers... (and I'm not going to attempt
some snappy descriptions now). IMO, we may even omit such information;
this doc. does not certainly aim for completeness, after all. OTOH, we
ought to refrain from making this doc. an excuse to transform (what it
is really) high-school maths into some black magic. ;-) So once again,
thank you for your feedback!

  Andrea


> 
> ---------------------
> Memory operations are listed in this document as follows:
> 
> 	R:	Read portion of RMW
> 	W:	Write portion of RMW
> 	DR:	Dependent read (address dependency)
> 	DW:	Dependent write (address, data, or control dependency)
> 	RMW:	Atomic read-modify-write operation
> 	SV	Other accesses to the same variable
> 
> 
> Memory access operations order other memory operations against themselves as
> follows:
> 
>                                    Prior Operation   Subsequent Operation
>                                    ---------------   ---------------------
>                                    R  W  RMW  SV     R  W  DR  DW  RMW  SV
>                                    -  -  ---  --     -  -  --  --  ---  --
> Store, e.g., WRITE_ONCE()                      Y                         Y
> Load, e.g., READ_ONCE()                        Y            Y   Y        Y
> Unsuccessful RMW operation                     Y            Y   Y        Y
> *_relaxed() or void RMW operation              Y            Y   Y        Y
> rcu_dereference()                              Y            Y   Y        Y
> Successful *_acquire()                         Y      r  r  r   r    r   Y
> Successful *_release()             w  w    w   Y                         Y
> smp_store_mb()                     Y  Y    Y   Y      Y  Y   Y   Y   Y   Y
> Successful full non-void RMW       Y  Y    Y   Y      Y  Y   Y   Y   Y   Y
> 
> Key:	Y:	Memory operation provides ordering
> 	r:	Cannot move past the read portion of the *_acquire()
> 	w:	Cannot move past the write portion of the *_release()
> 
> 
> Memory barriers order prior memory operations against subsequent memory
> operations.  Two operations are ordered if both have non-empty cells in
> the following table:
> 
>                                    Prior Operation   Subsequent Operation
>                                    ---------------   --------------------
>                                    R  W  RMW         R  W  DR  DW  RMW
>                                    -  -  ---         -  -  --  --  ---
> smp_rmb()                          Y      r          Y      Y       Y
> smp_wmb()                             Y   Y             Y       Y   w
> smp_mb() & synchronize_rcu()       Y  Y   Y          Y  Y   Y   Y   Y
> smp_mb__before_atomic()            Y  Y   Y          a  a   a   a   Y
> smp_mb__after_atomic()             a  a   Y          Y  Y   Y   Y
> 
> 
> Key:	Y:	Barrier provides ordering
> 	r:	Barrier provides ordering against the read portion of RMW
> 	w:	Barrier provides ordering against the write portion of RMW
> 	a:	Barrier provides ordering given intervening RMW atomic operation
> 
> 
> Finally the following describes which operations provide cumulative and
> propagating fences:
> 
>                                      Cumulative         Propagates
>                                      ----------         ----------
> Store, e.g., WRITE_ONCE()
> Load, e.g., READ_ONCE()
> Unsuccessful RMW operation
> *_relaxed() or void RMW operation
> rcu_dereference()
> Successful *_acquire()
> Successful *_release()                   Y
> smp_store_mb()                           Y                  Y
> Successful full non-void RMW             Y                  Y
> smp_rmb()
> smp_wmb()
> smp_mb() & synchronize_rcu()             Y                  Y
> smp_mb__before_atomic()                  Y                  Y
> smp_mb__after_atomic()                   Y                  Y
> ----------
> 
> Perhaps you can see some obvious improvements.  Otherwise I'll send patches
> for the above issues.
> 
> Thanks,
> 
> Paolo

Re: [PATCH] memory-model: fix cheat sheet typo

[Paolo Bonzini]

On 12/04/2018 11:23, Andrea Parri wrote:
>>
>> - smp_store_mb() is missing
> 
> Good point. In fact, we could add this to the model as well:
> following Peter's remark/the generic implementation,

Good idea.  smp_store_mb() can save some clock cycles in the relatively
common idiom

	write a				write b
	read b				read a
	if (b)				if (a)
	  wake 'em			  we've been woken

> Yeah, those 'Ordering is cumulative', 'Ordering propagates' could
> mean different things to different readers... IMO, we may even omit
> such information; this doc. does not certainly aim for completeness,
> after all. OTOH, we ought to refrain from making this doc. an excuse
> to transform (what it is really) high-school maths into some black
> magic.
FWIW, what I miss in explanation.txt (and to some extent in the paper)
is a clear pointer to litmus tests that rely on cumulativity and
propagation.  In the meanwhile I'll send some patches.  Thanks for the
feedback, as it also helps validating my understanding of the model.

Thanks,

Paolo

Re: [PATCH] memory-model: fix cheat sheet typo

[Andrea Parri]

On Thu, Apr 12, 2018 at 12:18:13PM +0200, Paolo Bonzini wrote:
> On 12/04/2018 11:23, Andrea Parri wrote:
> >>
> >> - smp_store_mb() is missing
> > 
> > Good point. In fact, we could add this to the model as well:
> > following Peter's remark/the generic implementation,
> 
> Good idea.  smp_store_mb() can save some clock cycles in the relatively
> common idiom
> 
> 	write a				write b
> 	read b				read a
> 	if (b)				if (a)
> 	  wake 'em			  we've been woken
> 
> > Yeah, those 'Ordering is cumulative', 'Ordering propagates' could
> > mean different things to different readers... IMO, we may even omit
> > such information; this doc. does not certainly aim for completeness,
> > after all. OTOH, we ought to refrain from making this doc. an excuse
> > to transform (what it is really) high-school maths into some black
> > magic.
> FWIW, what I miss in explanation.txt (and to some extent in the paper)
> is a clear pointer to litmus tests that rely on cumulativity and
> propagation.  In the meanwhile I'll send some patches.  Thanks for the
> feedback, as it also helps validating my understanding of the model.

The litmus test that first comes to my mind when I think of cumulativity
(at least, 'cumulativity' as intended in LKMM) is:

   WRC+pooncerelease+rmbonceonce+Once.litmus

for 'propagation', I could mention:

   IRIW+mbonceonces+OnceOnce.litmus

(both tests are availabe in tools/memory-model/litmus-tests/). It would
be a nice to mention these properties in the test descriptions, indeed.

You might find it useful to also visualize the 'valid' executions (with
the main events/relations) associated to each of these tests; for this,

   $ herd7 -conf linux-kernel.cfg litmus-tests/your-test.litmus \
	-show all -gv

(assuming you have 'gv' installed).

  Andrea


> 
> Thanks,
> 
> Paolo

Re: [PATCH] memory-model: fix cheat sheet typo

[Paul E. McKenney]

On Thu, Apr 12, 2018 at 01:21:55PM +0200, Andrea Parri wrote:
> On Thu, Apr 12, 2018 at 12:18:13PM +0200, Paolo Bonzini wrote:
> > On 12/04/2018 11:23, Andrea Parri wrote:
> > >>
> > >> - smp_store_mb() is missing
> > > 
> > > Good point. In fact, we could add this to the model as well:
> > > following Peter's remark/the generic implementation,
> > 
> > Good idea.  smp_store_mb() can save some clock cycles in the relatively
> > common idiom
> > 
> > 	write a				write b
> > 	read b				read a
> > 	if (b)				if (a)
> > 	  wake 'em			  we've been woken
> > 
> > > Yeah, those 'Ordering is cumulative', 'Ordering propagates' could
> > > mean different things to different readers... IMO, we may even omit
> > > such information; this doc. does not certainly aim for completeness,
> > > after all. OTOH, we ought to refrain from making this doc. an excuse
> > > to transform (what it is really) high-school maths into some black
> > > magic.
> > FWIW, what I miss in explanation.txt (and to some extent in the paper)
> > is a clear pointer to litmus tests that rely on cumulativity and
> > propagation.  In the meanwhile I'll send some patches.  Thanks for the
> > feedback, as it also helps validating my understanding of the model.
> 
> The litmus test that first comes to my mind when I think of cumulativity
> (at least, 'cumulativity' as intended in LKMM) is:
> 
>    WRC+pooncerelease+rmbonceonce+Once.litmus

Removing the "cumul-fence* ;" from "let prop" does cause this test to be
allowed, so looks plausible.

> for 'propagation', I could mention:
> 
>    IRIW+mbonceonces+OnceOnce.litmus

And removing the "acyclic pb as propagation" causes this one to be allowed,
so again plausible.

> (both tests are availabe in tools/memory-model/litmus-tests/). It would
> be a nice to mention these properties in the test descriptions, indeed.

Please see below.

							Thanx, Paul

> You might find it useful to also visualize the 'valid' executions (with
> the main events/relations) associated to each of these tests; for this,
> 
>    $ herd7 -conf linux-kernel.cfg litmus-tests/your-test.litmus \
> 	-show all -gv
> 
> (assuming you have 'gv' installed).

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

commit 494f11d10dd7d86e4a381cbe79e77f04cb0cee04
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date:   Thu Apr 12 14:15:57 2018 -0700

    EXP tools/memory-model: Flag "cumulativity" and "propagation" tests
    
    This commit flags WRC+pooncerelease+rmbonceonce+Once.litmus as being
    forbidden by LKMM cumulativity and IRIW+mbonceonces+OnceOnce.litmus as
    being forbidden by LKMM propagation.
    
    Suggested-by: Andrea Parri <andrea.parri@amarulasolutions.com>
    Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

diff --git a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
index 50d5db9ea983..98a3716efa37 100644
--- a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
@@ -7,7 +7,7 @@ C IRIW+mbonceonces+OnceOnce
  * between each pairs of reads.  In other words, is smp_mb() sufficient to
  * cause two different reading processes to agree on the order of a pair
  * of writes, where each write is to a different variable by a different
- * process?
+ * process?  This litmus test exercises LKMM's "propagation" rule.
  *)
 
 {}
diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
index 6919909bbd0f..178941d2a51a 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -23,7 +23,8 @@ IRIW+mbonceonces+OnceOnce.litmus
 	between each pairs of reads.  In other words, is smp_mb()
 	sufficient to cause two different reading processes to agree on
 	the order of a pair of writes, where each write is to a different
-	variable by a different process?
+	variable by a different process?  This litmus test is an example
+	that is forbidden by LKMM propagation.
 
 IRIW+poonceonces+OnceOnce.litmus
 	Test of independent reads from independent writes with nothing
@@ -121,6 +122,7 @@ WRC+poonceonces+Once.litmus
 WRC+pooncerelease+rmbonceonce+Once.litmus
 	These two are members of an extension of the MP litmus-test class
 	in which the first write is moved to a separate process.
+	The second is an example that is forbidden by LKMM cumulativity.
 
 Z6.0+pooncelock+pooncelock+pombonce.litmus
 	Is the ordering provided by a spin_unlock() and a subsequent
diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
index 97fcbffde9a0..5bda4784eb34 100644
--- a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
@@ -5,7 +5,8 @@ C WRC+pooncerelease+rmbonceonce+Once
  *
  * This litmus test is an extension of the message-passing pattern, where
  * the first write is moved to a separate process.  Because it features
- * a release and a read memory barrier, it should be forbidden.
+ * a release and a read memory barrier, it should be forbidden.  This
+ * litmus test exercises LKMM cumulativity.
  *)
 
 {}

Re: [PATCH] memory-model: fix cheat sheet typo

[Andrea Parri]

On Thu, Apr 12, 2018 at 02:18:36PM -0700, Paul E. McKenney wrote:
> On Thu, Apr 12, 2018 at 01:21:55PM +0200, Andrea Parri wrote:
> > 
> > The litmus test that first comes to my mind when I think of cumulativity
> > (at least, 'cumulativity' as intended in LKMM) is:
> > 
> >    WRC+pooncerelease+rmbonceonce+Once.litmus
> 
> Removing the "cumul-fence* ;" from "let prop" does cause this test to be
> allowed, so looks plausible.
> 
> > for 'propagation', I could mention:
> > 
> >    IRIW+mbonceonces+OnceOnce.litmus
> 
> And removing the "acyclic pb as propagation" causes this one to be allowed,
> so again plausible.
> 
> > (both tests are availabe in tools/memory-model/litmus-tests/). It would
> > be a nice to mention these properties in the test descriptions, indeed.
> 
> Please see below.

Matching what I had in mind ;) thanks!

  Andrea


> 
> 							Thanx, Paul
> 
> > You might find it useful to also visualize the 'valid' executions (with
> > the main events/relations) associated to each of these tests; for this,
> > 
> >    $ herd7 -conf linux-kernel.cfg litmus-tests/your-test.litmus \
> > 	-show all -gv
> > 
> > (assuming you have 'gv' installed).
> 
> ------------------------------------------------------------------------
> 
> commit 494f11d10dd7d86e4a381cbe79e77f04cb0cee04
> Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> Date:   Thu Apr 12 14:15:57 2018 -0700
> 
>     EXP tools/memory-model: Flag "cumulativity" and "propagation" tests
>     
>     This commit flags WRC+pooncerelease+rmbonceonce+Once.litmus as being
>     forbidden by LKMM cumulativity and IRIW+mbonceonces+OnceOnce.litmus as
>     being forbidden by LKMM propagation.
>     
>     Suggested-by: Andrea Parri <andrea.parri@amarulasolutions.com>
>     Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> 
> diff --git a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
> index 50d5db9ea983..98a3716efa37 100644
> --- a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
> +++ b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
> @@ -7,7 +7,7 @@ C IRIW+mbonceonces+OnceOnce
>   * between each pairs of reads.  In other words, is smp_mb() sufficient to
>   * cause two different reading processes to agree on the order of a pair
>   * of writes, where each write is to a different variable by a different
> - * process?
> + * process?  This litmus test exercises LKMM's "propagation" rule.
>   *)
>  
>  {}
> diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
> index 6919909bbd0f..178941d2a51a 100644
> --- a/tools/memory-model/litmus-tests/README
> +++ b/tools/memory-model/litmus-tests/README
> @@ -23,7 +23,8 @@ IRIW+mbonceonces+OnceOnce.litmus
>  	between each pairs of reads.  In other words, is smp_mb()
>  	sufficient to cause two different reading processes to agree on
>  	the order of a pair of writes, where each write is to a different
> -	variable by a different process?
> +	variable by a different process?  This litmus test is an example
> +	that is forbidden by LKMM propagation.
>  
>  IRIW+poonceonces+OnceOnce.litmus
>  	Test of independent reads from independent writes with nothing
> @@ -121,6 +122,7 @@ WRC+poonceonces+Once.litmus
>  WRC+pooncerelease+rmbonceonce+Once.litmus
>  	These two are members of an extension of the MP litmus-test class
>  	in which the first write is moved to a separate process.
> +	The second is an example that is forbidden by LKMM cumulativity.
>  
>  Z6.0+pooncelock+pooncelock+pombonce.litmus
>  	Is the ordering provided by a spin_unlock() and a subsequent
> diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
> index 97fcbffde9a0..5bda4784eb34 100644
> --- a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
> +++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
> @@ -5,7 +5,8 @@ C WRC+pooncerelease+rmbonceonce+Once
>   *
>   * This litmus test is an extension of the message-passing pattern, where
>   * the first write is moved to a separate process.  Because it features
> - * a release and a read memory barrier, it should be forbidden.
> + * a release and a read memory barrier, it should be forbidden.  This
> + * litmus test exercises LKMM cumulativity.
>   *)
>  
>  {}
>