Thread Safety Annotations and Analysis (aka Annotalysis)

Status update 2012-04-19: Google will no longer develop this project in GCC.

Background

Multi-threading is an increasingly important technique to boost performance on multi-core/multiprocessor systems. Unfortunately, multi-threaded programming is hard: timing-dependent bugs, such as data races and deadlocks, are very difficult to expose in testing and hard to reproduce and isolate once discovered. Proper documentation of synchronization policies and thread safety guarantees is probably one of the most useful techniques to manage multi-threaded code and avoid concurrency bugs. In practice, programmers' intended synchronization policies, such as lock acquisition order and lock requirement for shared variables and functions, are often documented in comments. Comments help maintainers avoid introducing errors, but it is hard for program analysis tools to use the information to tell programmers when they have violated their synchronization policies and identify potential thread safety issues. Therefore this project creates program annotations for C/C++ to help developers document locks and how they need to be used to safely read and write shared variables. We design and implement a new GCC pass that uses the annotations to identify and warn about the issues that could potentially result in race conditions and deadlocks.

Design Doc

This document describes the proposed design. All the work is being done on the SVN branch annotalysis. (Note that the old branch thread-annotations is deprecated and no longer maintained.)

We are also working on emitting the annotations in DWARF format in the binary files so that other dynamic/static analysis tools can make use of the information. The design doc of the new DWARF extension is located at ThreadSafetyAnnotationsInDWARF and here.

Branch Status (updated 2011-04-01)

To run the thread safety annotation specific test cases, do the following

$ make check-gcc RUNTESTFLAGS="dg.exp=thread_annot*"

When submitting patches to this branch, use the tag [annotalysis] in the subject line and cc Jeffrey Yasskin and Le-Chun Wu.

Contact

The annotalysis branch is currently maintained by Jeffrey Yasskin and Le-Chun Wu.

None: ThreadSafetyAnnotation (last edited 2012-04-19 14:18:30 by DiegoNovillo)