summaryrefslogtreecommitdiffstats
path: root/tools/memory-model/linux-kernel.cat
diff options
context:
space:
mode:
authorLuc Maranget <Luc.Maranget@inria.fr>2018-12-27 16:27:12 +0100
committerPaul E. McKenney <paulmck@linux.ibm.com>2019-03-18 10:27:52 -0700
commit9393998e9ee094f99d18783cc85c489e20f0e0e7 (patch)
treeb2d6cea2bd7343fa600a53c6269496d0bea91be1 /tools/memory-model/linux-kernel.cat
parent648e717586f2a832687fe44e2e0afb7a6fdea232 (diff)
downloadlinux-9393998e9ee094f99d18783cc85c489e20f0e0e7.tar.gz
linux-9393998e9ee094f99d18783cc85c489e20f0e0e7.tar.bz2
linux-9393998e9ee094f99d18783cc85c489e20f0e0e7.zip
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.cat')
-rw-r--r--tools/memory-model/linux-kernel.cat2
1 files changed, 2 insertions, 0 deletions
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>,