Skip to content
Commit 0031e38a authored by Alan Stern's avatar Alan Stern Committed by Paul E. McKenney
Browse files

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: default avatarAlan Stern <stern@rowland.harvard.edu>
Reviewed-by: default avatarAndrea Parri <andrea.parri@amarulasolutions.com>
Signed-off-by: default avatarPaul E. McKenney <paulmck@linux.ibm.com>
parent d1a84ab1
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment