[cfe-dev] Thread Safety Analysis: negative capabilities and visibility

[Aaron Ballman]

On Tue, Aug 5, 2014 at 12:11 PM, Delesley Hutchins <delesley at google.com> wrote:
> TL;DR: ongoing discussion about thread safety analysis and deadlock
> prevention.  Posted to the list for the benefit of interested readers.
>
> The new negative capabilities patch (r214789) solves a long-standing
> problem whereby LOCKS_EXCLUDED was not transitive.  For example,
> assume you have the following:
>
> Mutex mu;
> void a() { mu.lock(); b(); mu.unlock(); }
> void b() { c(); }
> void c() LOCKS_EXCLUDED(mu);
>
> There is no warning in this code, because a() does not call c()
> directly, and even though b() calls a function that excludes mu, it
> does not have to exclude mu itself (although it should).  Negative
> capabilities solve this problem by propagating a negative requirement
> (a requirement that mu is not held) in the same way as an ordinary
> requirement, so if we change c() to:
>
> void c() REQUIRES(!mu);
>
> Then b() must also declare REQUIRES(!mu) to avoid a warning, and then
> we get a warning in a(), which is what we want, because a() calls b()
> with mu held.
>
> However, there is no way to acquire a negative capability.  In other
> words, you cannot prove to the analysis that mu is *not* held, except
> by putting a REQUIRES(!mu) on the calling function.  Thus, an
> attribute like REQUIRES(!mu) will simply propagate outwards, up the
> call graph.  At some point, we want to stop the propagation; otherwise
> every function will have to exclude all of the mutexes that might be
> acquired by anything it calls, which is not feasible.
>
> Right now, I stop the propagation at the boundary of the enclosing
> class.  Thus, every class method must exclude mutexes that are local
> to the class, but a method does not have to exclude mutexes that are
> declared in other classes.  This is overly conservative because it
> does not consider (1) public or protected mutexes inherited from base
> classes (2) mutexes in friend classes, or (3) global mutexes.
>
> Aaron has written a patch that uses the normal C++ rules for
> visibility -- e.g. a function must exclude any mutex that is publicly
> visible from the current scope.  At first, that made sense to me, but
> now I'm afraid it might extend visibility too far, because public and
> global mutexes would still propagate everywhere.
>
> Global mutexes in particular are a problem, because C++ does not have
> any way to restrict the visibility of a global variable to a single
> "module." Global mutexes are frequently declared within a header file,
> and then used within multiple translation units.  Moreover, deadlock
> prevention in such cases is important.  Because visibility of the
> mutex extends so far, it is easy to acquire the same mutex twice,
> which is what the negative capability is supposed to prevent.  On the
> other hand, we don't want the mutex to be visible outside of the scope
> in which it is used, even if the "scope" is poorly-defined.
>
> The same holds true for a protected mutex in a base class that is
> inherited by many derived classes.  Should the mutex be regarded as
> visible, or not?
>
> I'm looking for any ideas.  Should I add a new attribute to control
> visibility of mutexes?

Once there's a requirement that mu not be held, anywhere mu is visible
would need to be analyzed, which could require cross-TU analysis and
be a rather hard problem to solve with our current architecture. So I
agree that propagation is problematic here.

I think one thing we could do is when seeing REQUIRES(!mu), we test
mu's visibility and if it can escape the TU, diagnose on that usage.
Eg) static file-scope mu we can possibly track. class private mu we
can track. protected, public, global mu... I don't see that being
feasible to track without false positives, so we should tell the user
"sorry, we can't support this requirement fully, but we'll try our
best." That at least sets the user's expectations, though it doesn't
help them too much.

I'm not certain how a new visibility attribute would help; could you
describe what you were thinking of a bit more?

Thanks!

~Aaron