tools/memory-model: Flag "cumulativity" and "propagation" tests
This commit flags WRC+pooncerelease+rmbonceonce+Once.litmus as being forbidden by smp_store_release() A-cumulativity and IRIW+mbonceonces+OnceOnce.litmus as being forbidden by the LKMM propagation rule. Suggested-by: Andrea Parri <andrea.parri@amarulasolutions.com> Reported-by: Paolo Bonzini <pbonzini@redhat.com> [ paulmck: Updated wording as suggested by Alan Stern. ] Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Cc: Andrew Morton <akpm@linux-foundation.org> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-11-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
This commit is contained in:
parent
15553dcbca
commit
1bd3742043
@ -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.
|
||||
*)
|
||||
|
||||
{}
|
||||
|
@ -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 forbidden
|
||||
by LKMM's propagation rule.
|
||||
|
||||
IRIW+poonceonces+OnceOnce.litmus
|
||||
Test of independent reads from independent writes with nothing
|
||||
@ -119,8 +120,10 @@ S+wmbonceonce+poacquireonce.litmus
|
||||
|
||||
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.
|
||||
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 forbidden because smp_store_release() is
|
||||
A-cumulative in LKMM.
|
||||
|
||||
Z6.0+pooncelock+pooncelock+pombonce.litmus
|
||||
Is the ordering provided by a spin_unlock() and a subsequent
|
||||
|
@ -5,7 +5,9 @@ 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. More
|
||||
* specifically, this litmus test is forbidden because smp_store_release()
|
||||
* is A-cumulative in LKMM.
|
||||
*)
|
||||
|
||||
{}
|
||||
|
Loading…
Reference in New Issue
Block a user