[RFC,LKMM,7/7] tools/memory-model: Dynamically check SRCU lock-to-unlock matching
diff mbox series

Message ID 20190109210748.29074-7-paulmck@linux.ibm.com
State In Next
Commit 71e2ff5304c1ffa94f89f00e0aa29f077c9e4988
Headers show
Series
  • LKMM updates
Related show

Commit Message

Paul E. McKenney Jan. 9, 2019, 9:07 p.m. UTC
From: Luc Maranget <Luc.Maranget@inria.fr>

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@inria.fr>
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
[ 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(-)

Comments

Andrea Parri Jan. 10, 2019, 9:41 a.m. UTC | #1
On Wed, Jan 09, 2019 at 01:07:48PM -0800, Paul E. McKenney wrote:
> From: Luc Maranget <Luc.Maranget@inria.fr>
> 
> 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@inria.fr>
> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
> [ 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@ucl.ac.uk>,
  * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
  * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
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@ucl.ac.uk>,
>   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
>   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> 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
>
Paul E. McKenney Jan. 10, 2019, 2:40 p.m. UTC | #2
On Thu, Jan 10, 2019 at 10:41:31AM +0100, Andrea Parri wrote:
> On Wed, Jan 09, 2019 at 01:07:48PM -0800, Paul E. McKenney wrote:
> > From: Luc Maranget <Luc.Maranget@inria.fr>
> > 
> > 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@inria.fr>
> > Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
> > [ 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.

Sounds like a very good point to me!

Should have pointers in the various files to the README file?  Or maybe
get people used to using scripting that checks versions?  Or maybe
after answering questions for some time, people will get used to
checking versions?

							Thanx, Paul

>   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@ucl.ac.uk>,
>   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
>   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> 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@ucl.ac.uk>,
> >   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
> >   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> > 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
> > 
>
Andrea Parri Jan. 10, 2019, 11:20 p.m. UTC | #3
> > 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.
> 
> Sounds like a very good point to me!
> 
> Should have pointers in the various files to the README file?  Or maybe
> get people used to using scripting that checks versions?  Or maybe
> after answering questions for some time, people will get used to
> checking versions?

As discussed off-list: I have no strong opinion on this regard, well,
except that I think we ought to fix the README, somehow (consider my
diff below as a first proposal).  Akira actually preceded me on this
and suggested another solution [1].

  Andrea

[1] http://lkml.kernel.org/r/04d15c18-d210-e3da-01e2-483eff135cb7@gmail.com


> 
> 							Thanx, Paul
> 
> >   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@ucl.ac.uk>,
> >   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
> >   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> > 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@ucl.ac.uk>,
> > >   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
> > >   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> > > 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
> > > 
> > 
>
Paul E. McKenney Jan. 11, 2019, 9:44 p.m. UTC | #4
On Fri, Jan 11, 2019 at 12:20:45AM +0100, Andrea Parri wrote:
> > > 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.
> > 
> > Sounds like a very good point to me!
> > 
> > Should have pointers in the various files to the README file?  Or maybe
> > get people used to using scripting that checks versions?  Or maybe
> > after answering questions for some time, people will get used to
> > checking versions?
> 
> As discussed off-list: I have no strong opinion on this regard, well,
> except that I think we ought to fix the README, somehow (consider my
> diff below as a first proposal).  Akira actually preceded me on this
> and suggested another solution [1].
> 
>   Andrea
> 
> [1] http://lkml.kernel.org/r/04d15c18-d210-e3da-01e2-483eff135cb7@gmail.com

My concern with this approach is that it seems to me to implicitly promise
that herd will provide backwards compatibility, which is a real pain to
test, let alone to provide.  Yes, the latest version of herd probably
supports latest mainline, but will five-years-from-now herd work correctly
on the .bell, .cat, and .def files from current mainline?

							Thanx, Paul

> > >   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@ucl.ac.uk>,
> > >   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
> > >   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> > > 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@ucl.ac.uk>,
> > > >   * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
> > > >   * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
> > > > 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
> > > > 
> > > 
> > 
>
Alan Stern Jan. 11, 2019, 9:57 p.m. UTC | #5
On Fri, 11 Jan 2019, Paul E. McKenney wrote:

> On Fri, Jan 11, 2019 at 12:20:45AM +0100, Andrea Parri wrote:
> > > > 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.
> > > 
> > > Sounds like a very good point to me!
> > > 
> > > Should have pointers in the various files to the README file?  Or maybe
> > > get people used to using scripting that checks versions?  Or maybe
> > > after answering questions for some time, people will get used to
> > > checking versions?
> > 
> > As discussed off-list: I have no strong opinion on this regard, well,
> > except that I think we ought to fix the README, somehow (consider my
> > diff below as a first proposal).  Akira actually preceded me on this
> > and suggested another solution [1].
> > 
> >   Andrea
> > 
> > [1] http://lkml.kernel.org/r/04d15c18-d210-e3da-01e2-483eff135cb7@gmail.com
> 
> My concern with this approach is that it seems to me to implicitly promise
> that herd will provide backwards compatibility, which is a real pain to
> test, let alone to provide.  Yes, the latest version of herd probably
> supports latest mainline, but will five-years-from-now herd work correctly
> on the .bell, .cat, and .def files from current mainline?

The README file can say something along the lines of:

	Herd version 7.52 (later versions may or may not be 
	compatible).  Herd can be downloaded from...

Alan

Patch
diff mbox series

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.
+ *
  * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
  * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
  * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
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