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

Sun Jul 3 02:48:23 PDT 2011

Hi Chris,

I sent you a presentation which describes the project design and some of its implementation details, please check.

Also Francesco is collaborating with Vikram’s group at UPCRC to evaluate to use our tool as a base for the deterministic parallel C++ project (http://dpj.cs.uiuc.edu/DPJ/Future_Directions.html), which devises a set of annotations to document low level properties of functions in a more finely grained approach than our “high level” annotation of function properties like reentrancy. Francesco can provide more details if you are interested.

Cheers
~Michael

From: Chris Lattner [mailto:clattner at apple.com]
Sent: Sunday, July 03, 2011 4:12 AM
To: Michael Han
Cc: Caitlin Sadowski; cfe-dev at cs.uiuc.edu; Delesley Hutchins; Jaeheon Yi; Jeffrey Yasskin; cormac at cs.ucsc.edu; Benoit Belley; Francesco Iorio
Subject: Re: [cfe-dev] Proposal for thread safety attributes for Clang

Hi Michael,

This sounds very interesting.  Do you have any documentation that explains the model that this exposes to programmers?

-Chris

On Jun 30, 2011, at 11:37 PM, Michael Han <Michael.Han at autodesk.com<mailto: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> [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<mailto:cfe-dev at cs.uiuc.edu>; Delesley Hutchins; Jaeheon Yi; Jeffrey Yasskin; cormac at cs.ucsc.edu<mailto: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.
_______________________________________________
cfe-dev mailing list
cfe-dev at cs.uiuc.edu<mailto:cfe-dev at cs.uiuc.edu>
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20110703/05619574/attachment.html>