[cfe-dev] Proposal for thread safety attributes for Clang

[Delesley Hutchins]

An extensible annotation framework would indeed be very useful.  One
of my long-term goals for the project is to implement something along
the lines of "pluggable type systems", e.g.

http://portal.acm.org/citation.cfm?id=1167479
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.87.9425&rep=rep1&type=pdf

in which various forms of static analysis could be implemented as
independent "type-checking" passes which make use of annotations in
the source code.  Such a system would require an extensible annotation
framework, along the lines of what you are describing.

Our more immediate goal, of course, is to add support for a particular
set of annotations, and a particular form of analysis, which is
already used in a number of important projects here at Google.  Once
that has been implemented, we can look at how best to generalize it.

  -DeLesley

On Thu, Jun 30, 2011 at 11:37 PM, Michael Han <Michael.Han at autodesk.com> wrote:
> We have implemented a tool based on clang at Autodesk to help developers
> express their design decisions. The basic idea is the design decisions
> implemented as a set of customized GNU style attributes can serve as metadta
> to the fuctions, classes, etc and these metadata could be checked by clang
> static analyzer to enforce specific data access pattern and call graph for
> functions. We use this tool to help us parallelize some of our legacy C++
> code base, for example, by enforcing a specific code is purely functinal
> style thus by definition is trivially thread safe.
>
>
>
> Our implementation touches many pieces of clang as we don’t find a less
> intrusive way to get the attributes / metadata into clang’s type system and
> AST. As a result we have to periodically merge our code base with Clang
> official trunk, which sometimes is quite touch. The checker is easy to write
> as it is very well decoupled from the rest of the system.
>
>
>
> I am wondering if this project would lead to an extensible annotation
> framework for Clang so user could encode arbitary metadata into Clang AST.
> That would be very useful and powerful for analysis code as it would involve
> develpers more intimately by capturing the design decisions eariler.
>
>
>
> Cheers
>
> ~Michael
>
> From: cfe-dev-bounces at cs.uiuc.edu [mailto:cfe-dev-bounces at cs.uiuc.edu] On
> Behalf Of Caitlin Sadowski
> Sent: Friday, July 01, 2011 8:58 AM
> To: cfe-dev at cs.uiuc.edu; Delesley Hutchins; Jaeheon Yi; Jeffrey Yasskin;
> cormac at cs.ucsc.edu
> Subject: [cfe-dev] Proposal for thread safety attributes for Clang
>
>
>
> The following is a proposal for a project we would like to contribute to
> Clang. Feel free to discuss.
>
>
>
> Cheers,
>
> Caitlin Sadowski
>
> Google & University of California at Santa Cruz
>
>
>
> Thread Safety Attributes for Clang
>
> Summary
>
> We would like to add a set of thread safety attributes to Clang. These
> attributes, based on a prior GCC implementation, will allow for checkable
> documentation of basic locking policies in multithreaded programs.
>
> Background
> The synchronization policies in modern multithreaded code may be poorly
> documented, and incorrectly inferred by new developers. Furthermore, when
> these policies are improperly followed they often lead to bugs which are
> difficult to reproduce and diagnose. One strategy for avoiding concurrency
> bugs is formal documentation of these synchronization policies. By writing
> this documentation using attribute-based annotations, Clang can mechanically
> check and warn about issues that could potentially result in race conditions
> and deadlocks.
>
> Example
>
> A code sample which demonstrates two of the proposed annotations is below.
> In this code sample, variables are protected by locks from the Mutex class.
> This class has been annotated to specify the API used to lock and unlock.
>
> * GUARDED_BY specifies a particular lock should be held when accessing the
> annotated variable. Violations of this locking policy may lead to data
> races.
> *  ACQUIRED_AFTER annotations document the acquisition order between locks
> that can be held simultaneously by a thread, by specify the locks that need
> to be acquired before the annotated lock. Violations of this locking policy
> may lead to deadlocks.
>
>  1 #include "thread_annotations.h"
>  2 #define GUARDED_BY(x) __attribute__((GUARDED_BY(x)))
>  3 #define ACQUIRED_AFTER(x) __attribute__((ACQUIRED_AFTER(x)))
>  4
>  5 Mutex mu1;
>  6 Mutex mu2 ACQUIRED_AFTER(mu1);
>  7
>  8 int x GUARDED_BY(mu1);
>  9 int a GUARDED_BY(mu2);
>  10
>  11 void foo()
>  12 {
> 13   mu2.Lock();
> 14   mu1.Lock();
> 15   if (x > 2)
> 16     a = x + 1;
> 17   else
> 18     a = x - 1;
> 19   mu1.Unlock();
> 20   mu2.Unlock();
> 21 }
>
> Sample compiler output:
> ex.cc: In function 'void foo()':
> ex.cc:12: warning: Lock 'mu1' is acquired after lock 'mu2' (acquired at line
> 14) but is annotated otherwise
>
> Previous Work
>
> As mentioned, thread safety annotations have been implemented in GCC. A full
> list of the annotations and descriptions for them can be found here:
>
> http://gcc.gnu.org/wiki/ThreadSafetyAnnotation
> https://docs.google.com/a/google.com/Doc?id=ddqtfwhb_0c49t6zgr
>
> These annotations have been in active use in Google’s C++ codebase for a
> couple of years, so there is a large informal case study of their
> usefulness. The ideas behind many of these annotations come originally from
> a research paper [1].
>
> Plan
>
> We are planning to re-implement the GCC thread safety attributes in Clang.
> We will submit a series of patches to the cfe-commits mailing list. Our
> current plan for this serie is as follows:
>
> 1) Basic parsing and semantic checking of the attributes which do not take
> arguments. In other words, checking whether the attribute is applied in the
> appropriate context (e.g. to a field, with no arguments).
> 2) Basic parsing and semantic checking of the attributes which do take
> arguments, but without parsing or checking the arguments themselves. At this
> point, we will simply discard the tokens making up the arguments.
> 3) Attribute argument parsing.
> 4) Adding the thread safety analysis checks. We will teach the static
> analysis-based warnings layer to warn for violations of the annotations
> discussed on the links above.
>
> Future Projects
>
> Once we have this core set of thread safety annotations implemented, we have
> several directions for future work we would like to pursue. These include
> supporting additional types of annotations. For example, we would like to
> extend the system to support annotations for functions which only touch
> thread-local data and atomic functions which always execute as if they are
> not interleaved with operations of other threads. We would also like to
> build an annotation inference system; this system would enable application
> of the thread safety analysis to large amounts of legacy code.
>
> [1] C. Flanagan and S. N. Freund. Type-based race detection for Java. In
> Programming Language Design and Implementation (PLDI), June 2000.

-- 
DeLesley Hutchins | Software Engineer | delesley at google.com | 505-206-0315