Re: [PATCH] tools/memory-model: Model smp_mb__after_unlock_lock()

[Andrea Parri]

On Mon, Sep 24, 2018 at 12:44:49PM +0200, Andrea Parri wrote:
> From the header comment for smp_mb__after_unlock_lock():
> 
>   "Place this after a lock-acquisition primitive to guarantee that
>    an UNLOCK+LOCK pair acts as a full barrier.  This guarantee applies
>    if the UNLOCK and LOCK are executed by the same CPU or if the
>    UNLOCK and LOCK operate on the same lock variable."
> 
> This formalizes the above guarantee by defining (new) mb-links according
> to the law:
> 
>   ([M] ; po ; [UL] ; (co | po) ; [LKW] ;
> 	fencerel(After-unlock-lock) ; [M])
> 
> where the component ([UL] ; co ; [LKW]) identifies "UNLOCK+LOCK pairs on
> the same lock variable" and the component ([UL] ; po ; [LKW]) identifies
> "UNLOCK+LOCK pairs executed by the same CPU".
> 
> In particular, the LKMM forbids the following two behaviors (the second
> litmus test below is based on
> 
>   Documentation/RCU/Design/Memory-Ordering/Tree-RCU-Memory-Ordering.html
> 
> c.f., Section "Tree RCU Grace Period Memory Ordering Building Blocks"):
> 
> C after-unlock-lock-same-cpu
> 
> (*
>  * Result: Never
>  *)
> 
> {}
> 
> P0(spinlock_t *s, spinlock_t *t, int *x, int *y)
> {
> 	int r0;
> 
> 	spin_lock(s);
> 	WRITE_ONCE(*x, 1);
> 	spin_unlock(s);
> 	spin_lock(t);
> 	smp_mb__after_unlock_lock();
> 	r0 = READ_ONCE(*y);
> 	spin_unlock(t);
> }
> 
> P1(int *x, int *y)
> {
> 	int r0;
> 
> 	WRITE_ONCE(*y, 1);
> 	smp_mb();
> 	r0 = READ_ONCE(*x);
> }
> 
> exists (0:r0=0 /\ 1:r0=0)
> 
> C after-unlock-lock-same-lock-variable
> 
> (*
>  * Result: Never
>  *)
> 
> {}
> 
> P0(spinlock_t *s, int *x, int *y)
> {
> 	int r0;
> 
> 	spin_lock(s);
> 	WRITE_ONCE(*x, 1);
> 	r0 = READ_ONCE(*y);
> 	spin_unlock(s);
> }
> 
> P1(spinlock_t *s, int *y, int *z)
> {
> 	int r0;
> 
> 	spin_lock(s);
> 	smp_mb__after_unlock_lock();
> 	WRITE_ONCE(*y, 1);
> 	r0 = READ_ONCE(*z);
> 	spin_unlock(s);
> }
> 
> P2(int *z, int *x)
> {
> 	int r0;
> 
> 	WRITE_ONCE(*z, 1);
> 	smp_mb();
> 	r0 = READ_ONCE(*x);
> }
> 
> exists (0:r0=0 /\ 1:r0=0 /\ 2:r0=0)
> 
> Signed-off-by: Andrea Parri <andrea.parri@xxxxxxxxxxxxxxxxxxxx>
> Cc: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> Cc: Will Deacon <will.deacon@xxxxxxx>
> Cc: Peter Zijlstra <peterz@xxxxxxxxxxxxx>
> Cc: Boqun Feng <boqun.feng@xxxxxxxxx>
> Cc: Nicholas Piggin <npiggin@xxxxxxxxx>
> Cc: David Howells <dhowells@xxxxxxxxxx>
> Cc: Jade Alglave <j.alglave@xxxxxxxxx>
> Cc: Luc Maranget <luc.maranget@xxxxxxxx>
> Cc: "Paul E. McKenney" <paulmck@xxxxxxxxxxxxx>
> Cc: Akira Yokosawa <akiyks@xxxxxxxxx>
> Cc: Daniel Lustig <dlustig@xxxxxxxxxx>
> ---
> NOTES.
> 
> - A number of equivalent formalizations seems available; for example,
>   we could replace "co" in the law above with "coe" (by "coherence")
>   and we could limit "coe" to "singlestep(coe)" (by the "prop" term).
>   These changes did not show significant performance improvement and
>   they looked slightly less readable to me, hence...
> 
> - The mb-links order memory accesses po-_before_ the lock-release to
>   memory accesses po-_after_ the lock-acquire; in part., this forma-
>   lization does _not_ forbid the following behavior (after A. Stern):
> 
> C po-in-after-unlock-lock
> 
> {}
> 
> P0(spinlock_t *s, spinlock_t *t, int *y)
> {
> 	int r0;
> 
> 	spin_lock(s);
> 	spin_unlock(s);
> 
> 	spin_lock(t);
> 	smp_mb__after_unlock_lock();
> 	r0 = READ_ONCE(*y);
> 	spin_unlock(t);
> }
> 
> P1(spinlock_t *s, int *y)
> {
> 	int r0;
> 
> 	WRITE_ONCE(*y, 1);
> 	smp_mb();
> 	r0 = spin_is_locked(s);
> }
> 
> exists (0:r0=0 /\ 1:r0=0)

This should have been "exists (0:r0=0 /\ 1:r0=1)".

  Andrea


> 
> - I'm not aware of currently supported architectures (implementations)
>   of smp_mb__after_unlock_lock() and spin_{lock,unlock}() which would
>   violate the guarantee formalized in this patch.  It is worth noting
>   that the same conclusion does _not_ extend to other locking primiti-
>   ves (e.g., write_{lock,unlock}()), AFAICT: c.f., e.g., riscv.  This
>   "works" considered the callsites for the barrier, but yeah...
> ---
>  tools/memory-model/linux-kernel.bell | 3 ++-
>  tools/memory-model/linux-kernel.cat  | 4 +++-
>  tools/memory-model/linux-kernel.def  | 1 +
>  3 files changed, 6 insertions(+), 2 deletions(-)
> 
> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> index b84fb2f67109e..796513362c052 100644
> --- a/tools/memory-model/linux-kernel.bell
> +++ b/tools/memory-model/linux-kernel.bell
> @@ -29,7 +29,8 @@ enum Barriers = 'wmb (*smp_wmb*) ||
>  		'sync-rcu (*synchronize_rcu*) ||
>  		'before-atomic (*smp_mb__before_atomic*) ||
>  		'after-atomic (*smp_mb__after_atomic*) ||
> -		'after-spinlock (*smp_mb__after_spinlock*)
> +		'after-spinlock (*smp_mb__after_spinlock*) ||
> +		'after-unlock-lock (*smp_mb__after_unlock_lock*)
>  instructions F[Barriers]
>  
>  (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index 882fc33274ac3..8f23c74a96fdc 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -30,7 +30,9 @@ let wmb = [W] ; fencerel(Wmb) ; [W]
>  let mb = ([M] ; fencerel(Mb) ; [M]) |
>  	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
>  	([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
> -	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
> +	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
> +	([M] ; po ; [UL] ; (co | po) ; [LKW] ;
> +		fencerel(After-unlock-lock) ; [M])
>  let gp = po ; [Sync-rcu] ; po?
>  
>  let strong-fence = mb | gp
> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> index 6fa3eb28d40b5..b27911cc087d4 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -23,6 +23,7 @@ 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__after_unlock_lock() { __fence{after-unlock-lock}; }
>  
>  // Exchange
>  xchg(X,V)  __xchg{mb}(X,V)
> -- 
> 2.17.1
>