[tip:locking/core] tools/memory-model: Model 'smp_store_mb()'

[tip-bot for Andrea Parri]

Commit-ID:  bf8c6d963d16d40fbe70e94b61d9bf18c455fc6b
Gitweb:     https://git.kernel.org/tip/bf8c6d963d16d40fbe70e94b61d9bf18c455fc6b
Author:     Andrea Parri <andrea.parri@xxxxxxxxxxxxxxxxxxxx>
AuthorDate: Mon, 14 May 2018 16:33:45 -0700
Committer:  Ingo Molnar <mingo@xxxxxxxxxx>
CommitDate: Tue, 15 May 2018 08:11:16 +0200

tools/memory-model: Model 'smp_store_mb()'

This commit models 'smp_store_mb(x, val);' to be semantically equivalent
to 'WRITE_ONCE(x, val); smp_mb();'.

Suggested-by: Paolo Bonzini <pbonzini@xxxxxxxxxx>
Suggested-by: Peter Zijlstra <peterz@xxxxxxxxxxxxx>
Signed-off-by: Andrea Parri <andrea.parri@xxxxxxxxxxxxxxxxxxxx>
Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
Acked-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
Cc: Andrew Morton <akpm@xxxxxxxxxxxxxxxxxxxx>
Cc: Linus Torvalds <torvalds@xxxxxxxxxxxxxxxxxxxx>
Cc: Thomas Gleixner <tglx@xxxxxxxxxxxxx>
Cc: Will Deacon <will.deacon@xxxxxxx>
Cc: akiyks@xxxxxxxxx
Cc: boqun.feng@xxxxxxxxx
Cc: dhowells@xxxxxxxxxx
Cc: j.alglave@xxxxxxxxx
Cc: linux-arch@xxxxxxxxxxxxxxx
Cc: luc.maranget@xxxxxxxx
Cc: npiggin@xxxxxxxxx
Cc: parri.andrea@xxxxxxxxx
Link: http://lkml.kernel.org/r/1526340837-12222-7-git-send-email-paulmck@xxxxxxxxxxxxxxxxxx
Signed-off-by: Ingo Molnar <mingo@xxxxxxxxxx>
---
 tools/memory-model/linux-kernel.def | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index 397e4e67e8c8..acf86f6f360a 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} ; }