FindLocks is an approach for automatically proving the absence of data races in multi-threaded Java programs, using a combination of dynamic and static analysis. The program in question is instrumented so that when executed it will gather information about locking relationships. This information is then used to automatically generate annotations needed to type check the program using the Race-Free Java type system. Programs that type check are sure to be free from races. We call this technique \emph{dynamic annotation inference.
We have found that when using a reasonably comprehensive test suite, which is easy for small programs but harder for larger ones, the approach generates annotations that allows the program to typecheck under Race-Free Java.
A beta release of the tool is available here. We're working on adding support for the RFJ2 type system. The greater expressivity of RFJ2 should allow us to emit more precise annotations.
Our paper is available here.
| People: | James Rose, Nikhil Swamy, Michael Hicks |