Re: [PATCH] memory-model: fix cheat sheet typo
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> 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 > Signed-off-by: Paul E. McKenney > > 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
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 > 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 > Signed-off-by: Paul E. McKenney > > 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
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 'emwe'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. McKenneyDate: 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 Signed-off-by: Paul E. McKenney 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
Re: [PATCH] memory-model: fix cheat sheet typo
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 'emwe'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 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 Signed-off-by: Paul E. McKenney 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 +++
Re: [PATCH] memory-model: fix cheat sheet typo
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 YY 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 signature.asc Description: PGP signature
Re: [PATCH] memory-model: fix cheat sheet typo
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 YY 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 signature.asc Description: PGP signature
Re: [PATCH] memory-model: fix cheat sheet typo
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 'emwe'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
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 'emwe'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
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 'emwe'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
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 'emwe'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
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()YY YY > Unsuccessful RMW operation YY YY > *_relaxed() or void RMW operation YY YY > rcu_dereference() YY YY > Successful *_acquire() Y r r r rr Y > Successful *_release() w ww Y Y > smp_store_mb() Y YY Y Y Y Y Y Y Y > Successful full non-void RMW Y YY 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
Re: [PATCH] memory-model: fix cheat sheet typo
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()YY YY > Unsuccessful RMW operation YY YY > *_relaxed() or void RMW operation YY YY > rcu_dereference() YY YY > Successful *_acquire() Y r r r rr Y > Successful *_release() w ww Y Y > smp_store_mb() Y YY Y Y Y Y Y Y Y > Successful full non-void RMW Y YY 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
Re: [PATCH] memory-model: fix cheat sheet typo
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 YY 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
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 YY 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
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 YY 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
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 YY 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
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()YY YY > Unsuccessful RMW operation YY YY > *_relaxed() or void RMW operation YY YY > rcu_dereference() YY YY > Successful *_acquire() Y r r r rr Y > Successful *_release() w ww Y Y > smp_store_mb() Y YY Y Y Y Y Y Y Y > Successful full non-void RMW Y YY 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
Re: [PATCH] memory-model: fix cheat sheet typo
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()YY YY > Unsuccessful RMW operation YY YY > *_relaxed() or void RMW operation YY YY > rcu_dereference() YY YY > Successful *_acquire() Y r r r rr Y > Successful *_release() w ww Y Y > smp_store_mb() Y YY Y Y Y Y Y Y Y > Successful full non-void RMW Y YY 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
Re: [PATCH] memory-model: fix cheat sheet typo
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()YY YY Unsuccessful RMW operation YY YY *_relaxed() or void RMW operation YY YY rcu_dereference() YY YY Successful *_acquire() Y r r r rr Y Successful *_release() w ww Y Y smp_store_mb() Y YY Y Y Y Y Y Y Y Successful full non-void RMW Y YY 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
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()YY YY Unsuccessful RMW operation YY YY *_relaxed() or void RMW operation YY YY rcu_dereference() YY YY Successful *_acquire() Y r r r rr Y Successful *_release() w ww Y Y smp_store_mb() Y YY Y Y Y Y Y Y Y Successful full non-void RMW Y YY 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
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> >> > >> 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 > > 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 > > Signed-off-by: Paul E. McKenney > > > > 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
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 > >> > >> 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 > > 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 > > Signed-off-by: Paul E. McKenney > > > > 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
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>> >> 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 > 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 > Signed-off-by: Paul E. McKenney > > 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
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 >> >> 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 > 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 > Signed-off-by: Paul E. McKenney > > 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
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> > 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 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 Signed-off-by: Paul E. McKenney 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
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 > > 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 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 Signed-off-by: Paul E. McKenney 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
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 BonziniApplied, 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
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 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 >