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

[Richard Smith]

On Sun, Jul 7, 2013 at 10:17 AM, Dean Sutherland <dsutherland at cert.org> wrote:
> First an overall point that seems worthy of emphasis: Of course we intend to share as much with existing annotations and machinery as is plausible, diverging only where it makes sense.  Meanwhile, we appear to be wrestling over "where does it make sense to diverge?" After reading your feedback, it seems that I've succeeded in getting across the similarities between Thread Role Analysis (TRA, hereafter) and Lock Analysis (LA, hereafter), but I've failed to make the differences clear. That failure has led to a misunderstanding of the issues involved.
>
> This message focuses on two user-visible aspects of the analysis, regarding the annotations and use-cases.
> (1) Similarity in form isn't a good enough argument *by itself* to force similar things to be the same. Providing tools that match their expressive metaphor to the user's mental model *really matters* for adoptability. If this weren't true, we'd have only one programming language rather than many.
> (2) TRA and LA are optimized for different problems and express different mental models.
>
> Until we reach agreement on these user-visible issues, there's not much point in discussing implementation issues, so I'm deferring discussion of implementation issues to subsequent messages.

>From my perspective, this discussion is taking place one level of
abstraction too high. What you describe as user-visible issues are,
from my perspective, philosophical issues. I think the actual
user-visible issues are:

  1) What is the interface for annotating my code for LA or TRA?
  2) How do I enable the checking?
  3) Can I perform inference for the annotations, and if so, how?
  4) What form do the resulting diagnostics take?

I think the answers here are similar, but different, for TRA and LA:

(4) A high quality user experience would require different diagnostic
messages for TRA versus LA. We shouldn't tell users that they need to
acquire a lock if the real problem is that their thread doesn't have
the right role.
(1) The desired difference in diagnostics implies that the analysis
needs to know whether a region is guarded by a mutex or by a role,
which implies that the attributes used for the two cases are somehow
different.
(2) -Wthread-safety seems a reasonable warning flag for both cases.
(3) Any design for cross-function (and possibly
cross-translation-unit) attribute inference should really be the same
for both analyses. However, I strongly believe that any effort, or
even discussion, in this direction should be a separate topic from the
basic TRA annotations.

So I think the thing to discuss is, what should the concrete syntax
for specifying TRA annotations be? The obvious flavors of approach
seem to be:
 * just use the existing LA annotations as-is (this seems likely to be
suboptimal from a diagnostic-quality perspective)
 * use the existing LA annotations where possible, but add a minimal
set of additional attributes where necessary
 * add a new set of annotations parallel to the LA annotations
 * design a new set of annotations, for which both LA and TRA are
special cases, such that we can provide high-quality diagnostics for
both and present a consistent interface for them.

It's far from clear to me which of these you are proposing (and these
are just points on a continuum of options), so a much more specific
proposal would really help.