diff options
| author | Alan Stern <stern@rowland.harvard.edu> | 2019-04-22 19:18:09 +0300 |
|---|---|---|
| committer | Paul E. McKenney <paulmck@linux.ibm.com> | 2019-05-28 18:18:21 +0300 |
| commit | 0031e38adf38779acce5737f4905b9f60750b674 (patch) | |
| tree | 39190cc686db2933c0e8891fed8b3fc77a7c9233 /tools/memory-model/linux-kernel.def | |
| parent | d1a84ab190137cc2a980b6979b1f2790d51b2d87 (diff) | |
| download | linux-0031e38adf38779acce5737f4905b9f60750b674.tar.xz | |
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.def')
| -rw-r--r-- | tools/memory-model/linux-kernel.def | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index 551eeaa389d4..ef0f3c1850de 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -24,6 +24,7 @@ smp_mb__before_atomic() { __fence{before-atomic}; } smp_mb__after_atomic() { __fence{after-atomic}; } smp_mb__after_spinlock() { __fence{after-spinlock}; } smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; } +barrier() { __fence{barrier}; } // Exchange xchg(X,V) __xchg{mb}(X,V) |