tools/memory-model Flag suspicious use of srcu cookies
The herd model of LKMM deviates from actual implementations in the
range of cookies that might be returned by srcu_read_lock() and
similar functions. As a consequence, code that makes special use of
values returned by srcu_read_lock() might pass in herd but fail in the
real world.
This patch flags any code that looks at the value of a cookie without
passing it on to an srcu_read_unlock(). This indicates that the cookie
value might be being used in ways that can lead herd to produce incorrect
results, as in the following (contrived) case:
P0(struct srcu_struct *ss)
{
int r = srcu_read_lock(ss);
if (r==0)
srcu_read_unlock(ss, r);
}
Without this patch, the above code passes herd7 without any warnings.
However, real-world use of this code could result in SRCU grace-period
hangs.
With this patch, this code is flagged with illegal-srcu-cookie-ctrl,
indicating that a cookie is used to compute a control condition.
Real-world use of such code can result in executions that herd7 does
not evaluate. In this example, when srcu_read_lock() returns a non-zero
value, there is no matching srcu_read_unlock(), which (as noted above)
would result in calls to synchronize_srcu() never returning.
Besides use of cookies in control conditions, the patch also flags use
in address computation and any time a cookie is inspected but not later
passed to srcu_read_unlock().
Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Acked-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
1 file changed
