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 >
