summaryrefslogtreecommitdiffstats
path: root/tools/memory-model/linux-kernel.bell
diff options
context:
space:
mode:
authorAlan Stern <stern@rowland.harvard.edu>2019-04-22 12:18:09 -0400
committerPaul E. McKenney <paulmck@linux.ibm.com>2019-05-28 08:18:21 -0700
commit0031e38adf38779acce5737f4905b9f60750b674 (patch)
tree39190cc686db2933c0e8891fed8b3fc77a7c9233 /tools/memory-model/linux-kernel.bell
parentd1a84ab190137cc2a980b6979b1f2790d51b2d87 (diff)
downloadlinux-0031e38adf38779acce5737f4905b9f60750b674.tar.bz2
tools/memory-model: Add data-race detection
This patch adds data-race detection to the Linux-Kernel Memory Model. As part of this effort, support is added for: compiler barriers (the barrier() function), and a new Preserved Program Order term: (addr ; [Plain] ; wmb) Data races are marked with a special Flag warning in herd. It is not guaranteed that the model will provide accurate predictions when a data race is present. The patch does not include documentation for the data-race detection facility. The basic design has been explained in various emails, and a separate documentation patch will be submitted later. This work is based on an earlier formulation of data races for the LKMM by Andrea Parri. Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Reviewed-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com>
Diffstat (limited to 'tools/memory-model/linux-kernel.bell')
-rw-r--r--tools/memory-model/linux-kernel.bell1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index b60eb5a01053..5be86b1025e8 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -24,6 +24,7 @@ instructions RMW[{'once,'acquire,'release}]
enum Barriers = 'wmb (*smp_wmb*) ||
'rmb (*smp_rmb*) ||
'mb (*smp_mb*) ||
+ 'barrier (*barrier*) ||
'rcu-lock (*rcu_read_lock*) ||
'rcu-unlock (*rcu_read_unlock*) ||
'sync-rcu (*synchronize_rcu*) ||