Colloquium Details
Types for Atomicity
| Author: | Cormac Flanagan Systems Research Center, Hewlett Packard Laboratories |
|---|---|
| Date: | February 13, 2003 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
Abstract
Developing correct multithreaded programs is extremely challenging, due to the potential for unintended and nondeterministic interference between threads. A crucial concept for controlling this interference is the notion of atomicity: a function is considered atomic if its behavior is not influenced by the actions of concurrent threads. Atomicity is often achieved using mutual-exclusion locks, and atomic functions are much easier to reason about, since the effect of nondeterministically interleaved actions of other threads can be safely ignored.
In practice, many functions in multithreaded programs are designed to be atomic and their documentation claims that they are atomic. However, because of the difficult of correctly reasoning about multithreaded programs, these claimed atomicity properties are unreliable and often incorrect.
This talk presents the Java Atomicity Checker, a static analysis tool that focuses on specifying and verifying the atomicity of methods and classes in multithreaded Java programs. This tool has caught a number of subtle timing-dependent defects, even in widely used and well-tested library classes such as java.lang.String and java.lang.StringBuffer. These previously unknown defects may cause programs to crash in a nondeterministic and irreproducible manner.
Biography
Prof. Flanagan received his Ph.D. from Rice University in 1997; M.S. from Rice University, 1995; B.S. from University College, Dublin, Ireland, 1990. Research Interests: All aspects of programming languages and software engineering, with an emphasis on specifying and checking correctness properties of sequential, multi-threaded, and distributed programs.