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@xxxxxxxxxxxxxxxxxx>
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@xxxxxxxxxxxxxxxxxxxx>
    Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>

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.
  *)
 
 {}