From 9393998e9ee094f99d18783cc85c489e20f0e0e7 Mon Sep 17 00:00:00 2001 From: Luc Maranget Date: Thu, 27 Dec 2018 16:27:12 +0100 Subject: 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 Signed-off-by: Paul E. McKenney [ paulmck: Apply Andrea Parri's off-list feedback. ] Acked-by: Alan Stern --- tools/memory-model/linux-kernel.def | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools/memory-model/linux-kernel.def') 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 -- cgit v1.2.3