From 0031e38adf38779acce5737f4905b9f60750b674 Mon Sep 17 00:00:00 2001 From: Alan Stern Date: Mon, 22 Apr 2019 12:18:09 -0400 Subject: 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 Reviewed-by: Andrea Parri Signed-off-by: Paul E. McKenney --- tools/memory-model/linux-kernel.bell | 1 + 1 file changed, 1 insertion(+) (limited to 'tools/memory-model/linux-kernel.bell') 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*) || -- cgit v1.2.3