[cfe-dev] [RFC] Adding Thread Role Analysis

[Delesley Hutchins]

> Delesley, does Clang's current lock-based analysis really have no
> support for the annotation "No thread can hold both the GUI lock and
> the Compute lock at the same time"? You could sort of simulate this by

You might be able to hack it, but it would be ugly.  For simple cases like
this,
though, we could even reuse the existing attributes, e.g. by allowing
LOCKS_EXCLUDED on locks as well as functions:

Mutex gui_lock  LOCKS_EXCLUDED(compute_lock);
Mutex compute_lock  LOCKS_EXCLUDED(gui_lock);

I haven't implemented the checks to enforce this, but it would be pretty
trivial to add.
More complicated boolean expressions would be hard to express with the
existing
attributes, though.

  -DeLesley



On Mon, Jun 24, 2013 at 12:01 PM, Arthur O'Dwyer
<arthur.j.odwyer at gmail.com>wrote:

> On Mon, Jun 24, 2013 at 11:16 AM, Delesley Hutchins <delesley at google.com>
> wrote:
> >
> > In particular, I believe that "lock" and "role" are essentially the same
> > thing.  In both cases, the analysis is marking functions and data
> structures
> > as being "protected" by a particular lock/role, and ensuring that a
> thread
> > must hold/have the lock/role before calling protected functions, or
> > accessing protected data.
>
> Dean, perhaps you could expand on how your "roles" fundamentally
> differ from "locks"; e.g. how is the statement "Thread A has the GUI
> role" fundamentally different from "Thread A notionally holds the GUI
> write-lock"; how is "Thread B has the Compute role" fundamentally
> different from "Thread B notionally holds a Compute read-lock"?
>
> > That said, you did point out some useful missing features, which are:
> >
> >> We support more complex boolean expressions over thread roles. The
> >> existing Clang annotations cannot express multiple combinations of
> >> such properties.  For example, ((A & B & !C) | (D & !E)).
> >
> > As you mention, the existing analysis does not support this case.
>  However,
> > this functionality would not be hard to add -- it's simply a boolean
> > constraint on allowable lock sets.  If you feel it's valuable, then
> let's do
> > that!
>
> For reference, Dean gave an example of an (!A | !B) constraint that
> seems very valuable:
>
> Dean Sutherland wrote:
> >> * TRA allows statements that certain thread roles are mutually
> >> exclusive (a GUI thread can't be a Compute thread, and vice
> >> versa). The Clang annotations lack support for this property.
>
> Delesley, does Clang's current lock-based analysis really have no
> support for the annotation "No thread can hold both the GUI lock and
> the Compute lock at the same time"? You could sort of simulate this by
> annotating the invariants "Whenever you call the function lock_GUI(),
> you must not hold the Compute lock" and "Whenever you call the
> function lock_Compute(), you must not hold the GUI lock", but that's
> quite ugly, and also supposes that functions analogous to lock_GUI()
> and lock_Compute() exist for every role, which is probably false.
>
> Dean Sutherland wrote:
> >> If this statement requires user-written annotations for all such
> >> methods, the required annotation effort will make adoption exceedingly
> >> difficult for most practicing programmers.  One of the benefits of TRA
> >> is the application of well-founded techniques to avoid the need for
> >> most user-written annotations.  Perhaps some of these techniques could
> >> be brought to bear on the existing thread safety analysis.
>
> Dean, how does this work? Don't you need annotations somewhere to tell
> the analyzer what counts as a "GUI method", for example? You're saying
> that Clang's current analyzer would require a ton of annotation to
> mark all the GUI methods, which IMHO is true; but how would your
> solution avoid that burden?
>
> my $.02,
> –Arthur
>



-- 
DeLesley Hutchins | Software Engineer | delesley at google.com | 505-206-0315
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20130624/40bad772/attachment.html>