<div dir="ltr"><br><div><span style="font-family:arial,sans-serif;font-size:13px">> Delesley, does Clang's current lock-based analysis really have no</span><br style="font-family:arial,sans-serif;font-size:13px"><span style="font-family:arial,sans-serif;font-size:13px">> support for the annotation "No thread can hold both the GUI lock and</span><br style="font-family:arial,sans-serif;font-size:13px">
<span style="font-family:arial,sans-serif;font-size:13px">> the Compute lock at the same time"? You could sort of simulate this by</span><br></div><div><span style="font-family:arial,sans-serif;font-size:13px"><br>
</span></div><div><span style="font-family:arial,sans-serif;font-size:13px">You might be able to hack it, but it would be ugly. For simple cases like this, </span></div><div><span style="font-family:arial,sans-serif;font-size:13px">though, we could </span><span style="font-family:arial,sans-serif;font-size:13px">even reuse the existing attributes, e.g. by allowing </span></div>
<div><span style="font-family:arial,sans-serif;font-size:13px">LOCKS_EXCLUDED </span><span style="font-family:arial,sans-serif;font-size:13px">on locks as well as functions:</span></div><div><span style="font-family:arial,sans-serif;font-size:13px"><br>
</span></div><div><span style="font-family:arial,sans-serif;font-size:13px">Mutex gui_lock LOCKS_EXCLUDED(compute_lock);</span></div><div><span style="font-family:arial,sans-serif;font-size:13px">Mutex compute_lock LOCKS_EXCLUDED(gui_lock);</span></div>
<div><span style="font-family:arial,sans-serif;font-size:13px"><br></span></div><div><font face="arial, sans-serif">I haven't implemented the checks to enforce this, but it would be pretty trivial to add. </font></div>
<div><span style="font-family:arial,sans-serif">More complicated </span><span style="font-family:arial,sans-serif">boolean expressions would be hard to express with the existing </span></div><div><span style="font-family:arial,sans-serif">attributes, though.</span></div>
<div><span style="font-family:arial,sans-serif"><br></span></div><div><span style="font-family:arial,sans-serif"> -DeLesley </span></div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Jun 24, 2013 at 12:01 PM, Arthur O'Dwyer <span dir="ltr"><<a href="mailto:arthur.j.odwyer@gmail.com" target="_blank">arthur.j.odwyer@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On Mon, Jun 24, 2013 at 11:16 AM, Delesley Hutchins <<a href="mailto:delesley@google.com">delesley@google.com</a>> wrote:<br>
><br>
</div><div class="im">> In particular, I believe that "lock" and "role" are essentially the same<br>
> thing. In both cases, the analysis is marking functions and data structures<br>
> as being "protected" by a particular lock/role, and ensuring that a thread<br>
> must hold/have the lock/role before calling protected functions, or<br>
> accessing protected data.<br>
<br>
</div>Dean, perhaps you could expand on how your "roles" fundamentally<br>
differ from "locks"; e.g. how is the statement "Thread A has the GUI<br>
role" fundamentally different from "Thread A notionally holds the GUI<br>
write-lock"; how is "Thread B has the Compute role" fundamentally<br>
different from "Thread B notionally holds a Compute read-lock"?<br>
<div class="im"><br>
> That said, you did point out some useful missing features, which are:<br>
><br>
>> We support more complex boolean expressions over thread roles. The<br>
>> existing Clang annotations cannot express multiple combinations of<br>
>> such properties. For example, ((A & B & !C) | (D & !E)).<br>
><br>
> As you mention, the existing analysis does not support this case. However,<br>
> this functionality would not be hard to add -- it's simply a boolean<br>
> constraint on allowable lock sets. If you feel it's valuable, then let's do<br>
> that!<br>
<br>
</div>For reference, Dean gave an example of an (!A | !B) constraint that<br>
seems very valuable:<br>
<div class="im"><br>
Dean Sutherland wrote:<br>
>> * TRA allows statements that certain thread roles are mutually<br>
>> exclusive (a GUI thread can't be a Compute thread, and vice<br>
>> versa). The Clang annotations lack support for this property.<br>
<br>
</div>Delesley, does Clang's current lock-based analysis really have no<br>
support for the annotation "No thread can hold both the GUI lock and<br>
the Compute lock at the same time"? You could sort of simulate this by<br>
annotating the invariants "Whenever you call the function lock_GUI(),<br>
you must not hold the Compute lock" and "Whenever you call the<br>
function lock_Compute(), you must not hold the GUI lock", but that's<br>
quite ugly, and also supposes that functions analogous to lock_GUI()<br>
and lock_Compute() exist for every role, which is probably false.<br>
<div class="im"><br>
Dean Sutherland wrote:<br>
>> If this statement requires user-written annotations for all such<br>
>> methods, the required annotation effort will make adoption exceedingly<br>
>> difficult for most practicing programmers. One of the benefits of TRA<br>
>> is the application of well-founded techniques to avoid the need for<br>
>> most user-written annotations. Perhaps some of these techniques could<br>
>> be brought to bear on the existing thread safety analysis.<br>
<br>
</div>Dean, how does this work? Don't you need annotations somewhere to tell<br>
the analyzer what counts as a "GUI method", for example? You're saying<br>
that Clang's current analyzer would require a ton of annotation to<br>
mark all the GUI methods, which IMHO is true; but how would your<br>
solution avoid that burden?<br>
<br>
my $.02,<br>
–Arthur<br>
</blockquote></div><br><br clear="all"><div><br></div>-- <br>DeLesley Hutchins | Software Engineer | <a href="mailto:delesley@google.com" target="_blank">delesley@google.com</a> | 505-206-0315<br>
</div>