summaryrefslogtreecommitdiffstats
path: root/tools/memory-model/linux-kernel.bell
diff options
context:
space:
mode:
Diffstat (limited to 'tools/memory-model/linux-kernel.bell')
-rw-r--r--tools/memory-model/linux-kernel.bell3
1 files changed, 3 insertions, 0 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