OSDN Git Service

tools/memory-model: Add data-race detection
authorAlan Stern <stern@rowland.harvard.edu>
Mon, 22 Apr 2019 16:18:09 +0000 (12:18 -0400)
committerPaul E. McKenney <paulmck@linux.ibm.com>
Tue, 28 May 2019 15:18:21 +0000 (08:18 -0700)
commit0031e38adf38779acce5737f4905b9f60750b674
tree39190cc686db2933c0e8891fed8b3fc77a7c9233
parentd1a84ab190137cc2a980b6979b1f2790d51b2d87
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>
tools/memory-model/linux-kernel.bell
tools/memory-model/linux-kernel.cat
tools/memory-model/linux-kernel.def