Re: [PATCH RFC tools/memory-model 4/5] tools/memory-model: Add model support for spin_is_locked

[Andrea Parri]

On Mon, Apr 16, 2018 at 09:22:50AM -0700, Paul E. McKenney wrote:
> From: Luc Maranget <Luc.Maranget@xxxxxxxx>
> 
> This commit first adds a trivial macro for spin_is_locked() to
> linux-kernel.def.
> 
> It also adds cat code for enumerating all possible matches of lock
> write events (set LKW) with islocked events returning true (set RL,
> for Read from Lock), and unlock write events (set UL) with islocked
> events returning false (set RU, for Read from Unlock).  Note that this
> intentionally does not model uniprocessor kernels (CONFIG_SMP=n) built
> with CONFIG_DEBUG_SPINLOCK=n, in which spin_is_locked() unconditionally
> returns zero.
> 
> It also adds a pair of litmus tests demonstrating the minimal ordering
> provided by spin_is_locked() in conjunction with spin_lock().  Will Deacon
> noted that this minimal ordering happens on ARMv8:
> https://lkml.kernel.org/r/20180226162426.GB17158@xxxxxxx
> 
> Notice that herd7 installations strictly older than version 7.49
> do not handle the new constructs.
> 
> Signed-off-by: Luc Maranget <luc.maranget@xxxxxxxx>
> 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@xxxxxxxxxxxxxxxxxx>
> Cc: Akira Yokosawa <akiyks@xxxxxxxxx>
> Cc: Ingo Molnar <mingo@xxxxxxxxxx>
> Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>

I understand that it's acceptable to not list all maintainers in the
commit message, but that does look like an omission...


> ---
>  tools/memory-model/linux-kernel.def                |  1 +
>  .../MP+polockmbonce+poacquiresilsil.litmus         | 30 ++++++++++++
>  .../MP+polockonce+poacquiresilsil.litmus           | 29 ++++++++++++
>  tools/memory-model/litmus-tests/README             | 10 ++++
>  tools/memory-model/lock.cat                        | 53 ++++++++++++++++++++--
>  5 files changed, 119 insertions(+), 4 deletions(-)
>  create mode 100644 tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
>  create mode 100644 tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> 
> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> index 6bd3bc431b3d..f0553bd37c08 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -38,6 +38,7 @@ cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W)
>  spin_lock(X) { __lock(X); }
>  spin_unlock(X) { __unlock(X); }
>  spin_trylock(X) __trylock(X)
> +spin_is_locked(X) __islocked(X)
>  
>  // RCU
>  rcu_read_lock() { __fence{rcu-lock}; }
> diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> new file mode 100644
> index 000000000000..37357404a08d
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> @@ -0,0 +1,30 @@
> +C MP+polockmbonce+poacquiresilsil
> +
> +(*
> + * Result: Never
> + *
> + * Do spinlocks combined with smp_mb__after_spinlock() provide order
> + * to outside observers using spin_is_locked() to sense the lock-held
> + * state, ordered by acquire?  Note that when the first spin_is_locked()
> + * returns false and the second true, we know that the smp_load_acquire()
> + * executed before the lock was acquired (loosely speaking).
> + *)
> +
> +{
> +}
> +
> +P0 (spinlock_t *lo, int *x) {
> +	spin_lock(lo);
> +	smp_mb__after_spinlock();
> +	WRITE_ONCE(*x,1);
> +	spin_unlock(lo);
> +}
> +
> +P1 (spinlock_t *lo, int *x) {
> +	int r1; int r2; int r3;
> +	r1 = smp_load_acquire(x);
> +        r2 = spin_is_locked(lo);
> +	r3 = spin_is_locked(lo);
> +}
> +
> +exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)
> diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> new file mode 100644
> index 000000000000..ebc2668f95ff
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> @@ -0,0 +1,29 @@
> +C MP+polockonce+poacquiresilsil
> +
> +(*
> + * Result: Sometimes
> + *
> + * Do spinlocks provide order to outside observers using spin_is_locked()
> + * to sense the lock-held state, ordered by acquire?  Note that when the
> + * first spin_is_locked() returns false and the second true, we know that
> + * the smp_load_acquire() executed before the lock was acquired (loosely
> + * speaking).
> + *)
> +
> +{
> +}
> +
> +P0 (spinlock_t *lo, int *x) {
> +	spin_lock(lo);
> +	WRITE_ONCE(*x,1);
> +	spin_unlock(lo);
> +}
> +
> +P1 (spinlock_t *lo, int *x) {
> +	int r1; int r2; int r3;
> +	r1 = smp_load_acquire(x);
> +        r2 = spin_is_locked(lo);
> +	r3 = spin_is_locked(lo);
> +}
> +
> +exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)

Please fix the style in the above litmus tests (c.f., e.g., your 2/5).


> diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
> index 04096fb8b8d9..6919909bbd0f 100644
> --- a/tools/memory-model/litmus-tests/README
> +++ b/tools/memory-model/litmus-tests/README
> @@ -63,6 +63,16 @@ LB+poonceonces.litmus
>  MP+onceassign+derefonce.litmus
>  	As below, but with rcu_assign_pointer() and an rcu_dereference().
>  
> +MP+polockmbonce+poacquiresilsil.litmus
> +	Protect the access with a lock and an smp_mb__after_spinlock()
> +	in one process, and use an acquire load followed by a pair of
> +	spin_is_locked() calls in the other process.
> +
> +MP+polockonce+poacquiresilsil.litmus
> +	Protect the access with a lock in one process, and use an
> +	acquire load followed by a pair of spin_is_locked() calls
> +	in the other process.
> +
>  MP+polocks.litmus
>  	As below, but with the second access of the writer process
>  	and the first access of reader process protected by a lock.
> diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
> index ba4a4ec6d313..3b1439edc818 100644
> --- a/tools/memory-model/lock.cat
> +++ b/tools/memory-model/lock.cat
> @@ -5,7 +5,11 @@
>   *)
>  
>  (* Generate coherence orders and handle lock operations *)
> -
> +(*
> + * Warning, crashes with herd7 versions strictly before 7.48.
> + * spin_islocked is functional from version 7.49.
> + *
> + *)
>  include "cross.cat"
>  
>  (* From lock reads to their partner lock writes *)
> @@ -32,12 +36,16 @@ flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
>  (* The final value of a spinlock should not be tested *)
>  flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
>  
> -
> +(*
> + * Backward compatibility
> + *)
> +let RL = try RL with emptyset (* defined herd7 >= 7.49 *)
> +let RU = try RU with emptyset (* defined herd7 >= 7.49 *)
>  (*
>   * Put lock operations in their appropriate classes, but leave UL out of W
>   * until after the co relation has been generated.
>   *)
> -let R = R | LKR | LF
> +let R = R | LKR | LF | RL | RU
>  let W = W | LKW
>  
>  let Release = Release | UL
> @@ -72,8 +80,45 @@ let all-possible-rfe-lf =
>  
>  (* Generate all rf relations for LF events *)
>  with rfe-lf from cross(all-possible-rfe-lf)
> -let rf = rf | rfi-lf | rfe-lf
>  
> +let rf-lf = rfe-lf | rfi-lf
> +
> +(* rf for RL events, ie islocked returning true, similar to LF above *)
> +
> +(* islocked returning true inside a critical section
> + * must read from the opening lock
> + *)
> +let rfi-rl = ([LKW] ; po-loc ; [RL]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
> +
> +(* islocked returning true outside critical sections can match any
> + * external lock.
> + *)

multi-lines comments are

(*
 * line
 * line
 *)


> +let all-possible-rfe-rl =
> +  let possible-rfe-lf r =
> +    let pair-to-relation p = p ++ 0
> +    in map pair-to-relation ((LKW * {r}) & loc & ext)
> +  in map possible-rfe-lf (RL \ range(rfi-rl))
> +
> +with rfe-rl from cross(all-possible-rfe-rl)
> +let rf-rl = rfe-rl | rfi-rl
> +
> +(* Read from unlock, ie islocked returning false, slightly different *)
> +
> +(* islocked returning false can read from the last po-previous unlock *)
> +let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
> +
> +(* any islocked returning false can read from any external unlock *)
> +let all-possible-rfe-ru =
> +   let possible-rfe-ru r =

please fix the alignment/indentation


> +     let pair-to-relation p = p ++ 0
> +     in map pair-to-relation (((UL|IW) * {r}) & loc & ext)

spaces around binary operators  ^^^^

  Andrea


> +  in map possible-rfe-ru RU
> +
> +with rfe-ru from cross(all-possible-rfe-ru)
> +let rf-ru = rfe-ru | rfi-ru
> +
> +(* Final rf relation *)
> +let rf = rf | rf-lf | rf-rl | rf-ru
>  
>  (* Generate all co relations, including LKW events but not UL *)
>  let co0 = co0 | ([IW] ; loc ; [LKW]) |
> -- 
> 2.5.2
>