diff options
| author | Luc Maranget <Luc.Maranget@inria.fr> | 2018-12-27 16:27:12 +0100 |
|---|---|---|
| committer | Paul E. McKenney <paulmck@linux.ibm.com> | 2019-03-18 10:27:52 -0700 |
| commit | 9393998e9ee094f99d18783cc85c489e20f0e0e7 (patch) | |
| tree | b2d6cea2bd7343fa600a53c6269496d0bea91be1 /tools/memory-model/linux-kernel.def | |
| parent | 648e717586f2a832687fe44e2e0afb7a6fdea232 (diff) | |
| download | linux-rt-9393998e9ee094f99d18783cc85c489e20f0e0e7.tar.gz | |
tools/memory-model: Dynamically check SRCU lock-to-unlock matching
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. ]
Acked-by: Alan Stern <stern@rowland.harvard.edu>
Diffstat (limited to 'tools/memory-model/linux-kernel.def')
| -rw-r--r-- | tools/memory-model/linux-kernel.def | 2 |
1 files changed, 1 insertions, 1 deletions
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 |