diff options
Diffstat (limited to 'tools/memory-model')
| -rw-r--r-- | tools/memory-model/linux-kernel.bell | 3 | ||||
| -rw-r--r-- | tools/memory-model/linux-kernel.cat | 2 | ||||
| -rw-r--r-- | tools/memory-model/linux-kernel.def | 2 |
3 files changed, 6 insertions, 1 deletions
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 |