We present an approach for automatically proving the absence of race conditions 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 fed to our tool, FindLocks, that generates annotations needed to type check the program using the Race-Free Java type system. Our approach extends existing inference algorithms by being fully context-sensitive. We describe the design and implementation of our approach, and our experience applying the tool to a variety of Java programs. In general, we have found the approach works well, but has trouble scaling to large programs, which require extensive testing for full coverage.

[ .pdf ]

@inproceedings{rose04dynamic,
  author = {James Rose and Nikhil Swamy and Michael Hicks},
  title = {Dynamic Inference of Polymorphic Lock Types},
  booktitle = {Proceedings of the {ACM} Conference on Principles of Distributed Computing (PODC) Workshop on Concurrency and Synchronization in Java Programs (CSJP)},
  pages = {18--25},
  month = {July},
  year = 2004
}

This file was generated by bibtex2html 1.99.