<div dir="ltr">You don't seem to have addressed how this interacts with the *existing* thread safety analysis in Clang. I think you'll need to do that. I've CC-ed folks in the Clang community already working on these things. =]</div>
<div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Jun 20, 2013 at 2:03 PM, Aaron Ballman <span dir="ltr"><<a href="mailto:aaron@aaronballman.com" target="_blank">aaron@aaronballman.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello!<br>
<br>
We at CERT are interested in adding thread role analysis support (also<br>
known as thread coloring) to clang.  This email is meant to briefly<br>
introduce the subject and then open up to the community for comments.<br>
<br>
Thread role analysis (or TRA), allows programmers to express their<br>
thread usage policies in source code using simple and concise<br>
annotations.  A static analyzer can check whether the expressed<br>
policies and the as-written code are consistent, ensuring that the<br>
annotated contract remains effective.<br>
<br>
We've worked extensively with--and have demonstrated the utility<br>
of--TRA for Java, including analyzing and finding significant problems<br>
in dozens of fielded applications ranging from toy applets to<br>
multi-million LOC commercial applications.  As part of that prior work<br>
we demonstrated:<br>
* Required annotation density (for Java) of ~6 annotations per KLOC<br>
(and a design that should permit reducing this to <1 annotation per<br>
KLOC)<br>
* Composability of the analysis<br>
* Adoptability by working programmers<br>
* Capability to analyze large programs (>150KLOC in a single chunk;<br>
multi-million LOC in multiple chunks)<br>
* The annotation language and analysis suffice for analyzing a wide<br>
variety of real programs<br>
<br>
Publications regarding our previous work with TRA for Java include:<br>
* PPoPP'10 paper (best short introduction) --<br>
<a href="http://www.fluid.cs.cmu.edu:8080/Fluid/fluid-publications/p233-sutherland.pdf" target="_blank">http://www.fluid.cs.cmu.edu:8080/Fluid/fluid-publications/p233-sutherland.pdf</a><br>
* Ph.D. Dissertation (all the gory details, but LONG) --<br>
<a href="http://reports-archive.adm.cs.cmu.edu/anon/isr2008/abstracts/08-112.html" target="_blank">http://reports-archive.adm.cs.cmu.edu/anon/isr2008/abstracts/08-112.html</a><br>
* Blog post -- <a href="http://blog.sei.cmu.edu/post.cfm/thread-role-analysis" target="_blank">http://blog.sei.cmu.edu/post.cfm/thread-role-analysis</a><br>
<br>
Thread usage policies describe what kinds of threads ("thread roles")<br>
are permitted to invoke particular functions or methods.  TRA can be<br>
used to enforce a wide variety of policies including (but not limited<br>
to):<br>
* Single-thread-only (e.g., use of threads is forbidden)<br>
* Restricting use of GUI methods to the GUI event thread<br>
* Ensuring that threads engaged in reader-writer locking restrict<br>
themselves to calls that are consistent with their role -- e.g.,<br>
readers never attempt to write and outside threads neither read nor<br>
write.<br>
* Ensuring that llvm Function passes never invoke llvm Module passes<br>
(note that this would require C++ support; initial phases of this<br>
project involve C only)<br>
<br>
When combined with a sufficiently-powerful effects analysis, TRA can<br>
also be applied to data objects. In this mode, it can be used to<br>
either (1) prove thread confinement of data (which then need not be<br>
locked), or (2) identify data that is potentially shared across<br>
threads (and consequently requires concurrency control of some sort).<br>
However, we are not aware of a suitable effects analysis for C or C++,<br>
and consequently have no current plans to address this capability.<br>
<br>
In principle, TRA can be performed entirely one translation-unit at a<br>
time. However, this approach requires unrealistic numbers of<br>
user-written annotations.  Past research has demonstrated that TRA is<br>
most effective (in terms of bang for the end-user's effort) when<br>
performed over large groups of translation units. In this mode, we<br>
require annotations on the interfaces between groups of TUs, and infer<br>
annotations within each group.  The potential for using Modules (or<br>
something similar) should be obvious. Note that the cost of the<br>
analysis is O(n) in program size in the typical case.<br>
<br>
We realize that this RFC doesn't touch on implementation details (we<br>
wanted to spare you the wall of text).  However, we're happy to<br>
discuss our envisioned implementation strategy if you have any<br>
questions.  We propose to proceed by giving small RFCs on<br>
implementation details which may require us to introduce new concepts,<br>
but otherwise go with post-commit reviews for the majority of the<br>
work.<br>
<br>
Our implementation strategy from 50,000 feet:<br>
* Start by supporting C (only).<br>
* Begin adding C++ support in US Govt. FY14 (starting Oct. 1, 2013)<br>
* Add new declaration attributes<br>
* Add new statement attributes and round out the statement attribute subsystem<br>
* Emit YAML-based sidecar files (either during compilation or from the<br>
Static Analyzer)<br>
* Produce a utility application to read the sidecar files, perform the<br>
analysis, and produce results.<br>
* Add a static analyzer pass which reads the results and emits diagnostics<br>
<br>
Our Team:<br>
Dr. Dean Sutherland and I work for the securing coding group at CERT<br>
(within the Software Engineering Institute of Carnegie Mellon<br>
University) and will be the primary people working on<br>
implementing thread role analysis.  We are funded to develop and<br>
maintain this system for at least the next 16 months. You can find<br>
more information about CERT and the secure coding group at:<br>
<a href="http://www.cert.org/secure-coding/" target="_blank">http://www.cert.org/secure-coding/</a>.<br>
<br>
~Aaron<br>
_______________________________________________<br>
cfe-commits mailing list<br>
<a href="mailto:cfe-commits@cs.uiuc.edu">cfe-commits@cs.uiuc.edu</a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits</a><br>
</blockquote></div><br></div>