[PATCH 0/2] tools/memory-model: Model 'smp_store_mb()'

[PATCH 0/2] tools/memory-model: Model 'smp_store_mb()'

[Andrea Parri]

Hi,

This (tiny) series adds 'smp_store_mb()' to the model (patch 1/2), and
it fixes a stylistic discrepancy in 'linux-kernel.def (patch 2/2).

Cheers,
  Andrea

Andrea Parri (2):
  tools/memory-model: Model 'smp_store_mb()'
  tools/memory-model: Fix coding style in 'linux-kernel.def'

 tools/memory-model/linux-kernel.def | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

-- 
2.7.4

[PATCH 1/2] tools/memory-model: Model 'smp_store_mb()'

[Andrea Parri]

Says that 'smp_store_mb(x, val);' is _semantically_ equivalent to
'WRITE_ONCE(x, val); smp_mb();'.

Suggested-by: Paolo Bonzini <pbonzini@redhat.com>
Suggested-by: Peter Zijlstra <peterz@infradead.org>
Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com>
---
 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 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} ; }
-- 
2.7.4

[PATCH 2/2] tools/memory-model: Fix coding style in 'linux-kernel.def'

[Andrea Parri]

Fixes white spaces around semicolons.

Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com>
---
 tools/memory-model/linux-kernel.def | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index acf86f6f360a7..6bd3bc431b3da 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -17,12 +17,12 @@ rcu_dereference(X) __load{once}(X)
 smp_store_mb(X,V) { __store{once}(X,V); __fence{mb}; }
 
 // Fences
-smp_mb() { __fence{mb} ; }
-smp_rmb() { __fence{rmb} ; }
-smp_wmb() { __fence{wmb} ; }
-smp_mb__before_atomic() { __fence{before-atomic} ; }
-smp_mb__after_atomic() { __fence{after-atomic} ; }
-smp_mb__after_spinlock() { __fence{after-spinlock} ; }
+smp_mb() { __fence{mb}; }
+smp_rmb() { __fence{rmb}; }
+smp_wmb() { __fence{wmb}; }
+smp_mb__before_atomic() { __fence{before-atomic}; }
+smp_mb__after_atomic() { __fence{after-atomic}; }
+smp_mb__after_spinlock() { __fence{after-spinlock}; }
 
 // Exchange
 xchg(X,V)  __xchg{mb}(X,V)
@@ -35,26 +35,26 @@ cmpxchg_acquire(X,V,W) __cmpxchg{acquire}(X,V,W)
 cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W)
 
 // Spinlocks
-spin_lock(X) { __lock(X) ; }
-spin_unlock(X) { __unlock(X) ; }
+spin_lock(X) { __lock(X); }
+spin_unlock(X) { __unlock(X); }
 spin_trylock(X) __trylock(X)
 
 // RCU
 rcu_read_lock() { __fence{rcu-lock}; }
-rcu_read_unlock() { __fence{rcu-unlock};}
+rcu_read_unlock() { __fence{rcu-unlock}; }
 synchronize_rcu() { __fence{sync-rcu}; }
 synchronize_rcu_expedited() { __fence{sync-rcu}; }
 
 // Atomic
 atomic_read(X) READ_ONCE(*X)
-atomic_set(X,V) { WRITE_ONCE(*X,V) ; }
+atomic_set(X,V) { WRITE_ONCE(*X,V); }
 atomic_read_acquire(X) smp_load_acquire(X)
 atomic_set_release(X,V) { smp_store_release(X,V); }
 
-atomic_add(V,X) { __atomic_op(X,+,V) ; }
-atomic_sub(V,X) { __atomic_op(X,-,V) ; }
-atomic_inc(X)   { __atomic_op(X,+,1) ; }
-atomic_dec(X)   { __atomic_op(X,-,1) ; }
+atomic_add(V,X) { __atomic_op(X,+,V); }
+atomic_sub(V,X) { __atomic_op(X,-,V); }
+atomic_inc(X)   { __atomic_op(X,+,1); }
+atomic_dec(X)   { __atomic_op(X,-,1); }
 
 atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V)
 atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V)
-- 
2.7.4

Re: [PATCH 0/2] tools/memory-model: Model 'smp_store_mb()'

[Paul E. McKenney]

On Thu, Apr 12, 2018 at 02:22:48PM +0200, Andrea Parri wrote:
> Hi,
> 
> This (tiny) series adds 'smp_store_mb()' to the model (patch 1/2), and
> it fixes a stylistic discrepancy in 'linux-kernel.def (patch 2/2).

I applied them both, thank you!

I had to apply 2/2 by hand for reasons that are not at all clear to
me.  Please check to make sure I got it right.

							Thanx, Paul

> Cheers,
>   Andrea
> 
> Andrea Parri (2):
>   tools/memory-model: Model 'smp_store_mb()'
>   tools/memory-model: Fix coding style in 'linux-kernel.def'
> 
>  tools/memory-model/linux-kernel.def | 29 +++++++++++++++--------------
>  1 file changed, 15 insertions(+), 14 deletions(-)
> 
> -- 
> 2.7.4
> 

Re: [PATCH 0/2] tools/memory-model: Model 'smp_store_mb()'

[Andrea Parri]

On Thu, Apr 12, 2018 at 02:06:27PM -0700, Paul E. McKenney wrote:
> On Thu, Apr 12, 2018 at 02:22:48PM +0200, Andrea Parri wrote:
> > Hi,
> > 
> > This (tiny) series adds 'smp_store_mb()' to the model (patch 1/2), and
> > it fixes a stylistic discrepancy in 'linux-kernel.def (patch 2/2).
> 
> I applied them both, thank you!
> 
> I had to apply 2/2 by hand for reasons that are not at all clear to
> me.  Please check to make sure I got it right.

It's OK for me.  Thanks,

  Andrea


> 
> 							Thanx, Paul
> 
> > Cheers,
> >   Andrea
> > 
> > Andrea Parri (2):
> >   tools/memory-model: Model 'smp_store_mb()'
> >   tools/memory-model: Fix coding style in 'linux-kernel.def'
> > 
> >  tools/memory-model/linux-kernel.def | 29 +++++++++++++++--------------
> >  1 file changed, 15 insertions(+), 14 deletions(-)
> > 
> > -- 
> > 2.7.4
> > 
>