Re: [PATCH RFC LKMM 7/7] tools/memory-model: Dynamically check SRCU lock-to-unlock matching

[Andrea Parri]

On Wed, Jan 09, 2019 at 01:07:48PM -0800, Paul E. McKenney wrote:
> From: Luc Maranget <Luc.Maranget@xxxxxxxx>
> 
> This commit checks that the return value of srcu_read_lock() is passed
> to the matching srcu_read_unlock(), where "matching" is determined by
> nesting.  This check operates as follows:
> 
>    1. srcu_read_lock() creates an integer token, which is stored into
>       the generated events.
>    2. srcu_read_unlock() records its second (token) argument into the
>       generated event.
>    3. A new herd primitive 'different-values' filters out pairs of events
>       with identical values from the relation passed as its argument.
>    4. The bell file applies the above primitive to the (srcu)
>       read-side-critical-section relation 'srcu-rscs' and flags non-empty
>       results.
> 
> BEWARE: Works only with herd version 7.51+6 and onwards.
> 
> Signed-off-by: Luc Maranget <Luc.Maranget@xxxxxxxx>
> Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxx>
> [ paulmck: Apply Andrea Parri's off-list feedback. ]
> ---
>  tools/memory-model/linux-kernel.bell | 3 +++
>  tools/memory-model/linux-kernel.cat  | 2 ++
>  tools/memory-model/linux-kernel.def  | 2 +-
>  3 files changed, 6 insertions(+), 1 deletion(-)
> 
> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> index 9c42cd9ddcb4..def9131d3d8e 100644
> --- a/tools/memory-model/linux-kernel.bell
> +++ b/tools/memory-model/linux-kernel.bell
> @@ -73,3 +73,6 @@ flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking
>  
>  (* Check for use of synchronize_srcu() inside an RCU critical section *)
>  flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
> +
> +(* Validate SRCU dynamic match *)
> +flag ~empty different-values(srcu-rscs) as srcu-bad-nesting
> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> index 8dcb37835b61..95bf45f1215f 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -1,5 +1,7 @@
>  // SPDX-License-Identifier: GPL-2.0+
>  (*
> + * Requires herd version 7.51+6 or higher.

I'm not all that exited about spreading version requirements in the
source: we report this requirement in our README, and apparently we
already struggle to keep this information up-to-date.  So what about
squashing something like the below (assume that 7.52 will be released
by the time this patch hit mainline; if this won't be the case, we
may consider using the development version 7.51+6)? notice that this
also removes an (obsolete, at this point) comment from lock.cat.

  Andrea

diff --git a/tools/memory-model/README b/tools/memory-model/README
index 9d7d4f23503fd..b362a41358fa1 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -20,8 +20,8 @@ that litmus test to be exercised within the Linux kernel.
 REQUIREMENTS
 ============
 
-Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded
-separately:
+Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
+downloaded separately:
 
   https://github.com/herd/herdtools7
 
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
index 95bf45f1215fc..8dcb37835b613 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -1,7 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0+
 (*
- * Requires herd version 7.51+6 or higher.
- *
  * Copyright (C) 2015 Jade Alglave <j.alglave@xxxxxxxxx>,
  * Copyright (C) 2016 Luc Maranget <luc.maranget@xxxxxxxx> for Inria
  * Copyright (C) 2017 Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>,
diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
index 305ded17e7411..a059d1a6d8a29 100644
--- a/tools/memory-model/lock.cat
+++ b/tools/memory-model/lock.cat
@@ -6,9 +6,6 @@
 
 (*
  * Generate coherence orders and handle lock operations
- *
- * Warning: spin_is_locked() crashes herd7 versions strictly before 7.48.
- * spin_is_locked() is functional from herd7 version 7.49.
  *)
 
 include "cross.cat"



> + *
>   * Copyright (C) 2015 Jade Alglave <j.alglave@xxxxxxxxx>,
>   * Copyright (C) 2016 Luc Maranget <luc.maranget@xxxxxxxx> for Inria
>   * Copyright (C) 2017 Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>,
> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> index 1d6a120cde14..0c3f0ef486f4 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -49,7 +49,7 @@ synchronize_rcu_expedited() { __fence{sync-rcu}; }
>  
>  // SRCU
>  srcu_read_lock(X)  __srcu{srcu-lock}(X)
> -srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X); }
> +srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); }
>  synchronize_srcu(X)  { __srcu{sync-srcu}(X); }
>  
>  // Atomic
> -- 
> 2.17.1
>